Ugly retyping-hack to solve universe-constrains

[fakusb]

The ocaml-function Coq.retype (and Coq.tclRETYPE in #34 ) are used at various points. This has to do with the plugin building coq-terms without updating universe constrains (I guess?). This seems very fishy and like an ugly hack.

I need to investigate the right methode to compose terms without breaking the universe-constrains.

This might be related with the functions used #35 , or in general with the way the ocaml-side interfaces with the coq-side.

[MSoegtropIMC]

@fakusb : I started to clean up the code - also to fix the remaining exponential blow up (the tactic run time grows about 3^n, where n is term length in simple cases). I just want to avoid double work. If you are also working on improving aac-tactics, we should join forces.

[MSoegtropIMC]

Sorry, I just saw now that this is 5 years old - but the code is still there and I also stumbled across it.

[SkySkimmer]

The problem is typically https://github.com/coq-community/aac-tactics/blob/d3f4d8875382dc918ebeab3f04438ea6cb97ea68/src/aac_rewrite.ml#L110-L112 (mk_letin does the retype)

We have Theory.Stubs.eval which is

AAC.Internal.eval :
forall {X : Type@{AAC_tactics.AAC.58}} {R : relation X} [e_sym : idx -> Sym.pack]
  [e_bin : idx -> Bin.pack], (idx -> unit_pack e_bin) -> T e_sym -> X

and x some type (ie x : Type@{u} for some u), so for mkApp (eval, [|x; ...|]) to be valid we need u <= AAC.58.

Generally every time we have a mkApp we have preconditions such that is is well-typed, but only up to some universe constraints. To remove the tclRETYPE calls we need to explicitly produce the universe constraints.

So in the above example we would do something like

let eval = Coq.get_efresh Theory.Stubs.eval in
let (_, ety, _) = destProd sigma eval in
let euniv = destSort sigma ety in
let xuniv = Retyping.get_sort_of env sigma x in
let sigma = Evd.set_leq_sort env sigma xuniv euniv in
let eval = mkApp (eval, [|x; ...|]) in
Proofview.Unsafe.tclEVARS sigma >>= fun () ->
mk_letin ... (* if done for everything mk_letin can stop doing tclRETYPE *)

An intermediate solution is to replace let c = mkApp (hd, args) in tclRETYPE c >>= fun () -> ... with let sigma, c = Typing.checked_appvect env sigma hd args in tclEVARS sigma >>= fun () -> .... checked_appvect assumes that the subterms are well typed and only checks the application.

In the above example we would do

let sigma, eval = Typing.checked_appvect env sigma (Coq.get_efresh Theory.Stubs.eval) [|x; ...|] in
Proofview.Unsafe.tclEVARS sigma >>= fun () ->
mk_letin ... (* if done for everything mk_letin can stop doing tclRETYPE *)

or since only the first argument has universe constraint implications

let sigma, eval = Typing.checked_appvect env sigma (Coq.get_efresh Theory.Stubs.eval) [|x|] in
let eval = mkApp (eval, [|...|]) in
Proofview.Unsafe.tclEVARS sigma >>= fun () ->
mk_letin ... (* if done for everything mk_letin can stop doing tclRETYPE *)

In all cases we need to enter or more likely enter_one to get an env (or factorize checked_appvect into a tactic which does enter_one).

[MSoegtropIMC]

@SkySkimmer : thanks for sharing your insights on this - very useful!