diff --git a/engine/lib/ast_utils.ml b/engine/lib/ast_utils.ml
index c93339617..9c7f2984e 100644
--- a/engine/lib/ast_utils.ml
+++ b/engine/lib/ast_utils.ml
@@ -367,6 +367,10 @@ module Make (F : Features.T) = struct
                           bounds_impls;
                         };
                   }
+            (* Match scrutinees need to be ascribed as well
+               (see https://github.com/hacspec/hax/issues/1207).*)
+            | Match { scrutinee; arms } ->
+                { e with e = Match { scrutinee = ascribe scrutinee; arms } }
             | _ ->
                 (* Ascribe the return type of a function application & constructors *)
                 if (ascribe_app && is_app e.e) || [%matches? Construct _] e.e
diff --git a/test-harness/src/snapshots/toolchain__cyclic-modules into-fstar.snap b/test-harness/src/snapshots/toolchain__cyclic-modules into-fstar.snap
index 1cb9dc501..d964ad67b 100644
--- a/test-harness/src/snapshots/toolchain__cyclic-modules into-fstar.snap	
+++ b/test-harness/src/snapshots/toolchain__cyclic-modules into-fstar.snap	
@@ -270,22 +270,22 @@ type t_T =
   | T_t2 : t_T
 
 let t_T_cast_to_repr (x: t_T) : isize =
-  match x with
+  match x <: t_T with
   | T_t1  -> isz 0
   | T_t2  -> isz 1
 
 let rec hf (x: t_T) : t_T =
-  match x with
+  match x <: t_T with
   | T_t1  -> hf (T_t2 <: t_T)
   | T_t2  -> x
 
 let rec g1 (x: t_T) : t_T =
-  match x with
+  match x <: t_T with
   | T_t1  -> g2 x
   | T_t2  -> T_t1 <: t_T
 
 and g2 (x: t_T) : t_T =
-  match x with
+  match x <: t_T with
   | T_t1  -> g1 x
   | T_t2  -> hf x
 '''
@@ -325,7 +325,7 @@ type t_T1 = | T1_T1 : t_T1
 
 type t_T = | T_T : t_T1 -> t_T
 
-let t_T1_cast_to_repr (x: t_T1) : isize = match x with | T1_T1  -> isz 0
+let t_T1_cast_to_repr (x: t_T1) : isize = match x <: t_T1 with | T1_T1  -> isz 0
 
 type t_T2 = | T2_T2 : t_T -> t_T2
 
diff --git a/test-harness/src/snapshots/toolchain__enum-repr into-fstar.snap b/test-harness/src/snapshots/toolchain__enum-repr into-fstar.snap
index 600085987..30788080c 100644
--- a/test-harness/src/snapshots/toolchain__enum-repr into-fstar.snap	
+++ b/test-harness/src/snapshots/toolchain__enum-repr into-fstar.snap	
@@ -44,7 +44,7 @@ type t_EnumWithRepr =
   | EnumWithRepr_ImplicitDiscrEmptyStruct : t_EnumWithRepr
 
 let t_EnumWithRepr_cast_to_repr (x: t_EnumWithRepr) : u16 =
-  match x with
+  match x <: t_EnumWithRepr with
   | EnumWithRepr_ExplicitDiscr1  -> discriminant_EnumWithRepr_ExplicitDiscr1
   | EnumWithRepr_ExplicitDiscr2  -> discriminant_EnumWithRepr_ExplicitDiscr2
   | EnumWithRepr_ImplicitDiscrEmptyTuple  -> discriminant_EnumWithRepr_ExplicitDiscr2 +! 1us
diff --git a/test-harness/src/snapshots/toolchain__guards into-fstar.snap b/test-harness/src/snapshots/toolchain__guards into-fstar.snap
index ff12f664a..cf6aebabc 100644
--- a/test-harness/src/snapshots/toolchain__guards into-fstar.snap	
+++ b/test-harness/src/snapshots/toolchain__guards into-fstar.snap	
@@ -33,78 +33,88 @@ open Core
 open FStar.Mul
 
 let equivalent (x: Core.Option.t_Option (Core.Result.t_Result i32 i32)) : i32 =
-  match x with
+  match x <: Core.Option.t_Option (Core.Result.t_Result i32 i32) with
   | Core.Option.Option_None  -> 0l
   | _ ->
     match
-      match x with
-      | Core.Option.Option_Some v ->
-        (match v with
-          | Core.Result.Result_Ok y -> Core.Option.Option_Some y <: Core.Option.t_Option i32
-          | _ -> Core.Option.Option_None <: Core.Option.t_Option i32)
-      | _ -> Core.Option.Option_None <: Core.Option.t_Option i32
+      (match x <: Core.Option.t_Option (Core.Result.t_Result i32 i32) with
+        | Core.Option.Option_Some v ->
+          (match v <: Core.Result.t_Result i32 i32 with
+            | Core.Result.Result_Ok y -> Core.Option.Option_Some y <: Core.Option.t_Option i32
+            | _ -> Core.Option.Option_None <: Core.Option.t_Option i32)
+        | _ -> Core.Option.Option_None <: Core.Option.t_Option i32)
+      <:
+      Core.Option.t_Option i32
     with
     | Core.Option.Option_Some y -> y
     | Core.Option.Option_None  ->
-      match x with
+      match x <: Core.Option.t_Option (Core.Result.t_Result i32 i32) with
       | Core.Option.Option_Some (Core.Result.Result_Err y) -> y
       | _ -> 1l
 
 let if_guard (x: Core.Option.t_Option i32) : i32 =
   match
-    match x with
-    | Core.Option.Option_Some v ->
-      (match v >. 0l with
-        | true -> Core.Option.Option_Some v <: Core.Option.t_Option i32
-        | _ -> Core.Option.Option_None <: Core.Option.t_Option i32)
-    | _ -> Core.Option.Option_None <: Core.Option.t_Option i32
+    (match x <: Core.Option.t_Option i32 with
+      | Core.Option.Option_Some v ->
+        (match v >. 0l <: bool with
+          | true -> Core.Option.Option_Some v <: Core.Option.t_Option i32
+          | _ -> Core.Option.Option_None <: Core.Option.t_Option i32)
+      | _ -> Core.Option.Option_None <: Core.Option.t_Option i32)
+    <:
+    Core.Option.t_Option i32
   with
   | Core.Option.Option_Some x -> x
   | Core.Option.Option_None  -> 0l
 
 let if_let_guard (x: Core.Option.t_Option (Core.Result.t_Result i32 i32)) : i32 =
-  match x with
+  match x <: Core.Option.t_Option (Core.Result.t_Result i32 i32) with
   | Core.Option.Option_None  -> 0l
   | _ ->
     match
-      match x with
-      | Core.Option.Option_Some v ->
-        (match v with
-          | Core.Result.Result_Ok y -> Core.Option.Option_Some y <: Core.Option.t_Option i32
-          | _ -> Core.Option.Option_None <: Core.Option.t_Option i32)
-      | _ -> Core.Option.Option_None <: Core.Option.t_Option i32
+      (match x <: Core.Option.t_Option (Core.Result.t_Result i32 i32) with
+        | Core.Option.Option_Some v ->
+          (match v <: Core.Result.t_Result i32 i32 with
+            | Core.Result.Result_Ok y -> Core.Option.Option_Some y <: Core.Option.t_Option i32
+            | _ -> Core.Option.Option_None <: Core.Option.t_Option i32)
+        | _ -> Core.Option.Option_None <: Core.Option.t_Option i32)
+      <:
+      Core.Option.t_Option i32
     with
     | Core.Option.Option_Some x -> x
     | Core.Option.Option_None  ->
-      match x with
+      match x <: Core.Option.t_Option (Core.Result.t_Result i32 i32) with
       | Core.Option.Option_Some (Core.Result.Result_Err y) -> y
       | _ -> 1l
 
 let multiple_guards (x: Core.Option.t_Option (Core.Result.t_Result i32 i32)) : i32 =
-  match x with
+  match x <: Core.Option.t_Option (Core.Result.t_Result i32 i32) with
   | Core.Option.Option_None  -> 0l
   | _ ->
     match
-      match x with
-      | Core.Option.Option_Some (Core.Result.Result_Ok v) ->
-        (match Core.Option.Option_Some (v +! 1l) <: Core.Option.t_Option i32 with
-          | Core.Option.Option_Some 1l -> Core.Option.Option_Some 0l <: Core.Option.t_Option i32
-          | _ -> Core.Option.Option_None <: Core.Option.t_Option i32)
-      | _ -> Core.Option.Option_None <: Core.Option.t_Option i32
+      (match x <: Core.Option.t_Option (Core.Result.t_Result i32 i32) with
+        | Core.Option.Option_Some (Core.Result.Result_Ok v) ->
+          (match Core.Option.Option_Some (v +! 1l) <: Core.Option.t_Option i32 with
+            | Core.Option.Option_Some 1l -> Core.Option.Option_Some 0l <: Core.Option.t_Option i32
+            | _ -> Core.Option.Option_None <: Core.Option.t_Option i32)
+        | _ -> Core.Option.Option_None <: Core.Option.t_Option i32)
+      <:
+      Core.Option.t_Option i32
     with
     | Core.Option.Option_Some x -> x
     | Core.Option.Option_None  ->
       match
-        match x with
-        | Core.Option.Option_Some v ->
-          (match v with
-            | Core.Result.Result_Ok y -> Core.Option.Option_Some y <: Core.Option.t_Option i32
-            | _ -> Core.Option.Option_None <: Core.Option.t_Option i32)
-        | _ -> Core.Option.Option_None <: Core.Option.t_Option i32
+        (match x <: Core.Option.t_Option (Core.Result.t_Result i32 i32) with
+          | Core.Option.Option_Some v ->
+            (match v <: Core.Result.t_Result i32 i32 with
+              | Core.Result.Result_Ok y -> Core.Option.Option_Some y <: Core.Option.t_Option i32
+              | _ -> Core.Option.Option_None <: Core.Option.t_Option i32)
+          | _ -> Core.Option.Option_None <: Core.Option.t_Option i32)
+        <:
+        Core.Option.t_Option i32
       with
       | Core.Option.Option_Some x -> x
       | Core.Option.Option_None  ->
-        match x with
+        match x <: Core.Option.t_Option (Core.Result.t_Result i32 i32) with
         | Core.Option.Option_Some (Core.Result.Result_Err y) -> y
         | _ -> 1l
 '''
diff --git a/test-harness/src/snapshots/toolchain__let-else into-fstar.snap b/test-harness/src/snapshots/toolchain__let-else into-fstar.snap
index 44ed74878..856375311 100644
--- a/test-harness/src/snapshots/toolchain__let-else into-fstar.snap	
+++ b/test-harness/src/snapshots/toolchain__let-else into-fstar.snap	
@@ -33,12 +33,12 @@ open Core
 open FStar.Mul
 
 let let_else (opt: Core.Option.t_Option u32) : bool =
-  match opt with
+  match opt <: Core.Option.t_Option u32 with
   | Core.Option.Option_Some x -> true
   | _ -> false
 
 let let_else_different_type (opt: Core.Option.t_Option u32) : bool =
-  match opt with
+  match opt <: Core.Option.t_Option u32 with
   | Core.Option.Option_Some x ->
     let_else (Core.Option.Option_Some (x +! 1ul <: u32) <: Core.Option.t_Option u32)
   | _ -> false
diff --git a/test-harness/src/snapshots/toolchain__literals into-fstar.snap b/test-harness/src/snapshots/toolchain__literals into-fstar.snap
index 0ce6219db..355ca6097 100644
--- a/test-harness/src/snapshots/toolchain__literals into-fstar.snap	
+++ b/test-harness/src/snapshots/toolchain__literals into-fstar.snap	
@@ -153,7 +153,7 @@ let numeric (_: Prims.unit) : Prims.unit =
 
 let patterns (_: Prims.unit) : Prims.unit =
   let _:Prims.unit =
-    match 1uy with
+    match 1uy <: u8 with
     | 2uy -> () <: Prims.unit
     | _ -> () <: Prims.unit
   in
diff --git a/test-harness/src/snapshots/toolchain__loops into-fstar.snap b/test-harness/src/snapshots/toolchain__loops into-fstar.snap
index 2c35945ca..9edd883d9 100644
--- a/test-harness/src/snapshots/toolchain__loops into-fstar.snap	
+++ b/test-harness/src/snapshots/toolchain__loops into-fstar.snap	
@@ -71,6 +71,9 @@ let impl__M__decoded_message (self: t_M)
               (Core.Ops.Control_flow.t_ControlFlow
                   (Core.Option.t_Option (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global))
                   (Prims.unit & Prims.unit)) Prims.unit)
+    <:
+    Core.Ops.Control_flow.t_ControlFlow
+      (Core.Option.t_Option (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global)) Prims.unit
   with
   | Core.Ops.Control_flow.ControlFlow_Break ret -> ret
   | Core.Ops.Control_flow.ControlFlow_Continue _ ->
@@ -188,6 +191,8 @@ let double_sum2_return (v: t_Slice i32) : i32 =
             <:
             Core.Ops.Control_flow.t_ControlFlow
               (Core.Ops.Control_flow.t_ControlFlow i32 (Prims.unit & (i32 & i32))) (i32 & i32))
