Revising coercion mechanism to allow for implicit arguments

[mtzguido]

This allows to define coercions like this the one below:

[@@coercion]
let int_to_bv1 (#n : pos) (x : int) : Pure (BV.bv_t n) (requires fits x n) (ensures fun _ -> True)  = BV.int2bv x

or

[@@coercion]
let lseq (#a:Type) (l:list a) : seq a = seq_of_list l

let x : seq int = [1;2;3;4]                                           

which are parametrized by an implicit an universes.

The previous mechanism only allowed for coercions of type a -> b, where both a and b had to be top-level names without any arguments (e.g. term and term_view). This relaxes the shape to allow for coercions of shape x1:t1 -> ... -> xn:tn -> a a_args -> b b_args, with any amount of argument before the last one (which should be implicit so they can be solved, but that's not required by this code) and allowing a and b to be applied to any number of expressions.

I still kept the requirement that a and b be top-level names to easily distinguish which coercions may apply, and be as efficient as before for the existing cases. It's these two types which define the coercion to apply, there's no backtracking.

Now, when we have a term e of type a ... and expected type of b ..., we will find the coercion f (if any) and attempt to typechecked f e at type b .... This will instantiate f's implicits and, if it suceeds, we take this elaborated term to be the coerced one.

A different design is possible via typeclasses, but 1) there's a bootstrapping problem to still solve (see #2969 for some related context), 2) they don't work well wrt refinements, while here we can be smarter about them.

cc @bollu who requested this, maybe give this branch a try?

[bollu]

Super, this does indeed work for my use-case! Thanks a lot @mtzguido

module Foo

module U = FStar.UInt
module BV = FStar.BV
open FStar.BV



[@@coercion]
let int_to_bv1 (#n : pos) (x : int) : 
  Pure (BV.bv_t n) (requires U.fits x n) (ensures fun _ ->  True)  = BV.int2bv x

let works : BV.bv_t 2 = 1
let works_complex (#n : pos) (x : int) (prf : U.fits x n) : (BV.bv_t n) = x