Docs: Update subtyping rules to reflect the impl

See https://github.com/lampepfl/dotty/blob/9982f0dced80d96cf5ca01f89ad68d969b9516ba/compiler/src/dotty/tools/dotc/core/TypeComparer.scala#L814-L816

Where we check for equality of scrutinees

And https://github.com/lampepfl/dotty/blob/9982f0dced80d96cf5ca01f89ad68d969b9516ba/library/src/scala/internal/MatchCase.scala#L5

Where the pattern of a match case is invariant, meaning we also use
equality for those.

Author: OlivierBlanvillain

docs/docs/reference/new-types/match-types.md

@@ -85,12 +85,12 @@ is `Match(S, C1, ..., Cn) <: B` where each case `Ci` is of the form
 ```
 [Xs] => P => T
 ```
+
 Here, `[Xs]` is a type parameter clause of the variables bound in pattern `Pi`. If there are no bound type variables in a case, the type parameter clause is omitted and only the function type `P => T` is kept. So each case is either a unary function type or a type lambda over a unary function type.
 
 `B` is the declared upper bound of the match type, or `Any` if no such bound is given.
 We will leave it out in places where it does not matter for the discussion. Scrutinee, bound and pattern types must be first-order types.
 
-
 ## Match type reduction
 
 Match type reduction follows the semantics of match expression, that is, a match type of the form `S match { P1 => T1 ... Pn => Tn }` reduces to `Ti` if and only if `s: S match { _: P1 => T1 ... _: Pn => Tn }` evaluates to a value of type `Ti` for all `s: S`.
@@ -115,28 +115,36 @@ Disjointness proofs rely on the following properties of Scala types:
 The following rules apply to match types. For simplicity, we omit environments and constraints.
 
 The first rule is a structural comparison between two match types:
+
 ```
-Match(S, C1, ..., Cm) <: Match(T, D1, ..., Dn)
+S match { P1 => T1 ... Pm => Tm }  <:  T match { Q1 => U1 ... Qn => Un }
 ```
+
 if
+
 ```
-S <: T,  m >= n,  Ci <: Di for i in 1..n
+S =:= T,  m >= n,  Pi =:= Qi and Ti <: Qi for i in 1..n
 ```
-I.e. scrutinees and corresponding cases must be subtypes, no case re-ordering is allowed, but the subtype can have more cases than the supertype.
+
+I.e. scrutinees and patterns must be equal and the corresponding bodies must be subtypes. No case re-ordering is allowed, but the subtype can have more cases than the supertype.
 
 The second rule states that a match type and its redux are mutual subtypes
+
 ```
-  Match(S, Cs) <: T
-  T <: Match(S, Cs)
+S match { P1 => T1 ... Pn => Tn }  <:  U
+U  <:  S match { P1 => T1 ... Pn => Tn }
 ```
+
 if
+
 ```
-  Match(S, Cs)  reduces-to  T
+S match { P1 => T1 ... Pn => Tn }  reduces-to  U
 ```
 
-The third rule states that a match type conforms to its upper bound
+The third rule states that a match type conforms to its upper bound:
+
 ```
-  (Match(S, Cs) <: B)  <:  B
+(S match { P1 => T1 ... Pn => Tn } <: B)  <:  B
 ```
 
 ## Variance Laws for Match Types