How to handle names in patterns

[wezm]

Prior to the introduction of booleans in patterns, a name in a pattern always created a new binding that acts a catch-all. The initial implementation of booleans defines true and false in the rigid environment. For these to work in patterns we need to check if a name is defined in the environment and retrieve its value.

There is currently a hack in place to only do this for the names "true" and "false". Without this hack the value of any binding in the environment can be used in a pattern, which can lead to confusion as to when a new binding is created versus matching against the value of an existing one.

Some possible resolutions to this that @brendanzab proposed are:

• special casing true and false (and preventing matching on user-specified definitions) ← this is what we do now
• making variable patterns explicitly different to constant patterns (eg. $x or using capitalisation like in Mercury, Haskell, or OCaml) - this would have a big impact on what Fathom looks like
• making constant patterns different to variable patterns (eg. ^x like in Elixir or perhaps =x)
• just not pursuing pattern matching on constants for now, instead adding if as surface syntax for booleans (which we'll want anyway)

This issue aims to capture this for later consideration.

[Kmeakin]

Resolved by #343?

[brendanzab]

It’s… kind of a solution. I guess if we don’t want to be super exotic then “doing what Rust does” might work? 🤔

[Kmeakin]

The "doing what Rust does" solution seems like a practical low-tech solution:

• In 99% of situations in Rust, you can distinguish between variable bindings and unit enum/struct patterns by capitalization.
• Restrictions on which identifiers can be used in which position (a la Haskell) could make codegen by macros/tools more difficult.
• "uppercase/lowercase" isn't a meaningful concept in many Unicode scripts
• Users may want to break the uppercase/lowercase rule on purpose sometimes, like when using Greek letters with a well-established meaning (eg Γ for the context in typing rules)