Refinements to skolemizaton #23513
Refinements to skolemizaton #23513
Conversation
The order was the opposite before. That led to skolem types escaping in the constraint and then being installed in the inferred type of a val or def.
There are at least two instances where we might skolemize the type of an argument. One is in safeSubstParams when we compute a result type of a dependent method type application. The other is in constrainIfDependentParamRef where we constrain type variables representing dependent parameters. This used to give several skolem types that ended up in a common OrType. We now store computed skolem types in attachments of argument types and re-use them if possible.
odersky
changed the title
| if arg == null then | ||
| SkolemType(argType) | ||
| else | ||
| arg.getAttachment(Skolemized) match |
There was a problem hiding this comment.
Couldn't it happen that the same argument tree is shared among different application trees? In that case, wouldn't that be wrong to give them the same skolem type?
There was a problem hiding this comment.
Yes, that's indeed a concern. We don't usually share trees but we don't have a guarantee here.
The new scheme works also if argument trees are not unique. Instead of storing skolem types directly in attachment of arguments, we store a map from arguments to their skolems in the enclosing application node. But we check then that the same argument tree does not appear several times in an application. If it does appear several times, we don't generate the map. Furthermore, we are also safe if the whole application tree is used several times, since for each call we generate new skolems and store them in the map. So different calls get different skolems.
|
Commit message of last commit: Refinement: Make scheme work also if arguments are duplicated The new scheme works also if argument trees are not unique. Instead of storing Furthermore, we are also safe if the whole application tree is used several times, |
Deskolemize after fully defining type
The order was the opposite before. That led to skolem types escaping in the constraint and then being installed in the inferred type of a val or def. See Unexpected union of skolems as
Singletontype argument #23489 for a test case where this shows up.Re-use skolems generated for arguments.
Fixes #23489