Inference does not know about fundeps

[mtzguido]

module Bug

open FStar.Tactics.Typeclasses

[@@fundeps [1]]
class pts_to (a b : Type) = {
  foo : a -> b -> bool;
}

type box a = | B of x:a

instance pts_to_box (a:Type) : pts_to (box a) a = {
  foo =(fun _ _ -> true);
}

let test1 (x : box nat) = foo x 1
let test2 (x : box nat) = foo #_ #_ #(pts_to_box _) x 1 // forces the right instantiations

Above, test1 fails, since the unifier elaborated the body to foo #(box nat) #int #?d x 1, given the types of x and 1. However, the instance we want (and the only valid one) for ?d is pts_to_box nat, which means that the second implicit should be nat.

Given that that implicit is a functional dependency of the first, it would make sense to delay instantiating until we have solved the first one and ran a round of typeclass resolution. But, currently, the typechecker knows nothing at all about functional dependencies, it is just a check performed by tcresolve. Maybe we can add a tag to fundep set to prevent this, but probably the right thing is a closer interoperation between the typechecker/unifier and tactics like tcresolve.   Note that @@unrefine (#3406) does not help.