[GHC] #11319: ImpredicativeTypes even more broken than usual

[GHC]

#11319: ImpredicativeTypes even more broken than usual
-------------------------------------+-------------------------------------
        Reporter:  Iceland_jack      |                Owner:
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  7.11
  checker)                           |             Keywords:
      Resolution:                    |  ImpredicativeTypes
Operating System:  Linux             |         Architecture:
 Type of failure:  GHC rejects       |  Unknown/Multiple
  valid program                      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by goldfire):

 Upon further thought, the new behavior is actually less broken than the
 old behavior, for a certain definition of broken.

 Consider the typing rule for function applications, as in the "Practical
 Type Inference" and "Visible Type Application" papers (they're the same,
 in this respect):

 {{{
 G |- e1 => s1 -> s2
 G |- e2 <= s1
 ---------------- App
 G |- e1 e2 => s2
 }}}

 Here, `=>` indicates type inference, while `<=` indicates type checking.
 There is no type checking rule for applications. So this means that any
 type expected by the context is simply not propagated down when checking
 the individual pieces.

 Given this fact, we can think about `pure Nothing` in a vacuum, without
 any type expected by its context. We see `pure :: forall f. Applicative f
 => forall a. a -> f a`. We guess a type (call it `s`) for `a` and then
 check `Nothing` against `s`. Without `ImpredicativeTypes`, `s` is
 constrained to be a tau-type -- that is, with no foralls anywhere. Thus,
 `Nothing :: forall a. Maybe a` must be instantiated to `Nothing :: Maybe
 t` for some `t`. But with `ImpredicativeTypes`, `s` can have foralls. So
 GHC doesn't instantiate, as it has no good reason to. It infers `pure @f
 @(forall a. Maybe a) Nothing :: f (Maybe (forall a. Maybe a))`. This is
 fully correct behavior. Then, when GHC checks that inferred type against
 the expected type `f (Maybe b)` (for some known skolem `b`) the check
 fails.

 So, the behavior we see is entirely predictable given the published typing
 rules when you relax the restriction around tau-types. And that's why I
 say it's less broken than the old behavior.

 On the other hand, it is sad that `ImpredicativeTypes` fails to accept
 Haskell98. Simon has cooked up a scheme that, I believe, will fix this
 case (written up at wiki:Typechecking), but that won't make it for 8.0, I
 would think. (Unless Simon wants to implement that plan in short order!)
 The key bit is that it comes up with a "checking" (that is, `<=`) rule for
 function application that propagates information down, forcing
 instantiation of `Nothing`, as desired.

 In any case, this isn't a quick fix and so I will remove it from my queue,
 as investing time in patching together `ImpredicativeTypes` seems less
 useful than other ways of using that precious resource.

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