[GHC] #6134: Incorrect ambiguity error with functional dependencies

[GHC]

#6134: Incorrect ambiguity error with functional dependencies
----------------------------------------+-----------------------------------
    Reporter:  diatchki                 |       Owner:                           
        Type:  bug                      |      Status:  new                      
    Priority:  normal                   |   Milestone:                           
   Component:  Compiler (Type checker)  |     Version:  7.4.1                    
    Keywords:                           |          Os:  Unknown/Multiple         
Architecture:  Unknown/Multiple         |     Failure:  GHC rejects valid program
  Difficulty:  Unknown                  |    Testcase:                           
   Blockedby:                           |    Blocking:                           
     Related:                           |  
----------------------------------------+-----------------------------------
Changes (by simonpj):

  * difficulty:  => Unknown


Comment:

 Right. This check, on user type signatures, is ''purely'' there to report
 types that cannot possibly be used.  So for example we want to reject:
 {{{
 f :: C [a] => Int
 }}}
 The idea is there can be no legal calls to `f` because every call will
 give rise to an ambiguous constraint.  We could soundly omit the ambiguity
 check on type signatures entirely, at the expense of delaying ambiguity
 errors to call sites.

 But is every call to `f` ambiguous?  After all, we might have
 {{{
 intance C [a] where ...
 }}}
 at the call site.  So maybe that type is ok!  What about the
 quintessentially ambiguous type
 {{{
 f :: C a => Int
 }}}
 Well, with `UndecidableInstances` we could have
 {{{
 instance C a where ...
 }}}
 and now a call could be legal after all!  (But only with
 `UndecidableInstances`.

 So it's clear that the present check is too conservative (rejects
 perfectly ok programs).  Using the visible fundeps is also too
 conservative.  Consider
 {{{
 class C a b where ...
 class D a b | a -> b where ...
 instance D a b => C [a] b where...

 f :: C a b => a -> a
 }}}
 Here `f`'s type looks ambiguous in `b`, but here's a legal call:
 {{{
 ...(f [True])...
 }}}
 That gives rise to a `(C [Bool] beta)` constraint, and using the instance
 means we need `(D Bool beta)` and that fixes `beta` via `D`'s fundep!

 So I think the only types we can reject as definitely ambiguous are ones
 like this
 {{{
   f :: (Cambig, Cnonambig) => tau
 }}}
 where
  * `Cambig`, `Cnonambig` are each a set of constraints.
  * `fv(Cambig)` does not intersect `fv( Cnonambig => tau )`
  * The constraints in `Cambig` are all of form `(C a b c)` where a,b,c are
 type variables
  * `Cambig` is non-empty
  * `-XUndecidableInstances` is not on.

 That narrows the scope of the test considerably.  Make sense?

 Simon

-- 
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/6134#comment:1>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler