Ugly retyping-hack to solve universe-constrains about aac-tactics HOT 4 OPEN

The problem is typically

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).

from aac-tactics.

@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.

from aac-tactics.

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

from aac-tactics.

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

from aac-tactics.