QpfTypes
QpfTypes copied to clipboard
Indexed families should fast-fail rather than spin forever
In the current system, one can write:
data QpfList2 α
| nil
| cons : α → QpfList2 Bool → QpfList2 α
^^^^
Notice the improper use of Bool, which means this definition of QpfList2 uses α as an index.
This should throw an error, instead, currently this causes the elaborator to spin forever.