FStarLang
SizeT: make SizeT.t a new type
This PR improves responsiveness whenever we use a SizeT.t in a context where it is wrong to do so, like if the expected type is int (and we forgot the v). Instead of trying to prove int == SizeT.t by SMT, F* will now just fail during typechecking/unification. All other integer types already use new.
To do this, we must redefine SizeT.t as a fresh inductive, otherwise we cannot claim that it is new. I wonder if there's a reason against this, since I remember that this module had some custom extraction rules. Maybe @R1kM or @msprotz know?
I think the custom extraction rules are in FStar.Extraction.Krml.fs and as long as you can still pattern-match just like before, it should be good.
I think before the new keyword existed, you had to do something like:
type t = t'
type t' = | T: ...
and then sometimes in reduction you would see one or another which complicated the custom extraction. But that was ages ago, and I'm not even sure I remember this correctly.
I got an everest green locally, so I think this should be fine. Also HACL* dist had no diff, but I'm not sure if it's still regenerated on every make? I'm merging, please report if you find anything weird.
sadly HACL* has not been switched over to use sizet so I'm not surprised there's no diff there -- ping @cmovcc though for the starmalloc diff
Can confirm that StarMalloc's dist/ is left unchanged by this PR. Thanks for the ping Jonathan!
