Add refining annotations #4626
Add refining annotations #4626
Conversation
The idea is that such annotations create some proper subtype of the type they annotate. Hence, they cannot be stripped away like normal annotations are.
- some keep their annotations - some only keep refining annotations - most of them still strip all annotations
|
@gsps I recommend to use this status as a basis for further work. Next step could be to define an annotation like library/src/scala/annotation/internal |
| * Refining annotations are more "sticky" than normal ones. They are conceptually kept | ||
| * around when normal refinements would also not be stripped away. | ||
| */ | ||
| trait RefiningAnnotation extends StaticAnnotation |
There was a problem hiding this comment.
Why expose that in the stdlib, isn't this compiler internal only?
There was a problem hiding this comment.
No, you might want to define your own annotations (say units of measure). Maybe they need a compiler plugin to order to be checked, or maybe you can do it in the future with annotation macros. RefiningAnnotation just makes sure they propagate correctly.
In principle, we could consider this. But these two are a little bit different since they are also the main carriers of singleton types. Also the terms they capture are not very general, so it's not clear what we would win. |
There was a problem hiding this comment.
This looks nice! At this point, I'd actually be quite tempted to also add DistributiveRefiningAnnotation along with the appropriate cases to distributiveOr and distributiveAnd ;-)
In any case, I'll give it a shot and try to rebase our WIP transparent PR on this.
| def ClassfileAnnotationClass(implicit ctx: Context) = ClassfileAnnotationType.symbol.asClass | ||
| lazy val StaticAnnotationType = ctx.requiredClassRef("scala.annotation.StaticAnnotation") | ||
| def StaticAnnotationClass(implicit ctx: Context) = StaticAnnotationType.symbol.asClass | ||
| lazy val RefiningAnnotationType = ctx.requiredClassRef("scala.annotation.RefiningAnnotation") |
|
|
||
| /** Does this type have a supertype with an annotation satisfying given predicate `p`? */ | ||
| def derivesAnnotWith(p: Annotation => Boolean)(implicit ctx: Context): Boolean = this match { | ||
| case tp: AnnotatedType => p(tp.annot) || tp.tpe.derivesAnnotWith(p) |
There was a problem hiding this comment.
Consider renaming AnnotatedType#tpe to #parent or #info? (I find tp.tpe slightly confusing.)
| object common { | ||
|
|
||
| val alwaysTrue = Function.const(true) _ | ||
| val alwaysFalse = Function.const(false) _ |
There was a problem hiding this comment.
No. I used it in an intermediate version. I kept it for duality.
| case tycon1: TypeVar => | ||
| isMatchingApply(tycon1.underlying) | ||
| case tycon1: AnnotatedType => | ||
| case tycon1: AnnotatedType if !tycon1.isRefining => |
There was a problem hiding this comment.
I'm not sure when a type constructor would have a RefiningAnnotation, but wouldn't it in principle be okay to widen here, regardless of whether the annotation is refining?
There was a problem hiding this comment.
Yes, well spotted. Narrowing the lower bound is always safe, and it is the only thing we can do in this case.
There was a problem hiding this comment.
Looks like this PR was merged without addressing this comment?
odersky
force-pushed
the
add-refining-annotations
branch
from
a4745fd to
81a5cf9
Compare
|
LGTM. |
| tp1.underlying & tp2 | ||
| case tp1: AnnotatedType => | ||
| case tp1: AnnotatedType if !tp1.isRefining => | ||
| tp1.underlying & tp2 |
There was a problem hiding this comment.
Why not rewrap the annotation around the intersection if it's a refining annotation?
|
|
||
| override def stripAnnots(implicit ctx: Context): Type = tpe.stripAnnots | ||
| def isRefining(implicit ctx: Context) = { | ||
| if (!isRefiningKnown) { |
There was a problem hiding this comment.
Shouldn't the cache be invalidated at the start of a new run?
There was a problem hiding this comment.
I was thinking about that too, but decided that it's probably fine given the internal nature of such annotations. Then again, we do expose RefiningAnnotation in the public scala.annotation package.
|
This PR would really really benefits from having tests. |
4 participants
Adds a new kind of annotation that conceptually refines the annotated type. That is, refining annotations yield subtypes. They are more "sticky" than normal annotations. In a number of situations they are not stripped away where normal annotations are.
It is intended that this kind of annotation is a good basis to define
TypeOftypes.