From 43aae46a34b60ddf940d094caa9a7860ad1b9853 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Mon, 26 Aug 2024 15:48:35 -0700 Subject: [PATCH 1/3] Tc: refactor implicit instantiation into a single function --- src/syntax/FStar.Syntax.Subst.fst | 1 + src/syntax/FStar.Syntax.Subst.fsti | 1 + src/typechecker/FStar.TypeChecker.TcTerm.fst | 95 +++++--------------- src/typechecker/FStar.TypeChecker.Util.fst | 93 +++++++++++-------- src/typechecker/FStar.TypeChecker.Util.fsti | 2 + 5 files changed, 82 insertions(+), 110 deletions(-) diff --git a/src/syntax/FStar.Syntax.Subst.fst b/src/syntax/FStar.Syntax.Subst.fst index 170ee7d72ae..9929af5cbb0 100644 --- a/src/syntax/FStar.Syntax.Subst.fst +++ b/src/syntax/FStar.Syntax.Subst.fst @@ -294,6 +294,7 @@ let subst_binder' s b = b.binder_positivity (b.binder_attrs |> List.map (subst' s)) +let subst_binder s (b:binder) = subst_binder' ([s], NoUseRange) b let subst_binders' s bs = bs |> List.mapi (fun i b -> diff --git a/src/syntax/FStar.Syntax.Subst.fsti b/src/syntax/FStar.Syntax.Subst.fsti index a1c5ca27dca..647898fba76 100644 --- a/src/syntax/FStar.Syntax.Subst.fsti +++ b/src/syntax/FStar.Syntax.Subst.fsti @@ -31,6 +31,7 @@ val subst_aqual: list subst_elt -> aqual -> aqual val subst_ascription: list subst_elt -> ascription -> ascription val subst_decreasing_order: list subst_elt -> decreases_order -> decreases_order +val subst_binder: list subst_elt -> binder -> binder val subst_binders: list subst_elt -> binders -> binders val subst_residual_comp:list subst_elt -> residual_comp -> residual_comp val compress: term -> term diff --git a/src/typechecker/FStar.TypeChecker.TcTerm.fst b/src/typechecker/FStar.TypeChecker.TcTerm.fst index de952d45859..8e51bdfb156 100644 --- a/src/typechecker/FStar.TypeChecker.TcTerm.fst +++ b/src/typechecker/FStar.TypeChecker.TcTerm.fst @@ -2741,32 +2741,15 @@ and check_application_args env head (chead:comp) ghead args expected_topt : term bs (* formal parameters *) args (* remaining actual arguments *) : (term & lcomp & guard_t) = - (* We follow the exact same procedure as for instantiating an implicit, - * except that we keep track of the (uvar, env, metaprogram) pair in the environment - * so we can later come back to the implicit and, if it wasn't solved by unification, - * run the metaprogram on it. - * - * Why don't we run the metaprogram here? At this stage, it's very likely that `t` - * is full of unresolved uvars, and it wouldn't be a whole lot useful to try - * to find an instance for it. We might not even be able to, since instances - * are for concrete types. - *) - let instantiate_one_meta_and_go b rest_bs args = - let {binder_bv=x;binder_qual=qual;binder_attrs=attrs} = b in - let ctx_uvar_meta, g_tau_or_attr = - match qual, attrs with - | 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 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 - Ctx_uvar_meta_attr attr, g_attr - | _ -> failwith "Impossible, match is under a guard" - in - let t = SS.subst subst x.sort in - let t, g_ex = check_no_escape (Some head) env fvs t in + let (++) = Env.conj_guard in + let instantiate_one_and_go b rest_bs args = + (* We compute a range by combining the range of the head + * and the last argument we checked (if any). This is such that + * if we instantiate an implicit for `f ()` (of type `#x:a -> ...), + * we give it the range of `f ()` instead of just the range for `f`. + * See issue #2021. This is only for the use range, we take + * the def range from the head, so the 'see also' should still + * point to the definition of the head. *) let r = match outargs with | [] -> head.pos | ((t, _), _, _)::_ -> @@ -2774,60 +2757,26 @@ and check_application_args env head (chead:comp) ghead args expected_topt : term (Range.union_rng (Range.use_range head.pos) (Range.use_range t.pos)) in - let varg, _, implicits = - 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 - let arg = varg, aq in - let guard = List.fold_right Env.conj_guard [g_ex; g; g_tau_or_attr] implicits in - tc_args head_info (subst, (arg, None, S.mk_Total t |> TcComm.lcomp_of_comp)::outargs, arg::arg_rets, guard, fvs) rest_bs args + let b = SS.subst_binder subst b in + let tm, ty, aq, g' = TcUtil.instantiate_one_binder env r b in + let ty, g_ex = check_no_escape (Some head) env fvs ty in + let guard = g ++ g' ++ g_ex in + let arg = tm, aq in + let subst = NT(b.binder_bv, tm)::subst in + tc_args head_info (subst, (arg, None, S.mk_Total ty |> TcComm.lcomp_of_comp)::outargs, arg::arg_rets, guard, fvs) rest_bs args in match bs, args with - | ({binder_bv=x;binder_qual=Some (Implicit _);binder_attrs=[]})::rest, - (_, None)::_ -> (* instantiate an implicit arg that's not associated with a tactic, i.e. no Meta or attrs *) - let t = SS.subst subst x.sort in - let t, g_ex = check_no_escape (Some head) env fvs t in - (* We compute a range by combining the range of the head - * and the last argument we checked (if any). This is such that - * if we instantiate an implicit for `f ()` (of type `#x:a -> ...), - * we give it the range of `f ()` instead of just the range for `f`. - * See issue #2021. This is only for the use range, we take - * the def range from the head, so the 'see also' should still - * point to the definition of the head. *) - let r = match outargs with - | [] -> head.pos - | ((t, _), _, _)::_ -> - Range.range_of_rng (Range.def_range head.pos) - (Range.union_rng (Range.use_range head.pos) - (Range.use_range t.pos)) - in - let varg, _, implicits = TcUtil.new_implicit_var "Instantiating implicit argument in application" r env t in //new_uvar env t in - let subst = NT(x, varg)::subst in - let arg = varg, S.as_aqual_implicit true in - let guard = List.fold_right Env.conj_guard [g_ex; g] implicits in - tc_args head_info (subst, (arg, None, S.mk_Total t |> TcComm.lcomp_of_comp)::outargs, arg::arg_rets, guard, fvs) rest args - - | ({binder_bv=x;binder_qual=qual;binder_attrs=attrs})::rest, - (_, None)::_ - when (TcUtil.maybe_implicit_with_meta_or_attr qual attrs) -> (* instantiate a meta arg *) - instantiate_one_meta_and_go (List.hd bs) rest args + (* Expect an implicit but user provided a concrete argument, instantiate the implicit. *) + | ({binder_bv=x;binder_qual=Some (Implicit _)})::rest, (_, None)::_ + | ({binder_bv=x;binder_qual=Some (Meta _)})::rest, (_, None)::_ + -> + instantiate_one_and_go (List.hd bs) rest args (* User provided a _ for a meta arg, keep the meta for the unknown. *) | ({binder_bv=x;binder_qual=Some (Meta tau);binder_attrs=b_attrs})::rest, ({n = Tm_unknown}, Some {aqual_implicit=true})::rest' -> - instantiate_one_meta_and_go (List.hd bs) rest rest' (* NB: rest' instead of args, we consume the _ *) + instantiate_one_and_go (List.hd bs) rest rest' (* NB: rest' instead of args, we consume the _ *) | ({binder_bv=x;binder_qual=bqual;binder_attrs=b_attrs})::rest, (e, aq)::rest' -> (* a concrete argument *) let aq = check_expected_aqual_for_binder aq (List.hd bs) e.pos in diff --git a/src/typechecker/FStar.TypeChecker.Util.fst b/src/typechecker/FStar.TypeChecker.Util.fst index 9e03295495a..d1895fe8897 100644 --- a/src/typechecker/FStar.TypeChecker.Util.fst +++ b/src/typechecker/FStar.TypeChecker.Util.fst @@ -2833,6 +2833,54 @@ let maybe_implicit_with_meta_or_attr aq (attrs:list attribute) = | Some (Implicit _), _::_ -> true | _ -> false +(* Instantiation of implicit arguments (meta or implicit) + * + * For meta arguments, we follow the exact same procedure as for instantiating an implicit, + * except that we keep track of the (uvar, env, metaprogram) triple in the environment + * so we can later come back to the implicit and, if it wasn't solved by unification, + * run the metaprogram on it. + * + * Why don't we run the metaprogram here? At this stage, it's very likely that `t` + * is full of unresolved uvars, and it wouldn't be a whole lot useful to try + * to find an instance for it. We might not even be able to, since instances + * are for concrete types. + *) +let instantiate_one_binder (env:env_t) (r:Range.range) (b:binder) : term & typ & aqual & guard_t = + if Debug.high () then + BU.print1 "instantiate_one_binder: Instantiating implicit binder %s\n" (show b); + let (++) = Env.conj_guard in + let { binder_bv=x; binder_qual=qual; binder_attrs=attrs } = b in + let ctx_uvar_meta = + match qual, attrs with + | Some (Meta tau), _ -> + Some (Ctx_uvar_meta_tac tau) + | Some (Implicit _), attr::_ -> + Some (Ctx_uvar_meta_attr attr) + | _, _ -> + None + in + let t = x.sort in + let varg, _, implicits = + let msg = + let is_typeclass = + match ctx_uvar_meta with + | Some (Ctx_uvar_meta_tac tau) -> U.is_fvar C.tcresolve_lid tau + | _ -> false + in + if is_typeclass then "Typeclass constraint argument" + else if Some? ctx_uvar_meta then "Instantiating meta argument" + else "Instantiating implicit argument" + in + Env.new_implicit_var_aux msg r env t Strict ctx_uvar_meta + in + let aq = U.aqual_of_binder b in + let arg = varg, aq in + + let r = varg, t, aq, implicits in + if Debug.high () then + BU.print1 "instantiate_one_binder: result = %s\n" (show (r._1, r._2)); + r + let maybe_instantiate (env:Env.env) (e:term) (t:typ) : term & typ & guard_t = let torig = SS.compress t in if not env.instantiate_imp @@ -2890,44 +2938,15 @@ let maybe_instantiate (env:Env.env) (e:term) (t:typ) : term & typ & guard_t = let rec aux (subst:list subst_elt) inst_n bs = match inst_n, bs with | Some 0, _ -> [], bs, subst, Env.trivial_guard //no more instantiations to do - | _, ({binder_bv=x; binder_qual=Some (Implicit _);binder_attrs=[]})::rest -> - let t = SS.subst subst x.sort in - let v, _, g = new_implicit_var "Instantiation of implicit argument" e.pos env t in - if Debug.high () then - BU.print1 "maybe_instantiate: Instantiating implicit with %s\n" (show v); - let subst = NT(x, v)::subst in - let aq = U.aqual_of_binder (List.hd bs) in - let args, bs, subst, g' = aux subst (decr_inst inst_n) rest in - (v, aq)::args, bs, subst, Env.conj_guard g g' - - | _, ({binder_bv=x; binder_qual=qual; binder_attrs=attrs})::rest - when maybe_implicit_with_meta_or_attr qual attrs -> - let t = SS.subst subst x.sort in - let meta_t = - match qual, attrs with - | 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 - | _ -> 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 Debug.high () then - BU.print1 "maybe_instantiate: Instantiating meta argument with %s\n" (show v); - let subst = NT(x, v)::subst in - let aq = U.aqual_of_binder (List.hd bs) in + | _, {binder_qual = Some (Implicit _)} ::rest + | _, {binder_qual = Some (Meta _)} ::rest + | _, {binder_attrs = _::_} :: rest -> + let b = List.hd bs in + let b = SS.subst_binder subst b in + let tm, ty, aq, g = instantiate_one_binder env e.pos b in + let subst = NT(b.binder_bv, tm)::subst in let args, bs, subst, g' = aux subst (decr_inst inst_n) rest in - (v, aq)::args, bs, subst, Env.conj_guard g g' + (tm, aq)::args, bs, subst, Env.conj_guard g g' | _, bs -> [], bs, subst, Env.trivial_guard in diff --git a/src/typechecker/FStar.TypeChecker.Util.fsti b/src/typechecker/FStar.TypeChecker.Util.fsti index a9a8be5460f..dc9b58ef643 100644 --- a/src/typechecker/FStar.TypeChecker.Util.fsti +++ b/src/typechecker/FStar.TypeChecker.Util.fsti @@ -48,6 +48,8 @@ val decorated_pattern_as_term: pat -> list bv & term //instantiation of implicits val maybe_implicit_with_meta_or_attr: bqual -> list attribute -> bool + +val instantiate_one_binder (env:env_t) (r:Range.range) (b:binder) : term & typ & aqual & guard_t val maybe_instantiate : env -> term -> typ -> (term & typ & guard_t) //operations on computation types From 025dfd6a2bf38c77809dbb47fb27b70dc3ee909c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Mon, 26 Aug 2024 15:53:38 -0700 Subject: [PATCH 2/3] snap --- .../fstar-lib/generated/FStar_Syntax_Subst.ml | 4 + .../generated/FStar_TypeChecker_TcTerm.ml | 249 +++++------------- .../generated/FStar_TypeChecker_Util.ml | 243 ++++++++++------- 3 files changed, 218 insertions(+), 278 deletions(-) diff --git a/ocaml/fstar-lib/generated/FStar_Syntax_Subst.ml b/ocaml/fstar-lib/generated/FStar_Syntax_Subst.ml index 2a4e8ae9518..c1c70a751a6 100644 --- a/ocaml/fstar-lib/generated/FStar_Syntax_Subst.ml +++ b/ocaml/fstar-lib/generated/FStar_Syntax_Subst.ml @@ -540,6 +540,10 @@ let (subst_binder' : FStar_Compiler_List.map (subst' s) b.FStar_Syntax_Syntax.binder_attrs in FStar_Syntax_Syntax.mk_binder_with_attrs uu___ uu___1 b.FStar_Syntax_Syntax.binder_positivity uu___2 +let (subst_binder : + FStar_Syntax_Syntax.subst_elt Prims.list -> + FStar_Syntax_Syntax.binder -> FStar_Syntax_Syntax.binder) + = fun s -> fun b -> subst_binder' ([s], FStar_Syntax_Syntax.NoUseRange) b let (subst_binders' : (FStar_Syntax_Syntax.subst_elt Prims.list Prims.list * FStar_Syntax_Syntax.maybe_set_use_range) -> diff --git a/ocaml/fstar-lib/generated/FStar_TypeChecker_TcTerm.ml b/ocaml/fstar-lib/generated/FStar_TypeChecker_TcTerm.ml index 970bd3f577e..85089073da9 100644 --- a/ocaml/fstar-lib/generated/FStar_TypeChecker_TcTerm.ml +++ b/ocaml/fstar-lib/generated/FStar_TypeChecker_TcTerm.ml @@ -7491,197 +7491,78 @@ and (check_application_args : let rec tc_args head_info uu___1 bs args1 = match uu___1 with | (subst, outargs, arg_rets, g, fvs) -> - let instantiate_one_meta_and_go b rest_bs args2 = - let uu___2 = b in + let op_Plus_Plus = FStar_TypeChecker_Env.conj_guard in + let instantiate_one_and_go b rest_bs args2 = + let r1 = + match outargs with + | [] -> head.FStar_Syntax_Syntax.pos + | ((t, uu___2), uu___3, uu___4)::uu___5 -> + let uu___6 = + FStar_Compiler_Range_Type.def_range + head.FStar_Syntax_Syntax.pos in + let uu___7 = + let uu___8 = + FStar_Compiler_Range_Type.use_range + head.FStar_Syntax_Syntax.pos in + let uu___9 = + FStar_Compiler_Range_Type.use_range + t.FStar_Syntax_Syntax.pos in + FStar_Compiler_Range_Ops.union_rng uu___8 + uu___9 in + FStar_Compiler_Range_Type.range_of_rng uu___6 + uu___7 in + let b1 = FStar_Syntax_Subst.subst_binder subst b in + let uu___2 = + FStar_TypeChecker_Util.instantiate_one_binder env r1 + b1 in match uu___2 with - | { FStar_Syntax_Syntax.binder_bv = x; - FStar_Syntax_Syntax.binder_qual = qual; - FStar_Syntax_Syntax.binder_positivity = uu___3; - FStar_Syntax_Syntax.binder_attrs = attrs;_} -> - let uu___4 = - match (qual, attrs) with - | (FStar_Pervasives_Native.Some - (FStar_Syntax_Syntax.Meta tau), uu___5) -> - let tau1 = - FStar_Syntax_Subst.subst subst tau in - let uu___6 = - tc_tactic FStar_Syntax_Syntax.t_unit - FStar_Syntax_Syntax.t_unit env tau1 in - (match uu___6 with - | (tau2, uu___7, g_tau) -> - ((FStar_Syntax_Syntax.Ctx_uvar_meta_tac - tau2), g_tau)) - | (FStar_Pervasives_Native.Some - (FStar_Syntax_Syntax.Implicit uu___5), - attr::uu___6) -> - let attr1 = - FStar_Syntax_Subst.subst subst attr in - let uu___7 = tc_tot_or_gtot_term env attr1 in - (match uu___7 with - | (attr2, uu___8, g_attr) -> - ((FStar_Syntax_Syntax.Ctx_uvar_meta_attr - attr2), g_attr)) - | uu___5 -> - FStar_Compiler_Effect.failwith - "Impossible, match is under a guard" in - (match uu___4 with - | (ctx_uvar_meta, g_tau_or_attr) -> - let t = - FStar_Syntax_Subst.subst subst - x.FStar_Syntax_Syntax.sort in - let uu___5 = - check_no_escape - (FStar_Pervasives_Native.Some head) env - fvs t in - (match uu___5 with - | (t1, g_ex) -> - let r1 = - match outargs with - | [] -> head.FStar_Syntax_Syntax.pos - | ((t2, uu___6), uu___7, uu___8)::uu___9 - -> - let uu___10 = - FStar_Compiler_Range_Type.def_range - head.FStar_Syntax_Syntax.pos in - let uu___11 = - let uu___12 = - FStar_Compiler_Range_Type.use_range - head.FStar_Syntax_Syntax.pos in - let uu___13 = - FStar_Compiler_Range_Type.use_range - t2.FStar_Syntax_Syntax.pos in - FStar_Compiler_Range_Ops.union_rng - uu___12 uu___13 in - FStar_Compiler_Range_Type.range_of_rng - uu___10 uu___11 in - let uu___6 = - let msg = - let is_typeclass = - match ctx_uvar_meta with - | FStar_Syntax_Syntax.Ctx_uvar_meta_tac - tau -> - FStar_Syntax_Util.is_fvar - FStar_Parser_Const.tcresolve_lid - tau - | uu___7 -> false in - if is_typeclass - then "Typeclass constraint argument" - else - "Instantiating meta argument in application" in - FStar_TypeChecker_Env.new_implicit_var_aux - msg r1 env t1 - FStar_Syntax_Syntax.Strict - (FStar_Pervasives_Native.Some - ctx_uvar_meta) in - (match uu___6 with - | (varg, uu___7, implicits) -> - let subst1 = - (FStar_Syntax_Syntax.NT (x, varg)) - :: subst in - let aq = - let uu___8 = - FStar_Compiler_List.hd bs in - FStar_Syntax_Util.aqual_of_binder - uu___8 in - let arg = (varg, aq) in - let guard = - FStar_Compiler_List.fold_right - FStar_TypeChecker_Env.conj_guard - [g_ex; g; g_tau_or_attr] - implicits in - let uu___8 = - let uu___9 = - let uu___10 = - let uu___11 = - let uu___12 = - FStar_Syntax_Syntax.mk_Total - t1 in - FStar_TypeChecker_Common.lcomp_of_comp - uu___12 in - (arg, - FStar_Pervasives_Native.None, - uu___11) in - uu___10 :: outargs in - (subst1, uu___9, (arg :: - arg_rets), guard, fvs) in - tc_args head_info uu___8 rest_bs - args2))) in + | (tm, ty, aq, g') -> + let uu___3 = + check_no_escape + (FStar_Pervasives_Native.Some head) env fvs ty in + (match uu___3 with + | (ty1, g_ex) -> + let guard = + let uu___4 = op_Plus_Plus g g' in + op_Plus_Plus uu___4 g_ex in + let arg = (tm, aq) in + let subst1 = + (FStar_Syntax_Syntax.NT + ((b1.FStar_Syntax_Syntax.binder_bv), tm)) + :: subst in + let uu___4 = + let uu___5 = + let uu___6 = + let uu___7 = + let uu___8 = + FStar_Syntax_Syntax.mk_Total ty1 in + FStar_TypeChecker_Common.lcomp_of_comp + uu___8 in + (arg, FStar_Pervasives_Native.None, + uu___7) in + uu___6 :: outargs in + (subst1, uu___5, (arg :: arg_rets), guard, + fvs) in + tc_args head_info uu___4 rest_bs args2) in (match (bs, args1) with | ({ FStar_Syntax_Syntax.binder_bv = x; FStar_Syntax_Syntax.binder_qual = FStar_Pervasives_Native.Some (FStar_Syntax_Syntax.Implicit uu___2); FStar_Syntax_Syntax.binder_positivity = uu___3; - FStar_Syntax_Syntax.binder_attrs = [];_}::rest, - (uu___4, FStar_Pervasives_Native.None)::uu___5) -> - let t = - FStar_Syntax_Subst.subst subst - x.FStar_Syntax_Syntax.sort in - let uu___6 = - check_no_escape - (FStar_Pervasives_Native.Some head) env fvs t in - (match uu___6 with - | (t1, g_ex) -> - let r1 = - match outargs with - | [] -> head.FStar_Syntax_Syntax.pos - | ((t2, uu___7), uu___8, uu___9)::uu___10 -> - let uu___11 = - FStar_Compiler_Range_Type.def_range - head.FStar_Syntax_Syntax.pos in - let uu___12 = - let uu___13 = - FStar_Compiler_Range_Type.use_range - head.FStar_Syntax_Syntax.pos in - let uu___14 = - FStar_Compiler_Range_Type.use_range - t2.FStar_Syntax_Syntax.pos in - FStar_Compiler_Range_Ops.union_rng - uu___13 uu___14 in - FStar_Compiler_Range_Type.range_of_rng - uu___11 uu___12 in - let uu___7 = - FStar_TypeChecker_Util.new_implicit_var - "Instantiating implicit argument in application" - r1 env t1 in - (match uu___7 with - | (varg, uu___8, implicits) -> - let subst1 = - (FStar_Syntax_Syntax.NT (x, varg)) :: - subst in - let arg = - let uu___9 = - FStar_Syntax_Syntax.as_aqual_implicit - true in - (varg, uu___9) in - let guard = - FStar_Compiler_List.fold_right - FStar_TypeChecker_Env.conj_guard - [g_ex; g] implicits in - let uu___9 = - let uu___10 = - let uu___11 = - let uu___12 = - let uu___13 = - FStar_Syntax_Syntax.mk_Total t1 in - FStar_TypeChecker_Common.lcomp_of_comp - uu___13 in - (arg, FStar_Pervasives_Native.None, - uu___12) in - uu___11 :: outargs in - (subst1, uu___10, (arg :: arg_rets), - guard, fvs) in - tc_args head_info uu___9 rest args1)) + FStar_Syntax_Syntax.binder_attrs = uu___4;_}::rest, + (uu___5, FStar_Pervasives_Native.None)::uu___6) -> + let uu___7 = FStar_Compiler_List.hd bs in + instantiate_one_and_go uu___7 rest args1 | ({ FStar_Syntax_Syntax.binder_bv = x; - FStar_Syntax_Syntax.binder_qual = qual; - FStar_Syntax_Syntax.binder_positivity = uu___2; - FStar_Syntax_Syntax.binder_attrs = attrs;_}::rest, - (uu___3, FStar_Pervasives_Native.None)::uu___4) when - FStar_TypeChecker_Util.maybe_implicit_with_meta_or_attr - qual attrs - -> - let uu___5 = FStar_Compiler_List.hd bs in - instantiate_one_meta_and_go uu___5 rest args1 + FStar_Syntax_Syntax.binder_qual = + FStar_Pervasives_Native.Some + (FStar_Syntax_Syntax.Meta uu___2); + FStar_Syntax_Syntax.binder_positivity = uu___3; + FStar_Syntax_Syntax.binder_attrs = uu___4;_}::rest, + (uu___5, FStar_Pervasives_Native.None)::uu___6) -> + let uu___7 = FStar_Compiler_List.hd bs in + instantiate_one_and_go uu___7 rest args1 | ({ FStar_Syntax_Syntax.binder_bv = x; FStar_Syntax_Syntax.binder_qual = FStar_Pervasives_Native.Some @@ -7699,7 +7580,7 @@ and (check_application_args : FStar_Syntax_Syntax.aqual_attributes = uu___6;_})::rest') -> let uu___7 = FStar_Compiler_List.hd bs in - instantiate_one_meta_and_go uu___7 rest rest' + instantiate_one_and_go uu___7 rest rest' | ({ FStar_Syntax_Syntax.binder_bv = x; FStar_Syntax_Syntax.binder_qual = bqual; FStar_Syntax_Syntax.binder_positivity = uu___2; diff --git a/ocaml/fstar-lib/generated/FStar_TypeChecker_Util.ml b/ocaml/fstar-lib/generated/FStar_TypeChecker_Util.ml index 3a361639b32..b3ab2eff5fc 100644 --- a/ocaml/fstar-lib/generated/FStar_TypeChecker_Util.ml +++ b/ocaml/fstar-lib/generated/FStar_TypeChecker_Util.ml @@ -6465,6 +6465,82 @@ let (maybe_implicit_with_meta_or_attr : | (FStar_Pervasives_Native.Some (FStar_Syntax_Syntax.Implicit uu___), uu___1::uu___2) -> true | uu___ -> false +let (instantiate_one_binder : + FStar_TypeChecker_Env.env_t -> + FStar_Compiler_Range_Type.range -> + FStar_Syntax_Syntax.binder -> + (FStar_Syntax_Syntax.term * FStar_Syntax_Syntax.typ * + FStar_Syntax_Syntax.aqual * FStar_TypeChecker_Env.guard_t)) + = + fun env -> + fun r -> + fun b -> + (let uu___1 = FStar_Compiler_Debug.high () in + if uu___1 + then + let uu___2 = + FStar_Class_Show.show FStar_Syntax_Print.showable_binder b in + FStar_Compiler_Util.print1 + "instantiate_one_binder: Instantiating implicit binder %s\n" + uu___2 + else ()); + (let op_Plus_Plus = FStar_TypeChecker_Env.conj_guard in + let uu___1 = b in + match uu___1 with + | { FStar_Syntax_Syntax.binder_bv = x; + FStar_Syntax_Syntax.binder_qual = qual; + FStar_Syntax_Syntax.binder_positivity = uu___2; + FStar_Syntax_Syntax.binder_attrs = attrs;_} -> + let ctx_uvar_meta = + match (qual, attrs) with + | (FStar_Pervasives_Native.Some (FStar_Syntax_Syntax.Meta + tau), uu___3) -> + FStar_Pervasives_Native.Some + (FStar_Syntax_Syntax.Ctx_uvar_meta_tac tau) + | (FStar_Pervasives_Native.Some (FStar_Syntax_Syntax.Implicit + uu___3), attr::uu___4) -> + FStar_Pervasives_Native.Some + (FStar_Syntax_Syntax.Ctx_uvar_meta_attr attr) + | (uu___3, uu___4) -> FStar_Pervasives_Native.None in + let t = x.FStar_Syntax_Syntax.sort in + let uu___3 = + let msg = + let is_typeclass = + match ctx_uvar_meta with + | FStar_Pervasives_Native.Some + (FStar_Syntax_Syntax.Ctx_uvar_meta_tac tau) -> + FStar_Syntax_Util.is_fvar + FStar_Parser_Const.tcresolve_lid tau + | uu___4 -> false in + if is_typeclass + then "Typeclass constraint argument" + else + if FStar_Pervasives_Native.uu___is_Some ctx_uvar_meta + then "Instantiating meta argument" + else "Instantiating implicit argument" in + FStar_TypeChecker_Env.new_implicit_var_aux msg r env t + FStar_Syntax_Syntax.Strict ctx_uvar_meta in + (match uu___3 with + | (varg, uu___4, implicits) -> + let aq = FStar_Syntax_Util.aqual_of_binder b in + let arg = (varg, aq) in + let r1 = (varg, t, aq, implicits) in + ((let uu___6 = FStar_Compiler_Debug.high () in + if uu___6 + then + let uu___7 = + FStar_Class_Show.show + (FStar_Class_Show.show_tuple2 + FStar_Syntax_Print.showable_term + FStar_Syntax_Print.showable_term) + ((FStar_Pervasives_Native.__proj__Mktuple4__item___1 + r1), + (FStar_Pervasives_Native.__proj__Mktuple4__item___2 + r1)) in + FStar_Compiler_Util.print1 + "instantiate_one_binder: result = %s\n" uu___7 + else ()); + r1))) let (maybe_instantiate : FStar_TypeChecker_Env.env -> FStar_Syntax_Syntax.term -> @@ -6601,105 +6677,84 @@ let (maybe_instantiate : ([], bs2, subst, FStar_TypeChecker_Env.trivial_guard) | (uu___3, - { FStar_Syntax_Syntax.binder_bv = x; + { FStar_Syntax_Syntax.binder_bv = uu___4; FStar_Syntax_Syntax.binder_qual = FStar_Pervasives_Native.Some - (FStar_Syntax_Syntax.Implicit uu___4); - FStar_Syntax_Syntax.binder_positivity = uu___5; - FStar_Syntax_Syntax.binder_attrs = [];_}::rest) + (FStar_Syntax_Syntax.Implicit uu___5); + FStar_Syntax_Syntax.binder_positivity = uu___6; + FStar_Syntax_Syntax.binder_attrs = uu___7;_}::rest) -> - let t2 = - FStar_Syntax_Subst.subst subst - x.FStar_Syntax_Syntax.sort in - let uu___6 = - new_implicit_var - "Instantiation of implicit argument" - e.FStar_Syntax_Syntax.pos env t2 in - (match uu___6 with - | (v, uu___7, g) -> - ((let uu___9 = FStar_Compiler_Debug.high () in - if uu___9 - then - let uu___10 = - FStar_Class_Show.show - FStar_Syntax_Print.showable_term v in - FStar_Compiler_Util.print1 - "maybe_instantiate: Instantiating implicit with %s\n" - uu___10 - else ()); - (let subst1 = - (FStar_Syntax_Syntax.NT (x, v)) :: subst in - let aq = - let uu___9 = FStar_Compiler_List.hd bs2 in - FStar_Syntax_Util.aqual_of_binder uu___9 in - let uu___9 = - aux subst1 (decr_inst inst_n) rest in - match uu___9 with - | (args, bs3, subst2, g') -> - let uu___10 = - FStar_TypeChecker_Env.conj_guard g g' in - (((v, aq) :: args), bs3, subst2, - uu___10)))) + let b = FStar_Compiler_List.hd bs2 in + let b1 = FStar_Syntax_Subst.subst_binder subst b in + let uu___8 = + instantiate_one_binder env + e.FStar_Syntax_Syntax.pos b1 in + (match uu___8 with + | (tm, ty, aq, g) -> + let subst1 = + (FStar_Syntax_Syntax.NT + ((b1.FStar_Syntax_Syntax.binder_bv), tm)) + :: subst in + let uu___9 = + aux subst1 (decr_inst inst_n) rest in + (match uu___9 with + | (args, bs3, subst2, g') -> + let uu___10 = + FStar_TypeChecker_Env.conj_guard g g' in + (((tm, aq) :: args), bs3, subst2, + uu___10))) | (uu___3, - { FStar_Syntax_Syntax.binder_bv = x; - FStar_Syntax_Syntax.binder_qual = qual; - FStar_Syntax_Syntax.binder_positivity = uu___4; - FStar_Syntax_Syntax.binder_attrs = attrs;_}::rest) - when maybe_implicit_with_meta_or_attr qual attrs + { FStar_Syntax_Syntax.binder_bv = uu___4; + FStar_Syntax_Syntax.binder_qual = + FStar_Pervasives_Native.Some + (FStar_Syntax_Syntax.Meta uu___5); + FStar_Syntax_Syntax.binder_positivity = uu___6; + FStar_Syntax_Syntax.binder_attrs = uu___7;_}::rest) -> - let t2 = - FStar_Syntax_Subst.subst subst - x.FStar_Syntax_Syntax.sort in - let meta_t = - match (qual, attrs) with - | (FStar_Pervasives_Native.Some - (FStar_Syntax_Syntax.Meta tau), uu___5) -> - FStar_Syntax_Syntax.Ctx_uvar_meta_tac tau - | (uu___5, attr::uu___6) -> - FStar_Syntax_Syntax.Ctx_uvar_meta_attr attr - | uu___5 -> - FStar_Compiler_Effect.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 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 msg - e.FStar_Syntax_Syntax.pos env t2 - FStar_Syntax_Syntax.Strict - (FStar_Pervasives_Native.Some meta_t) in - (match uu___5 with - | (v, uu___6, g) -> - ((let uu___8 = FStar_Compiler_Debug.high () in - if uu___8 - then - let uu___9 = - FStar_Class_Show.show - FStar_Syntax_Print.showable_term v in - FStar_Compiler_Util.print1 - "maybe_instantiate: Instantiating meta argument with %s\n" - uu___9 - else ()); - (let subst1 = - (FStar_Syntax_Syntax.NT (x, v)) :: subst in - let aq = - let uu___8 = FStar_Compiler_List.hd bs2 in - FStar_Syntax_Util.aqual_of_binder uu___8 in - let uu___8 = - aux subst1 (decr_inst inst_n) rest in - match uu___8 with - | (args, bs3, subst2, g') -> - let uu___9 = - FStar_TypeChecker_Env.conj_guard g g' in - (((v, aq) :: args), bs3, subst2, - uu___9)))) + let b = FStar_Compiler_List.hd bs2 in + let b1 = FStar_Syntax_Subst.subst_binder subst b in + let uu___8 = + instantiate_one_binder env + e.FStar_Syntax_Syntax.pos b1 in + (match uu___8 with + | (tm, ty, aq, g) -> + let subst1 = + (FStar_Syntax_Syntax.NT + ((b1.FStar_Syntax_Syntax.binder_bv), tm)) + :: subst in + let uu___9 = + aux subst1 (decr_inst inst_n) rest in + (match uu___9 with + | (args, bs3, subst2, g') -> + let uu___10 = + FStar_TypeChecker_Env.conj_guard g g' in + (((tm, aq) :: args), bs3, subst2, + uu___10))) + | (uu___3, + { FStar_Syntax_Syntax.binder_bv = uu___4; + FStar_Syntax_Syntax.binder_qual = uu___5; + FStar_Syntax_Syntax.binder_positivity = uu___6; + FStar_Syntax_Syntax.binder_attrs = uu___7::uu___8;_}::rest) + -> + let b = FStar_Compiler_List.hd bs2 in + let b1 = FStar_Syntax_Subst.subst_binder subst b in + let uu___9 = + instantiate_one_binder env + e.FStar_Syntax_Syntax.pos b1 in + (match uu___9 with + | (tm, ty, aq, g) -> + let subst1 = + (FStar_Syntax_Syntax.NT + ((b1.FStar_Syntax_Syntax.binder_bv), tm)) + :: subst in + let uu___10 = + aux subst1 (decr_inst inst_n) rest in + (match uu___10 with + | (args, bs3, subst2, g') -> + let uu___11 = + FStar_TypeChecker_Env.conj_guard g g' in + (((tm, aq) :: args), bs3, subst2, + uu___11))) | (uu___3, bs3) -> ([], bs3, subst, FStar_TypeChecker_Env.trivial_guard) in From 0ab882faf1151d505026b9075fabaa98e818758b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Mon, 26 Aug 2024 15:54:02 -0700 Subject: [PATCH 3/3] Update expected output --- tests/error-messages/Bug2021.fst.expected | 6 +++--- tests/error-messages/ResolveImplicitsErrorPos.fst.expected | 2 +- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/tests/error-messages/Bug2021.fst.expected b/tests/error-messages/Bug2021.fst.expected index b100795ac1f..87a0c9b7c24 100644 --- a/tests/error-messages/Bug2021.fst.expected +++ b/tests/error-messages/Bug2021.fst.expected @@ -23,7 +23,7 @@ * Error 66 at Bug2021.fst(24,13-24,14): - Failed to resolve implicit argument ?9 of type Prims.int - introduced for Instantiating implicit argument in application + introduced for Instantiating implicit argument - See also Bug2021.fst(23,11-23,12) >>] @@ -31,7 +31,7 @@ * Error 66 at Bug2021.fst(30,13-30,17): - Failed to resolve implicit argument ?10 of type Prims.int - introduced for Instantiating implicit argument in application + introduced for Instantiating implicit argument - See also Bug2021.fst(29,11-29,12) >>] @@ -39,7 +39,7 @@ * Error 66 at Bug2021.fst(37,13-37,17): - Failed to resolve implicit argument ?13 of type Prims.int - introduced for Instantiating implicit argument in application + introduced for Instantiating implicit argument - See also Bug2021.fst(36,11-36,12) >>] diff --git a/tests/error-messages/ResolveImplicitsErrorPos.fst.expected b/tests/error-messages/ResolveImplicitsErrorPos.fst.expected index 1bf9cdd167b..849573085ae 100644 --- a/tests/error-messages/ResolveImplicitsErrorPos.fst.expected +++ b/tests/error-messages/ResolveImplicitsErrorPos.fst.expected @@ -1,6 +1,6 @@ proof-state: State dump @ depth 0 (at the time of failure): Location: ResolveImplicitsErrorPos.fst(14,13-16,7) -Goal 1/1 (Instantiation of meta argument): +Goal 1/1 (Instantiating meta argument): (_: Prims.unit) |- _ : Prims.int >> Got issues: [