purescript · rhendric · Jun 28, 2021 · May 28, 2021 · Jun 20, 2021 · Jun 26, 2021
diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -46,6 +46,8 @@ Bugfixes:
 
 * Remove generated names from errors about instances (#4118 by @rhendric)
 
+* Improve apartness checking (#4064, @rhendric)
+
 Internal:
 
 * Fix for Haddock (#4072 by @ncaq and @JordanMartinez)

diff --git a/src/Language/PureScript/Errors.hs b/src/Language/PureScript/Errors.hs
@@ -103,6 +103,7 @@ data SimpleErrorMessage
   | OverlappingInstances (Qualified (ProperName 'ClassName)) [SourceType] [Qualified (Either SourceType Ident)]
   | NoInstanceFound
       SourceConstraint -- ^ constraint that could not be solved
+      [Qualified (Either SourceType Ident)] -- ^ a list of instances that stopped further progress in instance chains due to ambiguity
       Bool -- ^ whether eliminating unknowns with annotations might help
   | AmbiguousTypeVariables SourceType [Int]
   | UnknownClass (Qualified (ProperName 'ClassName))
@@ -451,7 +452,7 @@ onTypesInErrorMessageM f (ErrorMessage hints simple) = ErrorMessage <$> traverse
   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 unks) = NoInstanceFound <$> overConstraintArgs (traverse f) con <*> pure unks
+  gSimple (NoInstanceFound con ambig unks) = NoInstanceFound <$> overConstraintArgs (traverse f) con <*> pure ambig <*> pure unks
   gSimple (AmbiguousTypeVariables t us) = AmbiguousTypeVariables <$> f t <*> pure us
   gSimple (OverlappingInstances cl ts insts) = OverlappingInstances cl <$> traverse f ts <*> traverse (traverse $ bitraverse f pure) insts
   gSimple (PossiblyInfiniteInstance cl ts) = PossiblyInfiniteInstance cl <$> traverse f ts
@@ -859,14 +860,14 @@ prettyPrintSingleError (PPEOptions codeColor full level showDocs relPath) e = fl
             , markCodeBox $ indent $ line (showQualified runProperName nm)
             , line "because the class was not in scope. Perhaps it was not exported."
             ]
-    renderSimpleErrorMessage (NoInstanceFound (Constraint _ C.Fail _ [ ty ] _) _) | Just box <- toTypelevelString ty =
+    renderSimpleErrorMessage (NoInstanceFound (Constraint _ C.Fail _ [ ty ] _) _ _) | Just box <- toTypelevelString ty =
       paras [ line "A custom type error occurred while solving type class constraints:"
             , indent box
             ]
     renderSimpleErrorMessage (NoInstanceFound (Constraint _ C.Partial
                                                           _
                                                           _
-                                                          (Just (PartialConstraintData bs b))) _) =
+                                                          (Just (PartialConstraintData bs b))) _ _) =
       paras [ line "A case expression could not be determined to cover all inputs."
             , line "The following additional cases are required to cover all inputs:"
             , indent $ paras $
@@ -875,18 +876,26 @@ prettyPrintSingleError (PPEOptions codeColor full level showDocs relPath) e = fl
                   : [line "..." | not b]
             , line "Alternatively, add a Partial constraint to the type of the enclosing value."
             ]
-    renderSimpleErrorMessage (NoInstanceFound (Constraint _ C.Discard _ [ty] _) _) =
+    renderSimpleErrorMessage (NoInstanceFound (Constraint _ C.Discard _ [ty] _) _ _) =
       paras [ line "A result of type"
             , markCodeBox $ indent $ prettyType ty
             , line "was implicitly discarded in a do notation block."
             , line ("You can use " <> markCode "_ <- ..." <> " to explicitly discard the result.")
             ]
-    renderSimpleErrorMessage (NoInstanceFound (Constraint _ nm _ ts _) unks) =
+    renderSimpleErrorMessage (NoInstanceFound (Constraint _ nm _ ts _) ambiguous unks) =
       paras [ line "No type class instance was found for"
             , markCodeBox $ indent $ Box.hsep 1 Box.left
                 [ line (showQualified runProperName nm)
                 , Box.vcat Box.left (map prettyTypeAtom ts)
                 ]
+            , paras $ let useMessage msg =
+                            [ line msg
+                            , indent $ paras (map prettyInstanceName ambiguous)
+                            ]
+                      in case ambiguous of
+                        [] -> []
+                        [_] -> useMessage "The following instance partially overlaps the above constraint, which means the rest of its instance chain will not be considered:"
+                        _ -> useMessage "The following instances partially overlap the above constraint, which means the rest of their instance chains will not be considered:"
             , paras [ line "The instance head contains unknown type variables. Consider adding a type annotation."
                     | unks
                     ]
@@ -1630,7 +1639,7 @@ prettyPrintSingleError (PPEOptions codeColor full level showDocs relPath) e = fl
       where
       isUnifyHint ErrorUnifyingTypes{} = True
       isUnifyHint _ = False
-    stripRedundantHints (NoInstanceFound (Constraint _ C.Coercible _ args _) _) = filter (not . isSolverHint)
+    stripRedundantHints (NoInstanceFound (Constraint _ C.Coercible _ args _) _ _) = filter (not . isSolverHint)
       where
       isSolverHint (ErrorSolvingConstraint (Constraint _ C.Coercible _ args' _)) = args == args'
       isSolverHint _ = False

diff --git a/src/Language/PureScript/TypeChecker/Entailment.hs b/src/Language/PureScript/TypeChecker/Entailment.hs
@@ -18,11 +18,12 @@ import Control.Monad.State
 import Control.Monad.Supply.Class (MonadSupply(..))
 import Control.Monad.Writer
 
+import Data.Either (lefts, partitionEithers)
 import Data.Foldable (for_, fold, toList)
 import Data.Function (on)
 import Data.Functor (($>))
-import Data.List (findIndices, minimumBy, groupBy, nubBy, sortOn)
-import Data.Maybe (fromMaybe, listToMaybe, mapMaybe)
+import Data.List (findIndices, minimumBy, groupBy, nubBy, sortOn, tails)
+import Data.Maybe (catMaybes, fromMaybe, listToMaybe, mapMaybe)
 import qualified Data.Map as M
 import qualified Data.Set as S
 import Data.Traversable (for)
@@ -229,22 +230,23 @@ entails SolverOptions{..} constraint context hints =
 
             dicts <- lift . lift $ forClassNameM env (combineContexts context inferred) className' kinds'' tys''
 
-            let instances = do
+            let (catMaybes -> ambiguous, instances) = partitionEithers $ do
                   chain <- groupBy ((==) `on` tcdChain) $
                            sortOn (tcdChain &&& tcdIndex)
                            dicts
                   -- process instances in a chain in index order
-                  let found = for chain $ \tcd ->
+                  let found = for (init $ tails chain) $ \(tcd:tl) ->
                                 -- Make sure the type unifies with the type in the type instance definition
                                 case matches typeClassDependencies tcd tys'' of
-                                  Apart        -> Right ()                  -- keep searching
-                                  Match substs -> Left (Just (substs, tcd)) -- found a match
-                                  Unknown      -> Left Nothing              -- can't continue with this chain yet, need proof of apartness
-                  case found of
-                    Right _               -> []          -- all apart
-                    Left Nothing          -> []          -- last unknown
-                    Left (Just substsTcd) -> [substsTcd] -- found a match
-            solution <- lift . lift $ unique kinds'' tys'' instances (unknownsInAllCoveringSets tys'' typeClassCoveringSets)
+                                  Apart        -> Right ()                   -- keep searching
+                                  Match substs -> Left (Right (substs, tcd)) -- found a match
+                                  Unknown ->
+                                    if null (tcdChain tcd) || null tl
+                                    then Right ()                                   -- need proof of apartness but this is either not in a chain or at the end
+                                    else Left (Left (tcdToInstanceDescription tcd)) -- can't continue with this chain yet, need proof of apartness
+
+                  lefts [found]
+            solution <- lift . lift $ unique kinds'' tys'' ambiguous instances (unknownsInAllCoveringSets tys'' typeClassCoveringSets)
             case solution of
               Solved substs tcd -> do
                 -- Note that we solved something.
@@ -322,16 +324,16 @@ entails SolverOptions{..} constraint context hints =
                       (substituteType currentSubst . replaceAllTypeVars (M.toList subst) $ instKind)
                       (substituteType currentSubst tyKind)
 
-            unique :: [SourceType] -> [SourceType] -> [(a, TypeClassDict)] -> Bool -> m (EntailsResult a)
-            unique kindArgs tyArgs [] unks
+            unique :: [SourceType] -> [SourceType] -> [Qualified (Either SourceType Ident)] -> [(a, TypeClassDict)] -> Bool -> m (EntailsResult a)
+            unique kindArgs tyArgs ambiguous [] unks
               | solverDeferErrors = return Deferred
               -- We need a special case for nullary type classes, since we want
               -- to generalize over Partial constraints.
               | solverShouldGeneralize && ((null kindArgs && null tyArgs) || any canBeGeneralized kindArgs || any canBeGeneralized tyArgs) =
                   return (Unsolved (srcConstraint className' kindArgs tyArgs conInfo))
-              | otherwise = throwError . errorMessage $ NoInstanceFound (srcConstraint className' kindArgs tyArgs conInfo) unks
-            unique _ _ [(a, dict)] _ = return $ Solved a dict
-            unique _ tyArgs tcds _
+              | otherwise = throwError . errorMessage $ NoInstanceFound (srcConstraint className' kindArgs tyArgs conInfo) ambiguous unks
+            unique _ _ _ [(a, dict)] _ = return $ Solved a dict
+            unique _ tyArgs _ tcds _
               | pairwiseAny overlapping (map snd tcds) =
                   throwError . errorMessage $ OverlappingInstances className' tyArgs (tcds >>= (toList . tcdToInstanceDescription . snd))
               | otherwise = return $ uncurry Solved (minimumBy (compare `on` length . tcdPath . snd) tcds)
@@ -638,6 +640,7 @@ matches deps TypeClassDictionaryInScope{..} tys =
         go (sd, r)                 ([], TypeVar _ v)                   = (Match (), M.singleton v [rowFromList (sd, r)])
         go _ _                                                         = (Apart, M.empty)
     typeHeadsAreEqual (TUnknown _ _) _ = (Unknown, M.empty)
+    typeHeadsAreEqual Skolem{} _       = (Unknown, M.empty)
     typeHeadsAreEqual _ _ = (Apart, M.empty)
 
     both :: (Matched (), Matching [Type a]) -> (Matched (), Matching [Type a]) -> (Matched (), Matching [Type a])
@@ -655,9 +658,11 @@ matches deps TypeClassDictionaryInScope{..} tys =
       typesAreEqual (KindedType _ t1 _)    t2                     = typesAreEqual t1 t2
       typesAreEqual t1                     (KindedType _ t2 _)    = typesAreEqual t1 t2
       typesAreEqual (TUnknown _ u1)        (TUnknown _ u2)        | u1 == u2 = Match ()
-      typesAreEqual (Skolem _ _ _ s1 _)      (Skolem _ _ _ s2 _)      | s1 == s2 = Match ()
-      typesAreEqual (Skolem _ _ _ _ _)       _                      = Unknown
-      typesAreEqual _                      (Skolem _ _ _ _ _)       = Unknown
+      typesAreEqual (TUnknown _ u1)        t2                     = if t2 `containsUnknown` u1 then Apart else Unknown
+      typesAreEqual t1                     (TUnknown _ u2)        = if t1 `containsUnknown` u2 then Apart else Unknown
+      typesAreEqual (Skolem _ _ _ s1 _)    (Skolem _ _ _ s2 _)    | s1 == s2 = Match ()
+      typesAreEqual (Skolem _ _ _ s1 _)    t2                     = if t2 `containsSkolem` s1 then Apart else Unknown
+      typesAreEqual t1                     (Skolem _ _ _ s2 _)    = if t1 `containsSkolem` s2 then Apart else Unknown
       typesAreEqual (TypeVar _ v1)         (TypeVar _ v2)         | v1 == v2 = Match ()
       typesAreEqual (TypeLevelString _ s1) (TypeLevelString _ s2) | s1 == s2 = Match ()
       typesAreEqual (TypeConstructor _ c1) (TypeConstructor _ c2) | c1 == c2 = Match ()
@@ -673,6 +678,8 @@ matches deps TypeClassDictionaryInScope{..} tys =
           go (l, t1)                (r, KindedType _ t2 _)            = go (l, t1) (r, t2)
           go ([], KindApp _ t1 k1)  ([], KindApp _ t2 k2)             = typesAreEqual t1 t2 <> typesAreEqual k1 k2
           go ([], TUnknown _ u1)    ([], TUnknown _ u2)    | u1 == u2 = Match ()
+          go ([], TUnknown _ _)     ([], _)                           = Unknown
+          go ([], _)                ([], TUnknown _ _)                = Unknown
           go ([], Skolem _ _ _ s1 _)  ([], Skolem _ _ _ s2 _)  | s1 == s2 = Match ()
           go ([], Skolem _ _ _ _ _)   _                               = Unknown
           go _                      ([], Skolem _ _ _ _ _)            = Unknown
@@ -685,6 +692,12 @@ matches deps TypeClassDictionaryInScope{..} tys =
       isRCons RCons{}    = True
       isRCons _          = False
 
+      containsSkolem :: Type a -> Int -> Bool
+      containsSkolem t s = everythingOnTypes (||) (\case Skolem _ _ _ s' _ -> s == s'; _ -> False) t
+
+      containsUnknown :: Type a -> Int -> Bool
+      containsUnknown t u = everythingOnTypes (||) (\case TUnknown _ u' -> u == u'; _ -> False) t
+
 -- | Add a dictionary for the constraint to the scope, and dictionaries
 -- for all implied superclass instances.
 newDictionaries

diff --git a/src/Language/PureScript/TypeChecker/Entailment/Coercible.hs b/src/Language/PureScript/TypeChecker/Entailment/Coercible.hs
@@ -527,7 +527,7 @@ insoluble
   -> SourceType
   -> MultipleErrors
 insoluble k a b =
-  errorMessage $ NoInstanceFound (srcConstraint Prim.Coercible [k] [a, b] Nothing) (any containsUnknowns [a, b])
+  errorMessage $ NoInstanceFound (srcConstraint Prim.Coercible [k] [a, b] Nothing) [] (any containsUnknowns [a, b])
 
 -- | Constraints of the form @Coercible a b@ can be solved if the two arguments
 -- are the same. Since we currently don't support higher-rank arguments in

diff --git a/tests/purs/failing/3329.out b/tests/purs/failing/3329.out
@@ -0,0 +1,28 @@
+Error found:
+in module [33mMain[0m
+at tests/purs/failing/3329.purs:24:8 - 24:11 (line 24, column 8 - line 24, column 11)
+
+  No type class instance was found for
+  [33m                            [0m
+  [33m  Main.Inject g0            [0m
+  [33m              (Either f1 g0)[0m
+  [33m                            [0m
+  The following instance partially overlaps the above constraint, which means the rest of its instance chain will not be considered:
+
+    [33mMain.injectLeft[0m
+
+
+while checking that type [33mforall (f :: Type) (g :: Type). Inject f g => f -> g[0m
+  is at least as general as type [33mg0 -> Either f1 g0[0m
+while checking that expression [33minj[0m
+  has type [33mg0 -> Either f1 g0[0m
+in value declaration [33minjR[0m
+
+where [33mf1[0m is a rigid type variable
+        bound at (line 24, column 8 - line 24, column 11)
+      [33mg0[0m is a rigid type variable
+        bound at (line 24, column 8 - line 24, column 11)
+
+See https://github.com/purescript/documentation/blob/master/errors/NoInstanceFound.md for more information,
+or to contribute content related to this error.
+
diff --git a/tests/purs/failing/3329.purs b/tests/purs/failing/3329.purs
@@ -0,0 +1,24 @@
+-- @shouldFailWith NoInstanceFound
+module Main where
+
+import Data.Either (Either(..))
+import Data.Maybe (Maybe(..))
+
+class Inject f g where
+  inj :: f -> g
+  prj :: g -> Maybe f
+
+instance injectRefl :: Inject x x where
+  inj x = x
+  prj x = Just x
+else instance injectLeft :: Inject l (Either l r) where
+  inj x = Left x
+  prj (Left x) = Just x
+  prj _ = Nothing
+else instance injectRight :: Inject x r => Inject x (Either l r) where
+  inj x = Right (inj x)
+  prj (Right x) = prj x
+  prj _ = Nothing
+
+injR :: forall f g. g -> Either f g
+injR = inj
diff --git a/tests/purs/failing/3531-2.out b/tests/purs/failing/3531-2.out
@@ -0,0 +1,27 @@
+Error found:
+in module [33mMain[0m
+at tests/purs/failing/3531-2.purs:22:11 - 22:22 (line 22, column 11 - line 22, column 22)
+
+  No type class instance was found for
+  [33m                   [0m
+  [33m  Main.C (X t2 Int)[0m
+  [33m                   [0m
+  The following instance partially overlaps the above constraint, which means the rest of its instance chain will not be considered:
+
+    [33mMain.cx[0m
+
+  The instance head contains unknown type variables. Consider adding a type annotation.
+
+while applying a function [33mthing[0m
+  of type [33mC t0 => t0 -> t0[0m
+  to argument [33mtest1[0m
+while inferring the type of [33mthing test1[0m
+in value declaration [33mtest2[0m
+
+where [33mt0[0m is an unknown type
+      [33mt1[0m is an unknown type
+      [33mt2[0m is an unknown type
+
+See https://github.com/purescript/documentation/blob/master/errors/NoInstanceFound.md for more information,
+or to contribute content related to this error.
+
diff --git a/tests/purs/failing/3531-2.purs b/tests/purs/failing/3531-2.purs
@@ -0,0 +1,23 @@
+-- @shouldFailWith NoInstanceFound
+module Main where
+
+import Prim.TypeError (class Fail, Text)
+
+class C x where
+  thing :: x -> x
+
+data X a b = X
+
+test1 :: forall a. X a Int
+test1 = X
+
+instance cx :: C (X x x) where
+  thing x = x
+
+else instance cxFail :: Fail (Text "Fell through") => C (X x y) where
+  thing x = x
+
+test2 :: Boolean
+test2 = do
+  let X = thing test1
+  true
diff --git a/tests/purs/failing/3531-3.out b/tests/purs/failing/3531-3.out
@@ -0,0 +1,32 @@
+Error found:
+in module [33mMain[0m
+at tests/purs/failing/3531-3.purs:22:11 - 22:22 (line 22, column 11 - line 22, column 22)
+
+  No type class instance was found for
+  [33m                        [0m
+  [33m  Main.C (X             [0m
+  [33m            { foo :: Int[0m
+  [33m            | t1        [0m
+  [33m            }           [0m
+  [33m            { foo :: Int[0m
+  [33m            }           [0m
+  [33m         )              [0m
+  [33m                        [0m
+  The following instance partially overlaps the above constraint, which means the rest of its instance chain will not be considered:
+
+    [33mMain.cx[0m
+
+  The instance head contains unknown type variables. Consider adding a type annotation.
+
+while applying a function [33mthing[0m
+  of type [33mC t0 => t0 -> t0[0m
+  to argument [33mtest1[0m
+while inferring the type of [33mthing test1[0m
+in value declaration [33mtest2[0m
+
+where [33mt0[0m is an unknown type
+      [33mt1[0m is an unknown type
+
+See https://github.com/purescript/documentation/blob/master/errors/NoInstanceFound.md for more information,
+or to contribute content related to this error.
+
diff --git a/tests/purs/failing/3531-3.purs b/tests/purs/failing/3531-3.purs
@@ -0,0 +1,23 @@
+-- @shouldFailWith NoInstanceFound
+module Main where
+
+import Prim.TypeError (class Fail, Text)
+
+class C x where
+  thing :: x -> x
+
+data X a b = X
+
+test1 :: forall r. X { foo :: Int | r } { foo :: Int }
+test1 = X
+
+instance cx :: C (X x x) where
+  thing x = x
+
+else instance cxFail :: Fail (Text "Fell through") => C (X x y) where
+  thing x = x
+
+test2 :: Boolean
+test2 = do
+  let X = thing test1
+  true