Hi, On 13/05/13 03:47, Akio Takano wrote:

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 think that this is a relatively subtle point about constraint solving during type inference. I'll work through what is going on to try to make sense of your results. Apologies if this is far too much information. (Full disclosure: I don't really understand GHC's constraint solver, but I know enough to make some intelligent guesses.) TL;DR: The constraint solver is not stable under adding information, so making extra hypotheses available can stop your program from typechecking. This is a bad thing, but difficult to avoid. The essence of your working example is

instance (Fractional (Scalar t)) => Fractional (AD t) foo :: forall a. (forall t. (Scalar t ~ a) => AD t) -> a bar = foo 0.1

When checking bar, the constraint solver is given exists a . forall t . Scalar t ~ a => Fractional (AD t) which can be rewritten using the Fractional (AD t) instance to exists a . forall t . Scalar t ~ a => Fractional (Scalar t) and thence to exists a . forall t . Fractional a so the |Fractional a| constraint floats out to the top level, and bar is given the type Fractional a => a (which specialises to Double in the presence of the monomorphism restriction). In the case of the non-working example

foo :: forall a. (forall t. (Num (Scalar t), Scalar t ~ a) => AD t) -> a

the constraint solver has exists a . forall t . (Num (Scalar t), Scalar t ~ a) => Fractional (AD t) and thence exists a . forall t . (Num (Scalar t), Scalar t ~ a) => Fractional (Scalar t) which might be rewritten to the implication constraint exists a . forall t . Num a => Fractional a if we are lucky. But this is still troublesome, because implication constraints cannot appear in types, so GHC complains (for good reason). In this case, simply forgetting about the hypothesis (Num a) would be the right thing to do, but this isn't always so. If you give bar a type signature bar :: (Fractional a) => a bar = foo 0.1 then instead the constraint solver is faced with forall a . Fractional a => forall t . (Num (Scalar t), Scalar t ~ a) => Fractional (AD t) which simplifies to forall a . Fractional a => forall t . Num a => Fractional a so now the implication is easily solved, because the desired conclusion (Fractional a) is available as a hypothesis. Hope this helps, Adam P.S. Yet more information on the GHC constraint solver is in Dimitrios Vytiniotis, Simon Peyton jones, Tom Schrijvers, and Martin Sulzmann. 2011. OutsideIn(X): modular type inference with local assumptions. J. Funct. Program. 21, 4-5 (September 2011), 333-412 (https://research.microsoft.com/apps/pubs/default.aspx?id=162516)

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

-- The University of Strathclyde is a charitable body, registered in Scotland, with registration number SC015263.