You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
In #9140 we needed to temporarily remove code for approximating/"healing" types with GADT constraints, as it introduced unsoundness.
The root of the issue is more-or-less that given constraints F[X] <: G[X]; A <: B we approximated F[A] ~ G[B], even though we should not as F/G might not be injective.
@smarter the code for approximating GADTs is almost a copy of IsFullyDefinedAccumulator. Given that, do you suppose there's an equivalent problem with type variable approximation (forcing)? If not, then why?
The text was updated successfully, but these errors were encountered:
@smarter the code for approximating GADTs is almost a copy of IsFullyDefinedAccumulator. Given that, do you suppose there's an equivalent problem with type variable approximation (forcing)? If not, then why?
I think it has to do with the difference between "may" and "must". IsFullyDefinedAccumulator forces a solution and cuts the possible solution space. But GADTs cannot do that since they can only compute what is entailed by the constraint, whereas type inference is allowed to produce anything that is consistent with the constraint.
Right, I discussed this in-person with Guillaume and he gave the same answer. To be very precise, IsFullyDefined forces A = B. This is surprising, as I'd expect ApproximateGadtAccumulator to fail at the equivalent point, which it does not. Will need to look into it.
Uh oh!
There was an error while loading. Please reload this page.
In #9140 we needed to temporarily remove code for approximating/"healing" types with GADT constraints, as it introduced unsoundness.
The root of the issue is more-or-less that given constraints
F[X] <: G[X]; A <: B
we approximatedF[A] ~ G[B]
, even though we should not as F/G might not be injective.@smarter the code for approximating GADTs is almost a copy of IsFullyDefinedAccumulator. Given that, do you suppose there's an equivalent problem with type variable approximation (forcing)? If not, then why?
The text was updated successfully, but these errors were encountered: