Opened 7 years ago

Closed 3 years ago

Last modified 9 months ago

#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:


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 ganesh

Cc: ganesh added

comment:2 Changed 7 years ago by igloo

Milestone: 7.2.1

comment:3 Changed 7 years ago by carlhowells

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?

comment:4 Changed 7 years ago by carlhowells

Cc: chowells79@… added

comment:5 Changed 7 years ago by simonpj

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

Let's be concrete: can you give a small test case, that worked before but not now?


comment:6 Changed 7 years ago by carlhowells

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 7 years ago by carlhowells

The thing that gets to me is this:

    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 7 years ago by simonpj

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 7 years ago by carlhowells

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 7 years ago by Blaisorblade

Cc: p.giarrusso@… added
Summary: Asymmetry of (impredicative) instantiation/higher rank typesBug 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

    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

    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 igloo


comment:12 Changed 5 years ago by igloo


comment:13 Changed 4 years ago by thoughtpolice


Moving to 7.10.1.

comment:14 Changed 3 years ago by thomie

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)

comment:15 Changed 3 years ago by dolio

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 simonpj

Resolution: wontfix
Status: newclosed

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


comment:17 Changed 9 months ago by simonpj

Keywords: ImpredicativeTypes added
Note: See TracTickets for help on using tickets.