[Haskell-cafe] ambiguous type variables at MPTC

[Nicolas Frisby]

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
-}