A type not inferred with RankNTypes

[Adam Gundry]

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.