Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

🐛🕳 Debug holes #14

Open
wants to merge 9 commits into
base: main
Choose a base branch
from
Prev Previous commit
Next Next commit
fix: in unleash_hole, goal type was quoted in the wrong env
  • Loading branch information
jonsterling authored and favonia committed Aug 27, 2023
commit e748a0138b613129c8c331a23e1c9b5c9f731a0c
14 changes: 6 additions & 8 deletions src/elaborator/Elaborator.ml
Original file line number Diff line number Diff line change
@@ -12,19 +12,17 @@ module T = R.Tactic
let unleash_hole loc : T.check =
T.Check.peek @@ fun goal ->
let bnds = R.Eff.Generalize.quote_ctx () in

let p =
let top_tp =
let make_pi bnd bdy =
match bnd with
| R.Eff.Generalize.VirType tp -> S.VirPi (tp, bdy)
| R.Eff.Generalize.Type tp -> S.Pi (tp, bdy)
in
let tp =
R.Eff.with_top_env @@ fun () ->
R.Eff.eval @@
S.vir_pi S.tp_ulvl @@ List.fold_right make_pi bnds @@ R.Eff.quote goal.tp
in
Eff.unleash ?loc None @@ R.ResolveData.Axiom {tp}
S.vir_pi S.tp_ulvl @@ List.fold_right make_pi bnds @@ R.Eff.quote goal.tp
in
let p =
let vtp = R.Eff.with_top_env @@ fun () -> R.Eff.eval top_tp in
Eff.unleash ?loc None @@ R.ResolveData.Axiom {tp = vtp}
in
T.Check.infer @@
let head = R.Structural.global_var p @@ R.ULvl.base in