diff --git a/CHANGELOG.md b/CHANGELOG.md index 6191fb1973..b6abcbff4e 100644 --- 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 index 9029417740..cc8c8ce1e5 100644 --- 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 index eb338a018c..067c5eb408 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.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 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..ce9bbe6c77 --- /dev/null +++ b/tests/purs/failing/3329.out @@ -0,0 +1,28 @@ +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 following instance partially overlaps the above constraint, which means the rest of its instance chain will not be considered: + + Main.injectLeft + + +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..dcb39d4592 --- /dev/null +++ b/tests/purs/failing/3531-2.out @@ -0,0 +1,27 @@ +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 following instance partially overlaps the above constraint, which means the rest of its instance chain will not be considered: + + Main.cx + + 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..8f52a662cc --- /dev/null +++ b/tests/purs/failing/3531-3.out @@ -0,0 +1,32 @@ +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 following instance partially overlaps the above constraint, which means the rest of its instance chain will not be considered: + + Main.cx + + 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..f82fb0d6a1 --- /dev/null +++ b/tests/purs/failing/3531-5.out @@ -0,0 +1,32 @@ +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 following instance partially overlaps the above constraint, which means the rest of its instance chain will not be considered: + + instance in module Main with type forall a. C String (Array a) (line 9, column 1 - line 10, column 15) + + +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..f454d0679e --- /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) (line 9, column 1 - line 10, column 15) + instance in module Main with type C Int Int (line 14, column 1 - line 15, column 15) + + +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..71e3f55972 --- /dev/null +++ b/tests/purs/failing/3531.out @@ -0,0 +1,27 @@ +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 following instance partially overlaps the above constraint, which means the rest of its instance chain will not be considered: + + Main.c1 + + +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..477c18364a --- /dev/null +++ b/tests/purs/failing/4028.out @@ -0,0 +1,27 @@ +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 following instance partially overlaps the above constraint, which means the rest of its instance chain will not be considered: + + Main.tlShow2 + + +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..f08c540f40 100644 --- a/tests/purs/failing/InstanceChainBothUnknownAndMatch.out +++ b/tests/purs/failing/InstanceChainBothUnknownAndMatch.out @@ -16,6 +16,10 @@ at tests/purs/failing/InstanceChainBothUnknownAndMatch.purs:17:13 - 17:55 (line  )   t4    + The following instance partially overlaps the above constraint, which means the rest of its instance chain will not be considered: + + InstanceChains.BothUnknownAndMatch.sameY + 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..fa66f419ef 100644 --- a/tests/purs/failing/InstanceChainSkolemUnknownMatch.out +++ b/tests/purs/failing/InstanceChainSkolemUnknownMatch.out @@ -8,6 +8,10 @@ at tests/purs/failing/InstanceChainSkolemUnknownMatch.purs:14:13 - 14:36 (line 1  (Proxy Int)  t4    + The following instance partially overlaps the above constraint, which means the rest of its instance chain will not be considered: + + InstanceChainSkolemUnknownMatch.sameY + 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"