add error code desc; use dedicated exception Undecided

src/lang_utils/error_codes.ml

@@ -203,4 +203,5 @@ let error_codes : (string * string option) list =
     "M0197", Some([%blob "lang_utils/error_codes/M0197.md"]); (* `system` capability required *)
     "M0198", Some([%blob "lang_utils/error_codes/M0198.md"]); (* Unused field pattern warning *)
     "M0199", Some([%blob "lang_utils/error_codes/M0199.md"]); (* Deprecate experimental stable memory *)
+    "M0200", Some([%blob "lang_utils/error_codes/M0200.md"]) (* Cannot determine subtyping or equality *)
   ]

src/lang_utils/error_codes/M0200.md

@@ -0,0 +1,44 @@
+# M0200
+
+This error means that the compiler encountered a subtyping, equivalence or constructor equivalence problem that it cannot decide is true or false in a timely manner.
+
+This is due to a limitation of the type system and may require you to rewrite
+some of your code to avoid the problem.
+
+The most like cause is a recursive type or class whose definition involves
+instantiating the type or class with nested type parameters.
+
+For example, this definition of `Box<T>`
+
+``` motoko
+class Box<T>(v : T) {
+  public let value = t;
+  public func map<R>(f : T -> R) : Box<R> {
+     Box<R>(f t)
+  };
+}
+```
+is problematic because `Box<R>` is instantiated at `R`, an inner type parameter, while
+
+``` motoko
+class Box<T>(v : T) {
+  public let value = v;
+  public func map(f : T -> T) : Box<T> {
+     Box<T>(f value)
+  };
+}
+```
+is accepted (but also less useful).
+
+Another workaround is to define the problematic method as a separate
+function, outside of the class:
+
+``` motoko
+class Box<T>(v : T) {
+  public let value = v
+};
+
+func map<T, R>(b : Box<T>, f : T -> R) : Box<R> {
+  Box<R>(f (b.value))
+};
+```

src/mo_frontend/typing.ml

@@ -334,13 +334,21 @@ let disjoint_union env at code fmt env1 env2 =
 
 
 let sub env at t1 t2 =
-  try T.sub t1 t2  with _ -> error env at "M0XXX" "can't determine subtyping?"
+  try T.sub t1 t2  with T.Undecided ->
+    error env at "M0200" "cannot decide subtyping between type%a\nand%a"
+      display_typ_expand t1
+      display_typ_expand t2
 
 let eq env at t1 t2 =
-  try T.eq t1 t2  with _ -> error env at "M0XXX" "can't determine type equality?"
+  try T.eq t1 t2  with T.Undecided ->
+    error env at "M0200" "cannot decide equality between type%a\nand%a"
+      display_typ_expand t1
+      display_typ_expand t2
+
 
 let eq_kind env at k1 k2 =
-  try T.eq_kind k1 k2  with _ -> error env at "M0XXX" "can't determine type constructor equality?"
+  try T.eq_kind k1 k2 with T.Undecided ->
+    error env at "M0200" "cannot decide type constructor equality"
 
 (* Coverage *)
 

src/mo_types/type.ml

@@ -904,6 +904,8 @@ let str = ref (fun _ -> failwith "")
 
 exception PreEncountered
 
+exception Undecided
+
 module SS = Set.Make (OrdPair)
 
 let max_depth = 10_000
@@ -913,7 +915,7 @@ let rel_list d p rel eq xs1 xs2 =
 
 let rec rel_typ d rel eq t1 t2 =
   let d = d + 1 in
-  if d > max_depth then failwith "subtyping: recursion too deep" else
+  if d > max_depth then raise Undecided else
   t1 == t2 || SS.mem (t1, t2) !rel || begin
   rel := SS.add (t1, t2) !rel;
   match t1, t2 with

src/mo_types/type.mli

@@ -221,8 +221,11 @@ val span : typ -> int option
 val cons: typ -> ConSet.t
 val cons_kind : kind -> ConSet.t
 
+
 (* Equivalence and Subtyping *)
 
+exception Undecided (* raised if termination depth exceeded  *)
+
 val eq : typ -> typ -> bool
 val eq_kind : kind -> kind -> bool
 

test/fail/ok/polyrec.tc.ok

@@ -1 +1 @@
-polyrec.mo:4.10-11.4: type error [M0XXX], can't determine type constructor equality?
+polyrec.mo:4.10-11.4: type error [M0200], cannot decide type constructor equality