I agree. My issue with "redundant branch" wording is that it makes me think that I can clean something up because these branches "do the same thing". But as you point out, in this case Dafny means "I will never go into that branch".
If I have 2 copies of the same function that do the same thing, one of them is redundant.
However, I would never expect that callsites for the redundant function would never execute.
Not exactly the same example, I know. But it was how I was interpreting that warning.

Oh, it looks like my recent issue #1789 is a duplicate of this one.

I thought of another way we could attack this. The code sample should also produce a style warning something along the lines of:

Warning: variable names should begin with a lowercase letter: "ShadesOfGray" 

That's a lot shorter than trying to explain the specific situation.

A related but slightly different issue: #1991

Which gives the following example:

datatype D = C1 | C2 | C3

var x: D = ...
match x {
    case C1 /* matches type C1 */ => ...
    case C2 /* matches type C2 */ => ...
    case C4 /* binds variable C4 */ => ...
}
vs
match x {
    case C1() /* matches constructor C1() */ => ...
    case C2() /* matches constructor C2() */ => ...
    case C4() /* ERROR, no constructor C4 */ => ...
}

The bigger issue seems to be that the syntax for capturing a variable and matching a datatype constructor is too similar. The imagined warning:

Warning: "ShadesOfGray" on line 5 is used as a variable, but it is also the name of a constructor that can be written here. If you intended to write a pattern that uses this constructor, add the parameters, like `ShadesOfGray(_)`.

Works for the case where the captured variable has the exact name of the constructor, but not for the case where a name that's not a constructor is captured as a variable, even though the programmer intended to match on a constructor.

An alternative solution would be a flag "strictMatchCases" that gives a warning for any case where a datatype constructor is not followed by parenthesis.

I thought of another way we could attack this. The code sample should also produce a style warning something along the lines of:

I like that but maybe that would make most sense if the language also came with a standard code style that's enforced through compiler warnings and for which there's an automated formatter.