Lack of polymorphic inference in haskell when a binding is absent

Question

Type get generalized or not depending on the presence or absence of a binding. This can lead to unexpected failure.

Is this a normal behavior, and is there a reason why ?

{-# LANGUAGE RankNTypes #-}


data IFix0 f a   = IFix0 ( f (IFix0 f) a   ) | In0 a 


msfcata0_OK :: (forall r. (a -> r a) -> (r a -> a) -> f r a -> a) -> (forall z. IFix0 f z) -> a 
msfcata0_OK f = go where go (IFix0 x) = f In0 go x
                         go (In0 v)   = v


msfcata0_KO :: (forall r. (a -> r a) -> (r a -> a) -> f r a -> a) -> (forall z. IFix0 f z) -> a 
msfcata0_KO f  (IFix0 x) = f In0 (msfcata0_KO f) x  -- Couldn't match type ‘IFix0 f a’ with ‘forall z. IFix0 f z’
msfcata0_KO f   (In0 v)  = v

Siriasis

Answer 1

Here's a very small rewrite to show what's going on a bit better.

{-# Language ScopedTypeVariables, RankNTypes #-}

data IFix0 f a = IFix0 (f (IFix0 f) a) | In0 a


msfcata0_OK
    :: forall f a.
       (forall r. (a -> r a) -> (r a -> a) -> f r a -> a)
    -> (forall z. IFix0 f z) -> a
msfcata0_OK f = go
  where
    go :: IFix0 f a -> a
    go (IFix0 x) = f In0 go x
    go (In0 v)   = v


msfcata0_KO
    :: forall f a.
       (forall r. (a -> r a) -> (r a -> a) -> f r a -> a)
    -> (forall z. IFix0 f z) -> a
msfcata0_KO f (IFix0 x) = f In0 (msfcata0_KO f) x -- line 21
msfcata0_KO f (In0 v)   = v

And then the error:

    • Couldn't match type ‘IFix0 f a’ with ‘forall z. IFix0 f z’
      Expected type: IFix0 f a -> a
        Actual type: (forall z. IFix0 f z) -> a
    • In the second argument of ‘f’, namely ‘(msfcata0_KO f)’
      In the expression: f In0 (msfcata0_KO f) x
      In an equation for ‘msfcata0_KO’:
          msfcata0_KO f (IFix0 x) = f In0 (msfcata0_KO f) x
    • Relevant bindings include
        x :: f (IFix0 f) a (bound at free.hs:21:22)
        f :: forall (r :: * -> *). (a -> r a) -> (r a -> a) -> f r a -> a
          (bound at free.hs:21:13)
        msfcata0_KO :: (forall (r :: * -> *).
                        (a -> r a) -> (r a -> a) -> f r a -> a)
                       -> (forall z. IFix0 f z) -> a
          (bound at free.hs:21:1)
   |
21 | msfcata0_KO f (IFix0 x) = f In0 (msfcata0_KO f) x -- line 21
   |                                  ^^^^^^^^^^^^^

So let's start with looking at the error message. It's saying (msfcata0_KO f) has the type (forall z. IFix0 f z) -> a but the second argument of f needs to be IFix0 f a -> a. That latter type is a specialization with r ~ IFix0 f, which follows from passing In0 as the first argument to f.

And it should be clear that those types don't match up that way. f cannot use an argument of type (forall z. IFix0 f z) -> a the same way it could use an argument of type IFix0 f a -> a. To do anything with the former, it needs to pass it a polymorphic value. To use the latter, it may make use of the fact that a is fixed within the context of f and pass in a value that works with a specific choice of a.

So what's different in msfcata0_OK? Well, when you create a local binding without providing it a type, the type is locally inferred. I used ScopedTypeVariables to specify the inferred type in my rewrite of that function. (Note that this means the f and a types there are the ones bound in the top-level type signature.) This type is compatible with the type of f, so it isn't an error to pass go to f.

This raises an obvious question though: If GHC couldn't unify (forall z. IFix0 f z) -> a with IFix0 f a -> a in msfcata0_KO, why can it do so in msfcata0_OK? The difference is the subtyping direction. In msfcata0_OK, an expression of type IFix0 f a -> a is being produced as a value of type (forall z. IFix0 f z) -> a, and that's fine. In msfcata0_KO, an expression of type (forall z. IFix0 f z) -> a is being consumed by something that requires a value of type IFix0 f a -> a, and that doesn't work. The direction of subtyping of polymorphic values depends on whether the type is in a positive or negative position.

In a positive position, a concrete type is a subtype of a polymorphic type. You can use a value of type (forall a. a) as if it was a value of type Int or Bool, so (forall a. a) is a supertype of Int, Bool, and any other concrete type. But in a negative position, this is reversed. A function of type Int -> Bool can accept an argument of type (forall a. a), but a function of type (forall a. a) -> Bool cannot accept an argument of type Int, so in a negative position (forall a. a) is a subtype of Int.

So going back to the original question at a high level - by allowing GHC to infer a type from scratch for go, you changed where it was doing the unification of more polymorphic and less polymorphic types. This resulted in the subtyping relationship working the correct direction, so things typechecked successfully.

Jeepers

key point : "when you create a local binding without providing it a type, the type is locally inferred" ... meaning there is no new local opaque type variable z (leading after local quantification to to Exist z. (IFix0 f z -> a which can't required to be a by a client). discharge/quantification is only done as the last step of the global msfcata0_OK typing – Siriasis

Follow up (maybe another SO question ?) : In msfcata0_KO our term is a client of the type-closed term msfcata0_KO, with all its requirement. The client can't decide what the existential z is, in particular he can't impose a/ generate z ~ a (there is no z to him just some unknown). But this happens because we are typechecking closed type-terms. Why GHC doesn't track a context with typechecking, carrying (z ~ a) (thus checking essentially as inmsfcata0_OK ) ? (I imagine that would give better error message too..) – Siriasis

@Siriasis Yeah, GHC could definitely give better context for the type errors when dealing with matching polytypes against monotypes. It really matters for understanding the error how the polymorphism is being used. – Jeepers