Here's a bit of an abstract question since my actual example is not self contained: I've got a OCaml tactic that builds a proof term for the current goal, which requires introducing constraints on these universes from the goal and some monomorphic universes. The tactic uses unification to ensure that these constraints are in place and it also calls `Unsafe.tclEVARS sigma`

. I can verify that the rest of the proof script (after calling the tactic) has the right universe constraints. However, at `Qed`

, my proof term no longer typechecks. Apparently that's because none of the constraints that were introduced are available any more. I get "... cannot be applied to ... because the <nth> term has type `Type@{U1}`

should be coercible to `Type@{U2}`

" errors for universes which, before Qed, had a `U1 = U2`

constraint.

Is there something special I need to do to handle/register the constraints so that they are available at `Qed`

?

(I can copy the proof term and give it to `refine`

and then everything works so my tactic must be missing something.)

Could it be because the tactic solves the goal by unifying the goal evar with the proof term?

What does Show Universes say?

A whole lot of undefined universes, interestingly enough!

let me simplify things a bit.. there are too many universes right now to say what's going on.

Okay, I don't think I can get this down to an acceptable level for this kind of channel. But learning about `Show Universes`

was already very helpful and it helped me realize that I was wrong in what I wrote before: not all constraints I expected actually end up being created and the missing one explains the `Qed`

failure.

I am beginning to understand what's going on: I have a parameter `MyAssum@{univ} : Type@{univ} -> Prop`

. I use a "pattern term" `MyAssum@{mono1} T`

with `T`

being an evar of type ` Type@{mono2}`

and I unify that with (the type of) an assumption in my context of type `MyAssum@{poly} X`

with `X: Type@{poly}`

. Unification succeeds but instead of `mono1 = poly`

and `mono2 = poly`

I get `mono1 = poly`

(from `MyAssum`

) and `new_universe = poly`

, where `new_universe`

(I think) is the result of refreshing the universes when unifying `Type@{poly}`

with `Type@{mono1}`

. The trouble is that the proof term I build assumes that I can use the `mono2`

universe from the pattern with terms found in the goal but there is *nothing * that connects the universes, despite everything unifying successfully. `new_universe`

has no relation to `mono2`

, only to `poly`

.

Is this a general restriction of `refresh_universes`

, that it loses the connection between the new and the old universe?

What actually is the specification of `refresh_universes`

?

A simpler question (maybe): does `refresh_universes`

assume that the (refreshed) term is later typechecked in its original context so that the new universes get all the right constraints?

Last updated: Dec 06 2023 at 15:01 UTC