Merge pull request #3720 from mtzguido/errs

Some fixes in support of Pulse errors

Author: mtzguido

src/tactics/FStarC.Tactics.V2.Basic.fst

@@ -2635,36 +2635,34 @@ let refl_check_prop_validity (g:env) (e:term) : tac (option unit & issues) =
   else return (None, [unexpected_uvars_issue (Env.get_range g)])
 
 let refl_check_match_complete (g:env) (sc:term) (scty:typ) (pats : list RD.pattern)
-: tac (option (list RD.pattern & list (list RD.binding)))
+: tac (option (list RD.pattern & list (list RD.binding)) & issues)
 =
-  return () ;!
+  refl_typing_builtin_wrapper "refl_check_match_complete" fun _ ->
   (* We just craft a match with the sc and patterns, using `1` in every
   branch, and check it against type int. *)
   let one = U.exp_int "1" in
   let brs = List.map (fun p -> let p = pack_pat p in (p, None, one)) pats in
   let mm = mk (Tm_match {scrutinee=sc; ret_opt=None; brs=brs; rc_opt=None}) sc.pos in
   let env = g in
   let env = Env.set_expected_typ env S.t_int in
-  let! mm, _, g = __tc env mm in
-
-  let errs, b = Errors.catch_errors_and_ignore_rest (fun () -> Env.is_trivial <| Rel.discharge_guard env g) in
-  match errs, b with
-  | [], Some true ->
-    let get_pats t =
-      match (U.unmeta t).n with
-      | Tm_match {brs} -> List.map (fun (p,_,_) -> p) brs
-      | _ -> failwith "refl_check_match_complete: not a match?"
-    in
-    let pats = get_pats mm in
-    let rec bnds_for_pat (p:pat) : list RD.binding =
-      match p.v with
-      | Pat_constant _ -> []
-      | Pat_cons (fv, _, pats) -> List.concatMap (fun (p, _) -> bnds_for_pat p) pats
-      | Pat_var bv -> [bv_to_binding bv]
-      | Pat_dot_term _ -> []
-    in
-    return (Some (List.map inspect_pat pats, List.map bnds_for_pat pats))
-  | _ -> return None
+  let mm, _, guard = TcTerm.typeof_tot_or_gtot_term env mm true in
+
+  Rel.force_trivial_guard env guard;
+  let get_pats t =
+    match (U.unmeta t).n with
+    | Tm_match {brs} -> List.map (fun (p,_,_) -> p) brs
+    | _ -> failwith "refl_check_match_complete: not a match?"
+  in
+  let mm = SC.deep_compress false true mm in // important! we must return fully-compressed patterns
+  let pats = get_pats mm in
+  let rec bnds_for_pat (p:pat) : list RD.binding =
+    match p.v with
+    | Pat_constant _ -> []
+    | Pat_cons (fv, _, pats) -> List.concatMap (fun (p, _) -> bnds_for_pat p) pats
+    | Pat_var bv -> [bv_to_binding bv]
+    | Pat_dot_term _ -> []
+  in
+  (List.map inspect_pat pats, List.map bnds_for_pat pats), []
 
 let refl_instantiate_implicits (g:env) (e:term) (expected_typ : option term)
   : tac (option (list (bv & typ) & term & typ) & issues) =
@@ -2714,6 +2712,9 @@ let refl_instantiate_implicits (g:env) (e:term) (expected_typ : option term)
 
     dbg_refl g (fun _ -> BU.format2 "refl_instantiate_implicits: inferred %s : %s" (show e) (show t));
 
+    // Stop now if we've already logged errors, it's less confusing to the user.
+    Errors.stop_if_err ();
+
     if not (no_univ_uvars_in_term e)
     then Errors.raise_error e Errors.Error_UnexpectedUnresolvedUvar
            (BU.format1 "Elaborated term has unresolved univ uvars: %s" (show e));

src/tactics/FStarC.Tactics.V2.Basic.fsti

