git.iko.soy/rowtype-yoga/purescript-native
on golang help sign in
Merge pull request #1601 from purescript/tc-refactor
1ae09f0Phil Freeman
psci/PSCi.hs+7−5
compare with golang
unifiedsplit
@@ -33,12 +33,11 @@ import Control.Arrow (first)
33import Control.Monad
33import Control.Monad
34import Control.Monad.Error.Class (MonadError(..))
34import Control.Monad.Error.Class (MonadError(..))
35import Control.Monad.Trans.Class
35import Control.Monad.Trans.Class
36−import Control.Monad.Trans.Except (runExceptT)
36+import Control.Monad.Trans.Except (ExceptT(), runExceptT)
37import Control.Monad.Trans.Maybe (MaybeT(..), runMaybeT)
37import Control.Monad.Trans.Maybe (MaybeT(..), runMaybeT)
38import Control.Monad.Trans.State.Strict
38import Control.Monad.Trans.State.Strict
39import Control.Monad.IO.Class (liftIO)
39import Control.Monad.IO.Class (liftIO)
40−import Control.Monad.Writer.Strict (runWriter)
40+import Control.Monad.Writer.Strict (Writer(), runWriter)
41−import qualified Control.Monad.Trans.State.Lazy as L
42
41
43import Options.Applicative as Opts
42import Options.Applicative as Opts
44
43
@@ -422,8 +421,11 @@ handleKindOf typ = do
422 Right env' ->
421 Right env' ->
423 case M.lookup (P.Qualified (Just mName) $ P.ProperName "IT") (P.typeSynonyms env') of
422 case M.lookup (P.Qualified (Just mName) $ P.ProperName "IT") (P.typeSynonyms env') of
424 Just (_, typ') -> do
423 Just (_, typ') -> do
425− let chk = P.CheckState env' 0 0 (Just mName)
424+ let chk = (P.emptyCheckState env') { P.checkCurrentModule = Just mName }
425+ k = check (P.kindOf typ') chk
426+
427+ check :: StateT P.CheckState (ExceptT P.MultipleErrors (Writer P.MultipleErrors)) a -> P.CheckState -> Either P.MultipleErrors (a, P.CheckState)
426− k = fst . runWriter . runExceptT $ L.runStateT (P.unCheck (P.kindOf typ')) chk
428+ check sew cs = fst . runWriter . runExceptT . runStateT sew $ cs
427 case k of
429 case k of
428 Left errStack -> PSCI . outputStrLn . P.prettyPrintMultipleErrors False $ errStack
430 Left errStack -> PSCI . outputStrLn . P.prettyPrintMultipleErrors False $ errStack
429 Right (kind, _) -> PSCI . outputStrLn . P.prettyPrintKind $ kind
431 Right (kind, _) -> PSCI . outputStrLn . P.prettyPrintKind $ kind
purescript.cabal−1
@@ -174,7 +174,6 @@ library
174 Language.PureScript.Publish.BoxesHelpers
174 Language.PureScript.Publish.BoxesHelpers
175
175
176 Control.Monad.Logger
176 Control.Monad.Logger
177− Control.Monad.Unify
178 Control.Monad.Supply
177 Control.Monad.Supply
179 Control.Monad.Supply.Class
178 Control.Monad.Supply.Class
180
179
src/Control/Monad/Unify.hsdeleted−160
@@ -1,160 +0,0 @@
1−-----------------------------------------------------------------------------
2−--
3−-- Module : Control.Monad.Unify
4−-- Copyright : (c) Phil Freeman 2013
5−-- License : MIT
6−--
7−-- Maintainer : Phil Freeman <paf31@cantab.net>
8−-- Stability : experimental
9−-- Portability :
10−--
11−-- |
12−--
13−--
14−-----------------------------------------------------------------------------
15−
16−{-# LANGUAGE GeneralizedNewtypeDeriving #-}
17−{-# LANGUAGE FlexibleInstances #-}
18−{-# LANGUAGE FlexibleContexts #-}
19−{-# LANGUAGE DeriveDataTypeable #-}
20−{-# LANGUAGE MultiParamTypeClasses #-}
21−{-# LANGUAGE FunctionalDependencies #-}
22−{-# LANGUAGE UndecidableInstances #-}
23−
24−module Control.Monad.Unify where
25−
26−import Data.Monoid
27−
28−import Control.Applicative
29−import Control.Monad.State
30−import Control.Monad.Error.Class (MonadError(..))
31−import Control.Monad.Writer.Class (MonadWriter(..))
32−
33−import Data.HashMap.Strict as M
34−
35−-- |
36−-- Untyped unification variables
37−--
38−type Unknown = Int
39−
40−-- |
41−-- A type which can contain unification variables
42−--
43−class Partial t where
44− unknown :: Unknown -> t
45− isUnknown :: t -> Maybe Unknown
46− unknowns :: t -> [Unknown]
47− ($?) :: Substitution t -> t -> t
48−
49−-- |
50−-- Identifies types which support unification
51−--
52−class (Partial t) => Unifiable m t | t -> m where
53− (=?=) :: t -> t -> UnifyT t m ()
54−
55−-- |
56−-- A substitution maintains a mapping from unification variables to their values
57−--
58−data Substitution t = Substitution { runSubstitution :: M.HashMap Int t }
59−
60−instance (Partial t) => Monoid (Substitution t) where
61− mempty = Substitution M.empty
62− s1 `mappend` s2 = Substitution $
63− M.map (s2 $?) (runSubstitution s1) `M.union`
64− M.map (s1 $?) (runSubstitution s2)
65−
66−-- |
67−-- State required for type checking
68−--
69−data UnifyState t = UnifyState {
70− -- |
71− -- The next fresh unification variable
72− --
73− unifyNextVar :: Int
74− -- |
75− -- The current substitution
76− --
77− , unifyCurrentSubstitution :: Substitution t
78− }
79−
80−-- |
81−-- An empty @UnifyState@
82−--
83−defaultUnifyState :: (Partial t) => UnifyState t
84−defaultUnifyState = UnifyState 0 mempty
85−
86−-- |
87−-- A class for errors which support unification errors
88−--
89−class UnificationError t e where
90− occursCheckFailed :: t -> e
91−
92−-- |
93−-- The type checking monad, which provides the state of the type checker, and error reporting capabilities
94−--
95−newtype UnifyT t m a = UnifyT { unUnify :: StateT (UnifyState t) m a }
96− deriving (Functor, Monad, Applicative, Alternative, MonadPlus, MonadWriter w)
97−
98−instance (MonadState s m) => MonadState s (UnifyT t m) where
99− get = UnifyT . lift $ get
100− put = UnifyT . lift . put
101−
102−instance (MonadError e m) => MonadError e (UnifyT t m) where
103− throwError = UnifyT . throwError
104− catchError e f = UnifyT $ catchError (unUnify e) (unUnify . f)
105−
106−-- |
107−-- Run a computation in the Unify monad, failing with an error, or succeeding with a return value and the new next unification variable
108−--
109−runUnify :: UnifyState t -> UnifyT t m a -> m (a, UnifyState t)
110−runUnify s = flip runStateT s . unUnify
111−
112−-- |
113−-- Substitute a single unification variable
114−--
115−substituteOne :: (Partial t) => Unknown -> t -> Substitution t
116−substituteOne u t = Substitution $ M.singleton u t
117−
118−-- |
119−-- Replace a unification variable with the specified value in the current substitution
120−--
121−(=:=) :: (UnificationError t e, Monad m, MonadError e m, Unifiable m t) => Unknown -> t -> UnifyT t m ()
122−(=:=) u t' = do
123− st <- UnifyT get
124− let sub = unifyCurrentSubstitution st
125− let t = sub $? t'
126− occursCheck u t
127− let current = sub $? unknown u
128− case isUnknown current of
129− Just u1 | u1 == u -> return ()
130− _ -> current =?= t
131− UnifyT $ modify $ \s -> s { unifyCurrentSubstitution = substituteOne u t <> unifyCurrentSubstitution s }
132−
133−-- |
134−-- Perform the occurs check, to make sure a unification variable does not occur inside a value
135−--
136−occursCheck :: (UnificationError t e, Monad m, MonadError e m, Partial t) => Unknown -> t -> UnifyT t m ()
137−occursCheck u t =
138− case isUnknown t of
139− Nothing -> when (u `elem` unknowns t) $ UnifyT . lift . throwError $ occursCheckFailed t
140− _ -> return ()
141−
142−-- |
143−-- Generate a fresh untyped unification variable
144−--
145−fresh' :: (Monad m) => UnifyT t m Unknown
146−fresh' = do
147− st <- UnifyT get
148− UnifyT $ modify $ \s -> s { unifyNextVar = succ (unifyNextVar s) }
149− return $ unifyNextVar st
150−
151−-- |
152−-- Generate a fresh unification variable at a specific type
153−--
154−fresh :: (Monad m, Partial t) => UnifyT t m t
155−fresh = do
156− u <- fresh'
157− return $ unknown u
158−
159−
160−
src/Language/PureScript/Errors.hs+2−15
@@ -29,7 +29,6 @@ import Data.Foldable (fold)
29import qualified Data.Map as M
29import qualified Data.Map as M
30
30
31import Control.Monad
31import Control.Monad
32−import Control.Monad.Unify
33import Control.Monad.Writer
32import Control.Monad.Writer
34import Control.Monad.Error.Class (MonadError(..))
33import Control.Monad.Error.Class (MonadError(..))
35import Control.Monad.Trans.State.Lazy
34import Control.Monad.Trans.State.Lazy
@@ -177,12 +176,6 @@ data HintCategory
177
176
178data ErrorMessage = ErrorMessage [ErrorMessageHint] SimpleErrorMessage deriving (Show)
177data ErrorMessage = ErrorMessage [ErrorMessageHint] SimpleErrorMessage deriving (Show)
179
178
180−instance UnificationError Type ErrorMessage where
181− occursCheckFailed t = ErrorMessage [] $ InfiniteType t
182−
183−instance UnificationError Kind ErrorMessage where
184− occursCheckFailed k = ErrorMessage [] $ InfiniteKind k
185−
186-- |
179-- |
187-- Get the error code for a particular error type
180-- Get the error code for a particular error type
188--
181--
@@ -285,12 +278,6 @@ errorCode em = case unwrapErrorMessage em of
285newtype MultipleErrors = MultipleErrors
278newtype MultipleErrors = MultipleErrors
286 { runMultipleErrors :: [ErrorMessage] } deriving (Show, Monoid)
279 { runMultipleErrors :: [ErrorMessage] } deriving (Show, Monoid)
287
280
288−instance UnificationError Type MultipleErrors where
289− occursCheckFailed t = MultipleErrors [occursCheckFailed t]
290−
291−instance UnificationError Kind MultipleErrors where
292− occursCheckFailed k = MultipleErrors [occursCheckFailed k]
293−
294-- | Check whether a collection of errors is empty or not.
281-- | Check whether a collection of errors is empty or not.
295nonEmpty :: MultipleErrors -> Bool
282nonEmpty :: MultipleErrors -> Bool
296nonEmpty = not . null . runMultipleErrors
283nonEmpty = not . null . runMultipleErrors
@@ -320,7 +307,7 @@ addHint hint = onErrorMessages $ \(ErrorMessage hints se) -> ErrorMessage (hint
320data LabelType = TypeLabel | SkolemLabel String deriving (Show, Read, Eq, Ord)
307data LabelType = TypeLabel | SkolemLabel String deriving (Show, Read, Eq, Ord)
321
308
322-- | A map from rigid type variable name/unknown variable pairs to new variables.
309-- | A map from rigid type variable name/unknown variable pairs to new variables.
323−type UnknownMap = M.Map (LabelType, Unknown) Unknown
310+type UnknownMap = M.Map (LabelType, Int) Int
324
311
325-- | How critical the issue is
312-- | How critical the issue is
326data Level = Error | Warning deriving Show
313data Level = Error | Warning deriving Show
@@ -334,7 +321,7 @@ unwrapErrorMessage (ErrorMessage _ se) = se
334replaceUnknowns :: Type -> State UnknownMap Type
321replaceUnknowns :: Type -> State UnknownMap Type
335replaceUnknowns = everywhereOnTypesM replaceTypes
322replaceUnknowns = everywhereOnTypesM replaceTypes
336 where
323 where
337− lookupTable :: (LabelType, Unknown) -> UnknownMap -> (Unknown, UnknownMap)
324+ lookupTable :: (LabelType, Int) -> UnknownMap -> (Int, UnknownMap)
338 lookupTable x m = case M.lookup x m of
325 lookupTable x m = case M.lookup x m of
339 Nothing -> let i = length (filter (on (==) fst x) (M.keys m)) in (i, M.insert x i m)
326 Nothing -> let i = length (filter (on (==) fst x) (M.keys m)) in (i, M.insert x i m)
340 Just i -> (i, m)
327 Just i -> (i, m)
src/Language/PureScript/Kinds.hs+1−3
@@ -23,8 +23,6 @@ import Prelude.Compat
23import Data.Data
23import Data.Data
24import qualified Data.Aeson.TH as A
24import qualified Data.Aeson.TH as A
25
25
26−import Control.Monad.Unify (Unknown)
27−
28-- |
26-- |
29-- The data type of kinds
27-- The data type of kinds
30--
28--
@@ -32,7 +30,7 @@ data Kind
32 -- |
30 -- |
33 -- Unification variable of type Kind
31 -- Unification variable of type Kind
34 --
32 --
35− = KUnknown Unknown
33+ = KUnknown Int
36 -- |
34 -- |
37 -- The kind of types
35 -- The kind of types
38 --
36 --
src/Language/PureScript/TypeChecker.hs+95−29
@@ -13,7 +13,9 @@
13--
13--
14-----------------------------------------------------------------------------
14-----------------------------------------------------------------------------
15
15
16+{-# LANGUAGE ScopedTypeVariables #-}
16{-# LANGUAGE FlexibleInstances #-}
17{-# LANGUAGE FlexibleInstances #-}
18+{-# LANGUAGE FlexibleContexts #-}
17
19
18module Language.PureScript.TypeChecker (
20module Language.PureScript.TypeChecker (
19 module T,
21 module T,
@@ -34,8 +36,10 @@ import Data.Foldable (for_, traverse_)
34
36
35import qualified Data.Map as M
37import qualified Data.Map as M
36
38
37−import Control.Monad.State
39+import Control.Monad (when, unless, void, forM, forM_)
40+import Control.Monad.State.Class (MonadState(..), modify)
38import Control.Monad.Error.Class (MonadError(..))
41import Control.Monad.Error.Class (MonadError(..))
42+import Control.Monad.Writer.Class (MonadWriter(..))
39
43
40import Language.PureScript.Crash
44import Language.PureScript.Crash
41import Language.PureScript.Types
45import Language.PureScript.Types
@@ -46,15 +50,31 @@ import Language.PureScript.TypeClassDictionaries
46import Language.PureScript.Environment
50import Language.PureScript.Environment
47import Language.PureScript.Errors
51import Language.PureScript.Errors
48
52
49−addDataType :: ModuleName -> DataDeclType -> ProperName -> [(String, Maybe Kind)] -> [(ProperName, [Type])] -> Kind -> Check ()
53+addDataType ::
54+ (Functor m, Applicative m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
55+ ModuleName ->
56+ DataDeclType ->
57+ ProperName ->
58+ [(String, Maybe Kind)] ->
59+ [(ProperName, [Type])] ->
60+ Kind ->
61+ m ()
50addDataType moduleName dtype name args dctors ctorKind = do
62addDataType moduleName dtype name args dctors ctorKind = do
51 env <- getEnv
63 env <- getEnv
52 putEnv $ env { types = M.insert (Qualified (Just moduleName) name) (ctorKind, DataType args dctors) (types env) }
64 putEnv $ env { types = M.insert (Qualified (Just moduleName) name) (ctorKind, DataType args dctors) (types env) }
53− forM_ dctors $ \(dctor, tys) ->
65+ for_ dctors $ \(dctor, tys) ->
54 warnAndRethrow (addHint (ErrorInDataConstructor dctor)) $
66 warnAndRethrow (addHint (ErrorInDataConstructor dctor)) $
55 addDataConstructor moduleName dtype name (map fst args) dctor tys
67 addDataConstructor moduleName dtype name (map fst args) dctor tys
56
68
57−addDataConstructor :: ModuleName -> DataDeclType -> ProperName -> [String] -> ProperName -> [Type] -> Check ()
69+addDataConstructor ::
70+ (Functor m, Applicative m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
71+ ModuleName ->
72+ DataDeclType ->
73+ ProperName ->
74+ [String] ->
75+ ProperName ->
76+ [Type] ->
77+ m ()
58addDataConstructor moduleName dtype name args dctor tys = do
78addDataConstructor moduleName dtype name args dctor tys = do
59 env <- getEnv
79 env <- getEnv
60 traverse_ checkTypeSynonyms tys
80 traverse_ checkTypeSynonyms tys
@@ -64,26 +84,50 @@ addDataConstructor moduleName dtype name args dctor tys = do
64 let fields = [Ident ("value" ++ show n) | n <- [0..(length tys - 1)]]
84 let fields = [Ident ("value" ++ show n) | n <- [0..(length tys - 1)]]
65 putEnv $ env { dataConstructors = M.insert (Qualified (Just moduleName) dctor) (dtype, name, polyType, fields) (dataConstructors env) }
85 putEnv $ env { dataConstructors = M.insert (Qualified (Just moduleName) dctor) (dtype, name, polyType, fields) (dataConstructors env) }
66
86
67−addTypeSynonym :: ModuleName -> ProperName -> [(String, Maybe Kind)] -> Type -> Kind -> Check ()
87+addTypeSynonym ::
88+ (Functor m, Applicative m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
89+ ModuleName ->
90+ ProperName ->
91+ [(String, Maybe Kind)] ->
92+ Type ->
93+ Kind ->
94+ m ()
68addTypeSynonym moduleName name args ty kind = do
95addTypeSynonym moduleName name args ty kind = do
69 env <- getEnv
96 env <- getEnv
70 checkTypeSynonyms ty
97 checkTypeSynonyms ty
71 putEnv $ env { types = M.insert (Qualified (Just moduleName) name) (kind, TypeSynonym) (types env)
98 putEnv $ env { types = M.insert (Qualified (Just moduleName) name) (kind, TypeSynonym) (types env)
72 , typeSynonyms = M.insert (Qualified (Just moduleName) name) (args, ty) (typeSynonyms env) }
99 , typeSynonyms = M.insert (Qualified (Just moduleName) name) (args, ty) (typeSynonyms env) }
73
100
74−valueIsNotDefined :: ModuleName -> Ident -> Check ()
101+valueIsNotDefined ::
102+ (Functor m, Applicative m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
103+ ModuleName ->
104+ Ident ->
105+ m ()
75valueIsNotDefined moduleName name = do
106valueIsNotDefined moduleName name = do
76 env <- getEnv
107 env <- getEnv
77 case M.lookup (moduleName, name) (names env) of
108 case M.lookup (moduleName, name) (names env) of
78 Just _ -> throwError . errorMessage $ RedefinedIdent name
109 Just _ -> throwError . errorMessage $ RedefinedIdent name
79 Nothing -> return ()
110 Nothing -> return ()
80
111
112+addValue ::
113+ (Functor m, Applicative m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
81−addValue :: ModuleName -> Ident -> Type -> NameKind -> Check ()
114+ ModuleName ->
115+ Ident ->
116+ Type ->
117+ NameKind ->
118+ m ()
82addValue moduleName name ty nameKind = do
119addValue moduleName name ty nameKind = do
83 env <- getEnv
120 env <- getEnv
84 putEnv (env { names = M.insert (moduleName, name) (ty, nameKind, Defined) (names env) })
121 putEnv (env { names = M.insert (moduleName, name) (ty, nameKind, Defined) (names env) })
85
122
86−addTypeClass :: ModuleName -> ProperName -> [(String, Maybe Kind)] -> [Constraint] -> [Declaration] -> Check ()
123+addTypeClass ::
124+ (Functor m, Applicative m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
125+ ModuleName ->
126+ ProperName ->
127+ [(String, Maybe Kind)] ->
128+ [Constraint] ->
129+ [Declaration] ->
130+ m ()
87addTypeClass moduleName pn args implies ds =
131addTypeClass moduleName pn args implies ds =
88 let members = map toPair ds in
132 let members = map toPair ds in
89 modify $ \st -> st { checkEnv = (checkEnv st) { typeClasses = M.insert (Qualified (Just moduleName) pn) (args, members, implies) (typeClasses . checkEnv $ st) } }
133 modify $ \st -> st { checkEnv = (checkEnv st) { typeClasses = M.insert (Qualified (Just moduleName) pn) (args, members, implies) (typeClasses . checkEnv $ st) } }
@@ -92,19 +136,30 @@ addTypeClass moduleName pn args implies ds =
92 toPair (PositionedDeclaration _ _ d) = toPair d
136 toPair (PositionedDeclaration _ _ d) = toPair d
93 toPair _ = internalError "Invalid declaration in TypeClassDeclaration"
137 toPair _ = internalError "Invalid declaration in TypeClassDeclaration"
94
138
139+addTypeClassDictionaries ::
140+ (Functor m, Applicative m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
141+ Maybe ModuleName ->
95−addTypeClassDictionaries :: Maybe ModuleName -> M.Map (Qualified ProperName) (M.Map (Qualified Ident) TypeClassDictionaryInScope) -> Check ()
142+ M.Map (Qualified ProperName) (M.Map (Qualified Ident) TypeClassDictionaryInScope) ->
143+ m ()
96addTypeClassDictionaries mn entries =
144addTypeClassDictionaries mn entries =
97 modify $ \st -> st { checkEnv = (checkEnv st) { typeClassDictionaries = insertState st } }
145 modify $ \st -> st { checkEnv = (checkEnv st) { typeClassDictionaries = insertState st } }
98 where insertState st = M.insertWith (M.unionWith M.union) mn entries (typeClassDictionaries . checkEnv $ st)
146 where insertState st = M.insertWith (M.unionWith M.union) mn entries (typeClassDictionaries . checkEnv $ st)
99
147
100−checkDuplicateTypeArguments :: [String] -> Check ()
148+checkDuplicateTypeArguments ::
149+ (Functor m, Applicative m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
150+ [String] ->
151+ m ()
101checkDuplicateTypeArguments args = for_ firstDup $ \dup ->
152checkDuplicateTypeArguments args = for_ firstDup $ \dup ->
102 throwError . errorMessage $ DuplicateTypeArgument dup
153 throwError . errorMessage $ DuplicateTypeArgument dup
103 where
154 where
104 firstDup :: Maybe String
155 firstDup :: Maybe String
105 firstDup = listToMaybe $ args \\ nub args
156 firstDup = listToMaybe $ args \\ nub args
106
157
107−checkTypeClassInstance :: ModuleName -> Type -> Check ()
158+checkTypeClassInstance ::
159+ (Functor m, Applicative m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
160+ ModuleName ->
161+ Type ->
162+ m ()
108checkTypeClassInstance _ (TypeVar _) = return ()
163checkTypeClassInstance _ (TypeVar _) = return ()
109checkTypeClassInstance _ (TypeConstructor ctor) = do
164checkTypeClassInstance _ (TypeConstructor ctor) = do
110 env <- getEnv
165 env <- getEnv
@@ -116,7 +171,10 @@ checkTypeClassInstance _ ty = throwError . errorMessage $ InvalidInstanceHead ty
116-- |
171-- |
117-- Check that type synonyms are fully-applied in a type
172-- Check that type synonyms are fully-applied in a type
118--
173--
119−checkTypeSynonyms :: Type -> Check ()
174+checkTypeSynonyms ::
175+ (Functor m, Applicative m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
176+ Type ->
177+ m ()
120checkTypeSynonyms = void . replaceAllTypeSynonyms
178checkTypeSynonyms = void . replaceAllTypeSynonyms
121
179
122-- |
180-- |
@@ -132,10 +190,15 @@ checkTypeSynonyms = void . replaceAllTypeSynonyms
132--
190--
133-- * Process module imports
191-- * Process module imports
134--
192--
135−typeCheckAll :: ModuleName -> [DeclarationRef] -> [Declaration] -> Check [Declaration]
193+typeCheckAll :: forall m.
194+ (Functor m, Applicative m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
195+ ModuleName ->
196+ [DeclarationRef] ->
197+ [Declaration] ->
198+ m [Declaration]
136typeCheckAll moduleName _ ds = traverse go ds <* traverse_ checkOrphanFixities ds
199typeCheckAll moduleName _ ds = traverse go ds <* traverse_ checkOrphanFixities ds
137 where
200 where
138− go :: Declaration -> Check Declaration
201+ go :: Declaration -> m Declaration
139 go (DataDeclaration dtype name args dctors) = do
202 go (DataDeclaration dtype name args dctors) = do
140 warnAndRethrow (addHint (ErrorInTypeConstructor name)) $ do
203 warnAndRethrow (addHint (ErrorInTypeConstructor name)) $ do
141 when (dtype == Newtype) $ checkNewtype dctors
204 when (dtype == Newtype) $ checkNewtype dctors
@@ -145,7 +208,7 @@ typeCheckAll moduleName _ ds = traverse go ds <* traverse_ checkOrphanFixities d
145 addDataType moduleName dtype name args' dctors ctorKind
208 addDataType moduleName dtype name args' dctors ctorKind
146 return $ DataDeclaration dtype name args dctors
209 return $ DataDeclaration dtype name args dctors
147 where
210 where
148− checkNewtype :: [(ProperName, [Type])] -> Check ()
211+ checkNewtype :: [(ProperName, [Type])] -> m ()
149 checkNewtype [(_, [_])] = return ()
212 checkNewtype [(_, [_])] = return ()
150 checkNewtype [(_, _)] = throwError . errorMessage $ InvalidNewtype name
213 checkNewtype [(_, _)] = throwError . errorMessage $ InvalidNewtype name
151 checkNewtype _ = throwError . errorMessage $ InvalidNewtype name
214 checkNewtype _ = throwError . errorMessage $ InvalidNewtype name
@@ -154,11 +217,11 @@ typeCheckAll moduleName _ ds = traverse go ds <* traverse_ checkOrphanFixities d
154 let syns = mapMaybe toTypeSynonym tys
217 let syns = mapMaybe toTypeSynonym tys
155 let dataDecls = mapMaybe toDataDecl tys
218 let dataDecls = mapMaybe toDataDecl tys
156 (syn_ks, data_ks) <- kindsOfAll moduleName syns (map (\(_, name, args, dctors) -> (name, args, concatMap snd dctors)) dataDecls)
219 (syn_ks, data_ks) <- kindsOfAll moduleName syns (map (\(_, name, args, dctors) -> (name, args, concatMap snd dctors)) dataDecls)
157− forM_ (zip dataDecls data_ks) $ \((dtype, name, args, dctors), ctorKind) -> do
220+ for_ (zip dataDecls data_ks) $ \((dtype, name, args, dctors), ctorKind) -> do
158 checkDuplicateTypeArguments $ map fst args
221 checkDuplicateTypeArguments $ map fst args
159 let args' = args `withKinds` ctorKind
222 let args' = args `withKinds` ctorKind
160 addDataType moduleName dtype name args' dctors ctorKind
223 addDataType moduleName dtype name args' dctors ctorKind
161− forM_ (zip syns syn_ks) $ \((name, args, ty), kind) -> do
224+ for_ (zip syns syn_ks) $ \((name, args, ty), kind) -> do
162 checkDuplicateTypeArguments $ map fst args
225 checkDuplicateTypeArguments $ map fst args
163 let args' = args `withKinds` kind
226 let args' = args `withKinds` kind
164 addTypeSynonym moduleName name args' ty kind
227 addTypeSynonym moduleName name args' ty kind
@@ -187,7 +250,7 @@ typeCheckAll moduleName _ ds = traverse go ds <* traverse_ checkOrphanFixities d
187 go (ValueDeclaration{}) = internalError "Binders were not desugared"
250 go (ValueDeclaration{}) = internalError "Binders were not desugared"
188 go (BindingGroupDeclaration vals) =
251 go (BindingGroupDeclaration vals) =
189 warnAndRethrow (addHint (ErrorInBindingGroup (map (\(ident, _, _) -> ident) vals))) $ do
252 warnAndRethrow (addHint (ErrorInBindingGroup (map (\(ident, _, _) -> ident) vals))) $ do
190− forM_ (map (\(ident, _, _) -> ident) vals) $ \name ->
253+ for_ (map (\(ident, _, _) -> ident) vals) $ \name ->
191 valueIsNotDefined moduleName name
254 valueIsNotDefined moduleName name
192 tys <- typesOf moduleName $ map (\(ident, _, ty) -> (ident, ty)) vals
255 tys <- typesOf moduleName $ map (\(ident, _, ty) -> (ident, ty)) vals
193 vals' <- forM [ (name, val, nameKind, ty)
256 vals' <- forM [ (name, val, nameKind, ty)
@@ -227,7 +290,7 @@ typeCheckAll moduleName _ ds = traverse go ds <* traverse_ checkOrphanFixities d
227 go (PositionedDeclaration pos com d) =
290 go (PositionedDeclaration pos com d) =
228 warnAndRethrowWithPosition pos $ PositionedDeclaration pos com <$> go d
291 warnAndRethrowWithPosition pos $ PositionedDeclaration pos com <$> go d
229
292
230− checkOrphanFixities :: Declaration -> Check ()
293+ checkOrphanFixities :: Declaration -> m ()
231 checkOrphanFixities (FixityDeclaration _ name) = do
294 checkOrphanFixities (FixityDeclaration _ name) = do
232 env <- getEnv
295 env <- getEnv
233 guardWith (errorMessage (OrphanFixityDeclaration name)) $ M.member (moduleName, Op name) $ names env
296 guardWith (errorMessage (OrphanFixityDeclaration name)) $ M.member (moduleName, Op name) $ names env
@@ -235,7 +298,7 @@ typeCheckAll moduleName _ ds = traverse go ds <* traverse_ checkOrphanFixities d
235 warnAndRethrowWithPosition pos $ checkOrphanFixities d
298 warnAndRethrowWithPosition pos $ checkOrphanFixities d
236 checkOrphanFixities _ = return ()
299 checkOrphanFixities _ = return ()
237
300
238− checkInstanceMembers :: [Declaration] -> Check [Declaration]
301+ checkInstanceMembers :: [Declaration] -> m [Declaration]
239 checkInstanceMembers instDecls = do
302 checkInstanceMembers instDecls = do
240 let idents = sort . map head . group . map memberName $ instDecls
303 let idents = sort . map head . group . map memberName $ instDecls
241 for_ (firstDuplicate idents) $ \ident ->
304 for_ (firstDuplicate idents) $ \ident ->
@@ -253,7 +316,7 @@ typeCheckAll moduleName _ ds = traverse go ds <* traverse_ checkOrphanFixities d
253 | otherwise = firstDuplicate xs
316 | otherwise = firstDuplicate xs
254 firstDuplicate _ = Nothing
317 firstDuplicate _ = Nothing
255
318
256− checkOrphanInstance :: Ident -> Qualified ProperName -> [Type] -> Check ()
319+ checkOrphanInstance :: Ident -> Qualified ProperName -> [Type] -> m ()
257 checkOrphanInstance dictName className@(Qualified (Just mn') _) tys'
320 checkOrphanInstance dictName className@(Qualified (Just mn') _) tys'
258 | moduleName == mn' || any checkType tys' = return ()
321 | moduleName == mn' || any checkType tys' = return ()
259 | otherwise = throwError . errorMessage $ OrphanInstance dictName className tys'
322 | otherwise = throwError . errorMessage $ OrphanInstance dictName className tys'
@@ -280,19 +343,22 @@ typeCheckAll moduleName _ ds = traverse go ds <* traverse_ checkOrphanFixities d
280-- Type check an entire module and ensure all types and classes defined within the module that are
343-- Type check an entire module and ensure all types and classes defined within the module that are
281-- required by exported members are also exported.
344-- required by exported members are also exported.
282--
345--
283−typeCheckModule :: Module -> Check Module
346+typeCheckModule :: forall m.
347+ (Functor m, Applicative m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
348+ Module ->
349+ m Module
284typeCheckModule (Module _ _ _ _ Nothing) = internalError "exports should have been elaborated"
350typeCheckModule (Module _ _ _ _ Nothing) = internalError "exports should have been elaborated"
285typeCheckModule (Module ss coms mn decls (Just exps)) = warnAndRethrow (addHint (ErrorInModule mn)) $ do
351typeCheckModule (Module ss coms mn decls (Just exps)) = warnAndRethrow (addHint (ErrorInModule mn)) $ do
286 modify (\s -> s { checkCurrentModule = Just mn })
352 modify (\s -> s { checkCurrentModule = Just mn })
287 decls' <- typeCheckAll mn exps decls
353 decls' <- typeCheckAll mn exps decls
288− forM_ exps $ \e -> do
354+ for_ exps $ \e -> do
289 checkTypesAreExported e
355 checkTypesAreExported e
290 checkClassMembersAreExported e
356 checkClassMembersAreExported e
291 checkClassesAreExported e
357 checkClassesAreExported e
292 return $ Module ss coms mn decls' (Just exps)
358 return $ Module ss coms mn decls' (Just exps)
293 where
359 where
294
360
295− checkMemberExport :: (Type -> [DeclarationRef]) -> DeclarationRef -> Check ()
361+ checkMemberExport :: (Type -> [DeclarationRef]) -> DeclarationRef -> m ()
296 checkMemberExport extract dr@(TypeRef name dctors) = do
362 checkMemberExport extract dr@(TypeRef name dctors) = do
297 env <- getEnv
363 env <- getEnv
298 case M.lookup (Qualified (Just mn) name) (typeSynonyms env) of
364 case M.lookup (Qualified (Just mn) name) (typeSynonyms env) of
@@ -300,7 +366,7 @@ typeCheckModule (Module ss coms mn decls (Just exps)) = warnAndRethrow (addHint
300 Just (_, ty) -> checkExport dr extract ty
366 Just (_, ty) -> checkExport dr extract ty
301 case dctors of
367 case dctors of
302 Nothing -> return ()
368 Nothing -> return ()
303− Just dctors' -> forM_ dctors' $ \dctor ->
369+ Just dctors' -> for_ dctors' $ \dctor ->
304 case M.lookup (Qualified (Just mn) dctor) (dataConstructors env) of
370 case M.lookup (Qualified (Just mn) dctor) (dataConstructors env) of
305 Nothing -> return ()
371 Nothing -> return ()
306 Just (_, _, ty, _) -> checkExport dr extract ty
372 Just (_, _, ty, _) -> checkExport dr extract ty
@@ -310,7 +376,7 @@ typeCheckModule (Module ss coms mn decls (Just exps)) = warnAndRethrow (addHint
310 checkExport dr extract ty
376 checkExport dr extract ty
311 checkMemberExport _ _ = return ()
377 checkMemberExport _ _ = return ()
312
378
313− checkExport :: DeclarationRef -> (Type -> [DeclarationRef]) -> Type -> Check ()
379+ checkExport :: DeclarationRef -> (Type -> [DeclarationRef]) -> Type -> m ()
314 checkExport dr extract ty = case filter (not . exported) (extract ty) of
380 checkExport dr extract ty = case filter (not . exported) (extract ty) of
315 [] -> return ()
381 [] -> return ()
316 hidden -> throwError . errorMessage $ TransitiveExportError dr hidden
382 hidden -> throwError . errorMessage $ TransitiveExportError dr hidden
@@ -325,7 +391,7 @@ typeCheckModule (Module ss coms mn decls (Just exps)) = warnAndRethrow (addHint
325
391
326 -- Check that all the type constructors defined in the current module that appear in member types
392 -- Check that all the type constructors defined in the current module that appear in member types
327 -- have also been exported from the module
393 -- have also been exported from the module
328− checkTypesAreExported :: DeclarationRef -> Check ()
394+ checkTypesAreExported :: DeclarationRef -> m ()
329 checkTypesAreExported = checkMemberExport findTcons
395 checkTypesAreExported = checkMemberExport findTcons
330 where
396 where
331 findTcons :: Type -> [DeclarationRef]
397 findTcons :: Type -> [DeclarationRef]
@@ -336,7 +402,7 @@ typeCheckModule (Module ss coms mn decls (Just exps)) = warnAndRethrow (addHint
336
402
337 -- Check that all the classes defined in the current module that appear in member types have also
403 -- Check that all the classes defined in the current module that appear in member types have also
338 -- been exported from the module
404 -- been exported from the module
339− checkClassesAreExported :: DeclarationRef -> Check ()
405+ checkClassesAreExported :: DeclarationRef -> m ()
340 checkClassesAreExported = checkMemberExport findClasses
406 checkClassesAreExported = checkMemberExport findClasses
341 where
407 where
342 findClasses :: Type -> [DeclarationRef]
408 findClasses :: Type -> [DeclarationRef]
@@ -348,7 +414,7 @@ typeCheckModule (Module ss coms mn decls (Just exps)) = warnAndRethrow (addHint
348 extractCurrentModuleClass (Qualified (Just mn') name) | mn == mn' = Just name
414 extractCurrentModuleClass (Qualified (Just mn') name) | mn == mn' = Just name
349 extractCurrentModuleClass _ = Nothing
415 extractCurrentModuleClass _ = Nothing
350
416
351− checkClassMembersAreExported :: DeclarationRef -> Check ()
417+ checkClassMembersAreExported :: DeclarationRef -> m ()
352 checkClassMembersAreExported dr@(TypeClassRef name) = do
418 checkClassMembersAreExported dr@(TypeClassRef name) = do
353 let members = ValueRef `map` head (mapMaybe findClassMembers decls)
419 let members = ValueRef `map` head (mapMaybe findClassMembers decls)
354 let missingMembers = members \\ exps
420 let missingMembers = members \\ exps
src/Language/PureScript/TypeChecker/Entailment.hs+14−7
@@ -13,6 +13,9 @@
13--
13--
14-----------------------------------------------------------------------------
14-----------------------------------------------------------------------------
15
15
16+{-# LANGUAGE ScopedTypeVariables #-}
17+{-# LANGUAGE FlexibleContexts #-}
18+
16module Language.PureScript.TypeChecker.Entailment (
19module Language.PureScript.TypeChecker.Entailment (
17 entails
20 entails
18) where
21) where
@@ -28,13 +31,12 @@ import qualified Data.Map as M
28import Control.Arrow (Arrow(..))
31import Control.Arrow (Arrow(..))
29import Control.Monad.State
32import Control.Monad.State
30import Control.Monad.Error.Class (MonadError(..))
33import Control.Monad.Error.Class (MonadError(..))
31−import Control.Monad.Writer.Class (tell)
34+import Control.Monad.Writer.Class (MonadWriter(..))
32
35
33import Language.PureScript.Crash
36import Language.PureScript.Crash
34import Language.PureScript.AST
37import Language.PureScript.AST
35import Language.PureScript.Errors
38import Language.PureScript.Errors
36import Language.PureScript.Names
39import Language.PureScript.Names
37−import Language.PureScript.TypeChecker.Monad
38import Language.PureScript.TypeChecker.Unify
40import Language.PureScript.TypeChecker.Unify
39import Language.PureScript.TypeClassDictionaries
41import Language.PureScript.TypeClassDictionaries
40import Language.PureScript.Types
42import Language.PureScript.Types
@@ -44,7 +46,12 @@ import qualified Language.PureScript.Constants as C
44-- Check that the current set of type class dictionaries entail the specified type class goal, and, if so,
46-- Check that the current set of type class dictionaries entail the specified type class goal, and, if so,
45-- return a type class dictionary reference.
47-- return a type class dictionary reference.
46--
48--
49+entails :: forall m.
50+ (Functor m, Applicative m, MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
51+ ModuleName ->
47−entails :: ModuleName -> M.Map (Maybe ModuleName) (M.Map (Qualified ProperName) (M.Map (Qualified Ident) TypeClassDictionaryInScope)) -> Constraint -> Check Expr
52+ M.Map (Maybe ModuleName) (M.Map (Qualified ProperName) (M.Map (Qualified Ident) TypeClassDictionaryInScope)) ->
53+ Constraint ->
54+ m Expr
48entails moduleName context = solve
55entails moduleName context = solve
49 where
56 where
50 forClassName :: Qualified ProperName -> [Type] -> [TypeClassDictionaryInScope]
57 forClassName :: Qualified ProperName -> [Type] -> [TypeClassDictionaryInScope]
@@ -60,12 +67,12 @@ entails moduleName context = solve
60 findDicts :: Qualified ProperName -> Maybe ModuleName -> [TypeClassDictionaryInScope]
67 findDicts :: Qualified ProperName -> Maybe ModuleName -> [TypeClassDictionaryInScope]
61 findDicts cn = maybe [] M.elems . (>>= M.lookup cn) . flip M.lookup context
68 findDicts cn = maybe [] M.elems . (>>= M.lookup cn) . flip M.lookup context
62
69
63− solve :: Constraint -> Check Expr
70+ solve :: Constraint -> m Expr
64 solve (className, tys) = do
71 solve (className, tys) = do
65 dict <- go 0 className tys
72 dict <- go 0 className tys
66 return $ dictionaryValueToValue dict
73 return $ dictionaryValueToValue dict
67 where
74 where
68− go :: Int -> Qualified ProperName -> [Type] -> Check DictionaryValue
75+ go :: Int -> Qualified ProperName -> [Type] -> m DictionaryValue
69 go work className' tys' | work > 1000 = throwError . errorMessage $ PossiblyInfiniteInstance className' tys'
76 go work className' tys' | work > 1000 = throwError . errorMessage $ PossiblyInfiniteInstance className' tys'
70 go work className' tys' = do
77 go work className' tys' = do
71 let instances = do
78 let instances = do
@@ -81,7 +88,7 @@ entails moduleName context = solve
81 (tcdPath tcd)
88 (tcdPath tcd)
82 where
89 where
83
90
84− unique :: [(a, TypeClassDictionaryInScope)] -> Check (a, TypeClassDictionaryInScope)
91+ unique :: [(a, TypeClassDictionaryInScope)] -> m (a, TypeClassDictionaryInScope)
85 unique [] = throwError . errorMessage $ NoInstanceFound className' tys'
92 unique [] = throwError . errorMessage $ NoInstanceFound className' tys'
86 unique [a] = return a
93 unique [a] = return a
87 unique tcds | pairwise overlapping (map snd tcds) = do
94 unique tcds | pairwise overlapping (map snd tcds) = do
@@ -104,7 +111,7 @@ entails moduleName context = solve
104 -- Create dictionaries for subgoals which still need to be solved by calling go recursively
111 -- Create dictionaries for subgoals which still need to be solved by calling go recursively
105 -- E.g. the goal (Show a, Show b) => Show (Either a b) can be satisfied if the current type
112 -- E.g. the goal (Show a, Show b) => Show (Either a b) can be satisfied if the current type
106 -- unifies with Either a b, and we can satisfy the subgoals Show a and Show b recursively.
113 -- unifies with Either a b, and we can satisfy the subgoals Show a and Show b recursively.
107− solveSubgoals :: [(String, Type)] -> Maybe [Constraint] -> Check (Maybe [DictionaryValue])
114+ solveSubgoals :: [(String, Type)] -> Maybe [Constraint] -> m (Maybe [DictionaryValue])
108 solveSubgoals _ Nothing = return Nothing
115 solveSubgoals _ Nothing = return Nothing
109 solveSubgoals subst (Just subgoals) = do
116 solveSubgoals subst (Just subgoals) = do
110 dict <- traverse (uncurry (go (work + 1)) . second (map (replaceAllTypeVars subst))) subgoals
117 dict <- traverse (uncurry (go (work + 1)) . second (map (replaceAllTypeVars subst))) subgoals
src/Language/PureScript/TypeChecker/Kinds.hs+125−90
@@ -13,10 +13,12 @@
13--
13--
14-----------------------------------------------------------------------------
14-----------------------------------------------------------------------------
15
15
16−{-# OPTIONS_GHC -fno-warn-orphans #-}
17{-# LANGUAGE MultiParamTypeClasses #-}
16{-# LANGUAGE MultiParamTypeClasses #-}
18{-# LANGUAGE FlexibleInstances #-}
17{-# LANGUAGE FlexibleInstances #-}
18+{-# LANGUAGE FlexibleContexts #-}
19{-# LANGUAGE TupleSections #-}
19{-# LANGUAGE TupleSections #-}
20+{-# LANGUAGE ScopedTypeVariables #-}
21+{-# LANGUAGE RankNTypes #-}
20
22
21module Language.PureScript.TypeChecker.Kinds (
23module Language.PureScript.TypeChecker.Kinds (
22 kindOf,
24 kindOf,
@@ -28,16 +30,13 @@ module Language.PureScript.TypeChecker.Kinds (
28import Prelude ()
30import Prelude ()
29import Prelude.Compat
31import Prelude.Compat
30
32
31−import Data.Maybe (fromMaybe)
32−
33−import qualified Data.HashMap.Strict as H
34import qualified Data.Map as M
33import qualified Data.Map as M
35
34
36import Control.Arrow (second)
35import Control.Arrow (second)
37import Control.Monad
36import Control.Monad
38import Control.Monad.Error.Class (MonadError(..))
37import Control.Monad.Error.Class (MonadError(..))
38+import Control.Monad.Writer.Class (MonadWriter(..))
39import Control.Monad.State
39import Control.Monad.State
40−import Control.Monad.Unify
41
40
42import Language.PureScript.Crash
41import Language.PureScript.Crash
43import Language.PureScript.Environment
42import Language.PureScript.Environment
@@ -47,177 +46,213 @@ import Language.PureScript.Names
47import Language.PureScript.TypeChecker.Monad
46import Language.PureScript.TypeChecker.Monad
48import Language.PureScript.Types
47import Language.PureScript.Types
49
48
50−instance Partial Kind where
49+-- | Generate a fresh kind variable
51− unknown = KUnknown
50+freshKind :: (MonadState CheckState m) => m Kind
52− isUnknown (KUnknown u) = Just u
51+freshKind = do
53− isUnknown _ = Nothing
52+ k <- gets checkNextKind
54− unknowns = everythingOnKinds (++) go
53+ modify $ \st -> st { checkNextKind = k + 1 }
55− where
54+ return $ KUnknown k
56− go (KUnknown u) = [u]
57− go _ = []
58− ($?) sub = everywhereOnKinds go
59− where
60− go t@(KUnknown u) = fromMaybe t $ H.lookup u (runSubstitution sub)
61− go other = other
62−
63−instance Unifiable Check Kind where
64− KUnknown u1 =?= KUnknown u2 | u1 == u2 = return ()
65− KUnknown u =?= k = u =:= k
66− k =?= KUnknown u = u =:= k
67− Star =?= Star = return ()
68− Bang =?= Bang = return ()
69− Row k1 =?= Row k2 = k1 =?= k2
70− FunKind k1 k2 =?= FunKind k3 k4 = do
71− k1 =?= k3
72− k2 =?= k4
73− k1 =?= k2 = UnifyT . lift . throwError . errorMessage $ KindsDoNotUnify k1 k2
74
55
75−-- |
56+-- | Update the substitution to solve a kind constraint
57+solveKind :: (Functor m, Applicative m, MonadError MultipleErrors m, MonadState CheckState m) => Int -> Kind -> m ()
58+solveKind u k = do
59+ occursCheck u k
60+ modify $ \cs -> cs { checkSubstitution =
61+ (checkSubstitution cs) { substKind =
62+ M.insert u k $ substKind $ checkSubstitution cs
63+ }
64+ }
65+
66+-- | Apply a substitution to a kind
67+substituteKind :: Substitution -> Kind -> Kind
68+substituteKind sub = everywhereOnKinds go
69+ where
70+ go (KUnknown u) =
71+ case M.lookup u (substKind sub) of
72+ Nothing -> KUnknown u
73+ Just (KUnknown u1) | u1 == u -> KUnknown u1
74+ Just t -> substituteKind sub t
75+ go other = other
76+
77+-- | Make sure that an unknown does not occur in a kind
78+occursCheck :: (Functor m, Applicative m, MonadError MultipleErrors m) => Int -> Kind -> m ()
79+occursCheck _ KUnknown{} = return ()
80+occursCheck u k = void $ everywhereOnKindsM go k
81+ where
82+ go (KUnknown u') | u == u' = throwError . errorMessage . InfiniteKind $ k
83+ go other = return other
84+
85+-- | Unify two kinds
86+unifyKinds :: (Functor m, Applicative m, MonadError MultipleErrors m, MonadState CheckState m) => Kind -> Kind -> m ()
87+unifyKinds k1 k2 = do
88+ sub <- gets checkSubstitution
89+ go (substituteKind sub k1) (substituteKind sub k2)
90+ where
91+ go (KUnknown u1) (KUnknown u2) | u1 == u2 = return ()
92+ go (KUnknown u) k = solveKind u k
93+ go k (KUnknown u) = solveKind u k
94+ go Star Star = return ()
95+ go Bang Bang = return ()
96+ go (Row k1') (Row k2') = go k1' k2'
97+ go (FunKind k1' k2') (FunKind k3 k4) = do
98+ go k1' k3
99+ go k2' k4
100+ go k1' k2' = throwError . errorMessage $ KindsDoNotUnify k1' k2'
101+
76−-- Infer the kind of a single type
102+-- | Infer the kind of a single type
77−--
78−kindOf :: Type -> Check Kind
103+kindOf ::
104+ (Functor m, Applicative m, MonadError MultipleErrors m, MonadState CheckState m, MonadWriter MultipleErrors m) =>
105+ Type ->
106+ m Kind
79kindOf ty = fst <$> kindOfWithScopedVars ty
107kindOf ty = fst <$> kindOfWithScopedVars ty
80
108
81−-- |
82−-- Infer the kind of a single type, returning the kinds of any scoped type variables
109+-- | Infer the kind of a single type, returning the kinds of any scoped type variables
83−--
84−kindOfWithScopedVars :: Type -> Check (Kind, [(String, Kind)])
110+kindOfWithScopedVars ::
111+ (Functor m, Applicative m, MonadError MultipleErrors m, MonadState CheckState m, MonadWriter MultipleErrors m) =>
112+ Type ->
113+ m (Kind, [(String, Kind)])
85kindOfWithScopedVars ty =
114kindOfWithScopedVars ty =
86 rethrow (addHint (ErrorCheckingKind ty)) $
115 rethrow (addHint (ErrorCheckingKind ty)) $
87 fmap tidyUp . liftUnify $ infer ty
116 fmap tidyUp . liftUnify $ infer ty
88 where
117 where
89− tidyUp ((k, args), sub) = ( starIfUnknown (sub $? k)
118+ tidyUp ((k, args), sub) = ( starIfUnknown (substituteKind sub k)
90− , map (second (starIfUnknown . (sub $?))) args
119+ , map (second (starIfUnknown . substituteKind sub)) args
91 )
120 )
92
121
93−-- |
94−-- Infer the kind of a type constructor with a collection of arguments and a collection of associated data constructors
122+-- | Infer the kind of a type constructor with a collection of arguments and a collection of associated data constructors
95−--
123+kindsOf ::
124+ (Functor m, Applicative m, MonadError MultipleErrors m, MonadState CheckState m, MonadWriter MultipleErrors m) =>
125+ Bool ->
126+ ModuleName ->
127+ ProperName ->
96−kindsOf :: Bool -> ModuleName -> ProperName -> [(String, Maybe Kind)] -> [Type] -> Check Kind
128+ [(String, Maybe Kind)] ->
129+ [Type] ->
130+ m Kind
97kindsOf isData moduleName name args ts = fmap tidyUp . liftUnify $ do
131kindsOf isData moduleName name args ts = fmap tidyUp . liftUnify $ do
98− tyCon <- fresh
132+ tyCon <- freshKind
99− kargs <- replicateM (length args) fresh
133+ kargs <- replicateM (length args) freshKind
100 rest <- zipWithM freshKindVar args kargs
134 rest <- zipWithM freshKindVar args kargs
101 let dict = (name, tyCon) : rest
135 let dict = (name, tyCon) : rest
102 bindLocalTypeVariables moduleName dict $
136 bindLocalTypeVariables moduleName dict $
103 solveTypes isData ts kargs tyCon
137 solveTypes isData ts kargs tyCon
104 where
138 where
105− tidyUp (k, sub) = starIfUnknown $ sub $? k
139+ tidyUp (k, sub) = starIfUnknown $ substituteKind sub k
106
140
141+freshKindVar ::
142+ (Functor m, Applicative m, MonadError MultipleErrors m, MonadState CheckState m) =>
107−freshKindVar :: (String, Maybe Kind) -> Kind -> UnifyT Kind Check (ProperName, Kind)
143+ (String, Maybe Kind) ->
144+ Kind ->
145+ m (ProperName, Kind)
108freshKindVar (arg, Nothing) kind = return (ProperName arg, kind)
146freshKindVar (arg, Nothing) kind = return (ProperName arg, kind)
109freshKindVar (arg, Just kind') kind = do
147freshKindVar (arg, Just kind') kind = do
110− kind =?= kind'
148+ unifyKinds kind kind'
111 return (ProperName arg, kind')
149 return (ProperName arg, kind')
112
150
113−-- |
114−-- Simultaneously infer the kinds of several mutually recursive type constructors
151+-- | Simultaneously infer the kinds of several mutually recursive type constructors
115−--
152+kindsOfAll ::
153+ (Functor m, Applicative m, MonadError MultipleErrors m, MonadState CheckState m, MonadWriter MultipleErrors m) =>
154+ ModuleName ->
116−kindsOfAll :: ModuleName -> [(ProperName, [(String, Maybe Kind)], Type)] -> [(ProperName, [(String, Maybe Kind)], [Type])] -> Check ([Kind], [Kind])
155+ [(ProperName, [(String, Maybe Kind)], Type)] ->
156+ [(ProperName, [(String, Maybe Kind)], [Type])] ->
157+ m ([Kind], [Kind])
117kindsOfAll moduleName syns tys = fmap tidyUp . liftUnify $ do
158kindsOfAll moduleName syns tys = fmap tidyUp . liftUnify $ do
118− synVars <- replicateM (length syns) fresh
159+ synVars <- replicateM (length syns) freshKind
119 let dict = zipWith (\(name, _, _) var -> (name, var)) syns synVars
160 let dict = zipWith (\(name, _, _) var -> (name, var)) syns synVars
120 bindLocalTypeVariables moduleName dict $ do
161 bindLocalTypeVariables moduleName dict $ do
121− tyCons <- replicateM (length tys) fresh
162+ tyCons <- replicateM (length tys) freshKind
122 let dict' = zipWith (\(name, _, _) tyCon -> (name, tyCon)) tys tyCons
163 let dict' = zipWith (\(name, _, _) tyCon -> (name, tyCon)) tys tyCons
123 bindLocalTypeVariables moduleName dict' $ do
164 bindLocalTypeVariables moduleName dict' $ do
124 data_ks <- zipWithM (\tyCon (_, args, ts) -> do
165 data_ks <- zipWithM (\tyCon (_, args, ts) -> do
125− kargs <- replicateM (length args) fresh
166+ kargs <- replicateM (length args) freshKind
126 argDict <- zipWithM freshKindVar args kargs
167 argDict <- zipWithM freshKindVar args kargs
127 bindLocalTypeVariables moduleName argDict $
168 bindLocalTypeVariables moduleName argDict $
128 solveTypes True ts kargs tyCon) tyCons tys
169 solveTypes True ts kargs tyCon) tyCons tys
129 syn_ks <- zipWithM (\synVar (_, args, ty) -> do
170 syn_ks <- zipWithM (\synVar (_, args, ty) -> do
130− kargs <- replicateM (length args) fresh
171+ kargs <- replicateM (length args) freshKind
131 argDict <- zipWithM freshKindVar args kargs
172 argDict <- zipWithM freshKindVar args kargs
132 bindLocalTypeVariables moduleName argDict $
173 bindLocalTypeVariables moduleName argDict $
133 solveTypes False [ty] kargs synVar) synVars syns
174 solveTypes False [ty] kargs synVar) synVars syns
134 return (syn_ks, data_ks)
175 return (syn_ks, data_ks)
135 where
176 where
136− tidyUp ((ks1, ks2), sub) = (map (starIfUnknown . (sub $?)) ks1, map (starIfUnknown . (sub $?)) ks2)
177+ tidyUp ((ks1, ks2), sub) = (map (starIfUnknown . substituteKind sub) ks1, map (starIfUnknown . substituteKind sub) ks2)
137
178
138−-- |
139−-- Solve the set of kind constraints associated with the data constructors for a type constructor
179+-- | Solve the set of kind constraints associated with the data constructors for a type constructor
140−--
141−solveTypes :: Bool -> [Type] -> [Kind] -> Kind -> UnifyT Kind Check Kind
180+solveTypes :: (Functor m, Applicative m, MonadError MultipleErrors m, MonadState CheckState m) => Bool -> [Type] -> [Kind] -> Kind -> m Kind
142solveTypes isData ts kargs tyCon = do
181solveTypes isData ts kargs tyCon = do
143 ks <- traverse (fmap fst . infer) ts
182 ks <- traverse (fmap fst . infer) ts
144 when isData $ do
183 when isData $ do
145− tyCon =?= foldr FunKind Star kargs
184+ unifyKinds tyCon (foldr FunKind Star kargs)
146− forM_ ks $ \k -> k =?= Star
185+ forM_ ks $ \k -> unifyKinds k Star
147 unless isData $
186 unless isData $
148− tyCon =?= foldr FunKind (head ks) kargs
187+ unifyKinds tyCon (foldr FunKind (head ks) kargs)
149 return tyCon
188 return tyCon
150
189
151−-- |
152−-- Default all unknown kinds to the Star kind of types
190+-- | Default all unknown kinds to the Star kind of types
153−--
154starIfUnknown :: Kind -> Kind
191starIfUnknown :: Kind -> Kind
155starIfUnknown (KUnknown _) = Star
192starIfUnknown (KUnknown _) = Star
156starIfUnknown (Row k) = Row (starIfUnknown k)
193starIfUnknown (Row k) = Row (starIfUnknown k)
157starIfUnknown (FunKind k1 k2) = FunKind (starIfUnknown k1) (starIfUnknown k2)
194starIfUnknown (FunKind k1 k2) = FunKind (starIfUnknown k1) (starIfUnknown k2)
158starIfUnknown k = k
195starIfUnknown k = k
159
196
160−-- |
161−-- Infer a kind for a type
197+-- | Infer a kind for a type
162−--
198+infer :: (Functor m, Applicative m, MonadError MultipleErrors m, MonadState CheckState m) => Type -> m (Kind, [(String, Kind)])
163−infer :: Type -> UnifyT Kind Check (Kind, [(String, Kind)])
164infer ty = rethrow (addHint (ErrorCheckingKind ty)) $ infer' ty
199infer ty = rethrow (addHint (ErrorCheckingKind ty)) $ infer' ty
165
200
166−infer' :: Type -> UnifyT Kind Check (Kind, [(String, Kind)])
201+infer' :: forall m. (Functor m, Applicative m, MonadError MultipleErrors m, MonadState CheckState m) => Type -> m (Kind, [(String, Kind)])
167infer' (ForAll ident ty _) = do
202infer' (ForAll ident ty _) = do
168− k1 <- fresh
203+ k1 <- freshKind
169 Just moduleName <- checkCurrentModule <$> get
204 Just moduleName <- checkCurrentModule <$> get
170 (k2, args) <- bindLocalTypeVariables moduleName [(ProperName ident, k1)] $ infer ty
205 (k2, args) <- bindLocalTypeVariables moduleName [(ProperName ident, k1)] $ infer ty
171− k2 =?= Star
206+ unifyKinds k2 Star
172 return (Star, (ident, k1) : args)
207 return (Star, (ident, k1) : args)
173infer' (KindedType ty k) = do
208infer' (KindedType ty k) = do
174 (k', args) <- infer ty
209 (k', args) <- infer ty
175− k =?= k'
210+ unifyKinds k k'
176 return (k', args)
211 return (k', args)
177infer' other = (, []) <$> go other
212infer' other = (, []) <$> go other
178 where
213 where
179− go :: Type -> UnifyT Kind Check Kind
214+ go :: Type -> m Kind
180 go (ForAll ident ty _) = do
215 go (ForAll ident ty _) = do
181− k1 <- fresh
216+ k1 <- freshKind
182 Just moduleName <- checkCurrentModule <$> get
217 Just moduleName <- checkCurrentModule <$> get
183 k2 <- bindLocalTypeVariables moduleName [(ProperName ident, k1)] $ go ty
218 k2 <- bindLocalTypeVariables moduleName [(ProperName ident, k1)] $ go ty
184− k2 =?= Star
219+ unifyKinds k2 Star
185 return Star
220 return Star
186 go (KindedType ty k) = do
221 go (KindedType ty k) = do
187 k' <- go ty
222 k' <- go ty
188− k =?= k'
223+ unifyKinds k k'
189 return k'
224 return k'
190− go TypeWildcard = fresh
225+ go TypeWildcard = freshKind
191 go (TypeVar v) = do
226 go (TypeVar v) = do
192 Just moduleName <- checkCurrentModule <$> get
227 Just moduleName <- checkCurrentModule <$> get
193− UnifyT . lift $ lookupTypeVariable moduleName (Qualified Nothing (ProperName v))
228+ lookupTypeVariable moduleName (Qualified Nothing (ProperName v))
194 go (Skolem v _ _) = do
229 go (Skolem v _ _) = do
195 Just moduleName <- checkCurrentModule <$> get
230 Just moduleName <- checkCurrentModule <$> get
196− UnifyT . lift $ lookupTypeVariable moduleName (Qualified Nothing (ProperName v))
231+ lookupTypeVariable moduleName (Qualified Nothing (ProperName v))
197 go (TypeConstructor v) = do
232 go (TypeConstructor v) = do
198− env <- liftCheck getEnv
233+ env <- getEnv
199 case M.lookup v (types env) of
234 case M.lookup v (types env) of
200− Nothing -> UnifyT . lift . throwError . errorMessage $ UnknownTypeConstructor v
235+ Nothing -> throwError . errorMessage $ UnknownTypeConstructor v
201 Just (kind, _) -> return kind
236 Just (kind, _) -> return kind
202 go (TypeApp t1 t2) = do
237 go (TypeApp t1 t2) = do
203− k0 <- fresh
238+ k0 <- freshKind
204 k1 <- go t1
239 k1 <- go t1
205 k2 <- go t2
240 k2 <- go t2
206− k1 =?= FunKind k2 k0
241+ unifyKinds k1 (FunKind k2 k0)
207 return k0
242 return k0
208 go REmpty = do
243 go REmpty = do
209− k <- fresh
244+ k <- freshKind
210 return $ Row k
245 return $ Row k
211 go (RCons _ ty row) = do
246 go (RCons _ ty row) = do
212 k1 <- go ty
247 k1 <- go ty
213 k2 <- go row
248 k2 <- go row
214− k2 =?= Row k1
249+ unifyKinds k2 (Row k1)
215 return $ Row k1
250 return $ Row k1
216 go (ConstrainedType deps ty) = do
251 go (ConstrainedType deps ty) = do
217 forM_ deps $ \(className, tys) -> do
252 forM_ deps $ \(className, tys) -> do
218 k <- go $ foldl TypeApp (TypeConstructor className) tys
253 k <- go $ foldl TypeApp (TypeConstructor className) tys
219− k =?= Star
254+ unifyKinds k Star
220 k <- go ty
255 k <- go ty
221− k =?= Star
256+ unifyKinds k Star
222 return Star
257 return Star
223 go _ = internalError "Invalid argument to infer"
258 go _ = internalError "Invalid argument to infer"
src/Language/PureScript/TypeChecker/Monad.hs+82−133
@@ -26,14 +26,12 @@ import Prelude ()
26import Prelude.Compat
26import Prelude.Compat
27
27
28import Data.Maybe
28import Data.Maybe
29−import Data.Foldable (for_)
30import qualified Data.Map as M
29import qualified Data.Map as M
31
30
31+import Control.Arrow (second)
32import Control.Monad.State
32import Control.Monad.State
33−import Control.Monad.Unify
34−import Control.Monad.Writer.Strict
35import Control.Monad.Error.Class (MonadError(..))
33import Control.Monad.Error.Class (MonadError(..))
36−import Control.Monad.Trans.Except
34+import Control.Monad.Writer.Class (MonadWriter(..), listen, censor)
37
35
38import Language.PureScript.Environment
36import Language.PureScript.Environment
39import Language.PureScript.Errors
37import Language.PureScript.Errors
@@ -42,9 +40,36 @@ import Language.PureScript.Names
42import Language.PureScript.TypeClassDictionaries
40import Language.PureScript.TypeClassDictionaries
43import Language.PureScript.Types
41import Language.PureScript.Types
44
42
45−-- |
43+-- | A substitution of unification variables for types or kinds
44+data Substitution = Substitution
45+ { substType :: M.Map Int Type -- ^ Type substitution
46+ , substKind :: M.Map Int Kind -- ^ Kind substitution
47+ }
48+
49+-- | An empty substitution
50+emptySubstitution :: Substitution
51+emptySubstitution = Substitution M.empty M.empty
52+
53+-- | State required for type checking
54+data CheckState = CheckState
55+ { checkEnv :: Environment -- ^ The current @Environment@
56+ , checkNextType :: Int -- ^ The next type unification variable
57+ , checkNextKind :: Int -- ^ The next kind unification variable
58+ , checkNextSkolem :: Int -- ^ The next skolem variable
59+ , checkNextSkolemScope :: Int -- ^ The next skolem scope constant
60+ , checkNextDictName :: Int -- ^ The next type class dictionary name
61+ , checkCurrentModule :: Maybe ModuleName -- ^ The current module
62+ , checkSubstitution :: Substitution -- ^ The current substitution
63+ }
64+
65+-- | Create an empty @CheckState@
66+emptyCheckState :: Environment -> CheckState
67+emptyCheckState env = CheckState env 0 0 0 0 0 Nothing emptySubstitution
68+
69+-- | Unification variables
70+type Unknown = Int
71+
46−-- Temporarily bind a collection of names to values
72+-- | Temporarily bind a collection of names to values
47−--
48bindNames :: (MonadState CheckState m) => M.Map (ModuleName, Ident) (Type, NameKind, NameVisibility) -> m a -> m a
73bindNames :: (MonadState CheckState m) => M.Map (ModuleName, Ident) (Type, NameKind, NameVisibility) -> m a -> m a
49bindNames newNames action = do
74bindNames newNames action = do
50 orig <- get
75 orig <- get
@@ -53,9 +78,7 @@ bindNames newNames action = do
53 modify $ \st -> st { checkEnv = (checkEnv st) { names = names . checkEnv $ orig } }
78 modify $ \st -> st { checkEnv = (checkEnv st) { names = names . checkEnv $ orig } }
54 return a
79 return a
55
80
56−-- |
57−-- Temporarily bind a collection of names to types
81+-- | Temporarily bind a collection of names to types
58−--
59bindTypes :: (MonadState CheckState m) => M.Map (Qualified ProperName) (Kind, TypeKind) -> m a -> m a
82bindTypes :: (MonadState CheckState m) => M.Map (Qualified ProperName) (Kind, TypeKind) -> m a -> m a
60bindTypes newNames action = do
83bindTypes newNames action = do
61 orig <- get
84 orig <- get
@@ -64,20 +87,16 @@ bindTypes newNames action = do
64 modify $ \st -> st { checkEnv = (checkEnv st) { types = types . checkEnv $ orig } }
87 modify $ \st -> st { checkEnv = (checkEnv st) { types = types . checkEnv $ orig } }
65 return a
88 return a
66
89
67−-- |
68−-- Temporarily bind a collection of names to types
90+-- | Temporarily bind a collection of names to types
69−--
70withScopedTypeVars :: (Functor m, Applicative m, MonadState CheckState m, MonadWriter MultipleErrors m) => ModuleName -> [(String, Kind)] -> m a -> m a
91withScopedTypeVars :: (Functor m, Applicative m, MonadState CheckState m, MonadWriter MultipleErrors m) => ModuleName -> [(String, Kind)] -> m a -> m a
71withScopedTypeVars mn ks ma = do
92withScopedTypeVars mn ks ma = do
72 orig <- get
93 orig <- get
73− for_ ks $ \(name, _) ->
94+ forM_ ks $ \(name, _) ->
74 when (Qualified (Just mn) (ProperName name) `M.member` types (checkEnv orig)) $
95 when (Qualified (Just mn) (ProperName name) `M.member` types (checkEnv orig)) $
75 tell . errorMessage $ ShadowedTypeVar name
96 tell . errorMessage $ ShadowedTypeVar name
76 bindTypes (M.fromList (map (\(name, k) -> (Qualified (Just mn) (ProperName name), (k, ScopedTypeVar))) ks)) ma
97 bindTypes (M.fromList (map (\(name, k) -> (Qualified (Just mn) (ProperName name), (k, ScopedTypeVar))) ks)) ma
77
98
78−-- |
79−-- Temporarily make a collection of type class dictionaries available
99+-- | Temporarily make a collection of type class dictionaries available
80−--
81withTypeClassDictionaries :: (MonadState CheckState m) => [TypeClassDictionaryInScope] -> m a -> m a
100withTypeClassDictionaries :: (MonadState CheckState m) => [TypeClassDictionaryInScope] -> m a -> m a
82withTypeClassDictionaries entries action = do
101withTypeClassDictionaries entries action = do
83 orig <- get
102 orig <- get
@@ -87,35 +106,30 @@ withTypeClassDictionaries entries action = do
87 modify $ \st -> st { checkEnv = (checkEnv st) { typeClassDictionaries = typeClassDictionaries . checkEnv $ orig } }
106 modify $ \st -> st { checkEnv = (checkEnv st) { typeClassDictionaries = typeClassDictionaries . checkEnv $ orig } }
88 return a
107 return a
89
108
90−-- |
91−-- Get the currently available map of type class dictionaries
109+-- | Get the currently available map of type class dictionaries
92−--
110+getTypeClassDictionaries ::
111+ (Functor m, MonadState CheckState m) =>
93−getTypeClassDictionaries :: (Functor m, MonadState CheckState m) => m (M.Map (Maybe ModuleName) (M.Map (Qualified ProperName) (M.Map (Qualified Ident) TypeClassDictionaryInScope)))
112+ m (M.Map (Maybe ModuleName) (M.Map (Qualified ProperName) (M.Map (Qualified Ident) TypeClassDictionaryInScope)))
94getTypeClassDictionaries = typeClassDictionaries . checkEnv <$> get
113getTypeClassDictionaries = typeClassDictionaries . checkEnv <$> get
95
114
96−-- |
97−-- Lookup type class dictionaries in a module.
115+-- | Lookup type class dictionaries in a module.
98−--
116+lookupTypeClassDictionaries ::
117+ (Functor m, MonadState CheckState m) =>
118+ Maybe ModuleName ->
99−lookupTypeClassDictionaries :: (Functor m, MonadState CheckState m) => Maybe ModuleName -> m (M.Map (Qualified ProperName) (M.Map (Qualified Ident) TypeClassDictionaryInScope))
119+ m (M.Map (Qualified ProperName) (M.Map (Qualified Ident) TypeClassDictionaryInScope))
100lookupTypeClassDictionaries mn = fromMaybe M.empty . M.lookup mn . typeClassDictionaries . checkEnv <$> get
120lookupTypeClassDictionaries mn = fromMaybe M.empty . M.lookup mn . typeClassDictionaries . checkEnv <$> get
101
121
102−-- |
103−-- Temporarily bind a collection of names to local variables
122+-- | Temporarily bind a collection of names to local variables
104−--
105bindLocalVariables :: (Functor m, MonadState CheckState m) => ModuleName -> [(Ident, Type, NameVisibility)] -> m a -> m a
123bindLocalVariables :: (Functor m, MonadState CheckState m) => ModuleName -> [(Ident, Type, NameVisibility)] -> m a -> m a
106bindLocalVariables moduleName bindings =
124bindLocalVariables moduleName bindings =
107 bindNames (M.fromList $ flip map bindings $ \(name, ty, visibility) -> ((moduleName, name), (ty, Private, visibility)))
125 bindNames (M.fromList $ flip map bindings $ \(name, ty, visibility) -> ((moduleName, name), (ty, Private, visibility)))
108
126
109−-- |
110−-- Temporarily bind a collection of names to local type variables
127+-- | Temporarily bind a collection of names to local type variables
111−--
112bindLocalTypeVariables :: (Functor m, MonadState CheckState m) => ModuleName -> [(ProperName, Kind)] -> m a -> m a
128bindLocalTypeVariables :: (Functor m, MonadState CheckState m) => ModuleName -> [(ProperName, Kind)] -> m a -> m a
113bindLocalTypeVariables moduleName bindings =
129bindLocalTypeVariables moduleName bindings =
114 bindTypes (M.fromList $ flip map bindings $ \(pn, kind) -> (Qualified (Just moduleName) pn, (kind, LocalTypeVariable)))
130 bindTypes (M.fromList $ flip map bindings $ \(pn, kind) -> (Qualified (Just moduleName) pn, (kind, LocalTypeVariable)))
115
131
116−-- |
117−-- Update the visibility of all names to Defined
132+-- | Update the visibility of all names to Defined
118−--
119makeBindingGroupVisible :: (Functor m, MonadState CheckState m) => m ()
133makeBindingGroupVisible :: (Functor m, MonadState CheckState m) => m ()
120makeBindingGroupVisible = modifyEnv $ \e -> e { names = M.map (\(ty, nk, _) -> (ty, nk, Defined)) (names e) }
134makeBindingGroupVisible = modifyEnv $ \e -> e { names = M.map (\(ty, nk, _) -> (ty, nk, Defined)) (names e) }
121
135
@@ -131,9 +145,7 @@ preservingNames action = do
131 modifyEnv $ \e -> e { names = orig }
145 modifyEnv $ \e -> e { names = orig }
132 return a
146 return a
133
147
134−-- |
135−-- Lookup the type of a value by name in the @Environment@
148+-- | Lookup the type of a value by name in the @Environment@
136−--
137lookupVariable :: (e ~ MultipleErrors, Functor m, MonadState CheckState m, MonadError e m) => ModuleName -> Qualified Ident -> m Type
149lookupVariable :: (e ~ MultipleErrors, Functor m, MonadState CheckState m, MonadError e m) => ModuleName -> Qualified Ident -> m Type
138lookupVariable currentModule (Qualified moduleName var) = do
150lookupVariable currentModule (Qualified moduleName var) = do
139 env <- getEnv
151 env <- getEnv
@@ -141,9 +153,7 @@ lookupVariable currentModule (Qualified moduleName var) = do
141 Nothing -> throwError . errorMessage $ NameIsUndefined var
153 Nothing -> throwError . errorMessage $ NameIsUndefined var
142 Just (ty, _, _) -> return ty
154 Just (ty, _, _) -> return ty
143
155
144−-- |
145−-- Lookup the visibility of a value by name in the @Environment@
156+-- | Lookup the visibility of a value by name in the @Environment@
146−--
147getVisibility :: (e ~ MultipleErrors, Functor m, MonadState CheckState m, MonadError e m) => ModuleName -> Qualified Ident -> m NameVisibility
157getVisibility :: (e ~ MultipleErrors, Functor m, MonadState CheckState m, MonadError e m) => ModuleName -> Qualified Ident -> m NameVisibility
148getVisibility currentModule (Qualified moduleName var) = do
158getVisibility currentModule (Qualified moduleName var) = do
149 env <- getEnv
159 env <- getEnv
@@ -151,9 +161,7 @@ getVisibility currentModule (Qualified moduleName var) = do
151 Nothing -> throwError . errorMessage $ NameIsUndefined var
161 Nothing -> throwError . errorMessage $ NameIsUndefined var
152 Just (_, _, vis) -> return vis
162 Just (_, _, vis) -> return vis
153
163
154−-- |
155−-- Assert that a name is visible
164+-- | Assert that a name is visible
156−--
157checkVisibility :: (e ~ MultipleErrors, Functor m, MonadState CheckState m, MonadError e m) => ModuleName -> Qualified Ident -> m ()
165checkVisibility :: (e ~ MultipleErrors, Functor m, MonadState CheckState m, MonadError e m) => ModuleName -> Qualified Ident -> m ()
158checkVisibility currentModule name@(Qualified _ var) = do
166checkVisibility currentModule name@(Qualified _ var) = do
159 vis <- getVisibility currentModule name
167 vis <- getVisibility currentModule name
@@ -161,9 +169,7 @@ checkVisibility currentModule name@(Qualified _ var) = do
161 Undefined -> throwError . errorMessage $ CycleInDeclaration var
169 Undefined -> throwError . errorMessage $ CycleInDeclaration var
162 _ -> return ()
170 _ -> return ()
163
171
164−-- |
165−-- Lookup the kind of a type by name in the @Environment@
172+-- | Lookup the kind of a type by name in the @Environment@
166−--
167lookupTypeVariable :: (e ~ MultipleErrors, Functor m, MonadState CheckState m, MonadError e m) => ModuleName -> Qualified ProperName -> m Kind
173lookupTypeVariable :: (e ~ MultipleErrors, Functor m, MonadState CheckState m, MonadError e m) => ModuleName -> Qualified ProperName -> m Kind
168lookupTypeVariable currentModule (Qualified moduleName name) = do
174lookupTypeVariable currentModule (Qualified moduleName name) = do
169 env <- getEnv
175 env <- getEnv
@@ -171,113 +177,56 @@ lookupTypeVariable currentModule (Qualified moduleName name) = do
171 Nothing -> throwError . errorMessage $ UndefinedTypeVariable name
177 Nothing -> throwError . errorMessage $ UndefinedTypeVariable name
172 Just (k, _) -> return k
178 Just (k, _) -> return k
173
179
174−-- |
175−-- State required for type checking:
176−--
177−data CheckState = CheckState {
178− -- |
179− -- The current @Environment@
180− --
181− checkEnv :: Environment
182− -- |
183− -- The next fresh unification variable name
184− --
185− , checkNextVar :: Int
186− -- |
187− -- The next type class dictionary name
188− --
189− , checkNextDictName :: Int
190− -- |
191− -- The current module
192− --
193− , checkCurrentModule :: Maybe ModuleName
194− }
195−
196−-- |
197−-- The type checking monad, which provides the state of the type checker, and error reporting capabilities
198−--
199−newtype Check a = Check { unCheck :: StateT CheckState (ExceptT MultipleErrors (Writer MultipleErrors)) a }
200− deriving (Functor, Monad, Applicative, MonadState CheckState, MonadError MultipleErrors, MonadWriter MultipleErrors)
201−
202−-- |
203−-- Get the current @Environment@
180+-- | Get the current @Environment@
204−--
205getEnv :: (Functor m, MonadState CheckState m) => m Environment
181getEnv :: (Functor m, MonadState CheckState m) => m Environment
206getEnv = checkEnv <$> get
182getEnv = checkEnv <$> get
207
183
208−-- |
209−-- Update the @Environment@
184+-- | Update the @Environment@
210−--
211putEnv :: (MonadState CheckState m) => Environment -> m ()
185putEnv :: (MonadState CheckState m) => Environment -> m ()
212putEnv env = modify (\s -> s { checkEnv = env })
186putEnv env = modify (\s -> s { checkEnv = env })
213
187
214−-- |
215−-- Modify the @Environment@
188+-- | Modify the @Environment@
216−--
217modifyEnv :: (MonadState CheckState m) => (Environment -> Environment) -> m ()
189modifyEnv :: (MonadState CheckState m) => (Environment -> Environment) -> m ()
218modifyEnv f = modify (\s -> s { checkEnv = f (checkEnv s) })
190modifyEnv f = modify (\s -> s { checkEnv = f (checkEnv s) })
219
191
220−-- |
221−-- Run a computation in the Check monad, starting with an empty @Environment@
192+-- | Run a computation in the typechecking monad, starting with an empty @Environment@
222−--
193+runCheck :: (Functor m) => StateT CheckState m a -> m (a, Environment)
223−runCheck :: (MonadError MultipleErrors m, MonadWriter MultipleErrors m) => Check a -> m (a, Environment)
224runCheck = runCheck' initEnvironment
194runCheck = runCheck' initEnvironment
225
195
226−-- |
227−-- Run a computation in the Check monad, failing with an error, or succeeding with a return value and the final @Environment@.
196+-- | Run a computation in the typechecking monad, failing with an error, or succeeding with a return value and the final @Environment@.
228−--
229−runCheck' :: (MonadError MultipleErrors m, MonadWriter MultipleErrors m) => Environment -> Check a -> m (a, Environment)
197+runCheck' :: (Functor m) => Environment -> StateT CheckState m a -> m (a, Environment)
230−runCheck' env = interpretMultipleErrorsAndWarnings . unwrapCheckWithWarnings env
198+runCheck' env check = fmap (second checkEnv) $ runStateT check (emptyCheckState env)
231− where
232− unwrapCheckWithWarnings :: Environment -> Check a -> (Either MultipleErrors (a, Environment), MultipleErrors)
233− unwrapCheckWithWarnings e =
234− (\(rc, w) -> (envCheck rc, w))
235− . runWriter
236− . runExceptT
237− . flip runStateT (CheckState e 0 0 Nothing)
238− . unCheck
239− envCheck :: Either MultipleErrors (a, CheckState) -> Either MultipleErrors (a, Environment)
240− envCheck rc = do
241− (a, s) <- rc
242− return (a, checkEnv s)
243
199
244−-- |
245−-- Make an assertion, failing with an error message
200+-- | Make an assertion, failing with an error message
246−--
247guardWith :: (MonadError e m) => e -> Bool -> m ()
201guardWith :: (MonadError e m) => e -> Bool -> m ()
248guardWith _ True = return ()
202guardWith _ True = return ()
249guardWith e False = throwError e
203guardWith e False = throwError e
250
204
251−-- |
252−-- Generate new type class dictionary name
205+-- | Generate new type class dictionary name
253−--
254−freshDictionaryName :: Check Int
206+freshDictionaryName :: (Functor m, MonadState CheckState m) => m Int
255freshDictionaryName = do
207freshDictionaryName = do
256 n <- checkNextDictName <$> get
208 n <- checkNextDictName <$> get
257 modify $ \s -> s { checkNextDictName = succ (checkNextDictName s) }
209 modify $ \s -> s { checkNextDictName = succ (checkNextDictName s) }
258 return n
210 return n
259
211
260−-- |
261−-- Lift a computation in the @Check@ monad into the substitution monad.
262−--
263−liftCheck :: Check a -> UnifyT t Check a
264−liftCheck = UnifyT . lift
265−
266−-- |
267−-- Run a computation in the substitution monad, generating a return value and the final substitution.
212+-- | Run a computation in the substitution monad, generating a return value and the final substitution.
268−--
213+liftUnify ::
214+ (MonadState CheckState m, MonadWriter MultipleErrors m) =>
215+ m a ->
269−liftUnify :: (Partial t) => UnifyT t Check a -> Check (a, Substitution t)
216+ m (a, Substitution)
270liftUnify = liftUnifyWarnings (const id)
217liftUnify = liftUnifyWarnings (const id)
271
218
272−-- |
273−-- Run a computation in the substitution monad, generating a return value, the final substitution and updating warnings values.
219+-- | Run a computation in the substitution monad, generating a return value, the final substitution and updating warnings values.
274−--
220+liftUnifyWarnings ::
221+ (MonadState CheckState m, MonadWriter MultipleErrors m) =>
275−liftUnifyWarnings :: (Partial t) => (Substitution t -> ErrorMessage -> ErrorMessage) -> UnifyT t Check a -> Check (a, Substitution t)
222+ (Substitution -> ErrorMessage -> ErrorMessage) ->
223+ m a ->
224+ m (a, Substitution)
276−liftUnifyWarnings replace unify = do
225+liftUnifyWarnings replace ma = do
277− st <- get
226+ orig <- get
278− let ru = runUnify (defaultUnifyState { unifyNextVar = checkNextVar st }) unify
227+ modify $ \st -> st { checkSubstitution = emptySubstitution }
279− ((a, ust), w) <- censor (const mempty) . listen $ ru
228+ (a, w) <- censor (const mempty) . listen $ ma
280− modify $ \st' -> st' { checkNextVar = unifyNextVar ust }
229+ subst <- gets checkSubstitution
281− let uust = unifyCurrentSubstitution ust
282− tell $ onErrorMessages (replace uust) w
230+ tell . onErrorMessages (replace subst) $ w
231+ modify $ \st -> st { checkSubstitution = checkSubstitution orig }
283− return (a, uust)
232+ return (a, subst)
src/Language/PureScript/TypeChecker/Rows.hs+13−7
@@ -13,38 +13,44 @@
13--
13--
14-----------------------------------------------------------------------------
14-----------------------------------------------------------------------------
15
15
16+{-# LANGUAGE ScopedTypeVariables #-}
17+{-# LANGUAGE FlexibleContexts #-}
18+{-# LANGUAGE CPP #-}
19+
16module Language.PureScript.TypeChecker.Rows (
20module Language.PureScript.TypeChecker.Rows (
17 checkDuplicateLabels
21 checkDuplicateLabels
18) where
22) where
19
23
20import Data.List
24import Data.List
21
25
26+#if __GLASGOW_HASKELL__ < 710
27+import Control.Applicative
28+#endif
22import Control.Monad
29import Control.Monad
23import Control.Monad.Error.Class (MonadError(..))
30import Control.Monad.Error.Class (MonadError(..))
31+import Control.Monad.State.Class (MonadState(..))
24
32
25import Language.PureScript.AST
33import Language.PureScript.AST
26import Language.PureScript.Errors
34import Language.PureScript.Errors
27import Language.PureScript.TypeChecker.Monad
35import Language.PureScript.TypeChecker.Monad
28import Language.PureScript.Types
36import Language.PureScript.Types
29
37
30−-- |
31−-- Ensure rows do not contain duplicate labels
38+-- | Ensure rows do not contain duplicate labels
32−--
39+checkDuplicateLabels :: forall m. (Functor m, Applicative m, MonadError MultipleErrors m, MonadState CheckState m) => Expr -> m ()
33−checkDuplicateLabels :: Expr -> Check ()
34checkDuplicateLabels =
40checkDuplicateLabels =
35 let (_, f, _) = everywhereOnValuesM def go def
41 let (_, f, _) = everywhereOnValuesM def go def
36 in void . f
42 in void . f
37 where
43 where
38− def :: a -> Check a
44+ def :: a -> m a
39 def = return
45 def = return
40
46
41− go :: Expr -> Check Expr
47+ go :: Expr -> m Expr
42 go e@(TypedValue _ val ty) = do
48 go e@(TypedValue _ val ty) = do
43 checkDups ty
49 checkDups ty
44 return e
50 return e
45
51
46 where
52 where
47− checkDups :: Type -> Check ()
53+ checkDups :: Type -> m ()
48 checkDups (TypeApp t1 t2) = checkDups t1 >> checkDups t2
54 checkDups (TypeApp t1 t2) = checkDups t1 >> checkDups t2
49 checkDups (ForAll _ t _) = checkDups t
55 checkDups (ForAll _ t _) = checkDups t
50 checkDups (ConstrainedType args t) = do
56 checkDups (ConstrainedType args t) = do
src/Language/PureScript/TypeChecker/Skolems.hs+15−7
@@ -13,6 +13,8 @@
13--
13--
14-----------------------------------------------------------------------------
14-----------------------------------------------------------------------------
15
15
16+{-# LANGUAGE FlexibleContexts #-}
17+
16module Language.PureScript.TypeChecker.Skolems (
18module Language.PureScript.TypeChecker.Skolems (
17 newSkolemConstant,
19 newSkolemConstant,
18 introduceSkolemScope,
20 introduceSkolemScope,
@@ -29,7 +31,7 @@ import Data.List (nub, (\\))
29import Data.Monoid
31import Data.Monoid
30
32
31import Control.Monad.Error.Class (MonadError(..))
33import Control.Monad.Error.Class (MonadError(..))
32−import Control.Monad.Unify
34+import Control.Monad.State.Class (MonadState(..), gets, modify)
33
35
34import Language.PureScript.Crash
36import Language.PureScript.Crash
35import Language.PureScript.AST
37import Language.PureScript.AST
@@ -40,13 +42,16 @@ import Language.PureScript.Types
40-- |
42-- |
41-- Generate a new skolem constant
43-- Generate a new skolem constant
42--
44--
43−newSkolemConstant :: UnifyT Type Check Int
45+newSkolemConstant :: (MonadState CheckState m) => m Int
44−newSkolemConstant = fresh'
46+newSkolemConstant = do
47+ s <- gets checkNextSkolem
48+ modify $ \st -> st { checkNextSkolem = s + 1 }
49+ return s
45
50
46-- |
51-- |
47-- Introduce skolem scope at every occurence of a ForAll
52-- Introduce skolem scope at every occurence of a ForAll
48--
53--
49−introduceSkolemScope :: Type -> UnifyT Type Check Type
54+introduceSkolemScope :: (Functor m, Applicative m, MonadState CheckState m) => Type -> m Type
50introduceSkolemScope = everywhereOnTypesM go
55introduceSkolemScope = everywhereOnTypesM go
51 where
56 where
52 go (ForAll ident ty Nothing) = ForAll ident ty <$> (Just <$> newSkolemScope)
57 go (ForAll ident ty Nothing) = ForAll ident ty <$> (Just <$> newSkolemScope)
@@ -55,8 +60,11 @@ introduceSkolemScope = everywhereOnTypesM go
55-- |
60-- |
56-- Generate a new skolem scope
61-- Generate a new skolem scope
57--
62--
58−newSkolemScope :: UnifyT Type Check SkolemScope
63+newSkolemScope :: (MonadState CheckState m) => m SkolemScope
59−newSkolemScope = SkolemScope <$> fresh'
64+newSkolemScope = do
65+ s <- gets checkNextSkolemScope
66+ modify $ \st -> st { checkNextSkolemScope = s + 1 }
67+ return $ SkolemScope s
60
68
61-- |
69-- |
62-- Skolemize a type variable by replacing its instances with fresh skolem constants
70-- Skolemize a type variable by replacing its instances with fresh skolem constants
@@ -84,7 +92,7 @@ skolemizeTypesInValue ident sko scope = let (_, f, _) = everywhereOnValues id on
84-- |
92-- |
85-- Ensure skolem variables do not escape their scope
93-- Ensure skolem variables do not escape their scope
86--
94--
87−skolemEscapeCheck :: Expr -> Check ()
95+skolemEscapeCheck :: (MonadError MultipleErrors m, MonadState CheckState m) => Expr -> m ()
88skolemEscapeCheck (TypedValue False _ _) = return ()
96skolemEscapeCheck (TypedValue False _ _) = return ()
89skolemEscapeCheck root@TypedValue{} =
97skolemEscapeCheck root@TypedValue{} =
90 -- Every skolem variable is created when a ForAll type is skolemized.
98 -- Every skolem variable is created when a ForAll type is skolemized.
src/Language/PureScript/TypeChecker/Subsumption.hs+23−17
@@ -13,6 +13,9 @@
13--
13--
14-----------------------------------------------------------------------------
14-----------------------------------------------------------------------------
15
15
16+{-# LANGUAGE FlexibleContexts #-}
17+{-# LANGUAGE CPP #-}
18+
16module Language.PureScript.TypeChecker.Subsumption (
19module Language.PureScript.TypeChecker.Subsumption (
17 subsumes
20 subsumes
18) where
21) where
@@ -20,8 +23,11 @@ module Language.PureScript.TypeChecker.Subsumption (
20import Data.List (sortBy)
23import Data.List (sortBy)
21import Data.Ord (comparing)
24import Data.Ord (comparing)
22
25
26+#if __GLASGOW_HASKELL__ < 710
23−import Control.Monad.Unify
27+import Control.Applicative
28+#endif
24−import Control.Monad.Error.Class (throwError)
29+import Control.Monad.Error.Class (MonadError(..))
30+import Control.Monad.State.Class (MonadState(..))
25
31
26import Language.PureScript.Crash
32import Language.PureScript.Crash
27import Language.PureScript.AST
33import Language.PureScript.AST
@@ -32,16 +38,16 @@ import Language.PureScript.TypeChecker.Skolems
32import Language.PureScript.TypeChecker.Unify
38import Language.PureScript.TypeChecker.Unify
33import Language.PureScript.Types
39import Language.PureScript.Types
34
40
35−-- |
36−-- Check whether one type subsumes another, rethrowing errors to provide a better error message
41+-- | Check that one type subsumes another, rethrowing errors to provide a better error message
37−--
38−subsumes :: Maybe Expr -> Type -> Type -> UnifyT Type Check (Maybe Expr)
42+subsumes :: (Functor m, Applicative m, MonadError MultipleErrors m, MonadState CheckState m) => Maybe Expr -> Type -> Type -> m (Maybe Expr)
39subsumes val ty1 ty2 = rethrow (addHint (ErrorInSubsumption ty1 ty2)) $ subsumes' val ty1 ty2
43subsumes val ty1 ty2 = rethrow (addHint (ErrorInSubsumption ty1 ty2)) $ subsumes' val ty1 ty2
40
44
41−-- |
42−-- Check whether one type subsumes another
45+-- | Check tahat one type subsumes another
43−--
46+subsumes' :: (Functor m, Applicative m, MonadError MultipleErrors m, MonadState CheckState m) =>
44−subsumes' :: Maybe Expr -> Type -> Type -> UnifyT Type Check (Maybe Expr)
47+ Maybe Expr ->
48+ Type ->
49+ Type ->
50+ m (Maybe Expr)
45subsumes' val (ForAll ident ty1 _) ty2 = do
51subsumes' val (ForAll ident ty1 _) ty2 = do
46 replaced <- replaceVarWithUnknown ident ty1
52 replaced <- replaceVarWithUnknown ident ty1
47 subsumes val replaced ty2
53 subsumes val replaced ty2
@@ -72,25 +78,25 @@ subsumes' val (TypeApp f1 r1) (TypeApp f2 r2) | f1 == tyObject && f2 == tyObject
72 go ts1' ts2' r1' r2'
78 go ts1' ts2' r1' r2'
73 return val
79 return val
74 where
80 where
75− go [] ts2 r1' r2' = r1' =?= rowFromList (ts2, r2')
81+ go [] ts2 r1' r2' = unifyTypes r1' (rowFromList (ts2, r2'))
76− go ts1 [] r1' r2' = r2' =?= rowFromList (ts1, r1')
82+ go ts1 [] r1' r2' = unifyTypes r2' (rowFromList (ts1, r1'))
77 go ((p1, ty1) : ts1) ((p2, ty2) : ts2) r1' r2'
83 go ((p1, ty1) : ts1) ((p2, ty2) : ts2) r1' r2'
78 | p1 == p2 = do _ <- subsumes Nothing ty1 ty2
84 | p1 == p2 = do _ <- subsumes Nothing ty1 ty2
79 go ts1 ts2 r1' r2'
85 go ts1 ts2 r1' r2'
80− | p1 < p2 = do rest <- fresh
86+ | p1 < p2 = do rest <- freshType
81 -- What happens next is a bit of a hack.
87 -- What happens next is a bit of a hack.
82 -- TODO: in the new type checker, object properties will probably be restricted to being monotypes
88 -- TODO: in the new type checker, object properties will probably be restricted to being monotypes
83 -- in which case, this branch of the subsumes function should not even be necessary.
89 -- in which case, this branch of the subsumes function should not even be necessary.
84 case r2' of
90 case r2' of
85 REmpty -> throwError . errorMessage $ AdditionalProperty p1
91 REmpty -> throwError . errorMessage $ AdditionalProperty p1
86− _ -> r2' =?= RCons p1 ty1 rest
92+ _ -> unifyTypes r2' (RCons p1 ty1 rest)
87 go ts1 ((p2, ty2) : ts2) r1' rest
93 go ts1 ((p2, ty2) : ts2) r1' rest
88− | otherwise = do rest <- fresh
94+ | otherwise = do rest <- freshType
89 case r1' of
95 case r1' of
90 REmpty -> throwError . errorMessage $ PropertyIsMissing p2
96 REmpty -> throwError . errorMessage $ PropertyIsMissing p2
91− _ -> r1' =?= RCons p2 ty2 rest
97+ _ -> unifyTypes r1' (RCons p2 ty2 rest)
92 go ((p1, ty1) : ts1) ts2 rest r2'
98 go ((p1, ty1) : ts1) ts2 rest r2'
93subsumes' val ty1 ty2@(TypeApp obj _) | obj == tyObject = subsumes val ty2 ty1
99subsumes' val ty1 ty2@(TypeApp obj _) | obj == tyObject = subsumes val ty2 ty1
94subsumes' val ty1 ty2 = do
100subsumes' val ty1 ty2 = do
95− ty1 =?= ty2
101+ unifyTypes ty1 ty2
96 return val
102 return val
src/Language/PureScript/TypeChecker/Types.hs+176−110
@@ -14,6 +14,7 @@
14-----------------------------------------------------------------------------
14-----------------------------------------------------------------------------
15
15
16{-# LANGUAGE FlexibleContexts #-}
16{-# LANGUAGE FlexibleContexts #-}
17+{-# LANGUAGE ScopedTypeVariables #-}
17{-# LANGUAGE MultiParamTypeClasses #-}
18{-# LANGUAGE MultiParamTypeClasses #-}
18{-# LANGUAGE OverloadedStrings #-}
19{-# LANGUAGE OverloadedStrings #-}
19
20
@@ -46,10 +47,9 @@ import Data.Maybe (fromMaybe)
46import qualified Data.Map as M
47import qualified Data.Map as M
47
48
48import Control.Monad
49import Control.Monad
49−import Control.Monad.State
50+import Control.Monad.State.Class (MonadState(..), gets)
50−import Control.Monad.Unify
51import Control.Monad.Error.Class (MonadError(..))
51import Control.Monad.Error.Class (MonadError(..))
52−import Control.Monad.Writer.Class (tell)
52+import Control.Monad.Writer.Class (MonadWriter(..))
53
53
54import Language.PureScript.Crash
54import Language.PureScript.Crash
55import Language.PureScript.AST
55import Language.PureScript.AST
@@ -69,11 +69,13 @@ import Language.PureScript.TypeChecker.Unify
69import Language.PureScript.TypeClassDictionaries
69import Language.PureScript.TypeClassDictionaries
70import Language.PureScript.Types
70import Language.PureScript.Types
71
71
72−-- |
73−-- Infer the types of multiple mutually-recursive values, and return elaborated values including
72+-- | Infer the types of multiple mutually-recursive values, and return elaborated values including
74-- type class dictionaries and type annotations.
73-- type class dictionaries and type annotations.
75−--
74+typesOf ::
75+ (Functor m, Applicative m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
76+ ModuleName ->
77+ [(Ident, Expr)] ->
76−typesOf :: ModuleName -> [(Ident, Expr)] -> Check [(Ident, (Expr, Type))]
78+ m [(Ident, (Expr, Type))]
77typesOf moduleName vals = do
79typesOf moduleName vals = do
78 tys <- fmap tidyUp . liftUnifyWarnings replace $ do
80 tys <- fmap tidyUp . liftUnifyWarnings replace $ do
79 (untyped, typed, dict, untypedDict) <- typeDictionaryForBindingGroup moduleName vals
81 (untyped, typed, dict, untypedDict) <- typeDictionaryForBindingGroup moduleName vals
@@ -91,17 +93,21 @@ typesOf moduleName vals = do
91 return (ident, (val', varIfUnknown ty))
93 return (ident, (val', varIfUnknown ty))
92 where
94 where
93 -- Apply the substitution that was returned from runUnify to both types and (type-annotated) values
95 -- Apply the substitution that was returned from runUnify to both types and (type-annotated) values
94− tidyUp (ts, sub) = map (\(i, (val, ty)) -> (i, (overTypes (sub $?) val, sub $? ty))) ts
96+ tidyUp (ts, sub) = map (\(i, (val, ty)) -> (i, (overTypes (substituteType sub) val, substituteType sub ty))) ts
95 -- Replace all the wildcards types with their inferred types
97 -- Replace all the wildcards types with their inferred types
96− replace sub (ErrorMessage hints (WildcardInferredType ty)) = ErrorMessage hints $ WildcardInferredType (sub $? ty)
98+ replace sub (ErrorMessage hints (WildcardInferredType ty)) = ErrorMessage hints . WildcardInferredType $ substituteType sub ty
97− replace sub (ErrorMessage hints (MissingTypeDeclaration name ty)) = ErrorMessage hints $ MissingTypeDeclaration name (varIfUnknown (sub $? ty))
99+ replace sub (ErrorMessage hints (MissingTypeDeclaration name ty)) = ErrorMessage hints $ MissingTypeDeclaration name (varIfUnknown (substituteType sub ty))
98 replace _ em = em
100 replace _ em = em
99
101
100type TypeData = M.Map (ModuleName, Ident) (Type, NameKind, NameVisibility)
102type TypeData = M.Map (ModuleName, Ident) (Type, NameKind, NameVisibility)
101
103
102type UntypedData = [(Ident, Type)]
104type UntypedData = [(Ident, Type)]
103
105
106+typeDictionaryForBindingGroup ::
107+ (Functor m, Applicative m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
108+ ModuleName ->
109+ [(Ident, Expr)] ->
104−typeDictionaryForBindingGroup :: ModuleName -> [(Ident, Expr)] -> UnifyT Type Check ([(Ident, Expr)], [(Ident, (Expr, Type, Bool))], TypeData, UntypedData)
110+ m ([(Ident, Expr)], [(Ident, (Expr, Type, Bool))], TypeData, UntypedData)
105typeDictionaryForBindingGroup moduleName vals = do
111typeDictionaryForBindingGroup moduleName vals = do
106 let
112 let
107 -- Map each declaration to a name/value pair, with an optional type, if the declaration is typed
113 -- Map each declaration to a name/value pair, with an optional type, if the declaration is typed
@@ -113,7 +119,7 @@ typeDictionaryForBindingGroup moduleName vals = do
113 typedDict = map (\(ident, (_, ty, _)) -> (ident, ty)) typed
119 typedDict = map (\(ident, (_, ty, _)) -> (ident, ty)) typed
114
120
115 -- Create fresh unification variables for the types of untyped declarations
121 -- Create fresh unification variables for the types of untyped declarations
116− untypedNames <- replicateM (length untyped) fresh
122+ untypedNames <- replicateM (length untyped) freshType
117
123
118 let
124 let
119 -- Make a map of names to the unification variables of untyped declarations
125 -- Make a map of names to the unification variables of untyped declarations
@@ -122,12 +128,17 @@ typeDictionaryForBindingGroup moduleName vals = do
122 dict = M.fromList (map (\(ident, ty) -> ((moduleName, ident), (ty, Private, Undefined))) $ typedDict ++ untypedDict)
128 dict = M.fromList (map (\(ident, ty) -> ((moduleName, ident), (ty, Private, Undefined))) $ typedDict ++ untypedDict)
123 return (untyped, typed, dict, untypedDict)
129 return (untyped, typed, dict, untypedDict)
124
130
125−checkTypedBindingGroupElement :: ModuleName -> (Ident, (Expr, Type, Bool)) -> TypeData -> UnifyT Type Check (Ident, (Expr, Type))
131+checkTypedBindingGroupElement ::
132+ (Functor m, Applicative m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
133+ ModuleName ->
134+ (Ident, (Expr, Type, Bool)) ->
135+ TypeData ->
136+ m (Ident, (Expr, Type))
126checkTypedBindingGroupElement mn (ident, (val', ty, checkType)) dict = do
137checkTypedBindingGroupElement mn (ident, (val', ty, checkType)) dict = do
127 -- Replace type wildcards
138 -- Replace type wildcards
128 ty' <- replaceTypeWildcards ty
139 ty' <- replaceTypeWildcards ty
129 -- Kind check
140 -- Kind check
130− (kind, args) <- liftCheck $ kindOfWithScopedVars ty
141+ (kind, args) <- kindOfWithScopedVars ty
131 checkTypeKind ty kind
142 checkTypeKind ty kind
132 -- Check the type with the new names in scope
143 -- Check the type with the new names in scope
133 ty'' <- introduceSkolemScope <=< replaceAllTypeSynonyms <=< replaceTypeWildcards $ ty'
144 ty'' <- introduceSkolemScope <=< replaceAllTypeSynonyms <=< replaceTypeWildcards $ ty'
@@ -136,17 +147,21 @@ checkTypedBindingGroupElement mn (ident, (val', ty, checkType)) dict = do
136 else return (TypedValue False val' ty'')
147 else return (TypedValue False val' ty'')
137 return (ident, (val'', ty''))
148 return (ident, (val'', ty''))
138
149
139−typeForBindingGroupElement :: Bool -> (Ident, Expr) -> TypeData -> UntypedData -> UnifyT Type Check (Ident, (Expr, Type))
150+typeForBindingGroupElement ::
151+ (Functor m, Applicative m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
152+ Bool ->
153+ (Ident, Expr) ->
154+ TypeData ->
155+ UntypedData ->
156+ m (Ident, (Expr, Type))
140typeForBindingGroupElement warn (ident, val) dict untypedDict = do
157typeForBindingGroupElement warn (ident, val) dict untypedDict = do
141 -- Infer the type with the new names in scope
158 -- Infer the type with the new names in scope
142 TypedValue _ val' ty <- bindNames dict $ infer val
159 TypedValue _ val' ty <- bindNames dict $ infer val
143− ty =?= fromMaybe (internalError "name not found in dictionary") (lookup ident untypedDict)
160+ unifyTypes ty $ fromMaybe (internalError "name not found in dictionary") (lookup ident untypedDict)
144 when warn . tell . errorMessage $ MissingTypeDeclaration ident ty
161 when warn . tell . errorMessage $ MissingTypeDeclaration ident ty
145 return (ident, (TypedValue True val' ty, ty))
162 return (ident, (TypedValue True val' ty, ty))
146
163
147−-- |
148−-- Check if a value contains a type annotation
164+-- | Check if a value contains a type annotation
149−--
150isTyped :: (Ident, Expr) -> Either (Ident, Expr) (Ident, (Expr, Type, Bool))
165isTyped :: (Ident, Expr) -> Either (Ident, Expr) (Ident, (Expr, Type, Bool))
151isTyped (name, TypedValue checkType value ty) = Right (name, (value, ty, checkType))
166isTyped (name, TypedValue checkType value ty) = Right (name, (value, ty, checkType))
152isTyped (name, value) = Left (name, value)
167isTyped (name, value) = Left (name, value)
@@ -162,10 +177,12 @@ overTypes f = let (_, f', _) = everywhereOnValues id g id in f'
162 g (TypeClassDictionary (nm, tys) sco) = TypeClassDictionary (nm, map f tys) sco
177 g (TypeClassDictionary (nm, tys) sco) = TypeClassDictionary (nm, map f tys) sco
163 g other = other
178 g other = other
164
179
165−-- |
166−-- Replace type class dictionary placeholders with inferred type class dictionaries
180+-- | Replace type class dictionary placeholders with inferred type class dictionaries
167−--
168−replaceTypeClassDictionaries :: ModuleName -> Expr -> Check Expr
181+replaceTypeClassDictionaries ::
182+ (Functor m, Applicative m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
183+ ModuleName ->
184+ Expr ->
185+ m Expr
169replaceTypeClassDictionaries mn =
186replaceTypeClassDictionaries mn =
170 let (_, f, _) = everywhereOnValuesTopDownM return go return
187 let (_, f, _) = everywhereOnValuesTopDownM return go return
171 in f
188 in f
@@ -173,20 +190,24 @@ replaceTypeClassDictionaries mn =
173 go (TypeClassDictionary constraint dicts) = entails mn dicts constraint
190 go (TypeClassDictionary constraint dicts) = entails mn dicts constraint
174 go other = return other
191 go other = return other
175
192
176−-- |
177−-- Check the kind of a type, failing if it is not of kind *.
193+-- | Check the kind of a type, failing if it is not of kind *.
178−--
179−checkTypeKind :: Type -> Kind -> UnifyT t Check ()
194+checkTypeKind ::
195+ (Functor m, Applicative m, MonadState CheckState m, MonadError MultipleErrors m) =>
196+ Type ->
197+ Kind ->
198+ m ()
180checkTypeKind ty kind = guardWith (errorMessage (ExpectedType ty kind)) $ kind == Star
199checkTypeKind ty kind = guardWith (errorMessage (ExpectedType ty kind)) $ kind == Star
181
200
182−-- |
183−-- Remove any ForAlls and ConstrainedType constructors in a type by introducing new unknowns
201+-- | Remove any ForAlls and ConstrainedType constructors in a type by introducing new unknowns
184-- or TypeClassDictionary values.
202-- or TypeClassDictionary values.
185--
203--
186-- This is necessary during type checking to avoid unifying a polymorphic type with a
204-- This is necessary during type checking to avoid unifying a polymorphic type with a
187-- unification variable.
205-- unification variable.
188−--
189−instantiatePolyTypeWithUnknowns :: Expr -> Type -> UnifyT Type Check (Expr, Type)
206+instantiatePolyTypeWithUnknowns ::
207+ (Functor m, Applicative m, MonadState CheckState m, MonadError MultipleErrors m) =>
208+ Expr ->
209+ Type ->
210+ m (Expr, Type)
190instantiatePolyTypeWithUnknowns val (ForAll ident ty _) = do
211instantiatePolyTypeWithUnknowns val (ForAll ident ty _) = do
191 ty' <- replaceVarWithUnknown ident ty
212 ty' <- replaceVarWithUnknown ident ty
192 instantiatePolyTypeWithUnknowns val ty'
213 instantiatePolyTypeWithUnknowns val ty'
@@ -196,16 +217,18 @@ instantiatePolyTypeWithUnknowns val (ConstrainedType constraints ty) = do
196 return (foldl App val (map (flip TypeClassDictionary dicts) constraints), ty')
217 return (foldl App val (map (flip TypeClassDictionary dicts) constraints), ty')
197instantiatePolyTypeWithUnknowns val ty = return (val, ty)
218instantiatePolyTypeWithUnknowns val ty = return (val, ty)
198
219
199−-- |
200−-- Infer a type for a value, rethrowing any error to provide a more useful error message
220+-- | Infer a type for a value, rethrowing any error to provide a more useful error message
201−--
221+infer ::
202−infer :: Expr -> UnifyT Type Check Expr
222+ (Functor m, Applicative m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
223+ Expr ->
224+ m Expr
203infer val = rethrow (addHint (ErrorInferringType val)) $ infer' val
225infer val = rethrow (addHint (ErrorInferringType val)) $ infer' val
204
226
205−-- |
206−-- Infer a type for a value
227+-- | Infer a type for a value
207−--
228+infer' ::
208−infer' :: Expr -> UnifyT Type Check Expr
229+ (Functor m, Applicative m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
230+ Expr ->
231+ m Expr
209infer' v@(NumericLiteral (Left _)) = return $ TypedValue True v tyInt
232infer' v@(NumericLiteral (Left _)) = return $ TypedValue True v tyInt
210infer' v@(NumericLiteral (Right _)) = return $ TypedValue True v tyNumber
233infer' v@(NumericLiteral (Right _)) = return $ TypedValue True v tyNumber
211infer' v@(StringLiteral _) = return $ TypedValue True v tyString
234infer' v@(StringLiteral _) = return $ TypedValue True v tyString
@@ -213,8 +236,8 @@ infer' v@(CharLiteral _) = return $ TypedValue True v tyChar
213infer' v@(BooleanLiteral _) = return $ TypedValue True v tyBoolean
236infer' v@(BooleanLiteral _) = return $ TypedValue True v tyBoolean
214infer' (ArrayLiteral vals) = do
237infer' (ArrayLiteral vals) = do
215 ts <- traverse infer vals
238 ts <- traverse infer vals
216− els <- fresh
239+ els <- freshType
217− forM_ ts $ \(TypedValue _ _ t) -> els =?= t
240+ forM_ ts $ \(TypedValue _ _ t) -> unifyTypes els t
218 return $ TypedValue True (ArrayLiteral ts) (TypeApp tyArray els)
241 return $ TypedValue True (ArrayLiteral ts) (TypeApp tyArray els)
219infer' (ObjectLiteral ps) = do
242infer' (ObjectLiteral ps) = do
220 ensureNoDuplicateProperties ps
243 ensureNoDuplicateProperties ps
@@ -224,20 +247,20 @@ infer' (ObjectLiteral ps) = do
224 return $ TypedValue True (ObjectLiteral (zip (map fst ps) ts)) ty
247 return $ TypedValue True (ObjectLiteral (zip (map fst ps) ts)) ty
225infer' (ObjectUpdate o ps) = do
248infer' (ObjectUpdate o ps) = do
226 ensureNoDuplicateProperties ps
249 ensureNoDuplicateProperties ps
227− row <- fresh
250+ row <- freshType
228 newVals <- zipWith (\(name, _) t -> (name, t)) ps <$> traverse (infer . snd) ps
251 newVals <- zipWith (\(name, _) t -> (name, t)) ps <$> traverse (infer . snd) ps
229 let newTys = map (\(name, TypedValue _ _ ty) -> (name, ty)) newVals
252 let newTys = map (\(name, TypedValue _ _ ty) -> (name, ty)) newVals
230− oldTys <- zip (map fst ps) <$> replicateM (length ps) fresh
253+ oldTys <- zip (map fst ps) <$> replicateM (length ps) freshType
231 let oldTy = TypeApp tyObject $ rowFromList (oldTys, row)
254 let oldTy = TypeApp tyObject $ rowFromList (oldTys, row)
232 o' <- TypedValue True <$> check o oldTy <*> pure oldTy
255 o' <- TypedValue True <$> check o oldTy <*> pure oldTy
233 return $ TypedValue True (ObjectUpdate o' newVals) $ TypeApp tyObject $ rowFromList (newTys, row)
256 return $ TypedValue True (ObjectUpdate o' newVals) $ TypeApp tyObject $ rowFromList (newTys, row)
234infer' (Accessor prop val) = rethrow (addHint (ErrorCheckingAccessor val prop)) $ do
257infer' (Accessor prop val) = rethrow (addHint (ErrorCheckingAccessor val prop)) $ do
235− field <- fresh
258+ field <- freshType
236− rest <- fresh
259+ rest <- freshType
237 typed <- check val (TypeApp tyObject (RCons prop field rest))
260 typed <- check val (TypeApp tyObject (RCons prop field rest))
238 return $ TypedValue True (Accessor prop typed) field
261 return $ TypedValue True (Accessor prop typed) field
239infer' (Abs (Left arg) ret) = do
262infer' (Abs (Left arg) ret) = do
240− ty <- fresh
263+ ty <- freshType
241 Just moduleName <- checkCurrentModule <$> get
264 Just moduleName <- checkCurrentModule <$> get
242 withBindingGroupVisible $ bindLocalVariables moduleName [(arg, ty, Defined)] $ do
265 withBindingGroupVisible $ bindLocalVariables moduleName [(arg, ty, Defined)] $ do
243 body@(TypedValue _ _ bodyTy) <- infer' ret
266 body@(TypedValue _ _ bodyTy) <- infer' ret
@@ -264,7 +287,7 @@ infer' v@(Constructor c) = do
264 return $ TypedValue True v' ty'
287 return $ TypedValue True v' ty'
265infer' (Case vals binders) = do
288infer' (Case vals binders) = do
266 (vals', ts) <- instantiateForBinders vals binders
289 (vals', ts) <- instantiateForBinders vals binders
267− ret <- fresh
290+ ret <- freshType
268 binders' <- checkBinders ts ret binders
291 binders' <- checkBinders ts ret binders
269 return $ TypedValue True (Case vals' binders') ret
292 return $ TypedValue True (Case vals' binders') ret
270infer' (IfThenElse cond th el) = do
293infer' (IfThenElse cond th el) = do
@@ -281,7 +304,7 @@ infer' (SuperClassDictionary className tys) = do
281 return $ TypeClassDictionary (className, tys) dicts
304 return $ TypeClassDictionary (className, tys) dicts
282infer' (TypedValue checkType val ty) = do
305infer' (TypedValue checkType val ty) = do
283 Just moduleName <- checkCurrentModule <$> get
306 Just moduleName <- checkCurrentModule <$> get
284− (kind, args) <- liftCheck $ kindOfWithScopedVars ty
307+ (kind, args) <- kindOfWithScopedVars ty
285 checkTypeKind ty kind
308 checkTypeKind ty kind
286 ty' <- introduceSkolemScope <=< replaceAllTypeSynonyms <=< replaceTypeWildcards $ ty
309 ty' <- introduceSkolemScope <=< replaceAllTypeSynonyms <=< replaceTypeWildcards $ ty
287 val' <- if checkType then withScopedTypeVars moduleName args (check val ty') else return val
310 val' <- if checkType then withScopedTypeVars moduleName args (check val ty') else return val
@@ -289,22 +312,28 @@ infer' (TypedValue checkType val ty) = do
289infer' (PositionedValue pos _ val) = warnAndRethrowWithPosition pos $ infer' val
312infer' (PositionedValue pos _ val) = warnAndRethrowWithPosition pos $ infer' val
290infer' _ = internalError "Invalid argument to infer"
313infer' _ = internalError "Invalid argument to infer"
291
314
292−inferLetBinding :: [Declaration] -> [Declaration] -> Expr -> (Expr -> UnifyT Type Check Expr) -> UnifyT Type Check ([Declaration], Expr)
315+inferLetBinding ::
316+ (Functor m, Applicative m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
317+ [Declaration] ->
318+ [Declaration] ->
319+ Expr ->
320+ (Expr -> m Expr) ->
321+ m ([Declaration], Expr)
293inferLetBinding seen [] ret j = (,) seen <$> withBindingGroupVisible (j ret)
322inferLetBinding seen [] ret j = (,) seen <$> withBindingGroupVisible (j ret)
294inferLetBinding seen (ValueDeclaration ident nameKind [] (Right (tv@(TypedValue checkType val ty))) : rest) ret j = do
323inferLetBinding seen (ValueDeclaration ident nameKind [] (Right (tv@(TypedValue checkType val ty))) : rest) ret j = do
295 Just moduleName <- checkCurrentModule <$> get
324 Just moduleName <- checkCurrentModule <$> get
296− (kind, args) <- liftCheck $ kindOfWithScopedVars ty
325+ (kind, args) <- kindOfWithScopedVars ty
297 checkTypeKind ty kind
326 checkTypeKind ty kind
298 let dict = M.singleton (moduleName, ident) (ty, nameKind, Undefined)
327 let dict = M.singleton (moduleName, ident) (ty, nameKind, Undefined)
299 ty' <- introduceSkolemScope <=< replaceAllTypeSynonyms <=< replaceTypeWildcards $ ty
328 ty' <- introduceSkolemScope <=< replaceAllTypeSynonyms <=< replaceTypeWildcards $ ty
300 TypedValue _ val' ty'' <- if checkType then withScopedTypeVars moduleName args (bindNames dict (check val ty')) else return tv
329 TypedValue _ val' ty'' <- if checkType then withScopedTypeVars moduleName args (bindNames dict (check val ty')) else return tv
301 bindNames (M.singleton (moduleName, ident) (ty'', nameKind, Defined)) $ inferLetBinding (seen ++ [ValueDeclaration ident nameKind [] (Right (TypedValue checkType val' ty''))]) rest ret j
330 bindNames (M.singleton (moduleName, ident) (ty'', nameKind, Defined)) $ inferLetBinding (seen ++ [ValueDeclaration ident nameKind [] (Right (TypedValue checkType val' ty''))]) rest ret j
302inferLetBinding seen (ValueDeclaration ident nameKind [] (Right val) : rest) ret j = do
331inferLetBinding seen (ValueDeclaration ident nameKind [] (Right val) : rest) ret j = do
303− valTy <- fresh
332+ valTy <- freshType
304 Just moduleName <- checkCurrentModule <$> get
333 Just moduleName <- checkCurrentModule <$> get
305 let dict = M.singleton (moduleName, ident) (valTy, nameKind, Undefined)
334 let dict = M.singleton (moduleName, ident) (valTy, nameKind, Undefined)
306 TypedValue _ val' valTy' <- bindNames dict $ infer val
335 TypedValue _ val' valTy' <- bindNames dict $ infer val
307− valTy =?= valTy'
336+ unifyTypes valTy valTy'
308 bindNames (M.singleton (moduleName, ident) (valTy', nameKind, Defined)) $ inferLetBinding (seen ++ [ValueDeclaration ident nameKind [] (Right val')]) rest ret j
337 bindNames (M.singleton (moduleName, ident) (valTy', nameKind, Defined)) $ inferLetBinding (seen ++ [ValueDeclaration ident nameKind [] (Right val')]) rest ret j
309inferLetBinding seen (BindingGroupDeclaration ds : rest) ret j = do
338inferLetBinding seen (BindingGroupDeclaration ds : rest) ret j = do
310 Just moduleName <- checkCurrentModule <$> get
339 Just moduleName <- checkCurrentModule <$> get
@@ -320,16 +349,18 @@ inferLetBinding seen (PositionedDeclaration pos com d : ds) ret j = warnAndRethr
320 return (PositionedDeclaration pos com d' : ds', val')
349 return (PositionedDeclaration pos com d' : ds', val')
321inferLetBinding _ _ _ _ = internalError "Invalid argument to inferLetBinding"
350inferLetBinding _ _ _ _ = internalError "Invalid argument to inferLetBinding"
322
351
323−-- |
324−-- Infer the types of variables brought into scope by a binder
352+-- | Infer the types of variables brought into scope by a binder
325−--
353+inferBinder :: forall m.
354+ (Functor m, Applicative m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
355+ Type ->
356+ Binder ->
326−inferBinder :: Type -> Binder -> UnifyT Type Check (M.Map Ident Type)
357+ m (M.Map Ident Type)
327inferBinder _ NullBinder = return M.empty
358inferBinder _ NullBinder = return M.empty
328−inferBinder val (StringBinder _) = val =?= tyString >> return M.empty
359+inferBinder val (StringBinder _) = unifyTypes val tyString >> return M.empty
329−inferBinder val (CharBinder _) = val =?= tyChar >> return M.empty
360+inferBinder val (CharBinder _) = unifyTypes val tyChar >> return M.empty
330−inferBinder val (NumberBinder (Left _)) = val =?= tyInt >> return M.empty
361+inferBinder val (NumberBinder (Left _)) = unifyTypes val tyInt >> return M.empty
331−inferBinder val (NumberBinder (Right _)) = val =?= tyNumber >> return M.empty
362+inferBinder val (NumberBinder (Right _)) = unifyTypes val tyNumber >> return M.empty
332−inferBinder val (BooleanBinder _) = val =?= tyBoolean >> return M.empty
363+inferBinder val (BooleanBinder _) = unifyTypes val tyBoolean >> return M.empty
333inferBinder val (VarBinder name) = return $ M.singleton name val
364inferBinder val (VarBinder name) = return $ M.singleton name val
334inferBinder val (ConstructorBinder ctor binders) = do
365inferBinder val (ConstructorBinder ctor binders) = do
335 env <- getEnv
366 env <- getEnv
@@ -339,7 +370,7 @@ inferBinder val (ConstructorBinder ctor binders) = do
339 fn' <- introduceSkolemScope <=< replaceAllTypeSynonyms $ fn
370 fn' <- introduceSkolemScope <=< replaceAllTypeSynonyms $ fn
340 let (args, ret) = peelArgs fn'
371 let (args, ret) = peelArgs fn'
341 unless (length args == length binders) . throwError . errorMessage $ IncorrectConstructorArity ctor
372 unless (length args == length binders) . throwError . errorMessage $ IncorrectConstructorArity ctor
342− ret =?= val
373+ unifyTypes ret val
343 M.unions <$> zipWithM inferBinder (reverse args) binders
374 M.unions <$> zipWithM inferBinder (reverse args) binders
344 _ -> throwError . errorMessage $ UnknownDataConstructor ctor Nothing
375 _ -> throwError . errorMessage $ UnknownDataConstructor ctor Nothing
345 where
376 where
@@ -349,23 +380,23 @@ inferBinder val (ConstructorBinder ctor binders) = do
349 go args (TypeApp (TypeApp fn arg) ret) | fn == tyFunction = go (arg : args) ret
380 go args (TypeApp (TypeApp fn arg) ret) | fn == tyFunction = go (arg : args) ret
350 go args ret = (args, ret)
381 go args ret = (args, ret)
351inferBinder val (ObjectBinder props) = do
382inferBinder val (ObjectBinder props) = do
352− row <- fresh
383+ row <- freshType
353− rest <- fresh
384+ rest <- freshType
354 m1 <- inferRowProperties row rest props
385 m1 <- inferRowProperties row rest props
355− val =?= TypeApp tyObject row
386+ unifyTypes val (TypeApp tyObject row)
356 return m1
387 return m1
357 where
388 where
358− inferRowProperties :: Type -> Type -> [(String, Binder)] -> UnifyT Type Check (M.Map Ident Type)
389+ inferRowProperties :: Type -> Type -> [(String, Binder)] -> m (M.Map Ident Type)
359− inferRowProperties nrow row [] = nrow =?= row >> return M.empty
390+ inferRowProperties nrow row [] = unifyTypes nrow row >> return M.empty
360 inferRowProperties nrow row ((name, binder):binders) = do
391 inferRowProperties nrow row ((name, binder):binders) = do
361− propTy <- fresh
392+ propTy <- freshType
362 m1 <- inferBinder propTy binder
393 m1 <- inferBinder propTy binder
363 m2 <- inferRowProperties nrow (RCons name propTy row) binders
394 m2 <- inferRowProperties nrow (RCons name propTy row) binders
364 return $ m1 `M.union` m2
395 return $ m1 `M.union` m2
365inferBinder val (ArrayBinder binders) = do
396inferBinder val (ArrayBinder binders) = do
366− el <- fresh
397+ el <- freshType
367 m1 <- M.unions <$> traverse (inferBinder el) binders
398 m1 <- M.unions <$> traverse (inferBinder el) binders
368− val =?= TypeApp tyArray el
399+ unifyTypes val (TypeApp tyArray el)
369 return m1
400 return m1
370inferBinder val (NamedBinder name binder) = do
401inferBinder val (NamedBinder name binder) = do
371 m <- inferBinder val binder
402 m <- inferBinder val binder
@@ -377,9 +408,9 @@ inferBinder val (PositionedBinder pos _ binder) =
377-- and use `kindOfWithScopedVars`.
408-- and use `kindOfWithScopedVars`.
378inferBinder val (TypedBinder ty binder) = do
409inferBinder val (TypedBinder ty binder) = do
379 ty1 <- replaceAllTypeSynonyms <=< replaceTypeWildcards $ ty
410 ty1 <- replaceAllTypeSynonyms <=< replaceTypeWildcards $ ty
380− kind <- liftCheck $ kindOf ty1
411+ kind <- kindOf ty1
381 checkTypeKind ty1 kind
412 checkTypeKind ty1 kind
382− val =?= ty1
413+ unifyTypes val ty1
383 inferBinder val binder
414 inferBinder val binder
384
415
385-- | Returns true if a binder requires its argument type to be a monotype.
416-- | Returns true if a binder requires its argument type to be a monotype.
@@ -392,7 +423,11 @@ binderRequiresMonotype (PositionedBinder _ _ b) = binderRequiresMonotype b
392binderRequiresMonotype _ = True
423binderRequiresMonotype _ = True
393
424
394-- | Instantiate polytypes only when necessitated by a binder.
425-- | Instantiate polytypes only when necessitated by a binder.
395−instantiateForBinders :: [Expr] -> [CaseAlternative] -> UnifyT Type Check ([Expr], [Type])
426+instantiateForBinders ::
427+ (Functor m, Applicative m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
428+ [Expr] ->
429+ [CaseAlternative] ->
430+ m ([Expr], [Type])
396instantiateForBinders vals cas = unzip <$> zipWithM (\val inst -> do
431instantiateForBinders vals cas = unzip <$> zipWithM (\val inst -> do
397 TypedValue _ val' ty <- infer val
432 TypedValue _ val' ty <- infer val
398 if inst
433 if inst
@@ -405,7 +440,12 @@ instantiateForBinders vals cas = unzip <$> zipWithM (\val inst -> do
405-- |
440-- |
406-- Check the types of the return values in a set of binders in a case statement
441-- Check the types of the return values in a set of binders in a case statement
407--
442--
408−checkBinders :: [Type] -> Type -> [CaseAlternative] -> UnifyT Type Check [CaseAlternative]
443+checkBinders ::
444+ (Functor m, Applicative m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
445+ [Type] ->
446+ Type ->
447+ [CaseAlternative] ->
448+ m [CaseAlternative]
409checkBinders _ _ [] = return []
449checkBinders _ _ [] = return []
410checkBinders nvals ret (CaseAlternative binders result : bs) = do
450checkBinders nvals ret (CaseAlternative binders result : bs) = do
411 guardWith (errorMessage $ OverlappingArgNames Nothing) $
451 guardWith (errorMessage $ OverlappingArgNames Nothing) $
@@ -430,13 +470,21 @@ checkBinders nvals ret (CaseAlternative binders result : bs) = do
430-- |
470-- |
431-- Check the type of a value, rethrowing errors to provide a better error message
471-- Check the type of a value, rethrowing errors to provide a better error message
432--
472--
433−check :: Expr -> Type -> UnifyT Type Check Expr
473+check ::
474+ (Functor m, Applicative m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
475+ Expr ->
476+ Type ->
477+ m Expr
434check val ty = rethrow (addHint (ErrorCheckingType val ty)) $ check' val ty
478check val ty = rethrow (addHint (ErrorCheckingType val ty)) $ check' val ty
435
479
436-- |
480-- |
437-- Check the type of a value
481-- Check the type of a value
438--
482--
439−check' :: Expr -> Type -> UnifyT Type Check Expr
483+check' :: forall m.
484+ (Functor m, Applicative m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
485+ Expr ->
486+ Type ->
487+ m Expr
440check' val (ForAll ident ty _) = do
488check' val (ForAll ident ty _) = do
441 scope <- newSkolemScope
489 scope <- newSkolemScope
442 sko <- newSkolemConstant
490 sko <- newSkolemConstant
@@ -446,15 +494,15 @@ check' val (ForAll ident ty _) = do
446 return $ TypedValue True val' (ForAll ident ty (Just scope))
494 return $ TypedValue True val' (ForAll ident ty (Just scope))
447check' val t@(ConstrainedType constraints ty) = do
495check' val t@(ConstrainedType constraints ty) = do
448 dictNames <- forM constraints $ \(Qualified _ (ProperName className), _) -> do
496 dictNames <- forM constraints $ \(Qualified _ (ProperName className), _) -> do
449− n <- liftCheck freshDictionaryName
497+ n <- freshDictionaryName
450 return $ Ident $ "__dict_" ++ className ++ "_" ++ show n
498 return $ Ident $ "__dict_" ++ className ++ "_" ++ show n
451− dicts <- join <$> liftCheck (zipWithM (newDictionaries []) (map (Qualified Nothing) dictNames) constraints)
499+ dicts <- join <$> zipWithM (newDictionaries []) (map (Qualified Nothing) dictNames) constraints
452 val' <- withBindingGroupVisible $ withTypeClassDictionaries dicts $ check val ty
500 val' <- withBindingGroupVisible $ withTypeClassDictionaries dicts $ check val ty
453 return $ TypedValue True (foldr (Abs . Left) val' dictNames) t
501 return $ TypedValue True (foldr (Abs . Left) val' dictNames) t
454 where
502 where
455 -- | Add a dictionary for the constraint to the scope, and dictionaries
503 -- | Add a dictionary for the constraint to the scope, and dictionaries
456− -- for all implies superclass instances.
504+ -- for all implied superclass instances.
457− newDictionaries :: [(Qualified ProperName, Integer)] -> Qualified Ident -> (Qualified ProperName, [Type]) -> Check [TypeClassDictionaryInScope]
505+ newDictionaries :: [(Qualified ProperName, Integer)] -> Qualified Ident -> (Qualified ProperName, [Type]) -> m [TypeClassDictionaryInScope]
458 newDictionaries path name (className, instanceTy) = do
506 newDictionaries path name (className, instanceTy) = do
459 tcs <- gets (typeClasses . checkEnv)
507 tcs <- gets (typeClasses . checkEnv)
460 let (args, _, superclasses) = fromMaybe (internalError "newDictionaries: type class lookup failed") $ M.lookup className tcs
508 let (args, _, superclasses) = fromMaybe (internalError "newDictionaries: type class lookup failed") $ M.lookup className tcs
@@ -471,7 +519,7 @@ check' val u@(TUnknown _) = do
471 val'@(TypedValue _ _ ty) <- infer val
519 val'@(TypedValue _ _ ty) <- infer val
472 -- Don't unify an unknown with an inferred polytype
520 -- Don't unify an unknown with an inferred polytype
473 (val'', ty') <- instantiatePolyTypeWithUnknowns val' ty
521 (val'', ty') <- instantiatePolyTypeWithUnknowns val' ty
474− ty' =?= u
522+ unifyTypes ty' u
475 return $ TypedValue True val'' ty'
523 return $ TypedValue True val'' ty'
476check' v@(NumericLiteral (Left _)) t | t == tyInt =
524check' v@(NumericLiteral (Left _)) t | t == tyInt =
477 return $ TypedValue True v t
525 return $ TypedValue True v t
@@ -484,11 +532,11 @@ check' v@(CharLiteral _) t | t == tyChar =
484check' v@(BooleanLiteral _) t | t == tyBoolean =
532check' v@(BooleanLiteral _) t | t == tyBoolean =
485 return $ TypedValue True v t
533 return $ TypedValue True v t
486check' (ArrayLiteral vals) t@(TypeApp a ty) = do
534check' (ArrayLiteral vals) t@(TypeApp a ty) = do
487− a =?= tyArray
535+ unifyTypes a tyArray
488 array <- ArrayLiteral <$> forM vals (`check` ty)
536 array <- ArrayLiteral <$> forM vals (`check` ty)
489 return $ TypedValue True array t
537 return $ TypedValue True array t
490check' (Abs (Left arg) ret) ty@(TypeApp (TypeApp t argTy) retTy) = do
538check' (Abs (Left arg) ret) ty@(TypeApp (TypeApp t argTy) retTy) = do
491− t =?= tyFunction
539+ unifyTypes t tyFunction
492 Just moduleName <- checkCurrentModule <$> get
540 Just moduleName <- checkCurrentModule <$> get
493 ret' <- withBindingGroupVisible $ bindLocalVariables moduleName [(arg, argTy, Defined)] $ check ret retTy
541 ret' <- withBindingGroupVisible $ bindLocalVariables moduleName [(arg, argTy, Defined)] $ check ret retTy
494 return $ TypedValue True (Abs (Left arg) ret') ty
542 return $ TypedValue True (Abs (Left arg) ret') ty
@@ -517,7 +565,7 @@ check' (SuperClassDictionary className tys) _ = do
517 return $ TypeClassDictionary (className, tys) dicts
565 return $ TypeClassDictionary (className, tys) dicts
518check' (TypedValue checkType val ty1) ty2 = do
566check' (TypedValue checkType val ty1) ty2 = do
519 Just moduleName <- checkCurrentModule <$> get
567 Just moduleName <- checkCurrentModule <$> get
520− (kind, args) <- liftCheck $ kindOfWithScopedVars ty1
568+ (kind, args) <- kindOfWithScopedVars ty1
521 checkTypeKind ty1 kind
569 checkTypeKind ty1 kind
522 ty1' <- introduceSkolemScope <=< replaceAllTypeSynonyms <=< replaceTypeWildcards $ ty1
570 ty1' <- introduceSkolemScope <=< replaceAllTypeSynonyms <=< replaceTypeWildcards $ ty1
523 ty2' <- introduceSkolemScope <=< replaceAllTypeSynonyms <=< replaceTypeWildcards $ ty2
571 ty2' <- introduceSkolemScope <=< replaceAllTypeSynonyms <=< replaceTypeWildcards $ ty2
@@ -549,12 +597,12 @@ check' e@(ObjectUpdate obj ps) t@(TypeApp o row) | o == tyObject = do
549 -- We check _obj_ against the type _t_ with the types in _ps_ replaced with unknowns.
597 -- We check _obj_ against the type _t_ with the types in _ps_ replaced with unknowns.
550 let (propsToCheck, rest) = rowToList row
598 let (propsToCheck, rest) = rowToList row
551 (removedProps, remainingProps) = partition (\(p, _) -> p `elem` map fst ps) propsToCheck
599 (removedProps, remainingProps) = partition (\(p, _) -> p `elem` map fst ps) propsToCheck
552− us <- zip (map fst removedProps) <$> replicateM (length ps) fresh
600+ us <- zip (map fst removedProps) <$> replicateM (length ps) freshType
553 obj' <- check obj (TypeApp tyObject (rowFromList (us ++ remainingProps, rest)))
601 obj' <- check obj (TypeApp tyObject (rowFromList (us ++ remainingProps, rest)))
554 ps' <- checkProperties e ps row True
602 ps' <- checkProperties e ps row True
555 return $ TypedValue True (ObjectUpdate obj' ps') t
603 return $ TypedValue True (ObjectUpdate obj' ps') t
556check' (Accessor prop val) ty = rethrow (addHint (ErrorCheckingAccessor val prop)) $ do
604check' (Accessor prop val) ty = rethrow (addHint (ErrorCheckingAccessor val prop)) $ do
557− rest <- fresh
605+ rest <- freshType
558 val' <- check val (TypeApp tyObject (RCons prop ty rest))
606 val' <- check val (TypeApp tyObject (RCons prop ty rest))
559 return $ TypedValue True (Accessor prop val') ty
607 return $ TypedValue True (Accessor prop val') ty
560check' v@(Constructor c) ty = do
608check' v@(Constructor c) ty = do
@@ -588,12 +636,18 @@ check' val ty = do
588--
636--
589-- The @lax@ parameter controls whether or not every record member has to be provided. For object updates, this is not the case.
637-- The @lax@ parameter controls whether or not every record member has to be provided. For object updates, this is not the case.
590--
638--
591−checkProperties :: Expr -> [(String, Expr)] -> Type -> Bool -> UnifyT Type Check [(String, Expr)]
639+checkProperties ::
640+ (Functor m, Applicative m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
641+ Expr ->
642+ [(String, Expr)] ->
643+ Type ->
644+ Bool ->
645+ m [(String, Expr)]
592checkProperties expr ps row lax = let (ts, r') = rowToList row in go ps ts r' where
646checkProperties expr ps row lax = let (ts, r') = rowToList row in go ps ts r' where
593 go [] [] REmpty = return []
647 go [] [] REmpty = return []
594 go [] [] u@(TUnknown _)
648 go [] [] u@(TUnknown _)
595 | lax = return []
649 | lax = return []
596− | otherwise = do u =?= REmpty
650+ | otherwise = do unifyTypes u REmpty
597 return []
651 return []
598 go [] [] Skolem{} | lax = return []
652 go [] [] Skolem{} | lax = return []
599 go [] ((p, _): _) _ | lax = return []
653 go [] ((p, _): _) _ | lax = return []
@@ -603,8 +657,8 @@ checkProperties expr ps row lax = let (ts, r') = rowToList row in go ps ts r' wh
603 case lookup p ts of
657 case lookup p ts of
604 Nothing -> do
658 Nothing -> do
605 v'@(TypedValue _ _ ty) <- infer v
659 v'@(TypedValue _ _ ty) <- infer v
606− rest <- fresh
660+ rest <- freshType
607− r =?= RCons p ty rest
661+ unifyTypes r (RCons p ty rest)
608 ps'' <- go ps' ts rest
662 ps'' <- go ps' ts rest
609 return $ (p, v') : ps''
663 return $ (p, v') : ps''
610 Just ty -> do
664 Just ty -> do
@@ -613,20 +667,28 @@ checkProperties expr ps row lax = let (ts, r') = rowToList row in go ps ts r' wh
613 return $ (p, v') : ps''
667 return $ (p, v') : ps''
614 go _ _ _ = throwError . errorMessage $ ExprDoesNotHaveType expr (TypeApp tyObject row)
668 go _ _ _ = throwError . errorMessage $ ExprDoesNotHaveType expr (TypeApp tyObject row)
615
669
616−-- |
617−-- Check the type of a function application, rethrowing errors to provide a better error message
670+-- | Check the type of a function application, rethrowing errors to provide a better error message
618−--
619−checkFunctionApplication :: Expr -> Type -> Expr -> Maybe Type -> UnifyT Type Check (Type, Expr)
671+checkFunctionApplication ::
672+ (Functor m, Applicative m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
673+ Expr ->
674+ Type ->
675+ Expr ->
676+ Maybe Type ->
677+ m (Type, Expr)
620checkFunctionApplication fn fnTy arg ret = rethrow (addHint (ErrorInApplication fn fnTy arg)) $ do
678checkFunctionApplication fn fnTy arg ret = rethrow (addHint (ErrorInApplication fn fnTy arg)) $ do
621− subst <- unifyCurrentSubstitution <$> UnifyT get
679+ subst <- gets checkSubstitution
622− checkFunctionApplication' fn (subst $? fnTy) arg (($?) subst <$> ret)
680+ checkFunctionApplication' fn (substituteType subst fnTy) arg (substituteType subst <$> ret)
623−
681+
624−-- |
625−-- Check the type of a function application
682+-- | Check the type of a function application
626−--
627−checkFunctionApplication' :: Expr -> Type -> Expr -> Maybe Type -> UnifyT Type Check (Type, Expr)
683+checkFunctionApplication' ::
684+ (Functor m, Applicative m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
685+ Expr ->
686+ Type ->
687+ Expr ->
688+ Maybe Type ->
689+ m (Type, Expr)
628checkFunctionApplication' fn (TypeApp (TypeApp tyFunction' argTy) retTy) arg ret = do
690checkFunctionApplication' fn (TypeApp (TypeApp tyFunction' argTy) retTy) arg ret = do
629− tyFunction' =?= tyFunction
691+ unifyTypes tyFunction' tyFunction
630 arg' <- check arg argTy
692 arg' <- check arg argTy
631 case ret of
693 case ret of
632 Nothing -> return (retTy, App fn arg')
694 Nothing -> return (retTy, App fn arg')
@@ -642,8 +704,8 @@ checkFunctionApplication' fn u@(TUnknown _) arg ret = do
642 (arg'', t') <- instantiatePolyTypeWithUnknowns arg' t
704 (arg'', t') <- instantiatePolyTypeWithUnknowns arg' t
643 return $ TypedValue True arg'' t'
705 return $ TypedValue True arg'' t'
644 let ty = (\(TypedValue _ _ t) -> t) arg'
706 let ty = (\(TypedValue _ _ t) -> t) arg'
645− ret' <- maybe fresh return ret
707+ ret' <- maybe freshType return ret
646− u =?= function ty ret'
708+ unifyTypes u (function ty ret')
647 return (ret', App fn arg')
709 return (ret', App fn arg')
648checkFunctionApplication' fn (KindedType ty _) arg ret =
710checkFunctionApplication' fn (KindedType ty _) arg ret =
649 checkFunctionApplication fn ty arg ret
711 checkFunctionApplication fn ty arg ret
@@ -654,11 +716,15 @@ checkFunctionApplication' fn fnTy dict@TypeClassDictionary{} _ =
654 return (fnTy, App fn dict)
716 return (fnTy, App fn dict)
655checkFunctionApplication' _ fnTy arg _ = throwError . errorMessage $ CannotApplyFunction fnTy arg
717checkFunctionApplication' _ fnTy arg _ = throwError . errorMessage $ CannotApplyFunction fnTy arg
656
718
657−-- |
658−-- Compute the meet of two types, i.e. the most general type which both types subsume.
719+-- | Compute the meet of two types, i.e. the most general type which both types subsume.
659−-- TODO: handle constrained types
720+-- TODO: is this really needed?
660−--
721+meet ::
722+ (Functor m, Applicative m, MonadState CheckState m, MonadError MultipleErrors m) =>
723+ Expr ->
724+ Expr ->
725+ Type ->
726+ Type ->
661−meet :: Expr -> Expr -> Type -> Type -> UnifyT Type Check (Expr, Expr, Type)
727+ m (Expr, Expr, Type)
662meet e1 e2 (ForAll ident t1 _) t2 = do
728meet e1 e2 (ForAll ident t1 _) t2 = do
663 t1' <- replaceVarWithUnknown ident t1
729 t1' <- replaceVarWithUnknown ident t1
664 meet e1 e2 t1' t2
730 meet e1 e2 t1' t2
@@ -666,7 +732,7 @@ meet e1 e2 t1 (ForAll ident t2 _) = do
666 t2' <- replaceVarWithUnknown ident t2
732 t2' <- replaceVarWithUnknown ident t2
667 meet e1 e2 t1 t2'
733 meet e1 e2 t1 t2'
668meet e1 e2 t1 t2 = do
734meet e1 e2 t1 t2 = do
669− t1 =?= t2
735+ unifyTypes t1 t2
670 return (e1, e2, t1)
736 return (e1, e2, t1)
671
737
672-- |
738-- |
src/Language/PureScript/TypeChecker/Unify.hs+76−43
@@ -13,12 +13,16 @@
13--
13--
14-----------------------------------------------------------------------------
14-----------------------------------------------------------------------------
15
15
16−{-# OPTIONS_GHC -fno-warn-orphans #-}
17{-# LANGUAGE FlexibleInstances #-}
16{-# LANGUAGE FlexibleInstances #-}
18{-# LANGUAGE FlexibleContexts #-}
17{-# LANGUAGE FlexibleContexts #-}
19{-# LANGUAGE MultiParamTypeClasses #-}
18{-# LANGUAGE MultiParamTypeClasses #-}
19+{-# LANGUAGE ScopedTypeVariables #-}
20+{-# LANGUAGE CPP #-}
20
21
21module Language.PureScript.TypeChecker.Unify (
22module Language.PureScript.TypeChecker.Unify (
23+ freshType,
24+ solveType,
25+ substituteType,
22 unifyTypes,
26 unifyTypes,
23 unifyRows,
27 unifyRows,
24 unifiesWith,
28 unifiesWith,
@@ -28,13 +32,15 @@ module Language.PureScript.TypeChecker.Unify (
28) where
32) where
29
33
30import Data.List (nub, sort)
34import Data.List (nub, sort)
31−import Data.Maybe (fromMaybe)
32−import qualified Data.HashMap.Strict as H
35+import qualified Data.Map as M
33
36
37+#if __GLASGOW_HASKELL__ < 710
38+import Control.Applicative
39+#endif
34import Control.Monad
40import Control.Monad
35−import Control.Monad.Unify
36−import Control.Monad.Writer
37import Control.Monad.Error.Class (MonadError(..))
41import Control.Monad.Error.Class (MonadError(..))
42+import Control.Monad.Writer.Class (MonadWriter(..))
43+import Control.Monad.State.Class (MonadState(..), gets, modify)
38
44
39import Language.PureScript.Crash
45import Language.PureScript.Crash
40import Language.PureScript.Errors
46import Language.PureScript.Errors
@@ -42,32 +48,59 @@ import Language.PureScript.TypeChecker.Monad
42import Language.PureScript.TypeChecker.Skolems
48import Language.PureScript.TypeChecker.Skolems
43import Language.PureScript.Types
49import Language.PureScript.Types
44
50
45−instance Partial Type where
51+-- | Generate a fresh type variable
46− unknown = TUnknown
52+freshType :: (MonadState CheckState m) => m Type
47− isUnknown (TUnknown u) = Just u
53+freshType = do
48− isUnknown _ = Nothing
54+ t <- gets checkNextType
49− unknowns = everythingOnTypes (++) go
55+ modify $ \st -> st { checkNextType = t + 1 }
50− where
56+ return $ TUnknown t
51− go (TUnknown u) = [u]
52− go _ = []
53− ($?) sub = everywhereOnTypes go
54− where
55− go t@(TUnknown u) = fromMaybe t $ H.lookup u (runSubstitution sub)
56− go other = other
57−
58−instance Unifiable Check Type where
59− (=?=) = unifyTypes
60
57
61−-- |
58+-- | Update the substitution to solve a type constraint
59+solveType :: (Functor m, Applicative m, MonadError MultipleErrors m, MonadState CheckState m) => Int -> Type -> m ()
60+solveType u t = do
61+ occursCheck u t
62+ modify $ \cs -> cs { checkSubstitution =
63+ (checkSubstitution cs) { substType =
64+ M.insert u t $ substType $ checkSubstitution cs
65+ }
66+ }
67+
68+-- | Apply a substitution to a type
69+substituteType :: Substitution -> Type -> Type
70+substituteType sub = everywhereOnTypes go
71+ where
72+ go (TUnknown u) =
73+ case M.lookup u (substType sub) of
74+ Nothing -> TUnknown u
75+ Just (TUnknown u1) | u1 == u -> TUnknown u1
76+ Just t -> substituteType sub t
77+ go other = other
78+
79+-- | Make sure that an unknown does not occur in a type
80+occursCheck :: (Functor m, Applicative m, MonadError MultipleErrors m) => Int -> Type -> m ()
81+occursCheck _ TUnknown{} = return ()
82+occursCheck u t = void $ everywhereOnTypesM go t
83+ where
84+ go (TUnknown u') | u == u' = throwError . errorMessage . InfiniteType $ t
85+ go other = return other
86+
87+-- | Compute a list of all unknowns appearing in a type
88+unknownsInType :: Type -> [Int]
89+unknownsInType t = everythingOnTypes (.) go t []
90+ where
91+ go :: Type -> [Int] -> [Int]
92+ go (TUnknown u) = (u :)
93+ go _ = id
94+
62−-- Unify two types, updating the current substitution
95+-- | Unify two types, updating the current substitution
63−--
96+unifyTypes :: (Functor m, Applicative m, MonadError MultipleErrors m, MonadState CheckState m) => Type -> Type -> m ()
64−unifyTypes :: Type -> Type -> UnifyT Type Check ()
97+unifyTypes t1 t2 = do
98+ sub <- gets checkSubstitution
65−unifyTypes t1 t2 = rethrow (addHint (ErrorUnifyingTypes t1 t2)) $
99+ rethrow (addHint (ErrorUnifyingTypes t1 t2)) $ unifyTypes' (substituteType sub t1) (substituteType sub t2)
66− unifyTypes' t1 t2
67 where
100 where
68 unifyTypes' (TUnknown u1) (TUnknown u2) | u1 == u2 = return ()
101 unifyTypes' (TUnknown u1) (TUnknown u2) | u1 == u2 = return ()
69− unifyTypes' (TUnknown u) t = u =:= t
102+ unifyTypes' (TUnknown u) t = solveType u t
70− unifyTypes' t (TUnknown u) = u =:= t
103+ unifyTypes' t (TUnknown u) = solveType u t
71 unifyTypes' (ForAll ident1 ty1 sc1) (ForAll ident2 ty2 sc2) =
104 unifyTypes' (ForAll ident1 ty1 sc1) (ForAll ident2 ty2 sc2) =
72 case (sc1, sc2) of
105 case (sc1, sc2) of
73 (Just sc1', Just sc2') -> do
106 (Just sc1', Just sc2') -> do
@@ -106,7 +139,7 @@ unifyTypes t1 t2 = rethrow (addHint (ErrorUnifyingTypes t1 t2)) $
106-- trailing row unification variable, if appropriate, otherwise leftover labels result in a unification
139-- trailing row unification variable, if appropriate, otherwise leftover labels result in a unification
107-- error.
140-- error.
108--
141--
109−unifyRows :: Type -> Type -> UnifyT Type Check ()
142+unifyRows :: forall m. (Functor m, Applicative m, MonadError MultipleErrors m, MonadState CheckState m) => Type -> Type -> m ()
110unifyRows r1 r2 =
143unifyRows r1 r2 =
111 let
144 let
112 (s1, r1') = rowToList r1
145 (s1, r1') = rowToList r1
@@ -115,18 +148,18 @@ unifyRows r1 r2 =
115 sd1 = [ (name, t1) | (name, t1) <- s1, name `notElem` map fst s2 ]
148 sd1 = [ (name, t1) | (name, t1) <- s1, name `notElem` map fst s2 ]
116 sd2 = [ (name, t2) | (name, t2) <- s2, name `notElem` map fst s1 ]
149 sd2 = [ (name, t2) | (name, t2) <- s2, name `notElem` map fst s1 ]
117 in do
150 in do
118− forM_ int (uncurry (=?=))
151+ forM_ int (uncurry unifyTypes)
119 unifyRows' sd1 r1' sd2 r2'
152 unifyRows' sd1 r1' sd2 r2'
120 where
153 where
121− unifyRows' :: [(String, Type)] -> Type -> [(String, Type)] -> Type -> UnifyT Type Check ()
154+ unifyRows' :: [(String, Type)] -> Type -> [(String, Type)] -> Type -> m ()
122− unifyRows' [] (TUnknown u) sd r = u =:= rowFromList (sd, r)
155+ unifyRows' [] (TUnknown u) sd r = solveType u (rowFromList (sd, r))
123− unifyRows' sd r [] (TUnknown u) = u =:= rowFromList (sd, r)
156+ unifyRows' sd r [] (TUnknown u) = solveType u (rowFromList (sd, r))
124 unifyRows' sd1 (TUnknown u1) sd2 (TUnknown u2) = do
157 unifyRows' sd1 (TUnknown u1) sd2 (TUnknown u2) = do
125 forM_ sd1 $ \(_, t) -> occursCheck u2 t
158 forM_ sd1 $ \(_, t) -> occursCheck u2 t
126 forM_ sd2 $ \(_, t) -> occursCheck u1 t
159 forM_ sd2 $ \(_, t) -> occursCheck u1 t
127− rest <- fresh
160+ rest <- freshType
128− u1 =:= rowFromList (sd2, rest)
161+ solveType u1 (rowFromList (sd2, rest))
129− u2 =:= rowFromList (sd1, rest)
162+ solveType u2 (rowFromList (sd1, rest))
130 unifyRows' [] REmpty [] REmpty = return ()
163 unifyRows' [] REmpty [] REmpty = return ()
131 unifyRows' [] (TypeVar v1) [] (TypeVar v2) | v1 == v2 = return ()
164 unifyRows' [] (TypeVar v1) [] (TypeVar v2) | v1 == v2 = return ()
132 unifyRows' [] (Skolem _ s1 _) [] (Skolem _ s2 _) | s1 == s2 = return ()
165 unifyRows' [] (Skolem _ s1 _) [] (Skolem _ s2 _) | s1 == s2 = return ()
@@ -164,21 +197,21 @@ unifiesWith _ _ = False
164-- |
197-- |
165-- Replace a single type variable with a new unification variable
198-- Replace a single type variable with a new unification variable
166--
199--
167−replaceVarWithUnknown :: String -> Type -> UnifyT Type Check Type
200+replaceVarWithUnknown :: (MonadState CheckState m) => String -> Type -> m Type
168replaceVarWithUnknown ident ty = do
201replaceVarWithUnknown ident ty = do
169− tu <- fresh
202+ tu <- freshType
170 return $ replaceTypeVars ident tu ty
203 return $ replaceTypeVars ident tu ty
171
204
172-- |
205-- |
173-- Replace type wildcards with unknowns
206-- Replace type wildcards with unknowns
174--
207--
175−replaceTypeWildcards :: Type -> UnifyT t Check Type
208+replaceTypeWildcards :: (Functor m, Applicative m, MonadWriter MultipleErrors m, MonadState CheckState m) => Type -> m Type
176replaceTypeWildcards = everywhereOnTypesM replace
209replaceTypeWildcards = everywhereOnTypesM replace
177 where
210 where
178 replace TypeWildcard = do
211 replace TypeWildcard = do
179− u <- fresh'
212+ t <- freshType
180− liftCheck . tell $ errorMessage . WildcardInferredType $ TUnknown u
213+ tell . errorMessage $ WildcardInferredType t
181− return $ TUnknown u
214+ return t
182 replace other = return other
215 replace other = return other
183
216
184-- |
217-- |
@@ -186,7 +219,7 @@ replaceTypeWildcards = everywhereOnTypesM replace
186--
219--
187varIfUnknown :: Type -> Type
220varIfUnknown :: Type -> Type
188varIfUnknown ty =
221varIfUnknown ty =
189− let unks = nub $ unknowns ty
222+ let unks = nub $ unknownsInType ty
190 toName = (:) 't' . show
223 toName = (:) 't' . show
191 ty' = everywhereOnTypes typeToVar ty
224 ty' = everywhereOnTypes typeToVar ty
192 typeToVar :: Type -> Type
225 typeToVar :: Type -> Type
src/Language/PureScript/Types.hs+1−2
@@ -28,7 +28,6 @@ import Data.Maybe (fromMaybe)
28import qualified Data.Aeson as A
28import qualified Data.Aeson as A
29import qualified Data.Aeson.TH as A
29import qualified Data.Aeson.TH as A
30
30
31−import Control.Monad.Unify
32import Control.Arrow (second)
31import Control.Arrow (second)
33import Control.Monad ((<=<))
32import Control.Monad ((<=<))
34
33
@@ -48,7 +47,7 @@ data Type
48 -- |
47 -- |
49 -- A unification variable of type Type
48 -- A unification variable of type Type
50 --
49 --
51− = TUnknown Unknown
50+ = TUnknown Int
52 -- |
51 -- |
53 -- A named type variable
52 -- A named type variable
54 --
53 --