You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
This is a new encoding of HOLE that differentiates between type and term
arguments of the hole.
```
-- pickled quote trees: These trees can only appear in pickled quotes. They will never be in a TASTy file.
EXPLICITtpt tpt_Term
-- Tag for a type tree that in a context where it is not explicitly known that this tree is a type.
HOLE Length idx_Nat tpe_Type arg_Tree*
-- Splice hole with index `idx`, the type of the hole `tpe`, type and term arguments of the hole `arg`s
```
We will pickle type trees in `arg_Tree` using the `EXPLICITtpt` tag.
We will only have hole captured types if there is a type defined in a
quote and used in a nested quote. Most of the time we do not have those
types and therefore no overhead in the encoding compared to before this
change.
Alternative to #17225Fixes#17137
0 commit comments