Janno (Aug 17 2020 at 12:56): Janno (Aug 17 2020 at 12:56):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.)
Janno (Aug 17 2020 at 13:02):Could it be because the tactic solves the goal by unifying the goal evar with the proof term?
Gaëtan Gilbert (Aug 17 2020 at 13:30):What does Show Universes say?
Janno (Aug 17 2020 at 13:31):A whole lot of undefined universes, interestingly enough!
Janno (Aug 17 2020 at 13:33):let me simplify things a bit.. there are too many universes right now to say what's going on.
Janno (Aug 17 2020 at 13:53):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.
Janno (Aug 17 2020 at 16:05):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?
Janno (Aug 17 2020 at 16:39):What actually is the specification of refresh_universes?
Janno (Aug 18 2020 at 11:47):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