Akio Takano | 13 May 04:47 2013
Picon

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
Attachment (forall.hs): application/octet-stream, 737 bytes
_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Adam Gundry | 13 May 11:16 2013
Picon
Picon

Re: A type not inferred with RankNTypes

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.
Simon Peyton-Jones | 13 May 16:55 2013
Picon

RE: A type not inferred with RankNTypes

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 <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

 

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

_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Gmane