For example, the Branches function in #172 computes a type as either a (right-nested) Pair or Unit (terminating the list). But if we take a value of that type and try to eliminate it by use of first, it won’t work; there’s no way for definitional equality to reduce the call to Branches to determine the actual type.
We might be able to work around this by the addition of eliminators specific to values typed by Branches, but in general it appears that our definitional equality isn’t strong enough.
For example, the
Branchesfunction in #172 computes a type as either a (right-nested)PairorUnit(terminating the list). But if we take a value of that type and try to eliminate it by use offirst, it won’t work; there’s no way for definitional equality to reduce the call toBranchesto determine the actual type.We might be able to work around this by the addition of eliminators specific to values typed by
Branches, but in general it appears that our definitional equality isn’t strong enough.