Merge pull request #1406 from purescript/421

Fix #421, match type instance heads eagerly

examples/failing/438.purs

@@ -1,4 +1,4 @@
--- @shouldFailWith NoInstanceFound
+-- @shouldFailWith PossiblyInfiniteInstance
 
 -- See issue 438 for details: this test is mainly here to test that code like
 -- this doesn't cause the compiler to loop.

examples/passing/Superclasses2.purs → examples/failing/Superclasses5.purs

@@ -1,3 +1,5 @@
+-- @shouldFailWith NoInstanceFound
+
 module Main where
 
 import Prelude

src/Language/PureScript/AST/Declarations.hs

@@ -386,7 +386,7 @@ data Expr
   -- at superclass implementations when searching for a dictionary, the type class name and
   -- instance type, and the type class dictionaries in scope.
   --
-  | TypeClassDictionary Bool Constraint (M.Map (Maybe ModuleName) (M.Map (Qualified ProperName) (M.Map (Qualified Ident) TypeClassDictionaryInScope)))
+  | TypeClassDictionary Constraint (M.Map (Maybe ModuleName) (M.Map (Qualified ProperName) (M.Map (Qualified Ident) TypeClassDictionaryInScope)))
   -- |
   -- A typeclass dictionary accessor, the implementation is left unspecified until CoreFn desugaring.
   --

src/Language/PureScript/AST/Traversals.hs

@@ -396,7 +396,7 @@ accumTypes f = everythingOnValues mappend forDecls forValues (const mempty) (con
   forDecls (TypeDeclaration _ ty) = f ty
   forDecls _ = mempty
 
-  forValues (TypeClassDictionary _ (_, cs) _) = mconcat (map f cs)
+  forValues (TypeClassDictionary (_, cs) _) = mconcat (map f cs)
   forValues (SuperClassDictionary _ tys) = mconcat (map f tys)
   forValues (TypedValue _ _ ty) = f ty
   forValues _ = mempty

src/Language/PureScript/Docs/ParseAndDesugar.hs

@@ -11,7 +11,7 @@ import Control.Monad
 import Control.Applicative
 
 import Control.Monad.Trans.Except
-import Control.Monad.Writer.Strict (WriterT(), runWriterT)
+import Control.Monad.Writer.Strict (runWriterT)
 import Control.Monad.Error.Class (MonadError(..))
 import Control.Monad.IO.Class (MonadIO(..))
 

src/Language/PureScript/Errors.hs

@@ -40,7 +40,6 @@ import Language.PureScript.Pretty
 import Language.PureScript.Types
 import Language.PureScript.Names
 import Language.PureScript.Kinds
-import Language.PureScript.TypeClassDictionaries
 
 import qualified Text.PrettyPrint.Boxes as Box
 
@@ -108,8 +107,9 @@ data SimpleErrorMessage
   | TypesDoNotUnify Type Type
   | KindsDoNotUnify Kind Kind
   | ConstrainedTypeUnified Type Type
-  | OverlappingInstances (Qualified ProperName) [Type] [DictionaryValue]
+  | OverlappingInstances (Qualified ProperName) [Type] [Qualified Ident]
   | NoInstanceFound (Qualified ProperName) [Type]
+  | PossiblyInfiniteInstance (Qualified ProperName) [Type]
   | CannotDerive (Qualified ProperName) [Type]
   | CannotFindDerivingType ProperName
   | DuplicateLabel String (Maybe Expr)
@@ -233,6 +233,7 @@ errorCode em = case unwrapErrorMessage em of
   ConstrainedTypeUnified{} -> "ConstrainedTypeUnified"
   OverlappingInstances{} -> "OverlappingInstances"
   NoInstanceFound{} -> "NoInstanceFound"
+  PossiblyInfiniteInstance{} -> "PossiblyInfiniteInstance"
   CannotDerive{} -> "CannotDerive"
   CannotFindDerivingType{} -> "CannotFindDerivingType"
   DuplicateLabel{} -> "DuplicateLabel"
@@ -544,10 +545,12 @@ prettyPrintSingleError full level e = prettyPrintErrorMessage <$> onTypesInError
             ]
     goSimple (OverlappingInstances nm ts ds) =
       paras [ line $ "Overlapping instances found for " ++ show nm ++ " " ++ unwords (map prettyPrintTypeAtom ts) ++ ":"
-            , paras $ map prettyPrintDictionaryValue ds
+            , line $ intercalate ", " (map show ds)
             ]
     goSimple (NoInstanceFound nm ts) =
       line $ "No instance found for " ++ show nm ++ " " ++ unwords (map prettyPrintTypeAtom ts)
