diff --git a/tests/test_default/good/mutliple_definitions.catala_en b/tests/test_default/good/mutliple_definitions.catala_en
index 23da3b31..c059d778 100644
--- a/tests/test_default/good/mutliple_definitions.catala_en
+++ b/tests/test_default/good/mutliple_definitions.catala_en
@@ -9,6 +9,42 @@ scope A:
   definition w equals 3
 ```
 
+
+
+```catala-test-inline
+$ catala Typecheck --check_invariants
+[WARNING] These definitions have identical justifications and consequences; is it a mistake?
+
+┌─⯈ tests/test_default/good/mutliple_definitions.catala_en:9.3-9.15:
+└─┐
+9 │   definition w equals 3
+  │   ‾‾‾‾‾‾‾‾‾‾‾‾
+
+┌─⯈ tests/test_default/good/mutliple_definitions.catala_en:6.3-6.15:
+└─┐
+6 │   definition w equals 3
+  │   ‾‾‾‾‾‾‾‾‾‾‾‾
+[RESULT]
+Invariant Dcalc__Invariants.invariant_typing_defaults
+   checked. result: [14/14]
+[RESULT]
+Invariant Dcalc__Invariants.invariant_match_inversion
+   checked. result: [0/0]
+[RESULT]
+Invariant Dcalc__Invariants.invariant_app_inversion
+   checked. result: [0/0]
+[RESULT]
+Invariant Dcalc__Invariants.invariant_no_return_a_function
+   checked. result: [0/0]
+[RESULT]
+Invariant Dcalc__Invariants.invariant_no_partial_evaluation
+   checked. result: [0/0]
+[RESULT]
+Invariant Dcalc__Invariants.invariant_default_no_arrow
+   checked. result: [3/3]
+[RESULT] Typechecking successful!
+```
+
 ```catala-test-inline
 $ catala Interpret -s A
 [WARNING] These definitions have identical justifications and consequences; is it a mistake?
diff --git a/tests/test_exception/good/double_definition.catala_en b/tests/test_exception/good/double_definition.catala_en
index e9203bc5..bf8bf779 100644
--- a/tests/test_exception/good/double_definition.catala_en
+++ b/tests/test_exception/good/double_definition.catala_en
@@ -10,6 +10,44 @@ scope Foo:
 
 ```
 
+
+
+```catala-test-inline
+$ catala Typecheck --check_invariants
+[WARNING] These definitions have identical justifications and consequences; is it a mistake?
+
+┌─⯈ tests/test_exception/good/double_definition.catala_en:9.3-9.15:
+└─┐
+9 │   definition x equals 1
+  │   ‾‾‾‾‾‾‾‾‾‾‾‾
+  └─ Foo
+
+┌─⯈ tests/test_exception/good/double_definition.catala_en:8.3-8.15:
+└─┐
+8 │   definition x equals 1
+  │   ‾‾‾‾‾‾‾‾‾‾‾‾
+  └─ Foo
+[RESULT]
+Invariant Dcalc__Invariants.invariant_typing_defaults
+   checked. result: [14/14]
+[RESULT]
+Invariant Dcalc__Invariants.invariant_match_inversion
+   checked. result: [0/0]
+[RESULT]
+Invariant Dcalc__Invariants.invariant_app_inversion
+   checked. result: [0/0]
+[RESULT]
+Invariant Dcalc__Invariants.invariant_no_return_a_function
+   checked. result: [0/0]
+[RESULT]
+Invariant Dcalc__Invariants.invariant_no_partial_evaluation
+   checked. result: [0/0]
+[RESULT]
+Invariant Dcalc__Invariants.invariant_default_no_arrow
+   checked. result: [3/3]
+[RESULT] Typechecking successful!
+```
+
 ```catala-test-inline
 $ catala Scopelang -s Foo
 [WARNING] These definitions have identical justifications and consequences; is it a mistake?
