Merge pull request #3083 from mtzguido/3081

Fixing #3081

src/typechecker/FStar.TypeChecker.TcTerm.fst

@@ -1754,7 +1754,8 @@ and tc_value env (e:term) : term
     let c, uc, f = tc_comp env c in
     let e = {U.arrow bs c with pos=top.pos} in
     (* checks the SMT pattern associated with this function is properly defined with regard to context *)
-    check_smt_pat env e bs c;
+    if not env.phase1 then
+      check_smt_pat env e bs c;
     (* taking the maximum of the universes of the computation and of all binders *)
     let u = S.U_max (uc::us) in
     (* create a universe of level u *)

tests/bug-reports/Bug3081.fst

@@ -0,0 +1,36 @@
+module Bug3081
+
+// Fail if we warn about missing a variable in an SMTPat
+#set-options "--warn_error @271"
+
+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 = ()
+
+val f_lemma_smtpat:
+  {|toto|} ->
+  x:t -> y:t ->
+  Lemma (f x y == g y x)
+  [SMTPat (f x y)]
+  // ^ This pattern mentions the dictionary after tc resolution
+  // so we shouldn't warn.
+let f_lemma_smtpat #toto_instance x y =
+  f_lemma x y
+
+// The SMT pattern works well
+let test_lemma #toto_instance x y z = ()