Better row unification error messages

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 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 ->

src/Language/PureScript/TypeChecker/Kinds.hs

@@ -385,7 +385,7 @@ unifyKinds
   => SourceType
   -> SourceType
   -> m ()
-unifyKinds = unifyKindsWithFailure $ UseUnifyishRows isKindsDoNotUnify $ \w1 w2 ->
+unifyKinds = unifyKindsWithFailure UseUnifyishRows $ \w1 w2 ->
   pure
     $ errorMessage''' (fst . getAnnForType <$> [w1, w2])
     $ KindsDoNotUnify w1 w2
@@ -398,7 +398,7 @@ unifyKinds'
   => SourceType
   -> SourceType
   -> m ()
-unifyKinds' = unifyKindsWithFailure $ UseUnifyishRows isKindsDoNotUnify $ \w1 w2 ->
+unifyKinds' = unifyKindsWithFailure UseUnifyishRows $ \w1 w2 ->
   pure
     $ errorMessage
     $ KindsDoNotUnify w1 w2
@@ -414,36 +414,31 @@ checkTypeKind ty kind =
   -- So, rather than use `unifyishRows` here and pay for its overhead,
   -- we'll use the approach that was used before we migrated to `unifyishRows`
   -- because the original approach fails faster.
-  unifyKindsWithFailure (UseSequential ty kind) kind E.kindType
+  unifyKindsWithFailure UseSequential
+    (\_ _ -> pure $ errorMessage $ ExpectedType ty kind)
+    kind
+    E.kindType
 
-data UnifyRowOptions m
-  -- type kind
-  = UseSequential SourceType SourceType
-  -- isExpectedError onFailure
-  | UseUnifyishRows (SimpleErrorMessage -> Bool) (SourceType -> SourceType -> m MultipleErrors)
+data UnifyRowOptions
+  = UseSequential
+  | UseUnifyishRows
 
 unifyKindsWithFailure
   :: (MonadError MultipleErrors m, MonadState CheckState m, HasCallStack)
-  => UnifyRowOptions m
+  => UnifyRowOptions
+  -> (SourceType -> SourceType -> m MultipleErrors)
   -> SourceType
   -> SourceType
   -> m ()
-unifyKindsWithFailure opts = go
+unifyKindsWithFailure opts onFailure = go
   where
-  (unifyRows, onFailure) = case opts of
-    UseSequential ty kind ->
-      ( \r1 r2 -> do
-          let (matches, rest) = alignRowsWith (\_ -> go) r1 r2
-          sequence_ matches
-          void $ unifyTails rest
-
-      , \_ _ -> 
-          pure $ errorMessage $ ExpectedType ty kind
-      )
-    UseUnifyishRows isExpectedError buildError ->
-      ( unifyishRows go unifyTails isExpectedError buildError
-      , buildError
-      )
+  unifyRows = case opts of
+    UseSequential -> \r1 r2 -> do
+      let (matches, rest) = alignRowsWith (const go) r1 r2
+      sequence_ matches
+      void $ unifyTails rest
+    UseUnifyishRows ->
+      unifyishRows unifyTails isKindsDoNotUnify onFailure go
 
   go = curry $ \case
     (TypeApp _ p1 p2, TypeApp _ p3 p4) -> do
@@ -470,12 +465,10 @@ unifyKindsWithFailure opts = go
       throwError =<< onFailure w1 w2
 
   unifyTails = \case
-    (([], TUnknown _ a'), (rs, p1)) -> do
-      solveUnknown a' $ rowFromList (rs, p1)
-      pure True
-    ((rs, p1), ([], TUnknown _ a')) -> do
-      solveUnknown a' $ rowFromList (rs, p1)
-      pure True
+    (([], TUnknown _ a'), (rs, p1)) ->
+      solveUnknown a' (rowFromList (rs, p1)) $> True
+    ((rs, p1), ([], TUnknown _ a')) ->
+      solveUnknown a' (rowFromList (rs, p1)) $> True
     (([], w1), ([], w2)) | eqType w1 w2 ->
       pure True
     ((rs1, TUnknown _ u1), (rs2, TUnknown _ u2)) | u1 /= u2 -> do

src/Language/PureScript/TypeChecker/Subsumption.hs

@@ -11,14 +11,14 @@ import Control.Monad.Error.Class (MonadError(..))
 import Control.Monad.State.Class (MonadState(..), gets)
 
 import Language.PureScript.AST (ErrorMessageHint(..), Expr(..), pattern NullSourceAnn)
+import Language.PureScript.Constants.Prim qualified as C
 import Language.PureScript.Crash (internalError)
-import Language.PureScript.Environment (tyFunction, tyRecord)
-import Language.PureScript.Errors (MultipleErrors, SimpleErrorMessage(..), errorMessage, internalCompilerError)
+import Language.PureScript.Environment (tyFunction)
+import Language.PureScript.Errors (MultipleErrors, internalCompilerError)
 import Language.PureScript.TypeChecker.Monad (CheckState(..), getHints, getTypeClassDictionaries, withErrorMessageHint)
 import Language.PureScript.TypeChecker.Skolems (newSkolemConstant, skolemize)
-import Language.PureScript.TypeChecker.Unify (freshTypeWithKind, substituteType, unifyTypes)
-import Language.PureScript.TypeChecker.Unify.Rows (unifyishRows, isTypesDoNotUnify)
-import Language.PureScript.Types (SourceType, Type(..), eqType, replaceTypeVars, rowFromList)
+import Language.PureScript.TypeChecker.Unify (freshTypeWithKind, substituteType, unifyishRowTypes, unifyTypesOrdered)
+import Language.PureScript.Types (SourceType, Type(..), eqType, replaceTypeVars)
 
 -- | Subsumption can operate in two modes:
 --
@@ -52,7 +52,7 @@ defaultCoercion :: ModeSing mode -> Coercion mode
 defaultCoercion SElaborate   = id
 defaultCoercion SNoElaborate = ()
 
--- | Check that one type subsumes another, rethrowing errors to provide a better error message
+-- | Check that one type (ty2) subsumes another (ty1), rethrowing errors to provide a better error message
 subsumes
   :: (MonadError MultipleErrors m, MonadState CheckState m)
   => SourceType
@@ -98,27 +98,12 @@ subsumes' SElaborate (ConstrainedType _ con ty1) ty2 = do
   elaborate <- subsumes' SElaborate ty1 ty2
   let addDicts val = App val (TypeClassDictionary con dicts hints)
   return (elaborate . addDicts)
-subsumes' mode (TypeApp _ f1 r1) (TypeApp _ f2 r2) | eqType f1 tyRecord && eqType f2 tyRecord = do
-  let 
-    withBoolError :: forall a. m a -> m Bool
-    withBoolError u = catchError (True <$ u) (pure . const False)
-  unifyishRows
-    -- Check subsumption for common labels
-    (subsumes' SNoElaborate) 
-    -- Inject the info here
-    (uncurry $ \(ts1', r1') (ts2', r2') ->
-      withBoolError $ unifyTypes (rowFromList (ts1', r1')) (rowFromList (ts2', r2')))
-    isTypesDoNotUnify
-    (\r1' r2' -> do
-      subst <- gets checkSubstitution
-      pure $ errorMessage $ TypesDoNotUnify (substituteType subst r1') (substituteType subst r2'))
-    r1
-    r2
+subsumes' mode (TypeApp s1 f1@(TypeConstructor _ C.Record) r1) (TypeApp s2 f2@(TypeConstructor _ C.Record) r2) = do
+  subst <- gets checkSubstitution
+  unifyishRowTypes True (TypeApp s1 f1) (TypeApp s2 f2) (subsumes' SNoElaborate) (substituteType subst r1) (substituteType subst r2)
   -- Nothing was elaborated, return the default coercion
   return (defaultCoercion mode)
-subsumes' mode ty1 ty2@(TypeApp _ obj _) | obj == tyRecord =
-  subsumes' mode ty2 ty1
 subsumes' mode ty1 ty2 = do
-  unifyTypes ty1 ty2
+  unifyTypesOrdered ty1 ty2
   -- Nothing was elaborated, return the default coercion
   return (defaultCoercion mode)