Subtype checking of recursive polymorphic types where the type parameters change with each recursion doesn't terminate

[nanikamado]

Sample code:

data R(A) forall { A }
type S1 = A | S1[R[A]] forall { A }
type S2 = A | R[S2[A]] forall { A }

main : () -> () =
    | () => do
        (() : S1[()]) : S2[()]

Currently there is a loop count limit to prevent stack overflow, but improving the type checking algorithm and removing the limit is better.