From a5d9a1f7d4ae0c966563f7671e6880f9e90b5fee Mon Sep 17 00:00:00 2001 From: Ryan Hendrickson Date: Fri, 28 May 2021 01:57:21 -0400 Subject: [PATCH] Improve apartness checking Instances in an instance chain that don't match the constraint being searched must be proven apart from the constraint for the search to continue to the next instance in the chain. This commit tweaks the apartness checker to fix a variety of incorrect apartness judgments, and also adds a hint to the NoInstanceFound error message if ambiguous instances (neither matching nor apart) excluded additional instances in a chain from consideration. --- CHANGELOG.md | 2 + src/Language/PureScript/Errors.hs | 36 ++++++++-- .../PureScript/TypeChecker/Entailment.hs | 69 ++++++++++++------- .../TypeChecker/Entailment/Coercible.hs | 2 +- tests/purs/failing/3329.out | 25 +++++++ tests/purs/failing/3329.purs | 24 +++++++ tests/purs/failing/3531-2.out | 24 +++++++ tests/purs/failing/3531-2.purs | 23 +++++++ tests/purs/failing/3531-3.out | 29 ++++++++ tests/purs/failing/3531-3.purs | 23 +++++++ tests/purs/failing/3531-4.out | 33 +++++++++ tests/purs/failing/3531-4.purs | 21 ++++++ tests/purs/failing/3531-5.out | 29 ++++++++ tests/purs/failing/3531-5.purs | 16 +++++ tests/purs/failing/3531-6.out | 33 +++++++++ tests/purs/failing/3531-6.purs | 21 ++++++ tests/purs/failing/3531.out | 24 +++++++ tests/purs/failing/3531.purs | 16 +++++ tests/purs/failing/4028.out | 24 +++++++ tests/purs/failing/4028.purs | 29 ++++++++ .../InstanceChainBothUnknownAndMatch.out | 1 + .../InstanceChainSkolemUnknownMatch.out | 1 + tests/purs/passing/3329.purs | 34 +++++++++ tests/purs/passing/3941.purs | 25 +++++++ 24 files changed, 534 insertions(+), 30 deletions(-) create mode 100644 tests/purs/failing/3329.out create mode 100644 tests/purs/failing/3329.purs create mode 100644 tests/purs/failing/3531-2.out create mode 100644 tests/purs/failing/3531-2.purs create mode 100644 tests/purs/failing/3531-3.out create mode 100644 tests/purs/failing/3531-3.purs create mode 100644 tests/purs/failing/3531-4.out create mode 100644 tests/purs/failing/3531-4.purs create mode 100644 tests/purs/failing/3531-5.out create mode 100644 tests/purs/failing/3531-5.purs create mode 100644 tests/purs/failing/3531-6.out create mode 100644 tests/purs/failing/3531-6.purs create mode 100644 tests/purs/failing/3531.out create mode 100644 tests/purs/failing/3531.purs create mode 100644 tests/purs/failing/4028.out create mode 100644 tests/purs/failing/4028.purs create mode 100644 tests/purs/passing/3329.purs create mode 100644 tests/purs/passing/3941.purs diff --git a/CHANGELOG.md b/CHANGELOG.md index fecde031cb..edff00e0e7 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -14,6 +14,8 @@ Bugfixes: * Allow fixity, kind, role declarations in REPL (#4046, @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 index 6fce239501..c00ee61c3f 100644 --- a/src/Language/PureScript/Errors.hs +++ b/src/Language/PureScript/Errors.hs @@ -102,6 +102,7 @@ data SimpleErrorMessage | OverlappingInstances (Qualified (ProperName 'ClassName)) [SourceType] [Qualified 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)) @@ -450,7 +451,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 <*> pure insts gSimple (PossiblyInfiniteInstance cl ts) = PossiblyInfiniteInstance cl <$> traverse f ts @@ -858,14 +859,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 $ @@ -874,18 +875,28 @@ 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 $ case ambiguous of + [] -> [] + [ambig] -> + [ "The instance " Box.<> prettyInstanceName False ambig + Box.<> " partially overlaps the above constraint, which means the rest of its instance chain will not be considered." + ] + _ -> + [ line "The following instances partially overlap the above constraint, which means the rest of their instance chains will not be considered:" + , indent $ paras (map (prettyInstanceName True) ambiguous) + ] , paras [ line "The instance head contains unknown type variables. Consider adding a type annotation." | unks ] @@ -1629,7 +1640,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 @@ -1659,6 +1670,19 @@ prettyPrintSingleError (PPEOptions codeColor full level showDocs relPath) e = fl hintCategory PositionedError{} = PositionHint hintCategory _ = OtherHint + prettyInstanceName :: Bool -> Qualified (Either SourceType Ident) -> Box.Box + prettyInstanceName inList = \case + Qualified maybeMn (Left ty) -> + (if inList then "instance " else Box.nullBox) + Box.<> (case maybeMn of + Just mn -> "in module " + Box.<> line (markCode $ runModuleName mn) + Box.<> " " + Nothing -> Box.nullBox) + Box.<> "with type " + Box.<> markCodeBox (prettyType ty) + Qualified mn (Right inst) -> line . markCode . showQualified showIdent $ Qualified mn inst + -- Pretty print and export declaration prettyPrintExport :: DeclarationRef -> Text prettyPrintExport (TypeRef _ pn _) = runProperName pn diff --git a/src/Language/PureScript/TypeChecker/Entailment.hs b/src/Language/PureScript/TypeChecker/Entailment.hs index 5cf3419a9a..8f6159ce37 100644 --- 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.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.Either (lefts, partitionEithers) +import Data.Foldable (for_, fold, foldl', toList) +import Data.Function (on, (&)) +import Data.Functor (($>), (<&>)) +import Data.List (findIndices, minimumBy, groupBy, nubBy, sortOn, tails) +import Data.Maybe (fromMaybe, listToMaybe, mapMaybe, catMaybes) import qualified Data.Map as M import qualified Data.Set as S import Data.Traversable (for) @@ -229,22 +230,33 @@ 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 (getName tcd)) -- can't continue with this chain yet, need proof of apartness + where + getName TypeClassDictionaryInScope{..} = + namedInstanceIdentifier tcdValue <&> \case + Qualified mn (Ident i) | T.head i == '$' -> + Qualified mn . Left $ + tcdForAll & foldr srcForAll' ( + tcdInstanceTypes & foldl' srcTypeApp ( + srcTypeConstructor (fmap coerceProperName tcdClassName))) + other -> fmap Right other + srcForAll' (tv, k) ty = srcForAll tv (Just k) ty Nothing + + + 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 +334,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 . namedInstanceIdentifier . tcdValue . snd)) | otherwise = return $ uncurry Solved (minimumBy (compare `on` length . tcdPath . snd) tcds) @@ -631,6 +643,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]) @@ -648,9 +661,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 () @@ -666,6 +681,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 @@ -678,6 +695,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 index 1eed5d6c50..bb16e25b62 100644 --- 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 new file mode 100644 index 0000000000..c31dbeadf1 --- /dev/null +++ b/tests/purs/failing/3329.out @@ -0,0 +1,25 @@ +Error found: +in module Main +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 +   +  Main.Inject g0  +  (Either f1 g0) +   + The instance Main.injectLeft partially overlaps the above constraint, which means the rest of its instance chain will not be considered. + +while checking that type forall (f :: Type) (g :: Type). Inject f g => f -> g + is at least as general as type g0 -> Either f1 g0 +while checking that expression inj + has type g0 -> Either f1 g0 +in value declaration injR + +where f1 is a rigid type variable + bound at (line 24, column 8 - line 24, column 11) + g0 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 new file mode 100644 index 0000000000..7beb876929 --- /dev/null +++ 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 new file mode 100644 index 0000000000..800398d983 --- /dev/null +++ b/tests/purs/failing/3531-2.out @@ -0,0 +1,24 @@ +Error found: +in module Main +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 +   +  Main.C (X t2 Int) +   + The instance Main.cx partially overlaps the above constraint, which means the rest of its instance chain will not be considered. + The instance head contains unknown type variables. Consider adding a type annotation. + +while applying a function thing + of type C t0 => t0 -> t0 + to argument test1 +while inferring the type of thing test1 +in value declaration test2 + +where t0 is an unknown type + t1 is an unknown type + t2 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 new file mode 100644 index 0000000000..ed20e5f1cc --- /dev/null +++ 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 new file mode 100644 index 0000000000..0c17273f28 --- /dev/null +++ b/tests/purs/failing/3531-3.out @@ -0,0 +1,29 @@ +Error found: +in module Main +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 +   +  Main.C (X  +  { foo :: Int +  | t1  +  }  +  { foo :: Int +  }  +  )  +   + The instance Main.cx partially overlaps the above constraint, which means the rest of its instance chain will not be considered. + The instance head contains unknown type variables. Consider adding a type annotation. + +while applying a function thing + of type C t0 => t0 -> t0 + to argument test1 +while inferring the type of thing test1 +in value declaration test2 + +where t0 is an unknown type + t1 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 new file mode 100644 index 0000000000..5d3704101c --- /dev/null +++ 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 diff --git a/tests/purs/failing/3531-4.out b/tests/purs/failing/3531-4.out new file mode 100644 index 0000000000..04b5b756d5 --- /dev/null +++ b/tests/purs/failing/3531-4.out @@ -0,0 +1,33 @@ +Error found: +in module Main +at tests/purs/failing/3531-4.purs:21:7 - 21:27 (line 21, column 7 - line 21, column 27) + + No type class instance was found for +   +  Main.C a4 +  b5 +   + The following instances partially overlap the above constraint, which means the rest of their instance chains will not be considered: + + Main.c1 + Main.c3 + + +while applying a function c + of type C @t0 @t1 t2 t3 => Proxy @t0 t2 -> Proxy @t1 t3 -> Boolean + to argument Proxy +while inferring the type of c Proxy +in value declaration fn + +where a4 is a rigid type variable + bound at (line 0, column 0 - line 0, column 0) + b5 is a rigid type variable + bound at (line 0, column 0 - line 0, column 0) + t0 is an unknown type + t1 is an unknown type + t2 is an unknown type + t3 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-4.purs b/tests/purs/failing/3531-4.purs new file mode 100644 index 0000000000..46c73fd52e --- /dev/null +++ b/tests/purs/failing/3531-4.purs @@ -0,0 +1,21 @@ +-- @shouldFailWith NoInstanceFound +module Main where + +data Proxy a = Proxy + +class C a b where + c :: Proxy a -> Proxy b -> Boolean + +instance c1 :: C String String where + c _ _ = true +else instance c2 :: C String a where + c _ _ = false + +instance c3 :: C Int Int where + c _ _ = true +else instance c4 :: C Int a where + c _ _ = false + +fn :: forall a b. Proxy a -> Proxy b -> Int +fn _ _ = 42 where + x = c (Proxy :: Proxy a) (Proxy :: Proxy b) diff --git a/tests/purs/failing/3531-5.out b/tests/purs/failing/3531-5.out new file mode 100644 index 0000000000..e23d2094fd --- /dev/null +++ b/tests/purs/failing/3531-5.out @@ -0,0 +1,29 @@ +Error found: +in module Main +at tests/purs/failing/3531-5.purs:16:7 - 16:27 (line 16, column 7 - line 16, column 27) + + No type class instance was found for +   +  Main.C a4 +  b5 +   + The instance in module Main with type forall a. C String (Array a) partially overlaps the above constraint, which means the rest of its instance chain will not be considered. + +while applying a function c + of type C @t0 @t1 t2 t3 => Proxy @t0 t2 -> Proxy @t1 t3 -> Boolean + to argument Proxy +while inferring the type of c Proxy +in value declaration fn + +where a4 is a rigid type variable + bound at (line 0, column 0 - line 0, column 0) + b5 is a rigid type variable + bound at (line 0, column 0 - line 0, column 0) + t0 is an unknown type + t1 is an unknown type + t2 is an unknown type + t3 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-5.purs b/tests/purs/failing/3531-5.purs new file mode 100644 index 0000000000..5c19ed374e --- /dev/null +++ b/tests/purs/failing/3531-5.purs @@ -0,0 +1,16 @@ +-- @shouldFailWith NoInstanceFound +module Main where + +data Proxy a = Proxy + +class C a b where + c :: Proxy a -> Proxy b -> Boolean + +instance C String (Array a) where + c _ _ = true +else instance c2 :: C String a where + c _ _ = false + +fn :: forall a b. Proxy a -> Proxy b -> Int +fn _ _ = 42 where + x = c (Proxy :: Proxy a) (Proxy :: Proxy b) diff --git a/tests/purs/failing/3531-6.out b/tests/purs/failing/3531-6.out new file mode 100644 index 0000000000..e6b36b4333 --- /dev/null +++ b/tests/purs/failing/3531-6.out @@ -0,0 +1,33 @@ +Error found: +in module Main +at tests/purs/failing/3531-6.purs:21:7 - 21:27 (line 21, column 7 - line 21, column 27) + + No type class instance was found for +   +  Main.C a4 +  b5 +   + The following instances partially overlap the above constraint, which means the rest of their instance chains will not be considered: + + instance in module Main with type forall a. C String (Array a) + instance in module Main with type C Int Int + + +while applying a function c + of type C @t0 @t1 t2 t3 => Proxy @t0 t2 -> Proxy @t1 t3 -> Boolean + to argument Proxy +while inferring the type of c Proxy +in value declaration fn + +where a4 is a rigid type variable + bound at (line 0, column 0 - line 0, column 0) + b5 is a rigid type variable + bound at (line 0, column 0 - line 0, column 0) + t0 is an unknown type + t1 is an unknown type + t2 is an unknown type + t3 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-6.purs b/tests/purs/failing/3531-6.purs new file mode 100644 index 0000000000..204ef158a1 --- /dev/null +++ b/tests/purs/failing/3531-6.purs @@ -0,0 +1,21 @@ +-- @shouldFailWith NoInstanceFound +module Main where + +data Proxy a = Proxy + +class C a b where + c :: Proxy a -> Proxy b -> Boolean + +instance C String (Array a) where + c _ _ = true +else instance c2 :: C String a where + c _ _ = false + +instance C Int Int where + c _ _ = true +else instance c4 :: C Int a where + c _ _ = false + +fn :: forall a b. Proxy a -> Proxy b -> Int +fn _ _ = 42 where + x = c (Proxy :: Proxy a) (Proxy :: Proxy b) diff --git a/tests/purs/failing/3531.out b/tests/purs/failing/3531.out new file mode 100644 index 0000000000..64ad44c4d1 --- /dev/null +++ b/tests/purs/failing/3531.out @@ -0,0 +1,24 @@ +Error found: +in module Main +at tests/purs/failing/3531.purs:16:7 - 16:27 (line 16, column 7 - line 16, column 27) + + No type class instance was found for +   +  Main.C a2 +   + The instance Main.c1 partially overlaps the above constraint, which means the rest of its instance chain will not be considered. + +while applying a function c + of type C @t0 t1 => Proxy @t0 t1 -> Boolean + to argument Proxy +while inferring the type of c Proxy +in value declaration fn + +where a2 is a rigid type variable + bound at (line 0, column 0 - line 0, column 0) + t0 is an unknown type + t1 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.purs b/tests/purs/failing/3531.purs new file mode 100644 index 0000000000..b7d28a2c96 --- /dev/null +++ b/tests/purs/failing/3531.purs @@ -0,0 +1,16 @@ +-- @shouldFailWith NoInstanceFound +module Main where + +data Proxy a = Proxy + +class C a where + c :: Proxy a -> Boolean + +instance c1 :: C String where + c _ = true +else instance c2 :: C a where + c _ = false + +fn :: forall a. Proxy a -> Int +fn _ = 42 where + x = c (Proxy :: Proxy a) diff --git a/tests/purs/failing/4028.out b/tests/purs/failing/4028.out new file mode 100644 index 0000000000..5502ba5c3f --- /dev/null +++ b/tests/purs/failing/4028.out @@ -0,0 +1,24 @@ +Error found: +in module Main +at tests/purs/failing/4028.purs:29:12 - 29:37 (line 29, column 12 - line 29, column 37) + + No type class instance was found for +   +  Main.TLShow (S i2) +   + The instance Main.tlShow2 partially overlaps the above constraint, which means the rest of its instance chain will not be considered. + +while applying a function go + of type TLShow @t0 t1 => Proxy @t0 t1 -> Int -> String + to argument Proxy +while inferring the type of go Proxy +in value declaration peano + +where i2 is a rigid type variable + bound at (line 0, column 0 - line 0, column 0) + t0 is an unknown type + t1 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/4028.purs b/tests/purs/failing/4028.purs new file mode 100644 index 0000000000..590d85d42b --- /dev/null +++ b/tests/purs/failing/4028.purs @@ -0,0 +1,29 @@ +-- @shouldFailWith NoInstanceFound +module Main where + +import Prelude + +import Type.Proxy (Proxy(..)) + +foreign import data Peano :: Type + +foreign import data Z :: Peano +foreign import data S :: Peano -> Peano + +class TLShow :: forall k. k -> Constraint +class TLShow i where + tlShow :: Proxy i -> String + +instance tlShow2 :: TLShow (S (S Z)) where + tlShow _ = "2" +else instance tlShow0 :: TLShow Z where + tlShow _ = "0" +else instance tlShowS :: TLShow x => TLShow (S x) where + tlShow _ = "S" <> tlShow (Proxy :: Proxy x) + +peano :: Int -> String +peano = go (Proxy :: Proxy Z) + where + go :: forall i. TLShow i => Proxy i -> Int -> String + go p 0 = tlShow p + go _ n = go (Proxy :: Proxy (S i)) (n - 1) diff --git a/tests/purs/failing/InstanceChainBothUnknownAndMatch.out b/tests/purs/failing/InstanceChainBothUnknownAndMatch.out index 153cfa51a9..9181734c47 100644 --- a/tests/purs/failing/InstanceChainBothUnknownAndMatch.out +++ b/tests/purs/failing/InstanceChainBothUnknownAndMatch.out @@ -16,6 +16,7 @@ at tests/purs/failing/InstanceChainBothUnknownAndMatch.purs:17:13 - 17:55 (line  )   t4    + The instance InstanceChains.BothUnknownAndMatch.sameY partially overlaps the above constraint, which means the rest of its instance chain will not be considered. while applying a function same of type Same @Type @Type t0 t1 t2 => t0 -> t1 -> SProxy t2 diff --git a/tests/purs/failing/InstanceChainSkolemUnknownMatch.out b/tests/purs/failing/InstanceChainSkolemUnknownMatch.out index 7bb44148c0..3f6e4f43cc 100644 --- a/tests/purs/failing/InstanceChainSkolemUnknownMatch.out +++ b/tests/purs/failing/InstanceChainSkolemUnknownMatch.out @@ -8,6 +8,7 @@ at tests/purs/failing/InstanceChainSkolemUnknownMatch.purs:14:13 - 14:36 (line 1  (Proxy Int)  t4    + The instance InstanceChainSkolemUnknownMatch.sameY partially overlaps the above constraint, which means the rest of its instance chain will not be considered. while applying a function same of type Same @Type @Type t0 t1 t2 => t0 -> t1 -> SProxy t2 diff --git a/tests/purs/passing/3329.purs b/tests/purs/passing/3329.purs new file mode 100644 index 0000000000..5d531182d5 --- /dev/null +++ b/tests/purs/passing/3329.purs @@ -0,0 +1,34 @@ +module Main where + +import Prelude + +import Data.Either (Either(..)) +import Data.Maybe (Maybe(..)) +import Effect (Effect) +import Effect.Console (log) + +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 + +injL :: forall f g. f -> Either f g +injL = inj + +main :: Effect Unit +main = log "Done" + where + testInjLWithUnknowns a = case inj a of + Left a' -> a' + Right _ -> a diff --git a/tests/purs/passing/3941.purs b/tests/purs/passing/3941.purs new file mode 100644 index 0000000000..321ccedacb --- /dev/null +++ b/tests/purs/passing/3941.purs @@ -0,0 +1,25 @@ +module Main where + +import Effect.Console (log) +import Unsafe.Coerce (unsafeCoerce) + +class TwoParams a b where + func :: a -> b + +instance equals :: TwoParams a a where + func a = a +else +instance any :: TwoParams a b where + func = unsafeCoerce + +testEquals :: forall a. a -> a +testEquals = func -- with instance `equals` +testAny :: Int -> Boolean +testAny = func -- with instance `any` + +-- `a` and `m a` are never unifiable unless we have infinite types (and of course not) +-- so expected that the instance `any` is chosen. +thisShouldBeCompiled :: forall m a. a -> m a +thisShouldBeCompiled = func + +main = log "Done"