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