+    <:
+    Core.Ops.Control_flow.t_ControlFlow i32 (i32 & i32)
   with
   | Core.Ops.Control_flow.ControlFlow_Break ret -> ret
   | Core.Ops.Control_flow.ControlFlow_Continue (sum, sum2) -> sum +! sum2
@@ -218,6 +223,8 @@ let double_sum_return (v: t_Slice i32) : i32 =
             <:
             Core.Ops.Control_flow.t_ControlFlow
               (Core.Ops.Control_flow.t_ControlFlow i32 (Prims.unit & i32)) i32)
+    <:
+    Core.Ops.Control_flow.t_ControlFlow i32 i32
   with
   | Core.Ops.Control_flow.ControlFlow_Break ret -> ret
   | Core.Ops.Control_flow.ControlFlow_Continue sum -> sum *! 2l
@@ -314,6 +321,8 @@ let nested_return (_: Prims.unit) : i32 =
             <:
             Core.Ops.Control_flow.t_ControlFlow
               (Core.Ops.Control_flow.t_ControlFlow i32 (Prims.unit & i32)) i32)
+    <:
+    Core.Ops.Control_flow.t_ControlFlow i32 i32
   with
   | Core.Ops.Control_flow.ControlFlow_Break ret -> ret
   | Core.Ops.Control_flow.ControlFlow_Continue sum -> sum *! 2l
