QpfTypes icon indicating copy to clipboard operation
QpfTypes copied to clipboard

Indexed families should fast-fail rather than spin forever

Open Equilibris opened this issue 1 year ago • 0 comments

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.

Equilibris avatar Jul 02 '24 17:07 Equilibris