Adding GHC's inferred type signatures to a working program can make it fail with Rank2Types

[guest]

{-# LANGUAGE Rank2Types #-}
module Test where

data Foo = Foo { unFoo :: forall r . (RealFrac r) => r -> String }

mkFoo1 :: (forall r. RealFrac r => r -> String) -> Maybe Foo
mkFoo1 val = Just $ Foo val

--mkFoo2 :: (forall r. RealFrac r => r -> String) -> Maybe Foo
mkFoo2 val = Foo `fmap` Just val

Without the commented-out type signature, the program typechecks without complaint. With it, the program fails to compile with the error:

Test.hs:10:30:
    Couldn't match expected type `forall r. RealFrac r => r -> String'
                with actual type `r0 -> String'
    In the first argument of `Just', namely `val'
    In the second argument of `fmap', namely `Just val'
    In the expression: Foo `fmap` Just val

Note that the commented-out type is exactly what's inferred by GHC.

Also note that (with ImpredicativeTypes? also enabled), this is fine (but mkFoo2 still fails if its type signature is included):

mkFoo3 :: (forall r. RealFrac r => r -> String) -> Maybe Foo
mkFoo3 val = Foo `fmap` (Just :: (forall s. RealFrac s => s -> String) -> (Maybe (forall s. RealFrac s => s -> String))) val

It's confusing that adding a valid, GHC-inferred type signature to a program can break it, and the error message leaves something to be desired.

[simonpj]

This is bad. Here's a slightly cut down example:

{-# LANGUAGE Rank2Types #-}
module T7264 where

data Foo = Foo (forall r . r -> String)

mmap :: (a->b) -> Maybe a -> Maybe b
mmap f (Just x) = f x
mmap f Nothing  = Nothing

-- mkFoo2 :: (forall r. r -> String) -> Maybe Foo
mkFoo2 val = mmap Foo (Just val)

• The commented-out type sig is inferred, because GHC assigns unknown type alpha to val; then instantiates mmap's type with beta and gamma; then unifies beta:=forall r. r->String. And then later unifies alpha and beta.

• But when the commented out type sig is provided ghc instantiates it at the occurrence of val.

You need to call mmap at a polymorphic type, which means you need impredicativity. Lacking ImpredicativeTypes the no-signature program should be rejected. The fact that it isn't is a bug.

Even if that bug is fixed, the progam shows, again, how tricky impredicativity is. We don't have a decent implementation of ImpredicativeTypes.

At least it's not a show-stopper for anyone.

Simon

[simonpj@…]

commit 10f83429ba493699af95cb8c3b16d179d78b7749

Author: Simon Peyton Jones <simonpj@microsoft.com>
Date:   Wed Oct 31 09:08:39 2012 +0000

    Do not instantiate unification variables with polytypes
    
    Without -XImpredicativeTypes, the typing rules say that a function
    should be instantiated only at a *monotype*.  In implementation terms,
    that means that a unification variable should not unify with a type
    involving foralls.  But we were not enforcing that rule, and that
    gave rise to some confusing error messages, such as
      Trac #7264, #6069
    
    This patch adds the test for foralls.  There are consequences
    
     * I put the test in occurCheckExpand, since that is where we see if a
       type can unify with a given unification variable.  So
       occurCheckExpand has to get DynFlags, so it can test for
       -XImpredicativeTypes
    
     * We want this to work
          foo :: (forall a. a -> a) -> Int
          foo = error "foo"
       But that means instantiating error at a polytype!  But error is special
       already because you can instantiate it at an unboxed type like Int#.
       So I extended the specialness to allow type variables of openTypeKind
       to unify with polytypes, regardless of -XImpredicativeTypes.
    
       Conveniently, this works in TcUnify.matchExpectedFunTys, which generates
       unification variable for the function arguments, which can be polymorphic.
    
     * GHC has a special typing rule for ($) (see Note [Typing rule
       for ($)] in TcExpr).  It unifies the argument and result with a
       unification variable to exclude unboxed types -- but that means I
       now need a kind of unificatdion variable that *can* unify with a
       polytype.
    
       So for this sole case I added PolyTv to the data type TcType.MetaInfo.
       I suspect we'll find mor uses for this, and the changes are tiny,
       but it still feel a bit of a hack.  Well the special rule for ($)
       is a hack!
    
    There were some consequential changes in error reporting (TcErrors).

 compiler/typecheck/TcCanonical.lhs |   21 +++---
 compiler/typecheck/TcErrors.lhs    |   62 +++++++++++++------
 compiler/typecheck/TcExpr.lhs      |    9 ++-
 compiler/typecheck/TcHsType.lhs    |   15 +++--
 compiler/typecheck/TcMType.lhs     |   10 +++-
 compiler/typecheck/TcType.lhs      |  118 ++++++++++++++++++++++++-----------
 compiler/typecheck/TcUnify.lhs     |   79 +++++++++++++++++++-----
 7 files changed, 223 insertions(+), 91 deletions(-)

[simonpj]

Now GHC does not instantiate mmap at a polymorphic type, and we get this error message from the program without the type signature

T7264.hs:11:19:
    Couldn't match type `a' with `forall r. r -> String'
      `a' is a rigid type variable bound by
          the inferred type of mkFoo2 :: a -> Maybe Foo at T7264.hs:11:1
    Expected type: a -> Foo
      Actual type: (forall r. r -> String) -> Foo
    Relevant bindings include
      mkFoo2 :: a -> Maybe Foo (bound at T7264.hs:11:1)
      val :: a (bound at T7264.hs:11:8)
    In the first argument of `mmap', namely `Foo'
    In the expression: mmap Foo (Just val)
    In an equation for `mkFoo2': mkFoo2 val = mmap Foo (Just val)

It's not a fantastic message, but it's on the money, and (without -XImpredicativeTypes) the program should certainly be rejected.

Simon