diff --git a/test-harness/src/snapshots/toolchain__pattern-or into-fstar.snap b/test-harness/src/snapshots/toolchain__pattern-or into-fstar.snap
index 9fdc477aa..84708e9bd 100644
--- a/test-harness/src/snapshots/toolchain__pattern-or into-fstar.snap	
+++ b/test-harness/src/snapshots/toolchain__pattern-or into-fstar.snap	
@@ -38,14 +38,14 @@ type t_E =
   | E_B : t_E
 
 let t_E_cast_to_repr (x: t_E) : isize =
-  match x with
+  match x <: t_E with
   | E_A  -> isz 0
   | E_B  -> isz 1
 
-let bar (x: t_E) : Prims.unit = match x with | E_A  | E_B  -> () <: Prims.unit
+let bar (x: t_E) : Prims.unit = match x <: t_E with | E_A  | E_B  -> () <: Prims.unit
 
 let deep (x: (i32 & Core.Option.t_Option i32)) : i32 =
-  match x with
+  match x <: (i32 & Core.Option.t_Option i32) with
   | 1l, Core.Option.Option_Some 3l
   | 1l, Core.Option.Option_Some 4l
   | 2l, Core.Option.Option_Some 3l
@@ -53,7 +53,7 @@ let deep (x: (i32 & Core.Option.t_Option i32)) : i32 =
   | x, _ -> x
 
 let deep_capture (x: Core.Result.t_Result (i32 & i32) (i32 & i32)) : i32 =
