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: May 28 2023 at 16:30 UTC