SizeT: make SizeT.t a new type

[mtzguido]

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?

[msprotz]

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.

[mtzguido]

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.

[msprotz]

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

[cmovcc]

Can confirm that StarMalloc's dist/ is left unchanged by this PR. Thanks for the ping Jonathan!