diff --git a/tests/test_func/good/context_func.catala_en b/tests/test_func/good/context_func.catala_en
index 467b95b5..7e3b5f3d 100644
--- a/tests/test_func/good/context_func.catala_en
+++ b/tests/test_func/good/context_func.catala_en
@@ -15,6 +15,35 @@ scope B:
   definition a.f of x under condition b and x > 0 consequence equals x - 1
 ```
 
+
+
+```catala-test-inline
+$ catala Typecheck --check_invariants
+[ERROR]
+It is impossible to give a definition to a subscope variable not tagged as input or context.
+
+Incriminated subscope:
+┌─⯈ tests/test_func/good/context_func.catala_en:9.3-9.4:
+└─┐
+9 │   a scope A
+  │   ‾
+  └─ Test
+
+Incriminated variable:
+┌─⯈ tests/test_func/good/context_func.catala_en:5.10-5.11:
+└─┐
+5 │   output f content integer depends on x content integer
+  │          ‾
+  └─ Test
+
+Incriminated subscope variable definition:
+┌─⯈ tests/test_func/good/context_func.catala_en:15.3-15.17:
+└──┐
+15 │   definition a.f of x under condition b and x > 0 consequence equals x - 1
+   │   ‾‾‾‾‾‾‾‾‾‾‾‾‾‾
+#return code 123#
+```
+
 ```catala-test-inline
 $ catala Scopelang -s B
 [ERROR]
diff --git a/tests/test_proof/good/enums-arith.catala_en b/tests/test_proof/good/enums-arith.catala_en
index 4fe972ee..e8270e60 100644
--- a/tests/test_proof/good/enums-arith.catala_en
+++ b/tests/test_proof/good/enums-arith.catala_en
@@ -19,6 +19,38 @@ scope A:
   definition x under condition match y with pattern -- A of a: a < 0 -- B of b: true consequence equals 1
 ```
 
+
+
+```catala-test-inline
+$ catala Typecheck --check_invariants
+[WARNING] The constructor "C" of enumeration "T" is never used; maybe it's unnecessary?
+
+┌─⯈ tests/test_proof/good/enums-arith.catala_en:5.7-5.8:
+└─┐
+5 │    -- C content boolean
+  │       ‾
+  └─ Test
+[RESULT]
+Invariant Dcalc__Invariants.invariant_typing_defaults
+   checked. result: [40/40]
+[RESULT]
+Invariant Dcalc__Invariants.invariant_match_inversion
+   checked. result: [2/2]
+[RESULT]
+Invariant Dcalc__Invariants.invariant_app_inversion
+   checked. result: [2/2]
+[RESULT]
+Invariant Dcalc__Invariants.invariant_no_return_a_function
+   checked. result: [4/4]
+[RESULT]
+Invariant Dcalc__Invariants.invariant_no_partial_evaluation
+   checked. result: [2/2]
+[RESULT]
+Invariant Dcalc__Invariants.invariant_default_no_arrow
+   checked. result: [5/5]
+[RESULT] Typechecking successful!
+```
+
 ```catala-test-inline
 $ catala Proof --disable_counterexamples 
 [WARNING] The constructor "C" of enumeration "T" is never used; maybe it's unnecessary?
diff --git a/tests/test_proof/good/enums-nonbool.catala_en b/tests/test_proof/good/enums-nonbool.catala_en
index 227d7d4e..4b7fea61 100644
--- a/tests/test_proof/good/enums-nonbool.catala_en
+++ b/tests/test_proof/good/enums-nonbool.catala_en
@@ -19,6 +19,38 @@ scope A:
   definition x under condition match y with pattern -- A of a: false -- B of b: true consequence equals 1
 ```
 
+
+
+```catala-test-inline
+$ catala Typecheck --check_invariants
+[WARNING] The constructor "C" of enumeration "T" is never used; maybe it's unnecessary?
+
+┌─⯈ tests/test_proof/good/enums-nonbool.catala_en:5.7-5.8:
+└─┐
+5 │    -- C content boolean
+  │       ‾
+  └─ Test
+[RESULT]
+Invariant Dcalc__Invariants.invariant_typing_defaults
+   checked. result: [37/37]
+[RESULT]
+Invariant Dcalc__Invariants.invariant_match_inversion
+   checked. result: [2/2]
+[RESULT]
+Invariant Dcalc__Invariants.invariant_app_inversion
+   checked. result: [1/1]
+[RESULT]
+Invariant Dcalc__Invariants.invariant_no_return_a_function
+   checked. result: [4/4]
+[RESULT]
+Invariant Dcalc__Invariants.invariant_no_partial_evaluation
+   checked. result: [1/1]
+[RESULT]
+Invariant Dcalc__Invariants.invariant_default_no_arrow
+   checked. result: [5/5]
+[RESULT] Typechecking successful!
+```
+
 ```catala-test-inline
 $ catala Proof --disable_counterexamples
 [WARNING] The constructor "C" of enumeration "T" is never used; maybe it's unnecessary?
