From d369011c760aa888cfcc7a31a7ae1d534619097d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Sun, 3 Dec 2023 09:26:44 -0800 Subject: [PATCH 01/29] nit: more show instances --- src/fstar/FStar.CheckedFiles.fst | 7 +++++++ src/parser/FStar.Parser.Dep.fst | 10 +++++++--- 2 files changed, 14 insertions(+), 3 deletions(-) diff --git a/src/fstar/FStar.CheckedFiles.fst b/src/fstar/FStar.CheckedFiles.fst index c5aad72c7c1..1c1d9832a0e 100644 --- a/src/fstar/FStar.CheckedFiles.fst +++ b/src/fstar/FStar.CheckedFiles.fst @@ -25,6 +25,7 @@ open FStar.Getopt open FStar.Syntax.Syntax open FStar.TypeChecker.Env open FStar.Syntax.DsEnv +open FStar.Class.Show (* Module abbreviations for the universal type-checker *) module Syntax = FStar.Syntax.Syntax @@ -94,6 +95,12 @@ type tc_result_t = | Invalid of string //reason why this is invalid | Valid of string //digest of the checked file +instance _ : showable tc_result_t = { + show = (function Unknown -> "Unknown" + | Invalid s -> "Invalid " ^ show s + | Valid s -> "Valid " ^ show s); +} + (* * The cache of checked files *) diff --git a/src/parser/FStar.Parser.Dep.fst b/src/parser/FStar.Parser.Dep.fst index 6189e635977..11a9ace8741 100644 --- a/src/parser/FStar.Parser.Dep.fst +++ b/src/parser/FStar.Parser.Dep.fst @@ -34,6 +34,7 @@ open FStar.Const open FStar.String open FStar.Ident open FStar.Errors +open FStar.Class.Show module Const = FStar.Parser.Const module BU = FStar.Compiler.Util @@ -141,6 +142,10 @@ let dep_to_string = function | PreferInterface f -> "PreferInterface " ^ f | UseImplementation f -> "UseImplementation " ^ f | FriendImplementation f -> "FriendImplementation " ^ f +instance showable_dependence : showable dependence = { + show = dep_to_string; +} + type dependences = list dependence let empty_dependences = [] type dep_node = { @@ -763,7 +768,7 @@ let collect_one if data_from_cache |> is_some then begin //we found the parsing data in the checked file let deps, has_inline_for_extraction, mo_roots = from_parsing_data (data_from_cache |> must) original_map filename in if Options.debug_at_level_no_module (Options.Other "Dep") then - BU.print2 "Reading the parsing data for %s from its checked file .. found [%s]\n" filename (List.map dep_to_string deps |> String.concat ", "); + BU.print2 "Reading the parsing data for %s from its checked file .. found [%s]\n" filename (show deps); data_from_cache |> must, deps, has_inline_for_extraction, mo_roots end @@ -1233,8 +1238,7 @@ let topological_dependences_of' | White -> if Options.debug_at_level_no_module (Options.Other "Dep") then BU.print2 "Visiting %s: direct deps are %s\n" - filename - (String.concat ", " (List.map dep_to_string dep_node.edges)); + filename (show dep_node.edges); (* Unvisited. Compute. *) deps_add_dep dep_graph filename ({dep_node with color=Gray}); let all_friends, all_files = From b3cdabf26ffc9da3d5cbc3a6a462419bfcff68e3 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Sun, 3 Dec 2023 11:18:50 -0800 Subject: [PATCH 02/29] Tc: Rel: nit, use show --- src/typechecker/FStar.TypeChecker.Rel.fst | 28 ++++++++++------------- 1 file changed, 12 insertions(+), 16 deletions(-) diff --git a/src/typechecker/FStar.TypeChecker.Rel.fst b/src/typechecker/FStar.TypeChecker.Rel.fst index 6c2368ddf28..acaca309ff2 100644 --- a/src/typechecker/FStar.TypeChecker.Rel.fst +++ b/src/typechecker/FStar.TypeChecker.Rel.fst @@ -59,8 +59,6 @@ let is_base_type env typ = | Tm_type _ -> true | _ -> false -let print_ctx_uvar ctx_uvar = Print.ctx_uvar_to_string ctx_uvar - let binders_as_bv_set (bs:binders) = FStar.Compiler.Util.as_set (List.map (fun b -> b.binder_bv) bs) Syntax.order_bv @@ -329,7 +327,7 @@ let term_to_string t = match head.n with | Tm_uvar (u, s) -> BU.format3 "%s%s %s" - (Print.ctx_uvar_to_string u) + (show u) (match fst s with | [] -> "" | s -> BU.format1 "@<%s>" (Print.subst_to_string (List.hd s))) (Print.args_to_string args) | _ -> show t @@ -577,7 +575,7 @@ let set_uvar env u (should_check_opt:option S.should_check_uvar) t = // if Env.debug env <| Options.Other "Rel" // then ( // BU.print2 "Setting uvar %s to %s\n" - // (Print.ctx_uvar_to_string u) + // (show u) // (show t); // match Unionfind.find u.ctx_uvar_head with // | None -> () @@ -800,7 +798,7 @@ let flex_uvar_has_meta_tac u = | _ -> false let flex_t_to_string (Flex (_, c, args)) = - BU.format2 "%s [%s]" (print_ctx_uvar c) (Print.args_to_string args) + BU.format2 "%s [%s]" (show c) (Print.args_to_string args) let is_flex t = let head, _args = U.head_and_args t in @@ -901,7 +899,7 @@ let ensure_no_uvar_subst env (t0:term) (wl:worklist) let sol = S.mk_Tm_app t_v args_sol t0.pos in if Env.debug env <| Options.Other "Rel" then BU.print2 "ensure_no_uvar_subst solving %s with %s\n" - (Print.ctx_uvar_to_string uv) + (show uv) (show sol); set_uvar env uv (Some Already_checked) sol; @@ -994,7 +992,7 @@ let solve_prob' resolve_ok prob logical_guard uvis wl = if debug wl <| Options.Other "Rel" then BU.print3 "Solving %s (%s) with formula %s\n" (string_of_int (p_pid prob)) - (print_ctx_uvar uv) + (show uv) (show phi); let phi = U.abs xs phi (Some (U.residual_tot U.ktype0)) in def_check_scoped (p_loc prob) ("solve_prob'.sol." ^ string_of_int (p_pid prob)) @@ -1004,7 +1002,7 @@ let solve_prob' resolve_ok prob logical_guard uvis wl = let uv = p_guard_uvar prob in let fail () = failwith (BU.format2 "Impossible: this instance %s has already been assigned a solution\n%s\n" - (Print.ctx_uvar_to_string uv) + (show uv) (show (p_guard prob))) in let args_as_binders args = @@ -1843,8 +1841,8 @@ let run_meta_arg_tac (ctx_u:ctx_uvar) : term = match ctx_u.ctx_uvar_meta with | Some (Ctx_uvar_meta_tac (env_dyn, tau)) -> let env : Env.env = FStar.Compiler.Dyn.undyn env_dyn in - if Env.debug env (Options.Other "Tac") - then BU.print1 "Running tactic for meta-arg %s\n" (Print.ctx_uvar_to_string ctx_u); + if Env.debug env (Options.Other "Tac") then + BU.print1 "Running tactic for meta-arg %s\n" (show ctx_u); Errors.with_ctx "Running tactic for meta-arg" (fun () -> env.synth_hook env (U.ctx_uvar_typ ctx_u) tau) | _ -> @@ -2627,7 +2625,7 @@ and imitate_arrow (orig:prob) (wl:worklist) | ({binder_bv=x;binder_qual=imp;binder_positivity=pqual;binder_attrs=attrs})::formals -> let _ctx_u_x, u_x, wl = copy_uvar u_lhs (bs_lhs@bs) (U.type_u() |> fst) wl in - //printfn "Generated formal %s where %s" (show t_y) (Print.ctx_uvar_to_string ctx_u_x); + //printfn "Generated formal %s where %s" (show t_y) (show ctx_u_x); let y = S.new_bv (Some (S.range_of_bv x)) u_x in let b = S.mk_binder_with_attrs y imp pqual attrs in aux (bs@[b]) (bs_terms@[U.arg_of_non_null_binder b]) formals wl @@ -3252,10 +3250,8 @@ and solve_t_flex_flex env orig wl (lhs:flex_t) (rhs:flex_t) : solution = let run_meta_arg_tac_and_try_again (flex:flex_t) = let uv = flex_uvar flex in let t = run_meta_arg_tac uv in - if debug wl <| Options.Other "Rel" - then BU.print2 "solve_t_flex_flex: solving meta arg uvar %s with %s\n" - (Print.ctx_uvar_to_string uv) - (show t); + if debug wl <| Options.Other "Rel" then + BU.print2 "solve_t_flex_flex: solving meta arg uvar %s with %s\n" (show uv) (show t); set_uvar env uv None t; solve (attempt [orig] wl) in @@ -5327,7 +5323,7 @@ let check_implicit_solution_and_discharge_guard env | Inr print_err -> raise_error (Errors.Fatal_FailToResolveImplicitArgument, BU.format5 "Core checking failed for implicit %s (is_tac: %s) (reason: %s) (%s <: %s)" - (Print.ctx_uvar_to_string imp_uvar) + (show imp_uvar) (string_of_bool is_tac) imp_reason (show imp_tm) From 4b2016e3b75c7dae8709c583531dc35c43bd5e96 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Sun, 3 Dec 2023 11:19:26 -0800 Subject: [PATCH 03/29] Tc: Rel: trying to delay meta-args that have uvars in their type or env --- src/typechecker/FStar.TypeChecker.Rel.fst | 94 +++++++++++++++-------- 1 file changed, 64 insertions(+), 30 deletions(-) diff --git a/src/typechecker/FStar.TypeChecker.Rel.fst b/src/typechecker/FStar.TypeChecker.Rel.fst index acaca309ff2..6794b1516bc 100644 --- a/src/typechecker/FStar.TypeChecker.Rel.fst +++ b/src/typechecker/FStar.TypeChecker.Rel.fst @@ -797,6 +797,10 @@ let flex_uvar_has_meta_tac u = | Some (Ctx_uvar_meta_tac _) -> true | _ -> false +let flex_uvar_meta_tac_env u : env_t = + match u.ctx_uvar_meta with + | Some (Ctx_uvar_meta_tac (denv, _)) -> Dyn.undyn denv + let flex_t_to_string (Flex (_, c, args)) = BU.format2 "%s [%s]" (show c) (Print.args_to_string args) @@ -2105,6 +2109,11 @@ let lazy_complete_repr (k:lazy_kind) : bool = | Lazy_universe -> true | _ -> false +let has_free_uvars (t:term) : bool = + not (BU.set_is_empty (Free.uvars_uncached t)) +let env_has_free_uvars (e:env_t) : bool = + List.existsb (fun b -> has_free_uvars b.binder_bv.sort) (Env.all_binders e) + (******************************************************************************************************) (* Main solving algorithm begins here *) (******************************************************************************************************) @@ -3245,7 +3254,9 @@ and solve_t_flex_flex env orig wl (lhs:flex_t) (rhs:flex_t) : solution = let should_run_meta_arg_tac (flex:flex_t) = let uv = flex_uvar flex in flex_uvar_has_meta_tac uv && - BU.set_is_empty (Free.uvars (U.ctx_uvar_typ uv)) in + not (has_free_uvars (U.ctx_uvar_typ uv)) && + not (env_has_free_uvars (flex_uvar_meta_tac_env uv)) + in let run_meta_arg_tac_and_try_again (flex:flex_t) = let uv = flex_uvar flex in @@ -5431,20 +5442,35 @@ let resolve_implicits' env is_tac is_gen (implicits:Env.implicits) in (* / cache *) - let rec until_fixpoint (acc:tagged_implicits * bool) + let rec until_fixpoint (acc : tagged_implicits & (*changed:*)bool & (*defer_open_metas:*)bool ) (implicits:Env.implicits) : tagged_implicits = - let out, changed = acc in + let out, changed, defer_open_metas = acc in + (* changed: we made some progress + defer_open_metas: starts at true, it means to not try to run + meta arg tactics in environments/types that have unresolved + uvars. We first do a pass with this set to true, and if nothing + changed, we then give up and set it to false, trying to eagerly + solve some partially-unresolved constraints. This is definitely + not ideal, maybe the right thing to do is to never run metas + in open contexts, but that is raising many regressions rihgt now, + particularly in Steel (which uses the resolve_implicits hook pervasively). *) match implicits with | [] -> - if not changed - then //Nothing changed in this iteration of the loop + if changed then ( + (* We made some progress, keep going from the start *) + until_fixpoint ([], false, true) (List.map fst out) + ) else if defer_open_metas then ( + (* No progress... but we could try being more eager with metas. *) + until_fixpoint ([], false, false) (List.map fst out) + ) else ( + //Nothing changed in this iteration of the loop //We will try to make progress by either solving a single valued implicit, // or solving an implicit that generates univ constraint, with force flag on let imps, changed = try_solve_single_valued_implicits env is_tac (List.map fst out) in - if changed then until_fixpoint ([], false) imps + if changed then until_fixpoint ([], false, true) imps else let imp_opt, rest = pick_a_univ_deffered_implicit out in (match imp_opt with | None -> rest //No such implicit exists, return remaining implicits @@ -5456,8 +5482,8 @@ let resolve_implicits' env is_tac is_gen (implicits:Env.implicits) imp is_tac force_univ_constraints |> must in - until_fixpoint ([], false) (imps@List.map fst rest)) - else until_fixpoint ([], false) (List.map fst out) + until_fixpoint ([], false, true) (imps@List.map fst rest)) + ) | hd::tl -> let { imp_reason = reason; imp_tm = tm; imp_uvar = ctx_u; imp_range = r } = hd in @@ -5467,39 +5493,47 @@ let resolve_implicits' env is_tac is_gen (implicits:Env.implicits) (show tm) (show ctx_u) (show is_tac); begin match () with | _ when Allow_unresolved? uvar_decoration_should_check -> - until_fixpoint (out, true) tl + until_fixpoint (out, true, defer_open_metas) tl | _ when unresolved ctx_u && flex_uvar_has_meta_tac ctx_u -> let Some (Ctx_uvar_meta_tac meta) = ctx_u.ctx_uvar_meta in let m_env : env_t = Dyn.undyn (fst meta) in let tac = snd meta in let typ = U.ctx_uvar_typ ctx_u in - let solve_with (t:term) = - let extra = - match teq_nosmt env t tm with - | None -> failwith "resolve_implicits: unifying with an unresolved uvar failed?" - | Some g -> g.implicits + if defer_open_metas && (has_free_uvars typ || env_has_free_uvars m_env) then ( + (* If the result type for this meta arg has a free uvar, delay it. + Some other meta arg being solved may instantiate the uvar. See #3130. *) + if Env.debug env <| Options.Other "Rel" then + BU.print1 "Deferring implicit due to open ctx/typ %s\n" (show ctx_u); + until_fixpoint ((hd, Implicit_unresolved)::out, changed, defer_open_metas) tl + ) else ( + let solve_with (t:term) = + let extra = + match teq_nosmt env t tm with + | None -> failwith "resolve_implicits: unifying with an unresolved uvar failed?" + | Some g -> g.implicits + in + until_fixpoint (out, true, defer_open_metas) (extra @ tl) in - until_fixpoint (out, true) (extra @ tl) - in - if cacheable tac then - match meta_arg_cache_lookup tac m_env typ with - | Some res -> solve_with res - | None -> + if cacheable tac then + match meta_arg_cache_lookup tac m_env typ with + | Some res -> solve_with res + | None -> + let t = run_meta_arg_tac ctx_u in + meta_arg_cache_result tac m_env typ t; + solve_with t + else let t = run_meta_arg_tac ctx_u in - meta_arg_cache_result tac m_env typ t; solve_with t - else - let t = run_meta_arg_tac ctx_u in - solve_with t + ) | _ when unresolved ctx_u -> - until_fixpoint ((hd, Implicit_unresolved)::out, changed) tl + until_fixpoint ((hd, Implicit_unresolved)::out, changed, defer_open_metas) tl | _ when Allow_untyped? uvar_decoration_should_check || Already_checked? uvar_decoration_should_check || is_gen -> - until_fixpoint (out, true) tl + until_fixpoint (out, true, defer_open_metas) tl | _ -> let env = {env with gamma=ctx_u.ctx_uvar_gamma} in (* @@ -5522,7 +5556,7 @@ let resolve_implicits' env is_tac is_gen (implicits:Env.implicits) then failwith "Impossible: check_implicit_solution_and_discharge_guard for tac must return Some []" else () else (); - until_fixpoint (out, true) tl + until_fixpoint (out, true, defer_open_metas) tl end else begin @@ -5536,14 +5570,14 @@ let resolve_implicits' env is_tac is_gen (implicits:Env.implicits) match imps_opt with | None -> - until_fixpoint ((hd, Implicit_checking_defers_univ_constraint)::out, changed) tl //Move hd to out + until_fixpoint ((hd, Implicit_checking_defers_univ_constraint)::out, changed, defer_open_metas) tl //Move hd to out | Some imps -> //add imps to out - until_fixpoint ((imps |> List.map (fun i -> i, Implicit_unresolved))@out, true) tl + until_fixpoint ((imps |> List.map (fun i -> i, Implicit_unresolved))@out, true, defer_open_metas) tl end end in - until_fixpoint ([], false) implicits + until_fixpoint ([], false, true) implicits let resolve_implicits env g = if Env.debug env <| Options.Other "ResolveImplicitsHook" From ab61854cf6e683dfc6b9df67fb803ff297ba0871 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Sun, 3 Dec 2023 13:20:21 -0800 Subject: [PATCH 04/29] Tc: setting a better internal reason for typeclass implicits --- src/typechecker/FStar.TypeChecker.TcTerm.fst | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) diff --git a/src/typechecker/FStar.TypeChecker.TcTerm.fst b/src/typechecker/FStar.TypeChecker.TcTerm.fst index 33a052b1ad6..02e400aca0a 100644 --- a/src/typechecker/FStar.TypeChecker.TcTerm.fst +++ b/src/typechecker/FStar.TypeChecker.TcTerm.fst @@ -2765,7 +2765,17 @@ and check_application_args env head (chead:comp) ghead args expected_topt : term (Range.use_range t.pos)) in let varg, _, implicits = - Env.new_implicit_var_aux "Instantiating meta argument in application" r env t Strict (Some ctx_uvar_meta) + let msg = + let is_typeclass = + match ctx_uvar_meta with + | Ctx_uvar_meta_tac (_, tau) -> U.is_fvar Const.tcresolve_lid tau + | _ -> false + in + if is_typeclass + then "Typeclass constraint argument" + else "Instantiating meta argument in application" + in + Env.new_implicit_var_aux msg r env t Strict (Some ctx_uvar_meta) in let subst = NT(x, varg)::subst in let aq = U.aqual_of_binder (List.hd bs) in From 497d581f1004fbb881e3cee1986685136eb9fe06 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Sun, 3 Dec 2023 13:40:10 -0800 Subject: [PATCH 05/29] Tc: Rel: in flex-flex quasi, retain meta-tac from the LHS If we happen to unify the implicits for two typeclass constraints (likely the same one), we need to retain the tag so this has any chance of being solved. This changes makes the unifier retain the meta tag, with a preference for the left one, which is of course totally arbitrary. --- src/typechecker/FStar.TypeChecker.Rel.fst | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/src/typechecker/FStar.TypeChecker.Rel.fst b/src/typechecker/FStar.TypeChecker.Rel.fst index 6794b1516bc..69530a42b1e 100644 --- a/src/typechecker/FStar.TypeChecker.Rel.fst +++ b/src/typechecker/FStar.TypeChecker.Rel.fst @@ -3252,6 +3252,8 @@ and solve_t_flex_rigid_eq (orig:prob) (wl:worklist) (lhs:flex_t) (rhs:term) *) and solve_t_flex_flex env orig wl (lhs:flex_t) (rhs:flex_t) : solution = let should_run_meta_arg_tac (flex:flex_t) = + (* If this flex has a meta-arg, and the problem is fully + defined (no uvars in env/typ), then we can run it now. *) let uv = flex_uvar flex in flex_uvar_has_meta_tac uv && not (has_free_uvars (U.ctx_uvar_typ uv)) && @@ -3342,7 +3344,10 @@ and solve_t_flex_flex env orig wl (lhs:flex_t) (rhs:flex_t) : solution = ^"\trhs=" ^u_rhs.ctx_uvar_reason) wl range gamma_w ctx_w new_uvar_typ new_uvar_should_check - None in + (if Some? u_lhs.ctx_uvar_meta + then u_lhs.ctx_uvar_meta + else u_rhs.ctx_uvar_meta) // Try to retain the meta, if any + in let w_app = S.mk_Tm_app w (List.map (fun ({binder_bv=z}) -> S.as_arg (S.bv_to_name z)) zs) w.pos in let _ = if debug wl <| Options.Other "Rel" From 8e9f09ab4e2dba50b6cd036a1d75094857c76e6f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Sun, 3 Dec 2023 11:21:12 -0800 Subject: [PATCH 06/29] Update tests --- tests/error-messages/Bug2021.fst.expected | 4 +- .../micro-benchmarks/ResolveImplicitsHook.fst | 7 +- tests/typeclasses/Bug3130b.fst | 3 + tests/typeclasses/Bug3130c.fst | 45 +++++ tests/typeclasses/Bug3130d.fst | 155 ++++++++++++++++++ 5 files changed, 210 insertions(+), 4 deletions(-) create mode 100644 tests/typeclasses/Bug3130c.fst create mode 100644 tests/typeclasses/Bug3130d.fst diff --git a/tests/error-messages/Bug2021.fst.expected b/tests/error-messages/Bug2021.fst.expected index 646b413f0a6..9dc9665b440 100644 --- a/tests/error-messages/Bug2021.fst.expected +++ b/tests/error-messages/Bug2021.fst.expected @@ -36,8 +36,8 @@ >>] >> Got issues: [ -* Error 66 at Bug2021.fst(37,13-37,14): - - Failed to resolved implicit argument ?11 +* Error 66 at Bug2021.fst(37,13-37,17): + - Failed to resolved implicit argument ?13 of type Prims.int introduced for Instantiating implicit argument in application - See also Bug2021.fst(36,11-36,12) diff --git a/tests/micro-benchmarks/ResolveImplicitsHook.fst b/tests/micro-benchmarks/ResolveImplicitsHook.fst index 13ac39dc3b0..306466a45b9 100644 --- a/tests/micro-benchmarks/ResolveImplicitsHook.fst +++ b/tests/micro-benchmarks/ResolveImplicitsHook.fst @@ -123,8 +123,11 @@ let resolve_tac_alt () : Tac unit = #push-options "--warn_error @348" //raises 348 for ambiguity in resolve_implicits -// GM 2023-02-01: Used to raise 348 five times, but now it's 15 after some scoping fixes in Tc (why?) -[@@expect_failure [348; 348; 348; 348; 348; 348; 348; 348; 348; 348; 348; 348; 348; 348; 348; 66]] +// GM 2023-02-01: Used to raise 348 five times, but now it's 15 after +// some scoping fixes in Tc (why?) +// GM 2023-12-03: Now 21 times, whatever. It's probably due to slight +// differences in the messages which decrease deduplication. +[@@expect_failure [348; 348; 348; 348; 348; 348; 348; 348; 348; 348; 348; 348; 348; 348; 348; 348; 348; 348; 348; 348; 348; 66]] let test3 (b:bool) : cmd (r1 ** r2 ** r3 ** r4 ** r5) (r1 ** r2 ** r3 ** r4 ** r5) diff --git a/tests/typeclasses/Bug3130b.fst b/tests/typeclasses/Bug3130b.fst index a98c9c7e488..dd0a6493447 100644 --- a/tests/typeclasses/Bug3130b.fst +++ b/tests/typeclasses/Bug3130b.fst @@ -19,5 +19,8 @@ let test5 (y : it 6) = let p : Type0 = y == mk6 in () let test6 () = let p : Type0 = mk5 == mk6 in () let test7 () = let p : Type0 = mk6 == mk5 in () +(* These are ambiguous. They only work since we are running the meta +args in contexts with yet-unresolved uvars, which is somewhat shady to +do. If we forbid that, and these break, it's not too bad. *) let test8 (x:_) = let p : Type0 = mk5 == x /\ x == mk6 in () let test9 (x:_) = let p : Type0 = mk6 == x /\ x == mk5 in () diff --git a/tests/typeclasses/Bug3130c.fst b/tests/typeclasses/Bug3130c.fst new file mode 100644 index 00000000000..363ed916f81 --- /dev/null +++ b/tests/typeclasses/Bug3130c.fst @@ -0,0 +1,45 @@ +module Bug3130c + +open FStar.Tactics.Typeclasses + +class typeclass1 (a:Type0) = { + x: unit; +} + +class typeclass2 (bytes:Type0) {|typeclass1 bytes|} (a:Type) = { + y:unit; +} + +assume val bytes: Type0 +assume val bytes_typeclass1: typeclass1 bytes +instance bytes_typeclass1_ = bytes_typeclass1 +assume val t: Type0 -> Type0 +assume val t_inst: t bytes + +assume val truc: + #bytes:Type0 -> {|typeclass1 bytes|} -> + #a:Type -> {|typeclass2 bytes a|} -> + t bytes -> a -> + Type0 + +noeq +type machin (a:Type) {|typeclass2 bytes a|} = { + pred: a -> prop; + lemma: + content:a -> + Lemma + (ensures truc t_inst content) + ; +} + +let pre (#a:Type) {|d : typeclass2 bytes a|} + (m : machin a) (x : a) + = m.pred x + +val bidule: + #a:Type -> {|typeclass2 bytes a|} -> + m:machin a -> x:a -> + Lemma + (requires m.pred x) + (ensures True) +let bidule #a #tc2 m x = () diff --git a/tests/typeclasses/Bug3130d.fst b/tests/typeclasses/Bug3130d.fst new file mode 100644 index 00000000000..6b348d2d9e7 --- /dev/null +++ b/tests/typeclasses/Bug3130d.fst @@ -0,0 +1,155 @@ +module Bug3130d + +(* Taken from Comparse *) + +open FStar.Mul + +type nat_lbytes (sz:nat) = n:nat{n < normalize_term (pow2 (8*sz))} + +assume +val nat_lbytes_helper: sz:nat -> Lemma (normalize_term (pow2 (8*sz)) == pow2 (8*sz)) +[SMTPat (nat_lbytes sz)] + +/// Minimal interface to manipulate symbolic bytes. +/// Here are the explanations for a few design decisions: +/// - We don't require that only `empty` has length zero, e.g. we may have `concat empty empty <> empty`. +/// - We implement `split` and not `slice`, because `slice` causes trouble in the symbolic case: +/// with `slice`, how do you get the left and right part of `concat empty (concat empty empty)`? +/// - `split` returns an option, hence can fail if the indices are not on the correct bounds. +/// * We require `split` to succeed on the bound of a `concat` (see `split_concat_...`). +/// * This is useful to state the `concat_split` lemma in a way which would be correct on symbolic bytes. +/// - To compensate the first fact, and the fact that we don't require decidable equality, +/// we need a function that recognize the `empty` bytes. +/// - The `to_nat` function can fail, if the bytes are not public for example + +class bytes_like (bytes:Type0) = { + length: bytes -> nat; + + empty: bytes; + empty_length: unit -> Lemma (length empty == 0); + recognize_empty: b:bytes -> res:bool{res <==> b == empty}; + + concat: bytes -> bytes -> bytes; + concat_length: b1:bytes -> b2:bytes -> Lemma (length (concat b1 b2) == (length b1) + (length b2)); + + split: b:bytes -> i:nat -> option (bytes & bytes); + split_length: b:bytes -> i:nat -> Lemma ( + match split b i with + | Some (b1, b2) -> length b1 == i /\ i+length b2 == length b + | None -> True + ); + + split_concat: b1:bytes -> b2:bytes -> Lemma (split (concat b1 b2) (length b1) == Some (b1, b2)); + + concat_split: b:bytes -> i:nat -> Lemma ( + match split b i with + | Some (lhs, rhs) -> concat lhs rhs == b + | _ -> True + ); + + to_nat: b:bytes -> option (nat_lbytes (length b)); + from_nat: sz:nat -> nat_lbytes sz -> b:bytes{length b == sz}; + + from_to_nat: sz:nat -> n:nat_lbytes sz -> Lemma + (to_nat (from_nat sz n) == Some n); + + to_from_nat: b:bytes -> Lemma ( + match to_nat b with + | Some n -> b == from_nat (length b) n + | None -> True + ); +} + +/// This type defines a predicate on `bytes` that is compatible with its structure. +/// It is meant to be used for labeling predicates, which are typically compatible with the `bytes` structure. + +let bytes_pre_is_compatible (#bytes:Type0) {|bytes_like bytes|} (pre:bytes -> prop) = + (pre empty) /\ + (forall b1 b2. pre b1 /\ pre b2 ==> pre (concat b1 b2)) /\ + (forall b i. pre b /\ Some? (split b i) ==> pre (fst (Some?.v (split b i))) /\ pre (snd (Some?.v (split b i)))) /\ + (forall sz n. pre (from_nat sz n)) + +let bytes_pre_is_compatible_intro + (#bytes:Type0) {|bytes_like bytes|} (pre:bytes -> prop) + (empty_proof:squash(pre empty)) + (concat_proof:(b1:bytes{pre b1} -> b2:bytes{pre b2} -> Lemma (pre (concat b1 b2)))) + (split_proof:(b:bytes{pre b} -> i:nat{Some? (split #bytes b i)} -> Lemma (pre (fst (Some?.v (split b i))) /\ pre (snd (Some?.v (split b i)))))) + (from_nat_proof:(sz:nat -> n:nat_lbytes sz -> Lemma (pre (from_nat sz n)))) + : squash (bytes_pre_is_compatible pre) + = + FStar.Classical.forall_intro_2 concat_proof; + FStar.Classical.forall_intro_2 split_proof; + FStar.Classical.forall_intro_2 from_nat_proof + +type bytes_compatible_pre (bytes:Type0) {|bytes_like bytes|} = + pre:(bytes -> prop){bytes_pre_is_compatible pre} + +let seq_u8_bytes_like: bytes_like (Seq.seq UInt8.t) = { + length = Seq.length; + + empty = (Seq.empty); + empty_length = (fun () -> ()); + recognize_empty = (fun b -> + assert(Seq.length b = 0 ==> b `Seq.eq` Seq.empty); + Seq.length b = 0 + ); + + concat = (fun b1 b2 -> Seq.append b1 b2); + concat_length = (fun b1 b2 -> ()); + + split = (fun b i -> + if i <= Seq.length b then + Some (Seq.slice b 0 i, Seq.slice b i (Seq.length b)) + else + None + ); + + split_length = (fun b i -> ()); + split_concat = (fun b1 b2 -> + assert(b1 `Seq.eq` (Seq.slice (Seq.append b1 b2) 0 (Seq.length b1))); + assert(b2 `Seq.eq` (Seq.slice (Seq.append b1 b2) (Seq.length b1) (Seq.length (Seq.append b1 b2)))) + ); + concat_split = (fun b i -> + if i <= Seq.length b then + assert(b `Seq.eq` Seq.append (Seq.slice b 0 i) (Seq.slice b i (Seq.length b))) + else () + ); + + to_nat = (fun b -> + FStar.Endianness.lemma_be_to_n_is_bounded b; + Some (FStar.Endianness.be_to_n b) + ); + from_nat = (fun sz n -> + FStar.Endianness.n_to_be sz n + ); + + from_to_nat = (fun sz n -> ()); + to_from_nat = (fun b -> ()); +} + +let refine_bytes_like (bytes:Type0) {|bytes_like bytes|} (pre:bytes_compatible_pre bytes): bytes_like (b:bytes{pre b}) = { + length = (fun (b:bytes{pre b}) -> length #bytes b); + + empty = empty #bytes; + empty_length = (fun () -> empty_length #bytes ()); + recognize_empty = (fun b -> recognize_empty #bytes b); + + concat = (fun b1 b2 -> concat #bytes b1 b2); + concat_length = (fun b1 b2 -> concat_length #bytes b1 b2); + + split = (fun b i -> + match split #bytes b i with + | None -> None + | Some (b1, b2) -> Some (b1, b2) + ); + split_length = (fun b i -> split_length #bytes b i); + + split_concat = (fun b1 b2 -> split_concat #bytes b1 b2); + concat_split = (fun b i -> concat_split #bytes b i); + + to_nat = (fun b -> to_nat #bytes b); + from_nat = (fun sz n -> from_nat #bytes sz n); + + from_to_nat = (fun sz n -> from_to_nat #bytes sz n); + to_from_nat = (fun b -> to_from_nat #bytes b); +} From 5a413821eafbb3f6cf86cf1f3c6beea2e3a137ee Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Sun, 3 Dec 2023 11:21:55 -0800 Subject: [PATCH 07/29] snap --- .../fstar-lib/generated/FStar_CheckedFiles.ml | 19 ++ ocaml/fstar-lib/generated/FStar_Parser_Dep.ml | 14 +- .../generated/FStar_TypeChecker_Rel.ml | 261 ++++++++++++------ .../generated/FStar_TypeChecker_TcTerm.ml | 17 +- 4 files changed, 212 insertions(+), 99 deletions(-) diff --git a/ocaml/fstar-lib/generated/FStar_CheckedFiles.ml b/ocaml/fstar-lib/generated/FStar_CheckedFiles.ml index b24d71acced..4d87cae8af6 100644 --- a/ocaml/fstar-lib/generated/FStar_CheckedFiles.ml +++ b/ocaml/fstar-lib/generated/FStar_CheckedFiles.ml @@ -81,6 +81,25 @@ let (uu___is_Valid : tc_result_t -> Prims.bool) = fun projectee -> match projectee with | Valid _0 -> true | uu___ -> false let (__proj__Valid__item___0 : tc_result_t -> Prims.string) = fun projectee -> match projectee with | Valid _0 -> _0 +let (uu___46 : tc_result_t FStar_Class_Show.showable) = + { + FStar_Class_Show.show = + (fun uu___ -> + match uu___ with + | Unknown -> "Unknown" + | Invalid s -> + let uu___1 = + FStar_Class_Show.show + (FStar_Class_Show.printableshow + FStar_Class_Printable.printable_string) s in + Prims.op_Hat "Invalid " uu___1 + | Valid s -> + let uu___1 = + FStar_Class_Show.show + (FStar_Class_Show.printableshow + FStar_Class_Printable.printable_string) s in + Prims.op_Hat "Valid " uu___1) + } type cache_t = (tc_result_t * (Prims.string, FStar_Parser_Dep.parsing_data) FStar_Pervasives.either) diff --git a/ocaml/fstar-lib/generated/FStar_Parser_Dep.ml b/ocaml/fstar-lib/generated/FStar_Parser_Dep.ml index f2d23378336..998c92b0751 100644 --- a/ocaml/fstar-lib/generated/FStar_Parser_Dep.ml +++ b/ocaml/fstar-lib/generated/FStar_Parser_Dep.ml @@ -191,6 +191,8 @@ let (dep_to_string : dependence -> Prims.string) = | PreferInterface f -> Prims.op_Hat "PreferInterface " f | UseImplementation f -> Prims.op_Hat "UseImplementation " f | FriendImplementation f -> Prims.op_Hat "FriendImplementation " f +let (showable_dependence : dependence FStar_Class_Show.showable) = + { FStar_Class_Show.show = dep_to_string } type dependences = dependence Prims.list let empty_dependences : 'uuuuu . unit -> 'uuuuu Prims.list = fun uu___ -> [] type dep_node = { @@ -1216,9 +1218,8 @@ let (collect_one : if uu___3 then let uu___4 = - let uu___5 = FStar_Compiler_List.map dep_to_string deps1 in - FStar_Compiler_Effect.op_Bar_Greater uu___5 - (FStar_Compiler_String.concat ", ") in + FStar_Class_Show.show + (FStar_Class_Show.show_list showable_dependence) deps1 in FStar_Compiler_Util.print2 "Reading the parsing data for %s from its checked file .. found [%s]\n" filename uu___4 @@ -1921,10 +1922,9 @@ let (topological_dependences_of' : if uu___2 then let uu___3 = - let uu___4 = - FStar_Compiler_List.map dep_to_string - dep_node1.edges in - FStar_Compiler_String.concat ", " uu___4 in + FStar_Class_Show.show + (FStar_Class_Show.show_list + showable_dependence) dep_node1.edges in FStar_Compiler_Util.print2 "Visiting %s: direct deps are %s\n" filename uu___3 diff --git a/ocaml/fstar-lib/generated/FStar_TypeChecker_Rel.ml b/ocaml/fstar-lib/generated/FStar_TypeChecker_Rel.ml index a1078249aef..b3fad8d8d57 100644 --- a/ocaml/fstar-lib/generated/FStar_TypeChecker_Rel.ml +++ b/ocaml/fstar-lib/generated/FStar_TypeChecker_Rel.ml @@ -65,8 +65,6 @@ let (is_base_type : | FStar_Syntax_Syntax.Tm_fvar uu___2 -> true | FStar_Syntax_Syntax.Tm_type uu___2 -> true | uu___2 -> false) -let (print_ctx_uvar : FStar_Syntax_Syntax.ctx_uvar -> Prims.string) = - fun ctx_uvar -> FStar_Syntax_Print.ctx_uvar_to_string ctx_uvar let (binders_as_bv_set : FStar_Syntax_Syntax.binders -> FStar_Syntax_Syntax.bv FStar_Compiler_Util.set) @@ -868,7 +866,8 @@ let (term_to_string : FStar_Syntax_Syntax.term -> Prims.string) = | (head, args) -> (match head.FStar_Syntax_Syntax.n with | FStar_Syntax_Syntax.Tm_uvar (u, s) -> - let uu___1 = FStar_Syntax_Print.ctx_uvar_to_string u in + let uu___1 = + FStar_Class_Show.show FStar_Syntax_Print.showable_ctxu u in let uu___2 = match FStar_Pervasives_Native.fst s with | [] -> "" @@ -1936,11 +1935,17 @@ let (flex_uvar_has_meta_tac : FStar_Syntax_Syntax.ctx_uvar -> Prims.bool) = | FStar_Pervasives_Native.Some (FStar_Syntax_Syntax.Ctx_uvar_meta_tac uu___) -> true | uu___ -> false +let (flex_uvar_meta_tac_env : + FStar_Syntax_Syntax.ctx_uvar -> FStar_TypeChecker_Env.env_t) = + fun u -> + match u.FStar_Syntax_Syntax.ctx_uvar_meta with + | FStar_Pervasives_Native.Some (FStar_Syntax_Syntax.Ctx_uvar_meta_tac + (denv, uu___)) -> FStar_Compiler_Dyn.undyn denv let (flex_t_to_string : flex_t -> Prims.string) = fun uu___ -> match uu___ with | Flex (uu___1, c, args) -> - let uu___2 = print_ctx_uvar c in + let uu___2 = FStar_Class_Show.show FStar_Syntax_Print.showable_ctxu c in let uu___3 = FStar_Syntax_Print.args_to_string args in FStar_Compiler_Util.format2 "%s [%s]" uu___2 uu___3 let (is_flex : FStar_Syntax_Syntax.term -> Prims.bool) = @@ -2046,8 +2051,8 @@ let (ensure_no_uvar_subst : if uu___6 then let uu___7 = - FStar_Syntax_Print.ctx_uvar_to_string - uv in + FStar_Class_Show.show + FStar_Syntax_Print.showable_ctxu uv in let uu___8 = FStar_Class_Show.show FStar_Syntax_Print.showable_term sol in @@ -2221,7 +2226,8 @@ let (solve_prob' : if uu___2 then let uu___3 = FStar_Compiler_Util.string_of_int (p_pid prob) in - let uu___4 = print_ctx_uvar uv in + let uu___4 = + FStar_Class_Show.show FStar_Syntax_Print.showable_ctxu uv in let uu___5 = FStar_Class_Show.show FStar_Syntax_Print.showable_term phi1 in @@ -2251,7 +2257,8 @@ let (solve_prob' : let uv = p_guard_uvar prob in let fail uu___1 = let uu___2 = - let uu___3 = FStar_Syntax_Print.ctx_uvar_to_string uv in + let uu___3 = + FStar_Class_Show.show FStar_Syntax_Print.showable_ctxu uv in let uu___4 = FStar_Class_Show.show FStar_Syntax_Print.showable_term (p_guard prob) in @@ -4182,7 +4189,8 @@ let (run_meta_arg_tac : FStar_TypeChecker_Env.debug env (FStar_Options.Other "Tac") in if uu___1 then - let uu___2 = FStar_Syntax_Print.ctx_uvar_to_string ctx_u in + let uu___2 = + FStar_Class_Show.show FStar_Syntax_Print.showable_ctxu ctx_u in FStar_Compiler_Util.print1 "Running tactic for meta-arg %s\n" uu___2 else ()); @@ -4850,6 +4858,19 @@ let (lazy_complete_repr : FStar_Syntax_Syntax.lazy_kind -> Prims.bool) = | FStar_Syntax_Syntax.Lazy_sigelt -> true | FStar_Syntax_Syntax.Lazy_universe -> true | uu___ -> false +let (has_free_uvars : FStar_Syntax_Syntax.term -> Prims.bool) = + fun t -> + let uu___ = + let uu___1 = FStar_Syntax_Free.uvars_uncached t in + FStar_Compiler_Util.set_is_empty uu___1 in + Prims.op_Negation uu___ +let (env_has_free_uvars : FStar_TypeChecker_Env.env_t -> Prims.bool) = + fun e -> + let uu___ = FStar_TypeChecker_Env.all_binders e in + FStar_Compiler_List.existsb + (fun b -> + has_free_uvars + (b.FStar_Syntax_Syntax.binder_bv).FStar_Syntax_Syntax.sort) uu___ let rec (solve : worklist -> solution) = fun probs -> (let uu___1 = @@ -7501,11 +7522,16 @@ and (solve_t_flex_flex : fun rhs -> let should_run_meta_arg_tac flex = let uv = flex_uvar flex in - (flex_uvar_has_meta_tac uv) && + ((flex_uvar_has_meta_tac uv) && + (let uu___ = + let uu___1 = FStar_Syntax_Util.ctx_uvar_typ uv in + has_free_uvars uu___1 in + Prims.op_Negation uu___)) + && (let uu___ = - let uu___1 = FStar_Syntax_Util.ctx_uvar_typ uv in - FStar_Syntax_Free.uvars uu___1 in - FStar_Compiler_Util.set_is_empty uu___) in + let uu___1 = flex_uvar_meta_tac_env uv in + env_has_free_uvars uu___1 in + Prims.op_Negation uu___) in let run_meta_arg_tac_and_try_again flex = let uv = flex_uvar flex in let t = run_meta_arg_tac uv in @@ -7514,7 +7540,8 @@ and (solve_t_flex_flex : (FStar_Options.Other "Rel") in if uu___1 then - let uu___2 = FStar_Syntax_Print.ctx_uvar_to_string uv in + let uu___2 = + FStar_Class_Show.show FStar_Syntax_Print.showable_ctxu uv in let uu___3 = FStar_Class_Show.show FStar_Syntax_Print.showable_term t in FStar_Compiler_Util.print2 @@ -7720,7 +7747,13 @@ and (solve_t_flex_flex : ctx_w new_uvar_typ new_uvar_should_check - FStar_Pervasives_Native.None in + (if + FStar_Pervasives_Native.uu___is_Some + u_lhs.FStar_Syntax_Syntax.ctx_uvar_meta + then + u_lhs.FStar_Syntax_Syntax.ctx_uvar_meta + else + u_rhs.FStar_Syntax_Syntax.ctx_uvar_meta) in (match uu___23 with | (uu___24, w, wl1) -> @@ -15080,7 +15113,8 @@ let (check_implicit_solution_and_discharge_guard : let uu___5 = let uu___6 = let uu___7 = - FStar_Syntax_Print.ctx_uvar_to_string + FStar_Class_Show.show + FStar_Syntax_Print.showable_ctxu imp_uvar in let uu___8 = FStar_Compiler_Util.string_of_bool is_tac in @@ -15230,48 +15264,58 @@ let (resolve_implicits' : let rec until_fixpoint acc implicits1 = let uu___ = acc in match uu___ with - | (out, changed) -> + | (out, changed, defer_open_metas) -> (match implicits1 with | [] -> - if Prims.op_Negation changed + if changed then let uu___1 = - let uu___2 = - FStar_Compiler_List.map - FStar_Pervasives_Native.fst out in - try_solve_single_valued_implicits env is_tac uu___2 in - (match uu___1 with - | (imps, changed1) -> - if changed1 - then until_fixpoint ([], false) imps - else - (let uu___3 = pick_a_univ_deffered_implicit out in - match uu___3 with - | (imp_opt, rest) -> - (match imp_opt with - | FStar_Pervasives_Native.None -> rest - | FStar_Pervasives_Native.Some imp -> - let force_univ_constraints = true in - let imps1 = - let uu___4 = - check_implicit_solution_and_discharge_guard - env imp is_tac - force_univ_constraints in - FStar_Compiler_Effect.op_Bar_Greater - uu___4 FStar_Compiler_Util.must in - let uu___4 = - let uu___5 = - FStar_Compiler_List.map - FStar_Pervasives_Native.fst - rest in - FStar_Compiler_List.op_At imps1 - uu___5 in - until_fixpoint ([], false) uu___4))) + FStar_Compiler_List.map FStar_Pervasives_Native.fst + out in + until_fixpoint ([], false, true) uu___1 else - (let uu___2 = - FStar_Compiler_List.map FStar_Pervasives_Native.fst - out in - until_fixpoint ([], false) uu___2) + if defer_open_metas + then + (let uu___2 = + FStar_Compiler_List.map + FStar_Pervasives_Native.fst out in + until_fixpoint ([], false, false) uu___2) + else + (let uu___3 = + let uu___4 = + FStar_Compiler_List.map + FStar_Pervasives_Native.fst out in + try_solve_single_valued_implicits env is_tac + uu___4 in + match uu___3 with + | (imps, changed1) -> + if changed1 + then until_fixpoint ([], false, true) imps + else + (let uu___5 = + pick_a_univ_deffered_implicit out in + match uu___5 with + | (imp_opt, rest) -> + (match imp_opt with + | FStar_Pervasives_Native.None -> rest + | FStar_Pervasives_Native.Some imp -> + let force_univ_constraints = true in + let imps1 = + let uu___6 = + check_implicit_solution_and_discharge_guard + env imp is_tac + force_univ_constraints in + FStar_Compiler_Effect.op_Bar_Greater + uu___6 FStar_Compiler_Util.must in + let uu___6 = + let uu___7 = + FStar_Compiler_List.map + FStar_Pervasives_Native.fst + rest in + FStar_Compiler_List.op_At imps1 + uu___7 in + until_fixpoint ([], false, true) + uu___6))) | hd::tl -> let uu___1 = hd in (match uu___1 with @@ -15316,7 +15360,9 @@ let (resolve_implicits' : | uu___5 when FStar_Syntax_Syntax.uu___is_Allow_unresolved uvar_decoration_should_check - -> until_fixpoint (out, true) tl + -> + until_fixpoint + (out, true, defer_open_metas) tl | uu___5 when (unresolved ctx_u) && (flex_uvar_has_meta_tac ctx_u) @@ -15336,43 +15382,73 @@ let (resolve_implicits' : let typ = FStar_Syntax_Util.ctx_uvar_typ ctx_u in - let solve_with t = - let extra = - let uu___7 = teq_nosmt env t tm in - match uu___7 with - | FStar_Pervasives_Native.None - -> - failwith - "resolve_implicits: unifying with an unresolved uvar failed?" - | FStar_Pervasives_Native.Some - g -> - g.FStar_TypeChecker_Common.implicits in - until_fixpoint (out, true) - (FStar_Compiler_List.op_At - extra tl) in - let uu___7 = cacheable tac in + let uu___7 = + defer_open_metas && + ((has_free_uvars typ) || + (env_has_free_uvars m_env)) in if uu___7 then - let uu___8 = - meta_arg_cache_lookup tac m_env - typ in - (match uu___8 with - | FStar_Pervasives_Native.Some - res -> solve_with res - | FStar_Pervasives_Native.None - -> - let t = - run_meta_arg_tac ctx_u in - (meta_arg_cache_result tac - m_env typ t; - solve_with t)) + ((let uu___9 = + FStar_Compiler_Effect.op_Less_Bar + (FStar_TypeChecker_Env.debug + env) + (FStar_Options.Other "Rel") in + if uu___9 + then + let uu___10 = + FStar_Class_Show.show + FStar_Syntax_Print.showable_ctxu + ctx_u in + FStar_Compiler_Util.print1 + "Deferring implicit due to open ctx/typ %s\n" + uu___10 + else ()); + until_fixpoint + (((hd, Implicit_unresolved) :: + out), changed, + defer_open_metas) tl) else - (let t = run_meta_arg_tac ctx_u in - solve_with t)) + (let solve_with t = + let extra = + let uu___9 = + teq_nosmt env t tm in + match uu___9 with + | FStar_Pervasives_Native.None + -> + failwith + "resolve_implicits: unifying with an unresolved uvar failed?" + | FStar_Pervasives_Native.Some + g -> + g.FStar_TypeChecker_Common.implicits in + until_fixpoint + (out, true, + defer_open_metas) + (FStar_Compiler_List.op_At + extra tl) in + let uu___9 = cacheable tac in + if uu___9 + then + let uu___10 = + meta_arg_cache_lookup tac + m_env typ in + match uu___10 with + | FStar_Pervasives_Native.Some + res -> solve_with res + | FStar_Pervasives_Native.None + -> + let t = + run_meta_arg_tac ctx_u in + (meta_arg_cache_result tac + m_env typ t; + solve_with t) + else + (let t = + run_meta_arg_tac ctx_u in + solve_with t))) | uu___5 when unresolved ctx_u -> until_fixpoint (((hd, Implicit_unresolved) :: out), - changed) tl + changed, defer_open_metas) tl | uu___5 when ((FStar_Syntax_Syntax.uu___is_Allow_untyped uvar_decoration_should_check) @@ -15380,7 +15456,9 @@ let (resolve_implicits' : (FStar_Syntax_Syntax.uu___is_Already_checked uvar_decoration_should_check)) || is_gen - -> until_fixpoint (out, true) tl + -> + until_fixpoint + (out, true, defer_open_metas) tl | uu___5 -> let env1 = { @@ -15543,7 +15621,8 @@ let (resolve_implicits' : "Impossible: check_implicit_solution_and_discharge_guard for tac must return Some []" else ()) else ()); - until_fixpoint (out, true) tl) + until_fixpoint + (out, true, defer_open_metas) tl) else (let force_univ_constraints = false in let imps_opt = @@ -15555,7 +15634,8 @@ let (resolve_implicits' : until_fixpoint (((hd1, Implicit_checking_defers_univ_constraint) - :: out), changed) tl + :: out), changed, + defer_open_metas) tl | FStar_Pervasives_Native.Some imps -> let uu___7 = @@ -15569,9 +15649,10 @@ let (resolve_implicits' : Implicit_unresolved))) in FStar_Compiler_List.op_At uu___9 out in - (uu___8, true) in + (uu___8, true, + defer_open_metas) in until_fixpoint uu___7 tl)))))) in - until_fixpoint ([], false) implicits + until_fixpoint ([], false, true) implicits let (resolve_implicits : FStar_TypeChecker_Env.env -> FStar_TypeChecker_Common.guard_t -> FStar_TypeChecker_Common.guard_t) diff --git a/ocaml/fstar-lib/generated/FStar_TypeChecker_TcTerm.ml b/ocaml/fstar-lib/generated/FStar_TypeChecker_TcTerm.ml index 2ea7ac34e64..4d934dfd042 100644 --- a/ocaml/fstar-lib/generated/FStar_TypeChecker_TcTerm.ml +++ b/ocaml/fstar-lib/generated/FStar_TypeChecker_TcTerm.ml @@ -7554,9 +7554,22 @@ and (check_application_args : FStar_Compiler_Range_Type.range_of_rng uu___11 uu___12 in let uu___7 = + let msg = + let is_typeclass = + match ctx_uvar_meta with + | FStar_Syntax_Syntax.Ctx_uvar_meta_tac + (uu___8, tau) -> + FStar_Syntax_Util.is_fvar + FStar_Parser_Const.tcresolve_lid + tau + | uu___8 -> false in + if is_typeclass + then "Typeclass constraint argument" + else + "Instantiating meta argument in application" in FStar_TypeChecker_Env.new_implicit_var_aux - "Instantiating meta argument in application" - r1 env t1 FStar_Syntax_Syntax.Strict + msg r1 env t1 + FStar_Syntax_Syntax.Strict (FStar_Pervasives_Native.Some ctx_uvar_meta) in (match uu___7 with From f7f5aa5748d0b5a18ba9f10b76a8d4bbd4bfe32a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Sun, 3 Dec 2023 16:23:25 -0800 Subject: [PATCH 08/29] Rel: never run meta-args in unresolved contexts I thought this was needed for backwards-compatibility, but apparently not. The few examples that break are ambiguous, and having this restriction in place seems like the right thing to do and brings some peace of mind. --- src/typechecker/FStar.TypeChecker.Rel.fst | 42 ++++++++--------------- 1 file changed, 15 insertions(+), 27 deletions(-) diff --git a/src/typechecker/FStar.TypeChecker.Rel.fst b/src/typechecker/FStar.TypeChecker.Rel.fst index 69530a42b1e..439c0e026c6 100644 --- a/src/typechecker/FStar.TypeChecker.Rel.fst +++ b/src/typechecker/FStar.TypeChecker.Rel.fst @@ -5447,35 +5447,23 @@ let resolve_implicits' env is_tac is_gen (implicits:Env.implicits) in (* / cache *) - let rec until_fixpoint (acc : tagged_implicits & (*changed:*)bool & (*defer_open_metas:*)bool ) + let rec until_fixpoint (acc : tagged_implicits & (*changed:*)bool) (implicits:Env.implicits) : tagged_implicits = - let out, changed, defer_open_metas = acc in - (* changed: we made some progress - defer_open_metas: starts at true, it means to not try to run - meta arg tactics in environments/types that have unresolved - uvars. We first do a pass with this set to true, and if nothing - changed, we then give up and set it to false, trying to eagerly - solve some partially-unresolved constraints. This is definitely - not ideal, maybe the right thing to do is to never run metas - in open contexts, but that is raising many regressions rihgt now, - particularly in Steel (which uses the resolve_implicits hook pervasively). *) + let out, changed = acc in match implicits with | [] -> if changed then ( (* We made some progress, keep going from the start *) - until_fixpoint ([], false, true) (List.map fst out) - ) else if defer_open_metas then ( - (* No progress... but we could try being more eager with metas. *) - until_fixpoint ([], false, false) (List.map fst out) + until_fixpoint ([], false) (List.map fst out) ) else ( //Nothing changed in this iteration of the loop //We will try to make progress by either solving a single valued implicit, // or solving an implicit that generates univ constraint, with force flag on let imps, changed = try_solve_single_valued_implicits env is_tac (List.map fst out) in - if changed then until_fixpoint ([], false, true) imps + if changed then until_fixpoint ([], false) imps else let imp_opt, rest = pick_a_univ_deffered_implicit out in (match imp_opt with | None -> rest //No such implicit exists, return remaining implicits @@ -5487,7 +5475,7 @@ let resolve_implicits' env is_tac is_gen (implicits:Env.implicits) imp is_tac force_univ_constraints |> must in - until_fixpoint ([], false, true) (imps@List.map fst rest)) + until_fixpoint ([], false) (imps@List.map fst rest)) ) | hd::tl -> @@ -5498,19 +5486,19 @@ let resolve_implicits' env is_tac is_gen (implicits:Env.implicits) (show tm) (show ctx_u) (show is_tac); begin match () with | _ when Allow_unresolved? uvar_decoration_should_check -> - until_fixpoint (out, true, defer_open_metas) tl + until_fixpoint (out, true) tl | _ when unresolved ctx_u && flex_uvar_has_meta_tac ctx_u -> let Some (Ctx_uvar_meta_tac meta) = ctx_u.ctx_uvar_meta in let m_env : env_t = Dyn.undyn (fst meta) in let tac = snd meta in let typ = U.ctx_uvar_typ ctx_u in - if defer_open_metas && (has_free_uvars typ || env_has_free_uvars m_env) then ( + if has_free_uvars typ || env_has_free_uvars m_env then ( (* If the result type for this meta arg has a free uvar, delay it. Some other meta arg being solved may instantiate the uvar. See #3130. *) if Env.debug env <| Options.Other "Rel" then BU.print1 "Deferring implicit due to open ctx/typ %s\n" (show ctx_u); - until_fixpoint ((hd, Implicit_unresolved)::out, changed, defer_open_metas) tl + until_fixpoint ((hd, Implicit_unresolved)::out, changed) tl ) else ( let solve_with (t:term) = let extra = @@ -5518,7 +5506,7 @@ let resolve_implicits' env is_tac is_gen (implicits:Env.implicits) | None -> failwith "resolve_implicits: unifying with an unresolved uvar failed?" | Some g -> g.implicits in - until_fixpoint (out, true, defer_open_metas) (extra @ tl) + until_fixpoint (out, true) (extra @ tl) in if cacheable tac then match meta_arg_cache_lookup tac m_env typ with @@ -5533,12 +5521,12 @@ let resolve_implicits' env is_tac is_gen (implicits:Env.implicits) ) | _ when unresolved ctx_u -> - until_fixpoint ((hd, Implicit_unresolved)::out, changed, defer_open_metas) tl + until_fixpoint ((hd, Implicit_unresolved)::out, changed) tl | _ when Allow_untyped? uvar_decoration_should_check || Already_checked? uvar_decoration_should_check || is_gen -> - until_fixpoint (out, true, defer_open_metas) tl + until_fixpoint (out, true) tl | _ -> let env = {env with gamma=ctx_u.ctx_uvar_gamma} in (* @@ -5561,7 +5549,7 @@ let resolve_implicits' env is_tac is_gen (implicits:Env.implicits) then failwith "Impossible: check_implicit_solution_and_discharge_guard for tac must return Some []" else () else (); - until_fixpoint (out, true, defer_open_metas) tl + until_fixpoint (out, true) tl end else begin @@ -5575,14 +5563,14 @@ let resolve_implicits' env is_tac is_gen (implicits:Env.implicits) match imps_opt with | None -> - until_fixpoint ((hd, Implicit_checking_defers_univ_constraint)::out, changed, defer_open_metas) tl //Move hd to out + until_fixpoint ((hd, Implicit_checking_defers_univ_constraint)::out, changed) tl //Move hd to out | Some imps -> //add imps to out - until_fixpoint ((imps |> List.map (fun i -> i, Implicit_unresolved))@out, true, defer_open_metas) tl + until_fixpoint ((imps |> List.map (fun i -> i, Implicit_unresolved))@out, true) tl end end in - until_fixpoint ([], false, true) implicits + until_fixpoint ([], false) implicits let resolve_implicits env g = if Env.debug env <| Options.Other "ResolveImplicitsHook" From 865e724e9ca1dab859d991e74c992161555860e5 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Sun, 3 Dec 2023 16:27:11 -0800 Subject: [PATCH 09/29] Update tests --- tests/bug-reports/Bug1918.fst | 2 +- tests/error-messages/Bug2021.fst.expected | 4 ++-- tests/micro-benchmarks/ResolveImplicitsHook.fst | 6 ++++++ tests/typeclasses/Bug3130b.fst | 7 ++++--- 4 files changed, 13 insertions(+), 6 deletions(-) diff --git a/tests/bug-reports/Bug1918.fst b/tests/bug-reports/Bug1918.fst index af139a8d20b..e6674259920 100644 --- a/tests/bug-reports/Bug1918.fst +++ b/tests/bug-reports/Bug1918.fst @@ -5,5 +5,5 @@ class mon = { comp : t -> t -> t; } -[@@(expect_failure [228])] +[@@expect_failure [66]] let (++) (a:_) (b:_) = comp a b diff --git a/tests/error-messages/Bug2021.fst.expected b/tests/error-messages/Bug2021.fst.expected index 9dc9665b440..646b413f0a6 100644 --- a/tests/error-messages/Bug2021.fst.expected +++ b/tests/error-messages/Bug2021.fst.expected @@ -36,8 +36,8 @@ >>] >> Got issues: [ -* Error 66 at Bug2021.fst(37,13-37,17): - - Failed to resolved implicit argument ?13 +* Error 66 at Bug2021.fst(37,13-37,14): + - Failed to resolved implicit argument ?11 of type Prims.int introduced for Instantiating implicit argument in application - See also Bug2021.fst(36,11-36,12) diff --git a/tests/micro-benchmarks/ResolveImplicitsHook.fst b/tests/micro-benchmarks/ResolveImplicitsHook.fst index 306466a45b9..bd7c5f57f96 100644 --- a/tests/micro-benchmarks/ResolveImplicitsHook.fst +++ b/tests/micro-benchmarks/ResolveImplicitsHook.fst @@ -104,6 +104,12 @@ val frame3 (f:cmd p q) : cmd pre post +(* +GM 2023-12-03: This example now fails since we don't run meta args +in contexts/types that have uvars in them. But the only thing forcing +the resolution of pre and post is the tactic +*) +[@@expect_failure [66]] let test2 : cmd (r1 ** r2) (r1 ** r2) = diff --git a/tests/typeclasses/Bug3130b.fst b/tests/typeclasses/Bug3130b.fst index dd0a6493447..0eb3f0bc474 100644 --- a/tests/typeclasses/Bug3130b.fst +++ b/tests/typeclasses/Bug3130b.fst @@ -19,8 +19,9 @@ let test5 (y : it 6) = let p : Type0 = y == mk6 in () let test6 () = let p : Type0 = mk5 == mk6 in () let test7 () = let p : Type0 = mk6 == mk5 in () -(* These are ambiguous. They only work since we are running the meta -args in contexts with yet-unresolved uvars, which is somewhat shady to -do. If we forbid that, and these break, it's not too bad. *) +(* These are ambiguous. They used to work when we ran meta args in +contexts with yet-unresolved uvars, but that is now forbidden. *) +[@@expect_failure [66]] let test8 (x:_) = let p : Type0 = mk5 == x /\ x == mk6 in () +[@@expect_failure [66]] let test9 (x:_) = let p : Type0 = mk6 == x /\ x == mk5 in () From 833ec1f17869a9cf8c5f96a9b161cce722ac7538 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Sun, 3 Dec 2023 16:29:28 -0800 Subject: [PATCH 10/29] snap --- .../generated/FStar_TypeChecker_Rel.ml | 105 +++++++----------- 1 file changed, 42 insertions(+), 63 deletions(-) diff --git a/ocaml/fstar-lib/generated/FStar_TypeChecker_Rel.ml b/ocaml/fstar-lib/generated/FStar_TypeChecker_Rel.ml index b3fad8d8d57..8d8e1f1d5a3 100644 --- a/ocaml/fstar-lib/generated/FStar_TypeChecker_Rel.ml +++ b/ocaml/fstar-lib/generated/FStar_TypeChecker_Rel.ml @@ -15264,7 +15264,7 @@ let (resolve_implicits' : let rec until_fixpoint acc implicits1 = let uu___ = acc in match uu___ with - | (out, changed, defer_open_metas) -> + | (out, changed) -> (match implicits1 with | [] -> if changed @@ -15272,50 +15272,40 @@ let (resolve_implicits' : let uu___1 = FStar_Compiler_List.map FStar_Pervasives_Native.fst out in - until_fixpoint ([], false, true) uu___1 + until_fixpoint ([], false) uu___1 else - if defer_open_metas - then - (let uu___2 = + (let uu___2 = + let uu___3 = FStar_Compiler_List.map FStar_Pervasives_Native.fst out in - until_fixpoint ([], false, false) uu___2) - else - (let uu___3 = - let uu___4 = - FStar_Compiler_List.map - FStar_Pervasives_Native.fst out in - try_solve_single_valued_implicits env is_tac - uu___4 in - match uu___3 with - | (imps, changed1) -> - if changed1 - then until_fixpoint ([], false, true) imps - else - (let uu___5 = - pick_a_univ_deffered_implicit out in - match uu___5 with - | (imp_opt, rest) -> - (match imp_opt with - | FStar_Pervasives_Native.None -> rest - | FStar_Pervasives_Native.Some imp -> - let force_univ_constraints = true in - let imps1 = - let uu___6 = - check_implicit_solution_and_discharge_guard - env imp is_tac - force_univ_constraints in - FStar_Compiler_Effect.op_Bar_Greater - uu___6 FStar_Compiler_Util.must in + try_solve_single_valued_implicits env is_tac uu___3 in + match uu___2 with + | (imps, changed1) -> + if changed1 + then until_fixpoint ([], false) imps + else + (let uu___4 = pick_a_univ_deffered_implicit out in + match uu___4 with + | (imp_opt, rest) -> + (match imp_opt with + | FStar_Pervasives_Native.None -> rest + | FStar_Pervasives_Native.Some imp -> + let force_univ_constraints = true in + let imps1 = + let uu___5 = + check_implicit_solution_and_discharge_guard + env imp is_tac + force_univ_constraints in + FStar_Compiler_Effect.op_Bar_Greater + uu___5 FStar_Compiler_Util.must in + let uu___5 = let uu___6 = - let uu___7 = - FStar_Compiler_List.map - FStar_Pervasives_Native.fst - rest in - FStar_Compiler_List.op_At imps1 - uu___7 in - until_fixpoint ([], false, true) - uu___6))) + FStar_Compiler_List.map + FStar_Pervasives_Native.fst + rest in + FStar_Compiler_List.op_At imps1 + uu___6 in + until_fixpoint ([], false) uu___5))) | hd::tl -> let uu___1 = hd in (match uu___1 with @@ -15360,9 +15350,7 @@ let (resolve_implicits' : | uu___5 when FStar_Syntax_Syntax.uu___is_Allow_unresolved uvar_decoration_should_check - -> - until_fixpoint - (out, true, defer_open_metas) tl + -> until_fixpoint (out, true) tl | uu___5 when (unresolved ctx_u) && (flex_uvar_has_meta_tac ctx_u) @@ -15383,9 +15371,8 @@ let (resolve_implicits' : FStar_Syntax_Util.ctx_uvar_typ ctx_u in let uu___7 = - defer_open_metas && - ((has_free_uvars typ) || - (env_has_free_uvars m_env)) in + (has_free_uvars typ) || + (env_has_free_uvars m_env) in if uu___7 then ((let uu___9 = @@ -15405,8 +15392,7 @@ let (resolve_implicits' : else ()); until_fixpoint (((hd, Implicit_unresolved) :: - out), changed, - defer_open_metas) tl) + out), changed) tl) else (let solve_with t = let extra = @@ -15420,9 +15406,7 @@ let (resolve_implicits' : | FStar_Pervasives_Native.Some g -> g.FStar_TypeChecker_Common.implicits in - until_fixpoint - (out, true, - defer_open_metas) + until_fixpoint (out, true) (FStar_Compiler_List.op_At extra tl) in let uu___9 = cacheable tac in @@ -15448,7 +15432,7 @@ let (resolve_implicits' : | uu___5 when unresolved ctx_u -> until_fixpoint (((hd, Implicit_unresolved) :: out), - changed, defer_open_metas) tl + changed) tl | uu___5 when ((FStar_Syntax_Syntax.uu___is_Allow_untyped uvar_decoration_should_check) @@ -15456,9 +15440,7 @@ let (resolve_implicits' : (FStar_Syntax_Syntax.uu___is_Already_checked uvar_decoration_should_check)) || is_gen - -> - until_fixpoint - (out, true, defer_open_metas) tl + -> until_fixpoint (out, true) tl | uu___5 -> let env1 = { @@ -15621,8 +15603,7 @@ let (resolve_implicits' : "Impossible: check_implicit_solution_and_discharge_guard for tac must return Some []" else ()) else ()); - until_fixpoint - (out, true, defer_open_metas) tl) + until_fixpoint (out, true) tl) else (let force_univ_constraints = false in let imps_opt = @@ -15634,8 +15615,7 @@ let (resolve_implicits' : until_fixpoint (((hd1, Implicit_checking_defers_univ_constraint) - :: out), changed, - defer_open_metas) tl + :: out), changed) tl | FStar_Pervasives_Native.Some imps -> let uu___7 = @@ -15649,10 +15629,9 @@ let (resolve_implicits' : Implicit_unresolved))) in FStar_Compiler_List.op_At uu___9 out in - (uu___8, true, - defer_open_metas) in + (uu___8, true) in until_fixpoint uu___7 tl)))))) in - until_fixpoint ([], false, true) implicits + until_fixpoint ([], false) implicits let (resolve_implicits : FStar_TypeChecker_Env.env -> FStar_TypeChecker_Common.guard_t -> FStar_TypeChecker_Common.guard_t) From 82c0c9abf42361855af8c659b423f6c6937cb683 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Mon, 4 Dec 2023 14:02:44 -0800 Subject: [PATCH 11/29] Class.Show: add instance for sets --- src/class/FStar.Class.Show.fst | 4 ++++ src/class/FStar.Class.Show.fsti | 2 ++ 2 files changed, 6 insertions(+) diff --git a/src/class/FStar.Class.Show.fst b/src/class/FStar.Class.Show.fst index 51670f11ea3..f42c1cf94a7 100644 --- a/src/class/FStar.Class.Show.fst +++ b/src/class/FStar.Class.Show.fst @@ -11,6 +11,10 @@ instance show_list (a:Type) (_ : showable a) : Tot (showable (list a)) = { show = FStar.Common.string_of_list show; } +instance show_set (a:Type) (_ : showable a) : Tot (showable (BU.set a)) = { + show = FStar.Common.string_of_set show; +} + instance show_option (a:Type) (_ : showable a) : Tot (showable (option a)) = { show = FStar.Common.string_of_option show; } diff --git a/src/class/FStar.Class.Show.fsti b/src/class/FStar.Class.Show.fsti index 9dc08feeb4f..79ab3a6d196 100644 --- a/src/class/FStar.Class.Show.fsti +++ b/src/class/FStar.Class.Show.fsti @@ -2,6 +2,7 @@ module FStar.Class.Show open FStar.Compiler.Effect open FStar.Class.Printable +module BU = FStar.Compiler.Util class showable (a:Type) = { show : a -> ML string; @@ -12,6 +13,7 @@ ML effect of the `printer. *) instance val printableshow (_ : printable 'a) : Tot (showable 'a) instance val show_list (a:Type) (_ : showable a) : Tot (showable (list a)) +instance val show_set (a:Type) (_ : showable a) : Tot (showable (BU.set a)) instance val show_option (a:Type) (_ : showable a) : Tot (showable (option a)) From ce43a2de33a216e6911753748a2b5963f1d32090 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Mon, 4 Dec 2023 14:03:08 -0800 Subject: [PATCH 12/29] Tc: another improved reason message for constraints --- src/typechecker/FStar.TypeChecker.Util.fst | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) diff --git a/src/typechecker/FStar.TypeChecker.Util.fst b/src/typechecker/FStar.TypeChecker.Util.fst index 36992f44906..21d5fae227e 100644 --- a/src/typechecker/FStar.TypeChecker.Util.fst +++ b/src/typechecker/FStar.TypeChecker.Util.fst @@ -2889,7 +2889,17 @@ let maybe_instantiate (env:Env.env) e t = Ctx_uvar_meta_attr attr | _ -> failwith "Impossible, match is under a guard, did not expect this case" in - let v, _, g = Env.new_implicit_var_aux "Instantiation of meta argument" + let msg = + let is_typeclass = + match meta_t with + | Ctx_uvar_meta_tac (_, tau) -> U.is_fvar C.tcresolve_lid tau + | _ -> false + in + if is_typeclass + then "Typeclass constraint argument" + else "Instantiation of meta argument" + in + let v, _, g = Env.new_implicit_var_aux msg e.pos env t Strict (Some meta_t) in if Env.debug env Options.High then From 0baba39fef574d5348f99bf753e6633df435d937 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Mon, 4 Dec 2023 09:41:25 -0800 Subject: [PATCH 13/29] Add a test cf. #3130 --- tests/typeclasses/Bug3130e.fst | 26 ++++++++++++++++++++++++++ 1 file changed, 26 insertions(+) create mode 100644 tests/typeclasses/Bug3130e.fst diff --git a/tests/typeclasses/Bug3130e.fst b/tests/typeclasses/Bug3130e.fst new file mode 100644 index 00000000000..a8524458cd0 --- /dev/null +++ b/tests/typeclasses/Bug3130e.fst @@ -0,0 +1,26 @@ +module Bug3130e + +class ord_leq (a:eqtype) = + { leq: a -> a -> bool + ; trans: (x:a) -> (y:a) -> (z:a) -> Lemma (x `leq` y /\ y `leq` z ==> x `leq` z) + } + +let transitivity {| ord_leq 'a |} (x y z : 'a) + : Lemma (x `leq` y /\ y `leq` z ==> x `leq` z) + [SMTPat (x `leq` y); SMTPat (x `leq` z)] + = trans x y z + +(* Currently fails since the type of the uu binder is undefined, +and tcresolve won't run *) +[@@expect_failure [66]] +let transitivity_forall #a {| ord_leq a |} uu + : Lemma (forall (x y z : a). x `leq` y /\ y `leq` z ==> x `leq` z ) += () + +let transitivity_forall2 #a {| ord_leq a |} + : Lemma (forall (x y z : a). x `leq` y /\ y `leq` z ==> x `leq` z ) += () + +let transitivity_forall3 #a #b {| ord_leq a |} (unit:b) + : Lemma (forall (x y z : a). x `leq` y /\ y `leq` z ==> x `leq` z ) += () From 866e3c0e4c2a98681adeaafe7d1b0efb04b8307c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Mon, 4 Dec 2023 14:00:40 -0800 Subject: [PATCH 14/29] Tc: do not force trivial guard when checking attributes Trying to force it would make typeclass instantiation run now, when there are possibly yet-unresolved variables in the environment, which would prevent the tactic from running. See the Bug3130f example. This patch makes the typechecker just accumulate the guard, and force it at the end, where the free uvars restriction will cause the constraints to be solved in order. --- src/typechecker/FStar.TypeChecker.Rel.fst | 2 +- src/typechecker/FStar.TypeChecker.Tc.fst | 5 ++++- src/typechecker/FStar.TypeChecker.TcTerm.fst | 12 +++++++--- src/typechecker/FStar.TypeChecker.TcTerm.fsti | 2 +- tests/typeclasses/Bug3130f.fst | 22 +++++++++++++++++++ 5 files changed, 37 insertions(+), 6 deletions(-) create mode 100644 tests/typeclasses/Bug3130f.fst diff --git a/src/typechecker/FStar.TypeChecker.Rel.fst b/src/typechecker/FStar.TypeChecker.Rel.fst index 439c0e026c6..e8eaa929c74 100644 --- a/src/typechecker/FStar.TypeChecker.Rel.fst +++ b/src/typechecker/FStar.TypeChecker.Rel.fst @@ -5494,7 +5494,7 @@ let resolve_implicits' env is_tac is_gen (implicits:Env.implicits) let tac = snd meta in let typ = U.ctx_uvar_typ ctx_u in if has_free_uvars typ || env_has_free_uvars m_env then ( - (* If the result type for this meta arg has a free uvar, delay it. + (* If the result type or env for this meta arg has a free uvar, delay it. Some other meta arg being solved may instantiate the uvar. See #3130. *) if Env.debug env <| Options.Other "Rel" then BU.print1 "Deferring implicit due to open ctx/typ %s\n" (show ctx_u); diff --git a/src/typechecker/FStar.TypeChecker.Tc.fst b/src/typechecker/FStar.TypeChecker.Tc.fst index 17593146b2d..f66878289d5 100644 --- a/src/typechecker/FStar.TypeChecker.Tc.fst +++ b/src/typechecker/FStar.TypeChecker.Tc.fst @@ -120,7 +120,10 @@ let tc_decl_attributes env se = if lid_exists env PC.attr_substitute_lid then ([], se.sigattrs) else partition ((=) attr_substitute) se.sigattrs - in {se with sigattrs = blacklisted_attrs @ tc_attributes env other_attrs } + in + let g, other_attrs = tc_attributes env other_attrs in + Rel.force_trivial_guard env g; + {se with sigattrs = blacklisted_attrs @ other_attrs } let tc_inductive' env ses quals attrs lids = if Env.debug env Options.Low then diff --git a/src/typechecker/FStar.TypeChecker.TcTerm.fst b/src/typechecker/FStar.TypeChecker.TcTerm.fst index 02e400aca0a..58f67e08e95 100644 --- a/src/typechecker/FStar.TypeChecker.TcTerm.fst +++ b/src/typechecker/FStar.TypeChecker.TcTerm.fst @@ -4395,7 +4395,8 @@ and tc_binder env ({binder_bv=x;binder_qual=imp;binder_positivity=pqual;binder_a Some (Meta tau), g | _ -> imp, Env.trivial_guard in - let attrs = tc_attributes env attrs in + let g_attrs, attrs = tc_attributes env attrs in + let g = Env.conj_guard g g_attrs in check_erasable_binder_attributes env attrs t; let x = S.mk_binder_with_attrs ({x with sort=t}) imp pqual attrs in if Env.debug env Options.High @@ -4464,8 +4465,13 @@ and tc_trivial_guard env t = Rel.force_trivial_guard env g; t,c -and tc_attributes env attrs = - List.map (fun attr -> fst (tc_trivial_guard env attr)) attrs +and tc_attributes (env:env_t) (attrs : list term) : guard_t * list term = + List.fold_left + (fun (g, attrs) attr -> + let attr', _, g' = tc_tot_or_gtot_term env attr in + Env.conj_guard g g', attr' :: attrs) + (Env.trivial_guard, []) + (List.rev attrs) let tc_check_trivial_guard env t k = let t, _, g = tc_check_tot_or_gtot_term env t k "" in diff --git a/src/typechecker/FStar.TypeChecker.TcTerm.fsti b/src/typechecker/FStar.TypeChecker.TcTerm.fsti index 9306f4a1f58..a9b5584f2a8 100644 --- a/src/typechecker/FStar.TypeChecker.TcTerm.fsti +++ b/src/typechecker/FStar.TypeChecker.TcTerm.fsti @@ -48,7 +48,7 @@ val tc_tot_or_gtot_term: env -> term -> term * lcomp * guard_t val tc_check_tot_or_gtot_term: env -> term -> typ -> string -> term * lcomp * guard_t val tc_tactic : typ -> typ -> env -> term -> term * lcomp * guard_t val tc_trivial_guard: env -> term -> term * lcomp -val tc_attributes: env -> list term -> list term +val tc_attributes: env -> list term -> guard_t & list term val tc_check_trivial_guard: env -> term -> term -> term val value_check_expected_typ: env -> term -> either typ lcomp -> guard_t -> term * lcomp * guard_t diff --git a/tests/typeclasses/Bug3130f.fst b/tests/typeclasses/Bug3130f.fst new file mode 100644 index 00000000000..96bd793c949 --- /dev/null +++ b/tests/typeclasses/Bug3130f.fst @@ -0,0 +1,22 @@ +module Bug3130f + +(* A shrunk down version of Comparse.Tests.TacticFeatures. *) + +class bytes_like (bytes:Type0) = { + length: bytes -> nat; +} + +assume val test_ei: bytes:Type0 -> {|bytes_like bytes|} -> Type0 +assume val ps_test_dep_nat_e: #bytes:Type0 -> {|bytes_like bytes|} -> nat + +assume +val fun_test_with_parser (bytes:Type0) {|d : bytes_like bytes|} : + (f1: option (test_ei bytes)) -> + [@@@ (ps_test_dep_nat_e #bytes)](u : unit) -> + unit + +noeq type test_with_parser (bytes:Type0) {|d : bytes_like bytes|} = { + f1: option (test_ei bytes); + [@@@ (ps_test_dep_nat_e #bytes) ] + u : unit; +} From 4f080362c79bf0f57b2c0052b9935c3323b9ce4e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Mon, 4 Dec 2023 14:45:41 -0800 Subject: [PATCH 15/29] Tc: fix typo --- src/typechecker/FStar.TypeChecker.Rel.fst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/typechecker/FStar.TypeChecker.Rel.fst b/src/typechecker/FStar.TypeChecker.Rel.fst index e8eaa929c74..b0da3e92b5c 100644 --- a/src/typechecker/FStar.TypeChecker.Rel.fst +++ b/src/typechecker/FStar.TypeChecker.Rel.fst @@ -5601,7 +5601,7 @@ let force_trivial_guard env g = | imp::_ -> let open FStar.Pprint in raise_error_doc (Errors.Fatal_FailToResolveImplicitArgument, [ - prefix 4 1 (text "Failed to resolved implicit argument") + prefix 4 1 (text "Failed to resolve implicit argument") (arbitrary_string (Print.uvar_to_string imp.imp_uvar.ctx_uvar_head)) ^/^ prefix 4 1 (text "of type") (N.term_to_doc env (U.ctx_uvar_typ imp.imp_uvar)) ^/^ From 682664503823388cce43344c8dd153994608e6b6 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Mon, 4 Dec 2023 14:46:14 -0800 Subject: [PATCH 16/29] Tc: Gen: improve error message --- src/typechecker/FStar.TypeChecker.Generalize.fst | 16 +++++++++------- 1 file changed, 9 insertions(+), 7 deletions(-) diff --git a/src/typechecker/FStar.TypeChecker.Generalize.fst b/src/typechecker/FStar.TypeChecker.Generalize.fst index 5ae52505bfe..e391a4c75b0 100644 --- a/src/typechecker/FStar.TypeChecker.Generalize.fst +++ b/src/typechecker/FStar.TypeChecker.Generalize.fst @@ -182,14 +182,16 @@ let gen env (is_rec:bool) (lecs:list (lbname * term * comp)) : option (list (lbn let lecs = lec_hd :: lecs in let gen_types (uvs:list ctx_uvar) : list (bv * bqual) = - let fail rng k : unit = + let fail (rng:Range.range) (k:typ) : unit = + let open FStar.Pprint in + let open FStar.Class.PP in let lbname, e, c = lec_hd in - raise_error (Errors.Fatal_FailToResolveImplicitArgument, - BU.format3 "Failed to resolve implicit argument of type '%s' in the type of %s (%s)" - (Print.term_to_string k) - (Print.lbname_to_string lbname) - (Print.term_to_string (U.comp_result c))) - rng + raise_error_doc (Errors.Fatal_FailToResolveImplicitArgument, [ + prefix 4 1 (text "Failed to resolve implicit argument of type") + (pp k) ^/^ + prefix 4 1 (group (text "in the type of" ^/^ squotes (doc_of_string (Print.lbname_to_string lbname)) ^^ colon)) + (pp (U.comp_result c)) + ]) rng in uvs |> List.map (fun u -> match UF.find u.ctx_uvar_head with From 56f628d6966ec1337b244207707397a0e16e13fe Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Mon, 4 Dec 2023 14:46:28 -0800 Subject: [PATCH 17/29] Tc: Gen: do not generalize implicits that have a meta Fixes Bug3130e --- src/typechecker/FStar.TypeChecker.Generalize.fst | 8 ++++++-- tests/typeclasses/Bug3130e.fst | 7 +++---- 2 files changed, 9 insertions(+), 6 deletions(-) diff --git a/src/typechecker/FStar.TypeChecker.Generalize.fst b/src/typechecker/FStar.TypeChecker.Generalize.fst index e391a4c75b0..39aa8eda86c 100644 --- a/src/typechecker/FStar.TypeChecker.Generalize.fst +++ b/src/typechecker/FStar.TypeChecker.Generalize.fst @@ -193,7 +193,11 @@ let gen env (is_rec:bool) (lecs:list (lbname * term * comp)) : option (list (lbn (pp (U.comp_result c)) ]) rng in - uvs |> List.map (fun u -> + uvs |> List.concatMap (fun u -> + (* If this implicit has a meta, don't generalize it. Just leave it + unresolved for the resolve_implicits phase to fill it in. *) + if Some? u.ctx_uvar_meta then [] else + match UF.find u.ctx_uvar_head with | Some _ -> failwith "Unexpected instantiation of mutually recursive uvar" | _ -> @@ -222,7 +226,7 @@ let gen env (is_rec:bool) (lecs:list (lbname * term * comp)) : option (list (lbn U.set_uvar u.ctx_uvar_head t; //t clearly has a free variable; this is the one place we break the //invariant of a uvar always being resolved to a term well-typed in its given context - a, S.as_bqual_implicit true) + [a, S.as_bqual_implicit true]) in let gen_univs = gen_univs env univs in diff --git a/tests/typeclasses/Bug3130e.fst b/tests/typeclasses/Bug3130e.fst index a8524458cd0..bff50956e4e 100644 --- a/tests/typeclasses/Bug3130e.fst +++ b/tests/typeclasses/Bug3130e.fst @@ -10,10 +10,9 @@ let transitivity {| ord_leq 'a |} (x y z : 'a) [SMTPat (x `leq` y); SMTPat (x `leq` z)] = trans x y z -(* Currently fails since the type of the uu binder is undefined, -and tcresolve won't run *) -[@@expect_failure [66]] -let transitivity_forall #a {| ord_leq a |} uu +(* NB: unused will be generalized *) +let transitivity_forall #a {| ord_leq a |} + unused : Lemma (forall (x y z : a). x `leq` y /\ y `leq` z ==> x `leq` z ) = () From fd2fe0cd89c13ae2496fa73e114a846fb4c8e24d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Mon, 4 Dec 2023 14:09:23 -0800 Subject: [PATCH 18/29] snap --- ocaml/fstar-lib/generated/FStar_Class_Show.ml | 2 + .../generated/FStar_TypeChecker_Generalize.ml | 199 +++++++++++------- .../generated/FStar_TypeChecker_Rel.ml | 2 +- .../generated/FStar_TypeChecker_Tc.ml | 35 +-- .../generated/FStar_TypeChecker_TcTerm.ml | 76 ++++--- .../generated/FStar_TypeChecker_Util.ml | 14 +- 6 files changed, 199 insertions(+), 129 deletions(-) diff --git a/ocaml/fstar-lib/generated/FStar_Class_Show.ml b/ocaml/fstar-lib/generated/FStar_Class_Show.ml index ab58a053cdc..5bc610d228d 100644 --- a/ocaml/fstar-lib/generated/FStar_Class_Show.ml +++ b/ocaml/fstar-lib/generated/FStar_Class_Show.ml @@ -9,6 +9,8 @@ let printableshow : 'a . 'a FStar_Class_Printable.printable -> 'a showable = fun uu___ -> { show = (FStar_Class_Printable.to_string uu___) } let show_list : 'a . 'a showable -> 'a Prims.list showable = fun uu___ -> { show = ((FStar_Common.string_of_list ()) (show uu___)) } +let show_set : 'a . 'a showable -> 'a FStar_Compiler_Util.set showable = + fun uu___ -> { show = (FStar_Common.string_of_set (show uu___)) } let show_option : 'a . 'a showable -> 'a FStar_Pervasives_Native.option showable = fun uu___ -> { show = (FStar_Common.string_of_option (show uu___)) } diff --git a/ocaml/fstar-lib/generated/FStar_TypeChecker_Generalize.ml b/ocaml/fstar-lib/generated/FStar_TypeChecker_Generalize.ml index 02c83603f9f..e6f1268ec01 100644 --- a/ocaml/fstar-lib/generated/FStar_TypeChecker_Generalize.ml +++ b/ocaml/fstar-lib/generated/FStar_TypeChecker_Generalize.ml @@ -391,90 +391,131 @@ let (gen : | (lbname, e, c) -> let uu___4 = let uu___5 = - let uu___6 = FStar_Syntax_Print.term_to_string k in - let uu___7 = - FStar_Syntax_Print.lbname_to_string lbname in - let uu___8 = - FStar_Syntax_Print.term_to_string - (FStar_Syntax_Util.comp_result c) in - FStar_Compiler_Util.format3 - "Failed to resolve implicit argument of type '%s' in the type of %s (%s)" - uu___6 uu___7 uu___8 in + let uu___6 = + let uu___7 = + let uu___8 = + FStar_Errors_Msg.text + "Failed to resolve implicit argument of type" in + let uu___9 = + FStar_Class_PP.pp + FStar_Syntax_Print.pretty_term k in + FStar_Pprint.prefix (Prims.of_int (4)) + Prims.int_one uu___8 uu___9 in + let uu___8 = + let uu___9 = + let uu___10 = + let uu___11 = + FStar_Errors_Msg.text "in the type of" in + let uu___12 = + let uu___13 = + let uu___14 = + let uu___15 = + FStar_Syntax_Print.lbname_to_string + lbname in + FStar_Pprint.doc_of_string uu___15 in + FStar_Pprint.squotes uu___14 in + FStar_Pprint.op_Hat_Hat uu___13 + FStar_Pprint.colon in + FStar_Pprint.op_Hat_Slash_Hat uu___11 + uu___12 in + FStar_Pprint.group uu___10 in + let uu___10 = + FStar_Class_PP.pp + FStar_Syntax_Print.pretty_term + (FStar_Syntax_Util.comp_result c) in + FStar_Pprint.prefix (Prims.of_int (4)) + Prims.int_one uu___9 uu___10 in + FStar_Pprint.op_Hat_Slash_Hat uu___7 uu___8 in + [uu___6] in (FStar_Errors_Codes.Fatal_FailToResolveImplicitArgument, uu___5) in - FStar_Errors.raise_error uu___4 rng in + FStar_Errors.raise_error_doc uu___4 rng in FStar_Compiler_Effect.op_Bar_Greater uvs1 - (FStar_Compiler_List.map + (FStar_Compiler_List.concatMap (fun u -> - let uu___3 = - FStar_Syntax_Unionfind.find - u.FStar_Syntax_Syntax.ctx_uvar_head in - match uu___3 with - | FStar_Pervasives_Native.Some uu___4 -> - failwith - "Unexpected instantiation of mutually recursive uvar" - | uu___4 -> - let k = - let uu___5 = FStar_Syntax_Util.ctx_uvar_typ u in - FStar_TypeChecker_Normalize.normalize - [FStar_TypeChecker_Env.Beta; - FStar_TypeChecker_Env.Exclude - FStar_TypeChecker_Env.Zeta] env uu___5 in - let uu___5 = FStar_Syntax_Util.arrow_formals k in - (match uu___5 with - | (bs, kres) -> - ((let uu___7 = - let uu___8 = - let uu___9 = - FStar_TypeChecker_Normalize.unfold_whnf - env kres in - FStar_Syntax_Util.unrefine uu___9 in - uu___8.FStar_Syntax_Syntax.n in - match uu___7 with - | FStar_Syntax_Syntax.Tm_type uu___8 -> - let free = - FStar_Syntax_Free.names kres in - let uu___9 = + if + FStar_Pervasives_Native.uu___is_Some + u.FStar_Syntax_Syntax.ctx_uvar_meta + then [] + else + (let uu___4 = + FStar_Syntax_Unionfind.find + u.FStar_Syntax_Syntax.ctx_uvar_head in + match uu___4 with + | FStar_Pervasives_Native.Some uu___5 -> + failwith + "Unexpected instantiation of mutually recursive uvar" + | uu___5 -> + let k = + let uu___6 = + FStar_Syntax_Util.ctx_uvar_typ u in + FStar_TypeChecker_Normalize.normalize + [FStar_TypeChecker_Env.Beta; + FStar_TypeChecker_Env.Exclude + FStar_TypeChecker_Env.Zeta] env uu___6 in + let uu___6 = + FStar_Syntax_Util.arrow_formals k in + (match uu___6 with + | (bs, kres) -> + ((let uu___8 = + let uu___9 = + let uu___10 = + FStar_TypeChecker_Normalize.unfold_whnf + env kres in + FStar_Syntax_Util.unrefine uu___10 in + uu___9.FStar_Syntax_Syntax.n in + match uu___8 with + | FStar_Syntax_Syntax.Tm_type uu___9 + -> + let free = + FStar_Syntax_Free.names kres in + let uu___10 = + let uu___11 = + FStar_Compiler_Util.set_is_empty + free in + Prims.op_Negation uu___11 in + if uu___10 + then + fail + u.FStar_Syntax_Syntax.ctx_uvar_range + kres + else () + | uu___9 -> + fail + u.FStar_Syntax_Syntax.ctx_uvar_range + kres); + (let a = + let uu___8 = + let uu___9 = + FStar_TypeChecker_Env.get_range + env in + FStar_Compiler_Effect.op_Less_Bar + (fun uu___10 -> + FStar_Pervasives_Native.Some + uu___10) uu___9 in + FStar_Syntax_Syntax.new_bv uu___8 + kres in + let t = + match bs with + | [] -> + FStar_Syntax_Syntax.bv_to_name a + | uu___8 -> + let uu___9 = + FStar_Syntax_Syntax.bv_to_name + a in + FStar_Syntax_Util.abs bs uu___9 + (FStar_Pervasives_Native.Some + (FStar_Syntax_Util.residual_tot + kres)) in + FStar_Syntax_Util.set_uvar + u.FStar_Syntax_Syntax.ctx_uvar_head + t; + (let uu___9 = let uu___10 = - FStar_Compiler_Util.set_is_empty - free in - Prims.op_Negation uu___10 in - if uu___9 - then - fail - u.FStar_Syntax_Syntax.ctx_uvar_range - kres - else () - | uu___8 -> - fail - u.FStar_Syntax_Syntax.ctx_uvar_range - kres); - (let a = - let uu___7 = - let uu___8 = - FStar_TypeChecker_Env.get_range env in - FStar_Compiler_Effect.op_Less_Bar - (fun uu___9 -> - FStar_Pervasives_Native.Some - uu___9) uu___8 in - FStar_Syntax_Syntax.new_bv uu___7 kres in - let t = - match bs with - | [] -> - FStar_Syntax_Syntax.bv_to_name a - | uu___7 -> - let uu___8 = - FStar_Syntax_Syntax.bv_to_name a in - FStar_Syntax_Util.abs bs uu___8 - (FStar_Pervasives_Native.Some - (FStar_Syntax_Util.residual_tot - kres)) in - FStar_Syntax_Util.set_uvar - u.FStar_Syntax_Syntax.ctx_uvar_head t; - (let uu___8 = - FStar_Syntax_Syntax.as_bqual_implicit - true in - (a, uu___8))))))) in + FStar_Syntax_Syntax.as_bqual_implicit + true in + (a, uu___10) in + [uu___9]))))))) in let gen_univs1 = gen_univs env univs in let gen_tvars = gen_types uvs in let ecs = diff --git a/ocaml/fstar-lib/generated/FStar_TypeChecker_Rel.ml b/ocaml/fstar-lib/generated/FStar_TypeChecker_Rel.ml index 8d8e1f1d5a3..94634e5cff8 100644 --- a/ocaml/fstar-lib/generated/FStar_TypeChecker_Rel.ml +++ b/ocaml/fstar-lib/generated/FStar_TypeChecker_Rel.ml @@ -15729,7 +15729,7 @@ let (force_trivial_guard : let uu___5 = let uu___6 = FStar_Errors_Msg.text - "Failed to resolved implicit argument" in + "Failed to resolve implicit argument" in let uu___7 = let uu___8 = FStar_Syntax_Print.uvar_to_string diff --git a/ocaml/fstar-lib/generated/FStar_TypeChecker_Tc.ml b/ocaml/fstar-lib/generated/FStar_TypeChecker_Tc.ml index d8fbbf6ddd2..1eba09d5e66 100644 --- a/ocaml/fstar-lib/generated/FStar_TypeChecker_Tc.ml +++ b/ocaml/fstar-lib/generated/FStar_TypeChecker_Tc.ml @@ -356,20 +356,25 @@ let (tc_decl_attributes : se.FStar_Syntax_Syntax.sigattrs in match uu___ with | (blacklisted_attrs, other_attrs) -> - let uu___1 = - let uu___2 = - FStar_TypeChecker_TcTerm.tc_attributes env other_attrs in - FStar_Compiler_List.op_At blacklisted_attrs uu___2 in - { - FStar_Syntax_Syntax.sigel = (se.FStar_Syntax_Syntax.sigel); - FStar_Syntax_Syntax.sigrng = (se.FStar_Syntax_Syntax.sigrng); - FStar_Syntax_Syntax.sigquals = (se.FStar_Syntax_Syntax.sigquals); - FStar_Syntax_Syntax.sigmeta = (se.FStar_Syntax_Syntax.sigmeta); - FStar_Syntax_Syntax.sigattrs = uu___1; - FStar_Syntax_Syntax.sigopens_and_abbrevs = - (se.FStar_Syntax_Syntax.sigopens_and_abbrevs); - FStar_Syntax_Syntax.sigopts = (se.FStar_Syntax_Syntax.sigopts) - } + let uu___1 = FStar_TypeChecker_TcTerm.tc_attributes env other_attrs in + (match uu___1 with + | (g, other_attrs1) -> + (FStar_TypeChecker_Rel.force_trivial_guard env g; + { + FStar_Syntax_Syntax.sigel = (se.FStar_Syntax_Syntax.sigel); + FStar_Syntax_Syntax.sigrng = + (se.FStar_Syntax_Syntax.sigrng); + FStar_Syntax_Syntax.sigquals = + (se.FStar_Syntax_Syntax.sigquals); + FStar_Syntax_Syntax.sigmeta = + (se.FStar_Syntax_Syntax.sigmeta); + FStar_Syntax_Syntax.sigattrs = + (FStar_Compiler_List.op_At blacklisted_attrs other_attrs1); + FStar_Syntax_Syntax.sigopens_and_abbrevs = + (se.FStar_Syntax_Syntax.sigopens_and_abbrevs); + FStar_Syntax_Syntax.sigopts = + (se.FStar_Syntax_Syntax.sigopts) + })) let (tc_inductive' : FStar_TypeChecker_Env.env -> FStar_Syntax_Syntax.sigelt Prims.list -> @@ -4957,7 +4962,7 @@ let (tc_decls : ([], env) ses) in match uu___ with | (ses1, env1) -> ((FStar_Compiler_List.rev_append ses1 []), env1) -let (uu___905 : unit) = +let (uu___909 : unit) = FStar_Compiler_Effect.op_Colon_Equals tc_decls_knot (FStar_Pervasives_Native.Some tc_decls) let (snapshot_context : diff --git a/ocaml/fstar-lib/generated/FStar_TypeChecker_TcTerm.ml b/ocaml/fstar-lib/generated/FStar_TypeChecker_TcTerm.ml index 4d934dfd042..ca67bc30eab 100644 --- a/ocaml/fstar-lib/generated/FStar_TypeChecker_TcTerm.ml +++ b/ocaml/fstar-lib/generated/FStar_TypeChecker_TcTerm.ml @@ -12233,33 +12233,37 @@ and (tc_binder : | uu___6 -> (imp, FStar_TypeChecker_Env.trivial_guard) in (match uu___5 with | (imp1, g') -> - let attrs1 = tc_attributes env attrs in - (check_erasable_binder_attributes env attrs1 t; - (let x1 = - FStar_Syntax_Syntax.mk_binder_with_attrs - { - FStar_Syntax_Syntax.ppname = - (x.FStar_Syntax_Syntax.ppname); - FStar_Syntax_Syntax.index = - (x.FStar_Syntax_Syntax.index); - FStar_Syntax_Syntax.sort = t - } imp1 pqual attrs1 in - (let uu___8 = - FStar_TypeChecker_Env.debug env - FStar_Options.High in - if uu___8 - then - let uu___9 = - FStar_Syntax_Print.bv_to_string - x1.FStar_Syntax_Syntax.binder_bv in - let uu___10 = - FStar_Syntax_Print.term_to_string t in - FStar_Compiler_Util.print2 - "Pushing binder %s at type %s\n" uu___9 - uu___10 - else ()); - (let uu___8 = push_binding env x1 in - (x1, uu___8, g, u)))))))) + let uu___6 = tc_attributes env attrs in + (match uu___6 with + | (g_attrs, attrs1) -> + let g1 = + FStar_TypeChecker_Env.conj_guard g g_attrs in + (check_erasable_binder_attributes env attrs1 t; + (let x1 = + FStar_Syntax_Syntax.mk_binder_with_attrs + { + FStar_Syntax_Syntax.ppname = + (x.FStar_Syntax_Syntax.ppname); + FStar_Syntax_Syntax.index = + (x.FStar_Syntax_Syntax.index); + FStar_Syntax_Syntax.sort = t + } imp1 pqual attrs1 in + (let uu___9 = + FStar_TypeChecker_Env.debug env + FStar_Options.High in + if uu___9 + then + let uu___10 = + FStar_Syntax_Print.bv_to_string + x1.FStar_Syntax_Syntax.binder_bv in + let uu___11 = + FStar_Syntax_Print.term_to_string t in + FStar_Compiler_Util.print2 + "Pushing binder %s at type %s\n" + uu___10 uu___11 + else ()); + (let uu___9 = push_binding env x1 in + (x1, uu___9, g1, u))))))))) and (tc_binders : FStar_TypeChecker_Env.env -> FStar_Syntax_Syntax.binders -> @@ -12442,14 +12446,22 @@ and (tc_trivial_guard : and (tc_attributes : FStar_TypeChecker_Env.env -> FStar_Syntax_Syntax.term Prims.list -> - FStar_Syntax_Syntax.term Prims.list) + (FStar_TypeChecker_Env.guard_t * FStar_Syntax_Syntax.term Prims.list)) = fun env -> fun attrs -> - FStar_Compiler_List.map - (fun attr -> - let uu___ = tc_trivial_guard env attr in - FStar_Pervasives_Native.fst uu___) attrs + FStar_Compiler_List.fold_left + (fun uu___ -> + fun attr -> + match uu___ with + | (g, attrs1) -> + let uu___1 = tc_tot_or_gtot_term env attr in + (match uu___1 with + | (attr', uu___2, g') -> + let uu___3 = FStar_TypeChecker_Env.conj_guard g g' in + (uu___3, (attr' :: attrs1)))) + (FStar_TypeChecker_Env.trivial_guard, []) + (FStar_Compiler_List.rev attrs) let (tc_check_trivial_guard : FStar_TypeChecker_Env.env -> FStar_Syntax_Syntax.term -> diff --git a/ocaml/fstar-lib/generated/FStar_TypeChecker_Util.ml b/ocaml/fstar-lib/generated/FStar_TypeChecker_Util.ml index 8491211076e..b129fd008c7 100644 --- a/ocaml/fstar-lib/generated/FStar_TypeChecker_Util.ml +++ b/ocaml/fstar-lib/generated/FStar_TypeChecker_Util.ml @@ -6721,9 +6721,19 @@ let (maybe_instantiate : | uu___5 -> failwith "Impossible, match is under a guard, did not expect this case" in + let msg = + let is_typeclass = + match meta_t with + | FStar_Syntax_Syntax.Ctx_uvar_meta_tac + (uu___5, tau) -> + FStar_Syntax_Util.is_fvar + FStar_Parser_Const.tcresolve_lid tau + | uu___5 -> false in + if is_typeclass + then "Typeclass constraint argument" + else "Instantiation of meta argument" in let uu___5 = - FStar_TypeChecker_Env.new_implicit_var_aux - "Instantiation of meta argument" + FStar_TypeChecker_Env.new_implicit_var_aux msg e.FStar_Syntax_Syntax.pos env t2 FStar_Syntax_Syntax.Strict (FStar_Pervasives_Native.Some meta_t) in From eb3a541b43684c6d14cf582c90464121b31b5beb Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Tue, 5 Dec 2023 02:19:10 -0800 Subject: [PATCH 19/29] Syntax/Tc: show instance for bindings/gamma --- src/syntax/FStar.Syntax.Print.fst | 7 ++++++ src/syntax/FStar.Syntax.Print.fsti | 25 ++++++++++---------- src/tactics/FStar.Tactics.V1.Basic.fst | 2 +- src/tactics/FStar.Tactics.V2.Basic.fst | 2 +- src/typechecker/FStar.TypeChecker.Common.fst | 12 +--------- src/typechecker/FStar.TypeChecker.Core.fst | 4 ++-- src/typechecker/FStar.TypeChecker.Env.fst | 10 -------- src/typechecker/FStar.TypeChecker.Env.fsti | 3 --- src/typechecker/FStar.TypeChecker.Rel.fst | 3 +-- 9 files changed, 26 insertions(+), 42 deletions(-) diff --git a/src/syntax/FStar.Syntax.Print.fst b/src/syntax/FStar.Syntax.Print.fst index 717f2cb2d9f..d6c3343c64f 100644 --- a/src/syntax/FStar.Syntax.Print.fst +++ b/src/syntax/FStar.Syntax.Print.fst @@ -999,3 +999,10 @@ instance showable_bv = { show = bv_to_string; } instance showable_binder = { show = binder_to_string; } instance showable_uvar = { show = uvar_to_string; } instance showable_ctxu = { show = ctx_uvar_to_string; } + +instance showable_binding = { + show = (function + | Binding_var x -> "Binding_var " ^ show x + | Binding_lid x -> "Binding_lid " ^ show x + | Binding_univ x -> "Binding_univ " ^ show x); +} diff --git a/src/syntax/FStar.Syntax.Print.fsti b/src/syntax/FStar.Syntax.Print.fsti index 239d66b14a6..00af6f6cb86 100644 --- a/src/syntax/FStar.Syntax.Print.fsti +++ b/src/syntax/FStar.Syntax.Print.fsti @@ -89,16 +89,17 @@ val term_to_doc : term -> Pprint.document val comp_to_doc : comp -> Pprint.document val sigelt_to_doc : sigelt -> Pprint.document -instance val pretty_term : pretty term -instance val pretty_univ : pretty universe -instance val pretty_comp : pretty comp -instance val pretty_sigelt : pretty sigelt +instance val pretty_term : pretty term +instance val pretty_univ : pretty universe +instance val pretty_comp : pretty comp +instance val pretty_sigelt : pretty sigelt -instance val showable_term : showable term -instance val showable_univ : showable universe -instance val showable_comp : showable comp -instance val showable_sigelt : showable sigelt -instance val showable_bv : showable bv -instance val showable_binder : showable binder -instance val showable_uvar : showable uvar -instance val showable_ctxu : showable ctx_uvar +instance val showable_term : showable term +instance val showable_univ : showable universe +instance val showable_comp : showable comp +instance val showable_sigelt : showable sigelt +instance val showable_bv : showable bv +instance val showable_binder : showable binder +instance val showable_uvar : showable uvar +instance val showable_ctxu : showable ctx_uvar +instance val showable_binding : showable binding diff --git a/src/tactics/FStar.Tactics.V1.Basic.fst b/src/tactics/FStar.Tactics.V1.Basic.fst index a54b5bc802c..e520d225a3b 100644 --- a/src/tactics/FStar.Tactics.V1.Basic.fst +++ b/src/tactics/FStar.Tactics.V1.Basic.fst @@ -964,7 +964,7 @@ let t_apply (uopt:bool) (only_match:bool) (tc_resolved_uvars:bool) (tm:term) : t (fun () -> BU.print5 "t_apply: tm = %s\nt_apply: goal = %s\nenv.gamma=%s\ntyp=%s\nguard=%s\n" (show tm) (goal_to_string_verbose goal) - (Env.print_gamma e.gamma) + (show e.gamma) (show typ) (Rel.guard_to_string e guard)) ;! // Focus helps keep the goal order diff --git a/src/tactics/FStar.Tactics.V2.Basic.fst b/src/tactics/FStar.Tactics.V2.Basic.fst index 96ef9abce8b..e292370314d 100644 --- a/src/tactics/FStar.Tactics.V2.Basic.fst +++ b/src/tactics/FStar.Tactics.V2.Basic.fst @@ -1000,7 +1000,7 @@ let t_apply (uopt:bool) (only_match:bool) (tc_resolved_uvars:bool) (tm:term) : t (fun () -> BU.print5 "t_apply: tm = %s\nt_apply: goal = %s\nenv.gamma=%s\ntyp=%s\nguard=%s\n" (show tm) (goal_to_string_verbose goal) - (Env.print_gamma e.gamma) + (show e.gamma) (show typ) (Rel.guard_to_string e guard)) ;! // Focus helps keep the goal order diff --git a/src/typechecker/FStar.TypeChecker.Common.fst b/src/typechecker/FStar.TypeChecker.Common.fst index 0a4fe72630b..693ccbd40c8 100644 --- a/src/typechecker/FStar.TypeChecker.Common.fst +++ b/src/typechecker/FStar.TypeChecker.Common.fst @@ -163,16 +163,6 @@ let id_info_at_pos (table: id_info_table) (fn:string) (row:int) (col:int) : opti if col <= last_col then Some info else None let check_uvar_ctx_invariant (reason:string) (r:range) (should_check:bool) (g:gamma) (bs:binders) = - let print_gamma gamma = - (gamma |> List.map (function - | Binding_var x -> "Binding_var " ^ (Print.bv_to_string x) - | Binding_univ u -> "Binding_univ " ^ (string_of_id u) - | Binding_lid (l, _) -> "Binding_lid " ^ (Ident.string_of_lid l)))// @ - // (env.gamma_sig |> List.map (fun (ls, _) -> - // "Binding_sig " ^ (ls |> List.map Ident.string_of_lid |> String.concat ", ") - // )) - |> String.concat "::\n" - in let fail () = failwith (BU.format5 "Invariant violation: gamma and binders are out of sync\n\t\ @@ -182,7 +172,7 @@ let check_uvar_ctx_invariant (reason:string) (r:range) (should_check:bool) (g:ga reason (Range.string_of_range r) (if should_check then "true" else "false") - (print_gamma g) + (show g) (FStar.Syntax.Print.binders_to_string ", " bs)) in if not should_check then () diff --git a/src/typechecker/FStar.TypeChecker.Core.fst b/src/typechecker/FStar.TypeChecker.Core.fst index 609d9b6dbb1..dcdb5f214fc 100644 --- a/src/typechecker/FStar.TypeChecker.Core.fst +++ b/src/typechecker/FStar.TypeChecker.Core.fst @@ -570,10 +570,10 @@ let lookup (g:env) (e:term) : result (tot_or_ghost & typ) = then ( record_cache_hit(); // BU.print4 "cache hit\n %s |- %s : %s\nmatching env %s\n" - // (Env.print_gamma g.tcenv.gamma) + // (show g.tcenv.gamma) // (P.term_to_string e) // (P.term_to_string (snd (fst he.he_res))) - // (Env.print_gamma he.he_gamma); + // (show he.he_gamma); fun _ -> Inl he.he_res ) else ( diff --git a/src/typechecker/FStar.TypeChecker.Env.fst b/src/typechecker/FStar.TypeChecker.Env.fst index 32053f9ec64..24f9052e9fb 100644 --- a/src/typechecker/FStar.TypeChecker.Env.fst +++ b/src/typechecker/FStar.TypeChecker.Env.fst @@ -1717,16 +1717,6 @@ let univnames env = in aux no_univ_names env.gamma -let print_gamma gamma = - (gamma |> List.map (function - | Binding_var x -> "Binding_var (" ^ (Print.bv_to_string x) ^ ":" ^ (Print.term_to_string x.sort) ^ ")" - | Binding_univ u -> "Binding_univ " ^ (string_of_id u) - | Binding_lid (l, _) -> "Binding_lid " ^ (Ident.string_of_lid l)))// @ - // (env.gamma_sig |> List.map (fun (ls, _) -> - // "Binding_sig " ^ (ls |> List.map Ident.string_of_lid |> String.concat ", ") - // )) - |> String.concat "::\n" - let string_of_delta_level = function | NoDelta -> "NoDelta" | InliningDelta -> "Inlining" diff --git a/src/typechecker/FStar.TypeChecker.Env.fsti b/src/typechecker/FStar.TypeChecker.Env.fsti index 20902bae56f..cb9de343f30 100644 --- a/src/typechecker/FStar.TypeChecker.Env.fsti +++ b/src/typechecker/FStar.TypeChecker.Env.fsti @@ -494,9 +494,6 @@ val new_implicit_var_aux : string -> option ctx_uvar_meta_t -> (term * list (ctx_uvar * Range.range) * guard_t) - -val print_gamma : gamma -> string - (* layered effect utils *) (* diff --git a/src/typechecker/FStar.TypeChecker.Rel.fst b/src/typechecker/FStar.TypeChecker.Rel.fst index b0da3e92b5c..d62a69c399c 100644 --- a/src/typechecker/FStar.TypeChecker.Rel.fst +++ b/src/typechecker/FStar.TypeChecker.Rel.fst @@ -4777,8 +4777,7 @@ let try_teq smt_ok env t1 t2 : option guard_t = Profiling.profile (fun () -> if Env.debug env <| Options.Other "Rel" then - BU.print3 "try_teq of %s and %s in %s {\n" (show t1) (show t2) - (Env.print_gamma env.gamma); + BU.print3 "try_teq of %s and %s in %s {\n" (show t1) (show t2) (show env.gamma); let prob, wl = new_t_problem (empty_worklist env) env t1 EQ t2 None (Env.get_range env) in let g = with_guard env prob <| solve_and_commit (singleton wl prob smt_ok) (fun _ -> None) in if Env.debug env <| Options.Other "Rel" then From ba86538a1b239ac157d5e8bb0c2f06dbdf57d3e9 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Mon, 4 Dec 2023 17:07:10 -0800 Subject: [PATCH 20/29] Add repro for #1066, somehow missing --- tests/bug-reports/Bug1066.fst | 14 ++++++++++++++ tests/bug-reports/Makefile | 2 +- 2 files changed, 15 insertions(+), 1 deletion(-) create mode 100644 tests/bug-reports/Bug1066.fst diff --git a/tests/bug-reports/Bug1066.fst b/tests/bug-reports/Bug1066.fst new file mode 100644 index 00000000000..f37c4471e35 --- /dev/null +++ b/tests/bug-reports/Bug1066.fst @@ -0,0 +1,14 @@ +module Bug1066 + +assume val m : Type -> Type +assume val return_m : #a:Type -> a -> m a +assume val bind_m : #a:Type -> #b:Type -> m a -> (a -> m b) -> m b +assume val push_m : #a:Type -> #b:(a -> Type) -> (x:a -> m (b x)) -> m (x:a -> b x) + +val push_sum : #a:Type -> #b:(a -> Type) -> + dtuple2 a (fun (x:a) -> m (b x)) -> m (dtuple2 a b) +let push_sum (#a:Type) (#b:(a -> Type)) (p : (dtuple2 a (fun (x:a) -> m (b x)))) = + match p with + | Mkdtuple2 x y -> + bind_m #(b x) (* #(dtuple2 a b) *) y (fun (y' : b x) -> + return_m (* #(dtuple2 a b) *) (Mkdtuple2 x y')) diff --git a/tests/bug-reports/Makefile b/tests/bug-reports/Makefile index 95ab57c9eb3..37ee5f22a1c 100644 --- a/tests/bug-reports/Makefile +++ b/tests/bug-reports/Makefile @@ -54,7 +54,7 @@ SHOULD_VERIFY_CLOSED=Bug022.fst Bug024.fst Bug025.fst Bug026.fst Bug026b.fst Bug Bug2756.fst MutualRecPositivity.fst Bug2806a.fst Bug2806b.fst Bug2806c.fst Bug2806d.fst Bug2809.fst\ Bug2849a.fst Bug2849b.fst Bug2045.fst Bug2876.fst Bug2882.fst Bug2895.fst Bug2894.fst \ Bug2415.fst Bug3028.fst Bug2954.fst Bug3089.fst Bug3102.fst Bug2981.fst Bug2980.fst Bug3115.fst \ - Bug2083.fst Bug2002.fst Bug1482.fst + Bug2083.fst Bug2002.fst Bug1482.fst Bug1066.fst SHOULD_VERIFY_INTERFACE_CLOSED=Bug771.fsti Bug771b.fsti SHOULD_VERIFY_AND_WARN_CLOSED=Bug016.fst From e37da50a39cd1af585b368be70a404144a272953 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Mon, 4 Dec 2023 18:21:15 -0800 Subject: [PATCH 21/29] Typeclass: more debug --- ulib/FStar.Tactics.Typeclasses.fst | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/ulib/FStar.Tactics.Typeclasses.fst b/ulib/FStar.Tactics.Typeclasses.fst index b7ebae7649c..aa6efec335b 100644 --- a/ulib/FStar.Tactics.Typeclasses.fst +++ b/ulib/FStar.Tactics.Typeclasses.fst @@ -163,6 +163,7 @@ let tcresolve () : Tac unit = // So intro if that's the case // Not using intros () directly, since that unfolds aggressively if the term is not an arrow // TODO: Should we..? Why wouldn't the head always be an FV? + let w = cur_witness () in maybe_intros (); // Fetch a list of all instances in scope right now. @@ -170,7 +171,8 @@ let tcresolve () : Tac unit = // stored. let glb = lookup_attr (`tcinstance) (cur_env ()) in try - tcresolve' [] glb 16 + tcresolve' [] glb 16; + debug (fun () -> "Solved to:\n\t" ^ term_to_string w) with | NoInst -> fail ("Could not solve constraint " ^ term_to_string (cur_goal ())) From 0bf2bc444c2a61691fc3f8f30197996bb87c6cb7 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Mon, 4 Dec 2023 15:25:00 -0800 Subject: [PATCH 22/29] nit: show instances --- src/typechecker/FStar.TypeChecker.Rel.fst | 7 +++++++ src/typechecker/FStar.TypeChecker.Rel.fsti | 4 ++++ 2 files changed, 11 insertions(+) diff --git a/src/typechecker/FStar.TypeChecker.Rel.fst b/src/typechecker/FStar.TypeChecker.Rel.fst index d62a69c399c..38d6065af87 100644 --- a/src/typechecker/FStar.TypeChecker.Rel.fst +++ b/src/typechecker/FStar.TypeChecker.Rel.fst @@ -50,6 +50,13 @@ module PC = FStar.Parser.Const module FC = FStar.Const module TcComm = FStar.TypeChecker.Common +instance showable_implicit_checking_status : showable implicit_checking_status = { + show = (function + | Implicit_unresolved -> "Implicit_unresolved" + | Implicit_checking_defers_univ_constraint -> "Implicit_checking_defers_univ_constraint" + | Implicit_has_typing_guard (tm, typ) -> "Implicit_has_typing_guard"); +} + let is_base_type env typ = let t = FStar.TypeChecker.Normalize.unfold_whnf env typ in let head, args = U.head_and_args t in diff --git a/src/typechecker/FStar.TypeChecker.Rel.fsti b/src/typechecker/FStar.TypeChecker.Rel.fsti index de236bd7813..0f6892faeb9 100644 --- a/src/typechecker/FStar.TypeChecker.Rel.fsti +++ b/src/typechecker/FStar.TypeChecker.Rel.fsti @@ -27,6 +27,8 @@ open FStar.TypeChecker.Env open FStar.Syntax.Syntax open FStar.TypeChecker.Common open FStar.Compiler.Range +open FStar.Class.Show + type match_result = | MisMatch of option delta_depth * option delta_depth | HeadMatch of bool // true iff the heads MAY match after further unification, false if already the same @@ -37,6 +39,8 @@ type implicit_checking_status = | Implicit_checking_defers_univ_constraint | Implicit_has_typing_guard of term * typ +instance val showable_implicit_checking_status : showable implicit_checking_status + type tagged_implicits = list (implicit * implicit_checking_status) val is_base_type : env -> typ -> bool From 84401cf3439e30e3063083c3b96139ee778d1b06 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Mon, 4 Dec 2023 17:08:09 -0800 Subject: [PATCH 23/29] Tc: Gen: don't fail due to unresolved non-Type implicits Leave that to the rest of the typechecker. --- .../FStar.TypeChecker.Generalize.fst | 60 ++++++++----------- 1 file changed, 26 insertions(+), 34 deletions(-) diff --git a/src/typechecker/FStar.TypeChecker.Generalize.fst b/src/typechecker/FStar.TypeChecker.Generalize.fst index 39aa8eda86c..8df35457372 100644 --- a/src/typechecker/FStar.TypeChecker.Generalize.fst +++ b/src/typechecker/FStar.TypeChecker.Generalize.fst @@ -182,17 +182,6 @@ let gen env (is_rec:bool) (lecs:list (lbname * term * comp)) : option (list (lbn let lecs = lec_hd :: lecs in let gen_types (uvs:list ctx_uvar) : list (bv * bqual) = - let fail (rng:Range.range) (k:typ) : unit = - let open FStar.Pprint in - let open FStar.Class.PP in - let lbname, e, c = lec_hd in - raise_error_doc (Errors.Fatal_FailToResolveImplicitArgument, [ - prefix 4 1 (text "Failed to resolve implicit argument of type") - (pp k) ^/^ - prefix 4 1 (group (text "in the type of" ^/^ squotes (doc_of_string (Print.lbname_to_string lbname)) ^^ colon)) - (pp (U.comp_result c)) - ]) rng - in uvs |> List.concatMap (fun u -> (* If this implicit has a meta, don't generalize it. Just leave it unresolved for the resolve_implicits phase to fill it in. *) @@ -203,30 +192,33 @@ let gen env (is_rec:bool) (lecs:list (lbname * term * comp)) : option (list (lbn | _ -> let k = N.normalize [Env.Beta; Env.Exclude Env.Zeta] env (U.ctx_uvar_typ u) in let bs, kres = U.arrow_formals k in - let _ = - //we only generalize variables at type k = a:Type{phi} - //where k is closed - //this is in support of ML-style polymorphism, while also allowing generalizing - //over things like eqtype, which is a common case - //Otherwise, things go badly wrong: see #1091 - match (U.unrefine (N.unfold_whnf env kres)).n with - | Tm_type _ -> - let free = FStar.Syntax.Free.names kres in - if not (BU.set_is_empty free) then fail u.ctx_uvar_range kres + //we only generalize variables at type k = a:Type{phi} + //where k is closed + //this is in support of ML-style polymorphism, while also allowing generalizing + //over things like eqtype, which is a common case + //Otherwise, things go badly wrong: see #1091 + match (U.unrefine (N.unfold_whnf env kres)).n with + | Tm_type _ -> + let free = FStar.Syntax.Free.names kres in + if not (BU.set_is_empty free) then + [] + else + let a = S.new_bv (Some <| Env.get_range env) kres in + let t = + match bs with + | [] -> S.bv_to_name a + | _ -> U.abs bs (S.bv_to_name a) (Some (U.residual_tot kres)) + in + U.set_uvar u.ctx_uvar_head t; + //t clearly has a free variable; this is the one place we break the + //invariant of a uvar always being resolved to a term well-typed in its given context + [a, S.as_bqual_implicit true] - | _ -> - fail u.ctx_uvar_range kres - in - let a = S.new_bv (Some <| Env.get_range env) kres in - let t = - match bs with - | [] -> S.bv_to_name a - | _ -> U.abs bs (S.bv_to_name a) (Some (U.residual_tot kres)) - in - U.set_uvar u.ctx_uvar_head t; - //t clearly has a free variable; this is the one place we break the - //invariant of a uvar always being resolved to a term well-typed in its given context - [a, S.as_bqual_implicit true]) + | _ -> + (* This uvar was not a type. Do not generalize it and + leave the rest of typechecker attempt solving it, or fail *) + [] + ) in let gen_univs = gen_univs env univs in From 92bc8c32b18a02034291be948ccda27d63dc34dc Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Mon, 4 Dec 2023 15:51:57 -0800 Subject: [PATCH 24/29] Tc: running meta args in uvar's env, not the original env We had previously made the choise to run meta argument tactics in the environment in which they were introduced, instead of the environment of the uvar that the meta is attached to. These two can differ if the uvar is unified with other uvars, possibly in more constrained environments. But, this leads to all sorts of weirdness, such as getting trying to solve a uvar in an environment that contains itself, if we have something like: let v : ty ?u1 = ... in let w : ty ?u2 = ... in (* something that unifies the type of v and w *) We may have set ?u2:=?u1 and copied the meta over, so when we try to run it to solve ?u1, we should not have ?u1 in scope. --- src/typechecker/FStar.TypeChecker.Rel.fst | 24 +++++++++++++---------- tests/bug-reports/Bug1918.fst | 8 +++++--- tests/typeclasses/Bug3130b.fst | 2 -- 3 files changed, 19 insertions(+), 15 deletions(-) diff --git a/src/typechecker/FStar.TypeChecker.Rel.fst b/src/typechecker/FStar.TypeChecker.Rel.fst index 38d6065af87..1ea084608c3 100644 --- a/src/typechecker/FStar.TypeChecker.Rel.fst +++ b/src/typechecker/FStar.TypeChecker.Rel.fst @@ -804,10 +804,6 @@ let flex_uvar_has_meta_tac u = | Some (Ctx_uvar_meta_tac _) -> true | _ -> false -let flex_uvar_meta_tac_env u : env_t = - match u.ctx_uvar_meta with - | Some (Ctx_uvar_meta_tac (denv, _)) -> Dyn.undyn denv - let flex_t_to_string (Flex (_, c, args)) = BU.format2 "%s [%s]" (show c) (Print.args_to_string args) @@ -1852,6 +1848,7 @@ let run_meta_arg_tac (ctx_u:ctx_uvar) : term = match ctx_u.ctx_uvar_meta with | Some (Ctx_uvar_meta_tac (env_dyn, tau)) -> let env : Env.env = FStar.Compiler.Dyn.undyn env_dyn in + let env = { env with gamma = ctx_u.ctx_uvar_gamma } in if Env.debug env (Options.Other "Tac") then BU.print1 "Running tactic for meta-arg %s\n" (show ctx_u); Errors.with_ctx "Running tactic for meta-arg" @@ -2118,9 +2115,14 @@ let lazy_complete_repr (k:lazy_kind) : bool = let has_free_uvars (t:term) : bool = not (BU.set_is_empty (Free.uvars_uncached t)) + let env_has_free_uvars (e:env_t) : bool = List.existsb (fun b -> has_free_uvars b.binder_bv.sort) (Env.all_binders e) +let gamma_has_free_uvars (g:list binding) : bool = + List.existsb (function Binding_var bv -> has_free_uvars bv.sort + | _ -> false) g + (******************************************************************************************************) (* Main solving algorithm begins here *) (******************************************************************************************************) @@ -3264,7 +3266,7 @@ and solve_t_flex_flex env orig wl (lhs:flex_t) (rhs:flex_t) : solution = let uv = flex_uvar flex in flex_uvar_has_meta_tac uv && not (has_free_uvars (U.ctx_uvar_typ uv)) && - not (env_has_free_uvars (flex_uvar_meta_tac_env uv)) + not (gamma_has_free_uvars uv.ctx_uvar_gamma) in let run_meta_arg_tac_and_try_again (flex:flex_t) = @@ -5496,13 +5498,15 @@ let resolve_implicits' env is_tac is_gen (implicits:Env.implicits) | _ when unresolved ctx_u && flex_uvar_has_meta_tac ctx_u -> let Some (Ctx_uvar_meta_tac meta) = ctx_u.ctx_uvar_meta in - let m_env : env_t = Dyn.undyn (fst meta) in + let env = { env with gamma = ctx_u.ctx_uvar_gamma } in let tac = snd meta in let typ = U.ctx_uvar_typ ctx_u in - if has_free_uvars typ || env_has_free_uvars m_env then ( + if (has_free_uvars typ || gamma_has_free_uvars ctx_u.ctx_uvar_gamma) + && Options.ext_getv "compat:open_metas" = "" then // i.e. compat option unset + ( (* If the result type or env for this meta arg has a free uvar, delay it. Some other meta arg being solved may instantiate the uvar. See #3130. *) - if Env.debug env <| Options.Other "Rel" then + if Env.debug env <| Options.Other "Rel" || Env.debug env <| Options.Other "Imps" then BU.print1 "Deferring implicit due to open ctx/typ %s\n" (show ctx_u); until_fixpoint ((hd, Implicit_unresolved)::out, changed) tl ) else ( @@ -5515,11 +5519,11 @@ let resolve_implicits' env is_tac is_gen (implicits:Env.implicits) until_fixpoint (out, true) (extra @ tl) in if cacheable tac then - match meta_arg_cache_lookup tac m_env typ with + match meta_arg_cache_lookup tac env typ with | Some res -> solve_with res | None -> let t = run_meta_arg_tac ctx_u in - meta_arg_cache_result tac m_env typ t; + meta_arg_cache_result tac env typ t; solve_with t else let t = run_meta_arg_tac ctx_u in diff --git a/tests/bug-reports/Bug1918.fst b/tests/bug-reports/Bug1918.fst index e6674259920..f9761a2de42 100644 --- a/tests/bug-reports/Bug1918.fst +++ b/tests/bug-reports/Bug1918.fst @@ -1,9 +1,11 @@ module Bug1918 class mon = { - t : Type; + t : Type0; comp : t -> t -> t; } -[@@expect_failure [66]] -let (++) (a:_) (b:_) = comp a b +let comp1 (_:mon) (x:t) (y:t) : t = comp x y + +[@@expect_failure [228]] +let comp2 (x:t) (y:t) : t = comp x y diff --git a/tests/typeclasses/Bug3130b.fst b/tests/typeclasses/Bug3130b.fst index 0eb3f0bc474..59102ad3626 100644 --- a/tests/typeclasses/Bug3130b.fst +++ b/tests/typeclasses/Bug3130b.fst @@ -21,7 +21,5 @@ let test7 () = let p : Type0 = mk6 == mk5 in () (* These are ambiguous. They used to work when we ran meta args in contexts with yet-unresolved uvars, but that is now forbidden. *) -[@@expect_failure [66]] let test8 (x:_) = let p : Type0 = mk5 == x /\ x == mk6 in () -[@@expect_failure [66]] let test9 (x:_) = let p : Type0 = mk6 == x /\ x == mk5 in () From e01a065c8b6028b0210abaf39663dbb60c4830d7 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Tue, 5 Dec 2023 03:16:19 -0800 Subject: [PATCH 25/29] Update tests + expected output --- tests/error-messages/Bug1918.fst | 11 +++++++++++ tests/error-messages/Bug1918.fst.expected | 14 ++++++++++++++ tests/error-messages/Bug2010.fst.expected | 5 +++-- tests/error-messages/Bug2021.fst.expected | 12 ++++++------ .../NegativeTests.ZZImplicitFalse.fst.expected | 2 +- tests/typeclasses/Bug3130b.fst | 4 ++-- 6 files changed, 37 insertions(+), 11 deletions(-) create mode 100644 tests/error-messages/Bug1918.fst create mode 100644 tests/error-messages/Bug1918.fst.expected diff --git a/tests/error-messages/Bug1918.fst b/tests/error-messages/Bug1918.fst new file mode 100644 index 00000000000..f9761a2de42 --- /dev/null +++ b/tests/error-messages/Bug1918.fst @@ -0,0 +1,11 @@ +module Bug1918 + +class mon = { + t : Type0; + comp : t -> t -> t; +} + +let comp1 (_:mon) (x:t) (y:t) : t = comp x y + +[@@expect_failure [228]] +let comp2 (x:t) (y:t) : t = comp x y diff --git a/tests/error-messages/Bug1918.fst.expected b/tests/error-messages/Bug1918.fst.expected new file mode 100644 index 00000000000..ac10422a473 --- /dev/null +++ b/tests/error-messages/Bug1918.fst.expected @@ -0,0 +1,14 @@ +proof-state: State dump @ depth 0 (at the time of failure): +Location: FStar.Tactics.Typeclasses.fst(178,6-178,73) +Goal 1/1: + |- _ : Bug1918.mon + +>> Got issues: [ +* Error 228 at Bug1918.fst(11,13-11,14): + - Tactic failed + - "Could not solve constraint Bug1918.mon" + - See also FStar.Tactics.Typeclasses.fst(178,6-178,73) + +>>] +Verified module: Bug1918 +All verification conditions discharged successfully diff --git a/tests/error-messages/Bug2010.fst.expected b/tests/error-messages/Bug2010.fst.expected index edb02ce2e02..87b5303ebd8 100644 --- a/tests/error-messages/Bug2010.fst.expected +++ b/tests/error-messages/Bug2010.fst.expected @@ -1,7 +1,8 @@ >> Got issues: [ * Error 66 at Bug2010.fst(6,66-6,67): - - Failed to resolve implicit argument of type 'Prims.nat' in the type of concat' (s1: FStar.Seq.Properties.lseq 'a l1 -> s2: FStar.Seq.Properties.lseq 'a l2 - -> FStar.Seq.Properties.lseq 'a (*?u14*) _) + - Failed to resolve implicit argument ?14 + of type Prims.nat + introduced for user-provided implicit term at Bug2010.fst(6,66-6,67) >>] Verified module: Bug2010 diff --git a/tests/error-messages/Bug2021.fst.expected b/tests/error-messages/Bug2021.fst.expected index 646b413f0a6..41aadd84b21 100644 --- a/tests/error-messages/Bug2021.fst.expected +++ b/tests/error-messages/Bug2021.fst.expected @@ -1,27 +1,27 @@ >> Got issues: [ * Error 66 at Bug2021.fst(5,15-5,16): - - Failed to resolved implicit argument ?2 + - Failed to resolve implicit argument ?2 of type Type introduced for user-provided implicit term at Bug2021.fst(5,15-5,16) >>] >> Got issues: [ * Error 66 at Bug2021.fst(10,8-10,9): - - Failed to resolved implicit argument ?2 + - Failed to resolve implicit argument ?2 of type Type introduced for user-provided implicit term at Bug2021.fst(10,8-10,9) >>] >> Got issues: [ * Error 66 at Bug2021.fst(16,12-16,13): - - Failed to resolved implicit argument ?5 + - Failed to resolve implicit argument ?5 of type Type introduced for user-provided implicit term at Bug2021.fst(16,12-16,13) >>] >> Got issues: [ * Error 66 at Bug2021.fst(24,13-24,14): - - Failed to resolved implicit argument ?9 + - Failed to resolve implicit argument ?9 of type Prims.int introduced for Instantiating implicit argument in application - See also Bug2021.fst(23,11-23,12) @@ -29,7 +29,7 @@ >>] >> Got issues: [ * Error 66 at Bug2021.fst(30,13-30,17): - - Failed to resolved implicit argument ?10 + - Failed to resolve implicit argument ?10 of type Prims.int introduced for Instantiating implicit argument in application - See also Bug2021.fst(29,11-29,12) @@ -37,7 +37,7 @@ >>] >> Got issues: [ * Error 66 at Bug2021.fst(37,13-37,14): - - Failed to resolved implicit argument ?11 + - Failed to resolve implicit argument ?11 of type Prims.int introduced for Instantiating implicit argument in application - See also Bug2021.fst(36,11-36,12) diff --git a/tests/error-messages/NegativeTests.ZZImplicitFalse.fst.expected b/tests/error-messages/NegativeTests.ZZImplicitFalse.fst.expected index 4df957a336b..3da6991f744 100644 --- a/tests/error-messages/NegativeTests.ZZImplicitFalse.fst.expected +++ b/tests/error-messages/NegativeTests.ZZImplicitFalse.fst.expected @@ -1,6 +1,6 @@ >> Got issues: [ * Error 66 at NegativeTests.ZZImplicitFalse.fst(20,26-20,27): - - Failed to resolved implicit argument ?1 + - Failed to resolve implicit argument ?1 of type Prims.l_False introduced for user-provided implicit term at diff --git a/tests/typeclasses/Bug3130b.fst b/tests/typeclasses/Bug3130b.fst index 59102ad3626..1683ea79ac8 100644 --- a/tests/typeclasses/Bug3130b.fst +++ b/tests/typeclasses/Bug3130b.fst @@ -19,7 +19,7 @@ let test5 (y : it 6) = let p : Type0 = y == mk6 in () let test6 () = let p : Type0 = mk5 == mk6 in () let test7 () = let p : Type0 = mk6 == mk5 in () -(* These are ambiguous. They used to work when we ran meta args in -contexts with yet-unresolved uvars, but that is now forbidden. *) +(* These are ambiguous, but they work. Wouldn't be a big deal if they +regress though. *) let test8 (x:_) = let p : Type0 = mk5 == x /\ x == mk6 in () let test9 (x:_) = let p : Type0 = mk6 == x /\ x == mk5 in () From b1024b83c581f6067f56de9efc2a0f982a4bd6ae Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Tue, 5 Dec 2023 03:23:55 -0800 Subject: [PATCH 26/29] snap --- .../fstar-lib/generated/FStar_Syntax_Print.ml | 23 +- .../generated/FStar_Tactics_Typeclasses.ml | 658 ++++++++++-------- .../generated/FStar_Tactics_V1_Basic.ml | 4 +- .../generated/FStar_Tactics_V2_Basic.ml | 4 +- .../generated/FStar_TypeChecker_Common.ml | 22 +- .../generated/FStar_TypeChecker_Env.ml | 27 - .../generated/FStar_TypeChecker_Generalize.ml | 156 ++--- .../generated/FStar_TypeChecker_Rel.ml | 312 ++++++++- 8 files changed, 744 insertions(+), 462 deletions(-) diff --git a/ocaml/fstar-lib/generated/FStar_Syntax_Print.ml b/ocaml/fstar-lib/generated/FStar_Syntax_Print.ml index f137c021750..6d5d6e7dc15 100644 --- a/ocaml/fstar-lib/generated/FStar_Syntax_Print.ml +++ b/ocaml/fstar-lib/generated/FStar_Syntax_Print.ml @@ -2039,4 +2039,25 @@ let (showable_binder : FStar_Syntax_Syntax.binder FStar_Class_Show.showable) let (showable_uvar : FStar_Syntax_Syntax.uvar FStar_Class_Show.showable) = { FStar_Class_Show.show = uvar_to_string } let (showable_ctxu : FStar_Syntax_Syntax.ctx_uvar FStar_Class_Show.showable) - = { FStar_Class_Show.show = ctx_uvar_to_string } \ No newline at end of file + = { FStar_Class_Show.show = ctx_uvar_to_string } +let (showable_binding : + FStar_Syntax_Syntax.binding FStar_Class_Show.showable) = + { + FStar_Class_Show.show = + (fun uu___ -> + match uu___ with + | FStar_Syntax_Syntax.Binding_var x -> + let uu___1 = FStar_Class_Show.show showable_bv x in + Prims.op_Hat "Binding_var " uu___1 + | FStar_Syntax_Syntax.Binding_lid x -> + let uu___1 = + FStar_Class_Show.show + (FStar_Class_Show.show_tuple2 FStar_Ident.showable_lident + (FStar_Class_Show.show_tuple2 + (FStar_Class_Show.show_list FStar_Ident.showable_ident) + showable_term)) x in + Prims.op_Hat "Binding_lid " uu___1 + | FStar_Syntax_Syntax.Binding_univ x -> + let uu___1 = FStar_Class_Show.show FStar_Ident.showable_ident x in + Prims.op_Hat "Binding_univ " uu___1) + } \ No newline at end of file diff --git a/ocaml/fstar-lib/generated/FStar_Tactics_Typeclasses.ml b/ocaml/fstar-lib/generated/FStar_Tactics_Typeclasses.ml index 915071f6d58..5e90923f9fc 100644 --- a/ocaml/fstar-lib/generated/FStar_Tactics_Typeclasses.ml +++ b/ocaml/fstar-lib/generated/FStar_Tactics_Typeclasses.ml @@ -952,7 +952,7 @@ let (tcresolve : unit -> (unit, unit) FStar_Tactics_Effect.tac_repr) = (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (166)) (Prims.of_int (4)) (Prims.of_int (179)) + (Prims.of_int (161)) (Prims.of_int (55)) (Prims.of_int (181)) (Prims.of_int (18))))) (Obj.magic (debug @@ -979,128 +979,208 @@ let (tcresolve : unit -> (unit, unit) FStar_Tactics_Effect.tac_repr) = (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (166)) (Prims.of_int (4)) - (Prims.of_int (166)) (Prims.of_int (19))))) + (Prims.of_int (166)) (Prims.of_int (12)) + (Prims.of_int (166)) (Prims.of_int (26))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (166)) (Prims.of_int (20)) - (Prims.of_int (179)) (Prims.of_int (18))))) - (Obj.magic (maybe_intros ())) + (Prims.of_int (167)) (Prims.of_int (4)) + (Prims.of_int (181)) (Prims.of_int (18))))) + (Obj.magic (FStar_Tactics_V2_Derived.cur_witness ())) (fun uu___2 -> - (fun uu___2 -> + (fun w -> Obj.magic (FStar_Tactics_Effect.tac_bind (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (171)) (Prims.of_int (14)) - (Prims.of_int (171)) (Prims.of_int (52))))) + (Prims.of_int (167)) (Prims.of_int (4)) + (Prims.of_int (167)) (Prims.of_int (19))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (172)) (Prims.of_int (4)) - (Prims.of_int (179)) (Prims.of_int (18))))) - (Obj.magic - (FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (171)) - (Prims.of_int (40)) - (Prims.of_int (171)) - (Prims.of_int (52))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (171)) - (Prims.of_int (14)) - (Prims.of_int (171)) - (Prims.of_int (52))))) - (Obj.magic - (FStar_Tactics_V2_Derived.cur_env ())) - (fun uu___3 -> - FStar_Tactics_Effect.lift_div_tac - (fun uu___4 -> - FStar_Reflection_V2_Builtins.lookup_attr - (FStar_Reflection_V2_Builtins.pack_ln - (FStar_Reflection_V2_Data.Tv_FVar - (FStar_Reflection_V2_Builtins.pack_fv - ["FStar"; - "Tactics"; - "Typeclasses"; - "tcinstance"]))) uu___3)))) - (fun uu___3 -> - (fun glb -> + (Prims.of_int (167)) (Prims.of_int (20)) + (Prims.of_int (181)) (Prims.of_int (18))))) + (Obj.magic (maybe_intros ())) + (fun uu___2 -> + (fun uu___2 -> Obj.magic - (FStar_Tactics_V2_Derived.try_with - (fun uu___3 -> - match () with - | () -> - tcresolve' [] glb - (Prims.of_int (16))) + (FStar_Tactics_Effect.tac_bind + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "FStar.Tactics.Typeclasses.fst" + (Prims.of_int (172)) + (Prims.of_int (14)) + (Prims.of_int (172)) + (Prims.of_int (52))))) + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "FStar.Tactics.Typeclasses.fst" + (Prims.of_int (173)) + (Prims.of_int (4)) + (Prims.of_int (181)) + (Prims.of_int (18))))) + (Obj.magic + (FStar_Tactics_Effect.tac_bind + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "FStar.Tactics.Typeclasses.fst" + (Prims.of_int (172)) + (Prims.of_int (40)) + (Prims.of_int (172)) + (Prims.of_int (52))))) + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "FStar.Tactics.Typeclasses.fst" + (Prims.of_int (172)) + (Prims.of_int (14)) + (Prims.of_int (172)) + (Prims.of_int (52))))) + (Obj.magic + (FStar_Tactics_V2_Derived.cur_env + ())) + (fun uu___3 -> + FStar_Tactics_Effect.lift_div_tac + (fun uu___4 -> + FStar_Reflection_V2_Builtins.lookup_attr + (FStar_Reflection_V2_Builtins.pack_ln + (FStar_Reflection_V2_Data.Tv_FVar + (FStar_Reflection_V2_Builtins.pack_fv + ["FStar"; + "Tactics"; + "Typeclasses"; + "tcinstance"]))) + uu___3)))) (fun uu___3 -> - (fun uu___3 -> - match uu___3 with - | NoInst -> - Obj.magic - (Obj.repr - (FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (176)) - (Prims.of_int (11)) - (Prims.of_int (176)) - (Prims.of_int (73))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (176)) - (Prims.of_int (6)) - (Prims.of_int (176)) - (Prims.of_int (73))))) - (Obj.magic - (FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic + (fun glb -> + Obj.magic + (FStar_Tactics_V2_Derived.try_with + (fun uu___3 -> + match () with + | () -> + FStar_Tactics_Effect.tac_bind + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "FStar.Tactics.Typeclasses.fst" + (Prims.of_int (174)) + (Prims.of_int (6)) + (Prims.of_int (174)) + (Prims.of_int (26))))) + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "FStar.Tactics.Typeclasses.fst" + (Prims.of_int (175)) + (Prims.of_int (6)) + (Prims.of_int (175)) + (Prims.of_int (59))))) + (Obj.magic + (tcresolve' [] + glb + (Prims.of_int (16)))) + (fun uu___4 -> + (fun uu___4 -> + Obj.magic + (debug + (fun + uu___5 -> + FStar_Tactics_Effect.tac_bind + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "FStar.Tactics.Typeclasses.fst" + (Prims.of_int (175)) + (Prims.of_int (42)) + (Prims.of_int (175)) + (Prims.of_int (58))))) + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "prims.fst" + (Prims.of_int (590)) + (Prims.of_int (19)) + (Prims.of_int (590)) + (Prims.of_int (31))))) + (Obj.magic + (FStar_Tactics_V2_Builtins.term_to_string + w)) + (fun + uu___6 -> + FStar_Tactics_Effect.lift_div_tac + (fun + uu___7 -> + Prims.strcat + "Solved to:\n\t" + uu___6))))) + uu___4)) + (fun uu___3 -> + (fun uu___3 -> + match uu___3 with + | NoInst -> + Obj.magic + (Obj.repr + (FStar_Tactics_Effect.tac_bind + ( + FStar_Sealed.seal + (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (176)) + (Prims.of_int (178)) + (Prims.of_int (11)) + (Prims.of_int (178)) + (Prims.of_int (73))))) + ( + FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "FStar.Tactics.Typeclasses.fst" + (Prims.of_int (178)) + (Prims.of_int (6)) + (Prims.of_int (178)) + (Prims.of_int (73))))) + ( + Obj.magic + (FStar_Tactics_Effect.tac_bind + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "FStar.Tactics.Typeclasses.fst" + (Prims.of_int (178)) (Prims.of_int (44)) - (Prims.of_int (176)) + (Prims.of_int (178)) (Prims.of_int (72))))) - (FStar_Sealed.seal - (Obj.magic + (FStar_Sealed.seal + (Obj.magic (FStar_Range.mk_range "prims.fst" (Prims.of_int (590)) (Prims.of_int (19)) (Prims.of_int (590)) (Prims.of_int (31))))) - (Obj.magic - (FStar_Tactics_Effect.tac_bind + (Obj.magic + (FStar_Tactics_Effect.tac_bind (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (176)) + (Prims.of_int (178)) (Prims.of_int (59)) - (Prims.of_int (176)) + (Prims.of_int (178)) (Prims.of_int (72))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (176)) + (Prims.of_int (178)) (Prims.of_int (44)) - (Prims.of_int (176)) + (Prims.of_int (178)) (Prims.of_int (72))))) (Obj.magic (FStar_Tactics_V2_Derived.cur_goal @@ -1113,31 +1193,35 @@ let (tcresolve : unit -> (unit, unit) FStar_Tactics_Effect.tac_repr) = (FStar_Tactics_V2_Builtins.term_to_string uu___4)) uu___4))) - (fun uu___4 -> - FStar_Tactics_Effect.lift_div_tac - ( - fun + (fun + uu___4 -> + FStar_Tactics_Effect.lift_div_tac + (fun uu___5 -> Prims.strcat "Could not solve constraint " uu___4)))) - (fun uu___4 -> - FStar_Tactics_V2_Derived.fail - uu___4))) - | FStar_Tactics_Common.TacticFailure - s -> - Obj.magic - (Obj.repr - (FStar_Tactics_V2_Derived.fail - (Prims.strcat - "Typeclass resolution failed: " - s))) - | e -> - Obj.magic - (Obj.repr - (FStar_Tactics_Effect.raise - e))) uu___3))) - uu___3))) uu___2))) uu___1) + ( + fun + uu___4 -> + FStar_Tactics_V2_Derived.fail + uu___4))) + | FStar_Tactics_Common.TacticFailure + s -> + Obj.magic + (Obj.repr + (FStar_Tactics_V2_Derived.fail + ( + Prims.strcat + "Typeclass resolution failed: " + s))) + | e -> + Obj.magic + (Obj.repr + (FStar_Tactics_Effect.raise + e))) + uu___3))) uu___3))) + uu___2))) uu___2))) uu___1) let _ = FStar_Tactics_Native.register_tactic "FStar.Tactics.Typeclasses.tcresolve" (Prims.of_int (2)) @@ -1171,8 +1255,8 @@ let rec (mk_abs : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (188)) (Prims.of_int (20)) - (Prims.of_int (188)) (Prims.of_int (47))))) + (Prims.of_int (190)) (Prims.of_int (20)) + (Prims.of_int (190)) (Prims.of_int (47))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "dummy" Prims.int_zero @@ -1183,17 +1267,17 @@ let rec (mk_abs : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (188)) + (Prims.of_int (190)) (Prims.of_int (30)) - (Prims.of_int (188)) + (Prims.of_int (190)) (Prims.of_int (46))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (188)) + (Prims.of_int (190)) (Prims.of_int (20)) - (Prims.of_int (188)) + (Prims.of_int (190)) (Prims.of_int (47))))) (Obj.magic (mk_abs bs1 body)) (fun uu___ -> @@ -1255,12 +1339,12 @@ let (mk_class : (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (221)) (Prims.of_int (13)) (Prims.of_int (221)) + (Prims.of_int (223)) (Prims.of_int (13)) (Prims.of_int (223)) (Prims.of_int (26))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (221)) (Prims.of_int (29)) (Prims.of_int (309)) + (Prims.of_int (223)) (Prims.of_int (29)) (Prims.of_int (311)) (Prims.of_int (35))))) (FStar_Tactics_Effect.lift_div_tac (fun uu___ -> FStar_Reflection_V2_Builtins.explode_qn nm)) @@ -1271,27 +1355,27 @@ let (mk_class : (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (222)) (Prims.of_int (12)) - (Prims.of_int (222)) (Prims.of_int (38))))) + (Prims.of_int (224)) (Prims.of_int (12)) + (Prims.of_int (224)) (Prims.of_int (38))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (223)) (Prims.of_int (4)) - (Prims.of_int (309)) (Prims.of_int (35))))) + (Prims.of_int (225)) (Prims.of_int (4)) + (Prims.of_int (311)) (Prims.of_int (35))))) (Obj.magic (FStar_Tactics_Effect.tac_bind (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (222)) (Prims.of_int (23)) - (Prims.of_int (222)) (Prims.of_int (35))))) + (Prims.of_int (224)) (Prims.of_int (23)) + (Prims.of_int (224)) (Prims.of_int (35))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (222)) (Prims.of_int (12)) - (Prims.of_int (222)) (Prims.of_int (38))))) + (Prims.of_int (224)) (Prims.of_int (12)) + (Prims.of_int (224)) (Prims.of_int (38))))) (Obj.magic (FStar_Tactics_V2_Builtins.top_env ())) (fun uu___ -> FStar_Tactics_Effect.lift_div_tac @@ -1306,14 +1390,14 @@ let (mk_class : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (223)) (Prims.of_int (4)) - (Prims.of_int (223)) (Prims.of_int (19))))) + (Prims.of_int (225)) (Prims.of_int (4)) + (Prims.of_int (225)) (Prims.of_int (19))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (223)) (Prims.of_int (20)) - (Prims.of_int (309)) (Prims.of_int (35))))) + (Prims.of_int (225)) (Prims.of_int (20)) + (Prims.of_int (311)) (Prims.of_int (35))))) (Obj.magic (FStar_Tactics_V2_Derived.guard (FStar_Pervasives_Native.uu___is_Some r))) @@ -1325,17 +1409,17 @@ let (mk_class : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (224)) + (Prims.of_int (226)) (Prims.of_int (18)) - (Prims.of_int (224)) + (Prims.of_int (226)) (Prims.of_int (19))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (223)) + (Prims.of_int (225)) (Prims.of_int (20)) - (Prims.of_int (309)) + (Prims.of_int (311)) (Prims.of_int (35))))) (FStar_Tactics_Effect.lift_div_tac (fun uu___1 -> r)) @@ -1350,17 +1434,17 @@ let (mk_class : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (225)) + (Prims.of_int (227)) (Prims.of_int (23)) - (Prims.of_int (225)) + (Prims.of_int (227)) (Prims.of_int (115))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (225)) + (Prims.of_int (227)) (Prims.of_int (118)) - (Prims.of_int (309)) + (Prims.of_int (311)) (Prims.of_int (35))))) (FStar_Tactics_Effect.lift_div_tac (fun uu___2 -> @@ -1385,18 +1469,18 @@ let (mk_class : Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (226)) + (Prims.of_int (228)) (Prims.of_int (13)) - (Prims.of_int (226)) + (Prims.of_int (228)) (Prims.of_int (30))))) (FStar_Sealed.seal ( Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (227)) + (Prims.of_int (229)) (Prims.of_int (4)) - (Prims.of_int (309)) + (Prims.of_int (311)) (Prims.of_int (35))))) (Obj.magic ( @@ -1412,17 +1496,17 @@ let (mk_class : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (227)) + (Prims.of_int (229)) (Prims.of_int (4)) - (Prims.of_int (227)) + (Prims.of_int (229)) (Prims.of_int (28))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (227)) + (Prims.of_int (229)) (Prims.of_int (29)) - (Prims.of_int (309)) + (Prims.of_int (311)) (Prims.of_int (35))))) (Obj.magic (FStar_Tactics_V2_Derived.guard @@ -1438,17 +1522,17 @@ let (mk_class : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (228)) + (Prims.of_int (230)) (Prims.of_int (63)) - (Prims.of_int (228)) + (Prims.of_int (230)) (Prims.of_int (65))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (227)) + (Prims.of_int (229)) (Prims.of_int (29)) - (Prims.of_int (309)) + (Prims.of_int (311)) (Prims.of_int (35))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -1480,17 +1564,17 @@ let (mk_class : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (232)) + (Prims.of_int (234)) (Prims.of_int (20)) - (Prims.of_int (232)) + (Prims.of_int (234)) (Prims.of_int (29))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (234)) + (Prims.of_int (236)) (Prims.of_int (4)) - (Prims.of_int (309)) + (Prims.of_int (311)) (Prims.of_int (35))))) (Obj.magic (last @@ -1506,17 +1590,17 @@ let (mk_class : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (234)) + (Prims.of_int (236)) (Prims.of_int (4)) - (Prims.of_int (234)) + (Prims.of_int (236)) (Prims.of_int (30))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (234)) + (Prims.of_int (236)) (Prims.of_int (31)) - (Prims.of_int (309)) + (Prims.of_int (311)) (Prims.of_int (35))))) (Obj.magic (FStar_Tactics_V2_Derived.guard @@ -1533,17 +1617,17 @@ let (mk_class : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (235)) + (Prims.of_int (237)) (Prims.of_int (25)) - (Prims.of_int (235)) + (Prims.of_int (237)) (Prims.of_int (30))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (234)) + (Prims.of_int (236)) (Prims.of_int (31)) - (Prims.of_int (309)) + (Prims.of_int (311)) (Prims.of_int (35))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -1565,17 +1649,17 @@ let (mk_class : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (237)) + (Prims.of_int (239)) (Prims.of_int (18)) - (Prims.of_int (237)) + (Prims.of_int (239)) (Prims.of_int (35))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (235)) + (Prims.of_int (237)) (Prims.of_int (33)) - (Prims.of_int (309)) + (Prims.of_int (311)) (Prims.of_int (35))))) (Obj.magic (FStar_Tactics_V2_SyntaxHelpers.collect_arr_bs @@ -1595,17 +1679,17 @@ let (mk_class : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (238)) + (Prims.of_int (240)) (Prims.of_int (12)) - (Prims.of_int (238)) + (Prims.of_int (240)) (Prims.of_int (28))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (239)) + (Prims.of_int (241)) (Prims.of_int (4)) - (Prims.of_int (309)) + (Prims.of_int (311)) (Prims.of_int (35))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -1622,17 +1706,17 @@ let (mk_class : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (239)) + (Prims.of_int (241)) (Prims.of_int (4)) - (Prims.of_int (239)) + (Prims.of_int (241)) (Prims.of_int (22))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (239)) + (Prims.of_int (241)) (Prims.of_int (23)) - (Prims.of_int (309)) + (Prims.of_int (311)) (Prims.of_int (35))))) (Obj.magic (FStar_Tactics_V2_Derived.guard @@ -1648,17 +1732,17 @@ let (mk_class : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (240)) + (Prims.of_int (242)) (Prims.of_int (22)) - (Prims.of_int (240)) + (Prims.of_int (242)) (Prims.of_int (23))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (239)) + (Prims.of_int (241)) (Prims.of_int (23)) - (Prims.of_int (309)) + (Prims.of_int (311)) (Prims.of_int (35))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -1679,17 +1763,17 @@ let (mk_class : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (249)) + (Prims.of_int (251)) (Prims.of_int (24)) - (Prims.of_int (249)) + (Prims.of_int (251)) (Prims.of_int (61))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (252)) + (Prims.of_int (254)) (Prims.of_int (4)) - (Prims.of_int (309)) + (Prims.of_int (311)) (Prims.of_int (35))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -1711,17 +1795,17 @@ let (mk_class : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (253)) + (Prims.of_int (255)) (Prims.of_int (26)) - (Prims.of_int (253)) + (Prims.of_int (255)) (Prims.of_int (42))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (253)) + (Prims.of_int (255)) (Prims.of_int (45)) - (Prims.of_int (308)) + (Prims.of_int (310)) (Prims.of_int (20))))) (Obj.magic (FStar_Tactics_V2_Derived.name_of_binder @@ -1735,17 +1819,17 @@ let (mk_class : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (254)) + (Prims.of_int (256)) (Prims.of_int (27)) - (Prims.of_int (254)) + (Prims.of_int (256)) (Prims.of_int (40))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (254)) + (Prims.of_int (256)) (Prims.of_int (43)) - (Prims.of_int (308)) + (Prims.of_int (310)) (Prims.of_int (20))))) (Obj.magic (FStar_Tactics_V2_Derived.cur_module @@ -1760,17 +1844,17 @@ let (mk_class : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (255)) + (Prims.of_int (257)) (Prims.of_int (28)) - (Prims.of_int (255)) + (Prims.of_int (257)) (Prims.of_int (46))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (255)) + (Prims.of_int (257)) (Prims.of_int (49)) - (Prims.of_int (308)) + (Prims.of_int (310)) (Prims.of_int (20))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -1789,17 +1873,17 @@ let (mk_class : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (256)) + (Prims.of_int (258)) (Prims.of_int (28)) - (Prims.of_int (256)) + (Prims.of_int (258)) (Prims.of_int (50))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (256)) + (Prims.of_int (258)) (Prims.of_int (53)) - (Prims.of_int (308)) + (Prims.of_int (310)) (Prims.of_int (20))))) (Obj.magic (FStar_Tactics_V2_Derived.fresh_namedv_named @@ -1814,17 +1898,17 @@ let (mk_class : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (257)) + (Prims.of_int (259)) (Prims.of_int (28)) - (Prims.of_int (257)) + (Prims.of_int (259)) (Prims.of_int (40))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (257)) + (Prims.of_int (259)) (Prims.of_int (43)) - (Prims.of_int (308)) + (Prims.of_int (310)) (Prims.of_int (20))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -1846,17 +1930,17 @@ let (mk_class : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (259)) + (Prims.of_int (261)) (Prims.of_int (20)) - (Prims.of_int (263)) + (Prims.of_int (265)) (Prims.of_int (32))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (264)) + (Prims.of_int (266)) (Prims.of_int (22)) - (Prims.of_int (308)) + (Prims.of_int (310)) (Prims.of_int (20))))) (Obj.magic (FStar_Tactics_Effect.tac_bind @@ -1864,17 +1948,17 @@ let (mk_class : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (261)) + (Prims.of_int (263)) (Prims.of_int (29)) - (Prims.of_int (261)) + (Prims.of_int (263)) (Prims.of_int (36))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (259)) + (Prims.of_int (261)) (Prims.of_int (20)) - (Prims.of_int (263)) + (Prims.of_int (265)) (Prims.of_int (32))))) (Obj.magic (FStar_Tactics_V2_Builtins.fresh @@ -1911,17 +1995,17 @@ let (mk_class : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (265)) + (Prims.of_int (267)) (Prims.of_int (34)) - (Prims.of_int (265)) + (Prims.of_int (267)) (Prims.of_int (60))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (265)) + (Prims.of_int (267)) (Prims.of_int (63)) - (Prims.of_int (308)) + (Prims.of_int (310)) (Prims.of_int (20))))) (Obj.magic (FStar_Tactics_Effect.tac_bind @@ -1929,17 +2013,17 @@ let (mk_class : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (265)) + (Prims.of_int (267)) (Prims.of_int (34)) - (Prims.of_int (265)) + (Prims.of_int (267)) (Prims.of_int (47))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (265)) + (Prims.of_int (267)) (Prims.of_int (34)) - (Prims.of_int (265)) + (Prims.of_int (267)) (Prims.of_int (60))))) (Obj.magic (FStar_Tactics_V2_Derived.cur_module @@ -1966,17 +2050,17 @@ let (mk_class : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (266)) + (Prims.of_int (268)) (Prims.of_int (29)) - (Prims.of_int (266)) + (Prims.of_int (268)) (Prims.of_int (63))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (266)) + (Prims.of_int (268)) (Prims.of_int (66)) - (Prims.of_int (308)) + (Prims.of_int (310)) (Prims.of_int (20))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -1995,17 +2079,17 @@ let (mk_class : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (269)) + (Prims.of_int (271)) (Prims.of_int (20)) - (Prims.of_int (274)) + (Prims.of_int (276)) (Prims.of_int (62))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (275)) + (Prims.of_int (277)) (Prims.of_int (20)) - (Prims.of_int (308)) + (Prims.of_int (310)) (Prims.of_int (20))))) (Obj.magic (FStar_Tactics_Effect.tac_bind @@ -2013,17 +2097,17 @@ let (mk_class : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (269)) + (Prims.of_int (271)) (Prims.of_int (26)) - (Prims.of_int (269)) + (Prims.of_int (271)) (Prims.of_int (59))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (269)) + (Prims.of_int (271)) (Prims.of_int (20)) - (Prims.of_int (274)) + (Prims.of_int (276)) (Prims.of_int (62))))) (Obj.magic (FStar_Tactics_Effect.tac_bind @@ -2031,17 +2115,17 @@ let (mk_class : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (269)) + (Prims.of_int (271)) (Prims.of_int (37)) - (Prims.of_int (269)) + (Prims.of_int (271)) (Prims.of_int (49))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (269)) + (Prims.of_int (271)) (Prims.of_int (26)) - (Prims.of_int (269)) + (Prims.of_int (271)) (Prims.of_int (59))))) (Obj.magic (FStar_Tactics_V2_Builtins.top_env @@ -2078,17 +2162,17 @@ let (mk_class : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (272)) + (Prims.of_int (274)) (Prims.of_int (28)) - (Prims.of_int (272)) + (Prims.of_int (274)) (Prims.of_int (45))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (272)) - (Prims.of_int (22)) (Prims.of_int (274)) + (Prims.of_int (22)) + (Prims.of_int (276)) (Prims.of_int (62))))) (Obj.magic (FStar_Tactics_NamedView.inspect_sigelt @@ -2134,17 +2218,17 @@ let (mk_class : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (278)) + (Prims.of_int (280)) (Prims.of_int (26)) - (Prims.of_int (285)) + (Prims.of_int (287)) (Prims.of_int (49))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (286)) + (Prims.of_int (288)) (Prims.of_int (20)) - (Prims.of_int (308)) + (Prims.of_int (310)) (Prims.of_int (20))))) (Obj.magic (FStar_Tactics_Effect.tac_bind @@ -2152,17 +2236,17 @@ let (mk_class : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (279)) + (Prims.of_int (281)) (Prims.of_int (34)) - (Prims.of_int (279)) + (Prims.of_int (281)) (Prims.of_int (63))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (278)) + (Prims.of_int (280)) (Prims.of_int (26)) - (Prims.of_int (285)) + (Prims.of_int (287)) (Prims.of_int (49))))) (Obj.magic (FStar_Tactics_V2_SyntaxHelpers.collect_arr_bs @@ -2182,17 +2266,17 @@ let (mk_class : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (280)) + (Prims.of_int (282)) (Prims.of_int (33)) - (Prims.of_int (280)) + (Prims.of_int (282)) (Prims.of_int (87))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (279)) + (Prims.of_int (281)) (Prims.of_int (66)) - (Prims.of_int (285)) + (Prims.of_int (287)) (Prims.of_int (49))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -2231,17 +2315,17 @@ let (mk_class : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (284)) + (Prims.of_int (286)) (Prims.of_int (33)) - (Prims.of_int (284)) + (Prims.of_int (286)) (Prims.of_int (55))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (285)) + (Prims.of_int (287)) (Prims.of_int (24)) - (Prims.of_int (285)) + (Prims.of_int (287)) (Prims.of_int (49))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -2274,17 +2358,17 @@ let (mk_class : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (287)) + (Prims.of_int (289)) (Prims.of_int (27)) - (Prims.of_int (294)) + (Prims.of_int (296)) (Prims.of_int (50))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (295)) + (Prims.of_int (297)) (Prims.of_int (20)) - (Prims.of_int (308)) + (Prims.of_int (310)) (Prims.of_int (20))))) (Obj.magic (FStar_Tactics_Effect.tac_bind @@ -2292,17 +2376,17 @@ let (mk_class : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (288)) + (Prims.of_int (290)) (Prims.of_int (35)) - (Prims.of_int (288)) + (Prims.of_int (290)) (Prims.of_int (61))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (287)) + (Prims.of_int (289)) (Prims.of_int (27)) - (Prims.of_int (294)) + (Prims.of_int (296)) (Prims.of_int (50))))) (Obj.magic (FStar_Tactics_V2_SyntaxHelpers.collect_abs @@ -2322,17 +2406,17 @@ let (mk_class : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (289)) + (Prims.of_int (291)) (Prims.of_int (33)) - (Prims.of_int (289)) + (Prims.of_int (291)) (Prims.of_int (87))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (288)) + (Prims.of_int (290)) (Prims.of_int (64)) - (Prims.of_int (294)) + (Prims.of_int (296)) (Prims.of_int (50))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -2371,17 +2455,17 @@ let (mk_class : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (293)) + (Prims.of_int (295)) (Prims.of_int (33)) - (Prims.of_int (293)) + (Prims.of_int (295)) (Prims.of_int (55))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (294)) + (Prims.of_int (296)) (Prims.of_int (24)) - (Prims.of_int (294)) + (Prims.of_int (296)) (Prims.of_int (50))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -2414,17 +2498,17 @@ let (mk_class : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (299)) + (Prims.of_int (301)) (Prims.of_int (34)) - (Prims.of_int (299)) + (Prims.of_int (301)) (Prims.of_int (36))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (299)) + (Prims.of_int (301)) (Prims.of_int (39)) - (Prims.of_int (308)) + (Prims.of_int (310)) (Prims.of_int (20))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -2440,17 +2524,17 @@ let (mk_class : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (300)) + (Prims.of_int (302)) (Prims.of_int (35)) - (Prims.of_int (300)) + (Prims.of_int (302)) (Prims.of_int (38))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (300)) + (Prims.of_int (302)) (Prims.of_int (41)) - (Prims.of_int (308)) + (Prims.of_int (310)) (Prims.of_int (20))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -2466,17 +2550,17 @@ let (mk_class : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (301)) + (Prims.of_int (303)) (Prims.of_int (33)) - (Prims.of_int (301)) + (Prims.of_int (303)) (Prims.of_int (36))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (301)) + (Prims.of_int (303)) (Prims.of_int (39)) - (Prims.of_int (308)) + (Prims.of_int (310)) (Prims.of_int (20))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -2492,17 +2576,17 @@ let (mk_class : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (303)) + (Prims.of_int (305)) (Prims.of_int (29)) - (Prims.of_int (303)) + (Prims.of_int (305)) (Prims.of_int (82))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (303)) + (Prims.of_int (305)) (Prims.of_int (87)) - (Prims.of_int (308)) + (Prims.of_int (310)) (Prims.of_int (20))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -2528,17 +2612,17 @@ let (mk_class : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (304)) + (Prims.of_int (306)) (Prims.of_int (27)) - (Prims.of_int (304)) + (Prims.of_int (306)) (Prims.of_int (71))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (306)) + (Prims.of_int (308)) (Prims.of_int (27)) - (Prims.of_int (306)) + (Prims.of_int (308)) (Prims.of_int (54))))) (Obj.magic (FStar_Tactics_NamedView.pack_sigelt diff --git a/ocaml/fstar-lib/generated/FStar_Tactics_V1_Basic.ml b/ocaml/fstar-lib/generated/FStar_Tactics_V1_Basic.ml index 8e4bc30853c..d63862a3bae 100644 --- a/ocaml/fstar-lib/generated/FStar_Tactics_V1_Basic.ml +++ b/ocaml/fstar-lib/generated/FStar_Tactics_V1_Basic.ml @@ -2954,7 +2954,9 @@ let (t_apply : FStar_Tactics_Printing.goal_to_string_verbose goal in let uu___10 = - FStar_TypeChecker_Env.print_gamma + FStar_Class_Show.show + (FStar_Class_Show.show_list + FStar_Syntax_Print.showable_binding) e.FStar_TypeChecker_Env.gamma in let uu___11 = FStar_Class_Show.show diff --git a/ocaml/fstar-lib/generated/FStar_Tactics_V2_Basic.ml b/ocaml/fstar-lib/generated/FStar_Tactics_V2_Basic.ml index 314c1a207ee..12ce6c8ccde 100644 --- a/ocaml/fstar-lib/generated/FStar_Tactics_V2_Basic.ml +++ b/ocaml/fstar-lib/generated/FStar_Tactics_V2_Basic.ml @@ -3022,7 +3022,9 @@ let (t_apply : FStar_Tactics_Printing.goal_to_string_verbose goal in let uu___10 = - FStar_TypeChecker_Env.print_gamma + FStar_Class_Show.show + (FStar_Class_Show.show_list + FStar_Syntax_Print.showable_binding) e.FStar_TypeChecker_Env.gamma in let uu___11 = FStar_Class_Show.show diff --git a/ocaml/fstar-lib/generated/FStar_TypeChecker_Common.ml b/ocaml/fstar-lib/generated/FStar_TypeChecker_Common.ml index 741df433ef8..1b72abd28a0 100644 --- a/ocaml/fstar-lib/generated/FStar_TypeChecker_Common.ml +++ b/ocaml/fstar-lib/generated/FStar_TypeChecker_Common.ml @@ -474,27 +474,13 @@ let (check_uvar_ctx_invariant : fun should_check -> fun g -> fun bs -> - let print_gamma gamma = - let uu___ = - FStar_Compiler_Effect.op_Bar_Greater gamma - (FStar_Compiler_List.map - (fun uu___1 -> - match uu___1 with - | FStar_Syntax_Syntax.Binding_var x -> - let uu___2 = FStar_Syntax_Print.bv_to_string x in - Prims.op_Hat "Binding_var " uu___2 - | FStar_Syntax_Syntax.Binding_univ u -> - let uu___2 = FStar_Ident.string_of_id u in - Prims.op_Hat "Binding_univ " uu___2 - | FStar_Syntax_Syntax.Binding_lid (l, uu___2) -> - let uu___3 = FStar_Ident.string_of_lid l in - Prims.op_Hat "Binding_lid " uu___3)) in - FStar_Compiler_Effect.op_Bar_Greater uu___ - (FStar_Compiler_String.concat "::\n") in let fail uu___ = let uu___1 = let uu___2 = FStar_Compiler_Range_Ops.string_of_range r in - let uu___3 = print_gamma g in + let uu___3 = + FStar_Class_Show.show + (FStar_Class_Show.show_list + FStar_Syntax_Print.showable_binding) g in let uu___4 = FStar_Syntax_Print.binders_to_string ", " bs in FStar_Compiler_Util.format5 "Invariant violation: gamma and binders are out of sync\n\treason=%s, range=%s, should_check=%s\n\t\n gamma=%s\n\tbinders=%s\n" diff --git a/ocaml/fstar-lib/generated/FStar_TypeChecker_Env.ml b/ocaml/fstar-lib/generated/FStar_TypeChecker_Env.ml index 2dbde2cddf0..60c2d3892b9 100644 --- a/ocaml/fstar-lib/generated/FStar_TypeChecker_Env.ml +++ b/ocaml/fstar-lib/generated/FStar_TypeChecker_Env.ml @@ -6249,33 +6249,6 @@ let (univnames : let uu___3 = FStar_Syntax_Free.univnames t in ext out uu___3 in aux uu___2 tl in aux no_univ_names env1.gamma -let (print_gamma : FStar_Syntax_Syntax.gamma -> Prims.string) = - fun gamma -> - let uu___ = - FStar_Compiler_Effect.op_Bar_Greater gamma - (FStar_Compiler_List.map - (fun uu___1 -> - match uu___1 with - | FStar_Syntax_Syntax.Binding_var x -> - let uu___2 = - let uu___3 = FStar_Syntax_Print.bv_to_string x in - let uu___4 = - let uu___5 = - let uu___6 = - FStar_Syntax_Print.term_to_string - x.FStar_Syntax_Syntax.sort in - Prims.op_Hat uu___6 ")" in - Prims.op_Hat ":" uu___5 in - Prims.op_Hat uu___3 uu___4 in - Prims.op_Hat "Binding_var (" uu___2 - | FStar_Syntax_Syntax.Binding_univ u -> - let uu___2 = FStar_Ident.string_of_id u in - Prims.op_Hat "Binding_univ " uu___2 - | FStar_Syntax_Syntax.Binding_lid (l, uu___2) -> - let uu___3 = FStar_Ident.string_of_lid l in - Prims.op_Hat "Binding_lid " uu___3)) in - FStar_Compiler_Effect.op_Bar_Greater uu___ - (FStar_Compiler_String.concat "::\n") let (string_of_delta_level : delta_level -> Prims.string) = fun uu___ -> match uu___ with diff --git a/ocaml/fstar-lib/generated/FStar_TypeChecker_Generalize.ml b/ocaml/fstar-lib/generated/FStar_TypeChecker_Generalize.ml index e6f1268ec01..73d04964999 100644 --- a/ocaml/fstar-lib/generated/FStar_TypeChecker_Generalize.ml +++ b/ocaml/fstar-lib/generated/FStar_TypeChecker_Generalize.ml @@ -385,51 +385,6 @@ let (gen : lecs2)) uu___3 [] in let lecs2 = lec_hd :: lecs1 in let gen_types uvs1 = - let fail rng k = - let uu___3 = lec_hd in - match uu___3 with - | (lbname, e, c) -> - let uu___4 = - let uu___5 = - let uu___6 = - let uu___7 = - let uu___8 = - FStar_Errors_Msg.text - "Failed to resolve implicit argument of type" in - let uu___9 = - FStar_Class_PP.pp - FStar_Syntax_Print.pretty_term k in - FStar_Pprint.prefix (Prims.of_int (4)) - Prims.int_one uu___8 uu___9 in - let uu___8 = - let uu___9 = - let uu___10 = - let uu___11 = - FStar_Errors_Msg.text "in the type of" in - let uu___12 = - let uu___13 = - let uu___14 = - let uu___15 = - FStar_Syntax_Print.lbname_to_string - lbname in - FStar_Pprint.doc_of_string uu___15 in - FStar_Pprint.squotes uu___14 in - FStar_Pprint.op_Hat_Hat uu___13 - FStar_Pprint.colon in - FStar_Pprint.op_Hat_Slash_Hat uu___11 - uu___12 in - FStar_Pprint.group uu___10 in - let uu___10 = - FStar_Class_PP.pp - FStar_Syntax_Print.pretty_term - (FStar_Syntax_Util.comp_result c) in - FStar_Pprint.prefix (Prims.of_int (4)) - Prims.int_one uu___9 uu___10 in - FStar_Pprint.op_Hat_Slash_Hat uu___7 uu___8 in - [uu___6] in - (FStar_Errors_Codes.Fatal_FailToResolveImplicitArgument, - uu___5) in - FStar_Errors.raise_error_doc uu___4 rng in FStar_Compiler_Effect.op_Bar_Greater uvs1 (FStar_Compiler_List.concatMap (fun u -> @@ -457,65 +412,60 @@ let (gen : FStar_Syntax_Util.arrow_formals k in (match uu___6 with | (bs, kres) -> - ((let uu___8 = + let uu___7 = + let uu___8 = let uu___9 = - let uu___10 = - FStar_TypeChecker_Normalize.unfold_whnf - env kres in - FStar_Syntax_Util.unrefine uu___10 in - uu___9.FStar_Syntax_Syntax.n in - match uu___8 with - | FStar_Syntax_Syntax.Tm_type uu___9 - -> - let free = - FStar_Syntax_Free.names kres in - let uu___10 = - let uu___11 = - FStar_Compiler_Util.set_is_empty - free in - Prims.op_Negation uu___11 in - if uu___10 - then - fail - u.FStar_Syntax_Syntax.ctx_uvar_range - kres - else () - | uu___9 -> - fail - u.FStar_Syntax_Syntax.ctx_uvar_range - kres); - (let a = - let uu___8 = - let uu___9 = - FStar_TypeChecker_Env.get_range - env in - FStar_Compiler_Effect.op_Less_Bar - (fun uu___10 -> - FStar_Pervasives_Native.Some - uu___10) uu___9 in - FStar_Syntax_Syntax.new_bv uu___8 - kres in - let t = - match bs with - | [] -> - FStar_Syntax_Syntax.bv_to_name a - | uu___8 -> - let uu___9 = - FStar_Syntax_Syntax.bv_to_name - a in - FStar_Syntax_Util.abs bs uu___9 - (FStar_Pervasives_Native.Some - (FStar_Syntax_Util.residual_tot - kres)) in - FStar_Syntax_Util.set_uvar - u.FStar_Syntax_Syntax.ctx_uvar_head - t; - (let uu___9 = - let uu___10 = - FStar_Syntax_Syntax.as_bqual_implicit - true in - (a, uu___10) in - [uu___9]))))))) in + FStar_TypeChecker_Normalize.unfold_whnf + env kres in + FStar_Syntax_Util.unrefine uu___9 in + uu___8.FStar_Syntax_Syntax.n in + (match uu___7 with + | FStar_Syntax_Syntax.Tm_type uu___8 -> + let free = + FStar_Syntax_Free.names kres in + let uu___9 = + let uu___10 = + FStar_Compiler_Util.set_is_empty + free in + Prims.op_Negation uu___10 in + if uu___9 + then [] + else + (let a = + let uu___11 = + let uu___12 = + FStar_TypeChecker_Env.get_range + env in + FStar_Compiler_Effect.op_Less_Bar + (fun uu___13 -> + FStar_Pervasives_Native.Some + uu___13) uu___12 in + FStar_Syntax_Syntax.new_bv + uu___11 kres in + let t = + match bs with + | [] -> + FStar_Syntax_Syntax.bv_to_name + a + | uu___11 -> + let uu___12 = + FStar_Syntax_Syntax.bv_to_name + a in + FStar_Syntax_Util.abs bs + uu___12 + (FStar_Pervasives_Native.Some + (FStar_Syntax_Util.residual_tot + kres)) in + FStar_Syntax_Util.set_uvar + u.FStar_Syntax_Syntax.ctx_uvar_head + t; + (let uu___12 = + let uu___13 = + FStar_Syntax_Syntax.as_bqual_implicit + true in + (a, uu___13) in + [uu___12])) + | uu___8 -> []))))) in let gen_univs1 = gen_univs env univs in let gen_tvars = gen_types uvs in let ecs = diff --git a/ocaml/fstar-lib/generated/FStar_TypeChecker_Rel.ml b/ocaml/fstar-lib/generated/FStar_TypeChecker_Rel.ml index 94634e5cff8..bce600a8deb 100644 --- a/ocaml/fstar-lib/generated/FStar_TypeChecker_Rel.ml +++ b/ocaml/fstar-lib/generated/FStar_TypeChecker_Rel.ml @@ -45,6 +45,17 @@ let (__proj__Implicit_has_typing_guard__item___0 : (FStar_Syntax_Syntax.term * FStar_Syntax_Syntax.typ)) = fun projectee -> match projectee with | Implicit_has_typing_guard _0 -> _0 +let (showable_implicit_checking_status : + implicit_checking_status FStar_Class_Show.showable) = + { + FStar_Class_Show.show = + (fun uu___ -> + match uu___ with + | Implicit_unresolved -> "Implicit_unresolved" + | Implicit_checking_defers_univ_constraint -> + "Implicit_checking_defers_univ_constraint" + | Implicit_has_typing_guard (tm, typ) -> "Implicit_has_typing_guard") + } type tagged_implicits = (FStar_TypeChecker_Common.implicit * implicit_checking_status) Prims.list let (is_base_type : @@ -1935,12 +1946,6 @@ let (flex_uvar_has_meta_tac : FStar_Syntax_Syntax.ctx_uvar -> Prims.bool) = | FStar_Pervasives_Native.Some (FStar_Syntax_Syntax.Ctx_uvar_meta_tac uu___) -> true | uu___ -> false -let (flex_uvar_meta_tac_env : - FStar_Syntax_Syntax.ctx_uvar -> FStar_TypeChecker_Env.env_t) = - fun u -> - match u.FStar_Syntax_Syntax.ctx_uvar_meta with - | FStar_Pervasives_Native.Some (FStar_Syntax_Syntax.Ctx_uvar_meta_tac - (denv, uu___)) -> FStar_Compiler_Dyn.undyn denv let (flex_t_to_string : flex_t -> Prims.string) = fun uu___ -> match uu___ with @@ -4185,8 +4190,106 @@ let (run_meta_arg_tac : | FStar_Pervasives_Native.Some (FStar_Syntax_Syntax.Ctx_uvar_meta_tac (env_dyn, tau)) -> let env = FStar_Compiler_Dyn.undyn env_dyn in + let env1 = + { + FStar_TypeChecker_Env.solver = (env.FStar_TypeChecker_Env.solver); + FStar_TypeChecker_Env.range = (env.FStar_TypeChecker_Env.range); + FStar_TypeChecker_Env.curmodule = + (env.FStar_TypeChecker_Env.curmodule); + FStar_TypeChecker_Env.gamma = + (ctx_u.FStar_Syntax_Syntax.ctx_uvar_gamma); + FStar_TypeChecker_Env.gamma_sig = + (env.FStar_TypeChecker_Env.gamma_sig); + FStar_TypeChecker_Env.gamma_cache = + (env.FStar_TypeChecker_Env.gamma_cache); + FStar_TypeChecker_Env.modules = + (env.FStar_TypeChecker_Env.modules); + FStar_TypeChecker_Env.expected_typ = + (env.FStar_TypeChecker_Env.expected_typ); + FStar_TypeChecker_Env.sigtab = (env.FStar_TypeChecker_Env.sigtab); + FStar_TypeChecker_Env.attrtab = + (env.FStar_TypeChecker_Env.attrtab); + FStar_TypeChecker_Env.instantiate_imp = + (env.FStar_TypeChecker_Env.instantiate_imp); + FStar_TypeChecker_Env.effects = + (env.FStar_TypeChecker_Env.effects); + FStar_TypeChecker_Env.generalize = + (env.FStar_TypeChecker_Env.generalize); + FStar_TypeChecker_Env.letrecs = + (env.FStar_TypeChecker_Env.letrecs); + FStar_TypeChecker_Env.top_level = + (env.FStar_TypeChecker_Env.top_level); + FStar_TypeChecker_Env.check_uvars = + (env.FStar_TypeChecker_Env.check_uvars); + FStar_TypeChecker_Env.use_eq_strict = + (env.FStar_TypeChecker_Env.use_eq_strict); + FStar_TypeChecker_Env.is_iface = + (env.FStar_TypeChecker_Env.is_iface); + FStar_TypeChecker_Env.admit = (env.FStar_TypeChecker_Env.admit); + FStar_TypeChecker_Env.lax = (env.FStar_TypeChecker_Env.lax); + FStar_TypeChecker_Env.lax_universes = + (env.FStar_TypeChecker_Env.lax_universes); + FStar_TypeChecker_Env.phase1 = (env.FStar_TypeChecker_Env.phase1); + FStar_TypeChecker_Env.failhard = + (env.FStar_TypeChecker_Env.failhard); + FStar_TypeChecker_Env.nosynth = + (env.FStar_TypeChecker_Env.nosynth); + FStar_TypeChecker_Env.uvar_subtyping = + (env.FStar_TypeChecker_Env.uvar_subtyping); + FStar_TypeChecker_Env.intactics = + (env.FStar_TypeChecker_Env.intactics); + FStar_TypeChecker_Env.nocoerce = + (env.FStar_TypeChecker_Env.nocoerce); + FStar_TypeChecker_Env.tc_term = + (env.FStar_TypeChecker_Env.tc_term); + FStar_TypeChecker_Env.typeof_tot_or_gtot_term = + (env.FStar_TypeChecker_Env.typeof_tot_or_gtot_term); + FStar_TypeChecker_Env.universe_of = + (env.FStar_TypeChecker_Env.universe_of); + FStar_TypeChecker_Env.typeof_well_typed_tot_or_gtot_term = + (env.FStar_TypeChecker_Env.typeof_well_typed_tot_or_gtot_term); + FStar_TypeChecker_Env.teq_nosmt_force = + (env.FStar_TypeChecker_Env.teq_nosmt_force); + FStar_TypeChecker_Env.subtype_nosmt_force = + (env.FStar_TypeChecker_Env.subtype_nosmt_force); + FStar_TypeChecker_Env.qtbl_name_and_index = + (env.FStar_TypeChecker_Env.qtbl_name_and_index); + FStar_TypeChecker_Env.normalized_eff_names = + (env.FStar_TypeChecker_Env.normalized_eff_names); + FStar_TypeChecker_Env.fv_delta_depths = + (env.FStar_TypeChecker_Env.fv_delta_depths); + FStar_TypeChecker_Env.proof_ns = + (env.FStar_TypeChecker_Env.proof_ns); + FStar_TypeChecker_Env.synth_hook = + (env.FStar_TypeChecker_Env.synth_hook); + FStar_TypeChecker_Env.try_solve_implicits_hook = + (env.FStar_TypeChecker_Env.try_solve_implicits_hook); + FStar_TypeChecker_Env.splice = (env.FStar_TypeChecker_Env.splice); + FStar_TypeChecker_Env.mpreprocess = + (env.FStar_TypeChecker_Env.mpreprocess); + FStar_TypeChecker_Env.postprocess = + (env.FStar_TypeChecker_Env.postprocess); + FStar_TypeChecker_Env.identifier_info = + (env.FStar_TypeChecker_Env.identifier_info); + FStar_TypeChecker_Env.tc_hooks = + (env.FStar_TypeChecker_Env.tc_hooks); + FStar_TypeChecker_Env.dsenv = (env.FStar_TypeChecker_Env.dsenv); + FStar_TypeChecker_Env.nbe = (env.FStar_TypeChecker_Env.nbe); + FStar_TypeChecker_Env.strict_args_tab = + (env.FStar_TypeChecker_Env.strict_args_tab); + FStar_TypeChecker_Env.erasable_types_tab = + (env.FStar_TypeChecker_Env.erasable_types_tab); + FStar_TypeChecker_Env.enable_defer_to_tac = + (env.FStar_TypeChecker_Env.enable_defer_to_tac); + FStar_TypeChecker_Env.unif_allow_ref_guards = + (env.FStar_TypeChecker_Env.unif_allow_ref_guards); + FStar_TypeChecker_Env.erase_erasable_args = + (env.FStar_TypeChecker_Env.erase_erasable_args); + FStar_TypeChecker_Env.core_check = + (env.FStar_TypeChecker_Env.core_check) + } in ((let uu___1 = - FStar_TypeChecker_Env.debug env (FStar_Options.Other "Tac") in + FStar_TypeChecker_Env.debug env1 (FStar_Options.Other "Tac") in if uu___1 then let uu___2 = @@ -4197,7 +4300,7 @@ let (run_meta_arg_tac : FStar_Errors.with_ctx "Running tactic for meta-arg" (fun uu___1 -> let uu___2 = FStar_Syntax_Util.ctx_uvar_typ ctx_u in - env.FStar_TypeChecker_Env.synth_hook env uu___2 tau)) + env1.FStar_TypeChecker_Env.synth_hook env1 uu___2 tau)) | uu___ -> failwith "run_meta_arg_tac must have been called with a uvar that has a meta tac" @@ -4871,6 +4974,15 @@ let (env_has_free_uvars : FStar_TypeChecker_Env.env_t -> Prims.bool) = (fun b -> has_free_uvars (b.FStar_Syntax_Syntax.binder_bv).FStar_Syntax_Syntax.sort) uu___ +let (gamma_has_free_uvars : + FStar_Syntax_Syntax.binding Prims.list -> Prims.bool) = + fun g -> + FStar_Compiler_List.existsb + (fun uu___ -> + match uu___ with + | FStar_Syntax_Syntax.Binding_var bv -> + has_free_uvars bv.FStar_Syntax_Syntax.sort + | uu___1 -> false) g let rec (solve : worklist -> solution) = fun probs -> (let uu___1 = @@ -7529,8 +7641,7 @@ and (solve_t_flex_flex : Prims.op_Negation uu___)) && (let uu___ = - let uu___1 = flex_uvar_meta_tac_env uv in - env_has_free_uvars uu___1 in + gamma_has_free_uvars uv.FStar_Syntax_Syntax.ctx_uvar_gamma in Prims.op_Negation uu___) in let run_meta_arg_tac_and_try_again flex = let uv = flex_uvar flex in @@ -13631,7 +13742,9 @@ let (try_teq : FStar_Class_Show.show FStar_Syntax_Print.showable_term t2 in let uu___8 = - FStar_TypeChecker_Env.print_gamma + FStar_Class_Show.show + (FStar_Class_Show.show_list + FStar_Syntax_Print.showable_binding) env.FStar_TypeChecker_Env.gamma in FStar_Compiler_Util.print3 "try_teq of %s and %s in %s {\n" uu___6 uu___7 uu___8 @@ -15361,25 +15474,176 @@ let (resolve_implicits' : | FStar_Pervasives_Native.Some (FStar_Syntax_Syntax.Ctx_uvar_meta_tac meta) -> - let m_env = - FStar_Compiler_Dyn.undyn - (FStar_Pervasives_Native.fst - meta) in + let env1 = + { + FStar_TypeChecker_Env.solver = + (env.FStar_TypeChecker_Env.solver); + FStar_TypeChecker_Env.range = + (env.FStar_TypeChecker_Env.range); + FStar_TypeChecker_Env.curmodule + = + (env.FStar_TypeChecker_Env.curmodule); + FStar_TypeChecker_Env.gamma = + (ctx_u.FStar_Syntax_Syntax.ctx_uvar_gamma); + FStar_TypeChecker_Env.gamma_sig + = + (env.FStar_TypeChecker_Env.gamma_sig); + FStar_TypeChecker_Env.gamma_cache + = + (env.FStar_TypeChecker_Env.gamma_cache); + FStar_TypeChecker_Env.modules = + (env.FStar_TypeChecker_Env.modules); + FStar_TypeChecker_Env.expected_typ + = + (env.FStar_TypeChecker_Env.expected_typ); + FStar_TypeChecker_Env.sigtab = + (env.FStar_TypeChecker_Env.sigtab); + FStar_TypeChecker_Env.attrtab = + (env.FStar_TypeChecker_Env.attrtab); + FStar_TypeChecker_Env.instantiate_imp + = + (env.FStar_TypeChecker_Env.instantiate_imp); + FStar_TypeChecker_Env.effects = + (env.FStar_TypeChecker_Env.effects); + FStar_TypeChecker_Env.generalize + = + (env.FStar_TypeChecker_Env.generalize); + FStar_TypeChecker_Env.letrecs = + (env.FStar_TypeChecker_Env.letrecs); + FStar_TypeChecker_Env.top_level + = + (env.FStar_TypeChecker_Env.top_level); + FStar_TypeChecker_Env.check_uvars + = + (env.FStar_TypeChecker_Env.check_uvars); + FStar_TypeChecker_Env.use_eq_strict + = + (env.FStar_TypeChecker_Env.use_eq_strict); + FStar_TypeChecker_Env.is_iface + = + (env.FStar_TypeChecker_Env.is_iface); + FStar_TypeChecker_Env.admit = + (env.FStar_TypeChecker_Env.admit); + FStar_TypeChecker_Env.lax = + (env.FStar_TypeChecker_Env.lax); + FStar_TypeChecker_Env.lax_universes + = + (env.FStar_TypeChecker_Env.lax_universes); + FStar_TypeChecker_Env.phase1 = + (env.FStar_TypeChecker_Env.phase1); + FStar_TypeChecker_Env.failhard + = + (env.FStar_TypeChecker_Env.failhard); + FStar_TypeChecker_Env.nosynth = + (env.FStar_TypeChecker_Env.nosynth); + FStar_TypeChecker_Env.uvar_subtyping + = + (env.FStar_TypeChecker_Env.uvar_subtyping); + FStar_TypeChecker_Env.intactics + = + (env.FStar_TypeChecker_Env.intactics); + FStar_TypeChecker_Env.nocoerce + = + (env.FStar_TypeChecker_Env.nocoerce); + FStar_TypeChecker_Env.tc_term = + (env.FStar_TypeChecker_Env.tc_term); + FStar_TypeChecker_Env.typeof_tot_or_gtot_term + = + (env.FStar_TypeChecker_Env.typeof_tot_or_gtot_term); + FStar_TypeChecker_Env.universe_of + = + (env.FStar_TypeChecker_Env.universe_of); + FStar_TypeChecker_Env.typeof_well_typed_tot_or_gtot_term + = + (env.FStar_TypeChecker_Env.typeof_well_typed_tot_or_gtot_term); + FStar_TypeChecker_Env.teq_nosmt_force + = + (env.FStar_TypeChecker_Env.teq_nosmt_force); + FStar_TypeChecker_Env.subtype_nosmt_force + = + (env.FStar_TypeChecker_Env.subtype_nosmt_force); + FStar_TypeChecker_Env.qtbl_name_and_index + = + (env.FStar_TypeChecker_Env.qtbl_name_and_index); + FStar_TypeChecker_Env.normalized_eff_names + = + (env.FStar_TypeChecker_Env.normalized_eff_names); + FStar_TypeChecker_Env.fv_delta_depths + = + (env.FStar_TypeChecker_Env.fv_delta_depths); + FStar_TypeChecker_Env.proof_ns + = + (env.FStar_TypeChecker_Env.proof_ns); + FStar_TypeChecker_Env.synth_hook + = + (env.FStar_TypeChecker_Env.synth_hook); + FStar_TypeChecker_Env.try_solve_implicits_hook + = + (env.FStar_TypeChecker_Env.try_solve_implicits_hook); + FStar_TypeChecker_Env.splice = + (env.FStar_TypeChecker_Env.splice); + FStar_TypeChecker_Env.mpreprocess + = + (env.FStar_TypeChecker_Env.mpreprocess); + FStar_TypeChecker_Env.postprocess + = + (env.FStar_TypeChecker_Env.postprocess); + FStar_TypeChecker_Env.identifier_info + = + (env.FStar_TypeChecker_Env.identifier_info); + FStar_TypeChecker_Env.tc_hooks + = + (env.FStar_TypeChecker_Env.tc_hooks); + FStar_TypeChecker_Env.dsenv = + (env.FStar_TypeChecker_Env.dsenv); + FStar_TypeChecker_Env.nbe = + (env.FStar_TypeChecker_Env.nbe); + FStar_TypeChecker_Env.strict_args_tab + = + (env.FStar_TypeChecker_Env.strict_args_tab); + FStar_TypeChecker_Env.erasable_types_tab + = + (env.FStar_TypeChecker_Env.erasable_types_tab); + FStar_TypeChecker_Env.enable_defer_to_tac + = + (env.FStar_TypeChecker_Env.enable_defer_to_tac); + FStar_TypeChecker_Env.unif_allow_ref_guards + = + (env.FStar_TypeChecker_Env.unif_allow_ref_guards); + FStar_TypeChecker_Env.erase_erasable_args + = + (env.FStar_TypeChecker_Env.erase_erasable_args); + FStar_TypeChecker_Env.core_check + = + (env.FStar_TypeChecker_Env.core_check) + } in let tac = FStar_Pervasives_Native.snd meta in let typ = FStar_Syntax_Util.ctx_uvar_typ ctx_u in let uu___7 = - (has_free_uvars typ) || - (env_has_free_uvars m_env) in + ((has_free_uvars typ) || + (gamma_has_free_uvars + ctx_u.FStar_Syntax_Syntax.ctx_uvar_gamma)) + && + (let uu___8 = + FStar_Options.ext_getv + "compat:open_metas" in + uu___8 = "") in if uu___7 then ((let uu___9 = - FStar_Compiler_Effect.op_Less_Bar - (FStar_TypeChecker_Env.debug - env) - (FStar_Options.Other "Rel") in + (FStar_Compiler_Effect.op_Less_Bar + (FStar_TypeChecker_Env.debug + env1) + (FStar_Options.Other "Rel")) + || + (FStar_Compiler_Effect.op_Less_Bar + (FStar_TypeChecker_Env.debug + env1) + (FStar_Options.Other + "Imps")) in if uu___9 then let uu___10 = @@ -15397,7 +15661,7 @@ let (resolve_implicits' : (let solve_with t = let extra = let uu___9 = - teq_nosmt env t tm in + teq_nosmt env1 t tm in match uu___9 with | FStar_Pervasives_Native.None -> @@ -15414,7 +15678,7 @@ let (resolve_implicits' : then let uu___10 = meta_arg_cache_lookup tac - m_env typ in + env1 typ in match uu___10 with | FStar_Pervasives_Native.Some res -> solve_with res @@ -15423,7 +15687,7 @@ let (resolve_implicits' : let t = run_meta_arg_tac ctx_u in (meta_arg_cache_result tac - m_env typ t; + env1 typ t; solve_with t) else (let t = From 2b22888be0f0a7a2eed564b6d41284a7fb2fc752 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Tue, 5 Dec 2023 03:42:58 -0800 Subject: [PATCH 27/29] Syntax: remove traces of env in Ctx_uvar_meta_tac --- src/syntax/FStar.Syntax.Syntax.fsti | 2 +- src/typechecker/FStar.TypeChecker.Env.fst | 2 +- src/typechecker/FStar.TypeChecker.Rel.fst | 16 +++++++--------- src/typechecker/FStar.TypeChecker.TcTerm.fst | 4 ++-- src/typechecker/FStar.TypeChecker.Util.fst | 8 +++----- 5 files changed, 14 insertions(+), 18 deletions(-) diff --git a/src/syntax/FStar.Syntax.Syntax.fsti b/src/syntax/FStar.Syntax.Syntax.fsti index 7962af809a1..1d0f252cd8f 100644 --- a/src/syntax/FStar.Syntax.Syntax.fsti +++ b/src/syntax/FStar.Syntax.Syntax.fsti @@ -187,7 +187,7 @@ and ctx_uvar = { (* (G |- ?u : t ctx_uvar_meta: option ctx_uvar_meta_t; } and ctx_uvar_meta_t = - | Ctx_uvar_meta_tac of dyn * term (* the dyn is an FStar.TypeChecker.Env.env *) + | Ctx_uvar_meta_tac of term | Ctx_uvar_meta_attr of term (* An attribute associated with an implicit argument using the #[@@...] notation *) and ctx_uvar_and_subst = ctx_uvar * subst_ts diff --git a/src/typechecker/FStar.TypeChecker.Env.fst b/src/typechecker/FStar.TypeChecker.Env.fst index 24f9052e9fb..00949672c43 100644 --- a/src/typechecker/FStar.TypeChecker.Env.fst +++ b/src/typechecker/FStar.TypeChecker.Env.fst @@ -1925,7 +1925,7 @@ let uvars_for_binders env (bs:S.binders) substs reason r = let ctx_uvar_meta_t = match b.binder_qual, b.binder_attrs with | Some (Meta t), [] -> - Some (Ctx_uvar_meta_tac (FStar.Compiler.Dyn.mkdyn env, t)) + Some (Ctx_uvar_meta_tac t) | _, t::_ -> Some (Ctx_uvar_meta_attr t) | _ -> None in diff --git a/src/typechecker/FStar.TypeChecker.Rel.fst b/src/typechecker/FStar.TypeChecker.Rel.fst index 1ea084608c3..2ae0bad305e 100644 --- a/src/typechecker/FStar.TypeChecker.Rel.fst +++ b/src/typechecker/FStar.TypeChecker.Rel.fst @@ -1844,10 +1844,9 @@ let quasi_pattern env (f:flex_t) : option (binders * typ) = let formals, t_res = U.arrow_formals t_hd in aux [] formals t_res args -let run_meta_arg_tac (ctx_u:ctx_uvar) : term = +let run_meta_arg_tac (env:env_t) (ctx_u:ctx_uvar) : term = match ctx_u.ctx_uvar_meta with - | Some (Ctx_uvar_meta_tac (env_dyn, tau)) -> - let env : Env.env = FStar.Compiler.Dyn.undyn env_dyn in + | Some (Ctx_uvar_meta_tac tau) -> let env = { env with gamma = ctx_u.ctx_uvar_gamma } in if Env.debug env (Options.Other "Tac") then BU.print1 "Running tactic for meta-arg %s\n" (show ctx_u); @@ -3271,7 +3270,7 @@ and solve_t_flex_flex env orig wl (lhs:flex_t) (rhs:flex_t) : solution = let run_meta_arg_tac_and_try_again (flex:flex_t) = let uv = flex_uvar flex in - let t = run_meta_arg_tac uv in + let t = run_meta_arg_tac env uv in if debug wl <| Options.Other "Rel" then BU.print2 "solve_t_flex_flex: solving meta arg uvar %s with %s\n" (show uv) (show t); set_uvar env uv None t; @@ -4950,7 +4949,7 @@ let try_solve_deferred_constraints (defer_ok:defer_ok_t) smt_ok deferred_to_tac_ |> List.collect (fun i -> match i.imp_uvar.ctx_uvar_meta with - | Some (Ctx_uvar_meta_tac (_, tac)) -> + | Some (Ctx_uvar_meta_tac tac) -> let head, _ = U.head_and_args_full tac in if U.is_fvar PC.tcresolve_lid head then ( @@ -5497,9 +5496,8 @@ let resolve_implicits' env is_tac is_gen (implicits:Env.implicits) until_fixpoint (out, true) tl | _ when unresolved ctx_u && flex_uvar_has_meta_tac ctx_u -> - let Some (Ctx_uvar_meta_tac meta) = ctx_u.ctx_uvar_meta in + let Some (Ctx_uvar_meta_tac tac) = ctx_u.ctx_uvar_meta in let env = { env with gamma = ctx_u.ctx_uvar_gamma } in - let tac = snd meta in let typ = U.ctx_uvar_typ ctx_u in if (has_free_uvars typ || gamma_has_free_uvars ctx_u.ctx_uvar_gamma) && Options.ext_getv "compat:open_metas" = "" then // i.e. compat option unset @@ -5522,11 +5520,11 @@ let resolve_implicits' env is_tac is_gen (implicits:Env.implicits) match meta_arg_cache_lookup tac env typ with | Some res -> solve_with res | None -> - let t = run_meta_arg_tac ctx_u in + let t = run_meta_arg_tac env ctx_u in meta_arg_cache_result tac env typ t; solve_with t else - let t = run_meta_arg_tac ctx_u in + let t = run_meta_arg_tac env ctx_u in solve_with t ) diff --git a/src/typechecker/FStar.TypeChecker.TcTerm.fst b/src/typechecker/FStar.TypeChecker.TcTerm.fst index 58f67e08e95..e1ce88adf0b 100644 --- a/src/typechecker/FStar.TypeChecker.TcTerm.fst +++ b/src/typechecker/FStar.TypeChecker.TcTerm.fst @@ -2748,7 +2748,7 @@ and check_application_args env head (chead:comp) ghead args expected_topt : term | Some (Meta tau), _ -> let tau = SS.subst subst tau in let tau, _, g_tau = tc_tactic t_unit t_unit env tau in - Ctx_uvar_meta_tac (mkdyn env, tau), g_tau + Ctx_uvar_meta_tac tau, g_tau | Some (Implicit _), attr::_ -> let attr = SS.subst subst attr in let attr, _, g_attr = tc_tot_or_gtot_term env attr in @@ -2768,7 +2768,7 @@ and check_application_args env head (chead:comp) ghead args expected_topt : term let msg = let is_typeclass = match ctx_uvar_meta with - | Ctx_uvar_meta_tac (_, tau) -> U.is_fvar Const.tcresolve_lid tau + | Ctx_uvar_meta_tac tau -> U.is_fvar Const.tcresolve_lid tau | _ -> false in if is_typeclass diff --git a/src/typechecker/FStar.TypeChecker.Util.fst b/src/typechecker/FStar.TypeChecker.Util.fst index 21d5fae227e..d5de3ef7476 100644 --- a/src/typechecker/FStar.TypeChecker.Util.fst +++ b/src/typechecker/FStar.TypeChecker.Util.fst @@ -2883,16 +2883,14 @@ let maybe_instantiate (env:Env.env) e t = let t = SS.subst subst x.sort in let meta_t = match qual, attrs with - | Some (Meta tau), _ -> - Ctx_uvar_meta_tac (mkdyn env, tau) - | _, attr::_ -> - Ctx_uvar_meta_attr attr + | Some (Meta tau), _ -> Ctx_uvar_meta_tac tau + | _, attr::_ -> Ctx_uvar_meta_attr attr | _ -> failwith "Impossible, match is under a guard, did not expect this case" in let msg = let is_typeclass = match meta_t with - | Ctx_uvar_meta_tac (_, tau) -> U.is_fvar C.tcresolve_lid tau + | Ctx_uvar_meta_tac tau -> U.is_fvar C.tcresolve_lid tau | _ -> false in if is_typeclass From faed6031c0bc8ed482f6247527f04d0d74d16a6c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Tue, 5 Dec 2023 03:44:14 -0800 Subject: [PATCH 28/29] Bump checked file version --- src/fstar/FStar.CheckedFiles.fst | 2 +- ulib/prims.fst | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/fstar/FStar.CheckedFiles.fst b/src/fstar/FStar.CheckedFiles.fst index 1c1d9832a0e..026605947cc 100644 --- a/src/fstar/FStar.CheckedFiles.fst +++ b/src/fstar/FStar.CheckedFiles.fst @@ -40,7 +40,7 @@ module Dep = FStar.Parser.Dep * detect when loading the cache that the version number is same * It needs to be kept in sync with prims.fst *) -let cache_version_number = 63 +let cache_version_number = 64 (* * Abbreviation for what we store in the checked files (stages as described below) diff --git a/ulib/prims.fst b/ulib/prims.fst index bc5aff77e0f..1ad07c23a81 100644 --- a/ulib/prims.fst +++ b/ulib/prims.fst @@ -708,4 +708,4 @@ val string_of_int: int -> Tot string (** THIS IS MEANT TO BE KEPT IN SYNC WITH FStar.CheckedFiles.fs Incrementing this forces all .checked files to be invalidated *) irreducible -let __cache_version_number__ = 63 +let __cache_version_number__ = 64 From bbbcff1b32c3b0a2d1e976817b2a47c93badc258 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Tue, 5 Dec 2023 03:49:57 -0800 Subject: [PATCH 29/29] snap --- .../fstar-lib/generated/FStar_CheckedFiles.ml | 2 +- .../generated/FStar_Syntax_Syntax.ml | 5 +- .../generated/FStar_TypeChecker_Env.ml | 10 +- .../generated/FStar_TypeChecker_Rel.ml | 272 +++++++++--------- .../generated/FStar_TypeChecker_TcTerm.ml | 12 +- .../generated/FStar_TypeChecker_Util.ml | 8 +- 6 files changed, 148 insertions(+), 161 deletions(-) diff --git a/ocaml/fstar-lib/generated/FStar_CheckedFiles.ml b/ocaml/fstar-lib/generated/FStar_CheckedFiles.ml index 4d87cae8af6..c758fdc4ca5 100644 --- a/ocaml/fstar-lib/generated/FStar_CheckedFiles.ml +++ b/ocaml/fstar-lib/generated/FStar_CheckedFiles.ml @@ -1,5 +1,5 @@ open Prims -let (cache_version_number : Prims.int) = (Prims.of_int (63)) +let (cache_version_number : Prims.int) = (Prims.of_int (64)) type tc_result = { checked_module: FStar_Syntax_Syntax.modul ; diff --git a/ocaml/fstar-lib/generated/FStar_Syntax_Syntax.ml b/ocaml/fstar-lib/generated/FStar_Syntax_Syntax.ml index cda459007d9..81cbb4018f9 100644 --- a/ocaml/fstar-lib/generated/FStar_Syntax_Syntax.ml +++ b/ocaml/fstar-lib/generated/FStar_Syntax_Syntax.ml @@ -316,7 +316,7 @@ and ctx_uvar = ctx_uvar_range: FStar_Compiler_Range_Type.range ; ctx_uvar_meta: ctx_uvar_meta_t FStar_Pervasives_Native.option } and ctx_uvar_meta_t = - | Ctx_uvar_meta_tac of (FStar_Compiler_Dyn.dyn * term' syntax) + | Ctx_uvar_meta_tac of term' syntax | Ctx_uvar_meta_attr of term' syntax and uvar_decoration = { @@ -684,8 +684,7 @@ let (__proj__Mkctx_uvar__item__ctx_uvar_meta : let (uu___is_Ctx_uvar_meta_tac : ctx_uvar_meta_t -> Prims.bool) = fun projectee -> match projectee with | Ctx_uvar_meta_tac _0 -> true | uu___ -> false -let (__proj__Ctx_uvar_meta_tac__item___0 : - ctx_uvar_meta_t -> (FStar_Compiler_Dyn.dyn * term' syntax)) = +let (__proj__Ctx_uvar_meta_tac__item___0 : ctx_uvar_meta_t -> term' syntax) = fun projectee -> match projectee with | Ctx_uvar_meta_tac _0 -> _0 let (uu___is_Ctx_uvar_meta_attr : ctx_uvar_meta_t -> Prims.bool) = fun projectee -> diff --git a/ocaml/fstar-lib/generated/FStar_TypeChecker_Env.ml b/ocaml/fstar-lib/generated/FStar_TypeChecker_Env.ml index 60c2d3892b9..56b0153837e 100644 --- a/ocaml/fstar-lib/generated/FStar_TypeChecker_Env.ml +++ b/ocaml/fstar-lib/generated/FStar_TypeChecker_Env.ml @@ -6853,14 +6853,8 @@ let (uvars_for_binders : with | (FStar_Pervasives_Native.Some (FStar_Syntax_Syntax.Meta t), []) -> - let uu___2 = - let uu___3 = - let uu___4 = - FStar_Compiler_Dyn.mkdyn env1 in - (uu___4, t) in - FStar_Syntax_Syntax.Ctx_uvar_meta_tac - uu___3 in - FStar_Pervasives_Native.Some uu___2 + FStar_Pervasives_Native.Some + (FStar_Syntax_Syntax.Ctx_uvar_meta_tac t) | (uu___2, t::uu___3) -> FStar_Pervasives_Native.Some (FStar_Syntax_Syntax.Ctx_uvar_meta_attr t) diff --git a/ocaml/fstar-lib/generated/FStar_TypeChecker_Rel.ml b/ocaml/fstar-lib/generated/FStar_TypeChecker_Rel.ml index bce600a8deb..2228c4ae461 100644 --- a/ocaml/fstar-lib/generated/FStar_TypeChecker_Rel.ml +++ b/ocaml/fstar-lib/generated/FStar_TypeChecker_Rel.ml @@ -4184,126 +4184,132 @@ let (quasi_pattern : (match uu___3 with | (formals, t_res) -> aux [] formals t_res args)) let (run_meta_arg_tac : - FStar_Syntax_Syntax.ctx_uvar -> FStar_Syntax_Syntax.term) = - fun ctx_u -> - match ctx_u.FStar_Syntax_Syntax.ctx_uvar_meta with - | FStar_Pervasives_Native.Some (FStar_Syntax_Syntax.Ctx_uvar_meta_tac - (env_dyn, tau)) -> - let env = FStar_Compiler_Dyn.undyn env_dyn in - let env1 = - { - FStar_TypeChecker_Env.solver = (env.FStar_TypeChecker_Env.solver); - FStar_TypeChecker_Env.range = (env.FStar_TypeChecker_Env.range); - FStar_TypeChecker_Env.curmodule = - (env.FStar_TypeChecker_Env.curmodule); - FStar_TypeChecker_Env.gamma = - (ctx_u.FStar_Syntax_Syntax.ctx_uvar_gamma); - FStar_TypeChecker_Env.gamma_sig = - (env.FStar_TypeChecker_Env.gamma_sig); - FStar_TypeChecker_Env.gamma_cache = - (env.FStar_TypeChecker_Env.gamma_cache); - FStar_TypeChecker_Env.modules = - (env.FStar_TypeChecker_Env.modules); - FStar_TypeChecker_Env.expected_typ = - (env.FStar_TypeChecker_Env.expected_typ); - FStar_TypeChecker_Env.sigtab = (env.FStar_TypeChecker_Env.sigtab); - FStar_TypeChecker_Env.attrtab = - (env.FStar_TypeChecker_Env.attrtab); - FStar_TypeChecker_Env.instantiate_imp = - (env.FStar_TypeChecker_Env.instantiate_imp); - FStar_TypeChecker_Env.effects = - (env.FStar_TypeChecker_Env.effects); - FStar_TypeChecker_Env.generalize = - (env.FStar_TypeChecker_Env.generalize); - FStar_TypeChecker_Env.letrecs = - (env.FStar_TypeChecker_Env.letrecs); - FStar_TypeChecker_Env.top_level = - (env.FStar_TypeChecker_Env.top_level); - FStar_TypeChecker_Env.check_uvars = - (env.FStar_TypeChecker_Env.check_uvars); - FStar_TypeChecker_Env.use_eq_strict = - (env.FStar_TypeChecker_Env.use_eq_strict); - FStar_TypeChecker_Env.is_iface = - (env.FStar_TypeChecker_Env.is_iface); - FStar_TypeChecker_Env.admit = (env.FStar_TypeChecker_Env.admit); - FStar_TypeChecker_Env.lax = (env.FStar_TypeChecker_Env.lax); - FStar_TypeChecker_Env.lax_universes = - (env.FStar_TypeChecker_Env.lax_universes); - FStar_TypeChecker_Env.phase1 = (env.FStar_TypeChecker_Env.phase1); - FStar_TypeChecker_Env.failhard = - (env.FStar_TypeChecker_Env.failhard); - FStar_TypeChecker_Env.nosynth = - (env.FStar_TypeChecker_Env.nosynth); - FStar_TypeChecker_Env.uvar_subtyping = - (env.FStar_TypeChecker_Env.uvar_subtyping); - FStar_TypeChecker_Env.intactics = - (env.FStar_TypeChecker_Env.intactics); - FStar_TypeChecker_Env.nocoerce = - (env.FStar_TypeChecker_Env.nocoerce); - FStar_TypeChecker_Env.tc_term = - (env.FStar_TypeChecker_Env.tc_term); - FStar_TypeChecker_Env.typeof_tot_or_gtot_term = - (env.FStar_TypeChecker_Env.typeof_tot_or_gtot_term); - FStar_TypeChecker_Env.universe_of = - (env.FStar_TypeChecker_Env.universe_of); - FStar_TypeChecker_Env.typeof_well_typed_tot_or_gtot_term = - (env.FStar_TypeChecker_Env.typeof_well_typed_tot_or_gtot_term); - FStar_TypeChecker_Env.teq_nosmt_force = - (env.FStar_TypeChecker_Env.teq_nosmt_force); - FStar_TypeChecker_Env.subtype_nosmt_force = - (env.FStar_TypeChecker_Env.subtype_nosmt_force); - FStar_TypeChecker_Env.qtbl_name_and_index = - (env.FStar_TypeChecker_Env.qtbl_name_and_index); - FStar_TypeChecker_Env.normalized_eff_names = - (env.FStar_TypeChecker_Env.normalized_eff_names); - FStar_TypeChecker_Env.fv_delta_depths = - (env.FStar_TypeChecker_Env.fv_delta_depths); - FStar_TypeChecker_Env.proof_ns = - (env.FStar_TypeChecker_Env.proof_ns); - FStar_TypeChecker_Env.synth_hook = - (env.FStar_TypeChecker_Env.synth_hook); - FStar_TypeChecker_Env.try_solve_implicits_hook = - (env.FStar_TypeChecker_Env.try_solve_implicits_hook); - FStar_TypeChecker_Env.splice = (env.FStar_TypeChecker_Env.splice); - FStar_TypeChecker_Env.mpreprocess = - (env.FStar_TypeChecker_Env.mpreprocess); - FStar_TypeChecker_Env.postprocess = - (env.FStar_TypeChecker_Env.postprocess); - FStar_TypeChecker_Env.identifier_info = - (env.FStar_TypeChecker_Env.identifier_info); - FStar_TypeChecker_Env.tc_hooks = - (env.FStar_TypeChecker_Env.tc_hooks); - FStar_TypeChecker_Env.dsenv = (env.FStar_TypeChecker_Env.dsenv); - FStar_TypeChecker_Env.nbe = (env.FStar_TypeChecker_Env.nbe); - FStar_TypeChecker_Env.strict_args_tab = - (env.FStar_TypeChecker_Env.strict_args_tab); - FStar_TypeChecker_Env.erasable_types_tab = - (env.FStar_TypeChecker_Env.erasable_types_tab); - FStar_TypeChecker_Env.enable_defer_to_tac = - (env.FStar_TypeChecker_Env.enable_defer_to_tac); - FStar_TypeChecker_Env.unif_allow_ref_guards = - (env.FStar_TypeChecker_Env.unif_allow_ref_guards); - FStar_TypeChecker_Env.erase_erasable_args = - (env.FStar_TypeChecker_Env.erase_erasable_args); - FStar_TypeChecker_Env.core_check = - (env.FStar_TypeChecker_Env.core_check) - } in - ((let uu___1 = - FStar_TypeChecker_Env.debug env1 (FStar_Options.Other "Tac") in - if uu___1 - then - let uu___2 = - FStar_Class_Show.show FStar_Syntax_Print.showable_ctxu ctx_u in - FStar_Compiler_Util.print1 "Running tactic for meta-arg %s\n" - uu___2 - else ()); - FStar_Errors.with_ctx "Running tactic for meta-arg" - (fun uu___1 -> - let uu___2 = FStar_Syntax_Util.ctx_uvar_typ ctx_u in - env1.FStar_TypeChecker_Env.synth_hook env1 uu___2 tau)) - | uu___ -> - failwith - "run_meta_arg_tac must have been called with a uvar that has a meta tac" + FStar_TypeChecker_Env.env_t -> + FStar_Syntax_Syntax.ctx_uvar -> FStar_Syntax_Syntax.term) + = + fun env -> + fun ctx_u -> + match ctx_u.FStar_Syntax_Syntax.ctx_uvar_meta with + | FStar_Pervasives_Native.Some (FStar_Syntax_Syntax.Ctx_uvar_meta_tac + tau) -> + let env1 = + { + FStar_TypeChecker_Env.solver = + (env.FStar_TypeChecker_Env.solver); + FStar_TypeChecker_Env.range = (env.FStar_TypeChecker_Env.range); + FStar_TypeChecker_Env.curmodule = + (env.FStar_TypeChecker_Env.curmodule); + FStar_TypeChecker_Env.gamma = + (ctx_u.FStar_Syntax_Syntax.ctx_uvar_gamma); + FStar_TypeChecker_Env.gamma_sig = + (env.FStar_TypeChecker_Env.gamma_sig); + FStar_TypeChecker_Env.gamma_cache = + (env.FStar_TypeChecker_Env.gamma_cache); + FStar_TypeChecker_Env.modules = + (env.FStar_TypeChecker_Env.modules); + FStar_TypeChecker_Env.expected_typ = + (env.FStar_TypeChecker_Env.expected_typ); + FStar_TypeChecker_Env.sigtab = + (env.FStar_TypeChecker_Env.sigtab); + FStar_TypeChecker_Env.attrtab = + (env.FStar_TypeChecker_Env.attrtab); + FStar_TypeChecker_Env.instantiate_imp = + (env.FStar_TypeChecker_Env.instantiate_imp); + FStar_TypeChecker_Env.effects = + (env.FStar_TypeChecker_Env.effects); + FStar_TypeChecker_Env.generalize = + (env.FStar_TypeChecker_Env.generalize); + FStar_TypeChecker_Env.letrecs = + (env.FStar_TypeChecker_Env.letrecs); + FStar_TypeChecker_Env.top_level = + (env.FStar_TypeChecker_Env.top_level); + FStar_TypeChecker_Env.check_uvars = + (env.FStar_TypeChecker_Env.check_uvars); + FStar_TypeChecker_Env.use_eq_strict = + (env.FStar_TypeChecker_Env.use_eq_strict); + FStar_TypeChecker_Env.is_iface = + (env.FStar_TypeChecker_Env.is_iface); + FStar_TypeChecker_Env.admit = (env.FStar_TypeChecker_Env.admit); + FStar_TypeChecker_Env.lax = (env.FStar_TypeChecker_Env.lax); + FStar_TypeChecker_Env.lax_universes = + (env.FStar_TypeChecker_Env.lax_universes); + FStar_TypeChecker_Env.phase1 = + (env.FStar_TypeChecker_Env.phase1); + FStar_TypeChecker_Env.failhard = + (env.FStar_TypeChecker_Env.failhard); + FStar_TypeChecker_Env.nosynth = + (env.FStar_TypeChecker_Env.nosynth); + FStar_TypeChecker_Env.uvar_subtyping = + (env.FStar_TypeChecker_Env.uvar_subtyping); + FStar_TypeChecker_Env.intactics = + (env.FStar_TypeChecker_Env.intactics); + FStar_TypeChecker_Env.nocoerce = + (env.FStar_TypeChecker_Env.nocoerce); + FStar_TypeChecker_Env.tc_term = + (env.FStar_TypeChecker_Env.tc_term); + FStar_TypeChecker_Env.typeof_tot_or_gtot_term = + (env.FStar_TypeChecker_Env.typeof_tot_or_gtot_term); + FStar_TypeChecker_Env.universe_of = + (env.FStar_TypeChecker_Env.universe_of); + FStar_TypeChecker_Env.typeof_well_typed_tot_or_gtot_term = + (env.FStar_TypeChecker_Env.typeof_well_typed_tot_or_gtot_term); + FStar_TypeChecker_Env.teq_nosmt_force = + (env.FStar_TypeChecker_Env.teq_nosmt_force); + FStar_TypeChecker_Env.subtype_nosmt_force = + (env.FStar_TypeChecker_Env.subtype_nosmt_force); + FStar_TypeChecker_Env.qtbl_name_and_index = + (env.FStar_TypeChecker_Env.qtbl_name_and_index); + FStar_TypeChecker_Env.normalized_eff_names = + (env.FStar_TypeChecker_Env.normalized_eff_names); + FStar_TypeChecker_Env.fv_delta_depths = + (env.FStar_TypeChecker_Env.fv_delta_depths); + FStar_TypeChecker_Env.proof_ns = + (env.FStar_TypeChecker_Env.proof_ns); + FStar_TypeChecker_Env.synth_hook = + (env.FStar_TypeChecker_Env.synth_hook); + FStar_TypeChecker_Env.try_solve_implicits_hook = + (env.FStar_TypeChecker_Env.try_solve_implicits_hook); + FStar_TypeChecker_Env.splice = + (env.FStar_TypeChecker_Env.splice); + FStar_TypeChecker_Env.mpreprocess = + (env.FStar_TypeChecker_Env.mpreprocess); + FStar_TypeChecker_Env.postprocess = + (env.FStar_TypeChecker_Env.postprocess); + FStar_TypeChecker_Env.identifier_info = + (env.FStar_TypeChecker_Env.identifier_info); + FStar_TypeChecker_Env.tc_hooks = + (env.FStar_TypeChecker_Env.tc_hooks); + FStar_TypeChecker_Env.dsenv = (env.FStar_TypeChecker_Env.dsenv); + FStar_TypeChecker_Env.nbe = (env.FStar_TypeChecker_Env.nbe); + FStar_TypeChecker_Env.strict_args_tab = + (env.FStar_TypeChecker_Env.strict_args_tab); + FStar_TypeChecker_Env.erasable_types_tab = + (env.FStar_TypeChecker_Env.erasable_types_tab); + FStar_TypeChecker_Env.enable_defer_to_tac = + (env.FStar_TypeChecker_Env.enable_defer_to_tac); + FStar_TypeChecker_Env.unif_allow_ref_guards = + (env.FStar_TypeChecker_Env.unif_allow_ref_guards); + FStar_TypeChecker_Env.erase_erasable_args = + (env.FStar_TypeChecker_Env.erase_erasable_args); + FStar_TypeChecker_Env.core_check = + (env.FStar_TypeChecker_Env.core_check) + } in + ((let uu___1 = + FStar_TypeChecker_Env.debug env1 (FStar_Options.Other "Tac") in + if uu___1 + then + let uu___2 = + FStar_Class_Show.show FStar_Syntax_Print.showable_ctxu ctx_u in + FStar_Compiler_Util.print1 "Running tactic for meta-arg %s\n" + uu___2 + else ()); + FStar_Errors.with_ctx "Running tactic for meta-arg" + (fun uu___1 -> + let uu___2 = FStar_Syntax_Util.ctx_uvar_typ ctx_u in + env1.FStar_TypeChecker_Env.synth_hook env1 uu___2 tau)) + | uu___ -> + failwith + "run_meta_arg_tac must have been called with a uvar that has a meta tac" let (simplify_guard : FStar_TypeChecker_Env.env -> FStar_TypeChecker_Common.guard_t -> FStar_TypeChecker_Common.guard_t) @@ -7624,7 +7630,7 @@ and (solve_t_flex_rigid_eq : | (FStar_Pervasives.Inl msg, uu___10) -> imitate orig env wl lhs rhs)))))) and (solve_t_flex_flex : - FStar_TypeChecker_Env.env -> + FStar_TypeChecker_Env.env_t -> FStar_TypeChecker_Common.prob -> worklist -> flex_t -> flex_t -> solution) = fun env -> @@ -7645,7 +7651,7 @@ and (solve_t_flex_flex : Prims.op_Negation uu___) in let run_meta_arg_tac_and_try_again flex = let uv = flex_uvar flex in - let t = run_meta_arg_tac uv in + let t = run_meta_arg_tac env uv in (let uu___1 = FStar_Compiler_Effect.op_Less_Bar (debug wl) (FStar_Options.Other "Rel") in @@ -14220,16 +14226,15 @@ let (try_solve_deferred_constraints : match (i.FStar_TypeChecker_Common.imp_uvar).FStar_Syntax_Syntax.ctx_uvar_meta with | FStar_Pervasives_Native.Some - (FStar_Syntax_Syntax.Ctx_uvar_meta_tac - (uu___2, tac)) -> - let uu___3 = + (FStar_Syntax_Syntax.Ctx_uvar_meta_tac tac) -> + let uu___2 = FStar_Syntax_Util.head_and_args_full tac in - (match uu___3 with - | (head, uu___4) -> - let uu___5 = + (match uu___2 with + | (head, uu___3) -> + let uu___4 = FStar_Syntax_Util.is_fvar FStar_Parser_Const.tcresolve_lid head in - if uu___5 + if uu___4 then let goal_type = FStar_Syntax_Util.ctx_uvar_typ @@ -15473,7 +15478,7 @@ let (resolve_implicits' : (match uu___6 with | FStar_Pervasives_Native.Some (FStar_Syntax_Syntax.Ctx_uvar_meta_tac - meta) -> + tac) -> let env1 = { FStar_TypeChecker_Env.solver = @@ -15617,8 +15622,6 @@ let (resolve_implicits' : = (env.FStar_TypeChecker_Env.core_check) } in - let tac = - FStar_Pervasives_Native.snd meta in let typ = FStar_Syntax_Util.ctx_uvar_typ ctx_u in @@ -15685,13 +15688,14 @@ let (resolve_implicits' : | FStar_Pervasives_Native.None -> let t = - run_meta_arg_tac ctx_u in + run_meta_arg_tac env1 + ctx_u in (meta_arg_cache_result tac env1 typ t; solve_with t) else (let t = - run_meta_arg_tac ctx_u in + run_meta_arg_tac env1 ctx_u in solve_with t))) | uu___5 when unresolved ctx_u -> until_fixpoint diff --git a/ocaml/fstar-lib/generated/FStar_TypeChecker_TcTerm.ml b/ocaml/fstar-lib/generated/FStar_TypeChecker_TcTerm.ml index ca67bc30eab..310f2390b4d 100644 --- a/ocaml/fstar-lib/generated/FStar_TypeChecker_TcTerm.ml +++ b/ocaml/fstar-lib/generated/FStar_TypeChecker_TcTerm.ml @@ -7503,14 +7503,8 @@ and (check_application_args : FStar_Syntax_Syntax.t_unit env tau1 in (match uu___7 with | (tau2, uu___8, g_tau) -> - let uu___9 = - let uu___10 = - let uu___11 = - FStar_Compiler_Dyn.mkdyn env in - (uu___11, tau2) in - FStar_Syntax_Syntax.Ctx_uvar_meta_tac - uu___10 in - (uu___9, g_tau)) + ((FStar_Syntax_Syntax.Ctx_uvar_meta_tac + tau2), g_tau)) | (FStar_Pervasives_Native.Some (FStar_Syntax_Syntax.Implicit uu___6), attr::uu___7) -> @@ -7558,7 +7552,7 @@ and (check_application_args : let is_typeclass = match ctx_uvar_meta with | FStar_Syntax_Syntax.Ctx_uvar_meta_tac - (uu___8, tau) -> + tau -> FStar_Syntax_Util.is_fvar FStar_Parser_Const.tcresolve_lid tau diff --git a/ocaml/fstar-lib/generated/FStar_TypeChecker_Util.ml b/ocaml/fstar-lib/generated/FStar_TypeChecker_Util.ml index b129fd008c7..81e9ae05ca4 100644 --- a/ocaml/fstar-lib/generated/FStar_TypeChecker_Util.ml +++ b/ocaml/fstar-lib/generated/FStar_TypeChecker_Util.ml @@ -6712,10 +6712,7 @@ let (maybe_instantiate : match (qual, attrs) with | (FStar_Pervasives_Native.Some (FStar_Syntax_Syntax.Meta tau), uu___5) -> - let uu___6 = - let uu___7 = FStar_Compiler_Dyn.mkdyn env in - (uu___7, tau) in - FStar_Syntax_Syntax.Ctx_uvar_meta_tac uu___6 + FStar_Syntax_Syntax.Ctx_uvar_meta_tac tau | (uu___5, attr::uu___6) -> FStar_Syntax_Syntax.Ctx_uvar_meta_attr attr | uu___5 -> @@ -6724,8 +6721,7 @@ let (maybe_instantiate : let msg = let is_typeclass = match meta_t with - | FStar_Syntax_Syntax.Ctx_uvar_meta_tac - (uu___5, tau) -> + | FStar_Syntax_Syntax.Ctx_uvar_meta_tac tau -> FStar_Syntax_Util.is_fvar FStar_Parser_Const.tcresolve_lid tau | uu___5 -> false in