Fix #5368: Canonical structure unification fails. #6436
Conversation
Universe instances were lost during constructions of the canonical instance.
| @@ -218,6 +218,8 @@ let check_conv_record env sigma (t1,sk1) (t2,sk2) = | |||
| let t' = EConstr.of_constr t' in | |||
| let t' = subst_univs_level_constr subst t' in | |||
| let bs' = List.map (EConstr.of_constr %> subst_univs_level_constr subst) bs in | |||
| let params = List.map (fun c -> subst_univs_level_constr subst c) params in | |||
There was a problem hiding this comment.
Could this bug have been prevented by a better API? For example, couldn't the types distinguish whether we applied the substitution or not?
There was a problem hiding this comment.
Hard to tell. But it's clear that the current API is not satisfactory. In particular, subst_univs_level_constr is somewhat misleading, we should use subst_instance_constr instead, but it's not yet defined in EConstr.
|
I've launched a bench here, but I highly doubt it'll have any observable consequence. The main reason being that in absence of polymorphic canonical structures, this shouldn't perform any additional substitution, and precisely because of the present bug the latter are not usable. |
|
No observable change in time nor memory. |
|
Build was canceled, restarting. |
…re unification fails.
Universe instances were lost during constructions of the canonical instance.