Documentation

\(a :: *) -> ifix (getShadF a) a

Test that shadowing does not result in variable capture. The definition is as follows:

/\(a :: *) -> wrap (getShadF a) a (\(x : a) -> /\(f :: * -> *) -> \(y : f i) -> 0)

Type checking this term we eventually reach

NORM (vPat (\(a :: k) -> ifix vPat a) arg)

(where in our case vPat is shadF and arg is a), which, if we were naive, would unfold into

a -> all (a :: * -> *). a a -> integer

i.e. we substituted the outer a for i, but due to variable capture via all that outer a now became an inner one, which would be a bug.

But that problem is already solved before type checking starts as we rename the program and that makes all binders uniques, so no variable capture is possible due to the outer and inner bindings being distinct.

ifix recUnitF ()

Test that a binder in a pattern functor does not get duplicated. The definition is as follows:

/\(a :: *) -> \(ru : recUnit) -> unwrap ru {a} ru

Type checking this term we eventually reach

NORM (vPat (\(a :: k) -> ifix vPat a) arg)

(where in our case vPat is recUnitF and arg is ()), which, if we were naive, would unfold into

all (r :: *). ifix (\(rec :: * -> *) (i :: *) -> all (r :: *). rec i -> r -> r) () -> r -> r

and break global uniqueness as the all (r :: *) binder appears twice.

But this doesn't happen in the actual code, since when a variable gets looked up during type normalization, its value gets renamed, which means that a fresh variable will be generated for the inner binder and there will be no shadowing.