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. Simon From: glasgow-haskell-users-bounces@haskell.org [mailto:glasgow-haskell-users-bounces@haskell.org] On Behalf Of Akio Takano Sent: 13 May 2013 03:47 To: glasgow-haskell-users@haskell.org Subject: A type not inferred with RankNTypes Hi, 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 ) forall.hs:18:11: 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 Regards, Takano Akio