Better row unification error messages

CHANGELOG.d/fix_better-row-error-messages.md

@@ -0,0 +1,165 @@
+* Significantly improved `Record`/`Row`-related error messages
+
+  The problems of the prior Record/Row-related error messages
+  are shown below with their updated counterparts. Vertical spacing
+  in the messages is omitted for brevity.
+
+  The errors `ExprDoesNotHaveType`, `PropertyIsMissing`, 
+  and `AdditionalProperty` have been removed, being replaced
+  with `TypesDoNotUnify` instead.
+
+  **Case 1: lack of expected/actual text when that is known**
+
+  The expected/actual distinction is not possible to determine in all cases,
+  but it can be known in some cases. Previously, it was not reported even 
+  if it was known. Now the compiler reports this distinction if known.
+
+  Before:
+  ```
+  Could not match type
+    X
+  with type
+    Y
+  ```
+  After:
+  ```
+  The actual type
+    X
+  does not match the expected type
+    Y
+  ```
+
+  **Case 2: reporting only the first additional label**
+
+  Before:
+  ```
+  Type of expression contains additional label extraLabel1
+  ```
+  After:
+  ```
+  The actual type
+    { extraLabel1 :: Int
+    , extraLabel2 :: Int
+    }
+  does not match the expected type
+    { ... }
+  ```
+
+  **Case 3: reporting only the first missing label**
+
+  Before:
+  ```
+  Type of expression lacks required label age
+  ```
+  After:
+  ```
+  The actual type
+    { first :: String
+    , last :: String
+    ...
+    }
+  does not match the expected type
+    { age :: Number
+    ...
+    | t0
+    }
+  ```
+
+  **Case 4: reporting all of two large records rather than just their differences**
+
+  Before:
+  ```
+  Could not match type
+    ( a :: Int
+    , b :: Int
+    , c :: Int
+    , d :: Int
+    , e :: Int
+    , f :: Int
+    , h :: Int
+    , j :: Int
+    ...
+    )
+  with type
+    ( a :: t7
+    , b :: t6
+    , c :: t5
+    , d :: t4
+    , e :: t3
+    , f :: t2
+    , g :: t1
+    ...
+    | t8
+    )
+  ```
+  After:
+  ```
+  Could not match type
+    ( h :: Int
+    , j :: Int
+    ...
+    )
+  with type
+    ( g :: t1
+    ...
+    | t8
+    )
+  ```
+
+  **Case 5: reporting only the first `TypesDoNotUnify` error rather than all such errors on record pattern matches whose labels are a subset of the expected record's labels**
+
+  The following behavior is unchanged, but it is explained to clarify
+  the next summary.
+
+  When pattern matching on a record where the pattern match's labels
+  differ from the labels of the expected record (e.g. from a type signature),
+  a `TypesDoNotUnify` error is thrown showing a diff between the two records' labels,
+  regardless of whether their corresponding types unify.
+
+  ```purs
+  data ExpectedType = ExpectedValue
+  data SomeOtherType = DifferentValue
+
+  {-  
+  Produces one error for the entire record; behavior unchanged.
+
+    The type
+      ( a :: ExpectedValue
+      , b :: String
+      )
+    does not unify with type
+      ( x :: SomeOtherType
+      , y :: Int
+      )
+  -}
+  test :: { a :: ExpectedType, b :: String } -> Int
+  test { x: DifferentValue, y: 7 } = 1
+  ```
+
+  However, if the labels in the pattern match are a subset of the labels
+  in the expected record, then previously a `TypesDoNotUnify` error is thrown
+  for only the _first_ detected error. Now, such an error is thrown
+  _for each_ type that fails to unify.
+
+  ```purs
+  data ExpectedType = ExpectedValue
+  data SomeOtherType = DifferentValue
+
+  data A = A
+
+  -- Errors thrown in previous behavior:
+  -- - under label sameLabel1, `TypesDoNotUnify ExpectedType SomeOtherType`
+  --
+  -- Errors thrown in new behavior:
+  -- - under label sameLabel1, `TypesDoNotUnify ExpectedType SomeOtherType`
+  -- - under label sameLabel2, `TypesDoNotUnify String Int`
+  test :: { sameLabel1 :: ExpectedType, sameLabel2 :: String, sameLabel3 :: A } -> Int
+  test { sameLabel1: DifferentValue, sameLabel2: 7, sameLabel3: A } = 1
+  ```
+
+  **Case 6: printing `Record row` using native syntax**
+
+  | Before | After |
+  | - | - |
+  | `Record ()` | `{}` |
+  | `Record (...)` | `{ ... }` |

purescript.cabal

