Documentation

Converts a GHC type-level Nat to a structural type-level natural (Peano).

Converts a structural type-level natural (Peano) to a GHC type-level Nat.

FunN n a b represents a function taking n linear arguments of type a and returning a result of type b.

The Arity type family exists to help the type checker fill in blanks. Chances are that you can safely ignore Arity completely if it's in the type of a function you care. But read on if you are curious.

The idea is that in a function like elim some of the type arguments are redundant. The function has an ambiguous type, so you will always have to help the compiler either with a type annotation or a type application. But there are several complete ways to do so. In elim, if you give the values of n, a, and b, then you can deduce the value of f (indeed, it's FunN n a b). With Arity we can go in the other direction: if b and f are both known, then we know that n is Arity b f

Arity returns a Nat rather than a Peano because the result is never consumed. It exists to infer arguments to functions such as elim from the other arguments if they are known.

Arity could theorically be an associated type family to the IsFunN type class. But it's better to make it a closed type family (which can't be associated to a type class) because it lets us give a well-defined error case. In addition, GHC cannot see that 0 /= 1 + (? :: Nat) and as a result we get some overlap which is only allowed in (ordered) closed type families.

The IsFun type class is meant to help the type checker fill in blanks. Chances are that you can safely ignore IsFun completely if it's in the type of a function you care. But read on if you are curious.

The type class IsFun is a kind of inverse to FunN, it is meant to be read as IsFunN a b f if and only if there exists n such that f = FunN n a b (n can be retrieved as Arity b f or ArityV f).

The reason why Arity (read its documentation first) is not sufficient for our purpose, is that it can find n if f is a linear function of the appropriate shape. But what if f is partially undetermined? Then it is likely that Arity will be stuck. But we know, for instance, that if f = a1 %1 -> a2 %1 -> c then we must have a1 ~ a2. The trick is that instance resolution of IsFun will add unification constraints that the type checker has to solve. Look in particular at the instance IsFunN a b (a' %p -> f)): it matches liberally, so triggers on quite underdetermined f, but has equality constraints in its context which will help the type checker.