diff --git a/doc/errors.txt b/doc/errors.txt
index 2b0e1e446..8cf0016bc 100644
--- a/doc/errors.txt
+++ b/doc/errors.txt
@@ -51,6 +51,7 @@ types/2036.txt TC: MightNotTerminate
 types/2037.txt TC: TyFunInLhs
 types/2038.txt TC: DICan'tDerive
 types/2039.txt TC: NotAnIdiom
+types/2040.txt TC: PolyTyFunRhs
 verify/3001.txt Verify: MalformedRecursiveRhs
 verify/3002.txt Verify: DefinedUnused
 verify/3003.txt Verify: ParseErrorInForeign
diff --git a/doc/errors/types/2040.txt b/doc/errors/types/2040.txt
new file mode 100644
index 000000000..bea734b44
--- /dev/null
+++ b/doc/errors/types/2040.txt
@@ -0,0 +1,84 @@
+Type functions with polymorphic (`forall .` or `forall ->`) headed types
+do not play nicely with how the Amulet type checker is implemented
+internally. Thus, using these types in practice might be a bit
+complicated.
+
+    type function foo ('x : bool) begin
+      foo true  = forall 'a. 'a -> 'a
+      foo false = ()
+    end
+
+    type sbool 'x =
+      | STrue  : sbool true
+      | SFalse : sbool false
+
+    let
+      foo :
+        forall 'b. sbool 'b -> foo 'b -> ()
+      =
+        fun x y ->
+          match x with
+          | STrue -> y ()
+          | SFalse -> y
+
+This program certainly looks reasonable, and one might reasonably expect
+it to type-check. But consider what happens when type-checking the
+branch
+
+    | STrue -> y ()
+
+The way type checking Amulet proceeds is by building up a set of
+constraints by walking over the term, then solving them afterwards, to
+support the more complex type system features (like GADTs and type
+functions, both of which are at play here).
+
+When amc sees an application like `y ()`, what it does is (roughly) as
+following:
+
+1. Assign an unknown type `alpha` for y
+2. Since `y` is used in an application, `alpha` must really be equal to
+`beta -> gamma` (for some unknown `beta`, `gamma`)
+3. The argument to `y` is `()`, so `beta` must be equal to `()`
+
+Solving these constraints, we arrive at the type `() -> gamma` for the
+term `y`.
+
+Back to the branch `| STrue -> y ()`, amc will see that `y` is used in a
+function position and infer a type like `alpha -> beta` for it, which is
+wrong. When generating constraints for the branch, amc doesn't yet know
+that `y` has type `forall 'a. 'a -> 'a`; It knows is `y : foo b`
+(from the type signature) and that `b ~ true` (from matching on STrue),
+but it hasn't quite pieced this information together to arrive at
+`y : forall 'a. 'a -> 'a`: that's what the solver does!
+
+A possible fix is to "invert" the pattern matching as follows:
+
+    let
+      foo :
+        forall 'b. sbool 'b -> foo 'b -> ()
+      =
+        function
+          | STrue -> fun (y : forall 'a. 'a -> 'a) -> y ()
+          | SFalse -> fun y -> y
+
+Here, the GADT pattern matching scopes over the function expression
+`fun (y : forall 'a. 'a -> 'a)`, and we can indeed conclude from
+`b ~ true` that `foo b ~ forall 'a. 'a -> 'a`. Thus, `y` enters scope
+with a known polymorphic type, and inference can proceed.
+
+The reason that ascribing a type to `y` in the left-hand side doesn't
+work is that type ascriptions against polymorphic types will make all
+the bound type variables rigid and then check the term against a type
+with no quantifiers. For example:
+
+    (fun x -> x) : forall 'a. 'a -> 'a
+
+What happens is that first we _skolemise_ the type
+`forall 'a. 'a -> 'a`,
+returning a type with a rigid variable instead of `'a` (say `'A`). Then,
+we check the function expression against the type `'A -> 'A`.
+
+You can already see why `(y : forall 'a. 'a -> 'a)` won't work: We
+skolemise the type to `'A -> 'A` and then try unifying
+`forall 'a. 'a -> 'a` (from the expansion of `foo b` with `b ~ true`)
+with `'A -> 'A`, which fails.
diff --git a/doc/make_error_index.sh b/doc/make_error_index.sh
index ba5c058d6..1f03d970c 100755
--- a/doc/make_error_index.sh
+++ b/doc/make_error_index.sh
@@ -30,7 +30,7 @@ cat errors.txt | while read -r file_desc; do
   printf "### E%.4d: \"%s\" {#%s}\n" $num $anchor $anchor >> $out
 
   cat errors/$fname | \
-    sed -re 's/`([ ,.])/`{.amulet}\1/g' \
+    sed -re 's/`([ ,.\):;])/`{.amulet}\1/g' \
     >> $out
 
   echo >> $out
diff --git a/src/Control/Monad/Infer.hs b/src/Control/Monad/Infer.hs
index 9010ce908..b4f68cf2f 100644
--- a/src/Control/Monad/Infer.hs
+++ b/src/Control/Monad/Infer.hs
@@ -161,6 +161,8 @@ data TypeError where
   TyFunInLhs :: SomeReason -> Type Typed -> TypeError
   NotAnIdiom :: Pretty (Var p) => Expr p -> TypeError
 
+  PolyTyFunRhs :: SomeReason -> Type Typed -> TypeError
+
 
 data WhatOverlaps = Overinst | Overeq Bool
 
@@ -580,6 +582,13 @@ instance Pretty TypeError where
   pretty (NotAnIdiom _) =
     vsep [ "This expression can not be used in an idiom bracket because it is not a function application" ]
 
+  pretty (PolyTyFunRhs _ tau) =
+    vsep [ "The right-hand-side of this type function equation is a polymorphic type."
+         , "This is technically unsupported, and might lead to strange type checking failures."
+         , "Offending type:"
+         , indent 2 (displayTypeTyped tau)
+         ]
+
   pretty (WarningError x) = pretty x
 
   pretty (UnsatClassCon _ (ConImplicit _ _ _ t) _) = string "No instance for" <+> pretty t
@@ -615,6 +624,7 @@ instance Spanned TypeError where
   annotation (OrphanInstance x _) = annotation x
   annotation (DIMalformedHead x) = annotation x
   annotation (DICan'tDerive _ x) = annotation x
+  annotation (PolyTyFunRhs x _) = annotation x
   annotation x = error (show (pretty x))
 
 instance Note TypeError Style where
@@ -624,6 +634,7 @@ instance Note TypeError Style where
   diagnosticKind DeadBranch{} = WarningMessage
   diagnosticKind MightNotTerminate{} = WarningMessage
   diagnosticKind AmbiguousType{} = WarningMessage
+  diagnosticKind PolyTyFunRhs{} = WarningMessage
   diagnosticKind WarningError{} = ErrorMessage
   diagnosticKind _ = ErrorMessage
 
@@ -934,6 +945,7 @@ instance Note TypeError Style where
   noteId DIMalformedHead{}    = Just 0008 -- This is a parse error that TC emits
   noteId DICan'tDerive{}      = Just 2038
   noteId NotAnIdiom{}         = Just 2039
+  noteId PolyTyFunRhs{}       = Just 2040
 
   noteId (Note x _) = noteId x
   noteId (Suggestion x _) = noteId x
diff --git a/src/Text/Pretty/Note.hs b/src/Text/Pretty/Note.hs
index ad9b0027f..b1a4faf68 100644
--- a/src/Text/Pretty/Note.hs
+++ b/src/Text/Pretty/Note.hs
@@ -72,12 +72,19 @@ format f x =
             NoteMessage -> annotate (NoteKind NoteMessage) "note"
             WarningMessage -> annotate (NoteKind WarningMessage) "warning"
             ErrorMessage -> annotate (NoteKind ErrorMessage) "error"
-      num = 
+      num =
         case noteId x of
           Just num -> parens (string (printf "%c%.4d" (toUpper (head (show c))) num))
           Nothing -> mempty
+      info =
+        case noteId x of
+          Just num -> (Right <$> formatSpan a <> colon)
+                  <+> string "Use amc explain"
+                  <+> (string (printf "%.4d" num))
+                  <+> string "for more information"
+          Nothing -> empty
       body = formatNote f x
-   in (Right <$> formatSpan a <> colon) <+> (Left <$> (c <+> num)) <##> body
+   in (Right <$> formatSpan a <> colon) <+> (Left <$> (c <+> num)) <##> body <##> info
 
 -- | Convert a note style to an ANSI style
 toAnsi :: NoteStyle -> AnsiStyle
diff --git a/src/Types/Infer/Function.hs b/src/Types/Infer/Function.hs
index 9b5c21189..8c8b40cd5 100644
--- a/src/Types/Infer/Function.hs
+++ b/src/Types/Infer/Function.hs
@@ -33,6 +33,8 @@ checkValidTypeFunction _ _ _ _ equations =
       familyFree (BecauseOf clause) lhs
       checkWildcard clause lhs
       checkWildcard clause rhs
+      when (isSkolemisable rhs) $
+        dictates (PolyTyFunRhs (BecauseOf clause) rhs)
     overlap mempty equations
     terminates equations
     pure ()
diff --git a/tests/amc/path.t b/tests/amc/path.t
index 96df0e3e4..7ed70ff1d 100644
--- a/tests/amc/path.t
+++ b/tests/amc/path.t
@@ -8,6 +8,7 @@ amc compile will extend the compile path
     │ 
   1 │ open import "my_lib.ml"
     │      ^^^^^^^^^^^^^^^^^^
+  tests/amc/files/import.ml[1:6 ..1:23]: Use amc explain 1010 for more information
 
   $ amc compile --lib tests/amc/lib tests/amc/files/import.ml
   do
diff --git a/tests/amc/prelude.t b/tests/amc/prelude.t
index bdd8e8336..55ad6e6a1 100644
--- a/tests/amc/prelude.t
+++ b/tests/amc/prelude.t
@@ -16,6 +16,7 @@ Not using the prelude will fail
     │ 
   1 │ print "Hello"
     │ ^^^^^
+  =stdin[1:1 ..1:5]: Use amc explain 1001 for more information
   > 
 
 One can use a custom prelude
diff --git a/tests/lexer/context/unaligned_let.out b/tests/lexer/context/unaligned_let.out
index 90ed128dd..e6885b425 100644
--- a/tests/lexer/context/unaligned_let.out
+++ b/tests/lexer/context/unaligned_let.out
@@ -14,6 +14,7 @@ $end $end <eof>
     │             ^
   4 │           in x
     │           ^^
+  unaligned_let.ml[4:11 ..4:12]: Use amc explain 0012 for more information
   unaligned_let.ml[7:13 ..7:14]: warning (W0012)
     This `in` is misaligned with the corresponding `let`
     │ 
@@ -21,4 +22,5 @@ $end $end <eof>
     │            ^
   7 │             in x
     │             ^^
+  unaligned_let.ml[7:13 ..7:14]: Use amc explain 0012 for more information
 *)
diff --git a/tests/lexer/fail_escape.out b/tests/lexer/fail_escape.out
index fce447e59..5780a141e 100644
--- a/tests/lexer/fail_escape.out
+++ b/tests/lexer/fail_escape.out
@@ -3,11 +3,13 @@ fail_escape.ml[1:2 ..1:3]: error (E0011)
   │ 
 1 │ "\#  \0 \
   │  ^^
+fail_escape.ml[1:2 ..1:3]: Use amc explain 0011 for more information
 fail_escape.ml[1:6 ..1:7]: error (E0011)
   Unknown escape code.
   │ 
 1 │ "\#  \0 \
   │      ^^
+fail_escape.ml[1:6 ..1:7]: Use amc explain 0011 for more information
 fail_escape.ml[2:1 ..2:1]: error (E0004)
   Unexpected end of input, expecting `"` to close string
   │ 
@@ -15,3 +17,4 @@ fail_escape.ml[2:1 ..2:1]: error (E0004)
   │ ^
 2 │ 
   │ ^
+fail_escape.ml[2:1 ..2:1]: Use amc explain 0004 for more information
diff --git a/tests/lexer/fail_unterminated_comment.out b/tests/lexer/fail_unterminated_comment.out
index 2c16af7ae..54d22a2d1 100644
--- a/tests/lexer/fail_unterminated_comment.out
+++ b/tests/lexer/fail_unterminated_comment.out
@@ -5,3 +5,4 @@ fail_unterminated_comment.ml[7:1 ..7:1]: error (E0005)
   │ ^
 7 │ 
   │ ^
+fail_unterminated_comment.ml[7:1 ..7:1]: Use amc explain 0005 for more information
diff --git a/tests/lexer/fail_unterminated_string.out b/tests/lexer/fail_unterminated_string.out
index 4ca5ad05d..2a01f2674 100644
--- a/tests/lexer/fail_unterminated_string.out
+++ b/tests/lexer/fail_unterminated_string.out
@@ -3,6 +3,7 @@ fail_unterminated_string.ml[1:15 ..1:15]: error (E0004)
   │ 
 1 │ let x = "hello
   │         ^     ^
+fail_unterminated_string.ml[1:15 ..1:15]: Use amc explain 0004 for more information
 fail_unterminated_string.ml[2:1 ..2:1]: error (E0004)
   Unexpected end of input, expecting `"` to close string
   │ 
@@ -10,3 +11,4 @@ fail_unterminated_string.ml[2:1 ..2:1]: error (E0004)
   │         ^
 2 │ 
   │ ^
+fail_unterminated_string.ml[2:1 ..2:1]: Use amc explain 0004 for more information
diff --git a/tests/parser/fail_bind_qualified.out b/tests/parser/fail_bind_qualified.out
index d4e0b7588..29f729a8a 100644
--- a/tests/parser/fail_bind_qualified.out
+++ b/tests/parser/fail_bind_qualified.out
@@ -3,3 +3,4 @@ fail_bind_qualified.ml[1:6 ..1:14]: error (E0010)
   │ 
 1 │ let (`Foo.bar`) = ()
   │      ^^^^^^^^^
+fail_bind_qualified.ml[1:6 ..1:14]: Use amc explain 0010 for more information
diff --git a/tests/parser/fail_do_with.out b/tests/parser/fail_do_with.out
index 50d3fc483..e5ed5a7e1 100644
--- a/tests/parser/fail_do_with.out
+++ b/tests/parser/fail_do_with.out
@@ -4,3 +4,4 @@ fail_do_with.ml[1:10 ..1:20]: error (E0009)
   │ 
 1 │ let () = with x <- 0
   │          ^^^^^^^^^^^
+fail_do_with.ml[1:10 ..1:20]: Use amc explain 0009 for more information
diff --git a/tests/parser/fail_malformed_class_name.out b/tests/parser/fail_malformed_class_name.out
index fb11459af..ce25621d8 100644
--- a/tests/parser/fail_malformed_class_name.out
+++ b/tests/parser/fail_malformed_class_name.out
@@ -3,6 +3,7 @@ fail_malformed_class_name.ml[1:7 ..1:12]: error (E0007)
   │ 
 1 │ class a -> b begin end
   │       ^^^^^^
+fail_malformed_class_name.ml[1:7 ..1:12]: Use amc explain 0007 for more information
 fail_malformed_class_name.ml[3:7 ..3:9]: error (E0007)
   Malformed class declaration beginning with X
 
@@ -12,6 +13,7 @@ fail_malformed_class_name.ml[3:7 ..3:9]: error (E0007)
   │ 
 3 │ class X a begin end
   │       ^^^
+fail_malformed_class_name.ml[3:7 ..3:9]: Use amc explain 0007 for more information
 fail_malformed_class_name.ml[4:7 ..4:11]: error (E0007)
   Malformed class declaration beginning with X
 
@@ -22,6 +24,7 @@ fail_malformed_class_name.ml[4:7 ..4:11]: error (E0007)
   │ 
 4 │ class X a b begin end
   │       ^^^^^
+fail_malformed_class_name.ml[4:7 ..4:11]: Use amc explain 0007 for more information
 fail_malformed_class_name.ml[6:7 ..6:9]: error (E0007)
   Malformed class declaration for x
 
@@ -31,6 +34,7 @@ fail_malformed_class_name.ml[6:7 ..6:9]: error (E0007)
   │ 
 6 │ class x a  begin end
   │       ^^^
+fail_malformed_class_name.ml[6:7 ..6:9]: Use amc explain 0007 for more information
 fail_malformed_class_name.ml[7:7 ..7:11]: error (E0007)
   Malformed class declaration for x
 
@@ -40,3 +44,4 @@ fail_malformed_class_name.ml[7:7 ..7:11]: error (E0007)
   │ 
 7 │ class x a b  begin end
   │       ^^^^^
+fail_malformed_class_name.ml[7:7 ..7:11]: Use amc explain 0007 for more information
diff --git a/tests/parser/fail_malformed_instance.out b/tests/parser/fail_malformed_instance.out
index 6d0f2228b..ca8a669ee 100644
--- a/tests/parser/fail_malformed_instance.out
+++ b/tests/parser/fail_malformed_instance.out
@@ -3,3 +3,4 @@ fail_malformed_instance.ml[1:10 ..1:11]: error (E0008)
   │ 
 1 │ instance 'a begin end
   │          ^^
+fail_malformed_instance.ml[1:10 ..1:11]: Use amc explain 0008 for more information
diff --git a/tests/resolve/fail_import_abandon.out b/tests/resolve/fail_import_abandon.out
index 4c05ccea4..73f4226e1 100644
--- a/tests/resolve/fail_import_abandon.out
+++ b/tests/resolve/fail_import_abandon.out
@@ -5,6 +5,7 @@ fail_import_abandon.ml[6:8 ..6:30]: error (E1010)
   │ 
 6 │   open import "./not_found.ml"
   │        ^^^^^^^^^^^^^^^^^^^^^^^
+fail_import_abandon.ml[6:8 ..6:30]: Use amc explain 1010 for more information
 fail_import_abandon.ml[15:17 ..15:39]: error (E1010)
   Cannot resolve "./not_found.ml"
 
@@ -12,6 +13,7 @@ fail_import_abandon.ml[15:17 ..15:39]: error (E1010)
    │ 
 15 │ module B = open import "./not_found.ml"
    │                 ^^^^^^^^^^^^^^^^^^^^^^^
+fail_import_abandon.ml[15:17 ..15:39]: Use amc explain 1010 for more information
 fail_import_abandon.ml[25:12 ..25:22]: error (E1001)
   Variable not in scope: `not_defined`
 
@@ -19,3 +21,4 @@ fail_import_abandon.ml[25:12 ..25:22]: error (E1001)
    │ 
 25 │   let () = not_defined
    │            ^^^^^^^^^^^
+fail_import_abandon.ml[25:12 ..25:22]: Use amc explain 1001 for more information
diff --git a/tests/resolve/fail_import_loop.out b/tests/resolve/fail_import_loop.out
index d7c89d45d..2e46b6d84 100644
--- a/tests/resolve/fail_import_loop.out
+++ b/tests/resolve/fail_import_loop.out
@@ -14,3 +14,4 @@ tests/resolve/modules/loop_3.ml[1:12 ..1:31]: error (E1011)
 1 │ module M = import "./loop_2.ml"
   │            ^^^^^^^^^^^^^^^^^^^^
   • Note: "tests/resolve/modules/loop_2.ml" imported from "tests/resolve/modules/loop_1.ml"
+tests/resolve/modules/loop_3.ml[1:12 ..1:31]: Use amc explain 1011 for more information
diff --git a/tests/resolve/fail_import_not_found.out b/tests/resolve/fail_import_not_found.out
index 6b5b906b5..a660bf91b 100644
--- a/tests/resolve/fail_import_not_found.out
+++ b/tests/resolve/fail_import_not_found.out
@@ -5,3 +5,4 @@ fail_import_not_found.ml[1:6 ..1:36]: error (E1010)
   │ 
 1 │ open import "./modules/not_found.ml"
   │      ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+fail_import_not_found.ml[1:6 ..1:36]: Use amc explain 1010 for more information
diff --git a/tests/resolve/fail_import_not_found_path.out b/tests/resolve/fail_import_not_found_path.out
index e61f33525..96ba6d3c3 100644
--- a/tests/resolve/fail_import_not_found_path.out
+++ b/tests/resolve/fail_import_not_found_path.out
@@ -5,3 +5,4 @@ fail_import_not_found_path.ml[1:6 ..1:26]: error (E1010)
   │ 
 1 │ open import "not_found.ml"
   │      ^^^^^^^^^^^^^^^^^^^^^
+fail_import_not_found_path.ml[1:6 ..1:26]: Use amc explain 1010 for more information
diff --git a/tests/resolve/fail_let_ambiguity.out b/tests/resolve/fail_let_ambiguity.out
index 69a2888c5..807151f89 100644
--- a/tests/resolve/fail_let_ambiguity.out
+++ b/tests/resolve/fail_let_ambiguity.out
@@ -5,3 +5,4 @@ fail_let_ambiguity.ml[8:18 ..8:18]: error (E1002)
   │ 
 8 │ let main _ = x + y
   │                  ^
+fail_let_ambiguity.ml[8:18 ..8:18]: Use amc explain 1002 for more information
diff --git a/tests/resolve/fail_let_open_struct.out b/tests/resolve/fail_let_open_struct.out
index 3b47bac8c..86e22bacb 100644
--- a/tests/resolve/fail_let_open_struct.out
+++ b/tests/resolve/fail_let_open_struct.out
@@ -5,3 +5,4 @@ fail_let_open_struct.ml[2:3 ..2:33]: error (E1009)
   │ 
 2 │   let open begin type t end in ()
   │   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+fail_let_open_struct.ml[2:3 ..2:33]: Use amc explain 1009 for more information
diff --git a/tests/resolve/fail_modules.out b/tests/resolve/fail_modules.out
index 25a955382..29ce212ca 100644
--- a/tests/resolve/fail_modules.out
+++ b/tests/resolve/fail_modules.out
@@ -5,3 +5,4 @@ fail_modules.ml[4:9 ..4:9]: error (E1001)
   │ 
 4 │ let y = x
   │         ^
+fail_modules.ml[4:9 ..4:9]: Use amc explain 1001 for more information
diff --git a/tests/resolve/fail_non_linear_record.out b/tests/resolve/fail_non_linear_record.out
index 77fffe255..c79c64e5a 100644
--- a/tests/resolve/fail_non_linear_record.out
+++ b/tests/resolve/fail_non_linear_record.out
@@ -4,3 +4,4 @@ fail_non_linear_record.ml[2:3 ..4:10]: error (E1004)
   │ 
 2 │   { x = 0,
   │   ^^^^^^^^
+fail_non_linear_record.ml[2:3 ..4:10]: Use amc explain 1004 for more information
diff --git a/tests/resolve/fail_pattern_ambiguity.out b/tests/resolve/fail_pattern_ambiguity.out
index eeaf5c9ee..da27177aa 100644
--- a/tests/resolve/fail_pattern_ambiguity.out
+++ b/tests/resolve/fail_pattern_ambiguity.out
@@ -5,6 +5,7 @@ fail_pattern_ambiguity.ml[4:3 ..4:8]: error (E1003)
   │ 
 4 │ | (a, a) -> a + a
   │    ^  ^
+fail_pattern_ambiguity.ml[4:3 ..4:8]: Use amc explain 1003 for more information
 fail_pattern_ambiguity.ml[4:13 ..4:13]: error (E1002)
   Ambiguous reference to variable: `a`
 
@@ -12,6 +13,7 @@ fail_pattern_ambiguity.ml[4:13 ..4:13]: error (E1002)
   │ 
 4 │ | (a, a) -> a + a
   │             ^
+fail_pattern_ambiguity.ml[4:13 ..4:13]: Use amc explain 1002 for more information
 fail_pattern_ambiguity.ml[4:17 ..4:17]: error (E1002)
   Ambiguous reference to variable: `a`
 
@@ -19,3 +21,4 @@ fail_pattern_ambiguity.ml[4:17 ..4:17]: error (E1002)
   │ 
 4 │ | (a, a) -> a + a
   │                 ^
+fail_pattern_ambiguity.ml[4:17 ..4:17]: Use amc explain 1002 for more information
diff --git a/tests/resolve/fail_private.out b/tests/resolve/fail_private.out
index 3e84066b7..d217c0b14 100644
--- a/tests/resolve/fail_private.out
+++ b/tests/resolve/fail_private.out
@@ -5,6 +5,7 @@ fail_private.ml[13:10 ..13:34]: error (E1001)
    │ 
 13 │ let () = (X.Y.a + X.b + X.A) : X.c
    │          ^^^^^^^^^^^^^^^^^^^^^^^^^
+fail_private.ml[13:10 ..13:34]: Use amc explain 1001 for more information
 fail_private.ml[13:11 ..13:15]: error (E1001)
   Variable not in scope: `X.Y.a`
 
@@ -12,6 +13,7 @@ fail_private.ml[13:11 ..13:15]: error (E1001)
    │ 
 13 │ let () = (X.Y.a + X.b + X.A) : X.c
    │           ^^^^^
+fail_private.ml[13:11 ..13:15]: Use amc explain 1001 for more information
 fail_private.ml[13:19 ..13:21]: error (E1001)
   Variable not in scope: `X.b`
 
@@ -19,6 +21,7 @@ fail_private.ml[13:19 ..13:21]: error (E1001)
    │ 
 13 │ let () = (X.Y.a + X.b + X.A) : X.c
    │                   ^^^
+fail_private.ml[13:19 ..13:21]: Use amc explain 1001 for more information
 fail_private.ml[13:25 ..13:27]: error (E1001)
   Constructor not in scope: `X.A`
 
@@ -26,6 +29,7 @@ fail_private.ml[13:25 ..13:27]: error (E1001)
    │ 
 13 │ let () = (X.Y.a + X.b + X.A) : X.c
    │                         ^^^
+fail_private.ml[13:25 ..13:27]: Use amc explain 1001 for more information
 fail_private.ml[15:1 ..15:26]: error (E1001)
   Type not in scope: `X.d`
 
@@ -33,6 +37,7 @@ fail_private.ml[15:1 ..15:26]: error (E1001)
    │ 
 15 │ instance X.d int begin end
    │ ^^^^^^^^^^^^^^^^^^^^^^^^^^
+fail_private.ml[15:1 ..15:26]: Use amc explain 1001 for more information
 fail_private.ml[15:1 ..15:26]: error (E1001)
   Type not in scope: `X.d`
 
@@ -40,3 +45,4 @@ fail_private.ml[15:1 ..15:26]: error (E1001)
    │ 
 15 │ instance X.d int begin end
    │ ^^^^^^^^^^^^^^^^^^^^^^^^^^
+fail_private.ml[15:1 ..15:26]: Use amc explain 1001 for more information
diff --git a/tests/resolve/fail_recursive.out b/tests/resolve/fail_recursive.out
index 04d1d2ac9..ec7d01ea0 100644
--- a/tests/resolve/fail_recursive.out
+++ b/tests/resolve/fail_recursive.out
@@ -9,6 +9,7 @@ fail_recursive.ml[5:30 ..5:32]: error (E1001)
   │ 
 3 │ let map f = function
   │     ^^^
+fail_recursive.ml[5:30 ..5:32]: Use amc explain 1001 for more information
 fail_recursive.ml[10:32 ..10:33]: error (E1001)
   Variable not in scope: `go`
 
@@ -20,3 +21,4 @@ fail_recursive.ml[10:32 ..10:33]: error (E1001)
    │ 
  8 │   let go = function
    │   ^^^^^^^^^^^^^^^^^
+fail_recursive.ml[10:32 ..10:33]: Use amc explain 1001 for more information
diff --git a/tests/resolve/fail_unresolved.out b/tests/resolve/fail_unresolved.out
index 1e7289276..62aeba8b4 100644
--- a/tests/resolve/fail_unresolved.out
+++ b/tests/resolve/fail_unresolved.out
@@ -5,6 +5,7 @@ fail_unresolved.ml[6:3 ..6:7]: error (E1001)
   │ 
 6 │   foo_0
   │   ^^^^^
+fail_unresolved.ml[6:3 ..6:7]: Use amc explain 1001 for more information
 fail_unresolved.ml[13:9 ..13:18]: error (E1001)
   Type not in scope: `foo_0`
 
@@ -12,6 +13,7 @@ fail_unresolved.ml[13:9 ..13:18]: error (E1001)
    │ 
 13 │ let _ : foo_0 = ()
    │         ^^^^^^^^^^
+fail_unresolved.ml[13:9 ..13:18]: Use amc explain 1001 for more information
 fail_unresolved.ml[18:9 ..18:12]: error (E1001)
   Constructor not in scope: `Foo0`
 
@@ -19,6 +21,7 @@ fail_unresolved.ml[18:9 ..18:12]: error (E1001)
    │ 
 18 │ let _ = Foo0
    │         ^^^^
+fail_unresolved.ml[18:9 ..18:12]: Use amc explain 1001 for more information
 fail_unresolved.ml[21:9 ..21:54]: error (E1001)
   Type variable not in scope: `foo_0`
 
@@ -26,3 +29,4 @@ fail_unresolved.ml[21:9 ..21:54]: error (E1001)
    │ 
 21 │ let _ : forall 'foo_1 'foo_2 'bar_0. () -> 'foo_0 = ()
    │         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+fail_unresolved.ml[21:9 ..21:54]: Use amc explain 1001 for more information
diff --git a/tests/resolve/fail_unresolved_module.out b/tests/resolve/fail_unresolved_module.out
index e9b2288d7..5780eb214 100644
--- a/tests/resolve/fail_unresolved_module.out
+++ b/tests/resolve/fail_unresolved_module.out
@@ -5,3 +5,4 @@ fail_unresolved_module.ml[8:6 ..8:8]: error (E1001)
   │ 
 8 │ open X.Z
   │      ^^^
+fail_unresolved_module.ml[8:6 ..8:8]: Use amc explain 1001 for more information
diff --git a/tests/resolve/pass_guard.out b/tests/resolve/pass_guard.out
index a685d9a61..7e903a9d1 100644
--- a/tests/resolve/pass_guard.out
+++ b/tests/resolve/pass_guard.out
@@ -5,3 +5,4 @@ pass_guard.ml[4:12 ..4:12]: error (E1001)
   │ 
 4 │ | x when x > 2 -> ()
   │            ^
+pass_guard.ml[4:12 ..4:12]: Use amc explain 1001 for more information
diff --git a/tests/types/begin01.out b/tests/types/begin01.out
index 65fa2940f..fc1aba55b 100644
--- a/tests/types/begin01.out
+++ b/tests/types/begin01.out
@@ -5,3 +5,4 @@ begin01.ml[8:5 ..8:5]: error (E2018)
   │     ^
   • Note: this constraint can not be quantified over
     because it is impossible to quantify over pattern bindings
+begin01.ml[8:5 ..8:5]: Use amc explain 2018 for more information
diff --git a/tests/types/begin04.out b/tests/types/begin04.out
index 600a51827..dddfbc1cb 100644
--- a/tests/types/begin04.out
+++ b/tests/types/begin04.out
@@ -4,3 +4,4 @@ begin04.ml[21:3 ..21:15]: error (E2001)
    │   ^^^^^^^^^^^^^
   Couldn't match actual type list int
     with the type expected by the context, identity 'b
+begin04.ml[21:3 ..21:15]: Use amc explain 2001 for more information
diff --git a/tests/types/begin05.out b/tests/types/begin05.out
index 18242ca9a..3c24e3b84 100644
--- a/tests/types/begin05.out
+++ b/tests/types/begin05.out
@@ -4,6 +4,7 @@ begin05.ml[10:3 ..10:3]: error (E2001)
    │   ^
   Couldn't match actual type int
     with the type expected by the context, identity 'b
+begin05.ml[10:3 ..10:3]: Use amc explain 2001 for more information
 begin05.ml[8:5 ..8:20]: error (E2018)
   No instance for monad identity arising in the binding
   │ 
@@ -11,3 +12,4 @@ begin05.ml[8:5 ..8:20]: error (E2018)
   │     ^^^^^^^^^^^^^^^^
   • Note: this constraint can not be quantified over
     because it is impossible to quantify over pattern bindings
+begin05.ml[8:5 ..8:20]: Use amc explain 2018 for more information
diff --git a/tests/types/class/ambiguous-method.out b/tests/types/class/ambiguous-method.out
index 27e67b160..c6c83dac9 100644
--- a/tests/types/class/ambiguous-method.out
+++ b/tests/types/class/ambiguous-method.out
@@ -5,3 +5,4 @@ ambiguous-method.ml[3:3 ..3:12]: error (E2017)
   Ambiguous type for method y
   • Note: The variable a is bound in the class head
   but doesn't appear in the method type
+ambiguous-method.ml[3:3 ..3:12]: Use amc explain 2017 for more information
diff --git a/tests/types/class/assoc-argl.out b/tests/types/class/assoc-argl.out
index a6d8970c4..b9218f3f6 100644
--- a/tests/types/class/assoc-argl.out
+++ b/tests/types/class/assoc-argl.out
@@ -3,3 +3,4 @@ assoc-argl.ml[6:3 ..6:15]: error (E2024)
 6 │   type bar = ()
   │   ^^^^^^^^^^^^^
   This associated type instance has 0 arguments, but 1 was expected
+assoc-argl.ml[6:3 ..6:15]: Use amc explain 2024 for more information
diff --git a/tests/types/class/assoc-missing.out b/tests/types/class/assoc-missing.out
index cace725d9..6f8be9a8d 100644
--- a/tests/types/class/assoc-missing.out
+++ b/tests/types/class/assoc-missing.out
@@ -3,3 +3,4 @@ assoc-missing.ml[5:1 ..5:26]: error (E2023)
 5 │ instance foo int begin end
   │ ^^^^^^^^^^^^^^^^^^^^^^^^^^
   Missing definition of type family bar in an instance for foo int
+assoc-missing.ml[5:1 ..5:26]: Use amc explain 2023 for more information
diff --git a/tests/types/class/assoc02.out b/tests/types/class/assoc02.out
index 80ac54acc..f500fc52e 100644
--- a/tests/types/class/assoc02.out
+++ b/tests/types/class/assoc02.out
@@ -5,3 +5,4 @@ assoc02.ml[17:22 ..17:23]: error (E2001)
   Couldn't match actual type unit
     with the type expected by the context, int
   • Note: Where bar string ~> int
+assoc02.ml[17:22 ..17:23]: Use amc explain 2001 for more information
diff --git a/tests/types/class/assoc03.out b/tests/types/class/assoc03.out
index c4c119c4f..12c050f2f 100644
--- a/tests/types/class/assoc03.out
+++ b/tests/types/class/assoc03.out
@@ -5,3 +5,4 @@ assoc03.ml[13:16 ..13:17]: error (E2001)
   Couldn't match actual type unit
     with the type expected by the context, string
   • Note: Where bar unit ~> string
+assoc03.ml[13:16 ..13:17]: Use amc explain 2001 for more information
diff --git a/tests/types/class/class02.out b/tests/types/class/class02.out
index ef9aede9b..b542280b0 100644
--- a/tests/types/class/class02.out
+++ b/tests/types/class/class02.out
@@ -6,6 +6,7 @@ class02.ml[3:3 ..3:27]: error (E2001)
     with the type expected by the context, 'k -> 'l
 
   • Did you apply a type constructor to too many arguments?
+class02.ml[3:3 ..3:27]: Use amc explain 2001 for more information
 class02.ml[3:3 ..3:27]: error (E2001)
   │ 
 3 │   val foo : 'a () -> string
@@ -14,3 +15,4 @@ class02.ml[3:3 ..3:27]: error (E2001)
     with the type expected by the context, 'bn -> 'bo
 
   • Did you apply a type constructor to too many arguments?
+class02.ml[3:3 ..3:27]: Use amc explain 2001 for more information
diff --git a/tests/types/class/class05.out b/tests/types/class/class05.out
index 46c943ccc..41414148f 100644
--- a/tests/types/class/class05.out
+++ b/tests/types/class/class05.out
@@ -5,3 +5,4 @@ class05.ml[5:5 ..5:5]: error (E2018)
   │     ^
   • Note: this constraint can not be quantified over
     because it is impossible to quantify over pattern bindings
+class05.ml[5:5 ..5:5]: Use amc explain 2018 for more information
diff --git a/tests/types/class/class06.out b/tests/types/class/class06.out
index 5993cb408..a8587dba1 100644
--- a/tests/types/class/class06.out
+++ b/tests/types/class/class06.out
@@ -3,3 +3,4 @@ class06.ml[6:11 ..6:16]: error (E2018)
   │ 
 6 │   let 0 = foo ()
   │           ^^^^^^
+class06.ml[6:11 ..6:16]: Use amc explain 2018 for more information
diff --git a/tests/types/class/class07.out b/tests/types/class/class07.out
index 4456c4369..4b1d70499 100644
--- a/tests/types/class/class07.out
+++ b/tests/types/class/class07.out
@@ -5,6 +5,7 @@ class07.ml[9:9 ..9:32]: warning (W2015)
   Ambiguous type for value foo:
     show 'a * read 'a * show 'dw => 'dw -> string
   The variable a is ambiguous
+class07.ml[9:9 ..9:32]: Use amc explain 2015 for more information
 class07.ml[9:5 ..9:7]: warning (W2015)
   │ 
 9 │ let foo x = show (read (show x))
@@ -12,3 +13,4 @@ class07.ml[9:5 ..9:7]: warning (W2015)
   Ambiguous type for value foo:
     show 'b * read 'b * show 'a => 'a -> string
   The variable b is ambiguous
+class07.ml[9:5 ..9:7]: Use amc explain 2015 for more information
diff --git a/tests/types/class/default02-fail.out b/tests/types/class/default02-fail.out
index 50c314b17..81054b4e3 100644
--- a/tests/types/class/default02-fail.out
+++ b/tests/types/class/default02-fail.out
@@ -10,3 +10,4 @@ default02-fail.ml[14:8 ..14:15]: error (E2018)
    │ 
 14 │     if x `eq` x then
    │        ^^^^^^^^
+default02-fail.ml[14:8 ..14:15]: Use amc explain 2018 for more information
diff --git a/tests/types/class/fd-coverage.out b/tests/types/class/fd-coverage.out
index a765c5209..3fce58315 100644
--- a/tests/types/class/fd-coverage.out
+++ b/tests/types/class/fd-coverage.out
@@ -9,3 +9,4 @@ fd-coverage.ml[2:1 ..2:35]: error (E2035)
 1 │ class foo 'a 'b | 'a -> 'b begin end
   │                   ^^^^^^^^
   Note: needed because of this functional dependency
+fd-coverage.ml[2:1 ..2:35]: Use amc explain 2035 for more information
diff --git a/tests/types/class/fundep03-fail.out b/tests/types/class/fundep03-fail.out
index 2e9f9050f..3b555a7e1 100644
--- a/tests/types/class/fundep03-fail.out
+++ b/tests/types/class/fundep03-fail.out
@@ -9,3 +9,4 @@ fundep03-fail.ml[36:17 ..36:59]: error (E2018)
 36 │ let onetofive = append (1 :: 2 :: Nil) (3 :: 4 :: 5 :: Nil)
    │                 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
   • Possible fix: add a parameter, or a type signature
+fundep03-fail.ml[36:17 ..36:59]: Use amc explain 2018 for more information
diff --git a/tests/types/class/gadt-instance-fail.out b/tests/types/class/gadt-instance-fail.out
index 9379ab80c..31929604a 100644
--- a/tests/types/class/gadt-instance-fail.out
+++ b/tests/types/class/gadt-instance-fail.out
@@ -6,3 +6,4 @@ gadt-instance-fail.ml[21:18 ..21:30]: warning (W2014)
    │                  ^^^^^^^^^^^^^
   Couldn't match actual type Z
     with the type expected by the context, S 'n
+gadt-instance-fail.ml[21:18 ..21:30]: Use amc explain 2014 for more information
diff --git a/tests/types/class/insufficient-ty-sig.out b/tests/types/class/insufficient-ty-sig.out
index 8103c94b3..cd43f0386 100644
--- a/tests/types/class/insufficient-ty-sig.out
+++ b/tests/types/class/insufficient-ty-sig.out
@@ -3,3 +3,4 @@ insufficient-ty-sig.ml[5:11 ..6:7]: error (E2018)
 6 │   (=.=)
   │    ^^^
   No instance for eq 'a arising from this expression
+insufficient-ty-sig.ml[5:11 ..6:7]: Use amc explain 2018 for more information
diff --git a/tests/types/class/minimal-def.out b/tests/types/class/minimal-def.out
index 6379f27b1..0b8770a23 100644
--- a/tests/types/class/minimal-def.out
+++ b/tests/types/class/minimal-def.out
@@ -5,3 +5,4 @@ minimal-def.ml[21:1 ..21:26]: error (E2022)
   Missing implementation of methods in instance for foo int
   Namely, there must be an implementation for at least
     i, j, either f or g, and one of k, l or m
+minimal-def.ml[21:1 ..21:26]: Use amc explain 2022 for more information
diff --git a/tests/types/class/missing01.out b/tests/types/class/missing01.out
index 1766814e9..870d3dfe7 100644
--- a/tests/types/class/missing01.out
+++ b/tests/types/class/missing01.out
@@ -5,3 +5,4 @@ missing01.ml[5:1 ..5:22]: error (E2022)
   Missing implementation of methods in instance for foo
   Namely, there must be an implementation for at least
     x
+missing01.ml[5:1 ..5:22]: Use amc explain 2022 for more information
diff --git a/tests/types/class/orphan-soundness.out b/tests/types/class/orphan-soundness.out
index dbd756743..df395d9cb 100644
--- a/tests/types/class/orphan-soundness.out
+++ b/tests/types/class/orphan-soundness.out
@@ -3,3 +3,4 @@ orphan-soundness.ml[6:3 ..8:5]: error (E2028)
 6 │   instance foo 'a begin
   │   ^^^^^^^^^^^^^^^^^^^^^
   This instance should be defined in the same module as foo
+orphan-soundness.ml[6:3 ..8:5]: Use amc explain 2028 for more information
diff --git a/tests/types/class/overlap01.out b/tests/types/class/overlap01.out
index 9bf36d61a..a5fccd5ee 100644
--- a/tests/types/class/overlap01.out
+++ b/tests/types/class/overlap01.out
@@ -8,3 +8,4 @@ overlap01.ml[4:1 ..4:38]: error (E2021)
   │ 
 5 │ instance foo () begin let x _ = () end
   │ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+overlap01.ml[4:1 ..4:38]: Use amc explain 2021 for more information
diff --git a/tests/types/class/overlap02.out b/tests/types/class/overlap02.out
index 47073e25d..6b6290bb9 100644
--- a/tests/types/class/overlap02.out
+++ b/tests/types/class/overlap02.out
@@ -8,3 +8,4 @@ overlap02.ml[2:1 ..2:25]: error (E2021)
   │ 
 3 │ instance foo () begin end
   │ ^^^^^^^^^^^^^^^^^^^^^^^^^
+overlap02.ml[2:1 ..2:25]: Use amc explain 2021 for more information
diff --git a/tests/types/class/poly-instance.out b/tests/types/class/poly-instance.out
index 57c2f583a..b0fa8e1c1 100644
--- a/tests/types/class/poly-instance.out
+++ b/tests/types/class/poly-instance.out
@@ -4,3 +4,4 @@ poly-instance.ml[4:1 ..4:38]: error (E2006)
   │ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
   Illegal use of polymorphic type trivial => 'a
     as argument to the type constructor Foo
+poly-instance.ml[4:1 ..4:38]: Use amc explain 2006 for more information
diff --git a/tests/types/class/quantified-cycle.out b/tests/types/class/quantified-cycle.out
index 636851525..0a96efbb0 100644
--- a/tests/types/class/quantified-cycle.out
+++ b/tests/types/class/quantified-cycle.out
@@ -16,3 +16,4 @@ quantified-cycle.ml[12:10 ..12:16]: error (E2019)
         (forall 'a. c (t1 'a)) => c (t2 'a)
       as a solution for the constraint
         c (t2 'a)
+quantified-cycle.ml[12:10 ..12:16]: Use amc explain 2019 for more information
diff --git a/tests/types/class/quantified-eq-loopy.out b/tests/types/class/quantified-eq-loopy.out
index 23deb4fc9..e0ffc3dd6 100644
--- a/tests/types/class/quantified-eq-loopy.out
+++ b/tests/types/class/quantified-eq-loopy.out
@@ -11,3 +11,4 @@ quantified-eq-loopy.ml[3:14 ..3:14]: error (E2009)
 3 │     fun x -> x
   │     ^^^^^^^^^^
   has type forall 'a 'b. ('a ~ 'b => 'a ~ 'b) => 'a -> 'b
+quantified-eq-loopy.ml[3:14 ..3:14]: Use amc explain 2009 for more information
diff --git a/tests/types/class/recursive03.out b/tests/types/class/recursive03.out
index 09608cfec..6b9393d14 100644
--- a/tests/types/class/recursive03.out
+++ b/tests/types/class/recursive03.out
@@ -12,3 +12,4 @@ recursive03.ml[20:9 ..20:27]: error (E2018)
 20 │ let rec foo (x : 'a) : unit =
    │         ^^^^^^^^^^^^^^^^^^^
    This binding should have had a complete type signature.
+recursive03.ml[20:9 ..20:27]: Use amc explain 2018 for more information
diff --git a/tests/types/class/row-cons-fail.out b/tests/types/class/row-cons-fail.out
index 23ca7c5d7..e725a98ad 100644
--- a/tests/types/class/row-cons-fail.out
+++ b/tests/types/class/row-cons-fail.out
@@ -11,3 +11,4 @@ row-cons-fail.ml[1:9 ..1:39]: error (E2018)
                        and exact record { x : int }
   • Note: no fields match
   • The following fields are missing: x
+row-cons-fail.ml[1:9 ..1:39]: Use amc explain 2018 for more information
diff --git a/tests/types/class/tf-not-injective.out b/tests/types/class/tf-not-injective.out
index 4b12c9f1b..c941314ea 100644
--- a/tests/types/class/tf-not-injective.out
+++ b/tests/types/class/tf-not-injective.out
@@ -4,3 +4,4 @@ tf-not-injective.ml[24:5 ..27:48]: error (E2018)
    │                         ^^^^^^^^
   Could not deduce eq_1 (rep 'a) (rep 'b) from the context recursive 'a * recursive 'b * eq_1 (rep 'a) (rep 'b)
   • Note: rep is an associated type, and so may not be injective
+tf-not-injective.ml[24:5 ..27:48]: Use amc explain 2018 for more information
diff --git a/tests/types/class/too-concrete01.out b/tests/types/class/too-concrete01.out
index 051126ff1..472eeb10f 100644
--- a/tests/types/class/too-concrete01.out
+++ b/tests/types/class/too-concrete01.out
@@ -3,3 +3,4 @@ too-concrete01.ml[6:15 ..6:24]: error (E2018)
   │ 
 6 │   fun x -> if x == "foo" then "foo" else "bar"
   │               ^^^^^^^^^^
+too-concrete01.ml[6:15 ..6:24]: Use amc explain 2018 for more information
diff --git a/tests/types/class/toomany01.out b/tests/types/class/toomany01.out
index 0a8f12c29..8cacf1863 100644
--- a/tests/types/class/toomany01.out
+++ b/tests/types/class/toomany01.out
@@ -3,3 +3,4 @@ toomany01.ml[9:7 ..9:9]: error (E2020)
 9 │   let bar = ()
   │       ^^^
   Method bar is not a member of the class foo
+toomany01.ml[9:7 ..9:9]: Use amc explain 2020 for more information
diff --git a/tests/types/class/undecidable-super-class.out b/tests/types/class/undecidable-super-class.out
index 1d00db887..13d4fa112 100644
--- a/tests/types/class/undecidable-super-class.out
+++ b/tests/types/class/undecidable-super-class.out
@@ -4,9 +4,11 @@ undecidable-super-class.ml[1:1 ..1:37]: error (E2027)
   │ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
   Invalid type in context for class declaration:
       'a
+undecidable-super-class.ml[1:1 ..1:37]: Use amc explain 2027 for more information
 undecidable-super-class.ml[1:1 ..1:37]: error (E2027)
   │ 
 1 │ class 'a * 'b => andc 'a 'b begin end
   │ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
   Invalid type in context for class declaration:
       'b
+undecidable-super-class.ml[1:1 ..1:37]: Use amc explain 2027 for more information
diff --git a/tests/types/err01.out b/tests/types/err01.out
index ad57c9808..30004c6b7 100644
--- a/tests/types/err01.out
+++ b/tests/types/err01.out
@@ -4,3 +4,4 @@ err01.ml[10:11 ..10:12]: error (E2001)
    │           ^^
   Couldn't match actual type option (int * int)
     with the type expected by the context, option ((int * int) * 'b)
+err01.ml[10:11 ..10:12]: Use amc explain 2001 for more information
diff --git a/tests/types/fail_guard.out b/tests/types/fail_guard.out
index bc23b2035..16c0cb73a 100644
--- a/tests/types/fail_guard.out
+++ b/tests/types/fail_guard.out
@@ -4,3 +4,4 @@ fail_guard.ml[2:10 ..2:10]: error (E2001)
   │          ^
   Couldn't match actual type int
     with the type expected by the context, bool
+fail_guard.ml[2:10 ..2:10]: Use amc explain 2001 for more information
diff --git a/tests/types/fail_skolem_escape.out b/tests/types/fail_skolem_escape.out
index 6b83bad1b..360bc11c0 100644
--- a/tests/types/fail_skolem_escape.out
+++ b/tests/types/fail_skolem_escape.out
@@ -7,3 +7,4 @@ fail_skolem_escape.ml[2:19 ..2:38]: error (E2008)
           forall 'b. 'b -> 'a,
   • Note: in the inferred type for escape_fail,
       'b
+fail_skolem_escape.ml[2:19 ..2:38]: Use amc explain 2008 for more information
diff --git a/tests/types/fail_skolem_poly.out b/tests/types/fail_skolem_poly.out
index f1e391fb8..fa999af92 100644
--- a/tests/types/fail_skolem_poly.out
+++ b/tests/types/fail_skolem_poly.out
@@ -11,6 +11,7 @@ fail_skolem_poly.ml[3:32 ..3:32]: error (E2009)
 3 │ let poly_fail = poly (fun x -> x + 1)
   │                       ^^^^^^^^^^^^^^
   has type forall 'a. 'a -> 'a
+fail_skolem_poly.ml[3:32 ..3:32]: Use amc explain 2009 for more information
 fail_skolem_poly.ml[3:32 ..3:36]: error (E2009)
   Could not match the rigid type variable 'a with the type int
 
@@ -24,3 +25,4 @@ fail_skolem_poly.ml[3:32 ..3:36]: error (E2009)
 3 │ let poly_fail = poly (fun x -> x + 1)
   │                       ^^^^^^^^^^^^^^
   has type forall 'a. 'a -> 'a
+fail_skolem_poly.ml[3:32 ..3:36]: Use amc explain 2009 for more information
diff --git a/tests/types/fail_skolem_pure.out b/tests/types/fail_skolem_pure.out
index 2be56348d..d8d8e5991 100644
--- a/tests/types/fail_skolem_pure.out
+++ b/tests/types/fail_skolem_pure.out
@@ -11,3 +11,4 @@ fail_skolem_pure.ml[2:32 ..2:32]: error (E2009)
 2 │ let pure_fail = pure (fun x -> x)
   │                       ^^^^^^^^^^
   has type forall 'a. 'a -> 'f 'a
+fail_skolem_pure.ml[2:32 ..2:32]: Use amc explain 2009 for more information
diff --git a/tests/types/fail_value_restriction.out b/tests/types/fail_value_restriction.out
index 0d9459cc6..f72f32619 100644
--- a/tests/types/fail_value_restriction.out
+++ b/tests/types/fail_value_restriction.out
@@ -4,3 +4,4 @@ fail_value_restriction.ml[9:10 ..9:11]: error (E2001)
   │          ^^
   Couldn't match actual type option int
     with the type expected by the context, string
+fail_value_restriction.ml[9:10 ..9:11]: Use amc explain 2001 for more information
diff --git a/tests/types/fail_value_restriction2.out b/tests/types/fail_value_restriction2.out
index f2f4502df..245035498 100644
--- a/tests/types/fail_value_restriction2.out
+++ b/tests/types/fail_value_restriction2.out
@@ -7,3 +7,4 @@ fail_value_restriction2.ml[2:5 ..2:5]: error (E2016)
   • Note: But the variable a needs to be determined
   • Solution: give it a monomorphic type signature. For example:
       unit -> unit
+fail_value_restriction2.ml[2:5 ..2:5]: Use amc explain 2016 for more information
diff --git a/tests/types/gadt/conbox02-fail.out b/tests/types/gadt/conbox02-fail.out
index 90722fed9..95f2ea48b 100644
--- a/tests/types/gadt/conbox02-fail.out
+++ b/tests/types/gadt/conbox02-fail.out
@@ -3,3 +3,4 @@ conbox02-fail.ml[15:28 ..15:32]: error (E2018)
    │ 
 15 │ let xs = [ Box (), Box "", Box 1 ]
    │                            ^^^^^
+conbox02-fail.ml[15:28 ..15:32]: Use amc explain 2018 for more information
diff --git a/tests/types/gadt/dict02-fail.out b/tests/types/gadt/dict02-fail.out
index 9cdbce161..0a4e6cbe8 100644
--- a/tests/types/gadt/dict02-fail.out
+++ b/tests/types/gadt/dict02-fail.out
@@ -4,3 +4,4 @@ dict02-fail.ml[17:25 ..17:26]: error (E2001)
    │                         ^^
   Couldn't match actual type unit
     with the type expected by the context, int
+dict02-fail.ml[17:25 ..17:26]: Use amc explain 2001 for more information
diff --git a/tests/types/gadt/fail_term.out b/tests/types/gadt/fail_term.out
index 27186af7a..2325a5010 100644
--- a/tests/types/gadt/fail_term.out
+++ b/tests/types/gadt/fail_term.out
@@ -4,3 +4,4 @@ fail_term.ml[16:3 ..16:30]: error (E2001)
    │   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^
   Couldn't match actual type 'a -> 'b -> 'b
     with the type expected by the context, 'x -> 'y -> 'x
+fail_term.ml[16:3 ..16:30]: Use amc explain 2001 for more information
diff --git a/tests/types/gadt/fin.out b/tests/types/gadt/fin.out
index 1c515ba68..76041a9db 100644
--- a/tests/types/gadt/fin.out
+++ b/tests/types/gadt/fin.out
@@ -4,3 +4,4 @@ fin.ml[11:14 ..11:18]: error (E2001)
    │              ^^^^^
   Couldn't match actual type 'n
     with the type expected by the context, S (S 'k)
+fin.ml[11:14 ..11:18]: Use amc explain 2001 for more information
diff --git a/tests/types/gadt/gadt01.out b/tests/types/gadt/gadt01.out
index 15360eabb..aaaedb4eb 100644
--- a/tests/types/gadt/gadt01.out
+++ b/tests/types/gadt/gadt01.out
@@ -6,6 +6,7 @@ gadt01.ml[3:1 ..3:23]: error (E2001)
     with the type expected by the context, type
 
   • Did you forget some of the arguments to a type constructor?
+gadt01.ml[3:1 ..3:23]: Use amc explain 2001 for more information
 gadt01.ml[3:16 ..3:23]: error (E2001)
   │ 
 3 │ type gadt 'a = R : gadt
@@ -14,3 +15,4 @@ gadt01.ml[3:16 ..3:23]: error (E2001)
     with the type expected by the context, type
 
   • Did you forget some of the arguments to a type constructor?
+gadt01.ml[3:16 ..3:23]: Use amc explain 2001 for more information
diff --git a/tests/types/gadt/gadt03-fail.out b/tests/types/gadt/gadt03-fail.out
index b7c201954..8eb67c7fe 100644
--- a/tests/types/gadt/gadt03-fail.out
+++ b/tests/types/gadt/gadt03-fail.out
@@ -4,3 +4,4 @@ gadt03-fail.ml[8:12 ..8:19]: error (E2001)
   │            ^^^^^^^^
   Couldn't match actual type bool
     with the type expected by the context, int
+gadt03-fail.ml[8:12 ..8:19]: Use amc explain 2001 for more information
diff --git a/tests/types/gadt/gadt07-escape-fail.out b/tests/types/gadt/gadt07-escape-fail.out
index efbd852ce..4e819c638 100644
--- a/tests/types/gadt/gadt07-escape-fail.out
+++ b/tests/types/gadt/gadt07-escape-fail.out
@@ -4,3 +4,4 @@ gadt07-escape-fail.ml[10:3 ..10:17]: error (E2001)
    │   ^^^^^^^^^^^^^^^
   Couldn't match actual type 'a
     with the type expected by the context, int
+gadt07-escape-fail.ml[10:3 ..10:17]: Use amc explain 2001 for more information
diff --git a/tests/types/holes.out b/tests/types/holes.out
index e5e2b342f..4c0d7dfcb 100644
--- a/tests/types/holes.out
+++ b/tests/types/holes.out
@@ -5,6 +5,7 @@ holes.ml[10:47 ..10:47]: error (E2005)
   Found typed hole _ of type 'a -> 'a || 'b
   • Valid replacements include:
       • fun c -> In1 c
+holes.ml[10:47 ..10:47]: Use amc explain 2005 for more information
 holes.ml[11:47 ..11:47]: error (E2005)
    │ 
 11 │   let or_in2 : forall 'a 'b. 'b -> 'a || 'b = _
@@ -12,6 +13,7 @@ holes.ml[11:47 ..11:47]: error (E2005)
   Found typed hole _ of type 'b -> 'a || 'b
   • Valid replacements include:
       • fun c -> In2 c
+holes.ml[11:47 ..11:47]: Use amc explain 2005 for more information
 holes.ml[13:79 ..13:79]: error (E2005)
    │ 
 13 │   let or_elim : forall 'a 'b 'r. ('a -> 'r) -> ('b -> 'r) -> 'a || 'b -> 'r = _
@@ -21,6 +23,7 @@ holes.ml[13:79 ..13:79]: error (E2005)
       • fun h g -> function
         | (In1 c) -> h c
         | (In2 a) -> g a
+holes.ml[13:79 ..13:79]: Use amc explain 2005 for more information
 holes.ml[15:54 ..15:54]: error (E2005)
    │ 
 15 │   let or_swap : forall 'a 'b. 'a || 'b -> 'b || 'a = _
@@ -30,6 +33,7 @@ holes.ml[15:54 ..15:54]: error (E2005)
       • function
         | (In1 z) -> In2 z
         | (In2 x) -> In1 x
+holes.ml[15:54 ..15:54]: Use amc explain 2005 for more information
 holes.ml[17:53 ..17:53]: error (E2005)
    │ 
 17 │   let and_in : forall 'a 'b. 'a -> 'b -> 'a && 'b = _
@@ -37,6 +41,7 @@ holes.ml[17:53 ..17:53]: error (E2005)
   Found typed hole _ of type 'a -> 'b -> 'a && 'b
   • Valid replacements include:
       • fun y z -> And (y, z)
+holes.ml[17:53 ..17:53]: Use amc explain 2005 for more information
 holes.ml[18:72 ..18:72]: error (E2005)
    │ 
 18 │   let and_elim : forall 'a 'b 'r. 'a && 'b -> ('a -> 'b -> 'r) -> 'r = _
@@ -44,6 +49,7 @@ holes.ml[18:72 ..18:72]: error (E2005)
   Found typed hole _ of type 'a && 'b -> ('a -> 'b -> 'r) -> 'r
   • Valid replacements include:
       • fun (And (y, z)) h -> h y z
+holes.ml[18:72 ..18:72]: Use amc explain 2005 for more information
 holes.ml[20:50 ..20:50]: error (E2005)
    │ 
 20 │   let and_p1 : forall 'a 'b 'r. 'a && 'b -> 'a = _
@@ -51,6 +57,7 @@ holes.ml[20:50 ..20:50]: error (E2005)
   Found typed hole _ of type 'a && 'b -> 'a
   • Valid replacements include:
       • fun (And (c, x)) -> c
+holes.ml[20:50 ..20:50]: Use amc explain 2005 for more information
 holes.ml[21:50 ..21:50]: error (E2005)
    │ 
 21 │   let and_p2 : forall 'a 'b 'r. 'a && 'b -> 'b = _
@@ -58,6 +65,7 @@ holes.ml[21:50 ..21:50]: error (E2005)
   Found typed hole _ of type 'a && 'b -> 'b
   • Valid replacements include:
       • fun (And (a, b)) -> b
+holes.ml[21:50 ..21:50]: Use amc explain 2005 for more information
 holes.ml[23:55 ..23:55]: error (E2005)
    │ 
 23 │   let and_swap : forall 'a 'b. 'a && 'b -> 'b && 'a = _
@@ -65,6 +73,7 @@ holes.ml[23:55 ..23:55]: error (E2005)
   Found typed hole _ of type 'a && 'b -> 'b && 'a
   • Valid replacements include:
       • fun (And (a, b)) -> And (b, a)
+holes.ml[23:55 ..23:55]: Use amc explain 2005 for more information
 holes.ml[25:73 ..25:73]: error (E2005)
    │ 
 25 │   let contrapositive : forall 'p 'q. ('p -> 'q) -> (not 'q -> not 'p) = _
@@ -72,6 +81,7 @@ holes.ml[25:73 ..25:73]: error (E2005)
   Found typed hole _ of type ('p -> 'q) -> not 'q -> not 'p
   • Valid replacements include:
       • fun g (Not h) -> Not (fun c -> h (g c))
+holes.ml[25:73 ..25:73]: Use amc explain 2005 for more information
 holes.ml[26:58 ..26:58]: error (E2005)
    │ 
 26 │   let noncontradiction : forall 'p. not ('p && not 'p) = _
@@ -79,6 +89,7 @@ holes.ml[26:58 ..26:58]: error (E2005)
   Found typed hole _ of type not ('p && not 'p)
   • Valid replacements include:
       • Not (fun (And (y, (Not h))) -> h y)
+holes.ml[26:58 ..26:58]: Use amc explain 2005 for more information
 holes.ml[27:42 ..27:42]: error (E2005)
    │ 
 27 │   let ex_falso : forall 'a. void -> 'a = _
@@ -86,3 +97,4 @@ holes.ml[27:42 ..27:42]: error (E2005)
   Found typed hole _ of type void -> 'a
   • Valid replacements include:
       • function ()
+holes.ml[27:42 ..27:42]: Use amc explain 2005 for more information
diff --git a/tests/types/letgen/letpattern.out b/tests/types/letgen/letpattern.out
index 4a27fb6d3..4c5b60d38 100644
--- a/tests/types/letgen/letpattern.out
+++ b/tests/types/letgen/letpattern.out
@@ -4,3 +4,4 @@ letpattern.ml[1:5 ..1:6]: error (E2001)
   │     ^^
   Couldn't match actual type {  }
     with the type expected by the context, unit
+letpattern.ml[1:5 ..1:6]: Use amc explain 2001 for more information
diff --git a/tests/types/letgen/letrec-01.out b/tests/types/letgen/letrec-01.out
index 8953de871..db3a56128 100644
--- a/tests/types/letgen/letrec-01.out
+++ b/tests/types/letgen/letrec-01.out
@@ -5,3 +5,4 @@ letrec-01.ml[1:9 ..1:14]: error (E2013)
   │ 
 1 │ let rec (a, b) = (a, b)
   │         ^^^^^^
+letrec-01.ml[1:9 ..1:14]: Use amc explain 2013 for more information
diff --git a/tests/types/letgen/letrec-02.out b/tests/types/letgen/letrec-02.out
index 41a7b26ab..f9a92a728 100644
--- a/tests/types/letgen/letrec-02.out
+++ b/tests/types/letgen/letrec-02.out
@@ -12,3 +12,4 @@ letrec-02.ml[1:9 ..1:14]: error (E2013)
   │     ^^^
 3 │ and bar = g
   │     ^^^
+letrec-02.ml[1:9 ..1:14]: Use amc explain 2013 for more information
diff --git a/tests/types/letgen/letrec-03.out b/tests/types/letgen/letrec-03.out
index 6100300a3..e3d62b2ea 100644
--- a/tests/types/letgen/letrec-03.out
+++ b/tests/types/letgen/letrec-03.out
@@ -15,3 +15,4 @@ letrec-03.ml[1:9 ..1:14]: error (E2013)
   │     ^
 4 │ and f = f h
   │     ^
+letrec-03.ml[1:9 ..1:14]: Use amc explain 2013 for more information
diff --git a/tests/types/letgen/local-let02.out b/tests/types/letgen/local-let02.out
index e16180130..a730797c6 100644
--- a/tests/types/letgen/local-let02.out
+++ b/tests/types/letgen/local-let02.out
@@ -4,9 +4,11 @@ local-let02.ml[9:15 ..9:15]: error (E2001)
   │               ^
   Couldn't match actual type int
     with the type expected by the context, string
+local-let02.ml[9:15 ..9:15]: Use amc explain 2001 for more information
 local-let02.ml[9:15 ..9:20]: error (E2001)
   │ 
 9 │   h (fun x -> x ^ "")
   │               ^^^^^^
   Couldn't match actual type string
     with the type expected by the context, int
+local-let02.ml[9:15 ..9:20]: Use amc explain 2001 for more information
diff --git a/tests/types/multi_errs01.out b/tests/types/multi_errs01.out
index 386aec4e7..8d3d127a6 100644
--- a/tests/types/multi_errs01.out
+++ b/tests/types/multi_errs01.out
@@ -4,3 +4,4 @@ multi_errs01.ml[3:19 ..3:22]: error (E2001)
   │                   ^^^^
   Couldn't match actual type bool
     with the type expected by the context, int
+multi_errs01.ml[3:19 ..3:22]: Use amc explain 2001 for more information
diff --git a/tests/types/multi_errs02.out b/tests/types/multi_errs02.out
index bc2ff8309..a4543a7a5 100644
--- a/tests/types/multi_errs02.out
+++ b/tests/types/multi_errs02.out
@@ -4,9 +4,11 @@ multi_errs02.ml[3:19 ..3:22]: error (E2001)
   │                   ^^^^
   Couldn't match actual type bool
     with the type expected by the context, int
+multi_errs02.ml[3:19 ..3:22]: Use amc explain 2001 for more information
 multi_errs02.ml[8:5 ..8:6]: error (E2001)
   │ 
 8 │ let () = "foo"
   │     ^^
   Couldn't match actual type string
     with the type expected by the context, unit
+multi_errs02.ml[8:5 ..8:6]: Use amc explain 2001 for more information
diff --git a/tests/types/multi_errs03.out b/tests/types/multi_errs03.out
index 52fa36c46..93b8a6877 100644
--- a/tests/types/multi_errs03.out
+++ b/tests/types/multi_errs03.out
@@ -4,9 +4,11 @@ multi_errs03.ml[4:19 ..4:22]: error (E2001)
   │                   ^^^^
   Couldn't match actual type bool
     with the type expected by the context, int
+multi_errs03.ml[4:19 ..4:22]: Use amc explain 2001 for more information
 multi_errs03.ml[8:5 ..8:6]: error (E2001)
   │ 
 8 │ and () = "foo"
   │     ^^
   Couldn't match actual type string
     with the type expected by the context, unit
+multi_errs03.ml[8:5 ..8:6]: Use amc explain 2001 for more information
diff --git a/tests/types/nasty_cycle.out b/tests/types/nasty_cycle.out
index 113427df1..92aa5df00 100644
--- a/tests/types/nasty_cycle.out
+++ b/tests/types/nasty_cycle.out
@@ -9,9 +9,11 @@ nasty_cycle.ml[19:25 ..19:25]: error (E2009)
    │ 
 19 │       | Right p -> Left p
    │                         ^
+nasty_cycle.ml[19:25 ..19:25]: Use amc explain 2009 for more information
 nasty_cycle.ml[18:26 ..18:32]: error (E2001)
    │ 
 18 │       | Left p -> Right (Even2 p)
    │                          ^^^^^^^
   Couldn't match actual type S 'n
     with the type expected by the context, S (S 's)
+nasty_cycle.ml[18:26 ..18:32]: Use amc explain 2001 for more information
diff --git a/tests/types/rankn/pattern02.out b/tests/types/rankn/pattern02.out
index f514ec1d6..e9787c2b3 100644
--- a/tests/types/rankn/pattern02.out
+++ b/tests/types/rankn/pattern02.out
@@ -7,6 +7,7 @@ pattern02.ml[4:5 ..4:20]: error (E2008)
           bound by the type of It, forall 'a. 'a * ('a -> int) -> exists,
   • Note: in the inferred type for foo,
       'a
+pattern02.ml[4:5 ..4:20]: Use amc explain 2008 for more information
 pattern02.ml[4:5 ..4:20]: error (E2008)
   │ 
 4 │ let It (foo, finger) = It (1, fun x -> x)
@@ -16,3 +17,4 @@ pattern02.ml[4:5 ..4:20]: error (E2008)
           bound by the type of It, forall 'a. 'a * ('a -> int) -> exists,
   • Note: in the inferred type for finger,
       'a -> int
+pattern02.ml[4:5 ..4:20]: Use amc explain 2008 for more information
diff --git a/tests/types/rankn/ql-impredicative05.out b/tests/types/rankn/ql-impredicative05.out
index c3a76f417..a916d4ea3 100644
--- a/tests/types/rankn/ql-impredicative05.out
+++ b/tests/types/rankn/ql-impredicative05.out
@@ -6,3 +6,4 @@ ql-impredicative05.ml[6:16 ..6:17]: error (E2001)
     with the type expected by the context, forall 'b. 'b -> 'b
 
   • Did you forget some of the arguments to a function?
+ql-impredicative05.ml[6:16 ..6:17]: Use amc explain 2001 for more information
diff --git a/tests/types/rankn/ql-impredicative06.out b/tests/types/rankn/ql-impredicative06.out
index 90225d2ee..1a4209c86 100644
--- a/tests/types/rankn/ql-impredicative06.out
+++ b/tests/types/rankn/ql-impredicative06.out
@@ -6,3 +6,4 @@ ql-impredicative06.ml[10:16 ..10:17]: error (E2001)
     with the type expected by the context, forall 'a. 'a -> 'a
 
   • Did you forget some of the arguments to a function?
+ql-impredicative06.ml[10:16 ..10:17]: Use amc explain 2001 for more information
diff --git a/tests/types/rankn/record02-fail.out b/tests/types/rankn/record02-fail.out
index 56e119420..7cbf53fe1 100644
--- a/tests/types/rankn/record02-fail.out
+++ b/tests/types/rankn/record02-fail.out
@@ -10,3 +10,4 @@ record02-fail.ml[5:17 ..5:36]: error (E2009)
   │ 
 5 │ let foo = Foo { bar = fun x -> x + 1 }
   │                 ^^^^^^^^^^^^^^^^^^^^
+record02-fail.ml[5:17 ..5:36]: Use amc explain 2009 for more information
diff --git a/tests/types/rankn/record04-fail.out b/tests/types/rankn/record04-fail.out
index 04fee8bc9..da5eb8e91 100644
--- a/tests/types/rankn/record04-fail.out
+++ b/tests/types/rankn/record04-fail.out
@@ -4,3 +4,4 @@ record04-fail.ml[3:35 ..3:46]: error (E2001)
   │                                   ^^^^^^^^^^^^
   Couldn't match actual type string
     with the type expected by the context, int
+record04-fail.ml[3:35 ..3:46]: Use amc explain 2001 for more information
diff --git a/tests/types/rankn/req-fail.out b/tests/types/rankn/req-fail.out
index e7560bca2..d5ac726c4 100644
--- a/tests/types/rankn/req-fail.out
+++ b/tests/types/rankn/req-fail.out
@@ -6,3 +6,4 @@ req-fail.ml[3:5 ..3:5]: error (E2001)
     with the type expected by the context, int -> 'm
 
   • Did you apply a function to too many arguments?
+req-fail.ml[3:5 ..3:5]: Use amc explain 2001 for more information
diff --git a/tests/types/rankn/tuple02-fail.out b/tests/types/rankn/tuple02-fail.out
index cab63f626..c1c51a98d 100644
--- a/tests/types/rankn/tuple02-fail.out
+++ b/tests/types/rankn/tuple02-fail.out
@@ -10,3 +10,4 @@ tuple02-fail.ml[1:42 ..1:52]: error (E2009)
   │ 
 1 │ let foo : (forall 'a. 'a -> 'a) * int = (fun 0 -> (), 1)
   │                                          ^^^^^^^^^^^
+tuple02-fail.ml[1:42 ..1:52]: Use amc explain 2009 for more information
diff --git a/tests/types/scope.out b/tests/types/scope.out
index 3f6bd096c..113beedf5 100644
--- a/tests/types/scope.out
+++ b/tests/types/scope.out
@@ -4,21 +4,25 @@ scope.ml[10:11 ..10:13]: error (E2001)
    │           ^^^
   Couldn't match actual type X.t
     with the type expected by the context, int
+scope.ml[10:11 ..10:13]: Use amc explain 2001 for more information
 scope.ml[14:5 ..14:5]: error (E2001)
    │ 
 14 │     x + 1
    │     ^
   Couldn't match actual type t
     with the type expected by the context, int
+scope.ml[14:5 ..14:5]: Use amc explain 2001 for more information
 scope.ml[15:15 ..15:15]: error (E2001)
    │ 
 15 │   let _ = X.( x + 1 )
    │               ^
   Couldn't match actual type t
     with the type expected by the context, int
+scope.ml[15:15 ..15:15]: Use amc explain 2001 for more information
 scope.ml[18:11 ..18:13]: error (E2001)
    │ 
 18 │   let _ = X.x + 1
    │           ^^^
   Couldn't match actual type X.t
     with the type expected by the context, int
+scope.ml[18:11 ..18:13]: Use amc explain 2001 for more information
diff --git a/tests/types/synonym/syn05.out b/tests/types/synonym/syn05.out
index ae47e946a..28acf649d 100644
--- a/tests/types/synonym/syn05.out
+++ b/tests/types/synonym/syn05.out
@@ -4,3 +4,4 @@ syn05.ml[4:1 ..4:24]: error (E2034)
   │ ^^^^^^^^^^^^^^^^^^^^^^^^
   Type synonym foo appears with no arguments,
   but in its definition it has 1
+syn05.ml[4:1 ..4:24]: Use amc explain 2034 for more information
diff --git a/tests/types/synonym/syn07.out b/tests/types/synonym/syn07.out
index 71194ee29..c02724890 100644
--- a/tests/types/synonym/syn07.out
+++ b/tests/types/synonym/syn07.out
@@ -4,3 +4,4 @@ syn07.ml[4:1 ..4:24]: error (E2034)
   │ ^^^^^^^^^^^^^^^^^^^^^^^^
   Type synonym foo appears with no arguments,
   but in its definition it has 1
+syn07.ml[4:1 ..4:24]: Use amc explain 2034 for more information
diff --git a/tests/types/synonym/syn08.out b/tests/types/synonym/syn08.out
index 9b86e63f1..fe8dc6ff5 100644
--- a/tests/types/synonym/syn08.out
+++ b/tests/types/synonym/syn08.out
@@ -4,3 +4,4 @@ syn08.ml[4:1 ..4:30]: error (E2034)
   │ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
   Type synonym foo appears with one argument,
   but in its definition it has 2
+syn08.ml[4:1 ..4:30]: Use amc explain 2034 for more information
diff --git a/tests/types/tyfun-err01.out b/tests/types/tyfun-err01.out
index febef3637..6b8911dd1 100644
--- a/tests/types/tyfun-err01.out
+++ b/tests/types/tyfun-err01.out
@@ -3,3 +3,4 @@ tyfun-err01.ml[9:22 ..9:23]: error (E2003)
 9 │ let foo : foo bool = ()
   │                      ^^
   Unexpected argument to foo: bool
+tyfun-err01.ml[9:22 ..9:23]: Use amc explain 2003 for more information
diff --git a/tests/types/tyfun-err02.out b/tests/types/tyfun-err02.out
index a1ba96ad8..a778d8141 100644
--- a/tests/types/tyfun-err02.out
+++ b/tests/types/tyfun-err02.out
@@ -3,3 +3,4 @@ tyfun-err02.ml[15:9 ..15:29]: error (E2003)
 15 │ let _ = show (fun x -> x + 1)
    │         ^^^^^^^^^^^^^^^^^^^^^
   Can't show functional type int -> int
+tyfun-err02.ml[15:9 ..15:29]: Use amc explain 2003 for more information
diff --git a/tests/types/tyfun/big-error.out b/tests/types/tyfun/big-error.out
index 53ca05ea4..84c3927e1 100644
--- a/tests/types/tyfun/big-error.out
+++ b/tests/types/tyfun/big-error.out
@@ -14,3 +14,4 @@ big-error.ml[12:58 ..12:61]: error (E2001)
         S (S (S (S Z))),
       is the reduction of
         length [1, 2, 3, 4]
+big-error.ml[12:58 ..12:61]: Use amc explain 2001 for more information
diff --git a/tests/types/tyfun/class-total.out b/tests/types/tyfun/class-total.out
index a261e1a68..e7f13e7f1 100644
--- a/tests/types/tyfun/class-total.out
+++ b/tests/types/tyfun/class-total.out
@@ -3,3 +3,4 @@ class-total.ml[6:3 ..6:27]: error (E2036)
 6 │   type loop_t = list loop_t
   │   ^^^^^^^^^^^^^^^^^^^^^^^^^
   Recursive call loop_t --> loop_t might not terminate
+class-total.ml[6:3 ..6:27]: Use amc explain 2036 for more information
diff --git a/tests/types/tyfun/constrained02-fail.out b/tests/types/tyfun/constrained02-fail.out
index ffe5fee94..ff6d254e2 100644
--- a/tests/types/tyfun/constrained02-fail.out
+++ b/tests/types/tyfun/constrained02-fail.out
@@ -3,3 +3,4 @@ constrained02-fail.ml[12:21 ..12:33]: error (E2018)
    │ 
 12 │ let foo x = fst (x, bot : f2 bool)
    │                     ^^^^^^^^^^^^^
+constrained02-fail.ml[12:21 ..12:33]: Use amc explain 2018 for more information
diff --git a/tests/types/tyfun/constrained02.out b/tests/types/tyfun/constrained02.out
index 87e9f4766..640379250 100644
--- a/tests/types/tyfun/constrained02.out
+++ b/tests/types/tyfun/constrained02.out
@@ -3,3 +3,4 @@ constrained02.ml[6:5 ..6:32]: error (E2018)
 6 │   | MkBox : bar 'a -> bar_box 'a
   │     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^
   Could not deduce foo 'a from the context given in the type bar 'a -> bar_box 'a
+constrained02.ml[6:5 ..6:32]: Use amc explain 2018 for more information
diff --git a/tests/types/tyfun/constrained03.out b/tests/types/tyfun/constrained03.out
index ecf63820f..4eadb79e5 100644
--- a/tests/types/tyfun/constrained03.out
+++ b/tests/types/tyfun/constrained03.out
@@ -3,3 +3,4 @@ constrained03.ml[9:1 ..11:3]: error (E2018)
 10 │   val foo : 'a -> f2 'a
    │   ^^^^^^^^^^^^^^^^^^^^^
   No instance for c2 'a arising from the method signature
+constrained03.ml[9:1 ..11:3]: Use amc explain 2018 for more information
diff --git a/tests/types/tyfun/constrained04.out b/tests/types/tyfun/constrained04.out
index dff904a87..b3c3e96e0 100644
--- a/tests/types/tyfun/constrained04.out
+++ b/tests/types/tyfun/constrained04.out
@@ -11,3 +11,4 @@ constrained04.ml[10:3 ..10:17]: error (E2018)
    │ 
 10 │   type f2 = f2 'a
    │   ^^^^^^^^^^^^^^^
+constrained04.ml[10:3 ..10:17]: Use amc explain 2018 for more information
diff --git a/tests/types/tyfun/constrained05.out b/tests/types/tyfun/constrained05.out
index 5f067e798..18a5edf16 100644
--- a/tests/types/tyfun/constrained05.out
+++ b/tests/types/tyfun/constrained05.out
@@ -3,3 +3,4 @@ constrained05.ml[9:15 ..9:26]: error (E2018)
 9 │ type foo 'a = Foo of f2 'a
   │               ^^^^^^^^^^^^
   Could not deduce c2 'a from the context given in the type f2 'a
+constrained05.ml[9:15 ..9:26]: Use amc explain 2018 for more information
diff --git a/tests/types/tyfun/error01.out b/tests/types/tyfun/error01.out
index 119e2ca40..0906c54c5 100644
--- a/tests/types/tyfun/error01.out
+++ b/tests/types/tyfun/error01.out
@@ -3,3 +3,4 @@ error01.ml[6:5 ..6:6]: error (E2003)
 6 │ let () = foo ()
   │     ^^
   foo
+error01.ml[6:5 ..6:6]: Use amc explain 2003 for more information
diff --git a/tests/types/tyfun/error02.out b/tests/types/tyfun/error02.out
index 9e5277395..77e4070ff 100644
--- a/tests/types/tyfun/error02.out
+++ b/tests/types/tyfun/error02.out
@@ -3,3 +3,4 @@ error02.ml[4:5 ..4:6]: error (E2003)
 4 │ let () = foo ()
   │     ^^
   Stuck type expression in Amc.type_error: foo int
+error02.ml[4:5 ..4:6]: Use amc explain 2003 for more information
diff --git a/tests/types/tyfun/lhs.out b/tests/types/tyfun/lhs.out
index 489aa16f2..b83e53138 100644
--- a/tests/types/tyfun/lhs.out
+++ b/tests/types/tyfun/lhs.out
@@ -3,3 +3,4 @@ lhs.ml[3:3 ..3:24]: error (E2037)
 3 │   bar (foo int) = string
   │   ^^^^^^^^^^^^^^^^^^^^^^
   Type synonym application foo int is illegal in LHS of type function equation
+lhs.ml[3:3 ..3:24]: Use amc explain 2037 for more information
diff --git a/tests/types/tyfun/overlap.out b/tests/types/tyfun/overlap.out
index eeda44a66..9f4192b4b 100644
--- a/tests/types/tyfun/overlap.out
+++ b/tests/types/tyfun/overlap.out
@@ -8,3 +8,4 @@ overlap.ml[2:3 ..2:18]: error (E2021)
   │ 
 3 │   foo int = bool
   │   ^^^^^^^^^^^^^^
+overlap.ml[2:3 ..2:18]: Use amc explain 2021 for more information
diff --git a/tests/types/tyfun/rec.out b/tests/types/tyfun/rec.out
index ee088e154..67e98d3b9 100644
--- a/tests/types/tyfun/rec.out
+++ b/tests/types/tyfun/rec.out
@@ -3,3 +3,4 @@ rec.ml[2:3 ..2:24]: warning (W2036)
 2 │   foo 'a = foo (list 'a)
   │   ^^^^^^^^^^^^^^^^^^^^^^
   Recursive call foo 'a --> foo (list 'a) might not terminate
+rec.ml[2:3 ..2:24]: Use amc explain 2036 for more information
diff --git a/tests/types/tyfun/soundness.out b/tests/types/tyfun/soundness.out
index 6e30663d7..a9a12e33b 100644
--- a/tests/types/tyfun/soundness.out
+++ b/tests/types/tyfun/soundness.out
@@ -3,3 +3,4 @@ soundness.ml[22:5 ..22:58]: error (E2018)
 22 │ let no : forall 'a 'b. trivial :- (discrim 'a 'b ~ string) = Sub (fun _ -> Dict)
    │                                                                            ^^^^
   No instance for discrim 'a 'b ~ string arising from this expression
+soundness.ml[22:5 ..22:58]: Use amc explain 2018 for more information
diff --git a/tests/types/tyfun/tyfun-apart.out b/tests/types/tyfun/tyfun-apart.out
index d76bc3796..5c9652652 100644
--- a/tests/types/tyfun/tyfun-apart.out
+++ b/tests/types/tyfun/tyfun-apart.out
@@ -3,3 +3,4 @@ tyfun-apart.ml[13:5 ..13:58]: error (E2018)
 13 │ let no : forall 'a 'b. trivial :- (discrim 'a 'b ~ string) = Sub (fun _ -> Dict)
    │                                                                            ^^^^
   No instance for discrim 'a 'b ~ string arising from this expression
+tyfun-apart.ml[13:5 ..13:58]: Use amc explain 2018 for more information
diff --git a/tests/types/tyfun/tyfun-arity.out b/tests/types/tyfun/tyfun-arity.out
index bfa71fe96..5b7df0141 100644
--- a/tests/types/tyfun/tyfun-arity.out
+++ b/tests/types/tyfun/tyfun-arity.out
@@ -4,3 +4,4 @@ tyfun-arity.ml[3:5 ..3:15]: error (E2034)
   │     ^^^^^^^^^^^
   Type function f appears with one argument,
   but in its definition it has 2
+tyfun-arity.ml[3:5 ..3:15]: Use amc explain 2034 for more information
diff --git a/tests/types/tyfun/tyfun-instance.out b/tests/types/tyfun/tyfun-instance.out
index c7e77436d..5591f2504 100644
--- a/tests/types/tyfun/tyfun-instance.out
+++ b/tests/types/tyfun/tyfun-instance.out
@@ -4,3 +4,4 @@ tyfun-instance.ml[7:1 ..7:26]: error (E2034)
   │ ^^^^^^^^^^^^^^^^^^^^^^^^^^
   Type function foo appears with no arguments,
   but in its definition it has 1
+tyfun-instance.ml[7:1 ..7:26]: Use amc explain 2034 for more information
diff --git a/tests/types/tyfun/tyfun-pi-fail.out b/tests/types/tyfun/tyfun-pi-fail.out
index c96506070..7adabf94e 100644
--- a/tests/types/tyfun/tyfun-pi-fail.out
+++ b/tests/types/tyfun/tyfun-pi-fail.out
@@ -4,3 +4,4 @@ tyfun-pi-fail.ml[8:3 ..8:52]: error (E2001)
   │   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
   Couldn't match actual type Z
     with the type expected by the context, S Z
+tyfun-pi-fail.ml[8:3 ..8:52]: Use amc explain 2001 for more information
diff --git a/tests/types/tyfun/tyfun-terminate.out b/tests/types/tyfun/tyfun-terminate.out
index 4cbb7432c..6265be377 100644
--- a/tests/types/tyfun/tyfun-terminate.out
+++ b/tests/types/tyfun/tyfun-terminate.out
@@ -1,30 +1,54 @@
+tyfun-terminate.ml[6:3 ..6:63]: warning (W2040)
+  │ 
+6 │   really_recursive C      = forall 'a. really_recursive C -> 'a
+  │   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+  The right-hand-side of this type function equation is a polymorphic type.
+  This is technically unsupported, and might lead to strange type checking failures.
+  Offending type:
+    forall 'a. really_recursive C -> 'a
+tyfun-terminate.ml[6:3 ..6:63]: Use amc explain 2040 for more information
+tyfun-terminate.ml[7:3 ..7:57]: warning (W2040)
+  │ 
+7 │   really_recursive (D 'c) = 'c => really_recursive (D 'c)
+  │   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+  The right-hand-side of this type function equation is a polymorphic type.
+  This is technically unsupported, and might lead to strange type checking failures.
+  Offending type:
+    'c => really_recursive (D 'c)
+tyfun-terminate.ml[7:3 ..7:57]: Use amc explain 2040 for more information
 tyfun-terminate.ml[4:3 ..4:69]: warning (W2036)
   │ 
 4 │   really_recursive A      = (really_recursive A * really_recursive A)
   │   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
   Recursive call really_recursive A --> really_recursive A might not terminate
+tyfun-terminate.ml[4:3 ..4:69]: Use amc explain 2036 for more information
 tyfun-terminate.ml[5:3 ..5:52]: warning (W2036)
   │ 
 5 │   really_recursive B      = really_recursive B -> ()
   │   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
   Recursive call really_recursive B --> really_recursive B might not terminate
+tyfun-terminate.ml[5:3 ..5:52]: Use amc explain 2036 for more information
 tyfun-terminate.ml[6:3 ..6:63]: warning (W2036)
   │ 
 6 │   really_recursive C      = forall 'a. really_recursive C -> 'a
   │   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
   Recursive call really_recursive C --> really_recursive C might not terminate
+tyfun-terminate.ml[6:3 ..6:63]: Use amc explain 2036 for more information
 tyfun-terminate.ml[7:3 ..7:57]: warning (W2036)
   │ 
 7 │   really_recursive (D 'c) = 'c => really_recursive (D 'c)
   │   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
   Recursive call really_recursive (D 'c) --> really_recursive (D 'c) might not terminate
+tyfun-terminate.ml[7:3 ..7:57]: Use amc explain 2036 for more information
 tyfun-terminate.ml[8:3 ..8:54]: warning (W2036)
   │ 
 8 │   really_recursive E      = { x : really_recursive E }
   │   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
   Recursive call really_recursive E --> really_recursive E might not terminate
+tyfun-terminate.ml[8:3 ..8:54]: Use amc explain 2036 for more information
 tyfun-terminate.ml[9:3 ..9:64]: warning (W2036)
   │ 
 9 │   really_recursive (F 'a) = { 'a | x : really_recursive (F 'a) }
   │   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
   Recursive call really_recursive (F 'a) --> really_recursive (F 'a) might not terminate
+tyfun-terminate.ml[9:3 ..9:64]: Use amc explain 2036 for more information
diff --git a/tests/types/tyfun/tyfun02-fail.out b/tests/types/tyfun/tyfun02-fail.out
index 96a64b289..f55fb3b34 100644
--- a/tests/types/tyfun/tyfun02-fail.out
+++ b/tests/types/tyfun/tyfun02-fail.out
@@ -3,3 +3,4 @@ tyfun02-fail.ml[11:5 ..11:49]: error (E2018)
 14 │   | _ -> Xs
    │          ^^
   No instance for collapse 'a ~ string arising from the expression
+tyfun02-fail.ml[11:5 ..11:49]: Use amc explain 2018 for more information
diff --git a/tests/types/typeable-fail.out b/tests/types/typeable-fail.out
index e88d73271..55ad104d3 100644
--- a/tests/types/typeable-fail.out
+++ b/tests/types/typeable-fail.out
@@ -3,3 +3,4 @@ typeable-fail.ml[4:1 ..6:3]: error (E2025)
 4 │ instance typeable foo begin
   │ ^^^^^^^^^^^^^^^^^^^^^^^^^^^
   Can not make instance of built-in class typeable
+typeable-fail.ml[4:1 ..6:3]: Use amc explain 2025 for more information
diff --git a/tests/types/value.out b/tests/types/value.out
index 6e16b1d8f..9f8a616fd 100644
--- a/tests/types/value.out
+++ b/tests/types/value.out
@@ -6,3 +6,4 @@ value.ml[3:33 ..3:47]: error (E2016)
   it can not be used in a context where the polymorphic type
     forall 'a. 'a -> 'a
   is required.
+value.ml[3:33 ..3:47]: Use amc explain 2016 for more information
diff --git a/tests/types/vta/vta-fail01.out b/tests/types/vta/vta-fail01.out
index 822dde863..42e492068 100644
--- a/tests/types/vta/vta-fail01.out
+++ b/tests/types/vta/vta-fail01.out
@@ -4,3 +4,4 @@ vta-fail01.ml[3:17 ..3:21]: error (E2001)
   │                 ^^^^^
   Couldn't match actual type string
     with the type expected by the context, int
+vta-fail01.ml[3:17 ..3:21]: Use amc explain 2001 for more information
diff --git a/tests/types/vta/vta-fail02.out b/tests/types/vta/vta-fail02.out
index c1f828e33..67bcb02c1 100644
--- a/tests/types/vta/vta-fail02.out
+++ b/tests/types/vta/vta-fail02.out
@@ -4,3 +4,4 @@ vta-fail02.ml[2:9 ..2:15]: error (E2030)
   │         ^^^^^^^
   Can not apply expression of type int -> int
     to visible type argument int
+vta-fail02.ml[2:9 ..2:15]: Use amc explain 2030 for more information
diff --git a/tests/types/vta/vta-fail03.out b/tests/types/vta/vta-fail03.out
index 1701da761..6bfe17d2e 100644
--- a/tests/types/vta/vta-fail03.out
+++ b/tests/types/vta/vta-fail03.out
@@ -4,3 +4,4 @@ vta-fail03.ml[1:13 ..1:18]: error (E2030)
   │             ^^^^^^
   Can not apply expression of type 'n
     to visible type argument int
+vta-fail03.ml[1:13 ..1:18]: Use amc explain 2030 for more information
diff --git a/tests/types/vta/vta-fail04.out b/tests/types/vta/vta-fail04.out
index 3f1ca08c6..393d9bb2c 100644
--- a/tests/types/vta/vta-fail04.out
+++ b/tests/types/vta/vta-fail04.out
@@ -4,3 +4,4 @@ vta-fail04.ml[1:9 ..1:38]: error (E2030)
   │         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
   Can not apply expression of type 'f -> 'f
     to visible type argument int
+vta-fail04.ml[1:9 ..1:38]: Use amc explain 2030 for more information
diff --git a/tests/types/wildcards/wild04.out b/tests/types/wildcards/wild04.out
index 957cda437..68f4d6d97 100644
--- a/tests/types/wildcards/wild04.out
+++ b/tests/types/wildcards/wild04.out
@@ -4,3 +4,4 @@ wild04.ml[4:9 ..4:9]: error (E2001)
   │         ^
   Couldn't match actual type unit
     with the type expected by the context, string
+wild04.ml[4:9 ..4:9]: Use amc explain 2001 for more information
diff --git a/tests/types/wildcards/wild05.out b/tests/types/wildcards/wild05.out
index 34ab5d207..0001102d3 100644
--- a/tests/types/wildcards/wild05.out
+++ b/tests/types/wildcards/wild05.out
@@ -11,3 +11,4 @@ wild05.ml[1:24 ..1:24]: error (E2009)
 1 │ let f (x : 'a) : int = x
   │       ^^^^^^^^^^^^^^^^^^
   has type forall 'a. 'a -> int
+wild05.ml[1:24 ..1:24]: Use amc explain 2009 for more information
diff --git a/tests/verify/check_lua_01.out b/tests/verify/check_lua_01.out
index 87358417d..a1098ebca 100644
--- a/tests/verify/check_lua_01.out
+++ b/tests/verify/check_lua_01.out
@@ -9,3 +9,5 @@ definition of x[1:3 ..1:3]: error
   │ 
 1 │ x x
   │   ^
+
+definition of x[1:3 ..1:3]: Use amc explain 3003 for more information
diff --git a/tests/verify/lazy_let_02.out b/tests/verify/lazy_let_02.out
index c4eb360bc..749ee13d1 100644
--- a/tests/verify/lazy_let_02.out
+++ b/tests/verify/lazy_let_02.out
@@ -12,3 +12,4 @@ lazy_let_02.ml[4:3 ..5:5]: warning (W3004)
   is strict.
   • Note: if this is what you want, use lazy explicitly
       to silence this warning.
+lazy_let_02.ml[4:3 ..5:5]: Use amc explain 3004 for more information
diff --git a/tests/verify/match_to.out b/tests/verify/match_to.out
index d4125190a..ea18d6111 100644
--- a/tests/verify/match_to.out
+++ b/tests/verify/match_to.out
@@ -4,6 +4,7 @@ match_to.ml[3:9 ..3:16]: note (N3007)
 3 │ let _ = function
   │         ^^^^^^^^
   • Note: Replace with let { x = x, y = y } = …
+match_to.ml[3:9 ..3:16]: Use amc explain 3007 for more information
 match_to.ml[7:9 ..7:16]: warning (W3006)
   Non-exhaustive patterns in expression
   │ 
@@ -11,12 +12,14 @@ match_to.ml[7:9 ..7:16]: warning (W3006)
   │         ^^^^^^^^
   • Note: The following patterns are not covered
       false
+match_to.ml[7:9 ..7:16]: Use amc explain 3006 for more information
 match_to.ml[14:3 ..14:17]: note (N3007)
   match with a single arm can be rewritten using let.
    │ 
 14 │   match g () with
    │   ^^^^^^^^^^^^^^^
   • Note: Replace with let { x = x, y = y } = …
+match_to.ml[14:3 ..14:17]: Use amc explain 3007 for more information
 match_to.ml[18:3 ..18:17]: warning (W3006)
   Non-exhaustive patterns in expression
    │ 
@@ -24,3 +27,4 @@ match_to.ml[18:3 ..18:17]: warning (W3006)
    │   ^^^^^^^^^^^^^^^
   • Note: The following patterns are not covered
       false
+match_to.ml[18:3 ..18:17]: Use amc explain 3006 for more information
diff --git a/tests/verify/pmcheck/empty_match_01.out b/tests/verify/pmcheck/empty_match_01.out
index fbfc442fe..6ee6281bc 100644
--- a/tests/verify/pmcheck/empty_match_01.out
+++ b/tests/verify/pmcheck/empty_match_01.out
@@ -5,6 +5,7 @@ empty_match_01.ml[2:33 ..2:40]: warning (W3006)
   │                                 ^^^^^^^^
   • Note: The following patterns are not covered
       _
+empty_match_01.ml[2:33 ..2:40]: Use amc explain 3006 for more information
 empty_match_01.ml[7:22 ..7:29]: warning (W3006)
   Non-exhaustive patterns in expression
   │ 
@@ -12,3 +13,4 @@ empty_match_01.ml[7:22 ..7:29]: warning (W3006)
   │                      ^^^^^^^^
   • Note: The following patterns are not covered
       _
+empty_match_01.ml[7:22 ..7:29]: Use amc explain 3006 for more information
diff --git a/tests/verify/pmcheck/empty_match_02.out b/tests/verify/pmcheck/empty_match_02.out
index 93539fd4e..dbc004f48 100644
--- a/tests/verify/pmcheck/empty_match_02.out
+++ b/tests/verify/pmcheck/empty_match_02.out
@@ -5,3 +5,4 @@ empty_match_02.ml[19:34 ..19:41]: warning (W3006)
    │                                  ^^^^^^^^
   • Note: The following patterns are not covered
       _
+empty_match_02.ml[19:34 ..19:41]: Use amc explain 3006 for more information
diff --git a/tests/verify/pmcheck/empty_match_03.out b/tests/verify/pmcheck/empty_match_03.out
index dde3e17de..61472c13d 100644
--- a/tests/verify/pmcheck/empty_match_03.out
+++ b/tests/verify/pmcheck/empty_match_03.out
@@ -4,3 +4,4 @@ empty_match_03.ml[3:26 ..3:32]: warning (W3005)
 3 │ let f : void -> () = fun _ -> ()
   │                          ^^^^^^^
   • Note: This can be replaced by an empty match.
+empty_match_03.ml[3:26 ..3:32]: Use amc explain 3005 for more information
diff --git a/tests/verify/pmcheck/gadt_04.out b/tests/verify/pmcheck/gadt_04.out
index f4e724258..045dd8d0c 100644
--- a/tests/verify/pmcheck/gadt_04.out
+++ b/tests/verify/pmcheck/gadt_04.out
@@ -4,3 +4,4 @@ gadt_04.ml[17:5 ..17:23]: warning (W3005)
 17 │   | Nil_, _ -> error ""
    │     ^^^^^^^^^^^^^^^^^^^
   • Note: This case can never occur.
+gadt_04.ml[17:5 ..17:23]: Use amc explain 3005 for more information
diff --git a/tests/verify/pmcheck/pattern_totality.out b/tests/verify/pmcheck/pattern_totality.out
index d39b7260e..5b1e0359a 100644
--- a/tests/verify/pmcheck/pattern_totality.out
+++ b/tests/verify/pmcheck/pattern_totality.out
@@ -5,6 +5,7 @@ pattern_totality.ml[10:9 ..10:17]: warning (W3006)
    │         ^^^^^^^^^
   • Note: The following patterns are not covered
       Some _
+pattern_totality.ml[10:9 ..10:17]: Use amc explain 3006 for more information
 pattern_totality.ml[11:10 ..11:21]: warning (W3006)
   Non-exhaustive patterns in expression
    │ 
@@ -12,12 +13,14 @@ pattern_totality.ml[11:10 ..11:21]: warning (W3006)
    │          ^^^^^^^^^^^^
   • Note: The following patterns are not covered
       None
+pattern_totality.ml[11:10 ..11:21]: Use amc explain 3006 for more information
 pattern_totality.ml[16:7 ..16:18]: warning (W3005)
   Redundant pattern in expression
    │ 
 16 │     | Some _ -> ()
    │       ^^^^^^^^^^^^
   • Note: This case is covered by all previous patterns and so can be removed
+pattern_totality.ml[16:7 ..16:18]: Use amc explain 3005 for more information
 pattern_totality.ml[37:11 ..37:18]: warning (W3006)
   Non-exhaustive patterns in expression
    │ 
@@ -25,6 +28,7 @@ pattern_totality.ml[37:11 ..37:18]: warning (W3006)
    │           ^^^^^^^^
   • Note: The following patterns are not covered
       Any _
+pattern_totality.ml[37:11 ..37:18]: Use amc explain 3006 for more information
 pattern_totality.ml[41:38 ..41:45]: warning (W3006)
   Non-exhaustive patterns in expression
    │ 
@@ -32,12 +36,14 @@ pattern_totality.ml[41:38 ..41:45]: warning (W3006)
    │                                      ^^^^^^^^
   • Note: The following patterns are not covered
       Unit _ | Any _
+pattern_totality.ml[41:38 ..41:45]: Use amc explain 3006 for more information
 pattern_totality.ml[48:7 ..48:17]: warning (W3005)
   Redundant pattern in expression
    │ 
 48 │     | Any _ -> ()
    │       ^^^^^^^^^^^
   • Note: This case is covered by all previous patterns and so can be removed
+pattern_totality.ml[48:7 ..48:17]: Use amc explain 3005 for more information
 pattern_totality.ml[55:11 ..55:18]: warning (W3006)
   Non-exhaustive patterns in expression
    │ 
@@ -45,12 +51,14 @@ pattern_totality.ml[55:11 ..55:18]: warning (W3006)
    │           ^^^^^^^^
   • Note: The following patterns are not covered
       { x = _, y = _ }
+pattern_totality.ml[55:11 ..55:18]: Use amc explain 3006 for more information
 pattern_totality.ml[62:7 ..62:21]: warning (W3005)
   Redundant pattern in expression
    │ 
 62 │     | { y = 0 } -> ()
    │       ^^^^^^^^^^^^^^^
   • Note: This case is covered by all previous patterns and so can be removed
+pattern_totality.ml[62:7 ..62:21]: Use amc explain 3005 for more information
 pattern_totality.ml[69:11 ..69:18]: warning (W3006)
   Non-exhaustive patterns in expression
    │ 
@@ -58,6 +66,7 @@ pattern_totality.ml[69:11 ..69:18]: warning (W3006)
    │           ^^^^^^^^
   • Note: The following patterns are not covered
       _, _
+pattern_totality.ml[69:11 ..69:18]: Use amc explain 3006 for more information
 pattern_totality.ml[73:11 ..73:18]: warning (W3006)
   Non-exhaustive patterns in expression
    │ 
@@ -65,12 +74,14 @@ pattern_totality.ml[73:11 ..73:18]: warning (W3006)
    │           ^^^^^^^^
   • Note: The following patterns are not covered
       None, Some _ | Some _, None
+pattern_totality.ml[73:11 ..73:18]: Use amc explain 3006 for more information
 pattern_totality.ml[80:7 ..80:18]: warning (W3005)
   Redundant pattern in expression
    │ 
 80 │     | (_, _) -> ()
    │       ^^^^^^^^^^^^
   • Note: This case is covered by all previous patterns and so can be removed
+pattern_totality.ml[80:7 ..80:18]: Use amc explain 3005 for more information
 pattern_totality.ml[93:11 ..93:18]: warning (W3006)
   Non-exhaustive patterns in expression
    │ 
@@ -78,6 +89,7 @@ pattern_totality.ml[93:11 ..93:18]: warning (W3006)
    │           ^^^^^^^^
   • Note: The following patterns are not covered
       false
+pattern_totality.ml[93:11 ..93:18]: Use amc explain 3006 for more information
 pattern_totality.ml[95:11 ..95:18]: warning (W3006)
   Non-exhaustive patterns in expression
    │ 
@@ -85,21 +97,25 @@ pattern_totality.ml[95:11 ..95:18]: warning (W3006)
    │           ^^^^^^^^
   • Note: The following patterns are not covered
       _
+pattern_totality.ml[95:11 ..95:18]: Use amc explain 3006 for more information
 pattern_totality.ml[101:7 ..101:13]: warning (W3005)
   Redundant pattern in expression
     │ 
 101 │     | _ -> ()
     │       ^^^^^^^
   • Note: This case is covered by all previous patterns and so can be removed
+pattern_totality.ml[101:7 ..101:13]: Use amc explain 3005 for more information
 pattern_totality.ml[105:7 ..105:13]: warning (W3005)
   Redundant pattern in expression
     │ 
 105 │     | _ -> ()
     │       ^^^^^^^
   • Note: This case is covered by all previous patterns and so can be removed
+pattern_totality.ml[105:7 ..105:13]: Use amc explain 3005 for more information
 pattern_totality.ml[108:7 ..108:13]: warning (W3005)
   Redundant pattern in expression
     │ 
 108 │     | 0 -> ()
     │       ^^^^^^^
   • Note: This case is covered by all previous patterns and so can be removed
+pattern_totality.ml[108:7 ..108:13]: Use amc explain 3005 for more information
diff --git a/tests/verify/recursive_01.out b/tests/verify/recursive_01.out
index 36ed98d29..9bcf71e86 100644
--- a/tests/verify/recursive_01.out
+++ b/tests/verify/recursive_01.out
@@ -5,8 +5,10 @@ recursive_01.ml[4:5 ..4:5]: error (E3001)
   │ 
 4 │ and g = f
   │     ^
+recursive_01.ml[4:5 ..4:5]: Use amc explain 3001 for more information
 recursive_01.ml[2:7 ..2:7]: warning (W3002)
   Bound locally but not used: 'y'
   │ 
 2 │   let y = 1
   │       ^
+recursive_01.ml[2:7 ..2:7]: Use amc explain 3002 for more information
diff --git a/tests/verify/recursive_02.out b/tests/verify/recursive_02.out
index 230b5df2f..31b694224 100644
--- a/tests/verify/recursive_02.out
+++ b/tests/verify/recursive_02.out
@@ -5,6 +5,7 @@ recursive_02.ml[6:11 ..6:11]: error (E3001)
   │ 
 6 │   let rec f = (fun _ -> g) 1
   │           ^
+recursive_02.ml[6:11 ..6:11]: Use amc explain 3001 for more information
 recursive_02.ml[7:7 ..7:7]: error (E3001)
   Invalid recursive right-hand side for variable g
   • Note: because evaluation of the variable f is not delayed
@@ -12,3 +13,4 @@ recursive_02.ml[7:7 ..7:7]: error (E3001)
   │ 
 7 │   and g = (fun _ -> f) 1
   │       ^
+recursive_02.ml[7:7 ..7:7]: Use amc explain 3001 for more information
diff --git a/tests/verify/recursive_03.out b/tests/verify/recursive_03.out
index fc1421895..18da6660c 100644
--- a/tests/verify/recursive_03.out
+++ b/tests/verify/recursive_03.out
@@ -5,3 +5,4 @@ recursive_03.ml[1:9 ..1:9]: error (E3001)
   │ 
 1 │ let rec x = x
   │         ^
+recursive_03.ml[1:9 ..1:9]: Use amc explain 3001 for more information
diff --git a/tests/verify/recursive_07.out b/tests/verify/recursive_07.out
index 31807b30c..7ca43841d 100644
--- a/tests/verify/recursive_07.out
+++ b/tests/verify/recursive_07.out
@@ -5,3 +5,4 @@ recursive_07.ml[2:5 ..2:5]: error (E3001)
   │ 
 2 │ and g = f
   │     ^
+recursive_07.ml[2:5 ..2:5]: Use amc explain 3001 for more information
diff --git a/tests/verify/topref.out b/tests/verify/topref.out
index c27529dc6..1946caf91 100644
--- a/tests/verify/topref.out
+++ b/tests/verify/topref.out
@@ -4,33 +4,39 @@ topref.ml[1:5 ..1:5]: warning (W3009)
   │ 
 1 │ let a = ref true
   │     ^
+topref.ml[1:5 ..1:5]: Use amc explain 3009 for more information
 topref.ml[2:6 ..2:6]: warning (W3009)
   This top-level binding defines a reference (of type ref bool)
   • Note: This is bad style.
   │ 
 2 │ let (a, b) = (ref true, ref "")
   │      ^
+topref.ml[2:6 ..2:6]: Use amc explain 3009 for more information
 topref.ml[2:9 ..2:9]: warning (W3009)
   This top-level binding defines a reference (of type ref string)
   • Note: This is bad style.
   │ 
 2 │ let (a, b) = (ref true, ref "")
   │         ^
+topref.ml[2:9 ..2:9]: Use amc explain 3009 for more information
 topref.ml[3:6 ..3:6]: warning (W3009)
   This top-level binding defines a reference (of type ref int)
   • Note: This is bad style.
   │ 
 3 │ let [a, b, c] = [ref 0, ref 1, ref 2]
   │      ^
+topref.ml[3:6 ..3:6]: Use amc explain 3009 for more information
 topref.ml[3:9 ..3:9]: warning (W3009)
   This top-level binding defines a reference (of type ref int)
   • Note: This is bad style.
   │ 
 3 │ let [a, b, c] = [ref 0, ref 1, ref 2]
   │         ^
+topref.ml[3:9 ..3:9]: Use amc explain 3009 for more information
 topref.ml[3:12 ..3:12]: warning (W3009)
   This top-level binding defines a reference (of type ref int)
   • Note: This is bad style.
   │ 
 3 │ let [a, b, c] = [ref 0, ref 1, ref 2]
   │            ^
+topref.ml[3:12 ..3:12]: Use amc explain 3009 for more information
diff --git a/tests/verify/unused_let_inner_01.out b/tests/verify/unused_let_inner_01.out
index 580f572c7..e4d885456 100644
--- a/tests/verify/unused_let_inner_01.out
+++ b/tests/verify/unused_let_inner_01.out
@@ -3,3 +3,4 @@ unused_let_inner_01.ml[2:7 ..2:7]: warning (W3002)
   │ 
 2 │   let y = 1
   │       ^
+unused_let_inner_01.ml[2:7 ..2:7]: Use amc explain 3002 for more information
diff --git a/tests/verify/unused_let_inner_03.out b/tests/verify/unused_let_inner_03.out
index 2323aa454..34fa2dbb8 100644
--- a/tests/verify/unused_let_inner_03.out
+++ b/tests/verify/unused_let_inner_03.out
@@ -3,8 +3,10 @@ unused_let_inner_03.ml[2:7 ..2:7]: warning (W3002)
   │ 
 2 │   let y = 0
   │       ^
+unused_let_inner_03.ml[2:7 ..2:7]: Use amc explain 3002 for more information
 unused_let_inner_03.ml[3:7 ..3:7]: warning (W3002)
   Bound locally but not used: 'x'
   │ 
 3 │   let x = 0
   │       ^
+unused_let_inner_03.ml[3:7 ..3:7]: Use amc explain 3002 for more information
diff --git a/tests/verify/unused_let_inner_04.out b/tests/verify/unused_let_inner_04.out
index e95f9dce7..42247472a 100644
--- a/tests/verify/unused_let_inner_04.out
+++ b/tests/verify/unused_let_inner_04.out
@@ -3,8 +3,10 @@ unused_let_inner_04.ml[2:8 ..2:8]: warning (W3002)
   │ 
 2 │   let (a, b) = (1, 2)
   │        ^
+unused_let_inner_04.ml[2:8 ..2:8]: Use amc explain 3002 for more information
 unused_let_inner_04.ml[2:11 ..2:11]: warning (W3002)
   Bound locally but not used: 'b'
   │ 
 2 │   let (a, b) = (1, 2)
   │           ^
+unused_let_inner_04.ml[2:11 ..2:11]: Use amc explain 3002 for more information
diff --git a/tests/verify/unused_let_top_03.out b/tests/verify/unused_let_top_03.out
index 7d3d3249c..f96333e9c 100644
--- a/tests/verify/unused_let_top_03.out
+++ b/tests/verify/unused_let_top_03.out
@@ -3,3 +3,4 @@ unused_let_top_03.ml[1:13 ..1:13]: warning (W3002)
   │ 
 1 │ let private x = 1
   │             ^
+unused_let_top_03.ml[1:13 ..1:13]: Use amc explain 3002 for more information
diff --git a/tests/verify/unused_let_top_04.out b/tests/verify/unused_let_top_04.out
index 771be9ee3..5fcb1e527 100644
--- a/tests/verify/unused_let_top_04.out
+++ b/tests/verify/unused_let_top_04.out
@@ -3,8 +3,10 @@ unused_let_top_04.ml[1:14 ..1:14]: warning (W3002)
   │ 
 1 │ let private (a, b) = (1, 2)
   │              ^
+unused_let_top_04.ml[1:14 ..1:14]: Use amc explain 3002 for more information
 unused_let_top_04.ml[1:17 ..1:17]: warning (W3002)
   Bound locally but not used: 'b'
   │ 
 1 │ let private (a, b) = (1, 2)
   │                 ^
+unused_let_top_04.ml[1:17 ..1:17]: Use amc explain 3002 for more information
diff --git a/tests/verify/unused_pat_01.out b/tests/verify/unused_pat_01.out
index 208d4d2f8..a602320fd 100644
--- a/tests/verify/unused_pat_01.out
+++ b/tests/verify/unused_pat_01.out
@@ -3,8 +3,10 @@ unused_pat_01.ml[4:6 ..4:6]: warning (W3002)
   │ 
 4 │   | (a, b) -> 0
   │      ^
+unused_pat_01.ml[4:6 ..4:6]: Use amc explain 3002 for more information
 unused_pat_01.ml[4:9 ..4:9]: warning (W3002)
   Bound locally but not used: 'b'
   │ 
 4 │   | (a, b) -> 0
   │         ^
+unused_pat_01.ml[4:9 ..4:9]: Use amc explain 3002 for more information
diff --git a/tests/verify/verify14.out b/tests/verify/verify14.out
index cd5945b9c..281b07777 100644
--- a/tests/verify/verify14.out
+++ b/tests/verify/verify14.out
@@ -3,3 +3,4 @@ verify14.ml[5:7 ..5:7]: warning (W3002)
   │ 
 5 │   let y = f x
   │       ^
+verify14.ml[5:7 ..5:7]: Use amc explain 3002 for more information
diff --git a/tests/verify/verify16.out b/tests/verify/verify16.out
index 207a68575..6bf804f61 100644
--- a/tests/verify/verify16.out
+++ b/tests/verify/verify16.out
@@ -5,6 +5,7 @@ verify16.ml[6:11 ..6:11]: error (E3001)
   │ 
 6 │   let rec f = id (fun _ -> g) 1
   │           ^
+verify16.ml[6:11 ..6:11]: Use amc explain 3001 for more information
 verify16.ml[7:7 ..7:7]: error (E3001)
   Invalid recursive right-hand side for variable g
   • Note: because evaluation of the variable f is not delayed
@@ -12,3 +13,4 @@ verify16.ml[7:7 ..7:7]: error (E3001)
   │ 
 7 │   and g = id (fun _ -> f) 1
   │       ^
+verify16.ml[7:7 ..7:7]: Use amc explain 3001 for more information