Strictly positive types

The rule: a type’s recursive occurrences may never appear to the left of an arrow, at any depth. The compiler checks every type definition against it, and there is no annotation that turns the check off.

What the compiler refuses

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

// ADR 7.8.26e: the headline witness. `Bad` occurs left of an arrow, so
// `omega(Mk(omega))` would diverge with no syntactic recursion anywhere.
// This is a size-1 SCC and so is absent from `mutual_recursion_groups` -
// the regression test for the all-definitions worklist.
type Bad = Mk(Bad -> Bad)

albite check bad.tg prints:

[E0061] Error: `Bad` is not strictly positive: `Bad` reaches a forbidden position in constructor `Mk`, field 0
   ╭─[bad.tg:5:1]
   │
 5 │ type Bad = Mk(Bad -> Bad)
   │ ────────────┬────────────  
   │             ╰────────────── 
   │ 
   │ Help: move the occurrence out of the argument position — store the result of the function rather than the function itself
   │ 
   │ Note: strict positivity is required for structural recursion to be well-founded
───╯

What it means

albite explain error E0061 says:

A type definition is strictly positive when its own recursive occurrences never appear to the left of an arrow, at any depth. Albite requires this, because it is what makes “structural subterm” a well-founded relation — the relation termination checking rests on.

Without the restriction a type can encode a fixpoint combinator, yielding a diverging term with no syntactic recursion anywhere, and at Void a closed inhabitant of the empty type.

Note this is strict positivity, not positivity: two occurrences to the left of an arrow do not cancel out. Mk((T -> Nat) -> Nat) is rejected too.

A violation can also be inherited. If Fn1<T> uses T to the left of an arrow, then B(Fn1<Bad>) places Bad in a forbidden position even though no arrow appears in Bad’s own source. The message names the intermediate type and parameter when that is what happened.

There is no escape hatch: a rejected type is fixed, not annotated. The usual fix is to store the result of the function rather than the function itself, or to break the cycle with an index into a separately-owned collection.

What to write instead

Follow the Help: line: let the type appear in what a function returns, never in what it takes. This is tests/golden/check/docs_positivity.tg:

// Rejected: `type Bad = Mk(Bad -> Bad)` puts `Bad` left of an arrow.
// Accepted: store the result of the function, not the function.
type Good = Mk(Nat -> Good) | Done(Nat)

fn value(g: Good) -> Nat {
    match g { Mk(f) => 0, Done(n) => n }
}

fn step(g: Good, input: Nat) -> Good {
    match g { Mk(f) => f(input), Done(n) => Done(n) }
}

fn main() -> Nat {
    let g = Mk(fn(n: Nat) => Done(n + 1));
    value(step(g, 41))
}

Good still refers to itself, and still holds a function — but only as the function’s result, which is allowed. albite run prints 42.

Recursive types with no arrows in them at all — List, Tree, Option — are unaffected. So is a recursive type nested inside a generic one, as far as this rule goes; matching on one is a separate restriction, described in A recursive type nested inside a generic one.

Ask the compiler

albite explain error E0061
albite doctor check type positivity <file> --verbose

The first prints the explanation above. The second explains why each type in a file that compiles passed — useful when a type is accepted and you expected otherwise.