Why redundant alternative?

Stream: lean4

[Shreyas Srinivas]

The following is an #mwe:

inductive SampleType : Type where
  | A : SampleType
  | B : SampleType

def f1 (x : SampleType) : String :=
  match x with
  | A => "A"
  | B => "B" -- Error message : redundant alternative


open SampleType

def f2 (x : SampleType) : String :=
  match x with
  | A => "A"
  | B => "B" -- No Errors

In the definition of f1 the namespace(correct term??) corresponding to SampleType is not yet open, so A and B should not be visible and accessible. This is fixed before the definition of f2. However, the error thrown by lean4 in f1 is not that it doesn't know about constructors A and B, but redundant alternative. Why?

[Arthur Paulino]

If you don't open SampleType, then A and B are understood as variables, not the constructors of SampleType

It's like saying:

def f1 (x : SampleType) : String :=
  match x with
  | x => "A"
  | y => "B"

[Shreyas Srinivas]

Even inside a match arm's LHS?

[Arthur Paulino]

My Lean writing skills are a bit rusty, but the following might work

def f1 (x : SampleType) : String :=
  match x with
  | .A => "A"
  | .B => "B"