TPZ5712 Constructor name used as a pattern binding

Write Name(patterns) in every pattern position. The payload list has the declared arity. A zero-payload constructor uses Name(), including None() and user enum variants such as Empty(). Nesting does not change this syntax. Parenthesized patterns with the wrong payload count retain the existing constructor-arity diagnostic.

Write Name(arguments) in every value position at every arity. Constructor calls use None(), Empty(), or Some(value). Qualified enum construction uses the same argument list, as in Choice.Empty(). The grammar rejects a bare prelude None value. User enum constructor names are resolved and checked after parsing.

A bare identifier in a pattern attempts to bind a new name. Its capitalization never selects a constructor role. A typed binding uses the same name rule.

The constructor namespace includes prelude constructors, visible declarations and imports, and variants obtained from the known expected type after resolving aliases. A pattern binder that has the same identifier as one of those constructors is rejected with TPZ5712. This check applies at every nested pattern, to typed binders, and to constructors of another visible type. A value binding does not hide a constructor for this check. Choose a fresh name to capture the value or use _ to ignore it.

None is already a reserved binding name. Without the constructor argument list it is rejected during parsing with TPZ2012. Other bare constructor names reach the namespace check. A removed bare enum pattern is never widened into a catch-all.