[GHC] #14160: Type inference breaking change in GHC 8.0.2
#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 Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- A regression reported by [https://www.reddit.com/r/haskell/comments/6w7grz/type_inference_breaking_cha... Milewski], {{{#!hs {-# LANGUAGE RankNTypes #-} module Test where import Data.Profunctor 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) }}} The regression is that these used to work, but do not currently {{{#!hs -- • Couldn't match type ‘p c0 c0’ with ‘forall a1. p a1 a1’ -- Expected type: p c0 c0 -> p a a -- Actual type: (forall a1. p a1 a1) -> p a a -- • In the second argument of ‘(.)’, namely ‘proj’ -- In the expression: dimap id f . proj -- In an equation for ‘f2’: f2 f = dimap id f . proj -- • Relevant bindings include -- f2 :: (a -> b) -> (forall c. p c c) -> p a b -- (bound at 24:1) f2 :: Profunctor p => (a -> b) -> (forall c. p c c) -> p a b f2 f = dimap id f . proj -- • Cannot instantiate unification variable ‘a0’ -- with a type involving foralls: (forall c. p c c) -> p a b -- GHC doesn't yet support impredicative polymorphism -- • In the expression: undefined -- In an equation for ‘f3’: f3 f = undefined -- • Relevant bindings include -- f :: a -> b -- (bound at 39:4) -- f3 :: (a -> b) -> (forall c. p c c) -> p a b -- (bound at 39:1) f3 :: Profunctor p => (a -> b) -> (forall c. p c c) -> p a b f3 f = undefined -- dimap id f . proj }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14160 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Description changed by Iceland_jack: Old description:
A regression reported by [https://www.reddit.com/r/haskell/comments/6w7grz/type_inference_breaking_cha... Milewski],
{{{#!hs {-# LANGUAGE RankNTypes #-} module Test where
import Data.Profunctor
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) }}}
The regression is that these used to work, but do not currently
{{{#!hs -- • Couldn't match type ‘p c0 c0’ with ‘forall a1. p a1 a1’ -- Expected type: p c0 c0 -> p a a -- Actual type: (forall a1. p a1 a1) -> p a a -- • In the second argument of ‘(.)’, namely ‘proj’ -- In the expression: dimap id f . proj -- In an equation for ‘f2’: f2 f = dimap id f . proj -- • Relevant bindings include -- f2 :: (a -> b) -> (forall c. p c c) -> p a b -- (bound at 24:1) f2 :: Profunctor p => (a -> b) -> (forall c. p c c) -> p a b f2 f = dimap id f . proj
-- • Cannot instantiate unification variable ‘a0’ -- with a type involving foralls: (forall c. p c c) -> p a b -- GHC doesn't yet support impredicative polymorphism -- • In the expression: undefined -- In an equation for ‘f3’: f3 f = undefined -- • Relevant bindings include -- f :: a -> b -- (bound at 39:4) -- f3 :: (a -> b) -> (forall c. p c c) -> p a b -- (bound at 39:1)
f3 :: Profunctor p => (a -> b) -> (forall c. p c c) -> p a b f3 f = undefined -- dimap id f . proj }}}
New description: A regression reported by [https://www.reddit.com/r/haskell/comments/6w7grz/type_inference_breaking_cha... Milewski], {{{#!hs {-# LANGUAGE RankNTypes #-} module Test where import Data.Profunctor 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) }}} Where these definitions no longer type check {{{#!hs -- • Couldn't match type ‘p c0 c0’ with ‘forall a1. p a1 a1’ -- Expected type: p c0 c0 -> p a a -- Actual type: (forall a1. p a1 a1) -> p a a -- • In the second argument of ‘(.)’, namely ‘proj’ -- In the expression: dimap id f . proj -- In an equation for ‘f2’: f2 f = dimap id f . proj -- • Relevant bindings include -- f2 :: (a -> b) -> (forall c. p c c) -> p a b -- (bound at 24:1) f2 :: Profunctor p => (a -> b) -> (forall c. p c c) -> p a b f2 f = dimap id f . proj -- • Cannot instantiate unification variable ‘a0’ -- with a type involving foralls: (forall c. p c c) -> p a b -- GHC doesn't yet support impredicative polymorphism -- • In the expression: undefined -- In an equation for ‘f3’: f3 f = undefined -- • Relevant bindings include -- f :: a -> b -- (bound at 39:4) -- f3 :: (a -> b) -> (forall c. p c c) -> p a b -- (bound at 39:1) f3 :: Profunctor p => (a -> b) -> (forall c. p c c) -> p a b f3 f = undefined -- dimap id f . proj }}} -- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14160#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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
#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: | -------------------------------------+------------------------------------- Comment (by goldfire): Agreed that this is an "improvement" (as in, GHC is behaving closer to spec) from previous behavior. Yes to allowing polytypes in visible type arguments. No to accepting `g = undefined`. It's impredicative! :) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14160#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): In that case, it sounds like this particular bug is resolved as "wontfix". We don't yet have a ticket for implementing the ability to visibly apply polytypes—should this ticket become that, or should we open a new one? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14160#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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: | -------------------------------------+------------------------------------- Comment (by goldfire): I'd say a new one. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14160#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14160: Type inference breaking change in GHC 8.0.2 -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Resolution: wontfix | Keywords: | ImpredicativeTypes Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #11319 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * status: new => closed * resolution: => wontfix * related: => #11319 Comment: I was just about to open a new ticket with a title like "Figure out how to salvage `ImpredicativeTypes`", but then I discovered #11319, with the very apt title "`ImpredicativeTypes` even more broken than usual". I think this is a good place for this discussion (especially since it talks about `TypeApplications`), so I'll move the discussion there. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14160#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC