Functional dependencies for typeclasses

[mtzguido]

This PR implements a simple flavor of functional dependencies for typeclasses. A class definition can now be annotated with the fundeps attribute, providing a list of the class arguments that are functionally dependent on the rest. For instance, the following definition represents a class of set-like types s over elements type e.

[@@Tactics.Typeclasses.fundeps [0]]
class setlike (e:Type) (s:Type) = {
  empty         : unit -> s;
  singleton     : e -> s;
  is_empty      : s -> bool;
  add           : e -> s -> s;
  [...]
}

The fundep attribute is indicating the the 0th argument (e) is determined from all other arguments (the complement of the ones listed in the fundep, in this case s).

Assuming we have an instance setlike a (Set.set a), this allows one to write something like is_empty (add 1 (empty ()). That would previously fail, since is_empty being called on a Set.set int, but nothing is constraining e to be int. For example we could also have instance setlike bool (Set.set int), though of course that's not the intention.

This change allows the tcresolve to instantiate some uvars in the goal (something we've been prohibiting so far, see #3134, #3130, #2591). I am now allowing this, only for tcresolve, since I made tcresolve aware of uvars and it should not instantiate uvars willy-nilly, it will only ever instantiate the uvars in the fundeps of a goal.

There is currently no check for the instances actually respecting the dependencies... so if the user states a functional dependency and does not respect it, some unexpected behavior may occur. This is basically an overlap check which we do not do for non-fundep classes either.

cc @TWal who may find this interesting.

[TWal]

This definitely looks interesting, thanks!