+    goSimple (PossiblyInfiniteInstance nm ts) =
+      line $ "Instance for " ++ show nm ++ " " ++ unwords (map prettyPrintTypeAtom ts) ++ " is possibly infinite."
     goSimple (CannotDerive nm ts) =
       line $ "Cannot derive " ++ show nm ++ " instance for " ++ unwords (map prettyPrintTypeAtom ts)
     goSimple (CannotFindDerivingType nm) =
@@ -736,19 +739,6 @@ prettyPrintSingleError full level e = prettyPrintErrorMessage <$> onTypesInError
   indent :: Box.Box -> Box.Box
   indent = Box.moveRight 2
 
-  -- |
-  -- Render a DictionaryValue fit for human consumption in error messages
-  --
-  prettyPrintDictionaryValue :: DictionaryValue -> Box.Box
-  prettyPrintDictionaryValue (LocalDictionaryValue _)           = line "Dictionary in scope"
-  prettyPrintDictionaryValue (GlobalDictionaryValue nm)         = line (show nm)
-  prettyPrintDictionaryValue (DependentDictionaryValue nm args) = paras [ line $ (show nm) ++ " via"
-                                                                        , indent $ paras $ map prettyPrintDictionaryValue args
-                                                                        ]
-  prettyPrintDictionaryValue (SubclassDictionaryValue sup nm _) = paras [ line $ (show nm) ++ " via superclass"
-                                                                        , indent $ prettyPrintDictionaryValue sup
-                                                                        ]
-
   -- |
   -- Pretty print and export declaration
   --

src/Language/PureScript/Pretty/Values.hs

@@ -74,7 +74,7 @@ literals = mkPattern' match
     ]
   match (OperatorSection op (Right val)) = return $ "(" ++ prettyPrintValue op ++ " " ++ prettyPrintValue val ++ ")"
   match (OperatorSection op (Left val)) = return $ "(" ++ prettyPrintValue val ++ " " ++ prettyPrintValue op ++ ")"
-  match (TypeClassDictionary _ (name, tys) _) = return $ "<<dict " ++ show name ++ " " ++ unwords (map prettyPrintTypeAtom tys) ++ ">>"
+  match (TypeClassDictionary (name, tys) _) = return $ "<<dict " ++ show name ++ " " ++ unwords (map prettyPrintTypeAtom tys) ++ ">>"
   match (SuperClassDictionary name _) = return $ "<<superclass dict " ++ show name ++ ">>"
   match (TypedValue _ val _) = prettyPrintValue' val
   match (PositionedValue _ _ val) = prettyPrintValue' val

src/Language/PureScript/TypeChecker.hs

@@ -130,7 +130,7 @@ checkTypeSynonyms = void . replaceAllTypeSynonyms
 --  * Process module imports
 --
 typeCheckAll :: Maybe ModuleName -> ModuleName -> [DeclarationRef] -> [Declaration] -> Check [Declaration]
-typeCheckAll mainModuleName moduleName exps ds = mapM go ds <* mapM_ checkOrphanFixities ds
+typeCheckAll mainModuleName moduleName _ ds = mapM go ds <* mapM_ checkOrphanFixities ds
   where
   go :: Declaration -> Check Declaration
   go (DataDeclaration dtype name args dctors) = do
@@ -236,16 +236,16 @@ typeCheckAll mainModuleName moduleName exps ds = mapM go ds <* mapM_ checkOrphan
     mapM_ (checkTypeClassInstance moduleName) tys
     forM_ deps $ mapM_ (checkTypeClassInstance moduleName) . snd
     checkOrphanInstance moduleName className tys
-    let dict = TypeClassDictionaryInScope (Qualified (Just moduleName) dictName) className tys (Just deps) TCDRegular isInstanceExported
+    let dict = TypeClassDictionaryInScope (Qualified (Just moduleName) dictName) [] className tys (Just deps) TCDRegular
     addTypeClassDictionaries (Just moduleName) . M.singleton className $ M.singleton (canonicalizeDictionary dict) dict
     return d
 
     where
 
     checkOrphanInstance :: ModuleName -> Qualified ProperName -> [Type] -> Check ()
