Use the MkProjectors tactic for all typeclasses

[mtzguido]

This tactic deprecates (in fact removes) the mk_class tactic in typeclasses and instead uses the MkProjectors tactic all classes too, by default. This tactic is meant to generate projectors that are easily typechecked, without SMT, and the relevant methods (defined to be an application of the projector). This tactic is used for all classes by default, but not for all types. This makes thing like these work out of the box:

unfold
let maybe_ghost (b:bool) (post : unit -> prop) =
  if b
  then unit -> squash (post ())
  else unit -> squash (post ())

class r (p:Type) = {
   ghost : bool;
   pred : p -> prop;
   ( ! ) : y:p -> maybe_ghost ghost (fun _ -> pred y);
}

while they currently fail (see #3166), unless we use the meta_projectors attribute to ask to use the tactic explicitly.

The default is not yet flipped for any other type. I can do that next.

[mtzguido]

module X
[@@FStar.Tactics.MkProjectors.meta_projectors]
(* type t = { x : int; y:int } *)
type t = | Mk : int -> bool -> t

let foo (x:t) = x._1

This fails to extract

[mtzguido]

A note: the tactic helps a lot for typechecking time (using intros makes a huge difference), but there's still the time for SMT-encoding the projectors, which are big matches. This can be avoided by using the Projector attribute and reusing the SMT projectors, but I haven't fully deciphered how that all works, it's worth a note in doc/ref.

Also, the "startup" time for the tactic seems high. I clocked at ~2s to just call collect_arr_bs of the constructor type on a large class (~100 methods). That's really bad, especially since this is a plugin.