#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