#4347 closed bug (wontfix)
Bug in unification of polymorphic and not-yet-polymorphic type
Reported by: | dolio | Owned by: | |
---|---|---|---|
Priority: | normal | Milestone: | 7.10.1 |
Component: | Compiler (Type checker) | Version: | 7.1 |
Keywords: | ImpredicativeTypes | Cc: | ganesh, chowells79@…, dimitris@…, p.giarrusso@… |
Operating System: | Linux | Architecture: | x86_64 (amd64) |
Type of failure: | GHC rejects valid program | Test Case: | |
Blocked By: | Blocking: | ||
Related Tickets: | Differential Rev(s): | ||
Wiki Page: |
Description
The new type checker in GHC 7 seems to reject some cases of impredicative instantiation that prior versions allowed. I was initially alerted to this by Simon Marlow, who sent a patch for vector-algorithms removing a use of ($)
where it would have to be instantiated impredicatively.
Initially, I thought this was due to a planned removal of impredicativity, but this cannot be the case, because:
const :: a -> (forall b. b) -> a
is accepted by the type checker. However, the simple:
id :: (forall a. a) -> (forall b. b)
is not, giving an error message:
Couldn't match type `b' with `forall a. a' `b' is a rigid type variable bound by an expression type signature at <interactive>:1:32 In the expression: id :: (forall a. a) -> (forall b. b)
This would seem to indicate that the type is being rewritten to:
forall b. (forall a. a) -> b
and then the forall a. a
matched with the bare b
. It is, of course, fine to rewrite the type this way, since the two are isomorphic, but it is unfortunate that it causes the checker to reject what would otherwise be a valid instantiation.
Change History (17)
comment:1 Changed 7 years ago by
Cc: | ganesh added |
---|
comment:2 Changed 7 years ago by
Milestone: | → 7.2.1 |
---|
comment:3 Changed 6 years ago by
comment:4 Changed 6 years ago by
Cc: | chowells79@… added |
---|
comment:5 Changed 6 years ago by
Impredicativity has always been a very experimental feature. Although I advertised that we'd remove it altogether, GHC 7 does still support a simple form of impredicativity, but it's simpler than 6.12. For what it's worth, the new support is closely modeled on QML http://research.microsoft.com/en-us/um/people/crusso/qml/
Let's be concrete: can you give a small test case, that worked before but not now?
Simon
comment:6 Changed 6 years ago by
Yes, I have a very small example:
{-# LANGUAGE ImpredicativeTypes #-} import Control.Concurrent.MVar import System.Random dumbTrick :: IO (forall a. Random a => (forall g. RandomGen g => g -> (a, g)) -> IO a) dumbTrick = do gen <- newMVar =<< newStdGen let apply :: forall b. Random b => (forall g'. RandomGen g' => g' -> (b, g')) -> IO b apply f = modifyMVar gen $ (\(a, b) -> return (b, a)) . f return apply
comment:7 Changed 6 years ago by
The thing that gets to me is this:
DumbTrick.hs:11:12: Couldn't match expected type `forall a. Random a => (forall g. RandomGen g => g -> (a, g)) -> IO a' with actual type `(forall g'. RandomGen g' => g' -> (b0, g')) -> IO b0' In the first argument of `return', namely `apply' In the expression: return apply In the expression: do { gen <- newMVar =<< newStdGen; let apply :: forall b. Random b => (forall g'. RandomGen g' => g' -> (b, g')) -> IO b apply f = modifyMVar gen $ (\ (a, b) -> ...) . f; return apply }
It's telling me that it can't unify two types, there the only difference between the reported types is whether the rank-1 polymorphism is implicit or explicit. (I'm ignoring the lack of reporting on the class constraint because I'm pretty sure that's not relevant.)
Furthermore, it does that even when I explicitly quantify the value it's telling me is implicitly quantified.
Between those two factors, this feels like a bug, rather a decision to remove a little-used (if awesome) feature.
comment:8 Changed 6 years ago by
Cc: | dimitris@… added |
---|
Here's a version that works
type Blob = (forall a. Random a => (forall g. RandomGen g => g -> (a, g)) -> IO a) dumbTrick :: IO Blob dumbTrick = do gen <- newMVar =<< newStdGen let apply :: forall b. Random b => (forall g'. RandomGen g' => g' -> (b, g')) -> IO b apply f = modifyMVar gen (\x -> (\(a, b) -> return (b, a)) (f x)) (return :: Blob -> IO Blob) apply -- ((return apply) :: IO Blob)
The (return :: Blob -> IO Blob)
fixes the instantiation of return :: forall a. a -> IO a
to instantiate a := Blob
, and then all is well. Bu the commented out line does not work, becuase apply is implicitly instantiated.
What GHC lacks at the moment is a "rigid type signature" in the QML sense. If we have that we could write
return (apply ! :: Blob)
where I'm using "!
to indicate a rigid signature. The "rigid" part means that the polymorphic type is not instantiated, so all will be well.
I plan to add rigid type signatures to GHC, but I keep hesitating over syntax. It's quite attractive to use (apply ::: Blob)
, but (:::)
is currently available for users so it seems bad to steal it. But maybe worth it. Other ideas welcome.
Read the QML paper: it's well explained.
comment:9 Changed 6 years ago by
Thank you, Simon. The more I thought about the QML overview (I didn't read the full paper), the more I suspected there was an answer like this - "It's possible, but in a way I won't guess without reading the paper or thinking about it a lot. And there's probably some syntax that could make it easier that I don't know about."
Now that I see what you did, that does make sense. I wish the error message was a little clearer, though.
I guess I need to read the QML paper for the details of this system, though.
comment:10 Changed 6 years ago by
Cc: | p.giarrusso@… added |
---|---|
Summary: | Asymmetry of (impredicative) instantiation/higher rank types → Bug in unification of polymorphic and not-yet-polymorphic type |
I think I'm seeing two instances of this bug in rather more simple contexts. The first involves the id function:
$ ghci -XScopedTypeVariables -XRank2Types Prelude> let (id2 :: forall t. t -> t) = \x -> x <interactive>:1:33: Couldn't match expected type `t0 -> t1' with actual type `forall t. t -> t' The lambda expression `\ x -> x' has one argument, but its type `forall t. t -> t' has none In the expression: \ x -> x In a pattern binding: (id2 :: forall t. t -> t) = \ x -> x
To me, it seems already buggy that the code is rejected without Rank2Types, because only rank-1 types are involved. I guess that the code requires first-class polymorphism, or that the message might appear only of the main failure. But that unification error? I think it reflects the fact that a term of type (forall t. t -> t), in System F, expects a type argument before a term argument. That's consistent with the errors shown here on Stackoverflow.
With polymorphic recursion, one gets even no clue about what's happening, just a "couldn't match" message, even if probably due to the same problem. Aren't similar errors supposed to produce similar messages?
Prelude> let a :: forall b. b -> b = a a <interactive>:1:31: Couldn't match expected type `forall b. b -> b' with actual type `b0 -> b0' In the first argument of `a', namely `a' In the expression: a a In a pattern binding: a :: forall b. b -> b = a a
comment:11 Changed 6 years ago by
Milestone: | 7.4.1 → 7.6.1 |
---|
comment:12 Changed 5 years ago by
Milestone: | 7.6.1 → 7.6.2 |
---|
comment:14 Changed 3 years ago by
difficulty: | → Unknown |
---|
With HEAD, the example from the description works (fails with 7.8.3). I don't know if this is incidental, or if anything got really fixed?
$ ghci -XRankNTypes GHCi, version 7.9.20141125: ... Prelude> let f = id :: (forall a. a) -> (forall b. b) Prelude>
comment:15 Changed 3 years ago by
To be honest, I'd be fine with closing this ticket. I filed it right around the 6 -> 7 cutover, and evidently thought that the new type checker was still supposed to handle impredicative instantiation. But, the truth is, I think, that if the new algorithm does handle certain impredicative cases, it's more a happy accident than a design principle. So my const example happened to work, but id didn't at the time. I interpreted that as a bug with id rather than being happy that it worked at all for const.
I'll leave it to the implementors to decide. If the id example works in 7.10, that's handy. But I've long since stopped considering 'regressions' in impredicative instantiation relative to 6.x actual regressions. It's merely the result a different set of tradeoffs.
comment:16 Changed 3 years ago by
Resolution: | → wontfix |
---|---|
Status: | new → closed |
Dolio is right here. I've backed off from making ANY claims about what GHC does or does not do for impredicative polymorphism. Really the language extension flag should be deprecated because it is not supported either by proper theory about what inference should do, or by an implementation of that theory. Whatever happens right now happens by luck.
I'm sure there is a route to a better story for impredicativity; but it is complex territory and there has been much else to do.
So yes I'll close this ticket
Simon
comment:17 Changed 4 months ago by
Keywords: | ImpredicativeTypes added |
---|
I've recently run into this. It's not fun when my code that worked on GHC 6.12 doesn't work on GHC 7. Any chance this'll get done before 7.4?