Implement AssumeInfo

[dwijnand]

No description provided.

[dwijnand]

I think I need to redo this because I need the GADT constraints installed for the pattern (and the guard, actually) as well - i.e. I can't just wrap the body I need to wrap the whole case...

[dwijnand]

@nicolasstucki Are there requirements around the test that uses Extractor? I'm pretty sure it was the BootstrappedStdLibTASYyTest test. Can I leave some internal details out?

[dwijnand]

test performance please

[dottybot]

performance test scheduled: 1 job(s) in queue, 0 running.

[dottybot]

Performance test finished successfully:

Visit https://dotty-bench.epfl.ch/15928/ to see the changes.

Benchmarks is based on merging with main (a6a3385)

[sjrd]

I've been assigned so here are some comments. Overall it looks reasonable, although I really can't judge the changes in Typer and TypeComparer.

[sjrd]

This seems fishy to me. IIUC, that means that top-level AssumeInfos in the body of a CaseDef actually also apply to their patten and guard? That's a pretty weird combo yielding semantics that cannot be understood for one separately from the the other. Have you considered:

• Surrounding the CaseDef with AssumeInfo (also a bit weird, because now a Match needs to deal with AssumeInfo in its cases; but at least the Match/CaseDef is already a very solid combo), or
• Repeating the required AssumeInfo in the pattern and guard, if necessary

?

[dwijnand]

This is necessary to satisfy the bounds check that happens in post typer. On the opposite side it needs to especially not be done in the TypeTestCasts checks, which are run during Erasure, in order to give correct results on whether any type test has any uncheckable parts.

It comes down to the fact that the assumed info may only be assume provided the pattern matches. So in PostTyper we want to check the bounds, which only matters if the pattern matches, while in TypeTestCasts we want to check uncheckable, which may not assume the pattern matches.

Wrapping the CaseDef is double hard. Firstly, because undoing the assumption for TypeTestCasts isn't easy. Secondly, because Match is already reused for inline matches and match types, so having all those code paths deal with this change is painful. There's a lot of code that expects matches to be of cases, so it's quite hairy to make it all deal with AssumeInfo vs CaseDef. In my original where I was holding onto a GadtConstraint I tried splitting CaseDef into {GadtCaseDef, CaseDef} <: GenericCaseDef, but it was very painful. I also tried having all CaseDef have a GadtConstraint, but it was still awkward.

Repeating the required AssumeInfo still runs into the TypeTestCasts issue. And would that be repeating as in copy or same reference? I could reuse the same reference, and do something awful for TypeTestCasts.

Btw, if you look at the before state (earlier in the file) it was set up in the opposite direction: the gadt as an attachment on the pattern was installed to be present when transforming the tree as a whole. So this is different but the same, as I see it.

[sjrd]

Suggested change

	inContext(ctx.withGadt(ctx.gadt.withAssumeInfos(assumeInfos))) {
	assumeInfos.foldRight(readTerm()) { case (AssumeInfo(sym, nestingLevel, info, _), body) =>
	inContext(ctx.withGadt(ctx.gadt.withAssumeInfos(assumeInfos))) {
	assumeInfos.foldRight(readTerm()) { case (AssumeInfo(sym, nestingLevel, info, _), body) =>

[sjrd]

Do we actually need this gadt.withAssumeInfos while unpickling? If yes, why?

[dwijnand]

I guess I don't have a canonical example that would fail without this. I haven't tried (today) to take it out and test - but I can. But my general desire is to have these known facts to always be present whenever there's a chance there's some type comparisons potentially happening. As I understand it the design is that there's only a very light, simple amount of type composition that happens during unpickling (e.g. List + Int = List[Int]). But does none of it require any type comparisons?

What's your concern here? Performance?

[sjrd]

My concern is mostly whether we can replicate this logic in tasty-query. In tasty-query, the unpickling step is not allowed to look at any information coming from outside the current .tasty file. If dotty requires contextual type information like this to unpickle, there's a good chance that tasty-query would need it as well, and that would be a problem.

[odersky]

I'd prefer not to enrich the context. First. it costs time. Second, I don't see a case where we would need it. Which means we should start without and see whether we are proven wrong. If we are proven wrong it might be that TreeUnpickler does more than we think it should do, which would require a fix there. Or we conclude that, indeed, adding assumed infos is necessary. But then in either case we have learned something. By contrast, adding stuff "just in case" tells us nothing.

[odersky]

Maybe that's a deal breaker then. I believe that TastyQuery (or any of the other tools) should not have to know about Gadt constraints. So, maybe we should abandon the effort and stick with casts.

[odersky]

Maybe my problem is that GadtConstraint itself is too complicated. To start with, it sits in the wrong place of the type comparer system: it should be a constraint, but it is really a constraint handler (i.e. a mutable abstraction that encapsulates a constraint field). Then there is all this complication of creating type variables for a real constraint that sits behind it. For type inference, all of this is a bit awkward, and should really be redesigned before we go further. For after type inference, it should have no place whatsoever.

So if assumeInfo should work, it should be decoupled from GadtConstraint.

My recommendation would be to stop all work for now on extending GadtConstraints until we have a better core design that we can actually understand.

[odersky]

What we could do (maybe, eventually):

• Change the context so that instead of a GadtConstraint it just contains a map from symbols to infos.
• TypeComparer would consult that map and, if a symbol has an entry, try that entry for comparisons.
• The entry could be a type variable linked to a GadtConstraint, but that's the business of Typer. Context knows nothing about this.
• We might also need to refactor GadtConstraint to split it into a real constraint and a handler (I know less about this part, just feel uncomfortable with the way it is done now).

[sjrd]

• Change the context so that instead of a GadtConstraint it just contains a map from symbols to infos.
• TypeComparer would consult that map and, if a symbol has an entry, try that entry for comparisons.

FWIW, this is also how I imagine tasty-query would deal with AssumeInfo, and with opaque type aliases. A map of symbols to infos for AssumeInfo handling, and a set of opaque type alias symbols that must be treated as translucent.

[dwijnand]

That all sounds good to me. I'll see what I can do and we can chat about it.

[odersky]

FWIW, this is also how I imagine tasty-query would deal with AssumeInfo, and with opaque type aliases. A map of symbols to infos for AssumeInfo handling, and a set of opaque type alias symbols that must be treated as translucent.

Interestingly, it does not work for opaque type aliases. My first attempt was to model them with Gadt constraints, but it turned out that was too weak. Gadt constraints are too weak in the sense that they come into play only for subtyping. On the other hand, member selection or basetype computation does not take Gadt constraints into account. I tried to change that so that Gadt constraints would be consulted in more situations but that ran into a lot of problems.

That's why we based opaque type aliases on self types, following an idea of Adriaan. The idea is that an opaque type alias should have essentially the same power as a combo of an abstract type in an interface and a type alias in the implementation. Just without having to split it into interface and implementation. Refining the self type can achieve that, but Gadt constraints do not.

[sjrd]

Gadt constraints are too weak in the sense that they come into play only for subtyping.

Right, but nothing says we have to follow the model of Gadt constraints in tasty-query. We can implement member lookup with the knowledge of which opaque type aliases are translucent and which aren't.

[odersky]

Right, but nothing says we have to follow the model of Gadt constraints in tasty-query. We can implement member lookup with the knowledge of which opaque type aliases are translucent and which aren't.

Yes, and baseType computation, that was the harder part. I think it could work. Maybe there will be some subtle differences where the compiler can resolve something but TastyQuery cannot (or vice versa), but maybe that does not matter.

[nicolasstucki]

The documentation of trait reflectModule must be updated