A recursive type nested inside a generic one

The rule: when a type’s recursive occurrence sits inside a generic type’s parameter — Node(Wrap<Rose>) rather than Node(Rose) — the definition is accepted, but a match on it is refused with E0064.

This is a different thing from the indexed families (length-indexed vectors and the like) listed under Current limitations. It is about where the recursion sits, not about indexing.

What the compiler refuses

This is the golden test tests/golden/error/nested_inductive_family_match.tg:

// == matching on a nested inductive family is rejected, not hung (ADR 11.8.26c)
//
// `Rose`'s recursive occurrence sits under a generic parameter, so its
// encoding is the vacuous `μα_Rose. α_Rose` and the inner-μ peel has no
// structural head to reach. Before the fixpoint guard this file did not
// produce an error — it spun in Body Elaboration at 100% CPU and flat RSS,
// which is why ADR 29.6.26e AC 11's fixture could not be written.
//
// Complementary to `termination_unsupported_family.tg`, which is a `Nat`
// cursor rejected by the *termination* gate: this one never reaches that
// gate, because Body Elaboration rejects it first.
type Wrap<T> = W(T)
type Rose = Node(Wrap<Rose>)

fn depth(r: Rose) -> Nat {
    match r { Node(w) => match w { W(inner) => 1 + depth(inner) } }
}

fn main() -> Nat { 0 }

albite check rose.tg prints:

[E0064] Error: cannot match on `Rose`: its recursive occurrence is nested under generic type `Wrap`, so its μ-encoding (binder `α_Rose`) does not unfold to a structural type
    ╭─[rose.tg:16:5]
    │
 16 │     match r { Node(w) => match w { W(inner) => 1 + depth(inner) } }
    │     ───────────────────────────────┬───────────────────────────────  
    │                                    ╰───────────────────────────────── 
    │ 
    │ Note: break the nesting with a non-generic intermediate type, in place of `Wrap<Rose>`
────╯

The error points at the match, not at the type. That is deliberate and a little surprising: the definition on line 13 is fine, and nothing complains until you try to take a value apart.

The same applies to the generic types you are most likely to reach for. type Tree = Node(List<Tree>) — a tree whose children are a List of trees — is this shape exactly, and a match on it is refused the same way — with the message naming List, the generic type the recursion passes through.

What it means

albite explain error E0064 says:

A type is a nested inductive family when its recursive occurrence sits under a generic parameter — Wrap<Rose> rather than Rose. Phase 1 does not support matching on one.

[…]

The type definition is accepted; only a match on it is rejected. The fix is to break the nesting with a non-generic intermediate type, which gives the recursion a concrete constructor to stop at.

Ordinary and mutual recursion are unaffected, and so is a generic ADT whose parameter is instantiated at a non-recursive type (Wrap<Nat>).

(Abridged: one paragraph on the compiler’s internal encoding of the type is omitted — albite explain error E0064 prints it in full.)

What to write instead

Replace the generic container with a type of your own that holds exactly this case. This is tests/golden/check/docs_recursion_under_a_generic.tg:

// Rejected: `type Rose = Node(Wrap<Rose>)` hides the recursion under a
// generic parameter, and every `match` on it is refused.
// Accepted: a non-generic intermediate type gives the recursion a
// concrete constructor to stop at.
type Rose = Node(Nat, RoseKids)
type RoseKids = NoKids | Kid(Rose, RoseKids)

fn size(r: Rose) -> Nat {
    match r { Node(v, kids) => 1 + size_kids(kids) }
}

fn size_kids(ks: RoseKids) -> Nat {
    match ks { NoKids => 0, Kid(r, rest) => size(r) + size_kids(rest) }
}

fn main() -> Nat {
    size(Node(1, Kid(Node(2, NoKids), Kid(Node(3, NoKids), NoKids))))
}

albite run prints 3.

Rose and RoseKids refer to each other — an ordinary pair of mutually recursive types, which the compiler handles, and which the termination check follows across size and size_kids. RoseKids is a List<Rose> written out by hand; the cost of the workaround is that you write it once per element type.

Ask the compiler

albite explain error E0064
albite doctor check type vacuous-mu <file>

The second finds this shape in a file before a match turns it into an error.