@@ -169,7 +169,6 @@ common defaults
     clock >=0.8.3 && <0.9,
     containers >=0.6.5.1 && <0.7,
     cryptonite ==0.30.*,
-    data-ordlist >=0.4.7.0 && <0.5,
     deepseq >=1.4.6.1 && <1.5,
     directory >=1.3.6.2 && <1.4,
     dlist ==1.0.*,
@@ -386,6 +385,7 @@ library
     Language.PureScript.TypeChecker.Types
     Language.PureScript.TypeChecker.TypeSearch
     Language.PureScript.TypeChecker.Unify
+    Language.PureScript.TypeChecker.Unify.Rows
     Language.PureScript.TypeClassDictionaries
     Language.PureScript.Types
     System.IO.UTF8

src/Language/PureScript/Errors.hs

@@ -10,7 +10,7 @@ import Control.Arrow ((&&&))
 import Control.Exception (displayException)
 import Control.Lens (both, head1, over)
 import Control.Monad (forM, unless)
-import Control.Monad.Error.Class (MonadError(..))
+import Control.Monad.Error.Class (MonadError(..), liftEither)
 import Control.Monad.Trans.State.Lazy (State, evalState, get, put)
 import Control.Monad.Writer (Last(..), MonadWriter(..), censor)
 import Data.Bifunctor (first, second)
@@ -47,7 +47,7 @@ import Language.PureScript.Pretty.Common (endWith)
 import Language.PureScript.PSString (decodeStringWithReplacement)
 import Language.PureScript.Roles (Role, displayRole)
 import Language.PureScript.Traversals (sndM)
-import Language.PureScript.Types (Constraint(..), ConstraintData(..), RowListItem(..), SourceConstraint, SourceType, Type(..), eraseForAllKindAnnotations, eraseKindApps, everywhereOnTypesTopDownM, getAnnForType, isMonoType, overConstraintArgs, rowFromList, rowToList, srcTUnknown)
+import Language.PureScript.Types (Constraint(..), ConstraintData(..), RowListItem(..), SourceConstraint, SourceType, Type(..), eqType, eraseForAllKindAnnotations, eraseKindApps, everywhereOnTypesTopDownM, getAnnForType, isMonoType, overConstraintArgs, rowFromList, rowToList, srcTUnknown)
 import Language.PureScript.Publish.BoxesHelpers qualified as BoxHelpers
 import System.Console.ANSI qualified as ANSI
 import System.FilePath (makeRelative)
