RE: ambiguity problem

 > 
 > GHC's rule (not documented I'm afraid) is this.  Consider the type
 > 
 >      f :: (C a b, D c c, E b c, F d) => a->a
 > 
 > 1. Find the free type variables of the part after the arrow, namely {a}.
 > 2. For any constraint that mentions any variable in the set, add to the
 > set
 >      any other variables mentioned in that constraint. For example,
 > (C a b)
 >      mentions a, so add b to the set, giving {a,b}
 > 3. Repeat step 2 to a fixed point.  For example, (E b c) mentions b, so
 > add c to
 >      the set, giving {a,b,c}
 > 4.  Any constraint that mentions type variables not in the set is
 > definitely ambiguous.
 >      In this example, the only definitely ambiguous constraint is (F
 > d)
 > 
 > 
 > This rule is pretty lax.  It allows many functions that are probably
 > ambiguous to pass.  But that's ok because YOU'LL GET A TYPE ERROR WHEN
 > YOU CALL THE FUNCTION.  For example, GHC permits 
 >      g :: Foo a b => a
 >      g = undefined
 > but when you call it (say (g :: Int)), you'll get a complaint "cant
 > satisfy constraint 
 > (Foo Int b)".
 > 
 > Failing to reject an ambiguous type signature may defer type errors but
 > it's perfectly sound.  GHC therefore only rejects *absoulutely
 > definitely* ambiguous type signatures, leaving the others for the call
 > sites.
 > 
 > This should really be documented, I suppose.
 > 

I see. Take a look at 

http://www.comp.nus.edu.sg/~sulzmann/chr/download/full.ps
(this is still the old version)

p22, Lemma 10

"Under the assumption that C=>t is unambiguous, we know that at any
possible instantiation site (where we ground t), the instantiated
constraint C can be reduced to True."

The important part is that

Property A:

Whenever we instantiate a type scheme,
the instantiated constraints must (eventually, because we can
only run main if its type is monomorphic) be reducible to True.
This is enough to ensure coherence.

Note that unambiguity is a sufficient but not necessary
condition to enforce property A. In essence, ghc implements a
sufficient check (weaker than unambiguity) to enforce property A.


Martin