Open TomasMikula opened 1 year ago
This looks like a bug to me. @abgruszecki @Linyxus can you confirm?
This seems like a completeness issue to me too. The constraint U =:= u
is not derived, because we do not assume the injectivity of this HK type F
(which means that given F[a] =:= F[b]
we can not show a =:= b
). Specifically, when we infer GADT bounds from Foo[F[T], U] >:< Foo[F[t], u]
:
F[T] =:= F[t]
.F
is non-injective, we won't derive the constraint T =:= t
(which we shouldn't), and returns false
in TypeComparer.F[T] =:= F[t]
is false
, we would just rollback the GADT constraints, and won't even examine U >:< u
(as seen here).Rolling back GADT constraints when the type comparer returns false feels a bit too restrictive to me. Since as long as we are careful enough when adding constraints (only adding the really necessary ones), whether type comparer thinks a subtyping relation is absurd should not matter. Does the logic here have other considerations (like for some sort of interactions with type inference)? Shall we drop it for better completeness?
As I remember it, this is actually a tricky issue. The problem is that with the way we implemented subtyping reconstruction, we do not properly distinguish between a subtype check that cannot possibly succeed and one that may succeed for some instantiation of abstract types.
In an Ideal World, while doing subtyping reconstruction, isSubtype
would only return false
if the desired subtyping relationship is contradictory, say Int <:< String
. Note that this should mean that F[T] <:< F[t]
should return true
, because the relationship is clearly possible (for instance for type F[X] = Unit
). In this Ideal World, we should roll back the constraints every time isSubtype
returns false
, and there would be cases where we could exploit that to reconstruct better bounds, but (!) only as long as we can trust that false
means that the relationship is genuinely contradictory.
As we are right now, we roll back the constraint, but also return false
too eagerly during subtyping recostruction. I think it's justifiable to never roll back the constraints, but IIRC it should be possible to construct examples where that gives us worse results, at least I recall that once Yichen implemented the rollback, we reconstructed better bounds in some cases.
And to make it clear: we've been trying to fix the problems with reusing isSubtype
for subtyping reconstruction and we keep finding new and new problems with it. I think it would take a dedicated project to clean things up on that front, and it might require separating subtyping reconstruction from isSubtype
.
Compiler version
3.2.2
Minimized code
Output
Compilation fails, see the errors in the comments.
Expectation
The code should compile.