Allow some form of type-level lemma

can cat_nil already be optimized away by ghc -O? Or might it return _|_? (is it possible for its recursion not to terminate?)

Replying to Isaac Dupree:

can cat_nil already be optimized away by ghc -O? Or might it return _|_? (is it possible for its recursion not to terminate?)

I am pretty sure that cat_nil cannot be optimized away. Consider the following additions to the program:

type instance Cat [a] () = [(a,a)]

unsoundCoerce :: Exp (Cat [a] ()) -> Exp [a]
unsoundCoerce = coerce undefined

If cat_nil is optimized away then unsoundCoerce exp does an invalid conversion from Exp [(a,a)] to Exp [a].