-  match x with
+  match x <: Core.Result.t_Result (i32 & i32) (i32 & i32) with
   | Core.Result.Result_Ok (1l, x)
   | Core.Result.Result_Ok (2l, x)
   | Core.Result.Result_Err (3l, x)
@@ -61,7 +61,7 @@ let deep_capture (x: Core.Result.t_Result (i32 & i32) (i32 & i32)) : i32 =
   | Core.Result.Result_Ok (x, _) | Core.Result.Result_Err (x, _) -> x
 
 let equivalent (x: (i32 & Core.Option.t_Option i32)) : i32 =
-  match x with
+  match x <: (i32 & Core.Option.t_Option i32) with
   | 1l, Core.Option.Option_Some 3l
   | 1l, Core.Option.Option_Some 4l
   | 2l, Core.Option.Option_Some 3l
@@ -69,7 +69,7 @@ let equivalent (x: (i32 & Core.Option.t_Option i32)) : i32 =
   | x, _ -> x
 
 let nested (x: Core.Option.t_Option i32) : i32 =
-  match x with
+  match x <: Core.Option.t_Option i32 with
   | Core.Option.Option_Some 1l | Core.Option.Option_Some 2l -> 1l
   | Core.Option.Option_Some x -> x
   | Core.Option.Option_None  -> 0l
