Why class constraint in type synonym needs RankNTypes

Question

This compiles fine:

type List a = [a] 

But when I introduce a class constraint, the compiler asks for RankNTypes to be included:

type List2 a = Num a => [a] 

After including that extension, it compiles fine. Why is that extension required for compiling the code ?

Edit: Why do I need the constraint in the first place ?

I was inspecting this Lens type (type RefF a b = Functor f => (b -> f b) -> (a -> f a)) from this post and found out that it actually needed RankNTypes because of the Functor constraint.

Answer 1

It's not standard

In which the question is answered

The simple answer is that standard Haskell does not allow qualified type synonym declarations, i.e. a type synonym involving =>. Per the 2010 Report, the syntax for a type synonym declaration is:

type simpletype = type

where type, if you look down at Section 4.1.2, can't contain a context.

By the way, the presence of the type variable a in the context doesn't matter. With no extensions, GHC rejects

type IrrelevantConstraint a = Num Int => [a] 

or, for that matter,

type QualifiedT = Num Int => String 

Furthermore, even if such a type synonym were permitted, no nontrivial use of it would be standard Haskell, as manual substitution shows:

List2 a      === forall a.   Num a => [a]        -- Okay List2 a -> b === forall a b. (Num a => [a]) -> b -- Not okay a -> List2 b === forall a b. a -> Num b => [b]   -- Not okay 

And so forth for Maybe (List2 a) etc. In each case, it's not that it's a higher-rank type in the usual sense. I've added explicit forall notation, which is also of course not standard, to emphasize that fact.

Rather, the problem is that each type is inappropriately qualified because => appears inside the type. Again, if you look at the 2010 Report sections on expression type signatures and declarations, you'll see that => is not strictly speaking part of a type, but rather a syntactically distinct thing, e.g.:

exp → exp :: [context =>] type

Since List2 is invalid Haskell2010, some language extension is necessary for it to work. It's not specifically documented that RankNTypes permits qualified type synonym declarations, but as you've noticed it has that effect. Why?

There's a hint in the GHC docs on RankNTypes:

The -XRankNTypes option is also required for any type with a forall or context to the right of an arrow (e.g. f :: Int -> forall a. a->a, or g :: Int -> Ord a => a -> a). Such types are technically rank 1, but are clearly not Haskell-98, and an extra flag did not seem worth the bother.

The g example is related to our List2 problem: there's no forall there, but there is a context to the right of an arrow, which is the third example I gave above. As it happens, RankNTypes enables the second example too.

A side trip through Template Haskell

In which a skippable detour is taken, Mr. Forall is discovered in an unexpected place, and ranks and contexts are pondered

I don't know whether the Template Haskell representation of a declaration is necessarily linked to the typechecker's internal representation or operation. But we find something a bit unusual: a forall where we wouldn't expect, and with no type variables:

> import Language.Haskell.TH > :set -XTemplateHaskell > runQ [d|type List2 a = Num a => [a]|] [TySynD List2_2         [PlainTV a_3]         (ForallT []                  [ClassP GHC.Num.Num [VarT a_3]]                  (AppT ListT (VarT a_3)))]  -- simpler example: > runQ [d|type T = Num Int => Int|] [TySynD T_0         []         (ForallT []                  [ClassP GHC.Num.Num [ConT GHC.Types.Int]]                  (ConT GHC.Types.Int))] 

The notable thing here is the apparently-spurious ForallT. In Template Haskell, this makes sense because ForallT is the only constructor of Type with a Cxt field, i.e. that can contain a context. If the typechecker similarly conflates forall and constraint contexts, it'd make sense that RankNTypes affected its behavior. But does it?

As implemented in GHC

In which it is discovered why RankNTypes allows List2

The precise error we get is:

Illegal polymorphic or qualified type: Num a => [a] Perhaps you intended to use RankNTypes or Rank2Types In the type declaration for `List2' 

Searching through the GHC source reveals that this error is generated in TcValidity.hs. The entry point we're concerned with is checkValidType.

We can verify that the compiler actually enters there by compiling with -ddump-tc-trace; the last debug output before the error message is:

Starting validity check [Type constructor `List2'] checkValidType Num a => [a] :: * 

Continuing in checkValidType, we see that, absent RankNTypes, the RHS of a type synonym must have rank 0. (Unfortunately the debug output doesn't specify the value of ctxt here, but it's presumably TySynCtxt.)

The note just above checkValidType define ranks in this context thus:

    basic ::= tyvar | T basic ... basic      r2  ::= forall tvs. cxt => r2a     r2a ::= r1 -> r2a | basic     r1  ::= forall tvs. cxt => r0     r0  ::= r0 -> r0 | basic 

That comment squares with the Template Haskell experiment, i.e. that a rank-0 type cannot involve =>, and any type involving => must include a forall and therefore be rank 1 or 2, even if there are no type variables in the forall. In the terminology outlined in TcType, contexts only appear in sigma types.

In other words, as implemented the typechecker rejects the RHS of List2 because it interprets the RHS as being rank 1 on account of its class qualification.

The branch that leads to our error message begins here. If I understand correctly, theta represents the constraint context. The core of the first line of the do block is forAllAllowed rank, which does what it sounds like. Recall from above that the RHS of a type synonym is restricted to rank 0; since a forall is not permitted, we get an error.

This explains why RankNTypes overrides this limitation. If we trace where the parameter rank comes from, through rank0 in checkValidType and then through the preceding few lines, we find that the RankNTypes flag basically overrides the rank0 restriction. (Contrast the situation with default declarations.) And because the extra context was treated as a rank error, RankNTypes permits it.