search

FStarLang / FStar

A Proof-oriented Programming Language
https://fstar-lang.org
Apache License 2.0
2.7k stars 234 forks source link

Introduce an attribute to unrefine type arguments #3406

Closed mtzguido closed 2 months ago

mtzguido commented 2 months ago

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, if x is nat, the equality x == x will happen at type int instead of nat as currently happens. This can be desirable if we try to relate this fact to, say, 0 == 0, which defaults to int as 0 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*).

TWal commented 2 months ago

If I understand correctly, nothing is changing unless we have the option --debug __unrefine passed to fstar.exe?

mtzguido commented 2 months ago

It's now --ext __unrefine (so it doesn't trigger the common debug output), but yes, this should not be noticeable at all. It can be a breaking change so I'd like to get some experience with it before considering making it default.

If you're curious, you're welcome to try it! It does make many things simpler for me in some Pulse code.