diff --git a/tests/test_proof/good/enums.catala_en b/tests/test_proof/good/enums.catala_en
index dbd08291..b9be652c 100644
--- a/tests/test_proof/good/enums.catala_en
+++ b/tests/test_proof/good/enums.catala_en
@@ -18,6 +18,38 @@ scope A:
   definition x under condition match y with pattern -- A of a: true -- B of b: false consequence equals 0
   definition x under condition match y with pattern -- A of a: false -- B of b: true consequence equals 1
 ```
+
+
+```catala-test-inline
+$ catala Typecheck --check_invariants
+[WARNING] The constructor "C" of enumeration "T" is never used; maybe it's unnecessary?
+
+┌─⯈ tests/test_proof/good/enums.catala_en:5.7-5.8:
+└─┐
+5 │    -- C content boolean
+  │       ‾
+  └─ Test
+[RESULT]
+Invariant Dcalc__Invariants.invariant_typing_defaults
+   checked. result: [34/34]
+[RESULT]
+Invariant Dcalc__Invariants.invariant_match_inversion
+   checked. result: [2/2]
+[RESULT]
+Invariant Dcalc__Invariants.invariant_app_inversion
+   checked. result: [0/0]
+[RESULT]
+Invariant Dcalc__Invariants.invariant_no_return_a_function
+   checked. result: [4/4]
+[RESULT]
+Invariant Dcalc__Invariants.invariant_no_partial_evaluation
+   checked. result: [0/0]
+[RESULT]
+Invariant Dcalc__Invariants.invariant_default_no_arrow
+   checked. result: [5/5]
+[RESULT] Typechecking successful!
+```
+
 ```catala-test-inline
 $ catala Proof --disable_counterexamples 
 [WARNING] The constructor "C" of enumeration "T" is never used; maybe it's unnecessary?
diff --git a/tests/test_struct/good/ambiguous_fields.catala_en b/tests/test_struct/good/ambiguous_fields.catala_en
index 6254803e..5208690e 100644
--- a/tests/test_struct/good/ambiguous_fields.catala_en
+++ b/tests/test_struct/good/ambiguous_fields.catala_en
@@ -16,6 +16,38 @@ scope A:
   definition y equals x.f
 ```
 
+
+
+```catala-test-inline
+$ catala Typecheck --check_invariants
+[WARNING] The structure "Bar" is never used; maybe it's unnecessary?
+
+┌─⯈ tests/test_struct/good/ambiguous_fields.catala_en:7.23-7.26:
+└─┐
+7 │ declaration structure Bar:
+  │                       ‾‾‾
+  └─ Article
+[RESULT]
+Invariant Dcalc__Invariants.invariant_typing_defaults
+   checked. result: [20/20]
+[RESULT]
+Invariant Dcalc__Invariants.invariant_match_inversion
+   checked. result: [0/0]
+[RESULT]
+Invariant Dcalc__Invariants.invariant_app_inversion
+   checked. result: [0/0]
+[RESULT]
+Invariant Dcalc__Invariants.invariant_no_return_a_function
+   checked. result: [0/0]
+[RESULT]
+Invariant Dcalc__Invariants.invariant_no_partial_evaluation
+   checked. result: [0/0]
+[RESULT]
+Invariant Dcalc__Invariants.invariant_default_no_arrow
+   checked. result: [4/4]
+[RESULT] Typechecking successful!
+```
+
 ```catala-test-inline
 $ catala Interpret -s A
 [WARNING] The structure "Bar" is never used; maybe it's unnecessary?