diff --git a/test-harness/src/snapshots/toolchain__patterns into-fstar.snap b/test-harness/src/snapshots/toolchain__patterns into-fstar.snap
index 77025089e..d3e3cf0f5 100644
--- a/test-harness/src/snapshots/toolchain__patterns into-fstar.snap	
+++ b/test-harness/src/snapshots/toolchain__patterns into-fstar.snap	
@@ -37,5 +37,5 @@ type t_Other = | Other : i32 -> t_Other
 
 type t_Test = | Test_C1 : t_Other -> t_Test
 
-let impl__test (self: t_Test) : i32 = match self with | Test_C1 c -> c._0
+let impl__test (self: t_Test) : i32 = match self <: t_Test with | Test_C1 c -> c._0
 '''
diff --git a/test-harness/src/snapshots/toolchain__reordering into-fstar.snap b/test-harness/src/snapshots/toolchain__reordering into-fstar.snap
index 385642dd2..50d0e39c8 100644
--- a/test-harness/src/snapshots/toolchain__reordering into-fstar.snap	
+++ b/test-harness/src/snapshots/toolchain__reordering into-fstar.snap	
@@ -39,7 +39,7 @@ type t_Foo =
 type t_Bar = | Bar : t_Foo -> t_Bar
 
 let t_Foo_cast_to_repr (x: t_Foo) : isize =
-  match x with
+  match x <: t_Foo with
   | Foo_A  -> isz 0
   | Foo_B  -> isz 1
 
diff --git a/test-harness/src/snapshots/toolchain__side-effects into-fstar.snap b/test-harness/src/snapshots/toolchain__side-effects into-fstar.snap
index a2038278d..66c41f5fa 100644
--- a/test-harness/src/snapshots/toolchain__side-effects into-fstar.snap	
+++ b/test-harness/src/snapshots/toolchain__side-effects into-fstar.snap	
@@ -71,10 +71,12 @@ let test (x y: Core.Option.t_Option i32) : Core.Option.t_Option i32 =
       x
       (fun i ->
           let i:i32 = i in
-          match y with
+          match y <: Core.Option.t_Option i32 with
           | Core.Option.Option_Some hoist1 ->
             Core.Option.Option_Some (i +! hoist1 <: i32) <: Core.Option.t_Option i32
           | Core.Option.Option_None  -> Core.Option.Option_None <: Core.Option.t_Option i32)
+    <:
+    Core.Option.t_Option (Core.Option.t_Option i32)
   with
   | Core.Option.Option_Some some -> some
   | Core.Option.Option_None  -> Core.Option.Option_None <: Core.Option.t_Option i32
@@ -198,14 +200,14 @@ let assign_non_trivial_lhs (foo: t_Foo) : t_Foo =
 /// Question mark without error coercion
 let direct_result_question_mark (y: Core.Result.t_Result Prims.unit u32)
     : Core.Result.t_Result i8 u32 =
-  match y with
+  match y <: Core.Result.t_Result Prims.unit u32 with
   | Core.Result.Result_Ok _ -> Core.Result.Result_Ok 0y <: Core.Result.t_Result i8 u32
   | Core.Result.Result_Err err -> Core.Result.Result_Err err <: Core.Result.t_Result i8 u32
 
 /// Question mark with an error coercion
 let direct_result_question_mark_coercion (y: Core.Result.t_Result i8 u16)
     : Core.Result.t_Result i8 u32 =
-  match y with
+  match y <: Core.Result.t_Result i8 u16 with
   | Core.Result.Result_Ok hoist5 -> Core.Result.Result_Ok hoist5 <: Core.Result.t_Result i8 u32
   | Core.Result.Result_Err err ->
     Core.Result.Result_Err (Core.Convert.f_from #u32 #u16 #FStar.Tactics.Typeclasses.solve err)
@@ -219,7 +221,7 @@ let early_returns (x: u32) : u32 =
   else
     if x >. 30ul
     then
-      match true with
+      match true <: bool with
       | true -> 34ul
       | _ ->
         let x, hoist9:(u32 & u32) = x, 3ul <: (u32 & u32) in
@@ -256,7 +258,7 @@ let local_mutation (x: u32) : u32 =
     Core.Num.impl__u32__wrapping_add x y
   else
     let (x, y), hoist19:((u32 & u32) & u32) =
-      match x with
+      match x <: u32 with
       | 12ul ->
         let y:u32 = Core.Num.impl__u32__wrapping_add x y in
         (x, y <: (u32 & u32)), 3ul <: ((u32 & u32) & u32)
@@ -281,11 +283,11 @@ let monad_lifting (x: u8) : Core.Result.t_Result t_A t_B =
 
 /// Test question mark on `Option`s with some control flow
 let options (x y: Core.Option.t_Option u8) (z: Core.Option.t_Option u64) : Core.Option.t_Option u8 =
-  match x with
+  match x <: Core.Option.t_Option u8 with
   | Core.Option.Option_Some hoist26 ->
     if hoist26 >. 10uy
     then
-      match x with
+      match x <: Core.Option.t_Option u8 with
       | Core.Option.Option_Some hoist28 ->
         (match
             Core.Option.Option_Some (Core.Num.impl__u8__wrapping_add hoist28 3uy)
@@ -293,14 +295,14 @@ let options (x y: Core.Option.t_Option u8) (z: Core.Option.t_Option u64) : Core.
             Core.Option.t_Option u8
           with
           | Core.Option.Option_Some hoist34 ->
-            (match hoist34 with
+            (match hoist34 <: u8 with
               | 3uy ->
                 (match Core.Option.Option_None <: Core.Option.t_Option u8 with
                   | Core.Option.Option_Some some ->
                     let v:u8 = some in
-                    (match x with
+                    (match x <: Core.Option.t_Option u8 with
                       | Core.Option.Option_Some hoist35 ->
-                        (match y with
+                        (match y <: Core.Option.t_Option u8 with
                           | Core.Option.Option_Some hoist36 ->
                             Core.Option.Option_Some
                             (Core.Num.impl__u8__wrapping_add (Core.Num.impl__u8__wrapping_add v
@@ -316,12 +318,12 @@ let options (x y: Core.Option.t_Option u8) (z: Core.Option.t_Option u64) : Core.
                         Core.Option.Option_None <: Core.Option.t_Option u8)
                   | Core.Option.Option_None  -> Core.Option.Option_None <: Core.Option.t_Option u8)
               | 4uy ->
-                (match z with
+                (match z <: Core.Option.t_Option u64 with
                   | Core.Option.Option_Some hoist23 ->
                     let v:u8 = 4uy +! (if hoist23 >. 4uL <: bool then 0uy else 3uy) in
-                    (match x with
+                    (match x <: Core.Option.t_Option u8 with
                       | Core.Option.Option_Some hoist35 ->
-                        (match y with
+                        (match y <: Core.Option.t_Option u8 with
                           | Core.Option.Option_Some hoist36 ->
                             Core.Option.Option_Some
                             (Core.Num.impl__u8__wrapping_add (Core.Num.impl__u8__wrapping_add v
@@ -338,9 +340,9 @@ let options (x y: Core.Option.t_Option u8) (z: Core.Option.t_Option u64) : Core.
                   | Core.Option.Option_None  -> Core.Option.Option_None <: Core.Option.t_Option u8)
               | _ ->
                 let v:u8 = 12uy in
-                match x with
+                match x <: Core.Option.t_Option u8 with
                 | Core.Option.Option_Some hoist35 ->
-                  (match y with
+                  (match y <: Core.Option.t_Option u8 with
                     | Core.Option.Option_Some hoist36 ->
                       Core.Option.Option_Some
                       (Core.Num.impl__u8__wrapping_add (Core.Num.impl__u8__wrapping_add v hoist35
@@ -355,9 +357,9 @@ let options (x y: Core.Option.t_Option u8) (z: Core.Option.t_Option u64) : Core.
           | Core.Option.Option_None  -> Core.Option.Option_None <: Core.Option.t_Option u8)
       | Core.Option.Option_None  -> Core.Option.Option_None <: Core.Option.t_Option u8
     else
-      (match x with
+      (match x <: Core.Option.t_Option u8 with
         | Core.Option.Option_Some hoist31 ->
-          (match y with
+          (match y <: Core.Option.t_Option u8 with
             | Core.Option.Option_Some hoist30 ->
               (match
                   Core.Option.Option_Some (Core.Num.impl__u8__wrapping_add hoist31 hoist30)
@@ -365,14 +367,14 @@ let options (x y: Core.Option.t_Option u8) (z: Core.Option.t_Option u64) : Core.
                   Core.Option.t_Option u8
                 with
                 | Core.Option.Option_Some hoist34 ->
-                  (match hoist34 with
+                  (match hoist34 <: u8 with
                     | 3uy ->
                       (match Core.Option.Option_None <: Core.Option.t_Option u8 with
                         | Core.Option.Option_Some some ->
                           let v:u8 = some in
-                          (match x with
+                          (match x <: Core.Option.t_Option u8 with
                             | Core.Option.Option_Some hoist35 ->
-                              (match y with
+                              (match y <: Core.Option.t_Option u8 with
                                 | Core.Option.Option_Some hoist36 ->
                                   Core.Option.Option_Some
                                   (Core.Num.impl__u8__wrapping_add (Core.Num.impl__u8__wrapping_add v
@@ -389,12 +391,12 @@ let options (x y: Core.Option.t_Option u8) (z: Core.Option.t_Option u64) : Core.
                         | Core.Option.Option_None  ->
                           Core.Option.Option_None <: Core.Option.t_Option u8)
                     | 4uy ->
-                      (match z with
+                      (match z <: Core.Option.t_Option u64 with
                         | Core.Option.Option_Some hoist23 ->
                           let v:u8 = 4uy +! (if hoist23 >. 4uL <: bool then 0uy else 3uy) in
-                          (match x with
+                          (match x <: Core.Option.t_Option u8 with
                             | Core.Option.Option_Some hoist35 ->
-                              (match y with
+                              (match y <: Core.Option.t_Option u8 with
                                 | Core.Option.Option_Some hoist36 ->
                                   Core.Option.Option_Some
                                   (Core.Num.impl__u8__wrapping_add (Core.Num.impl__u8__wrapping_add v
@@ -412,9 +414,9 @@ let options (x y: Core.Option.t_Option u8) (z: Core.Option.t_Option u64) : Core.
                           Core.Option.Option_None <: Core.Option.t_Option u8)
                     | _ ->
                       let v:u8 = 12uy in
-                      match x with
+                      match x <: Core.Option.t_Option u8 with
                       | Core.Option.Option_Some hoist35 ->
-                        (match y with
+                        (match y <: Core.Option.t_Option u8 with
                           | Core.Option.Option_Some hoist36 ->
                             Core.Option.Option_Some
                             (Core.Num.impl__u8__wrapping_add (Core.Num.impl__u8__wrapping_add v
@@ -460,7 +462,7 @@ let question_mark (x: u32) : Core.Result.t_Result u32 u32 =
 let simplifiable_question_mark (c: bool) (x: Core.Option.t_Option i32) : Core.Option.t_Option i32 =
   if c
   then
-    match x with
+    match x <: Core.Option.t_Option i32 with
     | Core.Option.Option_Some hoist40 ->
       let a:i32 = hoist40 +! 10l in
       let b:i32 = 20l in
diff --git a/test-harness/src/snapshots/toolchain__traits into-fstar.snap b/test-harness/src/snapshots/toolchain__traits into-fstar.snap
index 2568c7d3d..3976241ee 100644
--- a/test-harness/src/snapshots/toolchain__traits into-fstar.snap	
+++ b/test-harness/src/snapshots/toolchain__traits into-fstar.snap	
@@ -544,7 +544,7 @@ let impl__Error__for_application_callback (_: Prims.unit) :  Prims.unit -> t_Err
     let _:Prims.unit = temp_0_ in
     Error_Fail <: t_Error
 
-let t_Error_cast_to_repr (x: t_Error) : isize = match x with | Error_Fail  -> isz 0
+let t_Error_cast_to_repr (x: t_Error) : isize = match x <: t_Error with | Error_Fail  -> isz 0
 
 type t_Struct = | Struct : t_Struct
 
diff --git a/test-harness/src/snapshots/toolchain__unsafe into-fstar.snap b/test-harness/src/snapshots/toolchain__unsafe into-fstar.snap
index 310e2d094..4991e948c 100644
--- a/test-harness/src/snapshots/toolchain__unsafe into-fstar.snap	
+++ b/test-harness/src/snapshots/toolchain__unsafe into-fstar.snap	
@@ -35,7 +35,8 @@ open FStar.Mul
 
 type t_Impossible =
 
-let t_Impossible_cast_to_repr (x: t_Impossible) : Rust_primitives.Hax.t_Never = match x with
+let t_Impossible_cast_to_repr (x: t_Impossible) : Rust_primitives.Hax.t_Never =
+  match x <: t_Impossible with
 
 let get_unchecked_example (slice: t_Slice u8)
     : Prims.Pure u8