Pattern bound variable name seems to be relevant in trefl

[nikswamy]

@jaylorch reports that the trefl fails in this program

module Test58

let f1 (x: option int) : int =
  match x with
  | None -> 0
  | Some u -> 1

let f2 (x: option int) : int =
  match x with
  | None -> 0
  | Some _ -> 1

let equal_check_failing() : Lemma (f1 == f2) =
  assert (f1 == f2) by FStar.Tactics.trefl ()
  ``

[aseemr]

Looks like a Pat_var vs Pat_wild thing, any other name for the pattern bound variable in f2 works.

[aseemr]

Should Pat_wild unify with any pattern (the branches will anyway be compared after being opened with the pattern variables)?

[nikswamy]

No. This would allow bad things like

match e with | A -> 0 | _ -> 1

to unify with

match e with | _ -> 0 | _ -> 1

Pat_wild should unify with any other variable pattern Pat_var or Pat_wild itself. We might even just remove Pat_wild from the core AST. I think it's there only to support printing it back as an _.

[aseemr]

Yes, makes sense.

[mtzguido]

Hi. I agree that Pat_var and Pat_wild should be made the same, maybe just keeping some metadata to print wildcards back. Meanwhile, I think this patch can make this work OK:

diff --git a/src/syntax/FStar.Syntax.Syntax.fst b/src/syntax/FStar.Syntax.Syntax.fst
index 66a4ed0074..7c5ee19e2f 100644
--- a/src/syntax/FStar.Syntax.Syntax.fst
+++ b/src/syntax/FStar.Syntax.Syntax.fst
@@ -271,6 +271,10 @@ let rec eq_pat (p1 : pat) (p2 : pat) : bool =
         else false
     | Pat_var _, Pat_var _ -> true
     | Pat_wild _, Pat_wild _ -> true
+
+    (* Pat_var and Pat_wild are equivalent *)
+    | Pat_var _, Pat_wild _
+    | Pat_wild _, Pat_var _ -> true
     | Pat_dot_term (bv1, t1), Pat_dot_term (bv2, t2) -> true //&& term_eq t1 t2
     | _, _ -> false

This modifies eq_pat (which checks for syntactic equality), which is used by the unification rule for matches (which is just syntactic as far as patterns go). The only other callers to this are eq_tm and term_eq, and both could benefit from this same change I think?

(Of course this is only OK since Pat_wild also introduces a binder.)