Type Inference in Patterns

Question

I noticed that GHC wanted a type signature which I think should be inferred. I minimized my example down to this, which almost certainly does nothing meaningful (I don't recommend running it on your favorite types):

{-# LANGUAGE GADTs, RankNTypes, ScopedTypeVariables,
             TypeOperators, NoMonomorphismRestriction #-}
module Foo where

import Data.Typeable

data Bar rp rq

data Foo b = Foo (Foo b)


rebar :: forall rp rq rp' rp'' . (Typeable rp', Typeable rp'') 
     => Proxy rp' -> Proxy rp'' -> Foo rp -> Foo (Bar rp rq)
rebar p1 p2 (Foo x) =
  -- The signature for y should be inferred...
  let y = rebar p1 p2 x -- :: Foo (Bar rp rq)
  -- The case statement has nothing to do with the type of y
  in case (eqT :: Maybe (rp' :~: rp'')) of
    Just Refl -> y

Without a type signature on the definition of y, I get the error:

Foo.hs:19:20:
    Couldn't match type ‘rq0’ with ‘rq’
      ‘rq0’ is untouchable
        inside the constraints (rp' ~ rp'')
        bound by a pattern with constructor
                   Refl :: forall (k :: BOX) (a1 :: k). a1 :~: a1,
                 in a case alternative
        at testsuite/Foo.hs:19:12-15
      ‘rq’ is a rigid type variable bound by
           the type signature for
             rebar :: (Typeable rp', Typeable rp'') =>
                      Proxy rp' -> Proxy rp'' -> Foo rp -> Foo (Bar rp rq)
           at testsuite/Foo.hs:12:20
    Expected type: Foo (Bar rp rq)
      Actual type: Foo (Bar rp rq0)
    Relevant bindings include
      y :: Foo (Bar rp rq0) (bound at testsuite/Foo.hs:16:7)
      rebar :: Proxy rp' -> Proxy rp'' -> Foo rp -> Foo (Bar rp rq)
        (bound at testsuite/Foo.hs:14:1)
    In the expression: y
    In a case alternative: Just Refl -> y
Failed, modules loaded: none.

Having been caught by the dreaded monomorphism restriction on multiple occassions, I turned on NoMonomorphismRestriction, but that doesn't change the behavior.

Why is the type of y not inferred to be the output type of the function?

Coldblooded

I haven't the slightest idea. I found a fun fact though: if you add "_ -> y" under "Just Refl -> y", it works. – Marianomaribel

@AndrásKovács Weird! But _ -> error "" doesn't work! – Coldblooded

@leftaroundabout mentioned in this answer that "Still, the same [inference issues] can turn up even without the monomorphism restriction in RankNTypes code, it can't be avoided completely." Any thoughts on what exactly it is about my code that might cause it to fall into this "problematic RankNTypes" category? – Coldblooded

Answer 1

The monomorphism restriction applies only to top level bindings. The compiler is aware of the real type of y, but there is no way to infer a monomorphic type for it; that is the cause of the type error. If you really would like to turn off monomorphic let bindings, you have to use the correct extension:

{-# LANGUAGE NoMonoLocalBinds #-}

With it, your code compiles.

For much more detail about monomorphic let bindings, see the ghc wiki.

Daph

But you probably shouldn't use NoMonoLocalBinds, because monomorphic local bindings are turned on by one (or two?) of the extensions used, because those extensions are known to behave unpredictably with let generalization! – Lillith

Answer 2

I am not familiar with the typing algorithm of GHC. Still, here's my guess about why the compiler can not figure it out.

Consider this code:

rebar :: forall rp rq rp' rp'' . (Typeable rp', Typeable rp'') 
     => Proxy rp' -> Proxy rp'' -> Foo rp -> Foo (Bar rp rq)
rebar p1 p2 (Foo x) =
  let y = ... :: Foo (Bar rp Char)
  in case (eqT :: Maybe (Char :~: rq)) of
     Just Refl -> y

This should compile, since matching Refl proves Char ~ rq, hence y at the end has the correct return type Foo (Bar rp rq). The program passes type checking.

However, suppose we instead have

  let y = ... :: Foo (Bar rp rq)

in this case, y has already the correct type, and the Refl is useless. Again, the program passes type checking.

Now, suppose we have no type annotation. How would the compile figure out which is the correct type for the let y = ... binding? After all, there are (at least) two of them leading to a correct typing of the whole rebar.

This may also explain why if you add _ -> y it does work: in that case the compiler knows that the Refl is not needed. Instead, if you add y -> error "" no information about y can be deduced.

The actual full story may be more complicated than the above: here I am conveniently ignoring the information coming from the definition of y, i.e. rebar p1 p2 x. In other words, I am only considering the constraints the context puts on the definition on y, and not those going in the other direction.

In your example the type equation is actually rp' ~ rp'' which seems irrelevant w.r.t. the type of y at the end. Maybe the compiler is not smart enough to figure that out.

Demerol

Everything you said looks correct, but of course the crux of the issue is that the eqT refers to types which are irrelevant w.r.t y. It's not clear at all why GHC wouldn't be able to figure out the type of y, and your example doesn't seem to explain it, as you mentioned. – Coldblooded