Add specific error for constructors that could not be unified

purescript · MonoidMusician · May 22, 2022 · Oct 24, 2022 · Oct 24, 2022 · Oct 24, 2022
commit e1eb50d751e9d18cddc0f1dc3de84778c3ef38d8
diff --git a/src/Language/PureScript/Errors.hs b/src/Language/PureScript/Errors.hs
@@ -104,6 +104,7 @@ data SimpleErrorMessage
   | UndefinedTypeVariable (ProperName 'TypeName)
   | PartiallyAppliedSynonym (Qualified (ProperName 'TypeName))
   | EscapedSkolem Text (Maybe SourceSpan) SourceType
+  | TypeConstructorsDoNotUnify ModuleName SourceType ModuleName SourceType
   | TypesDoNotUnify SourceType SourceType
   | KindsDoNotUnify SourceType SourceType
   | ConstrainedTypeUnified SourceType SourceType
@@ -283,6 +284,7 @@ errorCode em = case unwrapErrorMessage em of
   UndefinedTypeVariable{} -> "UndefinedTypeVariable"
   PartiallyAppliedSynonym{} -> "PartiallyAppliedSynonym"
   EscapedSkolem{} -> "EscapedSkolem"
+  TypeConstructorsDoNotUnify{} -> "TypeConstructorsDoNotUnify"
   TypesDoNotUnify{} -> "TypesDoNotUnify"
   KindsDoNotUnify{} -> "KindsDoNotUnify"
   ConstrainedTypeUnified{} -> "ConstrainedTypeUnified"
@@ -410,6 +412,13 @@ addHint hint = addHints [hint]
 addHints :: [ErrorMessageHint] -> MultipleErrors -> MultipleErrors
 addHints hints = onErrorMessages $ \(ErrorMessage hints' se) -> ErrorMessage (hints ++ hints') se
 
+mkTypesDoNotUnify :: SourceType -> SourceType -> SimpleErrorMessage
+mkTypesDoNotUnify
+  t1@(TypeConstructor _ (Qualified (ByModuleName mn1) _))
+  t2@(TypeConstructor _ (Qualified (ByModuleName mn2) _))
+  = TypeConstructorsDoNotUnify mn1 t1 mn2 t2
+mkTypesDoNotUnify t1 t2 = TypesDoNotUnify t1 t2
+
 -- | A map from rigid type variable name/unknown variable pairs to new variables.
 data TypeMap = TypeMap
   { umSkolemMap   :: M.Map Int (String, Int, Maybe SourceSpan)
@@ -462,6 +471,7 @@ 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 (TypeConstructorsDoNotUnify mn1 t1 mn2 t2) = TypeConstructorsDoNotUnify mn1 <$> f t1 <*> pure mn2 <*> f t2
   gSimple (TypesDoNotUnify t1 t2) = TypesDoNotUnify <$> f t1 <*> f t2
   gSimple (KindsDoNotUnify t1 t2) = KindsDoNotUnify <$> f t1 <*> f t2
   gSimple (ConstrainedTypeUnified t1 t2) = ConstrainedTypeUnified <$> f t1 <*> f t2
@@ -856,6 +866,16 @@ prettyPrintSingleError (PPEOptions codeColor full level showDocs relPath fileCon
                  , line "with type"
                  , row2Box
                  ]
+    renderSimpleErrorMessage (TypeConstructorsDoNotUnify mn1 u1 mn2 u2)
+      = let (row1Box, row2Box) = printRows u1 u2
+
+        in paras [ line "Could not match type"
+                 , row1Box
+                 , line $ "(defined in module " <> markCode (runModuleName mn1) <> ")"
+                 , line "with type"
+                 , row2Box
+                 , line $ "(defined in module " <> markCode (runModuleName mn2) <> ")"
+                 ]
 
     renderSimpleErrorMessage (KindsDoNotUnify k1 k2) =
       paras [ line "Could not match kind"
@@ -1686,6 +1706,10 @@ prettyPrintSingleError (PPEOptions codeColor full level showDocs relPath fileCon
       where
       isCheckHint ErrorCheckingType{} = True
       isCheckHint _ = False
+    stripRedundantHints TypeConstructorsDoNotUnify{} = stripFirst isUnifyHint
+      where
+      isUnifyHint ErrorUnifyingTypes{} = True
+      isUnifyHint _ = False
     stripRedundantHints TypesDoNotUnify{} = stripFirst isUnifyHint
       where
       isUnifyHint ErrorUnifyingTypes{} = True

diff --git a/src/Language/PureScript/TypeChecker/Entailment/Coercible.hs b/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 $ mkTypesDoNotUnify (rowFromList rl1) (rowFromList rl2)
   | otherwise = empty
 
 -- | Unwraping 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 $ mkTypesDoNotUnify ax bx
         Representational ->
           pure $ S.singleton (ax, bx)
         Phantom ->

diff --git a/src/Language/PureScript/TypeChecker/Unify.hs b/src/Language/PureScript/TypeChecker/Unify.hs
@@ -130,7 +130,7 @@ unifyTypes t1 t2 = do
   unifyTypes' ty f@ForAll{} = f `unifyTypes` ty
   unifyTypes' (TypeVar _ v1) (TypeVar _ v2) | v1 == v2 = return ()
   unifyTypes' ty1@(TypeConstructor _ c1) ty2@(TypeConstructor _ c2) =
-    guardWith (errorMessage (TypesDoNotUnify ty1 ty2)) (c1 == c2)
+    guardWith (errorMessage (mkTypesDoNotUnify ty1 ty2)) (c1 == c2)
   unifyTypes' (TypeLevelString _ s1) (TypeLevelString _ s2) | s1 == s2 = return ()
   unifyTypes' (TypeLevelInt    _ n1) (TypeLevelInt    _ n2) | n1 == n2 = return ()
   unifyTypes' (TypeApp _ t3 t4) (TypeApp _ t5 t6) = do
@@ -154,7 +154,7 @@ unifyTypes t1 t2 = do
     throwError . errorMessage $ ConstrainedTypeUnified ty1 ty2
   unifyTypes' t3 t4@ConstrainedType{} = unifyTypes' t4 t3
   unifyTypes' t3 t4 =
-    throwError . errorMessage $ TypesDoNotUnify t3 t4
+    throwError . errorMessage $ mkTypesDoNotUnify t3 t4
 
 -- | Unify two rows, updating the current substitution
 --
@@ -177,7 +177,7 @@ unifyRows r1 r2 = sequence_ matches *> uncurry unifyTails rest where
     solveType u1 (rowFromList (sd2, rest'))
     solveType u2 (rowFromList (sd1, rest'))
   unifyTails _ _ =
-    throwError . errorMessage $ TypesDoNotUnify r1 r2
+    throwError . errorMessage $ mkTypesDoNotUnify r1 r2
 
 -- |
 -- Replace type wildcards with unknowns