I was following along Imp chapter of the Software Foundations textbook (found here at Benjamin Pierce’s webpage) and I got stuck pretty early on. By follow along, I mean I was retyping everything in the chapter so that I could be an active participant in the “reading along process.”
Here’s what the chapter says to do:
Inductive bexp : Type := | BTrue : bexp | BFalse : bexp | BEq : aexp → aexp → bexp | BLe : aexp → aexp → bexp | BNot : bexp → bexp | BAnd : bexp → bexp → bexp.
Here’s what I wrote.
Inductive bexp : Type := | BTrue : bexp | BFlase : bexp | BEq : aexp → aexp → bexp | BLe : aexp → aexp → bexp | BNot : bexp → bexp | BAnd : bexp → bexp → bexp.
Did you catch the difference? Well I didn’t, and neither did Coq, because frankly, it doesn’t care what you call your constructors – nor, should it.
Fast forward to the first time we tried to use the definition of bexp.
Fixpoint beval (e : bexp) : bool := match e with | BTrue => true | BFalse => false | BEq a1 a2 => beq_nat (aeval a1) (aeval a2) (* Error on this line*) | BLe a1 a2 => ble_nat (aeval a1) (aeval a2) | BNot b1 => negb (beval b1) | BAnd b1 b2 => andb (beval b1) (beval b2) end.
And we’re met with the supremely helpful message: Error: This clause is redundant.
Because the definition of bexp had a typo, there is no “BFalse” constructor. Instead, the BFlase in the pattern match of the defintion beval is a pattern match variable matching anything. So between the BTrue case and the “everything else” case, all patterns are matched making anything below the seemingly correct “BFalse” redundant.
Yes, perhaps it was a careless typo that caused the problem, but a more descriptive error message would have been really helpful. Having just run into this today, I don’t know if there exists some solution for catching this earlier, but here’s ideas I had.
- Warning mode: Warns when a “catch” all pattern is used. (Maybe only warns if the pattern is a variable instead of an underscore)
- Enhance the error message with “This clause is redundant because SomeOtherClause already caught this pattern.”