hierarchy-builder
hierarchy-builder copied to clipboard
`mixin-instance-type->mixin-src` does not use the typing information
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?