@@ -18,6 +18,7 @@ import Control.Arrow (Arrow(..))
1818import Control.Monad.State
1919import Control.Monad.Error.Class (MonadError(..))
2020import Control.Monad.Writer.Class (MonadWriter(..))
21+import Control.Monad.Supply.Class (MonadSupply(..))
2122
2223import Language.PureScript.Crash
2324import Language.PureScript.AST
@@ -34,11 +35,11 @@ import qualified Language.PureScript.Constants as C
3435--
3536entails
3637 :: forall m
37− . (Functor m, Applicative m, MonadError MultipleErrors m, MonadWriter MultipleErrors m)
38+ . (Functor m, Applicative m, MonadError MultipleErrors m, MonadWriter MultipleErrors m, MonadSupply m)
3839 => ModuleName
3940 -> M.Map (Maybe ModuleName) (M.Map (Qualified (ProperName 'ClassName)) (M.Map (Qualified Ident) TypeClassDictionaryInScope))
4041 -> Constraint
41− -> m Expr
42+ -> m (Expr, [(Ident, Constraint)])
4243entails moduleName context = solve
4344 where
4445 forClassName :: Qualified (ProperName 'ClassName) -> [Type] -> [TypeClassDictionaryInScope]
@@ -54,12 +55,12 @@ entails moduleName context = solve
5455 findDicts :: Qualified (ProperName 'ClassName) -> Maybe ModuleName -> [TypeClassDictionaryInScope]
5556 findDicts cn = maybe [] M.elems . (>>= M.lookup cn) . flip M.lookup context
5657
57− solve :: Constraint -> m Expr
58+ solve :: Constraint -> m (Expr, [(Ident, Constraint)])
5859 solve (className, tys) = do
59− dict <- go 0 className tys
60− return $ dictionaryValueToValue dict
60+ (dict, unsolved) <- go 0 className tys
61+ return (dictionaryValueToValue dict, unsolved)
6162 where
62− go :: Int -> Qualified (ProperName 'ClassName) -> [Type] -> m DictionaryValue
63+ go :: Int -> Qualified (ProperName 'ClassName) -> [Type] -> m (DictionaryValue, [(Ident, Constraint)])
6364 go work className' tys' | work > 1000 = throwError . errorMessage $ PossiblyInfiniteInstance className' tys'
6465 go work className' tys' = do
6566 let instances = do
@@ -67,21 +68,33 @@ entails moduleName context = solve
6768 -- Make sure the type unifies with the type in the type instance definition
6869 subst <- maybeToList . (>>= verifySubstitution) . fmap concat $ zipWithM (typeHeadsAreEqual moduleName) tys' (tcdInstanceTypes tcd)
6970 return (subst, tcd)
70− (subst, tcd) <- unique instances
71− -- Solve any necessary subgoals
72− args <- solveSubgoals subst (tcdDependencies tcd)
73− return $ foldr (\(superclassName, index) dict -> SubclassDictionaryValue dict superclassName index)
74− (mkDictionary (tcdName tcd) args)
75− (tcdPath tcd)
71+ solution <- unique instances
72+ case solution of
73+ Left (subst, tcd) -> do
74+ -- Solve any necessary subgoals
75+ (args, unsolved) <- solveSubgoals subst (tcdDependencies tcd)
76+ let match = foldr (\(superclassName, index) dict -> SubclassDictionaryValue dict superclassName index)
77+ (mkDictionary (tcdName tcd) args)
78+ (tcdPath tcd)
79+ return (match, unsolved)
80+ Right unsolved@(Qualified _ (ProperName unsolvedClassName), _) -> do
81+ ident <- freshIdent ("dict" ++ unsolvedClassName)
82+ return (LocalDictionaryValue (Qualified Nothing ident), [(ident, unsolved)])
7683 where
7784
78− unique :: [(a, TypeClassDictionaryInScope)] -> m (a, TypeClassDictionaryInScope)
79− unique [] = throwError . errorMessage $ NoInstanceFound className' tys'
80− unique [a] = return a
85+ unique :: [(a, TypeClassDictionaryInScope)] -> m (Either (a, TypeClassDictionaryInScope) Constraint)
86+ unique [] | all canBeGeneralized tys' = return $ Right (className, tys)
87+ | otherwise = throwError . errorMessage $ NoInstanceFound className' tys'
88+ unique [a] = return $ Left a
8189 unique tcds | pairwise overlapping (map snd tcds) = do
8290 tell . errorMessage $ OverlappingInstances className' tys' (map (tcdName . snd) tcds)
83− return (head tcds)
84− | otherwise = return (minimumBy (compare `on` length . tcdPath . snd) tcds)
91+ return $ Left (head tcds)
92+ | otherwise = return $ Left (minimumBy (compare `on` length . tcdPath . snd) tcds)
93+
94+ canBeGeneralized :: Type -> Bool
95+ canBeGeneralized TUnknown{} = True
96+ canBeGeneralized Skolem{} = True
97+ canBeGeneralized _ = False
8598
8699 -- |
87100 -- Check if two dictionaries are overlapping
@@ -98,11 +111,12 @@ entails moduleName context = solve
98111 -- Create dictionaries for subgoals which still need to be solved by calling go recursively
99112 -- E.g. the goal (Show a, Show b) => Show (Either a b) can be satisfied if the current type
100113 -- unifies with Either a b, and we can satisfy the subgoals Show a and Show b recursively.
101− solveSubgoals :: [(String, Type)] -> Maybe [Constraint] -> m (Maybe [DictionaryValue])
102− solveSubgoals _ Nothing = return Nothing
114+ solveSubgoals :: [(String, Type)] -> Maybe [Constraint] -> m (Maybe [DictionaryValue], [(Ident, Constraint)])
115+ solveSubgoals _ Nothing = return (Nothing, [])
103116 solveSubgoals subst (Just subgoals) = do
104− dict <- traverse (uncurry (go (work + 1)) . second (map (replaceAllTypeVars subst))) subgoals
105− return $ Just dict
117+ zipped <- traverse (uncurry (go (work + 1)) . second (map (replaceAllTypeVars subst))) subgoals
118+ let (dicts, unsolved) = unzip zipped
119+ return (Just dicts, concat unsolved)
106120
107121 -- Make a dictionary from subgoal dictionaries by applying the correct function
108122 mkDictionary :: Qualified Ident -> Maybe [DictionaryValue] -> DictionaryValue