Skip to content

Revisit approximating GADTs after implicit lookup #9158

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
abgruszecki opened this issue Jun 11, 2020 · 2 comments · Fixed by #9322
Closed

Revisit approximating GADTs after implicit lookup #9158

abgruszecki opened this issue Jun 11, 2020 · 2 comments · Fixed by #9322
Assignees

Comments

@abgruszecki
Copy link
Contributor

abgruszecki commented Jun 11, 2020

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?

@odersky
Copy link
Contributor

odersky commented Jun 11, 2020

@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.

@abgruszecki
Copy link
Contributor Author

abgruszecki commented Jun 11, 2020

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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging a pull request may close this issue.

2 participants