@@ -4,7 +4,7 @@
44-- |
55-- Type class entailment
66--
7−module Language.PureScript.TypeChecker.Entailment (entails) where
7+module Language.PureScript.TypeChecker.Entailment (Context, replaceTypeClassDictionaries) where
88
99import Prelude ()
1010import Prelude.Compat
@@ -16,8 +16,8 @@ import qualified Data.Map as M
1616
1717import Control.Arrow (Arrow(..))
1818import Control.Monad.State
19+import Control.Monad.Writer
1920import Control.Monad.Error.Class (MonadError(..))
20−import Control.Monad.Writer.Class (MonadWriter(..))
2121import Control.Monad.Supply.Class (MonadSupply(..))
2222
2323import Language.PureScript.Crash
@@ -29,6 +29,30 @@ import Language.PureScript.TypeClassDictionaries
2929import Language.PureScript.Types
3030import qualified Language.PureScript.Constants as C
3131
32+-- | The 'Context' tracks those constraints which can be satisfied.
33+type Context = M.Map (Maybe ModuleName)
34+ (M.Map (Qualified (ProperName 'ClassName))
35+ (M.Map (Qualified Ident)
36+ TypeClassDictionaryInScope))
37+
38+-- | Merge two type class contexts
39+combineContexts :: Context -> Context -> Context
40+combineContexts = M.unionWith (M.unionWith M.union)
41+
42+-- | Replace type class dictionary placeholders with inferred type class dictionaries
43+replaceTypeClassDictionaries
44+ :: (Functor m, Applicative m, MonadError MultipleErrors m, MonadWriter MultipleErrors m, MonadSupply m)
45+ => Bool
46+ -> ModuleName
47+ -> Expr
48+ -> m (Expr, [(Ident, Constraint)])
49+replaceTypeClassDictionaries shouldGeneralize mn =
50+ let (_, f, _) = everywhereOnValuesTopDownM return (WriterT . go) return
51+ in flip evalStateT M.empty . runWriterT . f
52+ where
53+ go (TypeClassDictionary constraint dicts) = entails shouldGeneralize mn dicts constraint
54+ go other = return (other, [])
55+
3256-- |
3357-- Check that the current set of type class dictionaries entail the specified type class goal, and, if so,
3458-- return a type class dictionary reference.
@@ -38,14 +62,14 @@ entails
3862 . (Functor m, Applicative m, MonadError MultipleErrors m, MonadWriter MultipleErrors m, MonadSupply m)
3963 => Bool
4064 -> ModuleName
41− -> M.Map (Maybe ModuleName) (M.Map (Qualified (ProperName 'ClassName)) (M.Map (Qualified Ident) TypeClassDictionaryInScope))
65+ -> Context
4266 -> Constraint
43− -> m (Expr, [(Ident, Constraint)])
67+ -> StateT Context m (Expr, [(Ident, Constraint)])
4468entails shouldGeneralize moduleName context = solve
4569 where
46− forClassName :: Qualified (ProperName 'ClassName) -> [Type] -> [TypeClassDictionaryInScope]
47− forClassName cn@(Qualified (Just mn) _) tys = concatMap (findDicts cn) (Nothing : Just mn : map Just (mapMaybe ctorModules tys))
48− forClassName _ _ = internalError "forClassName: expected qualified class name"
70+ forClassName :: Context -> Qualified (ProperName 'ClassName) -> [Type] -> [TypeClassDictionaryInScope]
71+ forClassName ctx cn@(Qualified (Just mn) _) tys = concatMap (findDicts ctx cn) (Nothing : Just mn : map Just (mapMaybe ctorModules tys))
72+ forClassName _ _ _ = internalError "forClassName: expected qualified class name"
4973
5074 ctorModules :: Type -> Maybe ModuleName
5175 ctorModules (TypeConstructor (Qualified (Just mn) _)) = Just mn
@@ -53,23 +77,25 @@ entails shouldGeneralize moduleName context = solve
5377 ctorModules (TypeApp ty _) = ctorModules ty
5478 ctorModules _ = Nothing
5579
56− findDicts :: Qualified (ProperName 'ClassName) -> Maybe ModuleName -> [TypeClassDictionaryInScope]
57− findDicts cn = maybe [] M.elems . (>>= M.lookup cn) . flip M.lookup context
80+ findDicts :: Context -> Qualified (ProperName 'ClassName) -> Maybe ModuleName -> [TypeClassDictionaryInScope]
81+ findDicts ctx cn = maybe [] M.elems . (>>= M.lookup cn) . flip M.lookup ctx
5882
59− solve :: Constraint -> m (Expr, [(Ident, Constraint)])
83+ solve :: Constraint -> StateT Context m (Expr, [(Ident, Constraint)])
6084 solve (className, tys) = do
6185 (dict, unsolved) <- go 0 className tys
6286 return (dictionaryValueToValue dict, unsolved)
6387 where
64− go :: Int -> Qualified (ProperName 'ClassName) -> [Type] -> m (DictionaryValue, [(Ident, Constraint)])
88+ go :: Int -> Qualified (ProperName 'ClassName) -> [Type] -> StateT Context m (DictionaryValue, [(Ident, Constraint)])
6589 go work className' tys' | work > 1000 = throwError . errorMessage $ PossiblyInfiniteInstance className' tys'
6690 go work className' tys' = do
91+ -- Get the inferred constraint context so far, and merge it with the global context
92+ inferred <- get
6793 let instances = do
68− tcd <- forClassName className' tys'
94+ tcd <- forClassName (combineContexts context inferred) className' tys'
6995 -- Make sure the type unifies with the type in the type instance definition
7096 subst <- maybeToList . (>>= verifySubstitution) . fmap concat $ zipWithM (typeHeadsAreEqual moduleName) tys' (tcdInstanceTypes tcd)
7197 return (subst, tcd)
72− solution <- unique instances
98+ solution <- lift $ unique instances
7399 case solution of
74100 Left (subst, tcd) -> do
75101 -- Solve any necessary subgoals
@@ -78,9 +104,16 @@ entails shouldGeneralize moduleName context = solve
78104 (mkDictionary (tcdName tcd) args)
79105 (tcdPath tcd)
80106 return (match, unsolved)
81− Right unsolved@(Qualified _ (ProperName unsolvedClassName), _) -> do
82− ident <- freshIdent ("dict" ++ unsolvedClassName)
83− return (LocalDictionaryValue (Qualified Nothing ident), [(ident, unsolved)])
107+ Right unsolved@(unsolvedClassName@(Qualified _ pn), unsolvedTys) -> do
108+ -- Generate a fresh name for the unsolved constraint's new dictionary
109+ ident <- freshIdent ("dict" ++ runProperName pn)
110+ let qident = Qualified Nothing ident
111+ -- Store the new dictionary in the Context so that we can solve this goal in
112+ -- future.
113+ let newDict = TypeClassDictionaryInScope qident [] unsolvedClassName unsolvedTys Nothing
114+ newContext = M.singleton Nothing (M.singleton unsolvedClassName (M.singleton qident newDict))
115+ modify (combineContexts newContext)
116+ return (LocalDictionaryValue qident, [(ident, unsolved)])
84117 where
85118
86119 unique :: [(a, TypeClassDictionaryInScope)] -> m (Either (a, TypeClassDictionaryInScope) Constraint)
@@ -112,7 +145,7 @@ entails shouldGeneralize moduleName context = solve
112145 -- Create dictionaries for subgoals which still need to be solved by calling go recursively
113146 -- E.g. the goal (Show a, Show b) => Show (Either a b) can be satisfied if the current type
114147 -- unifies with Either a b, and we can satisfy the subgoals Show a and Show b recursively.
115− solveSubgoals :: [(String, Type)] -> Maybe [Constraint] -> m (Maybe [DictionaryValue], [(Ident, Constraint)])
148+ solveSubgoals :: [(String, Type)] -> Maybe [Constraint] -> StateT Context m (Maybe [DictionaryValue], [(Ident, Constraint)])
116149 solveSubgoals _ Nothing = return (Nothing, [])
117150 solveSubgoals subst (Just subgoals) = do
118151 zipped <- traverse (uncurry (go (work + 1)) . second (map (replaceAllTypeVars subst))) subgoals
@@ -149,6 +182,7 @@ entails shouldGeneralize moduleName context = solve
149182-- and return a substitution from type variables to types which makes the type heads unify.
150183--
151184typeHeadsAreEqual :: ModuleName -> Type -> Type -> Maybe [(String, Type)]
185+typeHeadsAreEqual _ (TUnknown u1) (TUnknown u2) | u1 == u2 = Just []
152186typeHeadsAreEqual _ (Skolem _ s1 _ _) (Skolem _ s2 _ _) | s1 == s2 = Just []
153187typeHeadsAreEqual _ t (TypeVar v) = Just [(v, t)]
154188typeHeadsAreEqual _ (TypeConstructor c1) (TypeConstructor c2) | c1 == c2 = Just []