@@ -140,7 +140,7 @@ val refl_core_check_term_at_type      : env -> term -> typ -> tac (option Core.t
 val refl_tc_term                      : env -> term -> tac (option (term & (Core.tot_or_ghost & typ)) & issues)
 val refl_universe_of                  : env -> term -> tac (option universe & issues)
 val refl_check_prop_validity          : env -> term -> tac (option unit & issues)
-val refl_check_match_complete         : env -> term -> term -> list pattern -> tac (option (list pattern & list (list RD.binding)))
+val refl_check_match_complete         : env -> term -> term -> list pattern -> tac (option (list pattern & list (list RD.binding)) & issues)
 val refl_instantiate_implicits        : env -> term -> expected_typ:option term -> tac (option (list (bv & typ) & term & typ) & issues)
 val refl_try_unify                    : env -> list (bv & typ) -> term -> term -> tac (option (list (bv & term)) & issues)
 val refl_maybe_relate_after_unfolding : env -> term -> term -> tac (option Core.side & issues)

src/typechecker/FStarC.TypeChecker.Core.fst

@@ -429,6 +429,8 @@ let check_bqual (b0 b1:bqual)
       //we don't care about the inaccessibility qualifier
       //when comparing bquals
       return ()
+    | Some Equality, None
+    | None, Some Equality // The equality qualifier is metadata, ignore it
     | Some Equality, Some Equality ->
       return ()
     | Some (Meta t1), Some (Meta t2) when equal_term t1 t2 ->

src/typechecker/FStarC.TypeChecker.Rel.fst

@@ -2757,6 +2757,8 @@ and solve_binders (bs1:binders) (bs2:binders) (orig:prob) (wl:worklist)
        match a1, a2 with
        | Some (Implicit b1), Some (Implicit b2) ->
          true //we don't care about comparing the dot qualifier in this context
+       | Some Equality, None | None, Some Equality ->
+         true // also don't care about the equality qualifier
        | _ ->
          U.eq_bqual a1 a2
    in

tests/tactics/CheckMatchComplete.fst

@@ -9,36 +9,36 @@ let guard (b:bool) =
 let test_wild () : Tac unit =
   let pat = Reflection.V2.Pat_Var (Sealed.seal (`int)) (Sealed.seal "x") in
   let e = cur_env () in
-  let r = check_match_complete e (`1) (`int) [pat] in
+  let (r, _) = check_match_complete e (`1) (`int) [pat] in
   guard (Some? r)
 let _ = assert True by (test_wild ())
 
 let test_const_ok () : Tac unit =
   let pat = Reflection.V2.Pat_Constant (C_Int 1) in
   let e = cur_env () in
-  let r = check_match_complete e (`1) (`int) [pat] in
+  let (r, _) = check_match_complete e (`1) (`int) [pat] in
   guard (Some? r)
 let _ = assert True by (test_const_ok ())
 
 let test_const_bad () : Tac unit =
   let pat = Reflection.V2.Pat_Constant (C_Int 2) in
   let e = cur_env () in
-  let r = check_match_complete e (`1) (`int) [pat] in
+  let (r, _) = check_match_complete e (`1) (`int) [pat] in
   guard (None? r)
 let _ = assert True by (test_const_bad ())
 
 let test_const_two () : Tac unit =
   let pat1 = Reflection.V2.Pat_Constant (C_Int 1) in
   let pat2 = Reflection.V2.Pat_Var (Sealed.seal (`int)) (Sealed.seal "x") in
   let e = cur_env () in
-  let r = check_match_complete e (`1) (`int) [pat1; pat2] in
+  let (r, _) = check_match_complete e (`1) (`int) [pat1; pat2] in
   guard (Some? r)
 let _ = assert True by (test_const_two ())
 
 let test_const_two' () : Tac unit =
   let pat1 = Reflection.V2.Pat_Constant (C_Int 2) in
   let pat2 = Reflection.V2.Pat_Var (Sealed.seal (`int)) (Sealed.seal "x") in
   let e = cur_env () in
-  let r = check_match_complete e (`1) (`int) [pat1; pat2] in
+  let (r, _) = check_match_complete e (`1) (`int) [pat1; pat2] in
   guard (Some? r)
 let _ = assert True by (test_const_two' ())

ulib/FStar.Stubs.Tactics.V2.Builtins.fsti

@@ -555,9 +555,10 @@ val check_prop_validity (g:env) (t:term)
 val match_complete_token (g:env) (sc:term) (t:typ) (pats:list pattern) (bnds:list (list binding))
   : Type0
 
-// Returns elaborated patterns, the bindings for each one, and a token
+// Returns elaborated patterns, the bindings for each one, and a token. Possibly some issues
+// too.
 val check_match_complete (g:env) (sc:term) (t:typ) (pats:list pattern)
-  : Tac (option (pats_bnds:(list pattern & list (list binding))
+  : Tac (ret_t (pats_bnds:(list pattern & list (list binding))
                            {match_complete_token g sc t (fst pats_bnds) (snd pats_bnds)
                             /\ List.Tot.length (fst pats_bnds) == List.Tot.length (snd pats_bnds)
                             /\ List.Tot.length (fst pats_bnds) == List.Tot.length pats}))