hierarchy-builder icon indicating copy to clipboard operation
hierarchy-builder copied to clipboard

`mixin-instance-type->mixin-src` does not use the typing information

Open Tragicus opened this issue 9 months ago • 4 comments

mixin-instance-type->mixin-src produces clauses mixin-src clauses that call the unification, without giving the type of the evars it creates. This can lead to a unification of the form S.sort ?a = ?b where S.sort is a primitive projection. However, then Rocq retypes S.sort ?a and since ?a has type ?A which is not an inductive type, it fails. N.B. Using coq.typecheck feels a bit heavy to do this, when we just have to create the evar with the right type. Is there a better way to do this?

Tragicus avatar Mar 04 '25 15:03 Tragicus