Normalizer: do not drop internal ascriptions

Fixes #2452

Author: mtzguido

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})