F* wrongly allows non-linear patterns

[catalin-hritcu]

Recently discovered with @kyoDralliam that F* allows non-linear patterns:

let foo() : Tot int =
  match (1,2) with
  | (x,x) -> x

This is hugely unintuitive for users. Is this match complete? Does it equate the two elements of the pair? If not is this returning 1 or 2?

[cpitclaudel]

FTR "yes", "no", 2. I agree it's unintuitive.

Ocaml and F# complain:

# let foo : int =
  match (1,2) with
  | (x,x) -> x;;

    Characters 42-43:
    | (x,x) -> x;;
         ^
Error: Variable x is bound several times in this matching

> let foo : int =
  match (1,2) with
  | (x,x) -> x;;

    | (x,x) -> x;;
  -------^

stdin(3,8): error FS0038: 'x' is bound twice in this pattern

[nikswamy]

Probably an easy fix in FStar.ToSyntax.ToSyntax.fs, in desugar_data_pat. There's a check_linear_pattern_variables at the end of that function, which apparently does not do the right thing.

[mtzguido]

A PR for this: #1309

[mtzguido]

I merged it, fixed by 2554cc1