Decouple quoted Type interface from encoding V2 #9535
Conversation
nicolasstucki
changed the title
nicolasstucki
force-pushed
the
decouple-quoted-type-interface-from-encoding-2
branch
from
22c2f31 to
3b27d0b
Compare
Before, `quoted.Type` was defined as
```scala
// old
class Type[X <: AnyKind]:
type T = X
```
Where `T` is the proper type of the instance of a `Type`. This is the type used for all operations within the compiler.
The only purpose of the type `X` was to be able to write context bounds as `[X: Type]` and staged types `Type[X]` instead of
`Type { type T = X }`.
Unfortunately, the type `X` makes the assumption that `X` is known, which implies that instances of `Type` with unknown types need to be encoded with a whildcard type.
A `val t: Type[?] = ...` is unusable as we cannot heal staged wildcard types, even though we do have a `t.T` which can be handled.
Now, we change the definition of `Type` to only have the type member and rename it to `QuotedType`.
```scala
// new
class QuotedType:
type T <: AnyKind
```
This solves the aforementioned limitations with unkown staged types.
Now we are also able to remove the wildcard from `QuoteContext.tasty.Type.seal` and the result can be used in quotes.
To keep the context bound syntax and provide more descriptive name for the concept, we defined the `quoted.Type` type alias.
```scala
type Type[X <: AnyKind] = QuotedType { type T = X }
```
nicolasstucki
force-pushed
the
decouple-quoted-type-interface-from-encoding-2
branch
from
3b27d0b to
8536c98
Compare
What's special about types with wildcards that prevents them from being healed compared to types with abstract type members? |
|
We do not have a way to recover the tag in some situations as we cannot do an implicit search on |
Does that change if you replace |
|
The issue is that in the first one |
Where does that happen? That seems very wrong to me: a wildcard is a form of existential, it cannot be dealiased in any way without breaking soundness |
Before,
quoted.Typewas defined asWhere
Tis the proper type of the instance of aType. This is the type used for all operations within the compiler.The only purpose of the type
Xwas to be able to write context bounds as[X: Type]and staged typesType[X]instead ofType { type T = X }.Unfortunately, the type
Xmakes the assumption thatXis known, which implies that instances ofTypewith unknown types need to be encoded with a whildcard type.A
val t: Type[?] = ...is unusable as we cannot heal staged wildcard types, even though we do have at.Twhich can be handled.Now, we change the definition of
Typeto only have the type member and rename it toQuotedType.This solves the aforementioned limitations with unkown staged types.
Now we are also able to remove the wildcard from
QuoteContext.tasty.Type.sealand the result can be used in quotes.To keep the context bound syntax and provide more descriptive name for the concept, we defined the
quoted.Typetype alias.Alternative to #9485. This one does not affect the user interface.