Opened 2 years ago
Closed 2 years ago
#14160 closed bug (wontfix)
Type inference breaking change in GHC 8.0.2
Reported by: | Iceland_jack | Owned by: | |
---|---|---|---|
Priority: | normal | Milestone: | |
Component: | Compiler | Version: | 8.2.1 |
Keywords: | ImpredicativeTypes | Cc: | |
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: |
Description (last modified by )
A regression reported by Milewski,
{-# 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
-- • 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
Change History (6)
comment:1 Changed 2 years ago by
Description: | modified (diff) |
---|
comment:2 Changed 2 years ago by
Keywords: | ImpredicativeTypes added |
---|
comment:3 Changed 2 years ago by
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! :)
comment:4 Changed 2 years ago by
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?
comment:6 Changed 2 years ago by
Related Tickets: | → #11319 |
---|---|
Resolution: | → wontfix |
Status: | new → closed |
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.
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):
Now it's worth noting that
f2
:Has never typechecked, even on old versions of GHC. The only thing from this program that used to typecheck is
f3
:Really, the issue can be condensed down to just this:
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 likeg
.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: