Introduce an attribute to unrefine type arguments #3406
Merged
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This PR allows to tag certain type implicits with the
@@@unrefine
attribute, causing the unifier to attempt to peel away all refinements of the type before instantiating the uvar. With this, ifx
isnat
, the equalityx == x
will happen at typeint
instead ofnat
as currently happens. This can be desirable if we try to relate this fact to, say,0 == 0
, which defaults toint
as0
is an int literal.This is potentially controversial and can break some code, see also the
do_not_unrefine
attribute to fix some regressions. Hence, this logic is only enabled if--debug __unrefine
is passed (I will turn this into an extension flag--ext
, but the extension mechanism is currently inefficient and I don't want to slow down F*).