Erase functions to fun

[gebner]

Currently all erasable terms are erased to unit. This changes the non_informative function to return an option term instead of bool. This optional term specifies what the type should be erased to. For example, non_informative `(unit -> prop) returns Some `(fun _ -> ()).

There are no user-facing changes, you still write [@@erasable] val foo ... as before. This PR also makes the must_erase_for_extraction attribute a (deprecated) alias of erasable.

Fixes #3366. (only when --cmi is enabled, but we're planning to make that the default anyhow)

[gebner]

Check-world found two interesting regressions:

1. The Inria folks like to treat warnings as errors, which breaks now because the warning number changed.
2. The C code produced by Karamel in merkle-tree doesn't compile due to incorrect function names (?!):

MerkleTree.c: In function 'mt_init_hash':
MerkleTree.c:86:10: error: implicit declaration of function 'MerkleTree_Low_Hashfunctions_init_hash'; did you mean 'MerkleTree_Low_Hashfunctions_free_hash'? [-Werror=implicit-function-declaration]
   86 |   return MerkleTree_Low_Hashfunctions_init_hash(hash_size);
      |          ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
      |          MerkleTree_Low_Hashfunctions_free_hash
MerkleTree.c:86:10: error: returning 'int' from a function with return type 'uint8_t *' {aka 'unsigned char *'} makes pointer from integer without a cast [-Werror=int-conversion]
   86 |   return MerkleTree_Low_Hashfunctions_init_hash(hash_size);
      |          ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

[TWal]

I guess I am the Inria folk who like to treat warning as errors (sorry!), I can disable some more warnings if needed. I am doing this mainly because I was annoyed by the many warnings that shouldn't be warnings (e.g. #2705), but also because I think it's best practice (e.g. to ensure we don't have the proof splitting warning sprinkled throughout the project)

[gebner]

Sorry, that wasn't meant negatively at all! The F* library has lots of warnings too, and I agree it would be nicer to avoid them in the first place.

[TWal]

No worries, didn't take that negatively!

[gebner]

Check-world only reports two regressions now:

• dy-star: I believe this is only must_erase_for_extraction vs. erasable.
• steel: fixes here: https://github.com/FStarLang/steel/pull/204

[gebner]

This does not fix much without #3665, as effect promotion allows coercion from unit -> erased nat to unit -> GTot (erased nat) (giving you essentially the same bug). Shelving this for now until we have a plan for how to deal with the fallout from #3665.