Opened 4 years ago

Last modified 19 months ago

#4347 new bug

Bug in unification of polymorphic and not-yet-polymorphic type

Reported by: dolio Owned by:
Priority: normal Milestone: 7.6.2
Component: Compiler (Type checker) Version: 7.1
Keywords: Cc: ganesh, chowells79@…, dimitris@…, p.giarrusso@…
Operating System: Linux Architecture: x86_64 (amd64)
Type of failure: GHC rejects valid program Difficulty:
Test Case: Blocked By:
Blocking: Related Tickets:

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 (12)

comment:1 Changed 4 years ago by ganesh

  • Cc ganesh added

comment:2 Changed 3 years ago by igloo

  • Milestone set to 7.2.1

comment:3 Changed 3 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 3 years ago by carlhowells

  • Cc chowells79@… added

comment:5 Changed 3 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 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 3 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 3 years ago by carlhowells

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

  • Cc p.giarrusso@… added
  • Summary changed from Asymmetry of (impredicative) instantiation/higher rank types to 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 2 years ago by igloo

  • Milestone changed from 7.4.1 to 7.6.1

comment:12 Changed 19 months ago by igloo

  • Milestone changed from 7.6.1 to 7.6.2
Note: See TracTickets for help on using tickets.