Potential infinite loop in type checking

[Meowcolm024]

In cb89a08412b0badcc39dc2ec27dc8e2f158e5554

:NewDefs
:GADTs

abstract class Foo[type T]: Bar | Baz
class Bar extends Foo[Int]
class Baz[T](val x: Foo[T]) extends Foo[[T]]

fun foo[T](f: Foo[T]): Int = if f is
    Bar then 0
    Baz(x) then foo(x : Foo[x.T])
//│ ╔══[ERROR] Subtyping constraint of the form `([?a]) -> ?b <: ?c -> ?d` exceeded recursion depth limit (250)
//│ ║  l.14:    fun foo[T](f: Foo[T]): Int = if f is
//│ ║                                           ^^^^
//│ ║  l.15:        Bar then 0
//│ ║           ^^^^^^^^^^^^^^
//│ ║  l.16:        Baz(x) then foo(x : Foo[x.T])
//│ ║           ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
//│ ╙── Note: use flag `:ex` to see internal error info.
// (some more errors)

[Meowcolm024]

Update: an even smaller example:

class Box[type A](val get: A)
abstract class F[type A]: MkF
class MkF[T](t: T) extends F[Box[T]]

fun f[T](x: F[T]): T = if x is MkF(t) then Box(t) as x.A
//│ ╔══[ERROR] Subtyping constraint of the form `?a <: ?b` exceeded recursion depth limit (250)
//│ ╙── Note: use flag `:ex` to see internal error info.
//│ fun f: forall 'T. (x: F['T]) -> 'T

[LPTK]

So as we've discussed before, this seems to be happening during reconstraining after type extrusion. Recornstraining is basically a hacky plug on top of extrusion to detect type mismatches introduced by approximated skolems (in the context of first-class polymorphism).

The solution is not a low-hanging fruit. We need to rearchitect extrusion so it's done in a more principled way, accumulating all level-mismatched bounds first and extruding them all together, only reconstraining what's actually neede.

[LPTK]

Ok so it turns out the issue was not what I thought it was. There was a bug in extrusion, fixed in 55ae3631be9cd7a7d34c6b20701864858364b6a5.