### Re: A type not inferred with RankNTypes

Adam Gundry <adam.gundry <at> strath.ac.uk>

2013-05-13 09:16:56 GMT

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.