git.iko.soy/rowtype-yoga/purescript-native
on golang help sign in
Merge pull request #1934 from purescript/202

Infer class constraints

commit8847b66dd346a889121f852d1b7716bd706c1a07 authorPhil Freeman <paf31@cantab.net> dateSun 13 Mar 2016, 14:30 (11 years ago) parent5dad0d65674d64
7 files changed+170−76
compare with golang
unifiedsplit
examples/failing/ConstraintInference.purs+10 examples/passing/ConstraintInference.purs+7 examples/passing/ContextSimplification.purs+13 examples/passing/MonadState.purs+32−19 src/Language/PureScript/TypeChecker/Entailment.hs+81−32 src/Language/PureScript/TypeChecker/Types.hs+26−25 src/Language/PureScript/TypeChecker/Unify.hs+1
examples/failing/ConstraintInference.pursnew file+10
@@ -0,0 +1,10 @@
1+-- @shouldFailWith NoInstanceFound
2+
3+module Main where
4+
5+import Prelude
6+
7+spin :: forall a b. a -> b
8+spin x = spin x
9+
10+test = show <<< spin
examples/passing/ConstraintInference.pursnew file+7
@@ -0,0 +1,7 @@
1+module Main where
2+
3+import Prelude
4+
5+shout = Control.Monad.Eff.Console.log <<< (<> "!") <<< show
6+
7+main = shout "Done"
examples/passing/ContextSimplification.pursnew file+13
@@ -0,0 +1,13 @@
1+module Main where
2+
3+import Prelude
4+import Control.Monad.Eff.Console
5+
6+shout = log <<< (<> "!") <<< show
7+
8+-- Here, we should simplify the context so that only one Show
9+-- constraint is added.
10+usesShowTwice true = shout
11+usesShowTwice false = print
12+
13+main = usesShowTwice true "Done"
examples/passing/MonadState.purs+32−19
@@ -1,12 +1,16 @@
11module Main where
22
33import Prelude
4+import Control.Monad.Eff.Console
45
56data Tuple a b = Tuple a b
67
7−class MonadState s m where
8+instance showTuple :: (Show a, Show b) => Show (Tuple a b) where
9+ show (Tuple a b) = "(" <> show a <> ", " <> show b <> ")"
10+
11+class Monad m <= MonadState s m where
812 get :: m s
9− put :: s -> m {}
13+ put :: s -> m Unit
1014
1115data State s a = State (s -> Tuple s a)
1216
@@ -29,20 +33,29 @@ instance monadState :: Monad (State s)
2933
3034instance monadStateState :: MonadState s (State s) where
3135 get = State (\s -> Tuple s s)
32− put s = State (\_ -> Tuple s {})
33−
34−modify :: forall m s. (Prelude.Monad m, MonadState s m) => (s -> s) -> m {}
35−modify f = do
36− s <- get
37− put (f s)
38−
39−test :: Tuple String String
40−test = runState "" $ do
41− modify $ (++) "World!"
42− modify $ (++) "Hello, "
43− get
44−
45−main = do
46− let t1 = test
47− Control.Monad.Eff.Console.log "Done"
48−
36+ put s = State (\_ -> Tuple s unit)
37+
38+-- Without the call to same, the following strange (but correct, in the absence of
39+-- functional dependencies) type:
40+--
41+-- forall m t1 t2.
42+-- ( Bind m
43+-- , MonadState t1 m
44+-- , MonadState t2 m
45+-- ) => (t1 -> t2) -> m Unit
46+--
47+-- With the type hint, the inferred type is more sensible:
48+--
49+-- forall m t.
50+-- ( Bind m
51+-- , MonadState t m
52+-- ) => (t -> t) -> m Unit
53+modify f =
54+ do
55+ s <- get
56+ put (same f s)
57+ where
58+ same :: forall a. (a -> a) -> (a -> a)
59+ same = id
60+
61+main = print $ runState 0 (modify (+ 1))
src/Language/PureScript/TypeChecker/Entailment.hs+81−32
@@ -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,9 @@ 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(..))
21+import Control.Monad.Supply.Class (MonadSupply(..))
2122
2223import Language.PureScript.Crash
2324import Language.PureScript.AST
@@ -28,22 +29,47 @@ import Language.PureScript.TypeClassDictionaries
2829import Language.PureScript.Types
2930import qualified Language.PureScript.Constants as C
3031
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+ :: (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+
3156-- |
3257-- Check that the current set of type class dictionaries entail the specified type class goal, and, if so,
3358-- return a type class dictionary reference.
3459--
3560entails
3661 :: forall m
37− . (MonadError MultipleErrors m, MonadWriter MultipleErrors m)
38− => ModuleName
39− -> M.Map (Maybe ModuleName) (M.Map (Qualified (ProperName 'ClassName)) (M.Map (Qualified Ident) TypeClassDictionaryInScope))
62+ . (MonadError MultipleErrors m, MonadWriter MultipleErrors m, MonadSupply m)
63+ => Bool
64+ -> ModuleName
65+ -> Context
4066 -> Constraint
41− -> m Expr
42−entails moduleName context = solve
67+ -> StateT Context m (Expr, [(Ident, Constraint)])
68+entails shouldGeneralize moduleName context = solve
4369 where
44− forClassName :: Qualified (ProperName 'ClassName) -> [Type] -> [TypeClassDictionaryInScope]
45− forClassName cn@(Qualified (Just mn) _) tys = concatMap (findDicts cn) (Nothing : Just mn : map Just (mapMaybe ctorModules tys))
46− 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"
4773
4874 ctorModules :: Type -> Maybe ModuleName
4975 ctorModules (TypeConstructor (Qualified (Just mn) _)) = Just mn
@@ -51,37 +77,58 @@ entails moduleName context = solve
5177 ctorModules (TypeApp ty _) = ctorModules ty
5278 ctorModules _ = Nothing
5379
54− findDicts :: Qualified (ProperName 'ClassName) -> Maybe ModuleName -> [TypeClassDictionaryInScope]
55− 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
5682
57− solve :: Constraint -> m Expr
83+ solve :: Constraint -> StateT Context m (Expr, [(Ident, Constraint)])
5884 solve (className, tys) = do
59− dict <- go 0 className tys
60− return $ dictionaryValueToValue dict
85+ (dict, unsolved) <- go 0 className tys
86+ return (dictionaryValueToValue dict, unsolved)
6187 where
62− go :: Int -> Qualified (ProperName 'ClassName) -> [Type] -> m DictionaryValue
88+ go :: Int -> Qualified (ProperName 'ClassName) -> [Type] -> StateT Context m (DictionaryValue, [(Ident, Constraint)])
6389 go work className' tys' | work > 1000 = throwError . errorMessage $ PossiblyInfiniteInstance className' tys'
6490 go work className' tys' = do
91+ -- Get the inferred constraint context so far, and merge it with the global context
92+ inferred <- get
6593 let instances = do
66− tcd <- forClassName className' tys'
94+ tcd <- forClassName (combineContexts context inferred) className' tys'
6795 -- Make sure the type unifies with the type in the type instance definition
6896 subst <- maybeToList . (>>= verifySubstitution) . fmap concat $ zipWithM (typeHeadsAreEqual moduleName) tys' (tcdInstanceTypes tcd)
6997 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)
98+ solution <- lift $ unique instances
99+ case solution of
100+ Left (subst, tcd) -> do
101+ -- Solve any necessary subgoals
102+ (args, unsolved) <- solveSubgoals subst (tcdDependencies tcd)
103+ let match = foldr (\(superclassName, index) dict -> SubclassDictionaryValue dict superclassName index)
104+ (mkDictionary (tcdName tcd) args)
105+ (tcdPath tcd)
106+ return (match, 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)])
76117 where
77118
78− unique :: [(a, TypeClassDictionaryInScope)] -> m (a, TypeClassDictionaryInScope)
79− unique [] = throwError . errorMessage $ NoInstanceFound className' tys'
80− unique [a] = return a
119+ unique :: [(a, TypeClassDictionaryInScope)] -> m (Either (a, TypeClassDictionaryInScope) Constraint)
120+ unique [] | shouldGeneralize && all canBeGeneralized tys' = return $ Right (className, tys)
121+ | otherwise = throwError . errorMessage $ NoInstanceFound className' tys'
122+ unique [a] = return $ Left a
81123 unique tcds | pairwise overlapping (map snd tcds) = do
82124 tell . errorMessage $ OverlappingInstances className' tys' (map (tcdName . snd) tcds)
83− return (head tcds)
84− | otherwise = return (minimumBy (compare `on` length . tcdPath . snd) tcds)
125+ return $ Left (head tcds)
126+ | otherwise = return $ Left (minimumBy (compare `on` length . tcdPath . snd) tcds)
127+
128+ canBeGeneralized :: Type -> Bool
129+ canBeGeneralized TUnknown{} = True
130+ canBeGeneralized Skolem{} = True
131+ canBeGeneralized _ = False
85132
86133 -- |
87134 -- Check if two dictionaries are overlapping
@@ -98,11 +145,12 @@ entails moduleName context = solve
98145 -- Create dictionaries for subgoals which still need to be solved by calling go recursively
99146 -- E.g. the goal (Show a, Show b) => Show (Either a b) can be satisfied if the current type
100147 -- 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
148+ solveSubgoals :: [(String, Type)] -> Maybe [Constraint] -> StateT Context m (Maybe [DictionaryValue], [(Ident, Constraint)])
149+ solveSubgoals _ Nothing = return (Nothing, [])
103150 solveSubgoals subst (Just subgoals) = do
104− dict <- traverse (uncurry (go (work + 1)) . second (map (replaceAllTypeVars subst))) subgoals
105− return $ Just dict
151+ zipped <- traverse (uncurry (go (work + 1)) . second (map (replaceAllTypeVars subst))) subgoals
152+ let (dicts, unsolved) = unzip zipped
153+ return (Just dicts, concat unsolved)
106154
107155 -- Make a dictionary from subgoal dictionaries by applying the correct function
108156 mkDictionary :: Qualified Ident -> Maybe [DictionaryValue] -> DictionaryValue
@@ -134,6 +182,7 @@ entails moduleName context = solve
134182-- and return a substitution from type variables to types which makes the type heads unify.
135183--
136184typeHeadsAreEqual :: ModuleName -> Type -> Type -> Maybe [(String, Type)]
185+typeHeadsAreEqual _ (TUnknown u1) (TUnknown u2) | u1 == u2 = Just []
137186typeHeadsAreEqual _ (Skolem _ s1 _ _) (Skolem _ s2 _ _) | s1 == s2 = Just []
138187typeHeadsAreEqual _ t (TypeVar v) = Just [(v, t)]
139188typeHeadsAreEqual _ (TypeConstructor c1) (TypeConstructor c2) | c1 == c2 = Just []
src/Language/PureScript/TypeChecker/Types.hs+26−25
@@ -2,6 +2,7 @@
22{-# LANGUAGE ScopedTypeVariables #-}
33{-# LANGUAGE MultiParamTypeClasses #-}
44{-# LANGUAGE OverloadedStrings #-}
5+{-# LANGUAGE TupleSections #-}
56
67-- |
78-- This module implements the type checker
@@ -69,23 +70,38 @@ typesOf moduleName vals = do
6970 tys <- fmap tidyUp . liftUnifyWarnings replace $ do
7071 (untyped, typed, dict, untypedDict) <- typeDictionaryForBindingGroup moduleName vals
7172 ds1 <- parU typed $ \e -> checkTypedBindingGroupElement moduleName e dict
72− ds2 <- forM untyped $ \e -> typeForBindingGroupElement True e dict untypedDict
73− return $ ds1 ++ ds2
73+ ds2 <- forM untyped $ \e -> typeForBindingGroupElement e dict untypedDict
74+ return (map (\x -> (False, x)) ds1 ++ map (\x -> (True, x)) ds2)
7475
75− forM tys $ \(ident, (val, ty)) -> do
76+ forM tys $ \(shouldGeneralize, (ident, (val, ty))) -> do
7677 -- Replace type class dictionary placeholders with actual dictionaries
77− val' <- replaceTypeClassDictionaries moduleName val
78+ (val', unsolved) <- replaceTypeClassDictionaries shouldGeneralize moduleName val
79+ let unsolvedTypeVars = nub $ unknownsInType ty
80+ -- Generalize and constrain the type
81+ let generalized = generalize unsolved ty
82+ -- Make sure any unsolved type constraints only use type variables which appear
83+ -- unknown in the inferred type.
84+ when shouldGeneralize $ do
85+ tell . errorMessage $ MissingTypeDeclaration ident generalized
86+ forM_ unsolved $ \(_, (className, classTys)) -> do
87+ let constraintTypeVars = nub $ foldMap unknownsInType classTys
88+ when (any (`notElem` unsolvedTypeVars) constraintTypeVars) $
89+ throwError . errorMessage $ NoInstanceFound className classTys
7890 -- Check skolem variables did not escape their scope
7991 skolemEscapeCheck val'
8092 -- Check rows do not contain duplicate labels
8193 checkDuplicateLabels val'
82− return (ident, (val', varIfUnknown ty))
94+ return (ident, (foldr (Abs . Left . fst) val' unsolved, generalized))
8395 where
96+ -- | Generalize type vars using forall and add inferred constraints
97+ generalize unsolved = varIfUnknown . constrain unsolved
98+ -- | Add any unsolved constraints
99+ constrain [] = id
100+ constrain cs = ConstrainedType (map snd cs)
84101 -- Apply the substitution that was returned from runUnify to both types and (type-annotated) values
85− tidyUp (ts, sub) = map (\(i, (val, ty)) -> (i, (overTypes (substituteType sub) val, substituteType sub ty))) ts
102+ tidyUp (ts, sub) = map (\(b, (i, (val, ty))) -> (b, (i, (overTypes (substituteType sub) val, substituteType sub ty)))) ts
86103 -- Replace all the wildcards types with their inferred types
87104 replace sub (ErrorMessage hints (WildcardInferredType ty)) = ErrorMessage hints . WildcardInferredType $ substituteType sub ty
88− replace sub (ErrorMessage hints (MissingTypeDeclaration name ty)) = ErrorMessage hints $ MissingTypeDeclaration name (varIfUnknown (substituteType sub ty))
89105 replace _ em = em
90106
91107type TypeData = M.Map (ModuleName, Ident) (Type, NameKind, NameVisibility)
@@ -138,16 +154,14 @@ checkTypedBindingGroupElement mn (ident, (val', ty, checkType)) dict = do
138154
139155typeForBindingGroupElement ::
140156 (MonadSupply m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
141− Bool ->
142157 (Ident, Expr) ->
143158 TypeData ->
144159 UntypedData ->
145160 m (Ident, (Expr, Type))
146−typeForBindingGroupElement warn (ident, val) dict untypedDict = do
161+typeForBindingGroupElement (ident, val) dict untypedDict = do
147162 -- Infer the type with the new names in scope
148163 TypedValue _ val' ty <- bindNames dict $ infer val
149164 unifyTypes ty $ fromMaybe (internalError "name not found in dictionary") (lookup ident untypedDict)
150− when warn . tell . errorMessage $ MissingTypeDeclaration ident ty
151165 return (ident, (TypedValue True val' ty, ty))
152166
153167-- | Check if a value contains a type annotation
@@ -165,20 +179,7 @@ overTypes f = let (_, f', _) = everywhereOnValues id g id in f'
165179 g (TypedValue checkTy val t) = TypedValue checkTy val (f t)
166180 g (TypeClassDictionary (nm, tys) sco) = TypeClassDictionary (nm, map f tys) sco
167181 g other = other
168−
169−-- | Replace type class dictionary placeholders with inferred type class dictionaries
170−replaceTypeClassDictionaries ::
171− (MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
172− ModuleName ->
173− Expr ->
174− m Expr
175−replaceTypeClassDictionaries mn =
176− let (_, f, _) = everywhereOnValuesTopDownM return go return
177− in f
178− where
179− go (TypeClassDictionary constraint dicts) = entails mn dicts constraint
180− go other = return other
181−
182+
182183-- | Check the kind of a type, failing if it is not of kind *.
183184checkTypeKind ::
184185 (MonadState CheckState m, MonadError MultipleErrors m) =>
@@ -329,7 +330,7 @@ inferLetBinding seen (BindingGroupDeclaration ds : rest) ret j = do
329330 Just moduleName <- checkCurrentModule <$> get
330331 (untyped, typed, dict, untypedDict) <- typeDictionaryForBindingGroup moduleName (map (\(i, _, v) -> (i, v)) ds)
331332 ds1' <- parU typed $ \e -> checkTypedBindingGroupElement moduleName e dict
332− ds2' <- forM untyped $ \e -> typeForBindingGroupElement False e dict untypedDict
333+ ds2' <- forM untyped $ \e -> typeForBindingGroupElement e dict untypedDict
333334 let ds' = [(ident, Private, val') | (ident, (val', _)) <- ds1' ++ ds2']
334335 bindNames dict $ do
335336 makeBindingGroupVisible
src/Language/PureScript/TypeChecker/Unify.hs+1
@@ -23,6 +23,7 @@ module Language.PureScript.TypeChecker.Unify (
2323 freshType,
2424 solveType,
2525 substituteType,
26+ unknownsInType,
2627 unifyTypes,
2728 unifyRows,
2829 unifiesWith,