Well, a good reason for a test case to fail is that the test case is wrong. 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...