diff --git a/tests/test_struct/good/same_name_fields.catala_en b/tests/test_struct/good/same_name_fields.catala_en
index 95822f97..4f263f85 100644
--- a/tests/test_struct/good/same_name_fields.catala_en
+++ b/tests/test_struct/good/same_name_fields.catala_en
@@ -16,6 +16,38 @@ scope A:
   definition y equals x.Foo.f
 ```
 
+
+
+```catala-test-inline
+$ catala Typecheck --check_invariants
+[WARNING] The structure "Bar" is never used; maybe it's unnecessary?
+
+┌─⯈ tests/test_struct/good/same_name_fields.catala_en:7.23-7.26:
+└─┐
+7 │ declaration structure Bar:
+  │                       ‾‾‾
+  └─ Article
+[RESULT]
+Invariant Dcalc__Invariants.invariant_typing_defaults
+   checked. result: [39/39]
+[RESULT]
+Invariant Dcalc__Invariants.invariant_match_inversion
+   checked. result: [0/0]
+[RESULT]
+Invariant Dcalc__Invariants.invariant_app_inversion
+   checked. result: [2/2]
+[RESULT]
+Invariant Dcalc__Invariants.invariant_no_return_a_function
+   checked. result: [0/0]
+[RESULT]
+Invariant Dcalc__Invariants.invariant_no_partial_evaluation
+   checked. result: [2/2]
+[RESULT]
+Invariant Dcalc__Invariants.invariant_default_no_arrow
+   checked. result: [6/6]
+[RESULT] Typechecking successful!
+```
+
 ```catala-test-inline
 $ catala Interpret -s A
 [WARNING] The structure "Bar" is never used; maybe it's unnecessary?
diff --git a/tests/test_typing/good/common.catala_en b/tests/test_typing/good/common.catala_en
index b2f764d1..180c255d 100644
--- a/tests/test_typing/good/common.catala_en
+++ b/tests/test_typing/good/common.catala_en
@@ -15,6 +15,61 @@ declaration scope S:
   output a content decimal
 ```
 
+
+
+```catala-test-inline
+$ catala Typecheck --check_invariants
+[WARNING] In scope "S", the variable "z" is declared but never defined; did you forget something?
+
+┌─⯈ tests/test_typing/good/common.catala_en:14.10-14.11:
+└──┐
+14 │   output z content collection Structure
+   │          ‾
+[WARNING] In scope "S", the variable "a" is declared but never defined; did you forget something?
+
+┌─⯈ tests/test_typing/good/common.catala_en:15.10-15.11:
+└──┐
+15 │   output a content decimal
+   │          ‾
+[WARNING] This variable is dead code; it does not contribute to computing any of scope "S" outputs. Did you forget something?
+
+┌─⯈ tests/test_typing/good/common.catala_en:12.9-12.10:
+└──┐
+12 │   input x content integer
+   │         ‾
+[WARNING] The structure "Structure" is never used; maybe it's unnecessary?
+
+┌─⯈ tests/test_typing/good/common.catala_en:7.23-7.32:
+└─┐
+7 │ declaration structure Structure:
+  │                       ‾‾‾‾‾‾‾‾‾
+[WARNING] The enumeration "Enum" is never used; maybe it's unnecessary?
+
+┌─⯈ tests/test_typing/good/common.catala_en:2.25-2.29:
+└─┐
+2 │ declaration enumeration Enum:
+  │                         ‾‾‾‾
+[RESULT]
+Invariant Dcalc__Invariants.invariant_typing_defaults
+   checked. result: [16/16]
+[RESULT]
+Invariant Dcalc__Invariants.invariant_match_inversion
+   checked. result: [0/0]
+[RESULT]
+Invariant Dcalc__Invariants.invariant_app_inversion
+   checked. result: [0/0]
+[RESULT]
+Invariant Dcalc__Invariants.invariant_no_return_a_function
+   checked. result: [0/0]
+[RESULT]
+Invariant Dcalc__Invariants.invariant_no_partial_evaluation
+   checked. result: [0/0]
+[RESULT]
+Invariant Dcalc__Invariants.invariant_default_no_arrow
+   checked. result: [2/2]
+[RESULT] Typechecking successful!
+```
+
 ```catala-test-inline
 $ catala Typecheck --disable_warning
 [RESULT] Typechecking successful!