A type not inferred with RankNTypes

Simon Peyton-Jones simonpj at microsoft.com
Mon May 13 16:55:25 CEST 2013

Interesting example.  It's a fairly-fundamental limitation of type inference.   Here is a simpler version

foo :: forall a. (forall t. (t~a) => t) -> a

-- bar :: Num a => a
bar = foo 1

Suppose we try to *infer* the type for bar.   We instantiate
          foo at type alpha
          1 at type t, giving rise to (Num t)

So from the RHS of bar we get the constraint
          forall t. (t~alpha) => Num t
This is an "implication constraint"; see our paper "Modular type inference with local constraints".  The "forall t. (t~alpha) => ..." part comes directly from the type of foo's first argument.

A possible inferred type for bar would be this, where we simply abstract over the unsolved constraint:
          forall alpha. (forall t. (t~alpha) => Num t) => alpha

But GHC doesn't allow types with forall's in constraints, so when trying to *infer* the type for a let-bound identifier, GHC tries to approximate, to find a simpler constraint that will do, one that does not involve forall's in the constraint.  This approximation is necessarily a bit ad hoc.

In this particular case (Num alpha) would do just fine, but in general that is extremely hard to work out, because of the given equalities (here, t~alpha).   So when there are equalities in an implication constraint, GHC doesn't attempt to extract constraints from the body of the implication, lest we accidentally infer a non-principal type.

But if you supply a type signature, all is well, as you found.

That explains, I hope, why adding (C) makes your program work.

You also found that changing foo's type signature from (B) to (A) made it work, but that's not true in HEAD; both fail, as indeed they should.


From: glasgow-haskell-users-bounces at haskell.org [mailto:glasgow-haskell-users-bounces at haskell.org] On Behalf Of Akio Takano
Sent: 13 May 2013 03:47
To: glasgow-haskell-users at haskell.org
Subject: A type not inferred with RankNTypes


The attached program does not typecheck if I don't include a type signature for 'bar' (the line C). I can't figure out if this is a limitation in the type system or a bug in GHC. One thing that confuses me is that replacing the line (B) with (A) makes the program typecheck.

Could anyone help me figuring out what is going on?

I'm using GHC 7.6.2. The error was:

 % ghc forall.hs
[1 of 1] Compiling Foo              ( forall.hs, forall.o )

    Could not deduce (Fractional a) arising from the literal `0.1'
    from the context (Num (Scalar t), Scalar t ~ a)
      bound by a type expected by the context:
                 (Num (Scalar t), Scalar t ~ a) => AD t
      at forall.hs:18:7-13
    Possible fix:
      add (Fractional a) to the context of
        a type expected by the context:
          (Num (Scalar t), Scalar t ~ a) => AD t
        or the inferred type of bar :: a
    In the first argument of `foo', namely `0.1'
    In the expression: foo 0.1
    In an equation for `bar': bar = foo 0.1

Takano Akio
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/glasgow-haskell-users/attachments/20130513/580c5e5f/attachment.htm>

More information about the Glasgow-haskell-users mailing list