#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