[GHC] #9269: Type families returning quantified types

[GHC]

#9269: Type families returning quantified types
-------------------------------------+------------------------------------
        Reporter:  pumpkin           |            Owner:
            Type:  feature request   |           Status:  new
        Priority:  normal            |        Milestone:
       Component:  Compiler          |          Version:  7.8.2
      Resolution:                    |         Keywords:
Operating System:  Unknown/Multiple  |     Architecture:  Unknown/Multiple
 Type of failure:  None/Unknown      |       Difficulty:  Unknown
       Test Case:                    |       Blocked By:
        Blocking:                    |  Related Tickets:
-------------------------------------+------------------------------------

Comment (by goldfire):

 It depends on how "fundamental" a reason you want.

 Consider this:

 {{{
 type family Foo (x :: Bool) where
   Foo True = forall a. a -> a -> a
   Foo False = ()

 data SBool :: Bool -> * where
   STrue :: SBool True
   SFalse :: SBool False

 bar :: SBool b -> Foo b -> ()
 bar STrue x = (x 'a' 'b', x True False) `seq` ()
 bar SFalse x = x
 }}}

 It seems to be that it would be reasonable to expect the above code to
 typecheck, if we're allowed to write a family `Foo`. But, getting this to
 work wreaks havoc with the way GHC's typechecker is built.

 GHC walks over a term and builds up a set of constraints. For example, if
 the term is something like `z True`, then GHC will decide that `z` has
 type `alpha`, for some unknown type `alpha`. Then, it says that we must
 have `alpha ~ (beta -> gamma)`, from the fact that `z` is in a function
 position. We then see that `beta ~ Bool` from the type of `True`. After
 walking over an entire term, GHC then solves these constraints, in this
 case getting that the type of `z` must be `(Bool -> gamma)`.

 The crucial problem in the code above is that this algorithm runs into
 trouble on the RHS of the first clause of `bar`. GHC will see that `x` is
 used in a function position and will try to infer a type like `alpha ->
 beta` for `x`, which is dead wrong. "But wait," you say: "GHC can know
 that `x` should have type `forall a. a -> a -> a` by then!" Well, not
 quite. GHC knows that `x` has type `Foo b` (from the type signature) and
 that `b ~ True` (from the GADT pattern-match), but it hasn't yet put those
 pieces together: that's what the solver does! And, we don't want to try to
 run the solver before generating all the constraints, because the solver
 might do the wrong thing when it doesn't have enough information.

 One possible way forward here is to modify the offending line of the
 program above as follows:

 {{{
 bar STrue (x :: forall a. a -> a -> a) = ...
 }}}

 Now, GHC knows the correct type of `x` on the RHS and can generate
 constraints there without a problem. When the solver runs, it needs to
 solve `Foo b ~ forall a. a -> a -> a`, which works out just fine, given
 the GADT pattern-match.

 This requirement (the extra type annotation) is strange and unexpected to
 users, who are likely not thinking about GHC's constraint-solving
 algorithm. Does this fact make your proposed feature a bad idea? I don't
 know. And, there may be yet other reasons why what you want is a bad idea;
 this one is just one possible reason.

 Do others know of other problems here?

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