Opened 4 years ago
Closed 16 months ago
#11319 closed bug (fixed)
ImpredicativeTypes even more broken than usual
Reported by: | Iceland_jack | Owned by: | |
---|---|---|---|
Priority: | normal | Milestone: | |
Component: | Compiler (Type checker) | Version: | 7.11 |
Keywords: | ImpredicativeTypes | Cc: | goldfire, a.serranomena@… |
Operating System: | Linux | Architecture: | Unknown/Multiple |
Type of failure: | GHC rejects valid program | Test Case: | typecheck/should_compile/T11319 |
Blocked By: | Blocking: | ||
Related Tickets: | #14859 | Differential Rev(s): | |
Wiki Page: |
Description
I don't have the latest version of GHC, trying to derive Functor A
and Foldable A
is fine but when I derive Traversable A
in the attachment Error.hs:
{-# LANGUAGE DeriveFunctor, DeriveFoldable, DeriveTraversable, ImpredicativeTypes #-} import Data.Functor (Functor) import Data.Foldable (Foldable) import Data.Traversable (Traversable) data A a = A deriving (Functor, Foldable, Traversable)
GHC barks at me (verbose log attached):
/tmp/Error.hs:8:32: error: • Couldn't match type ‘forall a1. A a1’ with ‘A b’ Expected type: f (A b) Actual type: f (forall a. A a) • In the expression: pure A In an equation for ‘traverse’: traverse f A = pure A When typechecking the code for ‘traverse’ in a derived instance for ‘Traversable A’: To see the code I am typechecking, use -ddump-deriv In the instance declaration for ‘Traversable A’ • Relevant bindings include f :: a -> f b (bound at /tmp/Error.hs:8:32) traverse :: (a -> f b) -> A a -> f (A b) (bound at /tmp/Error.hs:8:32)
With -ddump-deriv
we get this (unqualified) instance:
instance Traversable A where traverse f_a2Le A = pure A
which by itself causes the same problem in the attachment Error2.hs:
{-# LANGUAGE DeriveFunctor, DeriveFoldable, ImpredicativeTypes #-} import Data.Functor (Functor) import Data.Foldable (Foldable) import Data.Traversable (Traversable) data A a = A deriving (Functor, Foldable) instance Traversable A where traverse f A = pure A
Works fine in GHC-7.10.2 and GHC-7.10.0.20150316 and GHC-7.4 (with some additional imports), is this an ImpredicativeTypes
regression?
Attachments (4)
Change History (18)
Changed 4 years ago by
Changed 4 years ago by
Handwritten instance of Traversable, cleaned up output of -ddump-deriv
Changed 4 years ago by
ghc-7.11.20151226 -v -ignore-dot-ghci --interactive /tmp/Error.hs &> /tmp/Error.log
Changed 4 years ago by
Attachment: | Error2.log added |
---|
ghc-7.11.20151226 -v -ignore-dot-ghci --interactive /tmp/Error2.hs &> /tmp/Error2.log
comment:1 Changed 4 years ago by
GHCi (version 7.11.20151226) and Glasgow Haskell Compiler (version 7.11.20151226, stage 2 booted by GHC version 7.8.4).
comment:2 Changed 4 years ago by
Cc: | goldfire added |
---|---|
Summary: | ImpredicativeTypes cause trouble (affects deriving of Traversable) → ImpredicativeTypes even more broken than usual |
Nothing special about deriving here, try:
{-# LANGUAGE ImpredicativeTypes #-} f :: Applicative f => f (Maybe a) f = pure Nothing main = return () {- Error.hs:4:5: error: • Couldn't match type ‘forall a1. Maybe a1’ with ‘Maybe a’ Expected type: f (Maybe a) Actual type: f (forall a. Maybe a) • In the expression: pure Nothing In an equation for ‘f’: f = pure Nothing • Relevant bindings include f :: f (Maybe a) (bound at Error.hs:4:1) -}
This is with an up-to-the-minute version of HEAD, that contains the relevant-looking Phab:1715.
As ImpredicativeTypes
is unsupported anyways, perhaps we should just take the opportunity to kill it?
comment:3 Changed 4 years ago by
It would make sense that the type-checker rewrite from visible type application would break impredicativity even more than usual. Given its already-quite-broken state, I didn't try to salvage it.
I don't want to completely kill it, though, as it sometimes is useful, if just for experimentation. And visible types lets you climb out of any hole you get in. For example, this works:
{-# LANGUAGE ImpredicativeTypes, ScopedTypeVariables, TypeApplications #-} module Bug where f :: forall a f. Applicative f => f (Maybe a) f = pure (Nothing @a)
All that said, I'll take a look at this one, as it would be nice to be less broken. And my hunch is that this will be quite easy to fix.
comment:4 Changed 4 years ago by
Cc: | a.serranomena@… added |
---|
This is definitely fallout from Visible Type Application. The program in comment:3 typechecks fine without ImpredicativeTypes
(indeed it does in Haskell 98!) and surely ImpredicativeTypes
should be a conservative extension.
But let's not invest much in "fixing" ImpredicativeTypes
which is simply not supported at the moment. Alejandro Serrano (cc'd) is working on impredicativity right now, so I've added him to the cc list.
Alejandro, what are you doing will be significantly affected by the "lazy instantiation" approach of Visible Type Application (see paper), so you might want to look carefully. VTA is in GHC now!
comment:5 Changed 4 years ago by
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.
comment:7 Changed 4 years ago by
Test Case: | → typecheck/should_compile/T11319 |
---|
comment:8 Changed 4 years ago by
Just to note that most of wiki:Typechecking is indeed in HEAD and 8.0 now. The bit that I believe would fix this ticket is ExpFun
, which is not implemented.
comment:9 Changed 2 years ago by
Simon, are you still hoping to make ImpredicativeTypes
work, or should this be closed as WONTFIX, or something else?
comment:10 Changed 2 years ago by
Leave it open as a useful test case. Alejandro is still thinking about impredicativity, making some progress.
comment:11 Changed 2 years ago by
Since this ticket was originally opened, SPJ started a very relevant discussion on the GHC devs mailing list about a way to salvage ImpredicativeTypes
. It wouldn't make the original program in this ticket typecheck again, but it would provide a way to possibly suggest a workaround in error messages.
To quote SPJ:
When you have
-XImpredicativeTypes
- You can write a polytype in a visible type argument; eg.
f @(forall a. a->a)
- You can write a polytype as an argument of a type in a signature e.g.
f :: [forall a. a->a] -> Int
And that’s all. A unification variable STILL CANNOT be unified with a polytype. The only way you can call a polymorphic function at a polytype is to use Visible Type Application.
So using impredicative types might be tiresome. E.g.
type SID = forall a. a->a xs :: [forall a. a->a] xs = (:) @SID id ( (:) @SID id ([] @ SID))In short, if you call a function at a polytype, you must use VTA. Simple, easy, predictable; and doubtless annoying. But possible.
However, this should undoubtedly go through a GHC proposal. At the very least, it's unclear to me whether SPJ's intention was to require actually enabling -XImpredicativeTypes
in order to visibly apply a polytype (the title of the GHC devs discussion, "Getting rid of -XImpredicativeTypes
", makes me think "no", but the actual contents of the discussion that I quoted would suggest "yes").
comment:13 Changed 2 years ago by
I also noticed this paper (Guarded impredicative polymorphism) from Simon's website as "in submission", how does it relate? :)
comment:14 Changed 16 months ago by
Related Tickets: | → #14859 |
---|---|
Resolution: | → fixed |
Status: | new → closed |
Note that:
- The test case in comment:2 passes as of b612da667fe8fa5277fc78e972a86d4b35f98364, and has been checked into the test suite.
- There is now a dedicated ticket (#14859) for tracking the request to allow explicit impredicativity.
Therefore, let's close this, and move the discussion about the latter point to #14859.
Derives Traversable