-    checkOrphanInstance mn (Qualified (Just mn') _) tys
-      | mn == mn' || any checkType tys = return ()
-      | otherwise = throwError . errorMessage $ OrphanInstance dictName className tys
+    checkOrphanInstance mn (Qualified (Just mn') _) tys'
+      | mn == mn' || any checkType tys' = return ()
+      | otherwise = throwError . errorMessage $ OrphanInstance dictName className tys'
       where
       checkType :: Type -> Bool
       checkType (TypeVar _) = False
@@ -255,14 +255,6 @@ typeCheckAll mainModuleName moduleName exps ds = mapM go ds <* mapM_ checkOrphan
       checkType _ = error "Invalid type in instance in checkOrphanInstance"
     checkOrphanInstance _ _ _ = error "Unqualified class name in checkOrphanInstance"
 
-    isInstanceExported :: Bool
-    isInstanceExported = any exportsInstance exps
-
-    exportsInstance :: DeclarationRef -> Bool
-    exportsInstance (TypeInstanceRef name) | name == dictName = True
-    exportsInstance (PositionedDeclarationRef _ _ r) = exportsInstance r
-    exportsInstance _ = False
-
   -- |
   -- This function adds the argument kinds for a type constructor so that they may appear in the externs file,
   -- extracted from the kind of the type constructor itself.

src/Language/PureScript/TypeChecker/Entailment.hs

@@ -41,13 +41,11 @@ import Language.PureScript.TypeClassDictionaries
 import Language.PureScript.Types
 import qualified Language.PureScript.Constants as C
 
-newtype Work = Work Integer deriving (Show, Eq, Ord, Num)
-
 -- |
 -- Check that the current set of type class dictionaries entail the specified type class goal, and, if so,
 -- return a type class dictionary reference.
 --
-entails :: Environment -> ModuleName -> M.Map (Maybe ModuleName) (M.Map (Qualified ProperName) (M.Map (Qualified Ident) TypeClassDictionaryInScope)) -> Constraint -> Bool -> Check Expr
+entails :: Environment -> ModuleName -> M.Map (Maybe ModuleName) (M.Map (Qualified ProperName) (M.Map (Qualified Ident) TypeClassDictionaryInScope)) -> Constraint -> Check Expr
 entails env moduleName context = solve
   where
     forClassName :: Qualified ProperName -> [TypeClassDictionaryInScope]
@@ -56,56 +54,57 @@ entails env moduleName context = solve
     findDicts :: Qualified ProperName -> Maybe ModuleName -> [TypeClassDictionaryInScope]
     findDicts cn = maybe [] M.elems . (>>= M.lookup cn) . flip M.lookup context
 
-    solve :: Constraint -> Bool -> Check Expr
-    solve (className, tys) trySuperclasses = do
-      let dicts = flip evalStateT (Work 0) $ go trySuperclasses className tys
-      checkOverlaps dicts
+    solve :: Constraint -> Check Expr
+    solve (className, tys) = do
+      dict <- go 0 className tys
+      return $ dictionaryValueToValue dict
       where
-      go :: Bool -> Qualified ProperName -> [Type] -> StateT Work [] DictionaryValue
-      go trySuperclasses' className' tys' = do
-        workDone <- get
-        guard $ workDone < 1000
-        modify (1 +)
-        directInstances <|> superclassInstances
+      go :: Int -> Qualified ProperName -> [Type] -> Check DictionaryValue
+      go work className' tys' | work > 1000 = throwError . errorMessage $ PossiblyInfiniteInstance className' tys'
+      go work className' tys' = do
+        let instances = do
+              tcd <- forClassName className'
+              -- Make sure the type unifies with the type in the type instance definition
+              subst <- maybeToList . (>>= verifySubstitution) . fmap concat $ zipWithM (typeHeadsAreEqual moduleName env) tys' (tcdInstanceTypes tcd)
+              return (subst, tcd)
+        (subst, tcd) <- unique instances
+        -- Solve any necessary subgoals
+        args <- solveSubgoals subst (tcdDependencies tcd)
+        return $ foldr (\(superclassName, index) dict -> SubclassDictionaryValue dict superclassName index) 
+                       (mkDictionary (canonicalizeDictionary tcd) args) 
+                       (tcdPath tcd)
         where
-        directInstances :: StateT Work [] DictionaryValue
-        directInstances = do
-          tcd <- lift $ forClassName className'
-          -- Make sure the type unifies with the type in the type instance definition
-          subst <- lift . maybeToList . (>>= verifySubstitution) . fmap concat $ zipWithM (typeHeadsAreEqual moduleName env) tys' (tcdInstanceTypes tcd)
-          -- Solve any necessary subgoals
-          args <- solveSubgoals subst (tcdDependencies tcd)
-          return $ mkDictionary (canonicalizeDictionary tcd) args
+
+        unique :: [(a, TypeClassDictionaryInScope)] -> Check (a, TypeClassDictionaryInScope)
+        unique [] = throwError . errorMessage $ NoInstanceFound className' tys'
+        unique [a] = return a
+        unique tcds | pairwise overlapping (map snd tcds) = throwError . errorMessage $ OverlappingInstances className' tys' (map (tcdName . snd) tcds)
+                    | otherwise = return (minimumBy (compare `on` length . tcdPath . snd) tcds)
 
-        superclassInstances :: StateT Work [] DictionaryValue
-        superclassInstances = do
-          guard trySuperclasses'
-          (subclassName, (args, _, implies)) <- lift $ M.toList (typeClasses env)
-          -- Try each superclass
-          (index, (superclass, suTyArgs)) <- lift $ zip [0..] implies
-          -- Make sure the type class name matches the superclass name
-          guard $ className' == superclass
-          -- Make sure the types unify with the types in the superclass implication
-          subst <- lift . maybeToList . (>>= verifySubstitution) . fmap concat $ zipWithM (typeHeadsAreEqual moduleName env) tys' suTyArgs
-          -- Finally, satisfy the subclass constraint
-          args' <- lift . maybeToList $ mapM ((`lookup` subst) . fst) args
-          suDict <- go True subclassName args'
-          return $ SubclassDictionaryValue suDict superclass index
+        -- |
+        -- Check if two dictionaries are overlapping
+        --
+        -- Dictionaries which are subclass dictionaries cannot overlap, since otherwise the overlap would have
+        -- been caught when constructing superclass dictionaries.
+        overlapping :: TypeClassDictionaryInScope -> TypeClassDictionaryInScope -> Bool
+        overlapping TypeClassDictionaryInScope{ tcdPath = _ : _ } _ = False
+        overlapping _ TypeClassDictionaryInScope{ tcdPath = _ : _ } = False
+        overlapping tcd1 tcd2 = tcdName tcd1 /= tcdName tcd2
 
-      -- Create dictionaries for subgoals which still need to be solved by calling go recursively
-      -- E.g. the goal (Show a, Show b) => Show (Either a b) can be satisfied if the current type
-      -- unifies with Either a b, and we can satisfy the subgoals Show a and Show b recursively.
-      solveSubgoals :: [(String, Type)] -> Maybe [Constraint] -> StateT Work [] (Maybe [DictionaryValue])
-      solveSubgoals _ Nothing = return Nothing
-      solveSubgoals subst (Just subgoals) = do
-        dict <- mapM (uncurry (go True) . second (map (replaceAllTypeVars subst))) subgoals
-        return $ Just dict
+        -- Create dictionaries for subgoals which still need to be solved by calling go recursively
+        -- E.g. the goal (Show a, Show b) => Show (Either a b) can be satisfied if the current type
+        -- unifies with Either a b, and we can satisfy the subgoals Show a and Show b recursively.
+        solveSubgoals :: [(String, Type)] -> Maybe [Constraint] -> Check (Maybe [DictionaryValue])
+        solveSubgoals _ Nothing = return Nothing
+        solveSubgoals subst (Just subgoals) = do
+          dict <- mapM (uncurry (go (work + 1)) . second (map (replaceAllTypeVars subst))) subgoals
+          return $ Just dict
 
-      -- Make a dictionary from subgoal dictionaries by applying the correct function
-      mkDictionary :: Qualified Ident -> Maybe [DictionaryValue] -> DictionaryValue
-      mkDictionary fnName Nothing = LocalDictionaryValue fnName
-      mkDictionary fnName (Just []) = GlobalDictionaryValue fnName
-      mkDictionary fnName (Just dicts) = DependentDictionaryValue fnName dicts
+        -- Make a dictionary from subgoal dictionaries by applying the correct function
+        mkDictionary :: Qualified Ident -> Maybe [DictionaryValue] -> DictionaryValue
+        mkDictionary fnName Nothing = LocalDictionaryValue fnName
+        mkDictionary fnName (Just []) = GlobalDictionaryValue fnName
+        mkDictionary fnName (Just dicts) = DependentDictionaryValue fnName dicts
 
       -- Turn a DictionaryValue into a Expr
       dictionaryValueToValue :: DictionaryValue -> Expr
@@ -122,46 +121,7 @@ entails env moduleName context = solve
         let grps = groupBy ((==) `on` fst) subst
         guard (all (pairwise (unifiesWith env) . map snd) grps)
         return $ map head grps
-      -- |
-      -- Check for overlapping instances
-      --
-      checkOverlaps :: [DictionaryValue] -> Check Expr
-      checkOverlaps dicts =
-        case [ (d1, d2) | d1 <- dicts, d2 <- dicts, d1 `overlapping` d2 ] of
-          ds@(_ : _) -> throwError . errorMessage $ OverlappingInstances className tys $ nub (map fst ds)
-          _ -> case chooseSimplestDictionaries dicts of
-                 [] -> throwError . errorMessage $ NoInstanceFound className tys
-                 d : _ -> return $ dictionaryValueToValue d
-      -- Choose the simplest DictionaryValues from a list of candidates
-      -- The reason for this function is as follows:
-      -- When considering overlapping instances, we don't want to consider the same dictionary
-      -- to be an overlap of itself when obtained as a superclass of another class.
-      -- Observing that we probably don't want to select a superclass instance when an instance
-      -- is available directly, and that there is no way for a superclass instance to actually
-      -- introduce an overlap that wouldn't have been there already, we simply remove dictionaries
-      -- obtained as superclass instances if there are simpler instances available.
-      chooseSimplestDictionaries :: [DictionaryValue] -> [DictionaryValue]
-      chooseSimplestDictionaries ds = case filter isSimpleDictionaryValue ds of
-                                        [] -> ds
-                                        simple -> simple
-      isSimpleDictionaryValue SubclassDictionaryValue{} = False
-      isSimpleDictionaryValue (DependentDictionaryValue _ ds) = all isSimpleDictionaryValue ds
-      isSimpleDictionaryValue _ = True
-      -- |
-      -- Check if two dictionaries are overlapping
-      --
-      -- Dictionaries which are subclass dictionaries cannot overlap, since otherwise the overlap would have
-      -- been caught when constructing superclass dictionaries.
-      --
-      overlapping :: DictionaryValue -> DictionaryValue -> Bool
-      overlapping (LocalDictionaryValue nm1)         (LocalDictionaryValue nm2)  | nm1 == nm2 = False
-      overlapping (GlobalDictionaryValue nm1)        (GlobalDictionaryValue nm2) | nm1 == nm2 = False
-      overlapping (DependentDictionaryValue nm1 ds1) (DependentDictionaryValue nm2 ds2)
-        | nm1 == nm2 = or $ zipWith overlapping ds1 ds2
-      overlapping SubclassDictionaryValue{} _ = False
-      overlapping _ SubclassDictionaryValue{} = False
-      overlapping _ _ = True
-
+
     valUndefined :: Expr
     valUndefined = Var (Qualified (Just (ModuleName [ProperName C.prim])) (Ident C.undefined))
 

src/Language/PureScript/TypeChecker/Subsumption.hs

@@ -69,7 +69,7 @@ subsumes' val ty1 (KindedType ty2 _) =
   subsumes val ty1 ty2
 subsumes' (Just val) (ConstrainedType constraints ty1) ty2 = do
   dicts <- getTypeClassDictionaries
-  subsumes' (Just $ foldl App val (map (flip (TypeClassDictionary True) dicts) constraints)) ty1 ty2
+  subsumes' (Just $ foldl App val (map (flip TypeClassDictionary dicts) constraints)) ty1 ty2
 subsumes' val (TypeApp f1 r1) (TypeApp f2 r2) | f1 == tyObject && f2 == tyObject = do
   let
     (ts1, r1') = rowToList r1