This is a question about some interesting behaviors in GHC's typechecker regarding MPTCs. The brief code is at the bottom of the message. By the way, the types can be inferred but not declared without the forall and ascription in the where clause. f1 below is illegal because we don't know what type the result of read should be: it's type is ambigious. Why isn't f2 illegal as well? If C had a functional dependency of a -> b, then I could understand accepting the type. However, without the functional dependency, b might not necessarily be determined from a. i) The above reasoning encroaches on the magic of TypeCast, which effectively allows local functional dependencies to be declared at the instance-level. Because of this, the typeclass mechanism might effectively have a means of determining b from a without the class being explicitly decorated with the functional dependency. ii) Type errors where b really isn't determined by a are caught by the typechecker wherever f2's arguments are instantiated (at some usage site). This is convenient at times (it admits the uncertainty of the "might not necessarily") and annoying at others (debugging): perhaps there's a ghc switch to disallow this? If f2 is legal, why if f3 illegal? For some usage site of f3, the constraint C String b might allow b to be resolved given whatever instances of C are in effect. Is there a motivation for these behaviors? Are these sorts of cases discussed in the CHR/FD paper that motivated the coverage condition (which I have yet to read)? If ATs or GADTs would handle these situations differently, why so? Should FDs also handle these situations differently? Thanks for your time. class C a b where method :: a -> b {- illegal due to ambiguous variable f1 :: forall a . (Read a) => String -> () f1 x = () where _ = read x :: a -} -- legal, despite the lack of an FD (a -> b) on C f2 :: forall a b . (C a b) => a -> () f2 x = () where _ = method x :: b {- illegal due to none of the forall'd variables being "reachable" from the type proper f3 :: forall b . (C String b) => String -> () f3 x = () where _ = method x :: b -}