Refutable vs. Failable Patterns

# What is the problem

The Haskell report defines `refutable/irrefutable` patterns. MonadFail desugaring requires `failable/failure-free` patterns. These two concepts are not the same, but GHC seems to confuse them. We need to define them precisely for the report.

## Details

The Haskell report introduces the notion of *refutable* or *irrefutable* patterns in Section 3.17.2.

> It is sometimes helpful to distinguish two kinds of patterns. Matching an irrefutable pattern is non-strict: the pattern matches even if the value to be matched is ⊥. Matching a refutable pattern is strict: if the value to be matched is ⊥ the match diverges. The irrefutable patterns are as follows: a variable, a wildcard, N apat where N is a constructor defined by newtype and apat is irrefutable (see Section [4.2.3](https://www.haskell.org/onlinereport/haskell2010/haskellch4.html#x10-740004.2.3)), var@apat where apat is irrefutable, or of the form ~apat (whether or not apat is irrefutable). All other patterns are refutable.

According to this definition, if a data type contains a single constructor then that constructor forms a refutable pattern. In particular, the expression `f` in the following snippet diverges:

```haskell
data T = MkT

f :: Bool
f = case undefined of { MkT -> True }
```

This terminology does not agree, as far as I can see, with how GHC developers use the term "irrefutable", in particular in the implementation here: https://gitlab.haskell.org/ghc/ghc/-/blob/master/compiler/GHC/Hs/Pat.hs . GHC considers the pattern `MkT` as irrefutable.

The correct term for what GHC is checking here seems to be "failable" pattern, which was the term used in the original MonadFail proposal and in the Haskell 1.4 report (that report calls those patterns "failure-free").
There is a comment in the GHC codebase which mentions this:
> (NB: this is not quite the same as the (silly) defn in 3.17.2 of the Haskell 98 report.)

## The semantic difference between refutable and failable patterns

Refutable and failable patterns can be defined semantically in terms of the result of pattern matching against a value:
Matching a pattern against an expression has one of three possible outcomes:
- Matching *succeeds* with a list of bindings. Example: Matching `(2,4)` against the pattern `(x,y)` succeeds with bindings `x |-> 2, y |-> 4`
- Matching the pattern *fails*, and the next pattern has to be tried in a case expression. Example: Matching the term `True` against `False` fails.
- Matching *diverges*, because the term contains some bottom term that the pattern scrutinizes. Example: Matching the term `undefined` against `True`.

Refutable and failable patterns can then be defined as follows:
- *Irrefutable Pattern*: A pattern is irrefutable if matching against a value can never diverge.
- *Failable Pattern*: A pattern is failure-free if matching against a value can never fail.

In that sense `MkT` is refutable but failure-free.

Start with the Haskell report's Section 3.17.2 and the linked GHC Hs/Pat.hs implementation, then compare the report's refutable/irrefutable terminology with failable or failure-free patterns and the issue's semantic definitions. Done means the revised report defines the two concepts precisely and distinguishes the MkT example without conflating them.

Written by the indexing model from the issue text.