Skip to content

Commit

Permalink
hack subtyping to accept polyrec.mo by treating equivalent instanstat…
Browse files Browse the repository at this point in the history
…ions of the same constructor as related by subtyping
  • Loading branch information
crusso committed Dec 4, 2024
1 parent d6baeec commit be2e422
Show file tree
Hide file tree
Showing 3 changed files with 8 additions and 8 deletions.
8 changes: 7 additions & 1 deletion src/mo_types/type.ml
Original file line number Diff line number Diff line change
Expand Up @@ -911,7 +911,9 @@ let rel_list p rel eq xs1 xs2 =
try List.for_all2 (p rel eq) xs1 xs2 with Invalid_argument _ -> false

let rec rel_typ rel eq t1 t2 =
t1 == t2 || SS.mem (t1, t2) !rel || begin
(* Printf.printf "%s rel %s\n" (!str t1) (!str t2); *)
t1 == t2 || SS.mem (t1, t2) !rel ||
begin
rel := SS.add (t1, t2) !rel;
match t1, t2 with
(* Second-class types first, since they mustn't relate to Any/Non *)
Expand All @@ -934,6 +936,10 @@ let rec rel_typ rel eq t1 t2 =
true
| Con (con1, ts1), Con (con2, ts2) ->
(match Cons.kind con1, Cons.kind con2 with
(* first clause is a hack to support (some) non-regular recursion *)
| Def (_, _), Def (_, _) when
Cons.eq con1 con2 && rel_list eq_typ rel eq ts1 ts2 ->
true
| Def (tbs, t), _ -> (* TBR this may fail to terminate *)
rel_typ rel eq (open_ ts1 t) t2
| _, Def (tbs, t) -> (* TBR this may fail to terminate *)
Expand Down
7 changes: 1 addition & 6 deletions test/fail/ok/polyrec.tc.ok
Original file line number Diff line number Diff line change
@@ -1,6 +1 @@
OOPS! You've triggered a compiler bug.
Please report this at https://github.com/dfinity/motoko/issues/new with the following details:

Motoko (source 0.13.4-30-gcedc663ea-dirty)

Fatal error: exception Stack overflow
polyrec.mo:10.24-10.25: warning [M0194], unused identifier f (delete or rename to wildcard `_` or `_f`)
1 change: 0 additions & 1 deletion test/fail/ok/polyrec.tc.ret.ok

This file was deleted.

0 comments on commit be2e422

Please sign in to comment.