Revisit approximating GADTs after implicit lookup

[abgruszecki]

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]

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

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.