Normalizer: do not drop internal ascriptions

src/typechecker/FStarC.TypeChecker.Normalize.fst

@@ -1297,7 +1297,7 @@ let rec norm : cfg -> env -> stack -> term -> term =
                 let t1 = norm cfg env [] t1 in
                 log cfg  (fun () -> BU.print_string "+++ Normalizing ascription \n");
                 let asc = norm_ascription cfg env asc in
-                rebuild cfg env stack (mk (Tm_ascribed {tm=U.unascribe t1; asc; eff_opt=l}) t.pos)
+                rebuild cfg env stack (mk (Tm_ascribed {tm=t1; asc; eff_opt=l}) t.pos)
             )
 
           | Tm_match {scrutinee=head; ret_opt=asc_opt; brs=branches; rc_opt=lopt} ->

tests/bug-reports/closed/Bug2452.fst

@@ -0,0 +1,19 @@
+module Bug2452
+
+[@@expect_failure]
+let f () : int = (-1) <: nat
+
+[@@expect_failure]
+let f x : bool = true <: (b:bool{false})
+
+[@@expect_failure]
+let g (x : bool) : bool = x <: (b:bool{false})
+
+(* This works, h is just inferred to have a refined type. *)
+let h x : bool = x <: (b:bool{false})
+
+[@@expect_failure]
+let q = f true
+
+[@@expect_failure]
+let z : bool = true <: (b:bool{false})

tests/tactics/DeltaDepth.fst

@@ -31,9 +31,9 @@ let v : t = synth_by_tactic (fun () -> exact (f ()))
 let m = match v with | B _ -> 0 | A x -> x
 
 let _ = assert True by (let t = `m in
-                        let t' = norm_term [delta;iota] t in
-                        (* The reduction of the match leaves an ascription *)
-                        let r = (`(1 <: int)) in
+                        let t' = norm_term [delta;iota;unascribe] t in
+                        (* ^ unascribe since the typechecker adds some ascriptions to the match *)
+                        let r = `1 in
                         if term_eq t' r
                         then ()
-                        else fail ("The match did not reduce!:" ^ term_to_string t'))
+                        else fail ("The match did not reduce!: " ^ term_to_string t'))