diff --git a/plugins/ltac2/tac2intern.ml b/plugins/ltac2/tac2intern.ml
index 1b291cd9f71f8..e214e72b56fc8 100644
--- a/plugins/ltac2/tac2intern.ml
+++ b/plugins/ltac2/tac2intern.ml
@@ -1714,7 +1714,7 @@ let debug_globalize_allow_ext ids tac =
 
 let { Goptions.get = typed_notations } =
   Goptions.declare_bool_option_and_ref
-    ~key:["Ltac2";"Typed";"Notations"] ~value:false ()
+    ~key:["Ltac2";"Typed";"Notations"] ~value:true ()
 
 let intern_notation_data ids body =
   if typed_notations () then
diff --git a/test-suite/output/ltac2_check_globalize.out b/test-suite/output/ltac2_check_globalize.out
index cf70cba87c4f8..b5a8f75bbb237 100644
--- a/test-suite/output/ltac2_check_globalize.out
+++ b/test-suite/output/ltac2_check_globalize.out
@@ -4,7 +4,7 @@ fun x => x : 'a -> 'a
 () ()
 (1, 2) 3
 let x := () in x ()
-File "./output/ltac2_check_globalize.v", line 20, characters 32-33:
+File "./output/ltac2_check_globalize.v", line 22, characters 32-33:
 The command has indeed failed with message:
 This expression has type unit. It is not a function and cannot be applied.
 let x := fun x => x in let _ := x 1 in let _ := x "" in ()
@@ -13,11 +13,11 @@ let accu := { contents := []} in
 (let x := fun x => accu.(contents) := (x :: accu.(contents)) in
  let _ := x 1 in let _ := x "" in ());
 accu.(contents)
-File "./output/ltac2_check_globalize.v", line 36, characters 0-144:
+File "./output/ltac2_check_globalize.v", line 38, characters 0-144:
 The command has indeed failed with message:
 This expression has type string but an expression was expected of type 
 int
-let m :=
+let (m : '__α Pattern.goal_matching) :=
   [(([(None, (Pattern.MatchPattern, pat:(_)))],
      (Pattern.MatchPattern, pat:(_))),
     (fun h =>
@@ -27,4 +27,5 @@ let m :=
      (fun _ => fun _ => fun _ => fun _ => fun _ => ()))] : _
     Pattern.goal_matching in
 Pattern.lazy_goal_match0 false m
+:'__α
 constr:(ltac2:(()))
diff --git a/test-suite/output/ltac2_check_globalize.v b/test-suite/output/ltac2_check_globalize.v
index 72ffc0d62f836..cbeea4f065812 100644
--- a/test-suite/output/ltac2_check_globalize.v
+++ b/test-suite/output/ltac2_check_globalize.v
@@ -1,5 +1,7 @@
 Require Import Ltac2.Ltac2.
 
+Unset Ltac2 Typed Notations.
+
 Ltac2 Notation "foo" := ().
 
 Ltac2 Globalize foo.
diff --git a/test-suite/output/ltac2_typed_notations.out b/test-suite/output/ltac2_typed_notations.out
new file mode 100644
index 0000000000000..91c0d870767a2
--- /dev/null
+++ b/test-suite/output/ltac2_typed_notations.out
@@ -0,0 +1,4 @@
+File "./output/ltac2_typed_notations.v", line 5, characters 9-10:
+The command has indeed failed with message:
+This expression has type bool but an expression was expected of type 
+constr
diff --git a/test-suite/output/ltac2_typed_notations.v b/test-suite/output/ltac2_typed_notations.v
new file mode 100644
index 0000000000000..5048223c00eef
--- /dev/null
+++ b/test-suite/output/ltac2_typed_notations.v
@@ -0,0 +1,9 @@
+Require Import Ltac2.Ltac2.
+
+Fail Ltac2 foo(b: bool): bool :=
+  let c := b in
+  match! c with
+  | true => true
+  | false => false
+  end.
+(* error used to be on the whole command *)