[GHC] #14160: Type inference breaking change in GHC 8.0.2

[GHC]

#14160: Type inference breaking change in GHC 8.0.2
-------------------------------------+-------------------------------------
        Reporter:  Iceland_jack      |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  8.2.1
      Resolution:                    |             Keywords:
                                     |  ImpredicativeTypes
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------
Changes (by RyanGlScott):

 * keywords:   => ImpredicativeTypes


Comment:

 I grant that this breakage is surprising, but it is somewhat expected. The
 nub of the issue is once again impredicativity.

 For the sake of being explicit, here is a version of the above code with
 no external dependencies (please make an effort to do this in future bug
 reports - it makes dissecting the problem much easier):

 {{{#!hs
 {-# LANGUAGE RankNTypes #-}
 module Test where

 class Profunctor p where
   dimap :: (a -> b) -> (c -> d) -> p b c -> p a d

 proj :: Profunctor p => forall c. (forall a. p a a) -> p c c
 proj e = e

 f1 :: Profunctor p => (a -> b) -> (forall c. p c c) -> p a b
 f1 f e = dimap f id (proj e)
 }}}

 Now it's worth noting that `f2`:

 {{{#!hs
 f2 :: Profunctor p => (a -> b) -> (forall c. p c c) -> p a b
 f2 f = dimap id f . proj
 }}}

 Has //never// typechecked, even on old versions of GHC. The only thing
 from this program that used to typecheck is `f3`:

 {{{#!hs
 f3 :: Profunctor p => (a -> b) -> (forall c. p c c) -> p a b
 f3 f = undefined
 }}}

 Really, the issue can be condensed down to just this:

 {{{#!hs
 {-# LANGUAGE RankNTypes #-}
 module Test where

 -- Typechecks
 f :: (forall a. a) -> b
 f x = x

 -- Typechecks on GHC 7.10.3, but not later versions
 g :: (forall a. a) -> b
 g = undefined
 }}}

 {{{
 $ /opt/ghc/7.10.3/bin/ghci Bug.hs
 GHCi, version 7.10.3: http://www.haskell.org/ghc/  :? for help
 [1 of 1] Compiling Test             ( Bug.hs, interpreted )
 Ok, modules loaded: Test.
 λ> :q
 Leaving GHCi.
 $ /opt/ghc/8.0.2/bin/ghci Bug.hs
 GHCi, version 8.0.2: http://www.haskell.org/ghc/  :? for help
 Loaded GHCi configuration from /home/rgscott/.ghci
 [1 of 1] Compiling Test             ( Bug.hs, interpreted )

 Bug.hs:10:5: error:
     • Cannot instantiate unification variable ‘a0’
       with a type involving foralls: (forall a. a) -> b
         GHC doesn't yet support impredicative polymorphism
     • In the expression: undefined
       In an equation for ‘g’: g = undefined
     • Relevant bindings include
         g :: (forall a. a) -> b (bound at Bug.hs:10:1)
 Failed, modules loaded: none.
 }}}

 The fact that the error message mentions impredicativity should be a solid
 clue that we're headed into murky territory. The issue is that we're
 trying to instantiate a type variable with `(forall a. a) -> b`, which of
 course is impredicative. GHC 7.10.3 and earlier, for whatever reason,
 allowed this, but it made type inference much more unpredictable, as noted
 in https://ghc.haskell.org/trac/ghc/ticket/12749#comment:2. GHC 8.0
 prevented this unpredictability by preventing type variables from being
 instantiated with polytypes, but at the cost of disallowing functions like
 `g`.

 For what it's worth, I don't think the solution is to re-allow `g`, but to
 instead allow a limited form of impredicativity that Simon Peyton Jones
 suggests in https://mail.haskell.org/pipermail/ghc-
 devs/2016-September/012940.html. That is, we would allow writing polytypes
 in visible type arguments, so this would be permissible:

 {{{#!hs
 g :: (forall a. a) -> b
 g = undefined @_ @((forall a. a) -> b)
 }}}

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