diff options
| -rw-r--r-- | examples/layeredeffects/RST.fst | 21 | ||||
| -rw-r--r-- | src/ocaml-output/FStar_TypeChecker_TcTerm.ml | 2585 | ||||
| -rw-r--r-- | src/typechecker/FStar.TypeChecker.TcTerm.fs | 9 |
3 files changed, 1330 insertions, 1285 deletions
diff --git a/examples/layeredeffects/RST.fst b/examples/layeredeffects/RST.fst index ec7dc8a..9a98181 100644 --- a/examples/layeredeffects/RST.fst +++ b/examples/layeredeffects/RST.fst @@ -103,3 +103,24 @@ let test () : RSTATE array emp array_resource = let ptr = alloc () in return ptr + + +(* + * Following example showcases a bug in checking match terms for layered effects + * + * When typechecking the pattern `C a x`, we generate a term with projectors and discriminators + * for each of the pattern bvs, a and x in this case, and those terms are then lax checked + * Crucially when lax checking pat_bv_tm for `x`, `a` must be in the environement, + * earlier it wasn't + *) + +noeq +type m : Type -> Type = +| C : a:Type -> x:a -> m a + + +assume val rst_unit (_:unit) : RSTATE unit emp (fun _ -> emp) + +let test_match (a:Type) (f:m a) : RSTATE unit emp (fun _ -> emp) += match f with + | C a x -> rst_unit () diff --git a/src/ocaml-output/FStar_TypeChecker_TcTerm.ml b/src/ocaml-output/FStar_TypeChecker_TcTerm.ml index 6facd54..81acacc 100644 --- a/src/ocaml-output/FStar_TypeChecker_TcTerm.ml +++ b/src/ocaml-output/FStar_TypeChecker_TcTerm.ml @@ -8492,292 +8492,315 @@ and (tc_eqn : FStar_Util.print_string "Typechecking pat_bv_tms ...\n" else ()); - (let pat_bv_tms1 = + (let uu____23725 = FStar_List.fold_left2 - (fun acc -> + (fun uu____23747 + -> fun pat_bv_tm -> fun bv -> + match uu____23747 + with + | + (env1,acc) + -> let expected_t = - let uu____23744 + let uu____23771 = - let uu____23753 + let uu____23780 = FStar_Syntax_Syntax.null_binder pat_t in - [uu____23753] + [uu____23780] in - let uu____23772 + let uu____23799 = - let uu____23775 + let uu____23802 = - let uu____23778 + let uu____23805 = FStar_TypeChecker_Env.new_u_univ () in FStar_All.pipe_right - uu____23778 + uu____23805 (fun - _23781 + _23808 -> FStar_Pervasives_Native.Some - _23781) + _23808) in FStar_Syntax_Syntax.mk_Total' bv.FStar_Syntax_Syntax.sort - uu____23775 + uu____23802 in FStar_Syntax_Util.arrow - uu____23744 - uu____23772 + uu____23771 + uu____23799 in - let env1 + let env2 = - let uu___3010_23783 + let uu___3012_23810 = FStar_TypeChecker_Env.set_expected_typ - env + env1 expected_t in { FStar_TypeChecker_Env.solver = - (uu___3010_23783.FStar_TypeChecker_Env.solver); + (uu___3012_23810.FStar_TypeChecker_Env.solver); FStar_TypeChecker_Env.range = - (uu___3010_23783.FStar_TypeChecker_Env.range); + (uu___3012_23810.FStar_TypeChecker_Env.range); FStar_TypeChecker_Env.curmodule = - (uu___3010_23783.FStar_TypeChecker_Env.curmodule); + (uu___3012_23810.FStar_TypeChecker_Env.curmodule); FStar_TypeChecker_Env.gamma = - (uu___3010_23783.FStar_TypeChecker_Env.gamma); + (uu___3012_23810.FStar_TypeChecker_Env.gamma); FStar_TypeChecker_Env.gamma_sig = - (uu___3010_23783.FStar_TypeChecker_Env.gamma_sig); + (uu___3012_23810.FStar_TypeChecker_Env.gamma_sig); FStar_TypeChecker_Env.gamma_cache = - (uu___3010_23783.FStar_TypeChecker_Env.gamma_cache); + (uu___3012_23810.FStar_TypeChecker_Env.gamma_cache); FStar_TypeChecker_Env.modules = - (uu___3010_23783.FStar_TypeChecker_Env.modules); + (uu___3012_23810.FStar_TypeChecker_Env.modules); FStar_TypeChecker_Env.expected_typ = - (uu___3010_23783.FStar_TypeChecker_Env.expected_typ); + (uu___3012_23810.FStar_TypeChecker_Env.expected_typ); FStar_TypeChecker_Env.sigtab = - (uu___3010_23783.FStar_TypeChecker_Env.sigtab); + (uu___3012_23810.FStar_TypeChecker_Env.sigtab); FStar_TypeChecker_Env.attrtab = - (uu___3010_23783.FStar_TypeChecker_Env.attrtab); + (uu___3012_23810.FStar_TypeChecker_Env.attrtab); FStar_TypeChecker_Env.instantiate_imp = - (uu___3010_23783.FStar_TypeChecker_Env.instantiate_imp); + (uu___3012_23810.FStar_TypeChecker_Env.instantiate_imp); FStar_TypeChecker_Env.effects = - (uu___3010_23783.FStar_TypeChecker_Env.effects); + (uu___3012_23810.FStar_TypeChecker_Env.effects); FStar_TypeChecker_Env.generalize = - (uu___3010_23783.FStar_TypeChecker_Env.generalize); + (uu___3012_23810.FStar_TypeChecker_Env.generalize); FStar_TypeChecker_Env.letrecs = - (uu___3010_23783.FStar_TypeChecker_Env.letrecs); + (uu___3012_23810.FStar_TypeChecker_Env.letrecs); FStar_TypeChecker_Env.top_level = - (uu___3010_23783.FStar_TypeChecker_Env.top_level); + (uu___3012_23810.FStar_TypeChecker_Env.top_level); FStar_TypeChecker_Env.check_uvars = - (uu___3010_23783.FStar_TypeChecker_Env.check_uvars); + (uu___3012_23810.FStar_TypeChecker_Env.check_uvars); FStar_TypeChecker_Env.use_eq = - (uu___3010_23783.FStar_TypeChecker_Env.use_eq); + (uu___3012_23810.FStar_TypeChecker_Env.use_eq); FStar_TypeChecker_Env.is_iface = - (uu___3010_23783.FStar_TypeChecker_Env.is_iface); + (uu___3012_23810.FStar_TypeChecker_Env.is_iface); FStar_TypeChecker_Env.admit = - (uu___3010_23783.FStar_TypeChecker_Env.admit); + (uu___3012_23810.FStar_TypeChecker_Env.admit); FStar_TypeChecker_Env.lax = true; FStar_TypeChecker_Env.lax_universes = - (uu___3010_23783.FStar_TypeChecker_Env.lax_universes); + (uu___3012_23810.FStar_TypeChecker_Env.lax_universes); FStar_TypeChecker_Env.phase1 = - (uu___3010_23783.FStar_TypeChecker_Env.phase1); + (uu___3012_23810.FStar_TypeChecker_Env.phase1); FStar_TypeChecker_Env.failhard = - (uu___3010_23783.FStar_TypeChecker_Env.failhard); + (uu___3012_23810.FStar_TypeChecker_Env.failhard); FStar_TypeChecker_Env.nosynth = - (uu___3010_23783.FStar_TypeChecker_Env.nosynth); + (uu___3012_23810.FStar_TypeChecker_Env.nosynth); FStar_TypeChecker_Env.uvar_subtyping = - (uu___3010_23783.FStar_TypeChecker_Env.uvar_subtyping); + (uu___3012_23810.FStar_TypeChecker_Env.uvar_subtyping); FStar_TypeChecker_Env.tc_term = - (uu___3010_23783.FStar_TypeChecker_Env.tc_term); + (uu___3012_23810.FStar_TypeChecker_Env.tc_term); FStar_TypeChecker_Env.type_of = - (uu___3010_23783.FStar_TypeChecker_Env.type_of); + (uu___3012_23810.FStar_TypeChecker_Env.type_of); FStar_TypeChecker_Env.universe_of = - (uu___3010_23783.FStar_TypeChecker_Env.universe_of); + (uu___3012_23810.FStar_TypeChecker_Env.universe_of); FStar_TypeChecker_Env.check_type_of = - (uu___3010_23783.FStar_TypeChecker_Env.check_type_of); + (uu___3012_23810.FStar_TypeChecker_Env.check_type_of); FStar_TypeChecker_Env.use_bv_sorts = - (uu___3010_23783.FStar_TypeChecker_Env.use_bv_sorts); + (uu___3012_23810.FStar_TypeChecker_Env.use_bv_sorts); FStar_TypeChecker_Env.qtbl_name_and_index = - (uu___3010_23783.FStar_TypeChecker_Env.qtbl_name_and_index); + (uu___3012_23810.FStar_TypeChecker_Env.qtbl_name_and_index); FStar_TypeChecker_Env.normalized_eff_names = - (uu___3010_23783.FStar_TypeChecker_Env.normalized_eff_names); + (uu___3012_23810.FStar_TypeChecker_Env.normalized_eff_names); FStar_TypeChecker_Env.fv_delta_depths = - (uu___3010_23783.FStar_TypeChecker_Env.fv_delta_depths); + (uu___3012_23810.FStar_TypeChecker_Env.fv_delta_depths); FStar_TypeChecker_Env.proof_ns = - (uu___3010_23783.FStar_TypeChecker_Env.proof_ns); + (uu___3012_23810.FStar_TypeChecker_Env.proof_ns); FStar_TypeChecker_Env.synth_hook = - (uu___3010_23783.FStar_TypeChecker_Env.synth_hook); + (uu___3012_23810.FStar_TypeChecker_Env.synth_hook); FStar_TypeChecker_Env.splice = - (uu___3010_23783.FStar_TypeChecker_Env.splice); + (uu___3012_23810.FStar_TypeChecker_Env.splice); FStar_TypeChecker_Env.mpreprocess = - (uu___3010_23783.FStar_TypeChecker_Env.mpreprocess); + (uu___3012_23810.FStar_TypeChecker_Env.mpreprocess); FStar_TypeChecker_Env.postprocess = - (uu___3010_23783.FStar_TypeChecker_Env.postprocess); + (uu___3012_23810.FStar_TypeChecker_Env.postprocess); FStar_TypeChecker_Env.is_native_tactic = - (uu___3010_23783.FStar_TypeChecker_Env.is_native_tactic); + (uu___3012_23810.FStar_TypeChecker_Env.is_native_tactic); FStar_TypeChecker_Env.identifier_info = - (uu___3010_23783.FStar_TypeChecker_Env.identifier_info); + (uu___3012_23810.FStar_TypeChecker_Env.identifier_info); FStar_TypeChecker_Env.tc_hooks = - (uu___3010_23783.FStar_TypeChecker_Env.tc_hooks); + (uu___3012_23810.FStar_TypeChecker_Env.tc_hooks); FStar_TypeChecker_Env.dsenv = - (uu___3010_23783.FStar_TypeChecker_Env.dsenv); + (uu___3012_23810.FStar_TypeChecker_Env.dsenv); FStar_TypeChecker_Env.nbe = - (uu___3010_23783.FStar_TypeChecker_Env.nbe); + (uu___3012_23810.FStar_TypeChecker_Env.nbe); FStar_TypeChecker_Env.strict_args_tab = - (uu___3010_23783.FStar_TypeChecker_Env.strict_args_tab); + (uu___3012_23810.FStar_TypeChecker_Env.strict_args_tab); FStar_TypeChecker_Env.erasable_types_tab = - (uu___3010_23783.FStar_TypeChecker_Env.erasable_types_tab) + (uu___3012_23810.FStar_TypeChecker_Env.erasable_types_tab) } in let pat_bv_tm1 = - let uu____23786 + let uu____23813 = tc_trivial_guard - env1 + env2 pat_bv_tm in FStar_All.pipe_right - uu____23786 + uu____23813 FStar_Pervasives_Native.fst in - FStar_List.append + let uu____23822 + = + FStar_TypeChecker_Env.push_bv + env2 bv + in + (uu____23822, + (FStar_List.append acc - [pat_bv_tm1]) - [] pat_bv_tms + [pat_bv_tm1]))) + (env, []) + pat_bv_tms pat_bvs1 in - let pat_bv_tms2 = - let uu____23798 = - FStar_All.pipe_right - pat_bv_tms1 - (FStar_List.map - (fun + match uu____23725 + with + | (uu____23827,pat_bv_tms1) + -> + let pat_bv_tms2 + = + let uu____23836 + = + FStar_All.pipe_right + pat_bv_tms1 + (FStar_List.map + (fun pat_bv_tm -> - let uu____23810 + let uu____23848 = - let uu____23815 + let uu____23853 = - let uu____23816 + let uu____23854 = FStar_All.pipe_right scrutinee_tm FStar_Syntax_Syntax.as_arg in - [uu____23816] + [uu____23854] in FStar_Syntax_Syntax.mk_Tm_app pat_bv_tm - uu____23815 + uu____23853 in - uu____23810 + uu____23848 FStar_Pervasives_Native.None FStar_Range.dummyRange)) - in - FStar_All.pipe_right - uu____23798 - (FStar_List.map - (FStar_TypeChecker_Normalize.normalize - [FStar_TypeChecker_Env.Beta] - env)) - in - (let uu____23854 = - FStar_All.pipe_left - (FStar_TypeChecker_Env.debug - env) - (FStar_Options.Other - "LayeredEffects") - in - if uu____23854 - then - let uu____23859 = - FStar_List.fold_left - (fun s -> - fun t -> - let uu____23868 + in + FStar_All.pipe_right + uu____23836 + (FStar_List.map + ( + FStar_TypeChecker_Normalize.normalize + [FStar_TypeChecker_Env.Beta] + env)) + in + ((let uu____23892 + = + FStar_All.pipe_left + (FStar_TypeChecker_Env.debug + env) + (FStar_Options.Other + "LayeredEffects") + in + if uu____23892 + then + let uu____23897 + = + FStar_List.fold_left + (fun s + -> + fun t -> + let uu____23906 = - let uu____23870 + let uu____23908 = FStar_Syntax_Print.term_to_string t in Prims.op_Hat ";" - uu____23870 + uu____23908 in Prims.op_Hat s - uu____23868) - "" + uu____23906) + "" + pat_bv_tms2 + in + FStar_Util.print1 + "tc_eqn: typechecked pat_bv_tms %s" + uu____23897 + else ()); + FStar_TypeChecker_Util.close_layered_lcomp + env pat_bvs1 pat_bv_tms2 - in - FStar_Util.print1 - "tc_eqn: typechecked pat_bv_tms %s" - uu____23859 - else ()); - FStar_TypeChecker_Util.close_layered_lcomp - env pat_bvs1 - pat_bv_tms2 - c_weak1)) + c_weak1))) else FStar_TypeChecker_Util.close_wp_lcomp env pat_bvs1 c_weak1 in - ((let uu____23880 = - (let uu____23884 = + ((let uu____23918 = + (let uu____23922 = FStar_TypeChecker_Env.try_lookup_effect_lid env FStar_Parser_Const.effect_GTot_lid in FStar_Option.isSome - uu____23884) + uu____23922) && (FStar_All.pipe_left (FStar_TypeChecker_Env.debug @@ -8785,34 +8808,34 @@ and (tc_eqn : (FStar_Options.Other "LayeredEffects")) in - if uu____23880 + if uu____23918 then - let uu____23890 = - let uu____23892 = + let uu____23928 = + let uu____23930 = maybe_return_c_weak false in FStar_TypeChecker_Common.lcomp_to_string - uu____23892 + uu____23930 in FStar_Util.print1 "tc_eqn: c_weak applied to false: %s\n" - uu____23890 + uu____23928 else ()); - (let uu____23897 = + (let uu____23935 = FStar_TypeChecker_Env.close_guard env binders g_when_weak in - let uu____23898 = + let uu____23936 = FStar_TypeChecker_Env.conj_guard guard_pat g_branch1 in ((c_weak.FStar_TypeChecker_Common.eff_name), (c_weak.FStar_TypeChecker_Common.cflags), maybe_return_c_weak, - uu____23897, - uu____23898)))) + uu____23935, + uu____23936)))) in match uu____23452 with | (effect_label,cflags,maybe_return_c,g_when1,g_branch1) @@ -8821,38 +8844,38 @@ and (tc_eqn : FStar_TypeChecker_Env.conj_guard g_when1 g_branch1 in - ((let uu____23953 = + ((let uu____23991 = FStar_TypeChecker_Env.debug env FStar_Options.High in - if uu____23953 + if uu____23991 then - let uu____23956 = + let uu____23994 = FStar_TypeChecker_Rel.guard_to_string env guard in FStar_All.pipe_left (FStar_Util.print1 "Carrying guard from match: %s\n") - uu____23956 + uu____23994 else ()); - (let uu____23962 = + (let uu____24000 = FStar_Syntax_Subst.close_branch (pattern1, when_clause1, branch_exp1) in - let uu____23979 = - let uu____23980 = + let uu____24017 = + let uu____24018 = FStar_List.map FStar_Syntax_Syntax.mk_binder pat_bvs1 in FStar_TypeChecker_Util.close_guard_implicits - env false uu____23980 guard + env false uu____24018 guard in - (uu____23962, branch_guard, + (uu____24000, branch_guard, effect_label, cflags, - maybe_return_c, uu____23979, + maybe_return_c, uu____24017, erasable1))))))))))) and (check_top_level_let : @@ -8866,42 +8889,42 @@ and (check_top_level_let : let env1 = instantiate_both env in match e.FStar_Syntax_Syntax.n with | FStar_Syntax_Syntax.Tm_let ((false ,lb::[]),e2) -> - let uu____24029 = check_let_bound_def true env1 lb in - (match uu____24029 with + let uu____24067 = check_let_bound_def true env1 lb in + (match uu____24067 with | (e1,univ_vars1,c1,g1,annotated) -> - let uu____24055 = + let uu____24093 = if annotated && (Prims.op_Negation env1.FStar_TypeChecker_Env.generalize) then - let uu____24077 = + let uu____24115 = FStar_TypeChecker_Normalize.reduce_uvar_solutions env1 e1 in - (g1, uu____24077, univ_vars1, c1) + (g1, uu____24115, univ_vars1, c1) else (let g11 = - let uu____24083 = + let uu____24121 = FStar_TypeChecker_Rel.solve_deferred_constraints env1 g1 in - FStar_All.pipe_right uu____24083 + FStar_All.pipe_right uu____24121 (FStar_TypeChecker_Rel.resolve_implicits env1) in - let uu____24084 = FStar_TypeChecker_Common.lcomp_comp c1 + let uu____24122 = FStar_TypeChecker_Common.lcomp_comp c1 in - match uu____24084 with + match uu____24122 with | (comp1,g_comp1) -> let g12 = FStar_TypeChecker_Env.conj_guard g11 g_comp1 in - let uu____24102 = - let uu____24115 = + let uu____24140 = + let uu____24153 = FStar_TypeChecker_Util.generalize env1 false [((lb.FStar_Syntax_Syntax.lbname), e1, comp1)] in - FStar_List.hd uu____24115 in - (match uu____24102 with - | (uu____24165,univs1,e11,c11,gvs) -> + FStar_List.hd uu____24153 in + (match uu____24140 with + | (uu____24203,univs1,e11,c11,gvs) -> let g13 = FStar_All.pipe_left (FStar_TypeChecker_Env.map_guard g12) @@ -8916,30 +8939,30 @@ and (check_top_level_let : let g14 = FStar_TypeChecker_Env.abstract_guard_n gvs g13 in - let uu____24179 = + let uu____24217 = FStar_TypeChecker_Common.lcomp_of_comp c11 in - (g14, e11, univs1, uu____24179))) + (g14, e11, univs1, uu____24217))) in - (match uu____24055 with + (match uu____24093 with | (g11,e11,univ_vars2,c11) -> - let uu____24196 = - let uu____24205 = + let uu____24234 = + let uu____24243 = FStar_TypeChecker_Env.should_verify env1 in - if uu____24205 + if uu____24243 then - let uu____24216 = + let uu____24254 = FStar_TypeChecker_Util.check_top_level env1 g11 c11 in - match uu____24216 with + match uu____24254 with | (ok,c12) -> (if ok then (e2, c12) else - ((let uu____24250 = + ((let uu____24288 = FStar_TypeChecker_Env.get_range env1 in - FStar_Errors.log_issue uu____24250 + FStar_Errors.log_issue uu____24288 FStar_TypeChecker_Err.top_level_effect); - (let uu____24251 = + (let uu____24289 = FStar_Syntax_Syntax.mk (FStar_Syntax_Syntax.Tm_meta (e2, @@ -8948,12 +8971,12 @@ and (check_top_level_let : FStar_Pervasives_Native.None e2.FStar_Syntax_Syntax.pos in - (uu____24251, c12)))) + (uu____24289, c12)))) else (FStar_TypeChecker_Rel.force_trivial_guard env1 g11; - (let uu____24263 = + (let uu____24301 = FStar_TypeChecker_Common.lcomp_comp c11 in - match uu____24263 with + match uu____24301 with | (comp1,g_comp1) -> (FStar_TypeChecker_Rel.force_trivial_guard env1 g_comp1; @@ -8966,15 +8989,15 @@ and (check_top_level_let : env1) in let e21 = - let uu____24287 = + let uu____24325 = FStar_Syntax_Util.is_pure_comp c in - if uu____24287 + if uu____24325 then e2 else - ((let uu____24295 = + ((let uu____24333 = FStar_TypeChecker_Env.get_range env1 in - FStar_Errors.log_issue uu____24295 + FStar_Errors.log_issue uu____24333 FStar_TypeChecker_Err.top_level_effect); FStar_Syntax_Syntax.mk (FStar_Syntax_Syntax.Tm_meta @@ -8986,22 +9009,22 @@ and (check_top_level_let : in (e21, c))))) in - (match uu____24196 with + (match uu____24234 with | (e21,c12) -> - ((let uu____24319 = + ((let uu____24357 = FStar_TypeChecker_Env.debug env1 FStar_Options.Medium in - if uu____24319 + if uu____24357 then - let uu____24322 = + let uu____24360 = FStar_Syntax_Print.term_to_string e11 in FStar_Util.print1 - "Let binding BEFORE tcnorm: %s\n" uu____24322 + "Let binding BEFORE tcnorm: %s\n" uu____24360 else ()); (let e12 = - let uu____24328 = FStar_Options.tcnorm () in - if uu____24328 + let uu____24366 = FStar_Options.tcnorm () in + if uu____24366 then FStar_TypeChecker_Normalize.normalize [FStar_TypeChecker_Env.UnfoldAttr @@ -9014,22 +9037,22 @@ and (check_top_level_let : FStar_TypeChecker_Env.DoNotUnfoldPureLets] env1 e11 else e11 in - (let uu____24334 = + (let uu____24372 = FStar_TypeChecker_Env.debug env1 FStar_Options.Medium in - if uu____24334 + if uu____24372 then - let uu____24337 = + let uu____24375 = FStar_Syntax_Print.term_to_string e12 in FStar_Util.print1 - "Let binding AFTER tcnorm: %s\n" uu____24337 + "Let binding AFTER tcnorm: %s\n" uu____24375 else ()); (let cres = - let uu____24343 = + let uu____24381 = FStar_Syntax_Util.is_pure_or_ghost_comp c12 in - if uu____24343 + if uu____24381 then FStar_Syntax_Syntax.mk_Total' FStar_Syntax_Syntax.t_unit @@ -9044,8 +9067,8 @@ and (check_top_level_let : let c1_wp = match c1_comp_typ.FStar_Syntax_Syntax.effect_args with - | (wp,uu____24351)::[] -> wp - | uu____24376 -> + | (wp,uu____24389)::[] -> wp + | uu____24414 -> failwith "Impossible! check_top_level_let: got unexpected effect args" in @@ -9058,28 +9081,28 @@ and (check_top_level_let : FStar_All.pipe_right c1_eff_decl FStar_Syntax_Util.get_return_vc_combinator in - let uu____24393 = - let uu____24398 = + let uu____24431 = + let uu____24436 = FStar_TypeChecker_Env.inst_effect_fun_with [FStar_Syntax_Syntax.U_zero] env1 c1_eff_decl ret1 in - let uu____24399 = - let uu____24400 = + let uu____24437 = + let uu____24438 = FStar_Syntax_Syntax.as_arg FStar_Syntax_Syntax.t_unit in - let uu____24409 = - let uu____24420 = + let uu____24447 = + let uu____24458 = FStar_Syntax_Syntax.as_arg FStar_Syntax_Syntax.unit_const in - [uu____24420] in - uu____24400 :: uu____24409 in + [uu____24458] in + uu____24438 :: uu____24447 in FStar_Syntax_Syntax.mk_Tm_app - uu____24398 uu____24399 + uu____24436 uu____24437 in - uu____24393 FStar_Pervasives_Native.None + uu____24431 FStar_Pervasives_Native.None e21.FStar_Syntax_Syntax.pos in let wp = @@ -9087,17 +9110,17 @@ and (check_top_level_let : FStar_All.pipe_right c1_eff_decl FStar_Syntax_Util.get_bind_vc_combinator in - let uu____24457 = - let uu____24462 = + let uu____24495 = + let uu____24500 = FStar_TypeChecker_Env.inst_effect_fun_with (FStar_List.append c1_comp_typ.FStar_Syntax_Syntax.comp_univs [FStar_Syntax_Syntax.U_zero]) env1 c1_eff_decl bind1 in - let uu____24463 = - let uu____24464 = - let uu____24473 = + let uu____24501 = + let uu____24502 = + let uu____24511 = FStar_Syntax_Syntax.mk (FStar_Syntax_Syntax.Tm_constant (FStar_Const.Const_range @@ -9107,35 +9130,35 @@ and (check_top_level_let : in FStar_All.pipe_left FStar_Syntax_Syntax.as_arg - uu____24473 + uu____24511 in - let uu____24482 = - let uu____24493 = + let uu____24520 = + let uu____24531 = FStar_All.pipe_left FStar_Syntax_Syntax.as_arg c1_comp_typ.FStar_Syntax_Syntax.result_typ in - let uu____24510 = - let uu____24521 = + let uu____24548 = + let uu____24559 = FStar_Syntax_Syntax.as_arg FStar_Syntax_Syntax.t_unit in - let uu____24530 = - let uu____24541 = + let uu____24568 = + let uu____24579 = FStar_Syntax_Syntax.as_arg c1_wp in - let uu____24550 = - let uu____24561 = - let uu____24570 = - let uu____24571 = - let uu____24572 = + let uu____24588 = + let uu____24599 = + let uu____24608 = + let uu____24609 = + let uu____24610 = FStar_Syntax_Syntax.null_binder c1_comp_typ.FStar_Syntax_Syntax.result_typ in - [uu____24572] in + [uu____24610] in FStar_Syntax_Util.abs - uu____24571 wp2 + uu____24609 wp2 (FStar_Pervasives_Native.Some (FStar_Syntax_Util.mk_residual_comp FStar_Parser_Const.effect_Tot_lid @@ -9144,24 +9167,24 @@ and (check_top_level_let : in FStar_All.pipe_left FStar_Syntax_Syntax.as_arg - uu____24570 + uu____24608 in - [uu____24561] in - uu____24541 :: uu____24550 in - uu____24521 :: uu____24530 in - uu____24493 :: uu____24510 in - uu____24464 :: uu____24482 in + [uu____24599] in + uu____24579 :: uu____24588 in + uu____24559 :: uu____24568 in + uu____24531 :: uu____24548 in + uu____24502 :: uu____24520 in FStar_Syntax_Syntax.mk_Tm_app - uu____24462 uu____24463 + uu____24500 uu____24501 in - uu____24457 FStar_Pervasives_Native.None + uu____24495 FStar_Pervasives_Native.None lb.FStar_Syntax_Syntax.lbpos in - let uu____24649 = - let uu____24650 = - let uu____24661 = + let uu____24687 = + let uu____24688 = + let uu____24699 = FStar_Syntax_Syntax.as_arg wp in - [uu____24661] in + [uu____24699] in { FStar_Syntax_Syntax.comp_univs = [FStar_Syntax_Syntax.U_zero]; @@ -9170,10 +9193,10 @@ and (check_top_level_let : FStar_Syntax_Syntax.result_typ = FStar_Syntax_Syntax.t_unit; FStar_Syntax_Syntax.effect_args = - uu____24650; + uu____24688; FStar_Syntax_Syntax.flags = [] } in - FStar_Syntax_Syntax.mk_Comp uu____24649) + FStar_Syntax_Syntax.mk_Comp uu____24687) in let lb1 = FStar_Syntax_Util.close_univs_and_mk_letbinding @@ -9184,18 +9207,18 @@ and (check_top_level_let : lb.FStar_Syntax_Syntax.lbattrs lb.FStar_Syntax_Syntax.lbpos in - let uu____24689 = + let uu____24727 = FStar_Syntax_Syntax.mk (FStar_Syntax_Syntax.Tm_let ((false, [lb1]), e21)) FStar_Pervasives_Native.None e.FStar_Syntax_Syntax.pos in - let uu____24703 = + let uu____24741 = FStar_TypeChecker_Common.lcomp_of_comp cres in - (uu____24689, uu____24703, + (uu____24727, uu____24741, FStar_TypeChecker_Env.trivial_guard))))))) - | uu____24704 -> failwith "Impossible" + | uu____24742 -> failwith "Impossible" and (maybe_intro_smt_lemma : FStar_TypeChecker_Env.env -> @@ -9205,15 +9228,15 @@ and (maybe_intro_smt_lemma : fun env -> fun lem_typ -> fun c2 -> - let uu____24715 = FStar_Syntax_Util.is_smt_lemma lem_typ in - if uu____24715 + let uu____24753 = FStar_Syntax_Util.is_smt_lemma lem_typ in + if uu____24753 then let universe_of_binders bs = - let uu____24742 = + let uu____24780 = FStar_List.fold_left - (fun uu____24767 -> + (fun uu____24805 -> fun b -> - match uu____24767 with + match uu____24805 with | (env1,us) -> let u = env1.FStar_TypeChecker_Env.universe_of env1 @@ -9223,7 +9246,7 @@ and (maybe_intro_smt_lemma : FStar_TypeChecker_Env.push_binders env1 [b] in (env2, (u :: us))) (env, []) bs in - match uu____24742 with | (uu____24815,us) -> FStar_List.rev us + match uu____24780 with | (uu____24853,us) -> FStar_List.rev us in let quant = FStar_Syntax_Util.smt_lemma_as_forall lem_typ universe_of_binders @@ -9244,107 +9267,107 @@ and (check_inner_let : match e.FStar_Syntax_Syntax.n with | FStar_Syntax_Syntax.Tm_let ((false ,lb::[]),e2) -> let env2 = - let uu___3133_24851 = env1 in + let uu___3137_24889 = env1 in { FStar_TypeChecker_Env.solver = - (uu___3133_24851.FStar_TypeChecker_Env.solver); + (uu___3137_24889.FStar_TypeChecker_Env.solver); FStar_TypeChecker_Env.range = - (uu___3133_24851.FStar_TypeChecker_Env.range); + (uu___3137_24889.FStar_TypeChecker_Env.range); FStar_TypeChecker_Env.curmodule = - (uu___3133_24851.FStar_TypeChecker_Env.curmodule); + (uu___3137_24889.FStar_TypeChecker_Env.curmodule); FStar_TypeChecker_Env.gamma = - (uu___3133_24851.FStar_TypeChecker_Env.gamma); + (uu___3137_24889.FStar_TypeChecker_Env.gamma); FStar_TypeChecker_Env.gamma_sig = - (uu___3133_24851.FStar_TypeChecker_Env.gamma_sig); + (uu___3137_24889.FStar_TypeChecker_Env.gamma_sig); FStar_TypeChecker_Env.gamma_cache = - (uu___3133_24851.FStar_TypeChecker_Env.gamma_cache); + (uu___3137_24889.FStar_TypeChecker_Env.gamma_cache); FStar_TypeChecker_Env.modules = - (uu___3133_24851.FStar_TypeChecker_Env.modules); + (uu___3137_24889.FStar_TypeChecker_Env.modules); FStar_TypeChecker_Env.expected_typ = - (uu___3133_24851.FStar_TypeChecker_Env.expected_typ); + (uu___3137_24889.FStar_TypeChecker_Env.expected_typ); FStar_TypeChecker_Env.sigtab = - (uu___3133_24851.FStar_TypeChecker_Env.sigtab); + (uu___3137_24889.FStar_TypeChecker_Env.sigtab); FStar_TypeChecker_Env.attrtab = - (uu___3133_24851.FStar_TypeChecker_Env.attrtab); + (uu___3137_24889.FStar_TypeChecker_Env.attrtab); FStar_TypeChecker_Env.instantiate_imp = - (uu___3133_24851.FStar_TypeChecker_Env.instantiate_imp); + (uu___3137_24889.FStar_TypeChecker_Env.instantiate_imp); FStar_TypeChecker_Env.effects = - (uu___3133_24851.FStar_TypeChecker_Env.effects); + (uu___3137_24889.FStar_TypeChecker_Env.effects); FStar_TypeChecker_Env.generalize = - (uu___3133_24851.FStar_TypeChecker_Env.generalize); + (uu___3137_24889.FStar_TypeChecker_Env.generalize); FStar_TypeChecker_Env.letrecs = - (uu___3133_24851.FStar_TypeChecker_Env.letrecs); + (uu___3137_24889.FStar_TypeChecker_Env.letrecs); FStar_TypeChecker_Env.top_level = false; FStar_TypeChecker_Env.check_uvars = - (uu___3133_24851.FStar_TypeChecker_Env.check_uvars); + (uu___3137_24889.FStar_TypeChecker_Env.check_uvars); FStar_TypeChecker_Env.use_eq = - (uu___3133_24851.FStar_TypeChecker_Env.use_eq); + (uu___3137_24889.FStar_TypeChecker_Env.use_eq); FStar_TypeChecker_Env.is_iface = - (uu___3133_24851.FStar_TypeChecker_Env.is_iface); + (uu___3137_24889.FStar_TypeChecker_Env.is_iface); FStar_TypeChecker_Env.admit = - (uu___3133_24851.FStar_TypeChecker_Env.admit); + (uu___3137_24889.FStar_TypeChecker_Env.admit); FStar_TypeChecker_Env.lax = - (uu___3133_24851.FStar_TypeChecker_Env.lax); + (uu___3137_24889.FStar_TypeChecker_Env.lax); FStar_TypeChecker_Env.lax_universes = - (uu___3133_24851.FStar_TypeChecker_Env.lax_universes); + (uu___3137_24889.FStar_TypeChecker_Env.lax_universes); FStar_TypeChecker_Env.phase1 = - (uu___3133_24851.FStar_TypeChecker_Env.phase1); + (uu___3137_24889.FStar_TypeChecker_Env.phase1); FStar_TypeChecker_Env.failhard = - (uu___3133_24851.FStar_TypeChecker_Env.failhard); + (uu___3137_24889.FStar_TypeChecker_Env.failhard); FStar_TypeChecker_Env.nosynth = - (uu___3133_24851.FStar_TypeChecker_Env.nosynth); + (uu___3137_24889.FStar_TypeChecker_Env.nosynth); FStar_TypeChecker_Env.uvar_subtyping = - (uu___3133_24851.FStar_TypeChecker_Env.uvar_subtyping); + (uu___3137_24889.FStar_TypeChecker_Env.uvar_subtyping); FStar_TypeChecker_Env.tc_term = - (uu___3133_24851.FStar_TypeChecker_Env.tc_term); + (uu___3137_24889.FStar_TypeChecker_Env.tc_term); FStar_TypeChecker_Env.type_of = - (uu___3133_24851.FStar_TypeChecker_Env.type_of); + (uu___3137_24889.FStar_TypeChecker_Env.type_of); FStar_TypeChecker_Env.universe_of = - (uu___3133_24851.FStar_TypeChecker_Env.universe_of); + (uu___3137_24889.FStar_TypeChecker_Env.universe_of); FStar_TypeChecker_Env.check_type_of = - (uu___3133_24851.FStar_TypeChecker_Env.check_type_of); + (uu___3137_24889.FStar_TypeChecker_Env.check_type_of); FStar_TypeChecker_Env.use_bv_sorts = - (uu___3133_24851.FStar_TypeChecker_Env.use_bv_sorts); + (uu___3137_24889.FStar_TypeChecker_Env.use_bv_sorts); FStar_TypeChecker_Env.qtbl_name_and_index = - (uu___3133_24851.FStar_TypeChecker_Env.qtbl_name_and_index); + (uu___3137_24889.FStar_TypeChecker_Env.qtbl_name_and_index); FStar_TypeChecker_Env.normalized_eff_names = - (uu___3133_24851.FStar_TypeChecker_Env.normalized_eff_names); + (uu___3137_24889.FStar_TypeChecker_Env.normalized_eff_names); FStar_TypeChecker_Env.fv_delta_depths = - (uu___3133_24851.FStar_TypeChecker_Env.fv_delta_depths); + (uu___3137_24889.FStar_TypeChecker_Env.fv_delta_depths); FStar_TypeChecker_Env.proof_ns = - (uu___3133_24851.FStar_TypeChecker_Env.proof_ns); + (uu___3137_24889.FStar_TypeChecker_Env.proof_ns); FStar_TypeChecker_Env.synth_hook = - (uu___3133_24851.FStar_TypeChecker_Env.synth_hook); + (uu___3137_24889.FStar_TypeChecker_Env.synth_hook); FStar_TypeChecker_Env.splice = - (uu___3133_24851.FStar_TypeChecker_Env.splice); + (uu___3137_24889.FStar_TypeChecker_Env.splice); FStar_TypeChecker_Env.mpreprocess = - (uu___3133_24851.FStar_TypeChecker_Env.mpreprocess); + (uu___3137_24889.FStar_TypeChecker_Env.mpreprocess); FStar_TypeChecker_Env.postprocess = - (uu___3133_24851.FStar_TypeChecker_Env.postprocess); + (uu___3137_24889.FStar_TypeChecker_Env.postprocess); FStar_TypeChecker_Env.is_native_tactic = - (uu___3133_24851.FStar_TypeChecker_Env.is_native_tactic); + (uu___3137_24889.FStar_TypeChecker_Env.is_native_tactic); FStar_TypeChecker_Env.identifier_info = - (uu___3133_24851.FStar_TypeChecker_Env.identifier_info); + (uu___3137_24889.FStar_TypeChecker_Env.identifier_info); FStar_TypeChecker_Env.tc_hooks = - (uu___3133_24851.FStar_TypeChecker_Env.tc_hooks); + (uu___3137_24889.FStar_TypeChecker_Env.tc_hooks); FStar_TypeChecker_Env.dsenv = - (uu___3133_24851.FStar_TypeChecker_Env.dsenv); + (uu___3137_24889.FStar_TypeChecker_Env.dsenv); FStar_TypeChecker_Env.nbe = - (uu___3133_24851.FStar_TypeChecker_Env.nbe); + (uu___3137_24889.FStar_TypeChecker_Env.nbe); FStar_TypeChecker_Env.strict_args_tab = - (uu___3133_24851.FStar_TypeChecker_Env.strict_args_tab); + (uu___3137_24889.FStar_TypeChecker_Env.strict_args_tab); FStar_TypeChecker_Env.erasable_types_tab = - (uu___3133_24851.FStar_TypeChecker_Env.erasable_types_tab) + (uu___3137_24889.FStar_TypeChecker_Env.erasable_types_tab) } in - let uu____24853 = - let uu____24865 = - let uu____24866 = FStar_TypeChecker_Env.clear_expected_typ env2 + let uu____24891 = + let uu____24903 = + let uu____24904 = FStar_TypeChecker_Env.clear_expected_typ env2 in - FStar_All.pipe_right uu____24866 FStar_Pervasives_Native.fst + FStar_All.pipe_right uu____24904 FStar_Pervasives_Native.fst in - check_let_bound_def false uu____24865 lb in - (match uu____24853 with - | (e1,uu____24889,c1,g1,annotated) -> + check_let_bound_def false uu____24903 lb in + (match uu____24891 with + | (e1,uu____24927,c1,g1,annotated) -> let pure_or_ghost = FStar_TypeChecker_Common.is_pure_or_ghost_lcomp c1 in let is_inline_let = @@ -9355,56 +9378,56 @@ and (check_inner_let : in (if is_inline_let && (Prims.op_Negation pure_or_ghost) then - (let uu____24903 = - let uu____24909 = - let uu____24911 = FStar_Syntax_Print.term_to_string e1 + (let uu____24941 = + let uu____24947 = + let uu____24949 = FStar_Syntax_Print.term_to_string e1 in - let uu____24913 = + let uu____24951 = FStar_Syntax_Print.lid_to_string c1.FStar_TypeChecker_Common.eff_name in FStar_Util.format2 "Definitions marked @inline_let are expected to be pure or ghost; got an expression \"%s\" with effect \"%s\"" - uu____24911 uu____24913 + uu____24949 uu____24951 in - (FStar_Errors.Fatal_ExpectedPureExpression, uu____24909) + (FStar_Errors.Fatal_ExpectedPureExpression, uu____24947) in - FStar_Errors.raise_error uu____24903 + FStar_Errors.raise_error uu____24941 e1.FStar_Syntax_Syntax.pos) else (); (let attrs = - let uu____24924 = + let uu____24962 = (pure_or_ghost && (Prims.op_Negation is_inline_let)) && (FStar_Syntax_Util.is_unit c1.FStar_TypeChecker_Common.res_typ) in - if uu____24924 + if uu____24962 then FStar_Syntax_Util.inline_let_attr :: (lb.FStar_Syntax_Syntax.lbattrs) else lb.FStar_Syntax_Syntax.lbattrs in let x = - let uu___3148_24936 = + let uu___3152_24974 = FStar_Util.left lb.FStar_Syntax_Syntax.lbname in { FStar_Syntax_Syntax.ppname = - (uu___3148_24936.FStar_Syntax_Syntax.ppname); + (uu___3152_24974.FStar_Syntax_Syntax.ppname); FStar_Syntax_Syntax.index = - (uu___3148_24936.FStar_Syntax_Syntax.index); + (uu___3152_24974.FStar_Syntax_Syntax.index); FStar_Syntax_Syntax.sort = (c1.FStar_TypeChecker_Common.res_typ) } in - let uu____24937 = - let uu____24942 = - let uu____24943 = FStar_Syntax_Syntax.mk_binder x in - [uu____24943] in - FStar_Syntax_Subst.open_term uu____24942 e2 in - match uu____24937 with + let uu____24975 = + let uu____24980 = + let uu____24981 = FStar_Syntax_Syntax.mk_binder x in + [uu____24981] in + FStar_Syntax_Subst.open_term uu____24980 e2 in + match uu____24975 with | (xb,e21) -> let xbinder = FStar_List.hd xb in let x1 = FStar_Pervasives_Native.fst xbinder in let env_x = FStar_TypeChecker_Env.push_bv env2 x1 in - let uu____24987 = tc_term env_x e21 in - (match uu____24987 with + let uu____25025 = tc_term env_x e21 in + (match uu____25025 with | (e22,c2,g2) -> let c21 = maybe_intro_smt_lemma env_x @@ -9436,15 +9459,15 @@ and (check_inner_let : attrs lb.FStar_Syntax_Syntax.lbpos in let e3 = - let uu____25013 = - let uu____25020 = - let uu____25021 = - let uu____25035 = + let uu____25051 = + let uu____25058 = + let uu____25059 = + let uu____25073 = FStar_Syntax_Subst.close xb e23 in - ((false, [lb1]), uu____25035) in - FStar_Syntax_Syntax.Tm_let uu____25021 in - FStar_Syntax_Syntax.mk uu____25020 in - uu____25013 FStar_Pervasives_Native.None + ((false, [lb1]), uu____25073) in + FStar_Syntax_Syntax.Tm_let uu____25059 in + FStar_Syntax_Syntax.mk uu____25058 in + uu____25051 FStar_Pervasives_Native.None e.FStar_Syntax_Syntax.pos in let e4 = @@ -9453,120 +9476,120 @@ and (check_inner_let : cres.FStar_TypeChecker_Common.res_typ in let x_eq_e1 = - let uu____25053 = - let uu____25054 = + let uu____25091 = + let uu____25092 = env2.FStar_TypeChecker_Env.universe_of env2 c1.FStar_TypeChecker_Common.res_typ in - let uu____25055 = + let uu____25093 = FStar_Syntax_Syntax.bv_to_name x1 in - FStar_Syntax_Util.mk_eq2 uu____25054 + FStar_Syntax_Util.mk_eq2 uu____25092 c1.FStar_TypeChecker_Common.res_typ - uu____25055 e11 + uu____25093 e11 in FStar_All.pipe_left - (fun _25056 -> - FStar_TypeChecker_Common.NonTrivial _25056) - uu____25053 + (fun _25094 -> + FStar_TypeChecker_Common.NonTrivial _25094) + uu____25091 in let g21 = - let uu____25058 = - let uu____25059 = + let uu____25096 = + let uu____25097 = FStar_TypeChecker_Env.guard_of_guard_formula x_eq_e1 in - FStar_TypeChecker_Env.imp_guard uu____25059 g2 + FStar_TypeChecker_Env.imp_guard uu____25097 g2 in FStar_TypeChecker_Env.close_guard env2 xb - uu____25058 + uu____25096 in let g22 = - let uu____25061 = - let uu____25063 = + let uu____25099 = + let uu____25101 = FStar_All.pipe_right cres.FStar_TypeChecker_Common.eff_name (FStar_TypeChecker_Env.norm_eff_name env2) in - FStar_All.pipe_right uu____25063 + FStar_All.pipe_right uu____25101 (FStar_TypeChecker_Env.is_layered_effect env2) in FStar_TypeChecker_Util.close_guard_implicits env2 - uu____25061 xb g21 + uu____25099 xb g21 in let guard = FStar_TypeChecker_Env.conj_guard g1 g22 in - let uu____25066 = - let uu____25068 = + let uu____25104 = + let uu____25106 = FStar_TypeChecker_Env.expected_typ env2 in - FStar_Option.isSome uu____25068 in - if uu____25066 + FStar_Option.isSome uu____25106 in + if uu____25104 then let tt = - let uu____25079 = + let uu____25117 = FStar_TypeChecker_Env.expected_typ env2 in - FStar_All.pipe_right uu____25079 + FStar_All.pipe_right uu____25117 FStar_Option.get in - ((let uu____25085 = + ((let uu____25123 = FStar_All.pipe_left (FStar_TypeChecker_Env.debug env2) (FStar_Options.Other "Exports") in - if uu____25085 + if uu____25123 then - let uu____25090 = + let uu____25128 = FStar_Syntax_Print.term_to_string tt in - let uu____25092 = + let uu____25130 = FStar_Syntax_Print.term_to_string cres.FStar_TypeChecker_Common.res_typ in FStar_Util.print2 "Got expected type from env %s\ncres.res_typ=%s\n" - uu____25090 uu____25092 + uu____25128 uu____25130 else ()); (e4, cres, guard)) else - (let uu____25099 = + (let uu____25137 = check_no_escape FStar_Pervasives_Native.None env2 [x1] cres.FStar_TypeChecker_Common.res_typ in - match uu____25099 with + match uu____25137 with | (t,g_ex) -> - ((let uu____25113 = + ((let uu____25151 = FStar_All.pipe_left (FStar_TypeChecker_Env.debug env2) (FStar_Options.Other "Exports") in - if uu____25113 + if uu____25151 then - let uu____25118 = + let uu____25156 = FStar_Syntax_Print.term_to_string cres.FStar_TypeChecker_Common.res_typ in - let uu____25120 = + let uu____25158 = FStar_Syntax_Print.term_to_string t in FStar_Util.print2 "Checked %s has no escaping types; normalized to %s\n" - uu____25118 uu____25120 + uu____25156 uu____25158 else ()); - (let uu____25125 = + (let uu____25163 = FStar_TypeChecker_Env.conj_guard g_ex guard in (e4, - (let uu___3181_25127 = cres in + (let uu___3185_25165 = cres in { FStar_TypeChecker_Common.eff_name = - (uu___3181_25127.FStar_TypeChecker_Common.eff_name); + (uu___3185_25165.FStar_TypeChecker_Common.eff_name); FStar_TypeChecker_Common.res_typ = t; FStar_TypeChecker_Common.cflags = - (uu___3181_25127.FStar_TypeChecker_Common.cflags); + (uu___3185_25165.FStar_TypeChecker_Common.cflags); FStar_TypeChecker_Common.comp_thunk = - (uu___3181_25127.FStar_TypeChecker_Common.comp_thunk) - }), uu____25125)))))))) - | uu____25128 -> + (uu___3185_25165.FStar_TypeChecker_Common.comp_thunk) + }), uu____25163)))))))) + | uu____25166 -> failwith "Impossible (inner let with more than one lb)" and (check_top_level_let_rec : @@ -9580,44 +9603,44 @@ and (check_top_level_let_rec : let env1 = instantiate_both env in match top.FStar_Syntax_Syntax.n with | FStar_Syntax_Syntax.Tm_let ((true ,lbs),e2) -> - let uu____25164 = FStar_Syntax_Subst.open_let_rec lbs e2 in - (match uu____25164 with + let uu____25202 = FStar_Syntax_Subst.open_let_rec lbs e2 in + (match uu____25202 with | (lbs1,e21) -> - let uu____25183 = + let uu____25221 = FStar_TypeChecker_Env.clear_expected_typ env1 in - (match uu____25183 with + (match uu____25221 with | (env0,topt) -> - let uu____25202 = build_let_rec_env true env0 lbs1 in - (match uu____25202 with + let uu____25240 = build_let_rec_env true env0 lbs1 in + (match uu____25240 with | (lbs2,rec_env,g_t) -> - let uu____25225 = check_let_recs rec_env lbs2 in - (match uu____25225 with + let uu____25263 = check_let_recs rec_env lbs2 in + (match uu____25263 with | (lbs3,g_lbs) -> let g_lbs1 = - let uu____25245 = - let uu____25246 = + let uu____25283 = + let uu____25284 = FStar_TypeChecker_Env.conj_guard g_t g_lbs in - FStar_All.pipe_right uu____25246 + FStar_All.pipe_right uu____25284 (FStar_TypeChecker_Rel.solve_deferred_constraints env1) in - FStar_All.pipe_right uu____25245 + FStar_All.pipe_right uu____25283 (FStar_TypeChecker_Rel.resolve_implicits env1) in let all_lb_names = - let uu____25252 = + let uu____25290 = FStar_All.pipe_right lbs3 (FStar_List.map (fun lb -> FStar_Util.right lb.FStar_Syntax_Syntax.lbname)) in - FStar_All.pipe_right uu____25252 - (fun _25269 -> - FStar_Pervasives_Native.Some _25269) + FStar_All.pipe_right uu____25290 + (fun _25307 -> + FStar_Pervasives_Native.Some _25307) in let lbs4 = if @@ -9648,25 +9671,25 @@ and (check_top_level_let_rec : lb.FStar_Syntax_Syntax.lbpos)) else (let ecs = - let uu____25306 = + let uu____25344 = FStar_All.pipe_right lbs3 (FStar_List.map (fun lb -> - let uu____25340 = + let uu____25378 = FStar_Syntax_Syntax.mk_Total lb.FStar_Syntax_Syntax.lbtyp in ((lb.FStar_Syntax_Syntax.lbname), (lb.FStar_Syntax_Syntax.lbdef), - uu____25340))) + uu____25378))) in FStar_TypeChecker_Util.generalize env1 - true uu____25306 + true uu____25344 in FStar_List.map2 - (fun uu____25375 -> + (fun uu____25413 -> fun lb -> - match uu____25375 with + match uu____25413 with | (x,uvs,e,c,gvs) -> FStar_Syntax_Util.close_univs_and_mk_letbinding all_lb_names x uvs @@ -9679,35 +9702,35 @@ and (check_top_level_let_rec : ecs lbs3) in let cres = - let uu____25423 = + let uu____25461 = FStar_Syntax_Syntax.mk_Total FStar_Syntax_Syntax.t_unit in FStar_All.pipe_left FStar_TypeChecker_Common.lcomp_of_comp - uu____25423 + uu____25461 in - let uu____25424 = + let uu____25462 = FStar_Syntax_Subst.close_let_rec lbs4 e21 in - (match uu____25424 with + (match uu____25462 with | (lbs5,e22) -> - ((let uu____25444 = + ((let uu____25482 = FStar_TypeChecker_Rel.discharge_guard env1 g_lbs1 in - FStar_All.pipe_right uu____25444 + FStar_All.pipe_right uu____25482 (FStar_TypeChecker_Rel.force_trivial_guard env1)); - (let uu____25445 = + (let uu____25483 = FStar_Syntax_Syntax.mk (FStar_Syntax_Syntax.Tm_let ((true, lbs5), e22)) FStar_Pervasives_Native.None top.FStar_Syntax_Syntax.pos in - (uu____25445, cres, + (uu____25483, cres, FStar_TypeChecker_Env.trivial_guard)))))))) - | uu____25459 -> failwith "Impossible" + | uu____25497 -> failwith "Impossible" and (check_inner_let_rec : FStar_TypeChecker_Env.env -> @@ -9720,64 +9743,64 @@ and (check_inner_let_rec : let env1 = instantiate_both env in match top.FStar_Syntax_Syntax.n with | FStar_Syntax_Syntax.Tm_let ((true ,lbs),e2) -> - let uu____25495 = FStar_Syntax_Subst.open_let_rec lbs e2 in - (match uu____25495 with + let uu____25533 = FStar_Syntax_Subst.open_let_rec lbs e2 in + (match uu____25533 with | (lbs1,e21) -> - let uu____25514 = + let uu____25552 = FStar_TypeChecker_Env.clear_expected_typ env1 in - (match uu____25514 with + (match uu____25552 with | (env0,topt) -> - let uu____25533 = build_let_rec_env false env0 lbs1 in - (match uu____25533 with + let uu____25571 = build_let_rec_env false env0 lbs1 in + (match uu____25571 with | (lbs2,rec_env,g_t) -> - let uu____25556 = - let uu____25563 = check_let_recs rec_env lbs2 in - FStar_All.pipe_right uu____25563 - (fun uu____25586 -> - match uu____25586 with + let uu____25594 = + let uu____25601 = check_let_recs rec_env lbs2 in + FStar_All.pipe_right uu____25601 + (fun uu____25624 -> + match uu____25624 with | (lbs3,g) -> - let uu____25605 = + let uu____25643 = FStar_TypeChecker_Env.conj_guard g_t g in - (lbs3, uu____25605)) + (lbs3, uu____25643)) in - (match uu____25556 with + (match uu____25594 with | (lbs3,g_lbs) -> - let uu____25620 = + let uu____25658 = FStar_All.pipe_right lbs3 (FStar_Util.fold_map (fun env2 -> fun lb -> let x = - let uu___3256_25643 = + let uu___3260_25681 = FStar_Util.left lb.FStar_Syntax_Syntax.lbname in { FStar_Syntax_Syntax.ppname = - (uu___3256_25643.FStar_Syntax_Syntax.ppname); + (uu___3260_25681.FStar_Syntax_Syntax.ppname); FStar_Syntax_Syntax.index = - (uu___3256_25643.FStar_Syntax_Syntax.index); + (uu___3260_25681.FStar_Syntax_Syntax.index); FStar_Syntax_Syntax.sort = (lb.FStar_Syntax_Syntax.lbtyp) } in let lb1 = - let uu___3259_25645 = lb in + let uu___3263_25683 = lb in { FStar_Syntax_Syntax.lbname = (FStar_Util.Inl x); FStar_Syntax_Syntax.lbunivs = - (uu___3259_25645.FStar_Syntax_Syntax.lbunivs); + (uu___3263_25683.FStar_Syntax_Syntax.lbunivs); FStar_Syntax_Syntax.lbtyp = - (uu___3259_25645.FStar_Syntax_Syntax.lbtyp); + (uu___3263_25683.FStar_Syntax_Syntax.lbtyp); FStar_Syntax_Syntax.lbeff = - (uu___3259_25645.FStar_Syntax_Syntax.lbeff); + (uu___3263_25683.FStar_Syntax_Syntax.lbeff); FStar_Syntax_Syntax.lbdef = - (uu___3259_25645.FStar_Syntax_Syntax.lbdef); + (uu___3263_25683.FStar_Syntax_Syntax.lbdef); FStar_Syntax_Syntax.lbattrs = - (uu___3259_25645.FStar_Syntax_Syntax.lbattrs); + (uu___3263_25683.FStar_Syntax_Syntax.lbattrs); FStar_Syntax_Syntax.lbpos = - (uu___3259_25645.FStar_Syntax_Syntax.lbpos) + (uu___3263_25683.FStar_Syntax_Syntax.lbpos) } in let env3 = FStar_TypeChecker_Env.push_let_binding @@ -9788,7 +9811,7 @@ and (check_inner_let_rec : in (env3, lb1)) env1) in - (match uu____25620 with + (match uu____25658 with | (env2,lbs4) -> let bvs = FStar_All.pipe_right lbs4 @@ -9797,8 +9820,8 @@ and (check_inner_let_rec : FStar_Util.left lb.FStar_Syntax_Syntax.lbname)) in - let uu____25672 = tc_term env2 e21 in - (match uu____25672 with + let uu____25710 = tc_term env2 e21 in + (match uu____25710 with | (e22,cres,g2) -> let cres1 = FStar_List.fold_right @@ -9818,17 +9841,17 @@ and (check_inner_let_rec : [FStar_Syntax_Syntax.SHOULD_NOT_INLINE] in let guard = - let uu____25696 = - let uu____25697 = + let uu____25734 = + let uu____25735 = FStar_List.map FStar_Syntax_Syntax.mk_binder bvs in FStar_TypeChecker_Env.close_guard - env2 uu____25697 g2 + env2 uu____25735 g2 in FStar_TypeChecker_Env.conj_guard - g_lbs uu____25696 + g_lbs uu____25734 in let cres4 = FStar_TypeChecker_Util.close_wp_lcomp @@ -9839,39 +9862,39 @@ and (check_inner_let_rec : cres4.FStar_TypeChecker_Common.res_typ in let cres5 = - let uu___3280_25707 = cres4 in + let uu___3284_25745 = cres4 in { FStar_TypeChecker_Common.eff_name = - (uu___3280_25707.FStar_TypeChecker_Common.eff_name); + (uu___3284_25745.FStar_TypeChecker_Common.eff_name); FStar_TypeChecker_Common.res_typ = tres; FStar_TypeChecker_Common.cflags = - (uu___3280_25707.FStar_TypeChecker_Common.cflags); + (uu___3284_25745.FStar_TypeChecker_Common.cflags); FStar_TypeChecker_Common.comp_thunk = - (uu___3280_25707.FStar_TypeChecker_Common.comp_thunk) + (uu___3284_25745.FStar_TypeChecker_Common.comp_thunk) } in let guard1 = let bs = FStar_All.pipe_right lbs4 (FStar_List.map (fun lb -> - let uu____25715 = + let uu____25753 = FStar_Util.left lb.FStar_Syntax_Syntax.lbname in FStar_Syntax_Syntax.mk_binder - uu____25715)) + uu____25753)) in FStar_TypeChecker_Util.close_guard_implicits env2 false bs guard in - let uu____25717 = + let uu____25755 = FStar_Syntax_Subst.close_let_rec lbs4 e22 in - (match uu____25717 with + (match uu____25755 with | (lbs5,e23) -> let e = FStar_Syntax_Syntax.mk @@ -9882,40 +9905,40 @@ and (check_inner_let_rec : in (match topt with | FStar_Pervasives_Native.Some - uu____25758 -> + uu____25796 -> (e, cres5, guard1) | FStar_Pervasives_Native.None -> - let uu____25759 = + let uu____25797 = check_no_escape FStar_Pervasives_Native.None env2 bvs tres in - (match uu____25759 with + (match uu____25797 with | (tres1,g_ex) -> let cres6 = - let uu___3296_25773 + let uu___3300_25811 = cres5 in { FStar_TypeChecker_Common.eff_name = - (uu___3296_25773.FStar_TypeChecker_Common.eff_name); + (uu___3300_25811.FStar_TypeChecker_Common.eff_name); FStar_TypeChecker_Common.res_typ = tres1; FStar_TypeChecker_Common.cflags = - (uu___3296_25773.FStar_TypeChecker_Common.cflags); + (uu___3300_25811.FStar_TypeChecker_Common.cflags); FStar_TypeChecker_Common.comp_thunk = - (uu___3296_25773.FStar_TypeChecker_Common.comp_thunk) + (uu___3300_25811.FStar_TypeChecker_Common.comp_thunk) } in - let uu____25774 = + let uu____25812 = FStar_TypeChecker_Env.conj_guard g_ex guard1 in (e, cres6, - uu____25774)))))))))) - | uu____25775 -> failwith "Impossible" + uu____25812)))))))))) + | uu____25813 -> failwith "Impossible" and (build_let_rec_env : Prims.bool -> @@ -9929,43 +9952,43 @@ and (build_let_rec_env : fun lbs -> let env0 = env in let termination_check_enabled lbname lbdef lbtyp = - let uu____25823 = FStar_Options.ml_ish () in - if uu____25823 + let uu____25861 = FStar_Options.ml_ish () in + if uu____25861 then false else (let t = FStar_TypeChecker_Normalize.unfold_whnf env lbtyp in - let uu____25831 = FStar_Syntax_Util.arrow_formals_comp t in - match uu____25831 with + let uu____25869 = FStar_Syntax_Util.arrow_formals_comp t in + match uu____25869 with | (formals,c) -> - let uu____25863 = FStar_Syntax_Util.abs_formals lbdef in - (match uu____25863 with - | (actuals,uu____25874,uu____25875) -> + let uu____25901 = FStar_Syntax_Util.abs_formals lbdef in + (match uu____25901 with + | (actuals,uu____25912,uu____25913) -> if ((FStar_List.length formals) < Prims.int_one) || ((FStar_List.length actuals) < Prims.int_one) then - let uu____25896 = - let uu____25902 = - let uu____25904 = + let uu____25934 = + let uu____25940 = + let uu____25942 = FStar_Syntax_Print.term_to_string lbdef in - let uu____25906 = + let uu____25944 = FStar_Syntax_Print.term_to_string lbtyp in FStar_Util.format2 "Only function literals with arrow types can be defined recursively; got %s : %s" - uu____25904 uu____25906 + uu____25942 uu____25944 in (FStar_Errors.Fatal_RecursiveFunctionLiteral, - uu____25902) + uu____25940) in - FStar_Errors.raise_error uu____25896 + FStar_Errors.raise_error uu____25934 lbtyp.FStar_Syntax_Syntax.pos else (let actuals1 = - let uu____25914 = + let uu____25952 = FStar_TypeChecker_Env.set_expected_typ env lbtyp in FStar_TypeChecker_Util.maybe_add_implicit_binders - uu____25914 actuals + uu____25952 actuals in if (FStar_List.length formals) <> @@ -9976,30 +9999,30 @@ and (build_let_rec_env : if n1 = Prims.int_one then "1 argument was found" else - (let uu____25945 = + (let uu____25983 = FStar_Util.string_of_int n1 in FStar_Util.format1 "%s arguments were found" - uu____25945) + uu____25983) in let formals_msg = let n1 = FStar_List.length formals in if n1 = Prims.int_one then "1 argument" else - (let uu____25964 = + (let uu____26002 = FStar_Util.string_of_int n1 in FStar_Util.format1 "%s arguments" - uu____25964) + uu____26002) in let msg = - let uu____25969 = + let uu____26007 = FStar_Syntax_Print.term_to_string lbtyp in - let uu____25971 = + let uu____26009 = FStar_Syntax_Print.lbname_to_string lbname in FStar_Util.format4 "From its type %s, the definition of `let rec %s` expects a function with %s, but %s" - uu____25969 uu____25971 formals_msg + uu____26007 uu____26009 formals_msg actuals_msg in FStar_Errors.raise_error @@ -10014,17 +10037,17 @@ and (build_let_rec_env : (FStar_List.contains FStar_Syntax_Syntax.TotalEffect))))) in - let uu____25983 = + let uu____26021 = FStar_List.fold_left - (fun uu____26016 -> + (fun uu____26054 -> fun lb -> - match uu____26016 with + match uu____26054 with | (lbs1,env1,g_acc) -> - let uu____26041 = + let uu____26079 = FStar_TypeChecker_Util.extract_let_rec_annotation env1 lb in - (match uu____26041 with + (match uu____26079 with | (univ_vars1,t,check_t) -> let env2 = FStar_TypeChecker_Env.push_univ_vars env1 @@ -10034,7 +10057,7 @@ and (build_let_rec_env : FStar_Syntax_Util.unascribe lb.FStar_Syntax_Syntax.lbdef in - let uu____26064 = + let uu____26102 = if Prims.op_Negation check_t then (g_acc, t) else @@ -10042,237 +10065,237 @@ and (build_let_rec_env : FStar_TypeChecker_Env.push_univ_vars env0 univ_vars1 in - let uu____26083 = - let uu____26090 = - let uu____26091 = + let uu____26121 = + let uu____26128 = + let uu____26129 = FStar_Syntax_Util.type_u () in FStar_All.pipe_left - FStar_Pervasives_Native.fst uu____26091 + FStar_Pervasives_Native.fst uu____26129 in tc_check_tot_or_gtot_term - (let uu___3342_26102 = env01 in + (let uu___3346_26140 = env01 in { FStar_TypeChecker_Env.solver = - (uu___3342_26102.FStar_TypeChecker_Env.solver); + (uu___3346_26140.FStar_TypeChecker_Env.solver); FStar_TypeChecker_Env.range = - (uu___3342_26102.FStar_TypeChecker_Env.range); + (uu___3346_26140.FStar_TypeChecker_Env.range); FStar_TypeChecker_Env.curmodule = - (uu___3342_26102.FStar_TypeChecker_Env.curmodule); + (uu___3346_26140.FStar_TypeChecker_Env.curmodule); FStar_TypeChecker_Env.gamma = - (uu___3342_26102.FStar_TypeChecker_Env.gamma); + (uu___3346_26140.FStar_TypeChecker_Env.gamma); FStar_TypeChecker_Env.gamma_sig = - (uu___3342_26102.FStar_TypeChecker_Env.gamma_sig); + (uu___3346_26140.FStar_TypeChecker_Env.gamma_sig); FStar_TypeChecker_Env.gamma_cache = - (uu___3342_26102.FStar_TypeChecker_Env.gamma_cache); + (uu___3346_26140.FStar_TypeChecker_Env.gamma_cache); FStar_TypeChecker_Env.modules = - (uu___3342_26102.FStar_TypeChecker_Env.modules); + (uu___3346_26140.FStar_TypeChecker_Env.modules); FStar_TypeChecker_Env.expected_typ = - (uu___3342_26102.FStar_TypeChecker_Env.expected_typ); + (uu___3346_26140.FStar_TypeChecker_Env.expected_typ); FStar_TypeChecker_Env.sigtab = - (uu___3342_26102.FStar_TypeChecker_Env.sigtab); + (uu___3346_26140.FStar_TypeChecker_Env.sigtab); FStar_TypeChecker_Env.attrtab = - (uu___3342_26102.FStar_TypeChecker_Env.attrtab); + (uu___3346_26140.FStar_TypeChecker_Env.attrtab); FStar_TypeChecker_Env.instantiate_imp = - (uu___3342_26102.FStar_TypeChecker_Env.instantiate_imp); + (uu___3346_26140.FStar_TypeChecker_Env.instantiate_imp); FStar_TypeChecker_Env.effects = - (uu___3342_26102.FStar_TypeChecker_Env.effects); + (uu___3346_26140.FStar_TypeChecker_Env.effects); FStar_TypeChecker_Env.generalize = - (uu___3342_26102.FStar_TypeChecker_Env.generalize); + (uu___3346_26140.FStar_TypeChecker_Env.generalize); FStar_TypeChecker_Env.letrecs = - (uu___3342_26102.FStar_TypeChecker_Env.letrecs); + (uu___3346_26140.FStar_TypeChecker_Env.letrecs); FStar_TypeChecker_Env.top_level = - (uu___3342_26102.FStar_TypeChecker_Env.top_level); + (uu___3346_26140.FStar_TypeChecker_Env.top_level); FStar_TypeChecker_Env.check_uvars = true; FStar_TypeChecker_Env.use_eq = - (uu___3342_26102.FStar_TypeChecker_Env.use_eq); + (uu___3346_26140.FStar_TypeChecker_Env.use_eq); FStar_TypeChecker_Env.is_iface = - (uu___3342_26102.FStar_TypeChecker_Env.is_iface); + (uu___3346_26140.FStar_TypeChecker_Env.is_iface); FStar_TypeChecker_Env.admit = - (uu___3342_26102.FStar_TypeChecker_Env.admit); + (uu___3346_26140.FStar_TypeChecker_Env.admit); FStar_TypeChecker_Env.lax = - (uu___3342_26102.FStar_TypeChecker_Env.lax); + (uu___3346_26140.FStar_TypeChecker_Env.lax); FStar_TypeChecker_Env.lax_universes = - (uu___3342_26102.FStar_TypeChecker_Env.lax_universes); + (uu___3346_26140.FStar_TypeChecker_Env.lax_universes); FStar_TypeChecker_Env.phase1 = - (uu___3342_26102.FStar_TypeChecker_Env.phase1); + (uu___3346_26140.FStar_TypeChecker_Env.phase1); FStar_TypeChecker_Env.failhard = - (uu___3342_26102.FStar_TypeChecker_Env.failhard); + (uu___3346_26140.FStar_TypeChecker_Env.failhard); FStar_TypeChecker_Env.nosynth = - (uu___3342_26102.FStar_TypeChecker_Env.nosynth); + (uu___3346_26140.FStar_TypeChecker_Env.nosynth); FStar_TypeChecker_Env.uvar_subtyping = - (uu___3342_26102.FStar_TypeChecker_Env.uvar_subtyping); + (uu___3346_26140.FStar_TypeChecker_Env.uvar_subtyping); FStar_TypeChecker_Env.tc_term = - (uu___3342_26102.FStar_TypeChecker_Env.tc_term); + (uu___3346_26140.FStar_TypeChecker_Env.tc_term); FStar_TypeChecker_Env.type_of = - (uu___3342_26102.FStar_TypeChecker_Env.type_of); + (uu___3346_26140.FStar_TypeChecker_Env.type_of); FStar_TypeChecker_Env.universe_of = - (uu___3342_26102.FStar_TypeChecker_Env.universe_of); + (uu___3346_26140.FStar_TypeChecker_Env.universe_of); FStar_TypeChecker_Env.check_type_of = - (uu___3342_26102.FStar_TypeChecker_Env.check_type_of); + (uu___3346_26140.FStar_TypeChecker_Env.check_type_of); FStar_TypeChecker_Env.use_bv_sorts = - (uu___3342_26102.FStar_TypeChecker_Env.use_bv_sorts); + (uu___3346_26140.FStar_TypeChecker_Env.use_bv_sorts); FStar_TypeChecker_Env.qtbl_name_and_index = - (uu___3342_26102.FStar_TypeChecker_Env.qtbl_name_and_index); + (uu___3346_26140.FStar_TypeChecker_Env.qtbl_name_and_index); FStar_TypeChecker_Env.normalized_eff_names = - (uu___3342_26102.FStar_TypeChecker_Env.normalized_eff_names); + (uu___3346_26140.FStar_TypeChecker_Env.normalized_eff_names); FStar_TypeChecker_Env.fv_delta_depths = - (uu___3342_26102.FStar_TypeChecker_Env.fv_delta_depths); + (uu___3346_26140.FStar_TypeChecker_Env.fv_delta_depths); FStar_TypeChecker_Env.proof_ns = - (uu___3342_26102.FStar_TypeChecker_Env.proof_ns); + (uu___3346_26140.FStar_TypeChecker_Env.proof_ns); FStar_TypeChecker_Env.synth_hook = - (uu___3342_26102.FStar_TypeChecker_Env.synth_hook); + (uu___3346_26140.FStar_TypeChecker_Env.synth_hook); FStar_TypeChecker_Env.splice = - (uu___3342_26102.FStar_TypeChecker_Env.splice); + (uu___3346_26140.FStar_TypeChecker_Env.splice); FStar_TypeChecker_Env.mpreprocess = - (uu___3342_26102.FStar_TypeChecker_Env.mpreprocess); + (uu___3346_26140.FStar_TypeChecker_Env.mpreprocess); FStar_TypeChecker_Env.postprocess = - (uu___3342_26102.FStar_TypeChecker_Env.postprocess); + (uu___3346_26140.FStar_TypeChecker_Env.postprocess); FStar_TypeChecker_Env.is_native_tactic = - (uu___3342_26102.FStar_TypeChecker_Env.is_native_tactic); + (uu___3346_26140.FStar_TypeChecker_Env.is_native_tactic); FStar_TypeChecker_Env.identifier_info = - (uu___3342_26102.FStar_TypeChecker_Env.identifier_info); + (uu___3346_26140.FStar_TypeChecker_Env.identifier_info); FStar_TypeChecker_Env.tc_hooks = - (uu___3342_26102.FStar_TypeChecker_Env.tc_hooks); + (uu___3346_26140.FStar_TypeChecker_Env.tc_hooks); FStar_TypeChecker_Env.dsenv = - (uu___3342_26102.FStar_TypeChecker_Env.dsenv); + (uu___3346_26140.FStar_TypeChecker_Env.dsenv); FStar_TypeChecker_Env.nbe = - (uu___3342_26102.FStar_TypeChecker_Env.nbe); + (uu___3346_26140.FStar_TypeChecker_Env.nbe); FStar_TypeChecker_Env.strict_args_tab = - (uu___3342_26102.FStar_TypeChecker_Env.strict_args_tab); + (uu___3346_26140.FStar_TypeChecker_Env.strict_args_tab); FStar_TypeChecker_Env.erasable_types_tab = - (uu___3342_26102.FStar_TypeChecker_Env.erasable_types_tab) - }) t uu____26090 + (uu___3346_26140.FStar_TypeChecker_Env.erasable_types_tab) + }) t uu____26128 in - match uu____26083 with - | (t1,uu____26111,g) -> - let uu____26113 = - let uu____26114 = - let uu____26115 = + match uu____26121 with + | (t1,uu____26149,g) -> + let uu____26151 = + let uu____26152 = + let uu____26153 = FStar_All.pipe_right g (FStar_TypeChecker_Rel.resolve_implicits env2) in - FStar_All.pipe_right uu____26115 + FStar_All.pipe_right uu____26153 (FStar_TypeChecker_Rel.discharge_guard env2) in FStar_TypeChecker_Env.conj_guard g_acc - uu____26114 + uu____26152 in - let uu____26116 = norm env01 t1 in - (uu____26113, uu____26116)) + let uu____26154 = norm env01 t1 in + (uu____26151, uu____26154)) in - (match uu____26064 with + (match uu____26102 with | (g,t1) -> let env3 = - let uu____26136 = + let uu____26174 = termination_check_enabled lb.FStar_Syntax_Syntax.lbname e t1 in - if uu____26136 + if uu____26174 then - let uu___3352_26139 = env2 in + let uu___3356_26177 = env2 in { FStar_TypeChecker_Env.solver = - (uu___3352_26139.FStar_TypeChecker_Env.solver); + (uu___3356_26177.FStar_TypeChecker_Env.solver); FStar_TypeChecker_Env.range = - (uu___3352_26139.FStar_TypeChecker_Env.range); + (uu___3356_26177.FStar_TypeChecker_Env.range); FStar_TypeChecker_Env.curmodule = - (uu___3352_26139.FStar_TypeChecker_Env.curmodule); + (uu___3356_26177.FStar_TypeChecker_Env.curmodule); FStar_TypeChecker_Env.gamma = - (uu___3352_26139.FStar_TypeChecker_Env.gamma); + (uu___3356_26177.FStar_TypeChecker_Env.gamma); FStar_TypeChecker_Env.gamma_sig = - (uu___3352_26139.FStar_TypeChecker_Env.gamma_sig); + (uu___3356_26177.FStar_TypeChecker_Env.gamma_sig); FStar_TypeChecker_Env.gamma_cache = - (uu___3352_26139.FStar_TypeChecker_Env.gamma_cache); + (uu___3356_26177.FStar_TypeChecker_Env.gamma_cache); FStar_TypeChecker_Env.modules = - (uu___3352_26139.FStar_TypeChecker_Env.modules); + (uu___3356_26177.FStar_TypeChecker_Env.modules); FStar_TypeChecker_Env.expected_typ = - (uu___3352_26139.FStar_TypeChecker_Env.expected_typ); + (uu___3356_26177.FStar_TypeChecker_Env.expected_typ); FStar_TypeChecker_Env.sigtab = - (uu___3352_26139.FStar_TypeChecker_Env.sigtab); + (uu___3356_26177.FStar_TypeChecker_Env.sigtab); FStar_TypeChecker_Env.attrtab = - (uu___3352_26139.FStar_TypeChecker_Env.attrtab); + (uu___3356_26177.FStar_TypeChecker_Env.attrtab); FStar_TypeChecker_Env.instantiate_imp = - (uu___3352_26139.FStar_TypeChecker_Env.instantiate_imp); + (uu___3356_26177.FStar_TypeChecker_Env.instantiate_imp); FStar_TypeChecker_Env.effects = - (uu___3352_26139.FStar_TypeChecker_Env.effects); + (uu___3356_26177.FStar_TypeChecker_Env.effects); FStar_TypeChecker_Env.generalize = - (uu___3352_26139.FStar_TypeChecker_Env.generalize); + (uu___3356_26177.FStar_TypeChecker_Env.generalize); FStar_TypeChecker_Env.letrecs = (((lb.FStar_Syntax_Syntax.lbname), t1, univ_vars1) :: (env2.FStar_TypeChecker_Env.letrecs)); FStar_TypeChecker_Env.top_level = - (uu___3352_26139.FStar_TypeChecker_Env.top_level); + (uu___3356_26177.FStar_TypeChecker_Env.top_level); FStar_TypeChecker_Env.check_uvars = - (uu___3352_26139.FStar_TypeChecker_Env.check_uvars); + (uu___3356_26177.FStar_TypeChecker_Env.check_uvars); FStar_TypeChecker_Env.use_eq = - (uu___3352_26139.FStar_TypeChecker_Env.use_eq); + (uu___3356_26177.FStar_TypeChecker_Env.use_eq); FStar_TypeChecker_Env.is_iface = - (uu___3352_26139.FStar_TypeChecker_Env.is_iface); + (uu___3356_26177.FStar_TypeChecker_Env.is_iface); FStar_TypeChecker_Env.admit = - (uu___3352_26139.FStar_TypeChecker_Env.admit); + (uu___3356_26177.FStar_TypeChecker_Env.admit); FStar_TypeChecker_Env.lax = - (uu___3352_26139.FStar_TypeChecker_Env.lax); + (uu___3356_26177.FStar_TypeChecker_Env.lax); FStar_TypeChecker_Env.lax_universes = - (uu___3352_26139.FStar_TypeChecker_Env.lax_universes); + (uu___3356_26177.FStar_TypeChecker_Env.lax_universes); FStar_TypeChecker_Env.phase1 = - (uu___3352_26139.FStar_TypeChecker_Env.phase1); + (uu___3356_26177.FStar_TypeChecker_Env.phase1); FStar_TypeChecker_Env.failhard = - (uu___3352_26139.FStar_TypeChecker_Env.failhard); + (uu___3356_26177.FStar_TypeChecker_Env.failhard); FStar_TypeChecker_Env.nosynth = - (uu___3352_26139.FStar_TypeChecker_Env.nosynth); + (uu___3356_26177.FStar_TypeChecker_Env.nosynth); FStar_TypeChecker_Env.uvar_subtyping = - (uu___3352_26139.FStar_TypeChecker_Env.uvar_subtyping); + (uu___3356_26177.FStar_TypeChecker_Env.uvar_subtyping); FStar_TypeChecker_Env.tc_term = - (uu___3352_26139.FStar_TypeChecker_Env.tc_term); + (uu___3356_26177.FStar_TypeChecker_Env.tc_term); FStar_TypeChecker_Env.type_of = - (uu___3352_26139.FStar_TypeChecker_Env.type_of); + (uu___3356_26177.FStar_TypeChecker_Env.type_of); FStar_TypeChecker_Env.universe_of = - (uu___3352_26139.FStar_TypeChecker_Env.universe_of); + (uu___3356_26177.FStar_TypeChecker_Env.universe_of); FStar_TypeChecker_Env.check_type_of = - (uu___3352_26139.FStar_TypeChecker_Env.check_type_of); + (uu___3356_26177.FStar_TypeChecker_Env.check_type_of); FStar_TypeChecker_Env.use_bv_sorts = - (uu___3352_26139.FStar_TypeChecker_Env.use_bv_sorts); + (uu___3356_26177.FStar_TypeChecker_Env.use_bv_sorts); FStar_TypeChecker_Env.qtbl_name_and_index = - (uu___3352_26139.FStar_TypeChecker_Env.qtbl_name_and_index); + (uu___3356_26177.FStar_TypeChecker_Env.qtbl_name_and_index); FStar_TypeChecker_Env.normalized_eff_names = - (uu___3352_26139.FStar_TypeChecker_Env.normalized_eff_names); + (uu___3356_26177.FStar_TypeChecker_Env.normalized_eff_names); FStar_TypeChecker_Env.fv_delta_depths = - (uu___3352_26139.FStar_TypeChecker_Env.fv_delta_depths); + (uu___3356_26177.FStar_TypeChecker_Env.fv_delta_depths); FStar_TypeChecker_Env.proof_ns = - (uu___3352_26139.FStar_TypeChecker_Env.proof_ns); + (uu___3356_26177.FStar_TypeChecker_Env.proof_ns); FStar_TypeChecker_Env.synth_hook = - (uu___3352_26139.FStar_TypeChecker_Env.synth_hook); + (uu___3356_26177.FStar_TypeChecker_Env.synth_hook); FStar_TypeChecker_Env.splice = - (uu___3352_26139.FStar_TypeChecker_Env.splice); + (uu___3356_26177.FStar_TypeChecker_Env.splice); FStar_TypeChecker_Env.mpreprocess = - (uu___3352_26139.FStar_TypeChecker_Env.mpreprocess); + (uu___3356_26177.FStar_TypeChecker_Env.mpreprocess); FStar_TypeChecker_Env.postprocess = - (uu___3352_26139.FStar_TypeChecker_Env.postprocess); + (uu___3356_26177.FStar_TypeChecker_Env.postprocess); FStar_TypeChecker_Env.is_native_tactic = - (uu___3352_26139.FStar_TypeChecker_Env.is_native_tactic); + (uu___3356_26177.FStar_TypeChecker_Env.is_native_tactic); FStar_TypeChecker_Env.identifier_info = - (uu___3352_26139.FStar_TypeChecker_Env.identifier_info); + (uu___3356_26177.FStar_TypeChecker_Env.identifier_info); FStar_TypeChecker_Env.tc_hooks = - (uu___3352_26139.FStar_TypeChecker_Env.tc_hooks); + (uu___3356_26177.FStar_TypeChecker_Env.tc_hooks); FStar_TypeChecker_Env.dsenv = - (uu___3352_26139.FStar_TypeChecker_Env.dsenv); + (uu___3356_26177.FStar_TypeChecker_Env.dsenv); FStar_TypeChecker_Env.nbe = - (uu___3352_26139.FStar_TypeChecker_Env.nbe); + (uu___3356_26177.FStar_TypeChecker_Env.nbe); FStar_TypeChecker_Env.strict_args_tab = - (uu___3352_26139.FStar_TypeChecker_Env.strict_args_tab); + (uu___3356_26177.FStar_TypeChecker_Env.strict_args_tab); FStar_TypeChecker_Env.erasable_types_tab = - (uu___3352_26139.FStar_TypeChecker_Env.erasable_types_tab) + (uu___3356_26177.FStar_TypeChecker_Env.erasable_types_tab) } else FStar_TypeChecker_Env.push_let_binding @@ -10280,24 +10303,24 @@ and (build_let_rec_env : (univ_vars1, t1) in let lb1 = - let uu___3355_26153 = lb in + let uu___3359_26191 = lb in { FStar_Syntax_Syntax.lbname = - (uu___3355_26153.FStar_Syntax_Syntax.lbname); + (uu___3359_26191.FStar_Syntax_Syntax.lbname); FStar_Syntax_Syntax.lbunivs = univ_vars1; FStar_Syntax_Syntax.lbtyp = t1; FStar_Syntax_Syntax.lbeff = - (uu___3355_26153.FStar_Syntax_Syntax.lbeff); + (uu___3359_26191.FStar_Syntax_Syntax.lbeff); FStar_Syntax_Syntax.lbdef = e; FStar_Syntax_Syntax.lbattrs = - (uu___3355_26153.FStar_Syntax_Syntax.lbattrs); + (uu___3359_26191.FStar_Syntax_Syntax.lbattrs); FStar_Syntax_Syntax.lbpos = - (uu___3355_26153.FStar_Syntax_Syntax.lbpos) + (uu___3359_26191.FStar_Syntax_Syntax.lbpos) } in ((lb1 :: lbs1), env3, g)))) ([], env, FStar_TypeChecker_Env.trivial_guard) lbs in - match uu____25983 with + match uu____26021 with | (lbs1,env1,g) -> ((FStar_List.rev lbs1), env1, g) and (check_let_recs : @@ -10308,64 +10331,64 @@ and (check_let_recs : = fun env -> fun lbs -> - let uu____26179 = - let uu____26188 = + let uu____26217 = + let uu____26226 = FStar_All.pipe_right lbs (FStar_List.map (fun lb -> - let uu____26214 = + let uu____26252 = FStar_Syntax_Util.abs_formals lb.FStar_Syntax_Syntax.lbdef in - match uu____26214 with + match uu____26252 with | (bs,t,lcomp) -> (match bs with | [] -> - let uu____26244 = + let uu____26282 = FStar_Syntax_Syntax.range_of_lbname lb.FStar_Syntax_Syntax.lbname in FStar_Errors.raise_error (FStar_Errors.Fatal_RecursiveFunctionLiteral, "Only function literals may be defined recursively") - uu____26244 - | uu____26251 -> + uu____26282 + | uu____26289 -> let lb1 = - let uu___3372_26254 = lb in - let uu____26255 = + let uu___3376_26292 = lb in + let uu____26293 = FStar_Syntax_Util.abs bs t lcomp in { FStar_Syntax_Syntax.lbname = - (uu___3372_26254.FStar_Syntax_Syntax.lbname); + (uu___3376_26292.FStar_Syntax_Syntax.lbname); FStar_Syntax_Syntax.lbunivs = - (uu___3372_26254.FStar_Syntax_Syntax.lbunivs); + (uu___3376_26292.FStar_Syntax_Syntax.lbunivs); FStar_Syntax_Syntax.lbtyp = - (uu___3372_26254.FStar_Syntax_Syntax.lbtyp); + (uu___3376_26292.FStar_Syntax_Syntax.lbtyp); FStar_Syntax_Syntax.lbeff = - (uu___3372_26254.FStar_Syntax_Syntax.lbeff); - FStar_Syntax_Syntax.lbdef = uu____26255; + (uu___3376_26292.FStar_Syntax_Syntax.lbeff); + FStar_Syntax_Syntax.lbdef = uu____26293; FStar_Syntax_Syntax.lbattrs = - (uu___3372_26254.FStar_Syntax_Syntax.lbattrs); + (uu___3376_26292.FStar_Syntax_Syntax.lbattrs); FStar_Syntax_Syntax.lbpos = - (uu___3372_26254.FStar_Syntax_Syntax.lbpos) + (uu___3376_26292.FStar_Syntax_Syntax.lbpos) } in - let uu____26258 = - let uu____26265 = + let uu____26296 = + let uu____26303 = FStar_TypeChecker_Env.set_expected_typ env lb1.FStar_Syntax_Syntax.lbtyp in - tc_tot_or_gtot_term uu____26265 + tc_tot_or_gtot_term uu____26303 lb1.FStar_Syntax_Syntax.lbdef in - (match uu____26258 with + (match uu____26296 with | (e,c,g) -> - ((let uu____26274 = - let uu____26276 = + ((let uu____26312 = + let uu____26314 = FStar_TypeChecker_Common.is_total_lcomp c in - Prims.op_Negation uu____26276 in - if uu____26274 + Prims.op_Negation uu____26314 in + if uu____26312 then FStar_Errors.raise_error (FStar_Errors.Fatal_UnexpectedGTotForLetRec, @@ -10383,8 +10406,8 @@ and (check_let_recs : in (lb2, g))))))) in - FStar_All.pipe_right uu____26188 FStar_List.unzip in - match uu____26179 with + FStar_All.pipe_right uu____26226 FStar_List.unzip in + match uu____26217 with | (lbs1,gs) -> let g_lbs = FStar_List.fold_right FStar_TypeChecker_Env.conj_guard gs @@ -10403,12 +10426,12 @@ and (check_let_bound_def : fun top_level -> fun env -> fun lb -> - let uu____26332 = FStar_TypeChecker_Env.clear_expected_typ env in - match uu____26332 with - | (env1,uu____26351) -> + let uu____26370 = FStar_TypeChecker_Env.clear_expected_typ env in + match uu____26370 with + | (env1,uu____26389) -> let e1 = lb.FStar_Syntax_Syntax.lbdef in - let uu____26359 = check_lbtyp top_level env lb in - (match uu____26359 with + let uu____26397 = check_lbtyp top_level env lb in + (match uu____26397 with | (topt,wf_annot,univ_vars1,univ_opening,env11) -> (if (Prims.op_Negation top_level) && (univ_vars1 <> []) then @@ -10418,140 +10441,140 @@ and (check_let_bound_def : e1.FStar_Syntax_Syntax.pos else (); (let e11 = FStar_Syntax_Subst.subst univ_opening e1 in - let uu____26408 = + let uu____26446 = tc_maybe_toplevel_term - (let uu___3403_26417 = env11 in + (let uu___3407_26455 = env11 in { FStar_TypeChecker_Env.solver = - (uu___3403_26417.FStar_TypeChecker_Env.solver); + (uu___3407_26455.FStar_TypeChecker_Env.solver); FStar_TypeChecker_Env.range = - (uu___3403_26417.FStar_TypeChecker_Env.range); + (uu___3407_26455.FStar_TypeChecker_Env.range); FStar_TypeChecker_Env.curmodule = - (uu___3403_26417.FStar_TypeChecker_Env.curmodule); + (uu___3407_26455.FStar_TypeChecker_Env.curmodule); FStar_TypeChecker_Env.gamma = - (uu___3403_26417.FStar_TypeChecker_Env.gamma); + (uu___3407_26455.FStar_TypeChecker_Env.gamma); FStar_TypeChecker_Env.gamma_sig = - (uu___3403_26417.FStar_TypeChecker_Env.gamma_sig); + (uu___3407_26455.FStar_TypeChecker_Env.gamma_sig); FStar_TypeChecker_Env.gamma_cache = - (uu___3403_26417.FStar_TypeChecker_Env.gamma_cache); + (uu___3407_26455.FStar_TypeChecker_Env.gamma_cache); FStar_TypeChecker_Env.modules = - (uu___3403_26417.FStar_TypeChecker_Env.modules); + (uu___3407_26455.FStar_TypeChecker_Env.modules); FStar_TypeChecker_Env.expected_typ = - (uu___3403_26417.FStar_TypeChecker_Env.expected_typ); + (uu___3407_26455.FStar_TypeChecker_Env.expected_typ); FStar_TypeChecker_Env.sigtab = - (uu___3403_26417.FStar_TypeChecker_Env.sigtab); + (uu___3407_26455.FStar_TypeChecker_Env.sigtab); FStar_TypeChecker_Env.attrtab = - (uu___3403_26417.FStar_TypeChecker_Env.attrtab); + (uu___3407_26455.FStar_TypeChecker_Env.attrtab); FStar_TypeChecker_Env.instantiate_imp = - (uu___3403_26417.FStar_TypeChecker_Env.instantiate_imp); + (uu___3407_26455.FStar_TypeChecker_Env.instantiate_imp); FStar_TypeChecker_Env.effects = - (uu___3403_26417.FStar_TypeChecker_Env.effects); + (uu___3407_26455.FStar_TypeChecker_Env.effects); FStar_TypeChecker_Env.generalize = - (uu___3403_26417.FStar_TypeChecker_Env.generalize); + (uu___3407_26455.FStar_TypeChecker_Env.generalize); FStar_TypeChecker_Env.letrecs = - (uu___3403_26417.FStar_TypeChecker_Env.letrecs); + (uu___3407_26455.FStar_TypeChecker_Env.letrecs); FStar_TypeChecker_Env.top_level = top_level; FStar_TypeChecker_Env.check_uvars = - (uu___3403_26417.FStar_TypeChecker_Env.check_uvars); + (uu___3407_26455.FStar_TypeChecker_Env.check_uvars); FStar_TypeChecker_Env.use_eq = - (uu___3403_26417.FStar_TypeChecker_Env.use_eq); + (uu___3407_26455.FStar_TypeChecker_Env.use_eq); FStar_TypeChecker_Env.is_iface = - (uu___3403_26417.FStar_TypeChecker_Env.is_iface); + (uu___3407_26455.FStar_TypeChecker_Env.is_iface); FStar_TypeChecker_Env.admit = - (uu___3403_26417.FStar_TypeChecker_Env.admit); + (uu___3407_26455.FStar_TypeChecker_Env.admit); FStar_TypeChecker_Env.lax = - (uu___3403_26417.FStar_TypeChecker_Env.lax); + (uu___3407_26455.FStar_TypeChecker_Env.lax); FStar_TypeChecker_Env.lax_universes = - (uu___3403_26417.FStar_TypeChecker_Env.lax_universes); + (uu___3407_26455.FStar_TypeChecker_Env.lax_universes); FStar_TypeChecker_Env.phase1 = - (uu___3403_26417.FStar_TypeChecker_Env.phase1); + (uu___3407_26455.FStar_TypeChecker_Env.phase1); FStar_TypeChecker_Env.failhard = - (uu___3403_26417.FStar_TypeChecker_Env.failhard); + (uu___3407_26455.FStar_TypeChecker_Env.failhard); FStar_TypeChecker_Env.nosynth = - (uu___3403_26417.FStar_TypeChecker_Env.nosynth); + (uu___3407_26455.FStar_TypeChecker_Env.nosynth); FStar_TypeChecker_Env.uvar_subtyping = - (uu___3403_26417.FStar_TypeChecker_Env.uvar_subtyping); + (uu___3407_26455.FStar_TypeChecker_Env.uvar_subtyping); FStar_TypeChecker_Env.tc_term = - (uu___3403_26417.FStar_TypeChecker_Env.tc_term); + (uu___3407_26455.FStar_TypeChecker_Env.tc_term); FStar_TypeChecker_Env.type_of = - (uu___3403_26417.FStar_TypeChecker_Env.type_of); + (uu___3407_26455.FStar_TypeChecker_Env.type_of); FStar_TypeChecker_Env.universe_of = - (uu___3403_26417.FStar_TypeChecker_Env.universe_of); + (uu___3407_26455.FStar_TypeChecker_Env.universe_of); FStar_TypeChecker_Env.check_type_of = - (uu___3403_26417.FStar_TypeChecker_Env.check_type_of); + (uu___3407_26455.FStar_TypeChecker_Env.check_type_of); FStar_TypeChecker_Env.use_bv_sorts = - (uu___3403_26417.FStar_TypeChecker_Env.use_bv_sorts); + (uu___3407_26455.FStar_TypeChecker_Env.use_bv_sorts); FStar_TypeChecker_Env.qtbl_name_and_index = - (uu___3403_26417.FStar_TypeChecker_Env.qtbl_name_and_index); + (uu___3407_26455.FStar_TypeChecker_Env.qtbl_name_and_index); FStar_TypeChecker_Env.normalized_eff_names = - (uu___3403_26417.FStar_TypeChecker_Env.normalized_eff_names); + (uu___3407_26455.FStar_TypeChecker_Env.normalized_eff_names); FStar_TypeChecker_Env.fv_delta_depths = - (uu___3403_26417.FStar_TypeChecker_Env.fv_delta_depths); + (uu___3407_26455.FStar_TypeChecker_Env.fv_delta_depths); FStar_TypeChecker_Env.proof_ns = - (uu___3403_26417.FStar_TypeChecker_Env.proof_ns); + (uu___3407_26455.FStar_TypeChecker_Env.proof_ns); FStar_TypeChecker_Env.synth_hook = - (uu___3403_26417.FStar_TypeChecker_Env.synth_hook); + (uu___3407_26455.FStar_TypeChecker_Env.synth_hook); FStar_TypeChecker_Env.splice = - (uu___3403_26417.FStar_TypeChecker_Env.splice); + (uu___3407_26455.FStar_TypeChecker_Env.splice); FStar_TypeChecker_Env.mpreprocess = - (uu___3403_26417.FStar_TypeChecker_Env.mpreprocess); + (uu___3407_26455.FStar_TypeChecker_Env.mpreprocess); FStar_TypeChecker_Env.postprocess = - (uu___3403_26417.FStar_TypeChecker_Env.postprocess); + (uu___3407_26455.FStar_TypeChecker_Env.postprocess); FStar_TypeChecker_Env.is_native_tactic = - (uu___3403_26417.FStar_TypeChecker_Env.is_native_tactic); + (uu___3407_26455.FStar_TypeChecker_Env.is_native_tactic); FStar_TypeChecker_Env.identifier_info = - (uu___3403_26417.FStar_TypeChecker_Env.identifier_info); + (uu___3407_26455.FStar_TypeChecker_Env.identifier_info); FStar_TypeChecker_Env.tc_hooks = - (uu___3403_26417.FStar_TypeChecker_Env.tc_hooks); + (uu___3407_26455.FStar_TypeChecker_Env.tc_hooks); FStar_TypeChecker_Env.dsenv = - (uu___3403_26417.FStar_TypeChecker_Env.dsenv); + (uu___3407_26455.FStar_TypeChecker_Env.dsenv); FStar_TypeChecker_Env.nbe = - (uu___3403_26417.FStar_TypeChecker_Env.nbe); + (uu___3407_26455.FStar_TypeChecker_Env.nbe); FStar_TypeChecker_Env.strict_args_tab = - (uu___3403_26417.FStar_TypeChecker_Env.strict_args_tab); + (uu___3407_26455.FStar_TypeChecker_Env.strict_args_tab); FStar_TypeChecker_Env.erasable_types_tab = - (uu___3403_26417.FStar_TypeChecker_Env.erasable_types_tab) + (uu___3407_26455.FStar_TypeChecker_Env.erasable_types_tab) }) e11 in - match uu____26408 with + match uu____26446 with | (e12,c1,g1) -> - let uu____26432 = - let uu____26437 = + let uu____26470 = + let uu____26475 = FStar_TypeChecker_Env.set_range env11 e12.FStar_Syntax_Syntax.pos in FStar_TypeChecker_Util.strengthen_precondition (FStar_Pervasives_Native.Some - (fun uu____26443 -> + (fun uu____26481 -> FStar_Util.return_all FStar_TypeChecker_Err.ill_kinded_type)) - uu____26437 e12 c1 wf_annot + uu____26475 e12 c1 wf_annot in - (match uu____26432 with + (match uu____26470 with | (c11,guard_f) -> let g11 = FStar_TypeChecker_Env.conj_guard g1 guard_f in - ((let uu____26460 = + ((let uu____26498 = FStar_TypeChecker_Env.debug env FStar_Options.Extreme in - if uu____26460 + if uu____26498 then - let uu____26463 = + let uu____26501 = FStar_Syntax_Print.lbname_to_string lb.FStar_Syntax_Syntax.lbname in - let uu____26465 = + let uu____26503 = FStar_TypeChecker_Common.lcomp_to_string c11 in - let uu____26467 = + let uu____26505 = FStar_TypeChecker_Rel.guard_to_string env g11 in FStar_Util.print3 "checked let-bound def %s : %s guard is %s\n" - uu____26463 uu____26465 uu____26467 + uu____26501 uu____26503 uu____26505 else ()); (e12, univ_vars1, c11, g11, (FStar_Option.isSome topt))))))) @@ -10571,23 +10594,23 @@ and (check_lbtyp : let t = FStar_Syntax_Subst.compress lb.FStar_Syntax_Syntax.lbtyp in match t.FStar_Syntax_Syntax.n with | FStar_Syntax_Syntax.Tm_unknown -> - let uu____26506 = + let uu____26544 = FStar_Syntax_Subst.univ_var_opening lb.FStar_Syntax_Syntax.lbunivs in - (match uu____26506 with + (match uu____26544 with | (univ_opening,univ_vars1) -> - let uu____26539 = + let uu____26577 = FStar_TypeChecker_Env.push_univ_vars env univ_vars1 in (FStar_Pervasives_Native.None, FStar_TypeChecker_Env.trivial_guard, univ_vars1, - univ_opening, uu____26539)) - | uu____26544 -> - let uu____26545 = + univ_opening, uu____26577)) + | uu____26582 -> + let uu____26583 = FStar_Syntax_Subst.univ_var_opening lb.FStar_Syntax_Syntax.lbunivs in - (match uu____26545 with + (match uu____26583 with | (univ_opening,univ_vars1) -> let t1 = FStar_Syntax_Subst.subst univ_opening t in let env1 = @@ -10596,45 +10619,45 @@ and (check_lbtyp : top_level && (Prims.op_Negation env.FStar_TypeChecker_Env.generalize) then - let uu____26595 = + let uu____26633 = FStar_TypeChecker_Env.set_expected_typ env1 t1 in ((FStar_Pervasives_Native.Some t1), FStar_TypeChecker_Env.trivial_guard, univ_vars1, - univ_opening, uu____26595) + univ_opening, uu____26633) else - (let uu____26602 = FStar_Syntax_Util.type_u () in - match uu____26602 with - | (k,uu____26622) -> - let uu____26623 = tc_check_tot_or_gtot_term env1 t1 k + (let uu____26640 = FStar_Syntax_Util.type_u () in + match uu____26640 with + | (k,uu____26660) -> + let uu____26661 = tc_check_tot_or_gtot_term env1 t1 k in - (match uu____26623 with - | (t2,uu____26645,g) -> - ((let uu____26648 = + (match uu____26661 with + | (t2,uu____26683,g) -> + ((let uu____26686 = FStar_TypeChecker_Env.debug env FStar_Options.Medium in - if uu____26648 + if uu____26686 then - let uu____26651 = - let uu____26653 = + let uu____26689 = + let uu____26691 = FStar_Syntax_Util.range_of_lbname lb.FStar_Syntax_Syntax.lbname in - FStar_Range.string_of_range uu____26653 + FStar_Range.string_of_range uu____26691 in - let uu____26654 = + let uu____26692 = FStar_Syntax_Print.term_to_string t2 in FStar_Util.print2 "(%s) Checked type annotation %s\n" - uu____26651 uu____26654 + uu____26689 uu____26692 else ()); (let t3 = norm env1 t2 in - let uu____26660 = + let uu____26698 = FStar_TypeChecker_Env.set_expected_typ env1 t3 in ((FStar_Pervasives_Native.Some t3), g, - univ_vars1, univ_opening, uu____26660)))))) + univ_vars1, univ_opening, uu____26698)))))) and (tc_binder : FStar_TypeChecker_Env.env -> @@ -10645,76 +10668,76 @@ and (tc_binder : FStar_TypeChecker_Env.guard_t * FStar_Syntax_Syntax.universe)) = fun env -> - fun uu____26666 -> - match uu____26666 with + fun uu____26704 -> + match uu____26704 with | (x,imp) -> - let uu____26693 = FStar_Syntax_Util.type_u () in - (match uu____26693 with + let uu____26731 = FStar_Syntax_Util.type_u () in + (match uu____26731 with | (tu,u) -> - ((let uu____26715 = + ((let uu____26753 = FStar_TypeChecker_Env.debug env FStar_Options.Extreme in - if uu____26715 + if uu____26753 then - let uu____26718 = FStar_Syntax_Print.bv_to_string x in - let uu____26720 = + let uu____26756 = FStar_Syntax_Print.bv_to_string x in + let uu____26758 = FStar_Syntax_Print.term_to_string x.FStar_Syntax_Syntax.sort in - let uu____26722 = FStar_Syntax_Print.term_to_string tu in + let uu____26760 = FStar_Syntax_Print.term_to_string tu in FStar_Util.print3 "Checking binder %s:%s at type %s\n" - uu____26718 uu____26720 uu____26722 + uu____26756 uu____26758 uu____26760 else ()); - (let uu____26727 = + (let uu____26765 = tc_check_tot_or_gtot_term env x.FStar_Syntax_Syntax.sort tu in - match uu____26727 with - | (t,uu____26749,g) -> - let uu____26751 = + match uu____26765 with + | (t,uu____26787,g) -> + let uu____26789 = match imp with | FStar_Pervasives_Native.Some (FStar_Syntax_Syntax.Meta tau) -> - let uu____26767 = + let uu____26805 = tc_tactic FStar_Syntax_Syntax.t_unit FStar_Syntax_Syntax.t_unit env tau in - (match uu____26767 with - | (tau1,uu____26781,g1) -> + (match uu____26805 with + | (tau1,uu____26819,g1) -> ((FStar_Pervasives_Native.Some (FStar_Syntax_Syntax.Meta tau1)), g1)) - | uu____26785 -> + | uu____26823 -> (imp, FStar_TypeChecker_Env.trivial_guard) in - (match uu____26751 with + (match uu____26789 with | (imp1,g') -> let x1 = - ((let uu___3465_26820 = x in + ((let uu___3469_26858 = x in { FStar_Syntax_Syntax.ppname = - (uu___3465_26820.FStar_Syntax_Syntax.ppname); + (uu___3469_26858.FStar_Syntax_Syntax.ppname); FStar_Syntax_Syntax.index = - (uu___3465_26820.FStar_Syntax_Syntax.index); + (uu___3469_26858.FStar_Syntax_Syntax.index); FStar_Syntax_Syntax.sort = t }), imp1) in - ((let uu____26822 = + ((let uu____26860 = FStar_TypeChecker_Env.debug env FStar_Options.High in - if uu____26822 + if uu____26860 then - let uu____26825 = + let uu____26863 = FStar_Syntax_Print.bv_to_string (FStar_Pervasives_Native.fst x1) in - let uu____26829 = + let uu____26867 = FStar_Syntax_Print.term_to_string t in FStar_Util.print2 - "Pushing binder %s at type %s\n" uu____26825 - uu____26829 + "Pushing binder %s at type %s\n" uu____26863 + uu____26867 else ()); - (let uu____26834 = push_binding env x1 in - (x1, uu____26834, g, u))))))) + (let uu____26872 = push_binding env x1 in + (x1, uu____26872, g, u))))))) and (tc_binders : FStar_TypeChecker_Env.env -> @@ -10724,30 +10747,30 @@ and (tc_binders : = fun env -> fun bs -> - (let uu____26846 = + (let uu____26884 = FStar_TypeChecker_Env.debug env FStar_Options.Extreme in - if uu____26846 + if uu____26884 then - let uu____26849 = FStar_Syntax_Print.binders_to_string ", " bs in - FStar_Util.print1 "Checking binders %s\n" uu____26849 + let uu____26887 = FStar_Syntax_Print.binders_to_string ", " bs in + FStar_Util.print1 "Checking binders %s\n" uu____26887 else ()); (let rec aux env1 bs1 = match bs1 with | [] -> ([], env1, FStar_TypeChecker_Env.trivial_guard, []) | b::bs2 -> - let uu____26962 = tc_binder env1 b in - (match uu____26962 with + let uu____27000 = tc_binder env1 b in + (match uu____27000 with | (b1,env',g,u) -> - let uu____27011 = aux env' bs2 in - (match uu____27011 with + let uu____27049 = aux env' bs2 in + (match uu____27049 with | (bs3,env'1,g',us) -> - let uu____27072 = - let uu____27073 = + let uu____27110 = + let uu____27111 = FStar_TypeChecker_Env.close_guard_univs [u] [b1] g' in - FStar_TypeChecker_Env.conj_guard g uu____27073 in - ((b1 :: bs3), env'1, uu____27072, (u :: us)))) + FStar_TypeChecker_Env.conj_guard g uu____27111 in + ((b1 :: bs3), env'1, uu____27110, (u :: us)))) in aux env bs) @@ -10764,30 +10787,30 @@ and (tc_smt_pats : fun pats -> let tc_args en1 args = FStar_List.fold_right - (fun uu____27181 -> - fun uu____27182 -> - match (uu____27181, uu____27182) with + (fun uu____27219 -> + fun uu____27220 -> + match (uu____27219, uu____27220) with | ((t,imp),(args1,g)) -> (FStar_All.pipe_right t (check_no_smt_theory_symbols en1); - (let uu____27274 = tc_term en1 t in - match uu____27274 with - | (t1,uu____27294,g') -> - let uu____27296 = + (let uu____27312 = tc_term en1 t in + match uu____27312 with + | (t1,uu____27332,g') -> + let uu____27334 = FStar_TypeChecker_Env.conj_guard g g' in - (((t1, imp) :: args1), uu____27296)))) args + (((t1, imp) :: args1), uu____27334)))) args ([], FStar_TypeChecker_Env.trivial_guard) in FStar_List.fold_right (fun p -> - fun uu____27350 -> - match uu____27350 with + fun uu____27388 -> + match uu____27388 with | (pats1,g) -> - let uu____27377 = tc_args en p in - (match uu____27377 with + let uu____27415 = tc_args en p in + (match uu____27415 with | (args,g') -> - let uu____27390 = FStar_TypeChecker_Env.conj_guard g g' + let uu____27428 = FStar_TypeChecker_Env.conj_guard g g' in - ((args :: pats1), uu____27390))) pats + ((args :: pats1), uu____27428))) pats ([], FStar_TypeChecker_Env.trivial_guard) and (tc_tot_or_gtot_term : @@ -10798,70 +10821,70 @@ and (tc_tot_or_gtot_term : = fun env -> fun e -> - let uu____27403 = tc_maybe_toplevel_term env e in - match uu____27403 with + let uu____27441 = tc_maybe_toplevel_term env e in + match uu____27441 with | (e1,c,g) -> - let uu____27419 = FStar_TypeChecker_Common.is_tot_or_gtot_lcomp c + let uu____27457 = FStar_TypeChecker_Common.is_tot_or_gtot_lcomp c in - if uu____27419 + if uu____27457 then (e1, c, g) else (let g1 = FStar_TypeChecker_Rel.solve_deferred_constraints env g in - let uu____27431 = FStar_TypeChecker_Common.lcomp_comp c in - match uu____27431 with + let uu____27469 = FStar_TypeChecker_Common.lcomp_comp c in + match uu____27469 with | (c1,g_c) -> let c2 = norm_c env c1 in - let uu____27445 = - let uu____27451 = + let uu____27483 = + let uu____27489 = FStar_TypeChecker_Util.is_pure_effect env (FStar_Syntax_Util.comp_effect_name c2) in - if uu____27451 + if uu____27489 then - let uu____27459 = + let uu____27497 = FStar_Syntax_Syntax.mk_Total (FStar_Syntax_Util.comp_result c2) in - (uu____27459, false) + (uu____27497, false) else - (let uu____27464 = + (let uu____27502 = FStar_Syntax_Syntax.mk_GTotal (FStar_Syntax_Util.comp_result c2) in - (uu____27464, true)) + (uu____27502, true)) in - (match uu____27445 with + (match uu____27483 with | (target_comp,allow_ghost) -> - let uu____27477 = + let uu____27515 = FStar_TypeChecker_Rel.sub_comp env c2 target_comp in - (match uu____27477 with + (match uu____27515 with | FStar_Pervasives_Native.Some g' -> - let uu____27487 = + let uu____27525 = FStar_TypeChecker_Common.lcomp_of_comp target_comp in - let uu____27488 = - let uu____27489 = + let uu____27526 = + let uu____27527 = FStar_TypeChecker_Env.conj_guard g_c g' in - FStar_TypeChecker_Env.conj_guard g1 uu____27489 + FStar_TypeChecker_Env.conj_guard g1 uu____27527 in - (e1, uu____27487, uu____27488) - | uu____27490 -> + (e1, uu____27525, uu____27526) + | uu____27528 -> if allow_ghost then - let uu____27500 = + let uu____27538 = FStar_TypeChecker_Err.expected_ghost_expression e1 c2 in - FStar_Errors.raise_error uu____27500 + FStar_Errors.raise_error uu____27538 e1.FStar_Syntax_Syntax.pos else - (let uu____27514 = + (let uu____27552 = FStar_TypeChecker_Err.expected_pure_expression e1 c2 in - FStar_Errors.raise_error uu____27514 + FStar_Errors.raise_error uu____27552 e1.FStar_Syntax_Syntax.pos)))) and (tc_check_tot_or_gtot_term : @@ -10884,8 +10907,8 @@ and (tc_trivial_guard : = fun env -> fun t -> - let uu____27538 = tc_tot_or_gtot_term env t in - match uu____27538 with + let uu____27576 = tc_tot_or_gtot_term env t in + match uu____27576 with | (t1,c,g) -> (FStar_TypeChecker_Rel.force_trivial_guard env g; (t1, c)) @@ -10897,9 +10920,9 @@ let (tc_check_trivial_guard : fun env -> fun t -> fun k -> - let uu____27569 = tc_check_tot_or_gtot_term env t k in - match uu____27569 with - | (t1,uu____27577,g) -> + let uu____27607 = tc_check_tot_or_gtot_term env t k in + match uu____27607 with + | (t1,uu____27615,g) -> (FStar_TypeChecker_Rel.force_trivial_guard env g; t1) let (type_of_tot_term : @@ -10910,153 +10933,153 @@ let (type_of_tot_term : = fun env -> fun e -> - (let uu____27598 = + (let uu____27636 = FStar_All.pipe_left (FStar_TypeChecker_Env.debug env) (FStar_Options.Other "RelCheck") in - if uu____27598 + if uu____27636 then - let uu____27603 = FStar_Syntax_Print.term_to_string e in - FStar_Util.print1 "Checking term %s\n" uu____27603 + let uu____27641 = FStar_Syntax_Print.term_to_string e in + FStar_Util.print1 "Checking term %s\n" uu____27641 else ()); (let env1 = - let uu___3557_27609 = env in + let uu___3561_27647 = env in { FStar_TypeChecker_Env.solver = - (uu___3557_27609.FStar_TypeChecker_Env.solver); + (uu___3561_27647.FStar_TypeChecker_Env.solver); FStar_TypeChecker_Env.range = - (uu___3557_27609.FStar_TypeChecker_Env.range); + (uu___3561_27647.FStar_TypeChecker_Env.range); FStar_TypeChecker_Env.curmodule = - (uu___3557_27609.FStar_TypeChecker_Env.curmodule); + (uu___3561_27647.FStar_TypeChecker_Env.curmodule); FStar_TypeChecker_Env.gamma = - (uu___3557_27609.FStar_TypeChecker_Env.gamma); + (uu___3561_27647.FStar_TypeChecker_Env.gamma); FStar_TypeChecker_Env.gamma_sig = - (uu___3557_27609.FStar_TypeChecker_Env.gamma_sig); + (uu___3561_27647.FStar_TypeChecker_Env.gamma_sig); FStar_TypeChecker_Env.gamma_cache = - (uu___3557_27609.FStar_TypeChecker_Env.gamma_cache); + (uu___3561_27647.FStar_TypeChecker_Env.gamma_cache); FStar_TypeChecker_Env.modules = - (uu___3557_27609.FStar_TypeChecker_Env.modules); + (uu___3561_27647.FStar_TypeChecker_Env.modules); FStar_TypeChecker_Env.expected_typ = - (uu___3557_27609.FStar_TypeChecker_Env.expected_typ); + (uu___3561_27647.FStar_TypeChecker_Env.expected_typ); FStar_TypeChecker_Env.sigtab = - (uu___3557_27609.FStar_TypeChecker_Env.sigtab); + (uu___3561_27647.FStar_TypeChecker_Env.sigtab); FStar_TypeChecker_Env.attrtab = - (uu___3557_27609.FStar_TypeChecker_Env.attrtab); + (uu___3561_27647.FStar_TypeChecker_Env.attrtab); FStar_TypeChecker_Env.instantiate_imp = - (uu___3557_27609.FStar_TypeChecker_Env.instantiate_imp); + (uu___3561_27647.FStar_TypeChecker_Env.instantiate_imp); FStar_TypeChecker_Env.effects = - (uu___3557_27609.FStar_TypeChecker_Env.effects); + (uu___3561_27647.FStar_TypeChecker_Env.effects); FStar_TypeChecker_Env.generalize = - (uu___3557_27609.FStar_TypeChecker_Env.generalize); + (uu___3561_27647.FStar_TypeChecker_Env.generalize); FStar_TypeChecker_Env.letrecs = []; FStar_TypeChecker_Env.top_level = false; FStar_TypeChecker_Env.check_uvars = - (uu___3557_27609.FStar_TypeChecker_Env.check_uvars); + (uu___3561_27647.FStar_TypeChecker_Env.check_uvars); FStar_TypeChecker_Env.use_eq = - (uu___3557_27609.FStar_TypeChecker_Env.use_eq); + (uu___3561_27647.FStar_TypeChecker_Env.use_eq); FStar_TypeChecker_Env.is_iface = - (uu___3557_27609.FStar_TypeChecker_Env.is_iface); + (uu___3561_27647.FStar_TypeChecker_Env.is_iface); FStar_TypeChecker_Env.admit = - (uu___3557_27609.FStar_TypeChecker_Env.admit); + (uu___3561_27647.FStar_TypeChecker_Env.admit); FStar_TypeChecker_Env.lax = - (uu___3557_27609.FStar_TypeChecker_Env.lax); + (uu___3561_27647.FStar_TypeChecker_Env.lax); FStar_TypeChecker_Env.lax_universes = - (uu___3557_27609.FStar_TypeChecker_Env.lax_universes); + (uu___3561_27647.FStar_TypeChecker_Env.lax_universes); FStar_TypeChecker_Env.phase1 = - (uu___3557_27609.FStar_TypeChecker_Env.phase1); + (uu___3561_27647.FStar_TypeChecker_Env.phase1); FStar_TypeChecker_Env.failhard = - (uu___3557_27609.FStar_TypeChecker_Env.failhard); + (uu___3561_27647.FStar_TypeChecker_Env.failhard); FStar_TypeChecker_Env.nosynth = - (uu___3557_27609.FStar_TypeChecker_Env.nosynth); + (uu___3561_27647.FStar_TypeChecker_Env.nosynth); FStar_TypeChecker_Env.uvar_subtyping = - (uu___3557_27609.FStar_TypeChecker_Env.uvar_subtyping); + (uu___3561_27647.FStar_TypeChecker_Env.uvar_subtyping); FStar_TypeChecker_Env.tc_term = - (uu___3557_27609.FStar_TypeChecker_Env.tc_term); + (uu___3561_27647.FStar_TypeChecker_Env.tc_term); FStar_TypeChecker_Env.type_of = - (uu___3557_27609.FStar_TypeChecker_Env.type_of); + (uu___3561_27647.FStar_TypeChecker_Env.type_of); FStar_TypeChecker_Env.universe_of = - (uu___3557_27609.FStar_TypeChecker_Env.universe_of); + (uu___3561_27647.FStar_TypeChecker_Env.universe_of); FStar_TypeChecker_Env.check_type_of = - (uu___3557_27609.FStar_TypeChecker_Env.check_type_of); + (uu___3561_27647.FStar_TypeChecker_Env.check_type_of); FStar_TypeChecker_Env.use_bv_sorts = - (uu___3557_27609.FStar_TypeChecker_Env.use_bv_sorts); + (uu___3561_27647.FStar_TypeChecker_Env.use_bv_sorts); FStar_TypeChecker_Env.qtbl_name_and_index = - (uu___3557_27609.FStar_TypeChecker_Env.qtbl_name_and_index); + (uu___3561_27647.FStar_TypeChecker_Env.qtbl_name_and_index); FStar_TypeChecker_Env.normalized_eff_names = - (uu___3557_27609.FStar_TypeChecker_Env.normalized_eff_names); + (uu___3561_27647.FStar_TypeChecker_Env.normalized_eff_names); FStar_TypeChecker_Env.fv_delta_depths = - (uu___3557_27609.FStar_TypeChecker_Env.fv_delta_depths); + (uu___3561_27647.FStar_TypeChecker_Env.fv_delta_depths); FStar_TypeChecker_Env.proof_ns = - (uu___3557_27609.FStar_TypeChecker_Env.proof_ns); + (uu___3561_27647.FStar_TypeChecker_Env.proof_ns); FStar_TypeChecker_Env.synth_hook = - (uu___3557_27609.FStar_TypeChecker_Env.synth_hook); + (uu___3561_27647.FStar_TypeChecker_Env.synth_hook); FStar_TypeChecker_Env.splice = - (uu___3557_27609.FStar_TypeChecker_Env.splice); + (uu___3561_27647.FStar_TypeChecker_Env.splice); FStar_TypeChecker_Env.mpreprocess = - (uu___3557_27609.FStar_TypeChecker_Env.mpreprocess); + (uu___3561_27647.FStar_TypeChecker_Env.mpreprocess); FStar_TypeChecker_Env.postprocess = - (uu___3557_27609.FStar_TypeChecker_Env.postprocess); + (uu___3561_27647.FStar_TypeChecker_Env.postprocess); FStar_TypeChecker_Env.is_native_tactic = - (uu___3557_27609.FStar_TypeChecker_Env.is_native_tactic); + (uu___3561_27647.FStar_TypeChecker_Env.is_native_tactic); FStar_TypeChecker_Env.identifier_info = - (uu___3557_27609.FStar_TypeChecker_Env.identifier_info); + (uu___3561_27647.FStar_TypeChecker_Env.identifier_info); FStar_TypeChecker_Env.tc_hooks = - (uu___3557_27609.FStar_TypeChecker_Env.tc_hooks); + (uu___3561_27647.FStar_TypeChecker_Env.tc_hooks); FStar_TypeChecker_Env.dsenv = - (uu___3557_27609.FStar_TypeChecker_Env.dsenv); + (uu___3561_27647.FStar_TypeChecker_Env.dsenv); FStar_TypeChecker_Env.nbe = - (uu___3557_27609.FStar_TypeChecker_Env.nbe); + (uu___3561_27647.FStar_TypeChecker_Env.nbe); FStar_TypeChecker_Env.strict_args_tab = - (uu___3557_27609.FStar_TypeChecker_Env.strict_args_tab); + (uu___3561_27647.FStar_TypeChecker_Env.strict_args_tab); FStar_TypeChecker_Env.erasable_types_tab = - (uu___3557_27609.FStar_TypeChecker_Env.erasable_types_tab) + (uu___3561_27647.FStar_TypeChecker_Env.erasable_types_tab) } in - let uu____27617 = + let uu____27655 = try - (fun uu___3561_27631 -> + (fun uu___3565_27669 -> match () with | () -> tc_tot_or_gtot_term env1 e) () with - | FStar_Errors.Error (e1,msg,uu____27652) -> - let uu____27655 = FStar_TypeChecker_Env.get_range env1 in - FStar_Errors.raise_error (e1, msg) uu____27655 + | FStar_Errors.Error (e1,msg,uu____27690) -> + let uu____27693 = FStar_TypeChecker_Env.get_range env1 in + FStar_Errors.raise_error (e1, msg) uu____27693 in - match uu____27617 with + match uu____27655 with | (t,c,g) -> let c1 = FStar_TypeChecker_Normalize.ghost_to_pure_lcomp env1 c in - let uu____27673 = FStar_TypeChecker_Common.is_total_lcomp c1 in - if uu____27673 + let uu____27711 = FStar_TypeChecker_Common.is_total_lcomp c1 in + if uu____27711 then (t, (c1.FStar_TypeChecker_Common.res_typ), g) else - (let uu____27684 = - let uu____27690 = - let uu____27692 = FStar_Syntax_Print.term_to_string e in + (let uu____27722 = + let uu____27728 = + let uu____27730 = FStar_Syntax_Print.term_to_string e in FStar_Util.format1 "Implicit argument: Expected a total term; got a ghost term: %s" - uu____27692 + uu____27730 in - (FStar_Errors.Fatal_UnexpectedImplictArgument, uu____27690) + (FStar_Errors.Fatal_UnexpectedImplictArgument, uu____27728) in - let uu____27696 = FStar_TypeChecker_Env.get_range env1 in - FStar_Errors.raise_error uu____27684 uu____27696)) + let uu____27734 = FStar_TypeChecker_Env.get_range env1 in + FStar_Errors.raise_error uu____27722 uu____27734)) let level_of_type_fail : - 'Auu____27712 . + 'Auu____27750 . FStar_TypeChecker_Env.env -> - FStar_Syntax_Syntax.term -> Prims.string -> 'Auu____27712 + FStar_Syntax_Syntax.term -> Prims.string -> 'Auu____27750 = fun env -> fun e -> fun t -> - let uu____27730 = - let uu____27736 = - let uu____27738 = FStar_Syntax_Print.term_to_string e in + let uu____27768 = + let uu____27774 = + let uu____27776 = FStar_Syntax_Print.term_to_string e in FStar_Util.format2 "Expected a term of type 'Type'; got %s : %s" - uu____27738 t + uu____27776 t in - (FStar_Errors.Fatal_UnexpectedTermType, uu____27736) in - let uu____27742 = FStar_TypeChecker_Env.get_range env in - FStar_Errors.raise_error uu____27730 uu____27742 + (FStar_Errors.Fatal_UnexpectedTermType, uu____27774) in + let uu____27780 = FStar_TypeChecker_Env.get_range env in + FStar_Errors.raise_error uu____27768 uu____27780 let (level_of_type : FStar_TypeChecker_Env.env -> @@ -11067,12 +11090,12 @@ let (level_of_type : fun e -> fun t -> let rec aux retry t1 = - let uu____27776 = - let uu____27777 = FStar_Syntax_Util.unrefine t1 in - uu____27777.FStar_Syntax_Syntax.n in - match uu____27776 with + let uu____27814 = + let uu____27815 = FStar_Syntax_Util.unrefine t1 in + uu____27815.FStar_Syntax_Syntax.n in + match uu____27814 with | FStar_Syntax_Syntax.Tm_type u -> u - | uu____27781 -> + | uu____27819 -> if retry then let t2 = @@ -11082,109 +11105,109 @@ let (level_of_type : in aux false t2 else - (let uu____27787 = FStar_Syntax_Util.type_u () in - match uu____27787 with + (let uu____27825 = FStar_Syntax_Util.type_u () in + match uu____27825 with | (t_u,u) -> let env1 = - let uu___3593_27795 = env in + let uu___3597_27833 = env in { FStar_TypeChecker_Env.solver = - (uu___3593_27795.FStar_TypeChecker_Env.solver); + (uu___3597_27833.FStar_TypeChecker_Env.solver); FStar_TypeChecker_Env.range = - (uu___3593_27795.FStar_TypeChecker_Env.range); + (uu___3597_27833.FStar_TypeChecker_Env.range); FStar_TypeChecker_Env.curmodule = - (uu___3593_27795.FStar_TypeChecker_Env.curmodule); + (uu___3597_27833.FStar_TypeChecker_Env.curmodule); FStar_TypeChecker_Env.gamma = - (uu___3593_27795.FStar_TypeChecker_Env.gamma); + (uu___3597_27833.FStar_TypeChecker_Env.gamma); FStar_TypeChecker_Env.gamma_sig = - (uu___3593_27795.FStar_TypeChecker_Env.gamma_sig); + (uu___3597_27833.FStar_TypeChecker_Env.gamma_sig); FStar_TypeChecker_Env.gamma_cache = - (uu___3593_27795.FStar_TypeChecker_Env.gamma_cache); + (uu___3597_27833.FStar_TypeChecker_Env.gamma_cache); FStar_TypeChecker_Env.modules = - (uu___3593_27795.FStar_TypeChecker_Env.modules); + (uu___3597_27833.FStar_TypeChecker_Env.modules); FStar_TypeChecker_Env.expected_typ = - (uu___3593_27795.FStar_TypeChecker_Env.expected_typ); + (uu___3597_27833.FStar_TypeChecker_Env.expected_typ); FStar_TypeChecker_Env.sigtab = - (uu___3593_27795.FStar_TypeChecker_Env.sigtab); + (uu___3597_27833.FStar_TypeChecker_Env.sigtab); FStar_TypeChecker_Env.attrtab = - (uu___3593_27795.FStar_TypeChecker_Env.attrtab); + (uu___3597_27833.FStar_TypeChecker_Env.attrtab); FStar_TypeChecker_Env.instantiate_imp = - (uu___3593_27795.FStar_TypeChecker_Env.instantiate_imp); + (uu___3597_27833.FStar_TypeChecker_Env.instantiate_imp); FStar_TypeChecker_Env.effects = - (uu___3593_27795.FStar_TypeChecker_Env.effects); + (uu___3597_27833.FStar_TypeChecker_Env.effects); FStar_TypeChecker_Env.generalize = - (uu___3593_27795.FStar_TypeChecker_Env.generalize); + (uu___3597_27833.FStar_TypeChecker_Env.generalize); FStar_TypeChecker_Env.letrecs = - (uu___3593_27795.FStar_TypeChecker_Env.letrecs); + (uu___3597_27833.FStar_TypeChecker_Env.letrecs); FStar_TypeChecker_Env.top_level = - (uu___3593_27795.FStar_TypeChecker_Env.top_level); + (uu___3597_27833.FStar_TypeChecker_Env.top_level); FStar_TypeChecker_Env.check_uvars = - (uu___3593_27795.FStar_TypeChecker_Env.check_uvars); + (uu___3597_27833.FStar_TypeChecker_Env.check_uvars); FStar_TypeChecker_Env.use_eq = - (uu___3593_27795.FStar_TypeChecker_Env.use_eq); + (uu___3597_27833.FStar_TypeChecker_Env.use_eq); FStar_TypeChecker_Env.is_iface = - (uu___3593_27795.FStar_TypeChecker_Env.is_iface); + (uu___3597_27833.FStar_TypeChecker_Env.is_iface); FStar_TypeChecker_Env.admit = - (uu___3593_27795.FStar_TypeChecker_Env.admit); + (uu___3597_27833.FStar_TypeChecker_Env.admit); FStar_TypeChecker_Env.lax = true; FStar_TypeChecker_Env.lax_universes = - (uu___3593_27795.FStar_TypeChecker_Env.lax_universes); + (uu___3597_27833.FStar_TypeChecker_Env.lax_universes); FStar_TypeChecker_Env.phase1 = - (uu___3593_27795.FStar_TypeChecker_Env.phase1); + (uu___3597_27833.FStar_TypeChecker_Env.phase1); FStar_TypeChecker_Env.failhard = - (uu___3593_27795.FStar_TypeChecker_Env.failhard); + (uu___3597_27833.FStar_TypeChecker_Env.failhard); FStar_TypeChecker_Env.nosynth = - (uu___3593_27795.FStar_TypeChecker_Env.nosynth); + (uu___3597_27833.FStar_TypeChecker_Env.nosynth); FStar_TypeChecker_Env.uvar_subtyping = - (uu___3593_27795.FStar_TypeChecker_Env.uvar_subtyping); + (uu___3597_27833.FStar_TypeChecker_Env.uvar_subtyping); FStar_TypeChecker_Env.tc_term = - (uu___3593_27795.FStar_TypeChecker_Env.tc_term); + (uu___3597_27833.FStar_TypeChecker_Env.tc_term); FStar_TypeChecker_Env.type_of = - (uu___3593_27795.FStar_TypeChecker_Env.type_of); + (uu___3597_27833.FStar_TypeChecker_Env.type_of); FStar_TypeChecker_Env.universe_of = - (uu___3593_27795.FStar_TypeChecker_Env.universe_of); + (uu___3597_27833.FStar_TypeChecker_Env.universe_of); FStar_TypeChecker_Env.check_type_of = - (uu___3593_27795.FStar_TypeChecker_Env.check_type_of); + (uu___3597_27833.FStar_TypeChecker_Env.check_type_of); FStar_TypeChecker_Env.use_bv_sorts = - (uu___3593_27795.FStar_TypeChecker_Env.use_bv_sorts); + (uu___3597_27833.FStar_TypeChecker_Env.use_bv_sorts); FStar_TypeChecker_Env.qtbl_name_and_index = - (uu___3593_27795.FStar_TypeChecker_Env.qtbl_name_and_index); + (uu___3597_27833.FStar_TypeChecker_Env.qtbl_name_and_index); FStar_TypeChecker_Env.normalized_eff_names = - (uu___3593_27795.FStar_TypeChecker_Env.normalized_eff_names); + (uu___3597_27833.FStar_TypeChecker_Env.normalized_eff_names); FStar_TypeChecker_Env.fv_delta_depths = - (uu___3593_27795.FStar_TypeChecker_Env.fv_delta_depths); + (uu___3597_27833.FStar_TypeChecker_Env.fv_delta_depths); FStar_TypeChecker_Env.proof_ns = - (uu___3593_27795.FStar_TypeChecker_Env.proof_ns); + (uu___3597_27833.FStar_TypeChecker_Env.proof_ns); FStar_TypeChecker_Env.synth_hook = - (uu___3593_27795.FStar_TypeChecker_Env.synth_hook); + (uu___3597_27833.FStar_TypeChecker_Env.synth_hook); FStar_TypeChecker_Env.splice = - (uu___3593_27795.FStar_TypeChecker_Env.splice); + (uu___3597_27833.FStar_TypeChecker_Env.splice); FStar_TypeChecker_Env.mpreprocess = - (uu___3593_27795.FStar_TypeChecker_Env.mpreprocess); + (uu___3597_27833.FStar_TypeChecker_Env.mpreprocess); FStar_TypeChecker_Env.postprocess = - (uu___3593_27795.FStar_TypeChecker_Env.postprocess); + (uu___3597_27833.FStar_TypeChecker_Env.postprocess); FStar_TypeChecker_Env.is_native_tactic = - (uu___3593_27795.FStar_TypeChecker_Env.is_native_tactic); + (uu___3597_27833.FStar_TypeChecker_Env.is_native_tactic); FStar_TypeChecker_Env.identifier_info = - (uu___3593_27795.FStar_TypeChecker_Env.identifier_info); + (uu___3597_27833.FStar_TypeChecker_Env.identifier_info); FStar_TypeChecker_Env.tc_hooks = - (uu___3593_27795.FStar_TypeChecker_Env.tc_hooks); + (uu___3597_27833.FStar_TypeChecker_Env.tc_hooks); FStar_TypeChecker_Env.dsenv = - (uu___3593_27795.FStar_TypeChecker_Env.dsenv); + (uu___3597_27833.FStar_TypeChecker_Env.dsenv); FStar_TypeChecker_Env.nbe = - (uu___3593_27795.FStar_TypeChecker_Env.nbe); + (uu___3597_27833.FStar_TypeChecker_Env.nbe); FStar_TypeChecker_Env.strict_args_tab = - (uu___3593_27795.FStar_TypeChecker_Env.strict_args_tab); + (uu___3597_27833.FStar_TypeChecker_Env.strict_args_tab); FStar_TypeChecker_Env.erasable_types_tab = - (uu___3593_27795.FStar_TypeChecker_Env.erasable_types_tab) + (uu___3597_27833.FStar_TypeChecker_Env.erasable_types_tab) } in let g = FStar_TypeChecker_Rel.teq env1 t1 t_u in ((match g.FStar_TypeChecker_Common.guard_f with | FStar_TypeChecker_Common.NonTrivial f -> - let uu____27800 = + let uu____27838 = FStar_Syntax_Print.term_to_string t1 in - level_of_type_fail env1 e uu____27800 - | uu____27802 -> + level_of_type_fail env1 e uu____27838 + | uu____27840 -> FStar_TypeChecker_Rel.force_trivial_guard env1 g); u)) in @@ -11197,61 +11220,61 @@ let rec (universe_of_aux : = fun env -> fun e -> - let uu____27819 = - let uu____27820 = FStar_Syntax_Subst.compress e in - uu____27820.FStar_Syntax_Syntax.n in - match uu____27819 with - | FStar_Syntax_Syntax.Tm_bvar uu____27823 -> failwith "Impossible" + let uu____27857 = + let uu____27858 = FStar_Syntax_Subst.compress e in + uu____27858.FStar_Syntax_Syntax.n in + match uu____27857 with + | FStar_Syntax_Syntax.Tm_bvar uu____27861 -> failwith "Impossible" | FStar_Syntax_Syntax.Tm_unknown -> failwith "Impossible" - | FStar_Syntax_Syntax.Tm_delayed uu____27826 -> failwith "Impossible" - | FStar_Syntax_Syntax.Tm_let uu____27850 -> + | FStar_Syntax_Syntax.Tm_delayed uu____27864 -> failwith "Impossible" + | FStar_Syntax_Syntax.Tm_let uu____27888 -> let e1 = FStar_TypeChecker_Normalize.normalize [] env e in universe_of_aux env e1 - | FStar_Syntax_Syntax.Tm_abs (bs,t,uu____27867) -> + | FStar_Syntax_Syntax.Tm_abs (bs,t,uu____27905) -> level_of_type_fail env e "arrow type" | FStar_Syntax_Syntax.Tm_uvar (u,s) -> FStar_Syntax_Subst.subst' s u.FStar_Syntax_Syntax.ctx_uvar_typ - | FStar_Syntax_Syntax.Tm_meta (t,uu____27912) -> universe_of_aux env t + | FStar_Syntax_Syntax.Tm_meta (t,uu____27950) -> universe_of_aux env t | FStar_Syntax_Syntax.Tm_name n1 -> n1.FStar_Syntax_Syntax.sort | FStar_Syntax_Syntax.Tm_fvar fv -> - let uu____27919 = + let uu____27957 = FStar_TypeChecker_Env.lookup_lid env (fv.FStar_Syntax_Syntax.fv_name).FStar_Syntax_Syntax.v in - (match uu____27919 with | ((uu____27928,t),uu____27930) -> t) + (match uu____27957 with | ((uu____27966,t),uu____27968) -> t) | FStar_Syntax_Syntax.Tm_lazy i -> - let uu____27936 = FStar_Syntax_Util.unfold_lazy i in - universe_of_aux env uu____27936 + let uu____27974 = FStar_Syntax_Util.unfold_lazy i in + universe_of_aux env uu____27974 | FStar_Syntax_Syntax.Tm_ascribed - (uu____27939,(FStar_Util.Inl t,uu____27941),uu____27942) -> t + (uu____27977,(FStar_Util.Inl t,uu____27979),uu____27980) -> t | FStar_Syntax_Syntax.Tm_ascribed - (uu____27989,(FStar_Util.Inr c,uu____27991),uu____27992) -> + (uu____28027,(FStar_Util.Inr c,uu____28029),uu____28030) -> FStar_Syntax_Util.comp_result c | FStar_Syntax_Syntax.Tm_type u -> FStar_Syntax_Syntax.mk (FStar_Syntax_Syntax.Tm_type (FStar_Syntax_Syntax.U_succ u)) FStar_Pervasives_Native.None e.FStar_Syntax_Syntax.pos - | FStar_Syntax_Syntax.Tm_quoted uu____28040 -> FStar_Syntax_Util.ktype0 + | FStar_Syntax_Syntax.Tm_quoted uu____28078 -> FStar_Syntax_Util.ktype0 | FStar_Syntax_Syntax.Tm_constant sc -> tc_constant env e.FStar_Syntax_Syntax.pos sc | FStar_Syntax_Syntax.Tm_uinst ({ FStar_Syntax_Syntax.n = FStar_Syntax_Syntax.Tm_fvar fv; - FStar_Syntax_Syntax.pos = uu____28049; - FStar_Syntax_Syntax.vars = uu____28050;_},us) + FStar_Syntax_Syntax.pos = uu____28087; + FStar_Syntax_Syntax.vars = uu____28088;_},us) -> - let uu____28056 = + let uu____28094 = FStar_TypeChecker_Env.lookup_lid env (fv.FStar_Syntax_Syntax.fv_name).FStar_Syntax_Syntax.v in - (match uu____28056 with - | ((us',t),uu____28067) -> + (match uu____28094 with + | ((us',t),uu____28105) -> (if (FStar_List.length us) <> (FStar_List.length us') then - (let uu____28074 = FStar_TypeChecker_Env.get_range env in + (let uu____28112 = FStar_TypeChecker_Env.get_range env in FStar_Errors.raise_error (FStar_Errors.Fatal_UnexpectedNumberOfUniverse, "Unexpected number of universe instantiations") - uu____28074) + uu____28112) else FStar_List.iter2 (fun u' -> @@ -11259,31 +11282,31 @@ let rec (universe_of_aux : match u' with | FStar_Syntax_Syntax.U_unif u'' -> FStar_Syntax_Unionfind.univ_change u'' u - | uu____28093 -> failwith "Impossible") us' us; + | uu____28131 -> failwith "Impossible") us' us; t)) - | FStar_Syntax_Syntax.Tm_uinst uu____28095 -> + | FStar_Syntax_Syntax.Tm_uinst uu____28133 -> failwith "Impossible: Tm_uinst's head must be an fvar" - | FStar_Syntax_Syntax.Tm_refine (x,uu____28104) -> + | FStar_Syntax_Syntax.Tm_refine (x,uu____28142) -> universe_of_aux env x.FStar_Syntax_Syntax.sort | FStar_Syntax_Syntax.Tm_arrow (bs,c) -> - let uu____28131 = FStar_Syntax_Subst.open_comp bs c in - (match uu____28131 with + let uu____28169 = FStar_Syntax_Subst.open_comp bs c in + (match uu____28169 with | (bs1,c1) -> let us = FStar_List.map - (fun uu____28151 -> - match uu____28151 with - | (b,uu____28159) -> - let uu____28164 = + (fun uu____28189 -> + match uu____28189 with + | (b,uu____28197) -> + let uu____28202 = universe_of_aux env b.FStar_Syntax_Syntax.sort in level_of_type env b.FStar_Syntax_Syntax.sort - uu____28164) bs1 + uu____28202) bs1 in let u_res = let res = FStar_Syntax_Util.comp_result c1 in - let uu____28169 = universe_of_aux env res in - level_of_type env res uu____28169 in + let uu____28207 = universe_of_aux env res in + level_of_type env res uu____28207 in let u_c = FStar_All.pipe_right c1 (FStar_TypeChecker_Util.universe_of_comp env u_res) @@ -11299,197 +11322,197 @@ let rec (universe_of_aux : let hd3 = FStar_Syntax_Subst.compress hd2 in match hd3.FStar_Syntax_Syntax.n with | FStar_Syntax_Syntax.Tm_unknown -> failwith "Impossible" - | FStar_Syntax_Syntax.Tm_bvar uu____28280 -> + | FStar_Syntax_Syntax.Tm_bvar uu____28318 -> failwith "Impossible" - | FStar_Syntax_Syntax.Tm_delayed uu____28296 -> + | FStar_Syntax_Syntax.Tm_delayed uu____28334 -> failwith "Impossible" - | FStar_Syntax_Syntax.Tm_fvar uu____28334 -> - let uu____28335 = universe_of_aux env hd3 in - (uu____28335, args1) - | FStar_Syntax_Syntax.Tm_name uu____28346 -> - let uu____28347 = universe_of_aux env hd3 in - (uu____28347, args1) - | FStar_Syntax_Syntax.Tm_uvar uu____28358 -> - let uu____28371 = universe_of_aux env hd3 in - (uu____28371, args1) - | FStar_Syntax_Syntax.Tm_uinst uu____28382 -> - let uu____28389 = universe_of_aux env hd3 in - (uu____28389, args1) - | FStar_Syntax_Syntax.Tm_ascribed uu____28400 -> + | FStar_Syntax_Syntax.Tm_fvar uu____28372 -> + let uu____28373 = universe_of_aux env hd3 in + (uu____28373, args1) + | FStar_Syntax_Syntax.Tm_name uu____28384 -> + let uu____28385 = universe_of_aux env hd3 in + (uu____28385, args1) + | FStar_Syntax_Syntax.Tm_uvar uu____28396 -> + let uu____28409 = universe_of_aux env hd3 in + (uu____28409, args1) + | FStar_Syntax_Syntax.Tm_uinst uu____28420 -> let uu____28427 = universe_of_aux env hd3 in (uu____28427, args1) - | FStar_Syntax_Syntax.Tm_refine uu____28438 -> - let uu____28445 = universe_of_aux env hd3 in - (uu____28445, args1) - | FStar_Syntax_Syntax.Tm_constant uu____28456 -> - let uu____28457 = universe_of_aux env hd3 in - (uu____28457, args1) - | FStar_Syntax_Syntax.Tm_arrow uu____28468 -> + | FStar_Syntax_Syntax.Tm_ascribed uu____28438 -> + let uu____28465 = universe_of_aux env hd3 in + (uu____28465, args1) + | FStar_Syntax_Syntax.Tm_refine uu____28476 -> let uu____28483 = universe_of_aux env hd3 in (uu____28483, args1) - | FStar_Syntax_Syntax.Tm_meta uu____28494 -> - let uu____28501 = universe_of_aux env hd3 in - (uu____28501, args1) - | FStar_Syntax_Syntax.Tm_type uu____28512 -> - let uu____28513 = universe_of_aux env hd3 in - (uu____28513, args1) - | FStar_Syntax_Syntax.Tm_match (uu____28524,hd4::uu____28526) -> - let uu____28591 = FStar_Syntax_Subst.open_branch hd4 in - (match uu____28591 with - | (uu____28606,uu____28607,hd5) -> - let uu____28625 = FStar_Syntax_Util.head_and_args hd5 + | FStar_Syntax_Syntax.Tm_constant uu____28494 -> + let uu____28495 = universe_of_aux env hd3 in + (uu____28495, args1) + | FStar_Syntax_Syntax.Tm_arrow uu____28506 -> + let uu____28521 = universe_of_aux env hd3 in + (uu____28521, args1) + | FStar_Syntax_Syntax.Tm_meta uu____28532 -> + let uu____28539 = universe_of_aux env hd3 in + (uu____28539, args1) + | FStar_Syntax_Syntax.Tm_type uu____28550 -> + let uu____28551 = universe_of_aux env hd3 in + (uu____28551, args1) + | FStar_Syntax_Syntax.Tm_match (uu____28562,hd4::uu____28564) -> + let uu____28629 = FStar_Syntax_Subst.open_branch hd4 in + (match uu____28629 with + | (uu____28644,uu____28645,hd5) -> + let uu____28663 = FStar_Syntax_Util.head_and_args hd5 in - (match uu____28625 with + (match uu____28663 with | (hd6,args2) -> type_of_head retry hd6 args2)) - | uu____28682 when retry -> + | uu____28720 when retry -> let e1 = FStar_TypeChecker_Normalize.normalize [FStar_TypeChecker_Env.Beta; FStar_TypeChecker_Env.DoNotUnfoldPureLets] env e in - let uu____28684 = FStar_Syntax_Util.head_and_args e1 in - (match uu____28684 with + let uu____28722 = FStar_Syntax_Util.head_and_args e1 in + (match uu____28722 with | (hd4,args2) -> type_of_head false hd4 args2) - | uu____28742 -> - let uu____28743 = + | uu____28780 -> + let uu____28781 = FStar_TypeChecker_Env.clear_expected_typ env in - (match uu____28743 with - | (env1,uu____28765) -> + (match uu____28781 with + | (env1,uu____28803) -> let env2 = - let uu___3754_28771 = env1 in + let uu___3758_28809 = env1 in { FStar_TypeChecker_Env.solver = - (uu___3754_28771.FStar_TypeChecker_Env.solver); + (uu___3758_28809.FStar_TypeChecker_Env.solver); FStar_TypeChecker_Env.range = - (uu___3754_28771.FStar_TypeChecker_Env.range); + (uu___3758_28809.FStar_TypeChecker_Env.range); FStar_TypeChecker_Env.curmodule = - (uu___3754_28771.FStar_TypeChecker_Env.curmodule); + (uu___3758_28809.FStar_TypeChecker_Env.curmodule); FStar_TypeChecker_Env.gamma = - (uu___3754_28771.FStar_TypeChecker_Env.gamma); + (uu___3758_28809.FStar_TypeChecker_Env.gamma); FStar_TypeChecker_Env.gamma_sig = - (uu___3754_28771.FStar_TypeChecker_Env.gamma_sig); + (uu___3758_28809.FStar_TypeChecker_Env.gamma_sig); FStar_TypeChecker_Env.gamma_cache = - (uu___3754_28771.FStar_TypeChecker_Env.gamma_cache); + (uu___3758_28809.FStar_TypeChecker_Env.gamma_cache); FStar_TypeChecker_Env.modules = - (uu___3754_28771.FStar_TypeChecker_Env.modules); + (uu___3758_28809.FStar_TypeChecker_Env.modules); FStar_TypeChecker_Env.expected_typ = - (uu___3754_28771.FStar_TypeChecker_Env.expected_typ); + (uu___3758_28809.FStar_TypeChecker_Env.expected_typ); FStar_TypeChecker_Env.sigtab = - (uu___3754_28771.FStar_TypeChecker_Env.sigtab); + (uu___3758_28809.FStar_TypeChecker_Env.sigtab); FStar_TypeChecker_Env.attrtab = - (uu___3754_28771.FStar_TypeChecker_Env.attrtab); + (uu___3758_28809.FStar_TypeChecker_Env.attrtab); FStar_TypeChecker_Env.instantiate_imp = - (uu___3754_28771.FStar_TypeChecker_Env.instantiate_imp); + (uu___3758_28809.FStar_TypeChecker_Env.instantiate_imp); FStar_TypeChecker_Env.effects = - (uu___3754_28771.FStar_TypeChecker_Env.effects); + (uu___3758_28809.FStar_TypeChecker_Env.effects); FStar_TypeChecker_Env.generalize = - (uu___3754_28771.FStar_TypeChecker_Env.generalize); + (uu___3758_28809.FStar_TypeChecker_Env.generalize); FStar_TypeChecker_Env.letrecs = - (uu___3754_28771.FStar_TypeChecker_Env.letrecs); + (uu___3758_28809.FStar_TypeChecker_Env.letrecs); FStar_TypeChecker_Env.top_level = false; FStar_TypeChecker_Env.check_uvars = - (uu___3754_28771.FStar_TypeChecker_Env.check_uvars); + (uu___3758_28809.FStar_TypeChecker_Env.check_uvars); FStar_TypeChecker_Env.use_eq = - (uu___3754_28771.FStar_TypeChecker_Env.use_eq); + (uu___3758_28809.FStar_TypeChecker_Env.use_eq); FStar_TypeChecker_Env.is_iface = - (uu___3754_28771.FStar_TypeChecker_Env.is_iface); + (uu___3758_28809.FStar_TypeChecker_Env.is_iface); FStar_TypeChecker_Env.admit = - (uu___3754_28771.FStar_TypeChecker_Env.admit); + (uu___3758_28809.FStar_TypeChecker_Env.admit); FStar_TypeChecker_Env.lax = true; FStar_TypeChecker_Env.lax_universes = - (uu___3754_28771.FStar_TypeChecker_Env.lax_universes); + (uu___3758_28809.FStar_TypeChecker_Env.lax_universes); FStar_TypeChecker_Env.phase1 = - (uu___3754_28771.FStar_TypeChecker_Env.phase1); + (uu___3758_28809.FStar_TypeChecker_Env.phase1); FStar_TypeChecker_Env.failhard = - (uu___3754_28771.FStar_TypeChecker_Env.failhard); + (uu___3758_28809.FStar_TypeChecker_Env.failhard); FStar_TypeChecker_Env.nosynth = - (uu___3754_28771.FStar_TypeChecker_Env.nosynth); + (uu___3758_28809.FStar_TypeChecker_Env.nosynth); FStar_TypeChecker_Env.uvar_subtyping = - (uu___3754_28771.FStar_TypeChecker_Env.uvar_subtyping); + (uu___3758_28809.FStar_TypeChecker_Env.uvar_subtyping); FStar_TypeChecker_Env.tc_term = - (uu___3754_28771.FStar_TypeChecker_Env.tc_term); + (uu___3758_28809.FStar_TypeChecker_Env.tc_term); FStar_TypeChecker_Env.type_of = - (uu___3754_28771.FStar_TypeChecker_Env.type_of); + (uu___3758_28809.FStar_TypeChecker_Env.type_of); FStar_TypeChecker_Env.universe_of = - (uu___3754_28771.FStar_TypeChecker_Env.universe_of); + (uu___3758_28809.FStar_TypeChecker_Env.universe_of); FStar_TypeChecker_Env.check_type_of = - (uu___3754_28771.FStar_TypeChecker_Env.check_type_of); + (uu___3758_28809.FStar_TypeChecker_Env.check_type_of); FStar_TypeChecker_Env.use_bv_sorts = true; FStar_TypeChecker_Env.qtbl_name_and_index = - (uu___3754_28771.FStar_TypeChecker_Env.qtbl_name_and_index); + (uu___3758_28809.FStar_TypeChecker_Env.qtbl_name_and_index); FStar_TypeChecker_Env.normalized_eff_names = - (uu___3754_28771.FStar_TypeChecker_Env.normalized_eff_names); + (uu___3758_28809.FStar_TypeChecker_Env.normalized_eff_names); FStar_TypeChecker_Env.fv_delta_depths = - (uu___3754_28771.FStar_TypeChecker_Env.fv_delta_depths); + (uu___3758_28809.FStar_TypeChecker_Env.fv_delta_depths); FStar_TypeChecker_Env.proof_ns = - (uu___3754_28771.FStar_TypeChecker_Env.proof_ns); + (uu___3758_28809.FStar_TypeChecker_Env.proof_ns); FStar_TypeChecker_Env.synth_hook = - (uu___3754_28771.FStar_TypeChecker_Env.synth_hook); + (uu___3758_28809.FStar_TypeChecker_Env.synth_hook); FStar_TypeChecker_Env.splice = - (uu___3754_28771.FStar_TypeChecker_Env.splice); + (uu___3758_28809.FStar_TypeChecker_Env.splice); FStar_TypeChecker_Env.mpreprocess = - (uu___3754_28771.FStar_TypeChecker_Env.mpreprocess); + (uu___3758_28809.FStar_TypeChecker_Env.mpreprocess); FStar_TypeChecker_Env.postprocess = - (uu___3754_28771.FStar_TypeChecker_Env.postprocess); + (uu___3758_28809.FStar_TypeChecker_Env.postprocess); FStar_TypeChecker_Env.is_native_tactic = - (uu___3754_28771.FStar_TypeChecker_Env.is_native_tactic); + (uu___3758_28809.FStar_TypeChecker_Env.is_native_tactic); FStar_TypeChecker_Env.identifier_info = - (uu___3754_28771.FStar_TypeChecker_Env.identifier_info); + (uu___3758_28809.FStar_TypeChecker_Env.identifier_info); FStar_TypeChecker_Env.tc_hooks = - (uu___3754_28771.FStar_TypeChecker_Env.tc_hooks); + (uu___3758_28809.FStar_TypeChecker_Env.tc_hooks); FStar_TypeChecker_Env.dsenv = - (uu___3754_28771.FStar_TypeChecker_Env.dsenv); + (uu___3758_28809.FStar_TypeChecker_Env.dsenv); FStar_TypeChecker_Env.nbe = - (uu___3754_28771.FStar_TypeChecker_Env.nbe); + (uu___3758_28809.FStar_TypeChecker_Env.nbe); FStar_TypeChecker_Env.strict_args_tab = - (uu___3754_28771.FStar_TypeChecker_Env.strict_args_tab); + (uu___3758_28809.FStar_TypeChecker_Env.strict_args_tab); FStar_TypeChecker_Env.erasable_types_tab = - (uu___3754_28771.FStar_TypeChecker_Env.erasable_types_tab) + (uu___3758_28809.FStar_TypeChecker_Env.erasable_types_tab) } in - ((let uu____28776 = + ((let uu____28814 = FStar_All.pipe_left (FStar_TypeChecker_Env.debug env2) (FStar_Options.Other "UniverseOf") in - if uu____28776 + if uu____28814 then - let uu____28781 = - let uu____28783 = + let uu____28819 = + let uu____28821 = FStar_TypeChecker_Env.get_range env2 in - FStar_Range.string_of_range uu____28783 in - let uu____28784 = + FStar_Range.string_of_range uu____28821 in + let uu____28822 = FStar_Syntax_Print.term_to_string hd3 in FStar_Util.print2 "%s: About to type-check %s\n" - uu____28781 uu____28784 + uu____28819 uu____28822 else ()); - (let uu____28789 = tc_term env2 hd3 in - match uu____28789 with - | (uu____28810,{ + (let uu____28827 = tc_term env2 hd3 in + match uu____28827 with + | (uu____28848,{ FStar_TypeChecker_Common.eff_name = - uu____28811; + uu____28849; FStar_TypeChecker_Common.res_typ = t; FStar_TypeChecker_Common.cflags = - uu____28813; + uu____28851; FStar_TypeChecker_Common.comp_thunk = - uu____28814;_},g) + uu____28852;_},g) -> - ((let uu____28832 = + ((let uu____28870 = FStar_TypeChecker_Rel.solve_deferred_constraints env2 g in - FStar_All.pipe_right uu____28832 (fun a1 -> ())); + FStar_All.pipe_right uu____28870 (fun a1 -> ())); (t, args1))))) in - let uu____28843 = type_of_head true hd1 args in - (match uu____28843 with + let uu____28881 = type_of_head true hd1 args in + (match uu____28881 with | (t,args1) -> let t1 = FStar_TypeChecker_Normalize.normalize [FStar_TypeChecker_Env.UnfoldUntil FStar_Syntax_Syntax.delta_constant] env t in - let uu____28882 = FStar_Syntax_Util.arrow_formals_comp t1 in - (match uu____28882 with + let uu____28920 = FStar_Syntax_Util.arrow_formals_comp t1 in + (match uu____28920 with | (bs,res) -> let res1 = FStar_Syntax_Util.comp_result res in if (FStar_List.length bs) = (FStar_List.length args1) @@ -11498,14 +11521,14 @@ let rec (universe_of_aux : in FStar_Syntax_Subst.subst subst1 res1 else - (let uu____28934 = + (let uu____28972 = FStar_Syntax_Print.term_to_string res1 in - level_of_type_fail env e uu____28934))) - | FStar_Syntax_Syntax.Tm_match (uu____28936,hd1::uu____28938) -> - let uu____29003 = FStar_Syntax_Subst.open_branch hd1 in - (match uu____29003 with - | (uu____29004,uu____29005,hd2) -> universe_of_aux env hd2) - | FStar_Syntax_Syntax.Tm_match (uu____29023,[]) -> + level_of_type_fail env e uu____28972))) + | FStar_Syntax_Syntax.Tm_match (uu____28974,hd1::uu____28976) -> + let uu____29041 = FStar_Syntax_Subst.open_branch hd1 in + (match uu____29041 with + | (uu____29042,uu____29043,hd2) -> universe_of_aux env hd2) + | FStar_Syntax_Syntax.Tm_match (uu____29061,[]) -> level_of_type_fail env e "empty match cases" let (universe_of : @@ -11514,8 +11537,8 @@ let (universe_of : = fun env -> fun e -> - let uu____29070 = universe_of_aux env e in - level_of_type env e uu____29070 + let uu____29108 = universe_of_aux env e in + level_of_type env e uu____29108 let (tc_tparams : FStar_TypeChecker_Env.env_t -> @@ -11525,8 +11548,8 @@ let (tc_tparams : = fun env0 -> fun tps -> - let uu____29094 = tc_binders env0 tps in - match uu____29094 with + let uu____29132 = tc_binders env0 tps in + match uu____29132 with | (tps1,env,g,us) -> (FStar_TypeChecker_Rel.force_trivial_guard env0 g; (tps1, env, us)) @@ -11543,142 +11566,142 @@ let rec (type_of_well_typed_term : in let t1 = FStar_Syntax_Subst.compress t in match t1.FStar_Syntax_Syntax.n with - | FStar_Syntax_Syntax.Tm_delayed uu____29152 -> failwith "Impossible" - | FStar_Syntax_Syntax.Tm_bvar uu____29178 -> failwith "Impossible" + | FStar_Syntax_Syntax.Tm_delayed uu____29190 -> failwith "Impossible" + | FStar_Syntax_Syntax.Tm_bvar uu____29216 -> failwith "Impossible" | FStar_Syntax_Syntax.Tm_name x -> FStar_Pervasives_Native.Some (x.FStar_Syntax_Syntax.sort) | FStar_Syntax_Syntax.Tm_lazy i -> - let uu____29184 = FStar_Syntax_Util.unfold_lazy i in - type_of_well_typed_term env uu____29184 + let uu____29222 = FStar_Syntax_Util.unfold_lazy i in + type_of_well_typed_term env uu____29222 | FStar_Syntax_Syntax.Tm_fvar fv -> - let uu____29186 = + let uu____29224 = FStar_TypeChecker_Env.try_lookup_and_inst_lid env [] (fv.FStar_Syntax_Syntax.fv_name).FStar_Syntax_Syntax.v in - FStar_Util.bind_opt uu____29186 - (fun uu____29200 -> - match uu____29200 with - | (t2,uu____29208) -> FStar_Pervasives_Native.Some t2) + FStar_Util.bind_opt uu____29224 + (fun uu____29238 -> + match uu____29238 with + | (t2,uu____29246) -> FStar_Pervasives_Native.Some t2) | FStar_Syntax_Syntax.Tm_uinst ({ FStar_Syntax_Syntax.n = FStar_Syntax_Syntax.Tm_fvar fv; - FStar_Syntax_Syntax.pos = uu____29210; - FStar_Syntax_Syntax.vars = uu____29211;_},us) + FStar_Syntax_Syntax.pos = uu____29248; + FStar_Syntax_Syntax.vars = uu____29249;_},us) -> - let uu____29217 = + let uu____29255 = FStar_TypeChecker_Env.try_lookup_and_inst_lid env us (fv.FStar_Syntax_Syntax.fv_name).FStar_Syntax_Syntax.v in - FStar_Util.bind_opt uu____29217 - (fun uu____29231 -> - match uu____29231 with - | (t2,uu____29239) -> FStar_Pervasives_Native.Some t2) + FStar_Util.bind_opt uu____29255 + (fun uu____29269 -> + match uu____29269 with + | (t2,uu____29277) -> FStar_Pervasives_Native.Some t2) | FStar_Syntax_Syntax.Tm_constant (FStar_Const.Const_reify ) -> FStar_Pervasives_Native.None | FStar_Syntax_Syntax.Tm_constant (FStar_Const.Const_reflect - uu____29240) -> FStar_Pervasives_Native.None + uu____29278) -> FStar_Pervasives_Native.None | FStar_Syntax_Syntax.Tm_constant sc -> - let uu____29242 = tc_constant env t1.FStar_Syntax_Syntax.pos sc in - FStar_Pervasives_Native.Some uu____29242 + let uu____29280 = tc_constant env t1.FStar_Syntax_Syntax.pos sc in + FStar_Pervasives_Native.Some uu____29280 | FStar_Syntax_Syntax.Tm_type u -> - let uu____29244 = mk_tm_type (FStar_Syntax_Syntax.U_succ u) in - FStar_Pervasives_Native.Some uu____29244 + let uu____29282 = mk_tm_type (FStar_Syntax_Syntax.U_succ u) in + FStar_Pervasives_Native.Some uu____29282 | FStar_Syntax_Syntax.Tm_abs (bs,body,FStar_Pervasives_Native.Some { FStar_Syntax_Syntax.residual_effect = eff; FStar_Syntax_Syntax.residual_typ = FStar_Pervasives_Native.Some tbody; - FStar_Syntax_Syntax.residual_flags = uu____29249;_}) + FStar_Syntax_Syntax.residual_flags = uu____29287;_}) -> let mk_comp = - let uu____29293 = + let uu____29331 = FStar_Ident.lid_equals eff FStar_Parser_Const.effect_Tot_lid in - if uu____29293 + if uu____29331 then FStar_Pervasives_Native.Some FStar_Syntax_Syntax.mk_Total' else - (let uu____29324 = + (let uu____29362 = FStar_Ident.lid_equals eff FStar_Parser_Const.effect_GTot_lid in - if uu____29324 + if uu____29362 then FStar_Pervasives_Native.Some FStar_Syntax_Syntax.mk_GTotal' else FStar_Pervasives_Native.None) in FStar_Util.bind_opt mk_comp (fun f -> - let uu____29394 = universe_of_well_typed_term env tbody in - FStar_Util.bind_opt uu____29394 + let uu____29432 = universe_of_well_typed_term env tbody in + FStar_Util.bind_opt uu____29432 (fun u -> - let uu____29402 = - let uu____29405 = - let uu____29412 = - let uu____29413 = - let uu____29428 = + let uu____29440 = + let uu____29443 = + let uu____29450 = + let uu____29451 = + let uu____29466 = f tbody (FStar_Pervasives_Native.Some u) in - (bs, uu____29428) in - FStar_Syntax_Syntax.Tm_arrow uu____29413 in - FStar_Syntax_Syntax.mk uu____29412 in - uu____29405 FStar_Pervasives_Native.None + (bs, uu____29466) in + FStar_Syntax_Syntax.Tm_arrow uu____29451 in + FStar_Syntax_Syntax.mk uu____29450 in + uu____29443 FStar_Pervasives_Native.None t1.FStar_Syntax_Syntax.pos in - FStar_Pervasives_Native.Some uu____29402)) + FStar_Pervasives_Native.Some uu____29440)) | FStar_Syntax_Syntax.Tm_arrow (bs,c) -> - let uu____29465 = FStar_Syntax_Subst.open_comp bs c in - (match uu____29465 with + let uu____29503 = FStar_Syntax_Subst.open_comp bs c in + (match uu____29503 with | (bs1,c1) -> let rec aux env1 us bs2 = match bs2 with | [] -> - let uu____29524 = + let uu____29562 = universe_of_well_typed_term env1 (FStar_Syntax_Util.comp_result c1) in - FStar_Util.bind_opt uu____29524 + FStar_Util.bind_opt uu____29562 (fun uc -> - let uu____29532 = + let uu____29570 = mk_tm_type (FStar_Syntax_Syntax.U_max (uc :: us)) in - FStar_Pervasives_Native.Some uu____29532) + FStar_Pervasives_Native.Some uu____29570) | (x,imp)::bs3 -> - let uu____29558 = + let uu____29596 = universe_of_well_typed_term env1 x.FStar_Syntax_Syntax.sort in - FStar_Util.bind_opt uu____29558 + FStar_Util.bind_opt uu____29596 (fun u_x -> let env2 = FStar_TypeChecker_Env.push_bv env1 x in aux env2 (u_x :: us) bs3) in aux env [] bs1) - | FStar_Syntax_Syntax.Tm_abs uu____29567 -> + | FStar_Syntax_Syntax.Tm_abs uu____29605 -> FStar_Pervasives_Native.None - | FStar_Syntax_Syntax.Tm_refine (x,uu____29587) -> - let uu____29592 = + | FStar_Syntax_Syntax.Tm_refine (x,uu____29625) -> + let uu____29630 = universe_of_well_typed_term env x.FStar_Syntax_Syntax.sort in - FStar_Util.bind_opt uu____29592 + FStar_Util.bind_opt uu____29630 (fun u_x -> - let uu____29600 = mk_tm_type u_x in - FStar_Pervasives_Native.Some uu____29600) + let uu____29638 = mk_tm_type u_x in + FStar_Pervasives_Native.Some uu____29638) | FStar_Syntax_Syntax.Tm_app ({ FStar_Syntax_Syntax.n = FStar_Syntax_Syntax.Tm_constant (FStar_Const.Const_range_of ); - FStar_Syntax_Syntax.pos = uu____29605; - FStar_Syntax_Syntax.vars = uu____29606;_},a::hd1::rest) + FStar_Syntax_Syntax.pos = uu____29643; + FStar_Syntax_Syntax.vars = uu____29644;_},a::hd1::rest) -> let rest1 = hd1 :: rest in - let uu____29685 = FStar_Syntax_Util.head_and_args t1 in - (match uu____29685 with - | (unary_op1,uu____29705) -> + let uu____29723 = FStar_Syntax_Util.head_and_args t1 in + (match uu____29723 with + | (unary_op1,uu____29743) -> let head1 = - let uu____29733 = + let uu____29771 = FStar_Range.union_ranges unary_op1.FStar_Syntax_Syntax.pos (FStar_Pervasives_Native.fst a).FStar_Syntax_Syntax.pos in FStar_Syntax_Syntax.mk (FStar_Syntax_Syntax.Tm_app (unary_op1, [a])) - FStar_Pervasives_Native.None uu____29733 + FStar_Pervasives_Native.None uu____29771 in let t2 = FStar_Syntax_Syntax.mk @@ -11690,21 +11713,21 @@ let rec (type_of_well_typed_term : ({ FStar_Syntax_Syntax.n = FStar_Syntax_Syntax.Tm_constant (FStar_Const.Const_set_range_of ); - FStar_Syntax_Syntax.pos = uu____29781; - FStar_Syntax_Syntax.vars = uu____29782;_},a1::a2::hd1::rest) + FStar_Syntax_Syntax.pos = uu____29819; + FStar_Syntax_Syntax.vars = uu____29820;_},a1::a2::hd1::rest) -> let rest1 = hd1 :: rest in - let uu____29878 = FStar_Syntax_Util.head_and_args t1 in - (match uu____29878 with - | (unary_op1,uu____29898) -> + let uu____29916 = FStar_Syntax_Util.head_and_args t1 in + (match uu____29916 with + | (unary_op1,uu____29936) -> let head1 = - let uu____29926 = + let uu____29964 = FStar_Range.union_ranges unary_op1.FStar_Syntax_Syntax.pos (FStar_Pervasives_Native.fst a1).FStar_Syntax_Syntax.pos in FStar_Syntax_Syntax.mk (FStar_Syntax_Syntax.Tm_app (unary_op1, [a1; a2])) - FStar_Pervasives_Native.None uu____29926 + FStar_Pervasives_Native.None uu____29964 in let t2 = FStar_Syntax_Syntax.mk @@ -11716,32 +11739,32 @@ let rec (type_of_well_typed_term : ({ FStar_Syntax_Syntax.n = FStar_Syntax_Syntax.Tm_constant (FStar_Const.Const_range_of ); - FStar_Syntax_Syntax.pos = uu____29982; - FStar_Syntax_Syntax.vars = uu____29983;_},uu____29984::[]) + FStar_Syntax_Syntax.pos = uu____30020; + FStar_Syntax_Syntax.vars = uu____30021;_},uu____30022::[]) -> FStar_Pervasives_Native.Some FStar_Syntax_Syntax.t_range | FStar_Syntax_Syntax.Tm_app ({ FStar_Syntax_Syntax.n = FStar_Syntax_Syntax.Tm_constant (FStar_Const.Const_set_range_of ); - FStar_Syntax_Syntax.pos = uu____30023; - FStar_Syntax_Syntax.vars = uu____30024;_},(t2,uu____30026)::uu____30027::[]) + FStar_Syntax_Syntax.pos = uu____30061; + FStar_Syntax_Syntax.vars = uu____30062;_},(t2,uu____30064)::uu____30065::[]) -> type_of_well_typed_term env t2 | FStar_Syntax_Syntax.Tm_app (hd1,args) -> let t_hd = type_of_well_typed_term env hd1 in let rec aux t_hd1 = - let uu____30123 = - let uu____30124 = + let uu____30161 = + let uu____30162 = FStar_TypeChecker_Normalize.unfold_whnf env t_hd1 in - uu____30124.FStar_Syntax_Syntax.n in - match uu____30123 with + uu____30162.FStar_Syntax_Syntax.n in + match uu____30161 with | FStar_Syntax_Syntax.Tm_arrow (bs,c) -> let n_args = FStar_List.length args in let n_bs = FStar_List.length bs in let bs_t_opt = if n_args < n_bs then - let uu____30197 = FStar_Util.first_N n_args bs in - match uu____30197 with + let uu____30235 = FStar_Util.first_N n_args bs in + match uu____30235 with | (bs1,rest) -> let t2 = FStar_Syntax_Syntax.mk @@ -11749,24 +11772,24 @@ let rec (type_of_well_typed_term : FStar_Pervasives_Native.None t_hd1.FStar_Syntax_Syntax.pos in - let uu____30285 = - let uu____30290 = FStar_Syntax_Syntax.mk_Total t2 + let uu____30323 = + let uu____30328 = FStar_Syntax_Syntax.mk_Total t2 in - FStar_Syntax_Subst.open_comp bs1 uu____30290 in - (match uu____30285 with + FStar_Syntax_Subst.open_comp bs1 uu____30328 in + (match uu____30323 with | (bs2,c1) -> FStar_Pervasives_Native.Some (bs2, (FStar_Syntax_Util.comp_result c1))) else if n_args = n_bs then - (let uu____30344 = FStar_Syntax_Subst.open_comp bs c + (let uu____30382 = FStar_Syntax_Subst.open_comp bs c in - match uu____30344 with + match uu____30382 with | (bs1,c1) -> - let uu____30365 = + let uu____30403 = FStar_Syntax_Util.is_tot_or_gtot_comp c1 in - if uu____30365 + if uu____30403 then FStar_Pervasives_Native.Some (bs1, (FStar_Syntax_Util.comp_result c1)) @@ -11774,8 +11797,8 @@ let rec (type_of_well_typed_term : else FStar_Pervasives_Native.None in FStar_Util.bind_opt bs_t_opt - (fun uu____30447 -> - match uu____30447 with + (fun uu____30485 -> + match uu____30485 with | (bs1,t2) -> let subst1 = FStar_List.map2 @@ -11786,36 +11809,36 @@ let rec (type_of_well_typed_term : (FStar_Pervasives_Native.fst a))) bs1 args in - let uu____30523 = FStar_Syntax_Subst.subst subst1 t2 + let uu____30561 = FStar_Syntax_Subst.subst subst1 t2 in - FStar_Pervasives_Native.Some uu____30523) - | FStar_Syntax_Syntax.Tm_refine (x,uu____30525) -> + FStar_Pervasives_Native.Some uu____30561) + | FStar_Syntax_Syntax.Tm_refine (x,uu____30563) -> aux x.FStar_Syntax_Syntax.sort - | FStar_Syntax_Syntax.Tm_ascribed (t2,uu____30531,uu____30532) -> + | FStar_Syntax_Syntax.Tm_ascribed (t2,uu____30569,uu____30570) -> aux t2 - | uu____30573 -> FStar_Pervasives_Native.None in + | uu____30611 -> FStar_Pervasives_Native.None in FStar_Util.bind_opt t_hd aux | FStar_Syntax_Syntax.Tm_ascribed - (uu____30574,(FStar_Util.Inl t2,uu____30576),uu____30577) -> + (uu____30612,(FStar_Util.Inl t2,uu____30614),uu____30615) -> FStar_Pervasives_Native.Some t2 | FStar_Syntax_Syntax.Tm_ascribed - (uu____30624,(FStar_Util.Inr c,uu____30626),uu____30627) -> + (uu____30662,(FStar_Util.Inr c,uu____30664),uu____30665) -> FStar_Pervasives_Native.Some (FStar_Syntax_Util.comp_result c) | FStar_Syntax_Syntax.Tm_uvar (u,s) -> - let uu____30692 = + let uu____30730 = FStar_Syntax_Subst.subst' s u.FStar_Syntax_Syntax.ctx_uvar_typ in - FStar_Pervasives_Native.Some uu____30692 + FStar_Pervasives_Native.Some uu____30730 | FStar_Syntax_Syntax.Tm_quoted (tm,qi) -> FStar_Pervasives_Native.Some FStar_Syntax_Syntax.t_term - | FStar_Syntax_Syntax.Tm_meta (t2,uu____30700) -> + | FStar_Syntax_Syntax.Tm_meta (t2,uu____30738) -> type_of_well_typed_term env t2 - | FStar_Syntax_Syntax.Tm_match uu____30705 -> + | FStar_Syntax_Syntax.Tm_match uu____30743 -> FStar_Pervasives_Native.None - | FStar_Syntax_Syntax.Tm_let uu____30728 -> + | FStar_Syntax_Syntax.Tm_let uu____30766 -> FStar_Pervasives_Native.None | FStar_Syntax_Syntax.Tm_unknown -> FStar_Pervasives_Native.None - | FStar_Syntax_Syntax.Tm_uinst uu____30742 -> + | FStar_Syntax_Syntax.Tm_uinst uu____30780 -> FStar_Pervasives_Native.None and (universe_of_well_typed_term : @@ -11825,14 +11848,14 @@ and (universe_of_well_typed_term : = fun env -> fun t -> - let uu____30753 = type_of_well_typed_term env t in - match uu____30753 with + let uu____30791 = type_of_well_typed_term env t in + match uu____30791 with | FStar_Pervasives_Native.Some { FStar_Syntax_Syntax.n = FStar_Syntax_Syntax.Tm_type u; - FStar_Syntax_Syntax.pos = uu____30759; - FStar_Syntax_Syntax.vars = uu____30760;_} + FStar_Syntax_Syntax.pos = uu____30797; + FStar_Syntax_Syntax.vars = uu____30798;_} -> FStar_Pervasives_Native.Some u - | uu____30763 -> FStar_Pervasives_Native.None + | uu____30801 -> FStar_Pervasives_Native.None let (check_type_of_well_typed_term' : Prims.bool -> @@ -11846,144 +11869,144 @@ let (check_type_of_well_typed_term' : fun k -> let env1 = FStar_TypeChecker_Env.set_expected_typ env k in let env2 = - let uu___4033_30791 = env1 in + let uu___4037_30829 = env1 in { FStar_TypeChecker_Env.solver = - (uu___4033_30791.FStar_TypeChecker_Env.solver); + (uu___4037_30829.FStar_TypeChecker_Env.solver); FStar_TypeChecker_Env.range = - (uu___4033_30791.FStar_TypeChecker_Env.range); + (uu___4037_30829.FStar_TypeChecker_Env.range); FStar_TypeChecker_Env.curmodule = - (uu___4033_30791.FStar_TypeChecker_Env.curmodule); + (uu___4037_30829.FStar_TypeChecker_Env.curmodule); FStar_TypeChecker_Env.gamma = - (uu___4033_30791.FStar_TypeChecker_Env.gamma); + (uu___4037_30829.FStar_TypeChecker_Env.gamma); FStar_TypeChecker_Env.gamma_sig = - (uu___4033_30791.FStar_TypeChecker_Env.gamma_sig); + (uu___4037_30829.FStar_TypeChecker_Env.gamma_sig); FStar_TypeChecker_Env.gamma_cache = - (uu___4033_30791.FStar_TypeChecker_Env.gamma_cache); + (uu___4037_30829.FStar_TypeChecker_Env.gamma_cache); FStar_TypeChecker_Env.modules = - (uu___4033_30791.FStar_TypeChecker_Env.modules); + (uu___4037_30829.FStar_TypeChecker_Env.modules); FStar_TypeChecker_Env.expected_typ = - (uu___4033_30791.FStar_TypeChecker_Env.expected_typ); + (uu___4037_30829.FStar_TypeChecker_Env.expected_typ); FStar_TypeChecker_Env.sigtab = - (uu___4033_30791.FStar_TypeChecker_Env.sigtab); + (uu___4037_30829.FStar_TypeChecker_Env.sigtab); FStar_TypeChecker_Env.attrtab = - (uu___4033_30791.FStar_TypeChecker_Env.attrtab); + (uu___4037_30829.FStar_TypeChecker_Env.attrtab); FStar_TypeChecker_Env.instantiate_imp = - (uu___4033_30791.FStar_TypeChecker_Env.instantiate_imp); + (uu___4037_30829.FStar_TypeChecker_Env.instantiate_imp); FStar_TypeChecker_Env.effects = - (uu___4033_30791.FStar_TypeChecker_Env.effects); + (uu___4037_30829.FStar_TypeChecker_Env.effects); FStar_TypeChecker_Env.generalize = - (uu___4033_30791.FStar_TypeChecker_Env.generalize); + (uu___4037_30829.FStar_TypeChecker_Env.generalize); FStar_TypeChecker_Env.letrecs = - (uu___4033_30791.FStar_TypeChecker_Env.letrecs); + (uu___4037_30829.FStar_TypeChecker_Env.letrecs); FStar_TypeChecker_Env.top_level = - (uu___4033_30791.FStar_TypeChecker_Env.top_level); + (uu___4037_30829.FStar_TypeChecker_Env.top_level); FStar_TypeChecker_Env.check_uvars = - (uu___4033_30791.FStar_TypeChecker_Env.check_uvars); + (uu___4037_30829.FStar_TypeChecker_Env.check_uvars); FStar_TypeChecker_Env.use_eq = - (uu___4033_30791.FStar_TypeChecker_Env.use_eq); + (uu___4037_30829.FStar_TypeChecker_Env.use_eq); FStar_TypeChecker_Env.is_iface = - (uu___4033_30791.FStar_TypeChecker_Env.is_iface); + (uu___4037_30829.FStar_TypeChecker_Env.is_iface); FStar_TypeChecker_Env.admit = - (uu___4033_30791.FStar_TypeChecker_Env.admit); + (uu___4037_30829.FStar_TypeChecker_Env.admit); FStar_TypeChecker_Env.lax = - (uu___4033_30791.FStar_TypeChecker_Env.lax); + (uu___4037_30829.FStar_TypeChecker_Env.lax); FStar_TypeChecker_Env.lax_universes = - (uu___4033_30791.FStar_TypeChecker_Env.lax_universes); + (uu___4037_30829.FStar_TypeChecker_Env.lax_universes); FStar_TypeChecker_Env.phase1 = - (uu___4033_30791.FStar_TypeChecker_Env.phase1); + (uu___4037_30829.FStar_TypeChecker_Env.phase1); FStar_TypeChecker_Env.failhard = - (uu___4033_30791.FStar_TypeChecker_Env.failhard); + (uu___4037_30829.FStar_TypeChecker_Env.failhard); FStar_TypeChecker_Env.nosynth = - (uu___4033_30791.FStar_TypeChecker_Env.nosynth); + (uu___4037_30829.FStar_TypeChecker_Env.nosynth); FStar_TypeChecker_Env.uvar_subtyping = - (uu___4033_30791.FStar_TypeChecker_Env.uvar_subtyping); + (uu___4037_30829.FStar_TypeChecker_Env.uvar_subtyping); FStar_TypeChecker_Env.tc_term = - (uu___4033_30791.FStar_TypeChecker_Env.tc_term); + (uu___4037_30829.FStar_TypeChecker_Env.tc_term); FStar_TypeChecker_Env.type_of = - (uu___4033_30791.FStar_TypeChecker_Env.type_of); + (uu___4037_30829.FStar_TypeChecker_Env.type_of); FStar_TypeChecker_Env.universe_of = - (uu___4033_30791.FStar_TypeChecker_Env.universe_of); + (uu___4037_30829.FStar_TypeChecker_Env.universe_of); FStar_TypeChecker_Env.check_type_of = - (uu___4033_30791.FStar_TypeChecker_Env.check_type_of); + (uu___4037_30829.FStar_TypeChecker_Env.check_type_of); FStar_TypeChecker_Env.use_bv_sorts = true; FStar_TypeChecker_Env.qtbl_name_and_index = - (uu___4033_30791.FStar_TypeChecker_Env.qtbl_name_and_index); + (uu___4037_30829.FStar_TypeChecker_Env.qtbl_name_and_index); FStar_TypeChecker_Env.normalized_eff_names = - (uu___4033_30791.FStar_TypeChecker_Env.normalized_eff_names); + (uu___4037_30829.FStar_TypeChecker_Env.normalized_eff_names); FStar_TypeChecker_Env.fv_delta_depths = - (uu___4033_30791.FStar_TypeChecker_Env.fv_delta_depths); + (uu___4037_30829.FStar_TypeChecker_Env.fv_delta_depths); FStar_TypeChecker_Env.proof_ns = - (uu___4033_30791.FStar_TypeChecker_Env.proof_ns); + (uu___4037_30829.FStar_TypeChecker_Env.proof_ns); FStar_TypeChecker_Env.synth_hook = - (uu___4033_30791.FStar_TypeChecker_Env.synth_hook); + (uu___4037_30829.FStar_TypeChecker_Env.synth_hook); FStar_TypeChecker_Env.splice = - (uu___4033_30791.FStar_TypeChecker_Env.splice); + (uu___4037_30829.FStar_TypeChecker_Env.splice); FStar_TypeChecker_Env.mpreprocess = - (uu___4033_30791.FStar_TypeChecker_Env.mpreprocess); + (uu___4037_30829.FStar_TypeChecker_Env.mpreprocess); FStar_TypeChecker_Env.postprocess = - (uu___4033_30791.FStar_TypeChecker_Env.postprocess); + (uu___4037_30829.FStar_TypeChecker_Env.postprocess); FStar_TypeChecker_Env.is_native_tactic = - (uu___4033_30791.FStar_TypeChecker_Env.is_native_tactic); + (uu___4037_30829.FStar_TypeChecker_Env.is_native_tactic); FStar_TypeChecker_Env.identifier_info = - (uu___4033_30791.FStar_TypeChecker_Env.identifier_info); + (uu___4037_30829.FStar_TypeChecker_Env.identifier_info); FStar_TypeChecker_Env.tc_hooks = - (uu___4033_30791.FStar_TypeChecker_Env.tc_hooks); + (uu___4037_30829.FStar_TypeChecker_Env.tc_hooks); FStar_TypeChecker_Env.dsenv = - (uu___4033_30791.FStar_TypeChecker_Env.dsenv); + (uu___4037_30829.FStar_TypeChecker_Env.dsenv); FStar_TypeChecker_Env.nbe = - (uu___4033_30791.FStar_TypeChecker_Env.nbe); + (uu___4037_30829.FStar_TypeChecker_Env.nbe); FStar_TypeChecker_Env.strict_args_tab = - (uu___4033_30791.FStar_TypeChecker_Env.strict_args_tab); + (uu___4037_30829.FStar_TypeChecker_Env.strict_args_tab); FStar_TypeChecker_Env.erasable_types_tab = - (uu___4033_30791.FStar_TypeChecker_Env.erasable_types_tab) + (uu___4037_30829.FStar_TypeChecker_Env.erasable_types_tab) } in - let slow_check uu____30798 = + let slow_check uu____30836 = if must_total then - let uu____30800 = env2.FStar_TypeChecker_Env.type_of env2 t in - match uu____30800 with | (uu____30807,uu____30808,g) -> g + let uu____30838 = env2.FStar_TypeChecker_Env.type_of env2 t in + match uu____30838 with | (uu____30845,uu____30846,g) -> g else - (let uu____30812 = env2.FStar_TypeChecker_Env.tc_term env2 t + (let uu____30850 = env2.FStar_TypeChecker_Env.tc_term env2 t in - match uu____30812 with | (uu____30819,uu____30820,g) -> g) + match uu____30850 with | (uu____30857,uu____30858,g) -> g) in - let uu____30822 = type_of_well_typed_term env2 t in - match uu____30822 with + let uu____30860 = type_of_well_typed_term env2 t in + match uu____30860 with | FStar_Pervasives_Native.None -> slow_check () | FStar_Pervasives_Native.Some k' -> - ((let uu____30827 = + ((let uu____30865 = FStar_All.pipe_left (FStar_TypeChecker_Env.debug env2) (FStar_Options.Other "FastImplicits") in - if uu____30827 + if uu____30865 then - let uu____30832 = + let uu____30870 = FStar_Range.string_of_range t.FStar_Syntax_Syntax.pos in - let uu____30834 = FStar_Syntax_Print.term_to_string t in - let uu____30836 = FStar_Syntax_Print.term_to_string k' in - let uu____30838 = FStar_Syntax_Print.term_to_string k in + let uu____30872 = FStar_Syntax_Print.term_to_string t in + let uu____30874 = FStar_Syntax_Print.term_to_string k' in + let uu____30876 = FStar_Syntax_Print.term_to_string k in FStar_Util.print4 "(%s) Fast check %s : %s <:? %s\n" - uu____30832 uu____30834 uu____30836 uu____30838 + uu____30870 uu____30872 uu____30874 uu____30876 else ()); (let g = FStar_TypeChecker_Rel.subtype_nosmt env2 k' k in - (let uu____30847 = + (let uu____30885 = FStar_All.pipe_left (FStar_TypeChecker_Env.debug env2) (FStar_Options.Other "FastImplicits") in - if uu____30847 + if uu____30885 then - let uu____30852 = + let uu____30890 = FStar_Range.string_of_range t.FStar_Syntax_Syntax.pos in - let uu____30854 = FStar_Syntax_Print.term_to_string t in - let uu____30856 = FStar_Syntax_Print.term_to_string k' in - let uu____30858 = FStar_Syntax_Print.term_to_string k in + let uu____30892 = FStar_Syntax_Print.term_to_string t in + let uu____30894 = FStar_Syntax_Print.term_to_string k' in + let uu____30896 = FStar_Syntax_Print.term_to_string k in FStar_Util.print5 "(%s) Fast check %s: %s : %s <: %s\n" - uu____30852 + uu____30890 (if FStar_Option.isSome g then "succeeded with guard" - else "failed") uu____30854 uu____30856 uu____30858 + else "failed") uu____30892 uu____30894 uu____30896 else ()); (match g with | FStar_Pervasives_Native.None -> slow_check () @@ -12001,112 +12024,112 @@ let (check_type_of_well_typed_term : fun k -> let env1 = FStar_TypeChecker_Env.set_expected_typ env k in let env2 = - let uu___4064_30895 = env1 in + let uu___4068_30933 = env1 in { FStar_TypeChecker_Env.solver = - (uu___4064_30895.FStar_TypeChecker_Env.solver); + (uu___4068_30933.FStar_TypeChecker_Env.solver); FStar_TypeChecker_Env.range = - (uu___4064_30895.FStar_TypeChecker_Env.range); + (uu___4068_30933.FStar_TypeChecker_Env.range); FStar_TypeChecker_Env.curmodule = - (uu___4064_30895.FStar_TypeChecker_Env.curmodule); + (uu___4068_30933.FStar_TypeChecker_Env.curmodule); FStar_TypeChecker_Env.gamma = - (uu___4064_30895.FStar_TypeChecker_Env.gamma); + (uu___4068_30933.FStar_TypeChecker_Env.gamma); FStar_TypeChecker_Env.gamma_sig = - (uu___4064_30895.FStar_TypeChecker_Env.gamma_sig); + (uu___4068_30933.FStar_TypeChecker_Env.gamma_sig); FStar_TypeChecker_Env.gamma_cache = - (uu___4064_30895.FStar_TypeChecker_Env.gamma_cache); + (uu___4068_30933.FStar_TypeChecker_Env.gamma_cache); FStar_TypeChecker_Env.modules = - (uu___4064_30895.FStar_TypeChecker_Env.modules); + (uu___4068_30933.FStar_TypeChecker_Env.modules); FStar_TypeChecker_Env.expected_typ = - (uu___4064_30895.FStar_TypeChecker_Env.expected_typ); + (uu___4068_30933.FStar_TypeChecker_Env.expected_typ); FStar_TypeChecker_Env.sigtab = - (uu___4064_30895.FStar_TypeChecker_Env.sigtab); + (uu___4068_30933.FStar_TypeChecker_Env.sigtab); FStar_TypeChecker_Env.attrtab = - (uu___4064_30895.FStar_TypeChecker_Env.attrtab); + (uu___4068_30933.FStar_TypeChecker_Env.attrtab); FStar_TypeChecker_Env.instantiate_imp = - (uu___4064_30895.FStar_TypeChecker_Env.instantiate_imp); + (uu___4068_30933.FStar_TypeChecker_Env.instantiate_imp); FStar_TypeChecker_Env.effects = - (uu___4064_30895.FStar_TypeChecker_Env.effects); + (uu___4068_30933.FStar_TypeChecker_Env.effects); FStar_TypeChecker_Env.generalize = - (uu___4064_30895.FStar_TypeChecker_Env.generalize); + (uu___4068_30933.FStar_TypeChecker_Env.generalize); FStar_TypeChecker_Env.letrecs = - (uu___4064_30895.FStar_TypeChecker_Env.letrecs); + (uu___4068_30933.FStar_TypeChecker_Env.letrecs); FStar_TypeChecker_Env.top_level = - (uu___4064_30895.FStar_TypeChecker_Env.top_level); + (uu___4068_30933.FStar_TypeChecker_Env.top_level); FStar_TypeChecker_Env.check_uvars = - (uu___4064_30895.FStar_TypeChecker_Env.check_uvars); + (uu___4068_30933.FStar_TypeChecker_Env.check_uvars); FStar_TypeChecker_Env.use_eq = - (uu___4064_30895.FStar_TypeChecker_Env.use_eq); + (uu___4068_30933.FStar_TypeChecker_Env.use_eq); FStar_TypeChecker_Env.is_iface = - (uu___4064_30895.FStar_TypeChecker_Env.is_iface); + (uu___4068_30933.FStar_TypeChecker_Env.is_iface); FStar_TypeChecker_Env.admit = - (uu___4064_30895.FStar_TypeChecker_Env.admit); + (uu___4068_30933.FStar_TypeChecker_Env.admit); FStar_TypeChecker_Env.lax = - (uu___4064_30895.FStar_TypeChecker_Env.lax); + (uu___4068_30933.FStar_TypeChecker_Env.lax); FStar_TypeChecker_Env.lax_universes = - (uu___4064_30895.FStar_TypeChecker_Env.lax_universes); + (uu___4068_30933.FStar_TypeChecker_Env.lax_universes); FStar_TypeChecker_Env.phase1 = - (uu___4064_30895.FStar_TypeChecker_Env.phase1); + (uu___4068_30933.FStar_TypeChecker_Env.phase1); FStar_TypeChecker_Env.failhard = - (uu___4064_30895.FStar_TypeChecker_Env.failhard); + (uu___4068_30933.FStar_TypeChecker_Env.failhard); FStar_TypeChecker_Env.nosynth = - (uu___4064_30895.FStar_TypeChecker_Env.nosynth); + (uu___4068_30933.FStar_TypeChecker_Env.nosynth); FStar_TypeChecker_Env.uvar_subtyping = - (uu___4064_30895.FStar_TypeChecker_Env.uvar_subtyping); + (uu___4068_30933.FStar_TypeChecker_Env.uvar_subtyping); FStar_TypeChecker_Env.tc_term = - (uu___4064_30895.FStar_TypeChecker_Env.tc_term); + (uu___4068_30933.FStar_TypeChecker_Env.tc_term); FStar_TypeChecker_Env.type_of = - (uu___4064_30895.FStar_TypeChecker_Env.type_of); + (uu___4068_30933.FStar_TypeChecker_Env.type_of); FStar_TypeChecker_Env.universe_of = - (uu___4064_30895.FStar_TypeChecker_Env.universe_of); + (uu___4068_30933.FStar_TypeChecker_Env.universe_of); FStar_TypeChecker_Env.check_type_of = - (uu___4064_30895.FStar_TypeChecker_Env.check_type_of); + (uu___4068_30933.FStar_TypeChecker_Env.check_type_of); FStar_TypeChecker_Env.use_bv_sorts = true; FStar_TypeChecker_Env.qtbl_name_and_index = - (uu___4064_30895.FStar_TypeChecker_Env.qtbl_name_and_index); + (uu___4068_30933.FStar_TypeChecker_Env.qtbl_name_and_index); FStar_TypeChecker_Env.normalized_eff_names = - (uu___4064_30895.FStar_TypeChecker_Env.normalized_eff_names); + (uu___4068_30933.FStar_TypeChecker_Env.normalized_eff_names); FStar_TypeChecker_Env.fv_delta_depths = - (uu___4064_30895.FStar_TypeChecker_Env.fv_delta_depths); + (uu___4068_30933.FStar_TypeChecker_Env.fv_delta_depths); FStar_TypeChecker_Env.proof_ns = - (uu___4064_30895.FStar_TypeChecker_Env.proof_ns); + (uu___4068_30933.FStar_TypeChecker_Env.proof_ns); FStar_TypeChecker_Env.synth_hook = - (uu___4064_30895.FStar_TypeChecker_Env.synth_hook); + (uu___4068_30933.FStar_TypeChecker_Env.synth_hook); FStar_TypeChecker_Env.splice = - (uu___4064_30895.FStar_TypeChecker_Env.splice); + (uu___4068_30933.FStar_TypeChecker_Env.splice); FStar_TypeChecker_Env.mpreprocess = - (uu___4064_30895.FStar_TypeChecker_Env.mpreprocess); + (uu___4068_30933.FStar_TypeChecker_Env.mpreprocess); FStar_TypeChecker_Env.postprocess = - (uu___4064_30895.FStar_TypeChecker_Env.postprocess); + (uu___4068_30933.FStar_TypeChecker_Env.postprocess); FStar_TypeChecker_Env.is_native_tactic = - (uu___4064_30895.FStar_TypeChecker_Env.is_native_tactic); + (uu___4068_30933.FStar_TypeChecker_Env.is_native_tactic); FStar_TypeChecker_Env.identifier_info = - (uu___4064_30895.FStar_TypeChecker_Env.identifier_info); + (uu___4068_30933.FStar_TypeChecker_Env.identifier_info); FStar_TypeChecker_Env.tc_hooks = - (uu___4064_30895.FStar_TypeChecker_Env.tc_hooks); + (uu___4068_30933.FStar_TypeChecker_Env.tc_hooks); FStar_TypeChecker_Env.dsenv = - (uu___4064_30895.FStar_TypeChecker_Env.dsenv); + (uu___4068_30933.FStar_TypeChecker_Env.dsenv); FStar_TypeChecker_Env.nbe = - (uu___4064_30895.FStar_TypeChecker_Env.nbe); + (uu___4068_30933.FStar_TypeChecker_Env.nbe); FStar_TypeChecker_Env.strict_args_tab = - (uu___4064_30895.FStar_TypeChecker_Env.strict_args_tab); + (uu___4068_30933.FStar_TypeChecker_Env.strict_args_tab); FStar_TypeChecker_Env.erasable_types_tab = - (uu___4064_30895.FStar_TypeChecker_Env.erasable_types_tab) + (uu___4068_30933.FStar_TypeChecker_Env.erasable_types_tab) } in - let slow_check uu____30902 = + let slow_check uu____30940 = if must_total then - let uu____30904 = env2.FStar_TypeChecker_Env.type_of env2 t in - match uu____30904 with | (uu____30911,uu____30912,g) -> g + let uu____30942 = env2.FStar_TypeChecker_Env.type_of env2 t in + match uu____30942 with | (uu____30949,uu____30950,g) -> g else - (let uu____30916 = env2.FStar_TypeChecker_Env.tc_term env2 t + (let uu____30954 = env2.FStar_TypeChecker_Env.tc_term env2 t in - match uu____30916 with | (uu____30923,uu____30924,g) -> g) + match uu____30954 with | (uu____30961,uu____30962,g) -> g) in - let uu____30926 = - let uu____30928 = FStar_Options.__temp_fast_implicits () in - FStar_All.pipe_left Prims.op_Negation uu____30928 in - if uu____30926 + let uu____30964 = + let uu____30966 = FStar_Options.__temp_fast_implicits () in + FStar_All.pipe_left Prims.op_Negation uu____30966 in + if uu____30964 then slow_check () else check_type_of_well_typed_term' must_total env2 t k
\ No newline at end of file diff --git a/src/typechecker/FStar.TypeChecker.TcTerm.fs b/src/typechecker/FStar.TypeChecker.TcTerm.fs index 346b87e..6500224 100644 --- a/src/typechecker/FStar.TypeChecker.TcTerm.fs +++ b/src/typechecker/FStar.TypeChecker.TcTerm.fs @@ -2605,15 +2605,16 @@ and tc_eqn scrutinee env branch BU.print_string "Typechecking pat_bv_tms ...\n" in //typecheck the pat_bv_tms, to resolve implicits etc. - let pat_bv_tms = - List.fold_left2 (fun acc pat_bv_tm bv -> + //AR: keep adding pat bvs to the env as we move from left to right + let _, pat_bv_tms = + List.fold_left2 (fun (env, acc) pat_bv_tm bv -> let expected_t = U.arrow [S.null_binder pat_t] (S.mk_Total' bv.sort (Env.new_u_univ () |> Some)) in //note, we are explicitly setting lax = true, since these terms apply projectors //which we know are sound as per the branch guard, but hard to convince the typechecker let env = { (Env.set_expected_typ env expected_t) with lax = true } in let pat_bv_tm = tc_trivial_guard env pat_bv_tm |> fst in - acc@[pat_bv_tm] - ) [] pat_bv_tms pat_bvs in + Env.push_bv env bv, acc@[pat_bv_tm] + ) (env, []) pat_bv_tms pat_bvs in let pat_bv_tms = pat_bv_tms |> List.map (fun pat_bv_tm -> mk_Tm_app pat_bv_tm [scrutinee_tm |> S.as_arg] None Range.dummyRange |