Understanding a rank 2 type alias with a class constraint

Question

I have code that frequently uses functions that look like

foo :: (MyMonad m) => MyType a -> MyOtherType a -> ListT m a

To try to shorten this, I wrote the following type alias:

type FooT m a = (MyMonad m) => ListT m a

GHC asked me to turn on Rank2Types (or RankNTypes), but didn't complain when I used the alias to shorten my code to

foo :: MyType a -> MyOtherType a -> FooT m a

By contrast, when I wrote another type alias

type Bar a b = (Something a, SomethingElse b) => NotAsBar a b

and used it in a negative position

bar :: Bar a b -> InsertTypeHere

GHC loudly yelled at me for being wrong.

I think I have an idea of what's going on, but I'm sure I could get a better grasp from your explanations, so I have two questions:

• What are the type aliases actually doing/what do they actually mean?
• Is there a way to get the terseness in both cases?

Answer 1

There are essentially three parts to a type signature:

1. variable declarations (these are usually implicit)
2. variable constraints
3. the type signature head

These three elements essentially stack. Type variables must be declared before they can be used, either in constraints or elsewhere, and a class constraint scopes over all uses within the type signature head.

We can rewrite your foo type so the variables are explicitly declared:

foo :: forall m a. (MyMonad m) => MyType a -> MyOtherType a -> ListT m a

The variable declarations are introduced by the forall keyword, and extend to the .. If you don't explicitly introduce them, GHC will automatically scope them at the top level of the declaration. Constraints come next, up to the =>. The rest is the type signature head.

Look at what happens when we try to splice in your type FooT definition:

foo :: forall m a. MyType a -> MyOtherType a -> ( (MyMonad m) => ListT m a )

The type variable m is brought into existence at the top level of foo, but your type alias adds a constraint only within the final value! There are two approaches to fixing it. You can either:

• move the forall to the end, so m comes into existence later
• or move the class constraint to the top

Moving the constraint to the top looks like

foo :: forall m a. MyMonad m => MyType a -> MyOtherType a -> ListT m a

GHC's suggestion of enabling RankNTypes does the former (sort of, there's something I'm still missing), resulting in:

foo :: forall a. MyType a -> MyOtherType a -> ( forall m. (MyMonad m) => ListT m a )

This works because m doesn't appear anywhere else, and it's right of the arrow, so these two mean essentially the same thing.

Compare to bar

bar :: (forall a b. (Something a, SomethingElse b) => NotAsBar a b) -> InsertTypeHere

With the type alias in a negative position, a higher-rank type has a different meaning. Now the first argument to bar must be polymorphic in a and b, with appropriate constraints. This is different from the usual meaning, where bars caller chooses how to instantiate those type variables. It's not

In all likelihood, the best approach is to enable the ConstraintKinds extension, which allows you to create type aliases for constraints.

type BarConstraint a b = (Something a, SomethingElse b)

bar :: BarConstraint a b => NotAsBar a b -> InsertTypeHere

It's not quite as terse as what you hoped for, but much better than writing out long constraints every time.

An alternative would be to change your type alias into a GADT, but that has several other consequences you may not want to bring in. If you're simply hoping to get more terse code, I think ConstraintKinds is the best option.