@@ -104,7 +104,10 @@ data SimpleErrorMessage
   | UndefinedTypeVariable (ProperName 'TypeName)
   | PartiallyAppliedSynonym (Qualified (ProperName 'TypeName))
   | EscapedSkolem Text (Maybe SourceSpan) SourceType
-  | TypesDoNotUnify SourceType SourceType
+  | TypesDoNotUnify
+      Bool -- ^ if this error is known to be a case where the first type is used but the second type is expected
+      SourceType
+      SourceType
   | KindsDoNotUnify SourceType SourceType
   | ConstrainedTypeUnified SourceType SourceType
   | OverlappingInstances (Qualified (ProperName 'ClassName)) [SourceType] [Qualified (Either SourceType Ident)]
@@ -132,9 +135,6 @@ data SimpleErrorMessage
   | ExpectedType SourceType SourceType
   -- | constructor name, expected argument count, actual argument count
   | IncorrectConstructorArity (Qualified (ProperName 'ConstructorName)) Int Int
-  | ExprDoesNotHaveType Expr SourceType
-  | PropertyIsMissing Label
-  | AdditionalProperty Label
   | OrphanInstance Ident (Qualified (ProperName 'ClassName)) (S.Set ModuleName) [SourceType]
   | InvalidNewtype (ProperName 'TypeName)
   | InvalidInstanceHead SourceType
@@ -309,9 +309,6 @@ errorCode em = case unwrapErrorMessage em of
   ExtraneousClassMember{} -> "ExtraneousClassMember"
   ExpectedType{} -> "ExpectedType"
   IncorrectConstructorArity{} -> "IncorrectConstructorArity"
-  ExprDoesNotHaveType{} -> "ExprDoesNotHaveType"
-  PropertyIsMissing{} -> "PropertyIsMissing"
-  AdditionalProperty{} -> "AdditionalProperty"
   OrphanInstance{} -> "OrphanInstance"
   InvalidNewtype{} -> "InvalidNewtype"
   InvalidInstanceHead{} -> "InvalidInstanceHead"
@@ -466,9 +463,8 @@ onTypesInErrorMessageM :: Applicative m => (SourceType -> m SourceType) -> Error
 onTypesInErrorMessageM f (ErrorMessage hints simple) = ErrorMessage <$> traverse gHint hints <*> gSimple simple
   where
   gSimple (InfiniteType t) = InfiniteType <$> f t
-  gSimple (TypesDoNotUnify t1 t2) = TypesDoNotUnify <$> f t1 <*> f t2
+  gSimple (TypesDoNotUnify isOrdered t1 t2) = TypesDoNotUnify isOrdered <$> f t1 <*> f t2
   gSimple (ConstrainedTypeUnified t1 t2) = ConstrainedTypeUnified <$> f t1 <*> f t2
-  gSimple (ExprDoesNotHaveType e t) = ExprDoesNotHaveType e <$> f t
   gSimple (InvalidInstanceHead t) = InvalidInstanceHead <$> f t
   gSimple (NoInstanceFound con ambig unks) = NoInstanceFound <$> overConstraintArgs (traverse f) con <*> pure ambig <*> pure unks
   gSimple (AmbiguousTypeVariables t uis) = AmbiguousTypeVariables <$> f t <*> pure uis
@@ -858,14 +854,21 @@ prettyPrintSingleError (PPEOptions codeColor full level showDocs relPath fileCon
             , line "has escaped its scope, appearing in the type"
             , markCodeBox $ indent $ prettyType ty
             ]
-    renderSimpleErrorMessage (TypesDoNotUnify u1 u2)
+    renderSimpleErrorMessage (TypesDoNotUnify isOrdered u1 u2)
       = let (row1Box, row2Box) = printRows u1 u2
 
-        in paras [ line "Could not match type"
-                 , row1Box
-                 , line "with type"
-                 , row2Box
-                 ]
+        in if isOrdered then
+          paras [ line "The actual type"
+                , row1Box
+                , line "does not match the expected type"
+                , row2Box
+                ]
+        else
+          paras [ line "Could not match type"
+                , row1Box
+                , line "with type"
+                , row2Box
+                ]
 
     renderSimpleErrorMessage (KindsDoNotUnify k1 k2) =
       paras [ line "Could not match kind"
@@ -1048,16 +1051,6 @@ prettyPrintSingleError (PPEOptions codeColor full level showDocs relPath fileCon
       paras [ line $ "Data constructor " <> markCode (showQualified runProperName nm) <> " was given " <> T.pack (show actual) <> " arguments in a case expression, but expected " <> T.pack (show expected) <> " arguments."
             , line $ "This problem can be fixed by giving " <> markCode (showQualified runProperName nm) <> " " <> T.pack (show expected) <> " arguments."
             ]
-    renderSimpleErrorMessage (ExprDoesNotHaveType expr ty) =
-      paras [ line "Expression"
-            , markCodeBox $ indent $ prettyPrintValue prettyDepth expr
-            , line "does not have type"
-            , markCodeBox $ indent $ prettyType ty
-            ]
-    renderSimpleErrorMessage (PropertyIsMissing prop) =
-      line $ "Type of expression lacks required label " <> markCode (prettyPrintLabel prop) <> "."
-    renderSimpleErrorMessage (AdditionalProperty prop) =
-      line $ "Type of expression contains additional label " <> markCode (prettyPrintLabel prop) <> "."
     renderSimpleErrorMessage (OrphanInstance nm cnm nonOrphanModules ts) =
       paras [ line $ "Orphan instance" <> prettyPrintPlainIdent nm <> " found for "
             , markCodeBox $ indent $ Box.hsep 1 Box.left
@@ -1614,6 +1607,10 @@ prettyPrintSingleError (PPEOptions codeColor full level showDocs relPath fileCon
         let (sorted1, sorted2) = filterRows (rowToList r1) (rowToList r2)
         in (printRow typeDiffAsBox sorted1, printRow typeDiffAsBox sorted2)
 
+      (_, TypeApp s1 f1@(TypeConstructor _ C.Record) r1'@RCons{}, TypeApp s2 f2@(TypeConstructor _ C.Record) r2'@RCons{}) ->
+        let (sorted1, sorted2) = filterRows (rowToList r1') (rowToList r2')
+        in (printRow typeDiffAsBox $ TypeApp s1 f1 sorted1, printRow typeDiffAsBox $ TypeApp s2 f2 sorted2)
+
       (_, _, _) -> (printRow typeAsBox r1, printRow typeAsBox r2)
 
 
@@ -1724,14 +1721,12 @@ prettyPrintSingleError (PPEOptions codeColor full level showDocs relPath fileCon
 
     -- See https://github.com/purescript/purescript/issues/1802
     stripRedundantHints :: SimpleErrorMessage -> [ErrorMessageHint] -> [ErrorMessageHint]
-    stripRedundantHints ExprDoesNotHaveType{} = stripFirst isCheckHint
-      where
-      isCheckHint ErrorCheckingType{} = True
-      isCheckHint _ = False
-    stripRedundantHints TypesDoNotUnify{} = stripFirst isUnifyHint
+    stripRedundantHints (TypesDoNotUnify _ t1 t2) = stripFirst isMatchingSubsumptionHint . stripFirst isUnifyHint
       where
       isUnifyHint ErrorUnifyingTypes{} = True
       isUnifyHint _ = False
+      isMatchingSubsumptionHint (ErrorInSubsumption t1' t2') = t1 `eqType` t1' && t2 `eqType` t2'
+      isMatchingSubsumptionHint _ = False
     stripRedundantHints (NoInstanceFound (Constraint _ C.Coercible _ args _) _ _) = filter (not . isSolverHint)
       where
       isSolverHint (ErrorSolvingConstraint (Constraint _ C.Coercible _ args' _)) = args == args'
@@ -2049,16 +2044,36 @@ parU
   -> (a -> m b)
   -> m [b]
 parU xs f =
-    forM xs (withError . f) >>= collectErrors
+    forM xs (tryError . f) >>= collectErrors
   where
-    withError :: m b -> m (Either MultipleErrors b)
-    withError u = catchError (Right <$> u) (return . Left)
+    -- exported from Control.Monad.Error.Class in mtl >= 2.3
+    tryError :: m b -> m (Either MultipleErrors b)
+    tryError u = catchError (Right <$> u) (return . Left)
 
     collectErrors :: [Either MultipleErrors b] -> m [b]
     collectErrors es = case partitionEithers es of
       ([], rs) -> return rs
       (errs, _) -> throwError $ fold errs
 
+-- | Collect errors in parallel, using a function to combine results
+liftParU2
+  :: forall m a b c
+   . MonadError MultipleErrors m
+  => (a -> b -> c)
+  -> m a
+  -> m b
+  -> m c
+liftParU2 f ma mb = f' <$> tryError ma <*> tryError mb >>= liftEither
+  where
+  -- exported from Control.Monad.Error.Class in mtl >= 2.3
+  tryError :: forall d. m d -> m (Either MultipleErrors d)
+  tryError u = catchError (Right <$> u) (return . Left)
+
+  f' (Left e) (Left e') = Left $ e <> e'
+  f' (Left e) (Right _) = Left e
+  f' (Right _) (Left e) = Left e
+  f' (Right a) (Right b) = Right $ f a b
+
 internalCompilerError
   :: (MonadError MultipleErrors m, GHC.Stack.HasCallStack)
   => Text

src/Language/PureScript/Pretty/Types.hs

@@ -99,10 +99,15 @@ convertPrettyPrintType = go
   goTypeApp d (TypeApp _ f a) b
     | eqType f tyFunction = PPFunction (go (d-1) a) (go (d-1) b)
     | otherwise = PPTypeApp (goTypeApp d f a) (go (d-1) b)
-  goTypeApp d o ty@RCons{}
-    | eqType o tyRecord = uncurry PPRecord (goRow d ty)
+  goTypeApp d o ty
+    | eqType o tyRecord, isConsOrEmpty ty = uncurry PPRecord (goRow d ty)
   goTypeApp d a b = PPTypeApp (go (d-1) a) (go (d-1) b)
 
+  isConsOrEmpty = \case
+    RCons{} -> True
+    REmpty{} -> True
+    _ -> False
+
 -- TODO(Christoph): get rid of T.unpack s
 
 constraintsAsBox :: TypeRenderOptions -> PrettyPrintConstraint -> Box -> Box

src/Language/PureScript/TypeChecker/Entailment/Coercible.hs

@@ -598,7 +598,7 @@ canonRow a b
         (deriveds, (([], tail1), ([], tail2))) -> do
           pure . Canonicalized . S.fromList $ (tail1, tail2) : deriveds
         (_, (rl1, rl2)) ->
-          throwError . errorMessage $ TypesDoNotUnify (rowFromList rl1) (rowFromList rl2)
+          throwError . errorMessage $ TypesDoNotUnify False (rowFromList rl1) (rowFromList rl2)
   | otherwise = empty
 
 -- | Unwrapping a newtype can fails in two ways:
@@ -768,7 +768,7 @@ decompose env tyName axs bxs = do
           | ax == bx ->
               pure mempty
           | otherwise ->
-              throwError . errorMessage $ TypesDoNotUnify ax bx
+              throwError . errorMessage $ TypesDoNotUnify False ax bx
         Representational ->
           pure $ S.singleton (ax, bx)
         Phantom ->