Limited rewording of some code comments

core/src/typecheck/mod.rs

@@ -1940,12 +1940,12 @@ fn check<V: TypecheckVisitor>(
             // case of the match expression. From there, the type of a valid argument for the match
             // expression is ideally the union of each pattern type.
             //
-            // For record types, we don't have any good way to express union: for example, what
-            // could be the type of something that is either `{x}` or `{y}`? In the case of record
-            // types, we just take the intersection of the types, which amounts to unify all
-            // pattern types together. While it might fail most of the time (including for `{x}`
-            // and `{y}`), it can typecheck interesting expressions when the goal is rather to
-            // match on a subfield, for example:
+            // For record types, we don't have a good way to express union: for example, what could
+            // be the type of something that is either `{x : a}` or `{y : a}`? In the case of
+            // record types, we thus just take the intersection of the types, which amounts to
+            // unify all pattern types together. While it might fail most of the time (including
+            // for the `{x}` and `{y}` example), it can still typecheck interesting expressions
+            // when the record pattern are similar enough:
             //
             // ```nickel
             // x |> match {
@@ -1962,12 +1962,10 @@ fn check<V: TypecheckVisitor>(
             // ?b |]`, unify them together, and close the result (unify the tail with an empty row
             // tail). The advantage of this approach is that unification takes care of descending
             // into record types and sub-patterns to perform this operation, and we're back to the
-            // same procedure (almost) than for record patterns: unify all pattern types. Although
-            // we have additional bookkeeping to perform (closing the right row types at the end of
-            // the procedure).
-            //
-            // This bookkeeping is performed at least partially by the
-            // `typecheck::pattern::PatternTypes::pattern_types` function.
+            // same procedure (almost) than for record patterns: simply unify all pattern types.
+            // Although we have additional bookkeeping to perform (remember the tail variables
+            // introduced to open enum rows and close the corresponding rows at the end of the
+            // procedure).
 
             // We zip the pattern types with each case
             let with_pat_types = data
@@ -2020,7 +2018,7 @@ fn check<V: TypecheckVisitor>(
                     .sum(),
             );
 
-            // We don't immediatly return if an error occurs while unifying the patterns together.
+            // We don't immediately return if an error occurs while unifying the patterns together.
             // For error reporting purposes, it's best to first close the tail variables (if
             // needed), to avoid cluttering the reported types with free unification variables
             // which are mostly an artifact of our implementation of typechecking pattern matching.
@@ -2050,18 +2048,18 @@ fn check<V: TypecheckVisitor>(
             // We unify the expected type of the match expression with `arg_type -> return_type`.
             //
             // This must happen last, or at least after having closed the tails: otherwise, the
-            // expected type could unduely unify some of the tails with rigid type variables. For
-            // example, take:
+            // enum type inferred for the argument could be unduly generalized. For example, take:
             //
             // ```
             // let exp : forall r. [| 'Foo; r |] -> Dyn = match { 'Foo => null }
             // ```
             //
             // This must not typecheck, as the match expression doesn't have a default case, and
             // its type is thus `[| 'Foo |] -> Dyn`. However, during the typechecking of the match
-            // expression, before tails are closed, the working type is `[| 'Foo; _erows_a |]`. If
-            // we would unify with `[| 'Foo; r |]` before closing the tail, this would succeed (and
-            // closer later would be a no-op), which isn't what we want.
+            // expression, before tails are closed, the working type is `[| 'Foo; _erows_a |]`,
+            // which can definitely unify with `[| 'Foo; r |]` while the tail is still open. If we
+            // close the tail first, then the type becomes [| 'Foo |] and the generalization fails
+            // as desired.
             //
             // As a safety net, the tail closing code panics (in debug mode) if it finds a rigid
             // type variable at the end of the tail of a pattern type.

core/src/typecheck/pattern.rs

@@ -55,22 +55,21 @@ pub struct PatternTypeData<T> {
     ///
     /// ```nickel
     /// match {
-    /// 'Foo ('Bar x) => <exp>,
-    /// 'Foo ('Qux x) => <exp>,
-    /// _ => <exp>
+    ///   'Foo ('Bar x) => <exp>,
+    ///   'Foo ('Qux x) => <exp>,
+    ///   _ => <exp>
     /// }
     /// ```
     ///
-    /// The presence of a default case means that the row variable of top-level enum patterns might
-    /// stay open. However, the type corresponding to the sub-patterns `'Bar x` and `'Qux x` must
-    /// be closed, because this match expression can't handle `'Foo ('Other 0)`. The type of the
-    /// expression is thus `[| 'Foo [| 'Bar: a, 'Qux: b |]; c|] -> d` where `a`, `b`, etc. are free
-    /// unification variables.
+    /// The presence of a default case means that the row variables of top-level enum patterns
+    /// might stay open. However, the type corresponding to the sub-patterns `'Bar x` and `'Qux x`
+    /// must be closed, because this match expression can't handle `'Foo ('Other 0)`. The type of
+    /// the expression is thus `[| 'Foo [| 'Bar: a, 'Qux: b |]; c|] -> d`.
     ///
-    /// Currently, only the top-level enum patterns are stored can have a default case, hence only
-    /// the top-leve enum patterns might stay open. However, this might change in the future, as a
-    /// wildcard pattern `_` is common and could then appear at any level of a pattern, making the
-    /// potential other enum at the same path to stay open as well.
+    /// Currently, only the top-level enum patterns can have a default case, hence only the
+    /// top-leve enum patterns might stay open. However, this might change in the future, as a
+    /// wildcard pattern `_` is common and could then appear at any level, making the potential
+    /// other enum located at the same path to stay open as well.
     ///
     /// See [^typechecking-match-expression] in [typecheck] for more details.
     pub enum_open_tails: Vec<(PatternPath, UnifEnumRows)>,
@@ -123,15 +122,16 @@ pub fn close_enum(tail: UnifEnumRows, state: &mut State) {
                 }
                 GenericUnifEnumRowsIteratorItem::TailVar(_)
                 | GenericUnifEnumRowsIteratorItem::TailConstant(_) => {
-                    // While unifying open enum rows coming from a pattern, we expect to always extend the
-                    // enum row with other open rows such that the result should always stay open.
-                    // So we expect to find a unification variable at the end of the enum row.
+                    // While unifying open enum rows coming from a pattern, we expect to always
+                    // extend the enum row with other open rows such that the result should always
+                    // stay open. So we expect to find a unification variable at the end of the
+                    // enum row.
                     //
                     // But in fact, all the tails for a given pattern path will point to the same
                     // enum row, so it might have been closed already by a previous call to
                     // `close_enum`, and that's fine. On the other hand, we should never encounter
-                    // a rigid type variable here (or a non-substituted type variable, although
-                    // it's less specific to patterns), so if we reach this point, something is
+                    // a rigid type variable here (or a non-substituted type variable, although it
+                    // has nothing to do with patterns), so if we reach this point, something is
                     // wrong with the typechecking of match expression.
                     debug_assert!(false);