F* (wrongly?) says SMT pattern miss bound variable when using typeclasses

[TWal]

See the following example. F* complains that the typeclass instance is not captured by the SMT pattern, but the SMT pattern works fine.

assume val t: Type0

class toto = {
  f: t -> t -> t;
  g: t -> t -> t;
  f_lemma: x:t -> y:t -> squash (f x y == g y x);
}

// Lemma that can be proven using f_lemma twice
val test_lemma:
  {|toto|} ->
  x:t -> y:t -> z:t ->
  Lemma
  (f x (f y z) == g (g z y) x)

// It can't be proven automatically
[@@expect_failure]
let test_lemma #toto_instance x y z = ()

// We create a lemma with SMT pattern.
// F* says: Pattern misses at least one bound variable: ...
val f_lemma_smtpat:
  {|toto|} ->
  x:t -> y:t ->
  Lemma (f x y == g y x)
  [SMTPat (f x y)]
let f_lemma_smtpat #toto_instance x y =
  f_lemma x y

// However the SMT pattern works well
let test_lemma #toto_instance x y z = ()

If we write the instance explicitly the error disappear, although I would have thought it is equivalent to the code above?

val f_lemma_smtpat:
  {|toto_instance:toto|} ->
  x:t -> y:t ->
  Lemma (f x y == g y x)
  [SMTPat (f #toto_instance x y)]
let f_lemma_smtpat #toto_instance x y =
  f_lemma x y

What is happening here, is there really something wrong with the first SMT pattern?

[mtzguido]

Thanks for the report Théophile! Pushing a fix for this. What is happening is that F* is checking that all arguments of the lemma are mentioned in the pattern before doing typeclass resolution, and giving a false warning. The pattern is itself fine.

[TWal]

Great, thanks!