[GHC] #11948: GHC forgets constraints

[GHC]

#11948: GHC forgets constraints
-------------------------------------+-------------------------------------
        Reporter:  crockeea          |                Owner:
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:  8.0.2
       Component:  Compiler          |              Version:  7.10.3
      Resolution:                    |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  GHC rejects       |  Unknown/Multiple
  valid program                      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by simonpj):

 This is a very delicate example.  You have, roughly
 {{{
 class C a where
   op :: Int -> a

 instance C a => C [a] where ...

 f :: forall z. C [z] => blah
 f = ...(op 3 :: [z])....
 }}}
 So arising from the call to `op` we need to solve `C [z]`.  There are two
 ways to solve this:

 * From the `instance` declaration
 * From the `C [z] => ...` in the type signature for `f`

 If we choose the former, type checking will fail.  But generally speaking
 it is ''good'' to reduce class constraints using instance declarations.
 It's very odd to have a type signature that ''overlaps'' the instance.

 GHC makes some effort to get this "right", by prioritising solving against
 "givens", but it's a bit of a hopeless task.   After all, it might look
 like
 {{{
 f = ...(h (op 3))....
 }}}
 where after a great deal of constraint solving, functional dependencies,
 type function reduction, etc etc, we finally discover that `h`'s argument
 must have type `[z]`.

 In this particular case, GHC is trying to infer the most general type for
 `x`:
 {{{
   let x = bar sk :: Foo zq
 }}}
 Arising from `bar` we get the constraint `Bar (Foo (F sk)) (Foo sk)`.
 When inferring the most general type for `bar` we simplify the constraint
 as much as possible, using the class `instance` declaration.

 If you use `MonoLocalBinds` GHC does not attempt to generalise the type of
 `bar`.  So now the (still delicate) prioritisation scheme works, and the
 program compiles.  This why adding `TypeFamilies` helps: `TypeFamilies`
 implies `MonoLocalBinds`.

 Anyway the robust solution is to use the `instance` declaration to
 simplify the constraint for `bar`:
 {{{
 bug :: forall zq .
   (Bar (F zq) zq)
   => Foo (F zq) -> Foo zq
 }}}
 Maybe GHC should warn about type signatures that have constraints that are
 reducible with class `instance`s, since they are so fragile.  That would
 be a very worthwhile improvement.

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