tcresolve: cannot infer in presence of universe variables

[W95Psp]

In the presence of universe variables, tcresolve doesn't work. Consider the following module:

module Bug

class foo (t: Type0): Type = { u: Type }
// or this explicit version, same issue:
// class foo (t: Type0): Type u#(max 1 (n+1)) = { u: Type u#n }

let works {| foo u#m 't |}: foo u#m 't = _ by (FStar.Tactics.Typeclasses.tcresolve ())
[@expect_failure]
let fails {| foo 't |}: foo 't = _ by (FStar.Tactics.Typeclasses.tcresolve ())

The uvars of the top-level fails are basically infered as:

let fails {| foo u#n 't |}: foo u#m 't = _ by (FStar.Tactics.Typeclasses.tcresolve ())

Thus the goal is impossible to fill.