Redundant alternative error

Stream: lean4

[Yicheng Qian]

Why does the last line produce a "redundant alternative error"? I think that the alternative is not redundant. Moreover, why swapping the last two lines make the error go away?

-- Positive number literal
declare_syntax_cat adig
declare_syntax_cat apos

syntax "⋄" : adig
syntax "‡" : adig
syntax adig : apos
syntax apos adig : apos

-- Arithmetic Expression
declare_syntax_cat aexp

syntax apos : aexp
syntax "⌢" apos : aexp
syntax aexp "⊹" : aexp
syntax aexp "⁻¹" : aexp

-- Continuation
declare_syntax_cat contelem
declare_syntax_cat cont
syntax "|" aexp "]" : contelem
syntax "&neg" : contelem
syntax "&⊹" : contelem
syntax "&⁻¹" : contelem
syntax contelem+ : cont

syntax "`[teval" cont : term


-- Executing continuation, ⊹
macro_rules
|`(`[teval |⌢$n:apos] &⁻¹ $ct*) => `(`[teval| $n:apos] &⊹ &neg $ct*)
|`(`[teval |⌢⋄] &⊹ $ct*) => `(`[teval |‡] $ct*)

[Yicheng Qian]

declare_syntax_cat adig
declare_syntax_cat apos

syntax "⋄" : adig
syntax "‡" : adig
syntax adig : apos
syntax apos adig : apos
syntax "`[|" apos "," adig "]" : term

macro_rules
|`(`[|$_:apos, ⋄]) => `(0)
|`(`[|⋄, ‡]) => `(0)

[Mario Carneiro]

I think this is difficult for the current syntax match to support. You should write the second alternative first

[Mario Carneiro]

Another option is to reorder the match order:

macro_rules
|`(`[|$a, $b]) => match b, a with
  | `(adig| ⋄), _ => `(0)
  | `(adig| ‡), `(apos| ⋄) => `(0)
  | _, _ => Macro.throwUnsupported

[Yicheng Qian]

Thanks!

[Yicheng Qian]

Using match seems to be more flexible.

[Thomas Murrills]

I'm also getting a redundant alternative #2 error, and strangely it seems to be tied to the presence of the syntax category in the match:

syntax myParser := "aa" <|> "bb"

-- Error:
def getMyParserState : TSyntax `myParser -> Bool
| `(myParser|aa) => true
| `(myParser|bb) => false -- redundant alternative #2
| _ => unreachable!

-- Error:
def getMyParserState' : TSyntax `myParser -> Bool
| `(myParser|$stx) => match stx with -- same behavior if using `($stx)
  | `(myParser|aa) => true
  | `(myParser|bb) => false -- redundant alternative #2
  | _ => unreachable!

-- No error:
def getMyParserState'' : TSyntax `myParser -> Bool
| `(myParser|$stx) => match stx with
  | `(aa) => true
  | `(bb) => false
  | _ => unreachable!

(The behavior is the same whether using declare_syntax_cat myParser or def myParser := leading_parser ..., and if TSyntax is abandoned in favor of Syntax.)

1. Is this a bug?
2. Why do I need to include unreachable!? If I leave out the _ case, it says "non-exhaustive match"...but shouldn't it be able to tell that this is exhaustive?

[Mario Carneiro]

update your lean install

[Thomas Murrills]

yay! (so satisfying when a bug is fixed by updating :octopus:)

[Mario Carneiro]

Your examples all compile on nightly. The reason it used to fail is because syntax match does not make use of the content of atoms, so the first arm would match both aa and bb and the second branch is unreachable. The workaround was to add an additional syntax node like so:

syntax aaStx := "aa"
syntax bbStx := "bb"
syntax myParser := aaStx <|> bbStx

Since a few weeks ago this transformation is now done automatically, so syntax match works as expected.

[Mario Carneiro]

The unreachable! case is not formally unreachable, since you can always lie and put some garbage in a TSyntax. More importantly, you always have to be prepared to receive a Syntax.missing, which most parsers will produce if the syntax they were parsing was malformed in some way

[Thomas Murrills]

Nice, thanks! That explanation is very useful—now I know how to deal with things manually via leading_parser too. :) Ah, that makes sense (re: unreachable!)!

[Kyle Miller]

For metaprogramming purposes, I want to generate match expressions that have a fallback case (like elab_rules etc), and I want to allow this to be a redundant alternative. It looks like I should be able to use no_error_if_unused% to mark possibly redundant cases, but I'm not able to get it to work:

#check match 1 with | _ => true | _ => no_error_if_unused% false
#check ((fun | _ => true | _ => no_error_if_unused% false) : Nat → Bool)
-- both have "redundant alternative" error

[Kyle Miller]

Should I be using no_error_if_unused%? Or is there another way I can give match/fun a fallback case?

[Kyle Miller]

Oh, no_error_if_unused% is only for match applied to syntax (Lean.Elab.Quotation). There's no such facility for general match syntax (Lean.Elab.Match), other than the option match.ignoreUnusedAlts