Closed tribbloid closed 9 months ago
I propose to add the Vtype-detail
plugin option which takes an integer:
<= 1
: status quo behaviour=2
: attach underlying type for dependent type (use Type.toLongString
instead of Type.safeToString
)=3
: in addition, attach existential context for existential types>=4
: in addition, attach type alias explanation for type alias before reduction/normalisation (you probably won't see it without enabling feature for #101)@tek what do you think?
Considering the example:
The original error:
is good enough if you read the code carefully and memorize the definition of every dependent types (in the function or the object), but it may be difficult for people without a background in dependent type theory. This is why Scala compiler 2.13 builtin diff use the following implementation:
Should we optionally do the same?