The trouble with writing good test cases for this type theory is that the ones that create general enough unification problems to be interesting require (as far as I can tell) fifth-order signatures to be typechecked. Or maybe it's fourth; what would you call a signature with a type family in it like
c : ({a:world} (({b:world} ((t -o t) -> t) -> t) -> t)) -> type.
?
My brain already becomes mushy at about three and a half levels of functional left-hand-side nesting, so it is complete purée now.
—
---
ETA:
Hey, I can get it down by one order after all:
c : ({a:w} (({b:w} (t @ p -> t @ q) -> t) -> t)) -> type
exhibits enough unificational generality, and it's almost something I can make sense of: a type family indexed by a sort of strong double-negation of a refinement of the type t -> t. Maybe with a merely half-mushy brain I can make some progress now...
