Type inference in templates

Question

I noticed that the GHC wanted to get a type signature, which I think should be output. I minimized my example before that, which almost certainly does nothing significant (I do not 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 in the definition of y I get an 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. 

Being caught by the terrible restriction of monomorphism in multiple cases, I included NoMonomorphismRestriction , but this does not change the behavior.

Why is type y not inferred as the output type of a function?

Answer 1

Monomorphism restriction applies only to top-level bindings. The compiler knows about the real type y , but there is no way to infer a monomorphic type for it; what causes the type error. If you really want to disable monomorphic let bindings, you need to use the correct extension:

 {-# LANGUAGE NoMonoLocalBinds #-} 

It compiles your code.

For more information on bindings to a monomorphic constraint, see the wiki .

Answer 2

I am not familiar with the GHC input algorithm. However, here I can guess why the compiler cannot 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 the Refl match proves Char ~ rq , so y at the end has the correct return type Foo (Bar rp rq) . The program is type checking.

However, suppose instead that we have

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

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

Now suppose we have no type annotation. How will it compile, what is the correct type for the binding let y = ... ? In the end, there are (at least) two of them leading to the correct set of all rebar .

It may also explain why if you add _ -> y , it works: in this case, the compiler knows that Refl not required. Instead, if you add y -> error "" , information about y will not be displayed.

The actual full story may be more complicated than the higher: here I just ignore the information coming from the definition of y , i.e. rebar p1 p2 x . In other words, I consider only the restrictions that the context places on the definition on y , and not those that go in the other direction.

In your example, an equation of type is actually rp' ~ rp'' , which seems to be inappropriate wrt type y at the end. Perhaps the compiler is not smart enough to figure this out.