git.iko.soy/rowtype-yoga/purescript-native
on golang help sign in
Progress on RankNTypes
8d75f74Phil Freeman
examples/passing/Rank2Types.psnew file+10
compare with golang
unifiedsplit
@@ -0,0 +1,10 @@
1+test1 :: (forall a. (a -> a)) -> Number
2+test1 = \f -> f 0
3+
4+foreign import data ST :: * -> * -> *
5+
6+foreign import runST :: forall a. (forall s. ST s a) -> a
7+
8+foreign import exampleST :: forall s. ST s Number
9+
10+testST = runST exampleST
src/Language/PureScript.hs+1−1
@@ -32,7 +32,7 @@ import Data.Maybe (mapMaybe)
32compile :: [Declaration] -> Either String (String, String, Environment)
32compile :: [Declaration] -> Either String (String, String, Environment)
33compile decls = do
33compile decls = do
34 bracketted <- rebracket decls
34 bracketted <- rebracket decls
35− (_, env) <- check (typeCheckAll bracketted)
35+ (_, env) <- runCheck (typeCheckAll bracketted)
36 let js = prettyPrintJS . map optimize . concat . mapMaybe (\decl -> declToJs Nothing global decl env) $ bracketted
36 let js = prettyPrintJS . map optimize . concat . mapMaybe (\decl -> declToJs Nothing global decl env) $ bracketted
37 let exts = intercalate "\n" . mapMaybe (externToPs 0 global env) $ bracketted
37 let exts = intercalate "\n" . mapMaybe (externToPs 0 global env) $ bracketted
38 return (js, exts, env)
38 return (js, exts, env)
src/Language/PureScript/Kinds.hs+2−1
@@ -17,9 +17,10 @@
17module Language.PureScript.Kinds where
17module Language.PureScript.Kinds where
18
18
19import Data.Data
19import Data.Data
20+import Language.PureScript.Unknown
20
21
21data Kind
22data Kind
22− = KUnknown Int
23+ = KUnknown (Unknown Kind)
23 | Star
24 | Star
24 | Row
25 | Row
25 | FunKind Kind Kind deriving (Show, Eq, Data, Typeable)
26 | FunKind Kind Kind deriving (Show, Eq, Data, Typeable)
src/Language/PureScript/TypeChecker.hs+1−1
@@ -76,7 +76,7 @@ typeCheckAll (ValueDeclaration name val : rest) = do
76 case M.lookup (modulePath, name) (names env) of
76 case M.lookup (modulePath, name) (names env) of
77 Just ty -> throwError $ show name ++ " is already defined"
77 Just ty -> throwError $ show name ++ " is already defined"
78 Nothing -> do
78 Nothing -> do
79− ty <- typeOf name val
79+ ty <- typeOf (Just name) val
80 putEnv (env { names = M.insert (modulePath, name) (ty, Value) (names env) })
80 putEnv (env { names = M.insert (modulePath, name) (ty, Value) (names env) })
81 typeCheckAll rest
81 typeCheckAll rest
82typeCheckAll (ExternDataDeclaration name kind : rest) = do
82typeCheckAll (ExternDataDeclaration name kind : rest) = do
src/Language/PureScript/TypeChecker/Kinds.hs+79−132
@@ -15,8 +15,6 @@
15{-# LANGUAGE DeriveDataTypeable #-}
15{-# LANGUAGE DeriveDataTypeable #-}
16
16
17module Language.PureScript.TypeChecker.Kinds (
17module Language.PureScript.TypeChecker.Kinds (
18− KindConstraint(..),
19− KindSolution(..),
20 kindsOf,
18 kindsOf,
21 kindOf
19 kindOf
22) where
20) where
@@ -32,6 +30,7 @@ import Language.PureScript.Names
32import Language.PureScript.Declarations
30import Language.PureScript.Declarations
33import Language.PureScript.TypeChecker.Monad
31import Language.PureScript.TypeChecker.Monad
34import Language.PureScript.Pretty
32import Language.PureScript.Pretty
33+import Language.PureScript.Unknown
35
34
36import Control.Monad.State
35import Control.Monad.State
37import Control.Monad.Error
36import Control.Monad.Error
@@ -42,148 +41,96 @@ import qualified Control.Category as C
42
41
43import qualified Data.Map as M
42import qualified Data.Map as M
44
43
45−data KindConstraintOrigin
44+instance Unifiable Kind where
46− = DataDeclOrigin
45+ unknown = KUnknown
47− | TypeOrigin Type
46+ isUnknown (KUnknown u) = Just u
48− | RowOrigin Row deriving (Show, Data, Typeable)
47+ isUnknown _ = Nothing
49−
48+ KUnknown u1 ~~ KUnknown u2 | u1 == u2 = return ()
50−prettyPrintKindConstraintOrigin :: KindConstraintOrigin -> String
49+ KUnknown u ~~ k = replace u k
51−prettyPrintKindConstraintOrigin (DataDeclOrigin) = "data declaration"
50+ k ~~ KUnknown u = replace u k
52−prettyPrintKindConstraintOrigin (TypeOrigin ty) = prettyPrintType ty
51+ Star ~~ Star = return ()
53−prettyPrintKindConstraintOrigin (RowOrigin row) = prettyPrintRow row
52+ Row ~~ Row = return ()
54−
53+ FunKind k1 k2 ~~ FunKind k3 k4 = do
55−data KindConstraint = KindConstraint Int Kind KindConstraintOrigin deriving (Show, Data, Typeable)
54+ k1 ~~ k3
56−
55+ k2 ~~ k4
57−newtype KindSolution = KindSolution { runKindSolution :: Int -> Kind }
56+ k1 ~~ k2 = throwError $ "Cannot unify " ++ prettyPrintKind k1 ++ " with " ++ prettyPrintKind k2 ++ "."
58−
57+ apply s (KUnknown u) = runSubstitution s u
59−emptyKindSolution :: KindSolution
58+ apply s (FunKind k1 k2) = FunKind (apply s k1) (apply s k2)
60−emptyKindSolution = KindSolution KUnknown
59+ apply _ k = k
60+ unknowns (KUnknown (Unknown u)) = [u]
61+ unknowns (FunKind k1 k2) = unknowns k1 ++ unknowns k2
62+ unknowns _ = []
61
63
62kindOf :: Type -> Check Kind
64kindOf :: Type -> Check Kind
63−kindOf ty = do
65+kindOf ty = runSubst $ starIfUnknown <$> infer Nothing M.empty ty
64− (cs, n, m) <- kindConstraints Nothing M.empty ty
65− solution <- solveKindConstraints cs emptyKindSolution
66− return $ starIfUnknown $ runKindSolution solution n
67
66
68kindsOf :: Maybe ProperName -> [String] -> [Type] -> Check Kind
67kindsOf :: Maybe ProperName -> [String] -> [Type] -> Check Kind
69−kindsOf name args ts = do
68+kindsOf name args ts = runSubst $ do
70 tyCon <- fresh
69 tyCon <- fresh
71− nargs <- replicateM (length args) fresh
70+ kargs <- replicateM (length args) fresh
72− (cs, ns, m) <- kindConstraintsAll (fmap (\pn -> (pn, tyCon)) name) (M.fromList (zip args nargs)) ts
71+ ks <- inferAll (fmap (\pn -> (pn, tyCon)) name) (M.fromList (zip args kargs)) ts
73− let extraConstraints =
72+ tyCon ~~ foldr FunKind Star kargs
74− KindConstraint tyCon (foldr (FunKind . KUnknown) Star nargs) DataDeclOrigin
73+ forM_ ks $ \k -> k ~~ Star
75− : zipWith (\n arg -> KindConstraint n Star (TypeOrigin arg)) ns ts
76− solution <- solveKindConstraints (extraConstraints ++ cs) emptyKindSolution
77− return $ starIfUnknown $ runKindSolution solution tyCon
74+ return $ starIfUnknown tyCon
78
75
79starIfUnknown :: Kind -> Kind
76starIfUnknown :: Kind -> Kind
80starIfUnknown (KUnknown _) = Star
77starIfUnknown (KUnknown _) = Star
81starIfUnknown (FunKind k1 k2) = FunKind (starIfUnknown k1) (starIfUnknown k2)
78starIfUnknown (FunKind k1 k2) = FunKind (starIfUnknown k1) (starIfUnknown k2)
82starIfUnknown k = k
79starIfUnknown k = k
83
80
84−kindConstraintsAll :: Maybe (ProperName, Int) -> M.Map String Int -> [Type] -> Check ([KindConstraint], [Int], M.Map String Int)
81+inferAll :: Maybe (ProperName, Kind) -> M.Map String Kind -> [Type] -> Subst Check [Kind]
85−kindConstraintsAll _ m [] = return ([], [], m)
82+inferAll _ _ [] = return []
86−kindConstraintsAll name m (t:ts) = do
83+inferAll name m (t:ts) = do
87− (cs, n1, m') <- kindConstraints name m t
84+ k <- infer name m t
88− (cs', ns, m'') <- kindConstraintsAll name m' ts
85+ ks <- inferAll name m ts
89− return (KindConstraint n1 Star (TypeOrigin t) : cs ++ cs', n1:ns, m'')
86+ return (k:ks)
90−
87+
91−kindConstraints :: Maybe (ProperName, Int) -> M.Map String Int -> Type -> Check ([KindConstraint], Int, M.Map String Int)
88+infer :: Maybe (ProperName, Kind) -> M.Map String Kind -> Type -> Subst Check Kind
92−kindConstraints name m a@(Array t) = do
89+infer name m a@(Array t) = do
93− me <- fresh
90+ k <- infer name m t
94− (cs, n1, m') <- kindConstraints name m t
91+ k ~~ Star
95− return (KindConstraint n1 Star (TypeOrigin t) : KindConstraint me Star (TypeOrigin a) : cs, me, m')
92+ return Star
96−kindConstraints name m o@(Object row) = do
93+infer name m o@(Object row) = do
97− me <- fresh
94+ k <- inferRow name m row
98− (cs, r, m') <- kindConstraintsForRow name m row
95+ k ~~ Row
99− return (KindConstraint me Star (TypeOrigin o) : KindConstraint r Row (RowOrigin row) : cs, me, m')
96+ return Star
100−kindConstraints name m f@(Function args ret) = do
97+infer name m f@(Function args ret) = do
101− me <- fresh
98+ ks <- inferAll name m args
102− (cs, ns, m') <- kindConstraintsAll name m args
99+ k <- infer name m ret
103− (cs', retN, m'') <- kindConstraints name m' ret
100+ k ~~ Star
104− return (KindConstraint retN Star (TypeOrigin ret) : KindConstraint me Star (TypeOrigin f) : zipWith (\n arg -> KindConstraint n Star (TypeOrigin arg)) ns args ++ cs ++ cs', me, m'')
101+ forM ks $ \k -> k ~~ Star
102+ return Star
105−kindConstraints _ m (TypeVar v) =
103+infer _ m (TypeVar v) =
106 case M.lookup v m of
104 case M.lookup v m of
107− Just u -> return ([], u, m)
105+ Just k -> return k
108 Nothing -> throwError $ "Unbound type variable " ++ v
106 Nothing -> throwError $ "Unbound type variable " ++ v
109−kindConstraints (Just (name, u)) m c@(TypeConstructor v@(Qualified (ModulePath []) pn)) | name == pn = do
107+infer (Just (name, k)) m c@(TypeConstructor v@(Qualified (ModulePath []) pn)) | name == pn = return k
110− env <- getEnv
111− me <- fresh
112− modulePath <- checkModulePath `fmap` get
113− return ([KindConstraint me (KUnknown u) (TypeOrigin c)], me, m)
114−kindConstraints name m c@(TypeConstructor v) = do
108+infer name m c@(TypeConstructor v) = do
115− env <- getEnv
109+ env <- lift getEnv
116− me <- fresh
117− modulePath <- checkModulePath `fmap` get
110+ modulePath <- checkModulePath `fmap` lift get
118 case M.lookup (qualify modulePath v) (types env) of
111 case M.lookup (qualify modulePath v) (types env) of
119 Nothing -> throwError $ "Unknown type constructor '" ++ show v ++ "'"
112 Nothing -> throwError $ "Unknown type constructor '" ++ show v ++ "'"
120− Just (kind, _) -> return ([KindConstraint me kind (TypeOrigin c)], me, m)
113+ Just (kind, _) -> return kind
121−kindConstraints name m a@(TypeApp t1 t2) = do
114+infer name m a@(TypeApp t1 t2) = do
122− me <- fresh
115+ k0 <- fresh
123− (cs1, n1, m1) <- kindConstraints name m t1
116+ k1 <- infer name m t1
124− (cs2, n2, m2) <- kindConstraints name m1 t2
117+ k2 <- infer name m t2
125− return (KindConstraint n1 (FunKind (KUnknown n2) (KUnknown me)) (TypeOrigin a) : cs1 ++ cs2, me, m2)
118+ k1 ~~ FunKind k2 k0
119+ return k0
126−kindConstraints name m (ForAll idents ty) = do
120+infer name m (ForAll idents ty) = do
127− ns <- replicateM (length idents) fresh
121+ ks <- replicateM (length idents) fresh
128− kindConstraints name (M.fromList (zip idents ns) `M.union` m) ty
122+ infer name (M.fromList (zip idents ks) `M.union` m) ty
129−kindConstraints _ m t = do
123+infer _ m t = return Star
130− me <- fresh
124+
131− return ([KindConstraint me Star (TypeOrigin t)], me, m)
132−
133−kindConstraintsForRow :: Maybe (ProperName, Int) -> M.Map String Int -> Row -> Check ([KindConstraint], Int, M.Map String Int)
125+inferRow :: Maybe (ProperName, Kind) -> M.Map String Kind -> Row -> Subst Check Kind
134−kindConstraintsForRow _ m r@(RowVar v) = do
126+inferRow _ m (RowVar v) = do
135− me <- case M.lookup v m of
127+ case M.lookup v m of
136− Just u -> return u
128+ Just k -> return k
137− Nothing -> fresh
129+ Nothing -> throwError $ "Unbound row variable " ++ v
138− return ([KindConstraint me Row (RowOrigin r)], me, M.insert v me m)
130+inferRow _ m r@REmpty = return Row
139−kindConstraintsForRow _ m r@REmpty = do
140− me <- fresh
141− return ([KindConstraint me Row (RowOrigin r)], me, m)
142−kindConstraintsForRow name m r@(RCons _ ty row) = do
131+inferRow name m r@(RCons _ ty row) = do
143− me <- fresh
132+ k1 <- infer name m ty
144− (cs1, n1, m1) <- kindConstraints name m ty
133+ k2 <- inferRow name m row
145− (cs2, n2, m2) <- kindConstraintsForRow name m1 row
134+ k1 ~~ Star
146− return (KindConstraint me Row (RowOrigin r) : KindConstraint n1 Star (TypeOrigin ty) : KindConstraint n2 Row (RowOrigin r) : cs1 ++ cs2, me, m2)
135+ k2 ~~ Row
147−
136+ return Row
148−solveKindConstraints :: [KindConstraint] -> KindSolution -> Check KindSolution
149−solveKindConstraints [] s = return s
150−solveKindConstraints all@(KindConstraint n k t : cs) s = do
151− (cs', s') <- rethrow (\err -> "Error in " ++ prettyPrintKindConstraintOrigin t ++ ": " ++ err) $ do
152− guardWith "Occurs check failed" $ not $ kindOccursCheck False n k
153− let s' = KindSolution $ replaceUnknownKind n k . runKindSolution s
154− cs' <- fmap concat $ mapM (substituteKindConstraint n k) cs
155− return (cs', s')
156− solveKindConstraints cs' s'
157−
158−substituteKindConstraint :: Int -> Kind -> KindConstraint -> Check [KindConstraint]
159−substituteKindConstraint n k (KindConstraint m l t)
160− | n == m = unifyKinds t k l
161− | otherwise = return [KindConstraint m (replaceUnknownKind n k l) t]
162−
163−replaceUnknownKind :: Int -> Kind -> Kind -> Kind
164−replaceUnknownKind n k = f
165− where
166− f (KUnknown m) | m == n = k
167− f (FunKind k1 k2) = FunKind (f k2) (f k2)
168− f other = other
169−
170−unifyKinds :: KindConstraintOrigin -> Kind -> Kind -> Check [KindConstraint]
171−unifyKinds _ (KUnknown u1) (KUnknown u2) | u1 == u2 = return []
172−unifyKinds t (KUnknown u) k = do
173− guardWith "Occurs check failed" $ not $ kindOccursCheck False u k
174− return [KindConstraint u k t]
175−unifyKinds t k (KUnknown u) = do
176− guardWith "Occurs check failed" $ not $ kindOccursCheck False u k
177− return [KindConstraint u k t]
178−unifyKinds _ Star Star = return []
179−unifyKinds _ Row Row = return []
180−unifyKinds t (FunKind k1 k2) (FunKind k3 k4) = do
181− cs1 <- unifyKinds t k1 k3
182− cs2 <- unifyKinds t k2 k4
183− return $ cs1 ++ cs2
184−unifyKinds _ k1 k2 = throwError $ "Cannot unify " ++ prettyPrintKind k1 ++ " with " ++ prettyPrintKind k2 ++ "."
185−
186−kindOccursCheck :: Bool -> Int -> Kind -> Bool
187−kindOccursCheck b u (KUnknown u') | u == u' = b
188−kindOccursCheck _ u (FunKind k1 k2) = kindOccursCheck True u k1 || kindOccursCheck True u k2
189−kindOccursCheck _ _ _ = False
src/Language/PureScript/TypeChecker/Monad.hs+71−9
@@ -12,14 +12,20 @@
12--
12--
13-----------------------------------------------------------------------------
13-----------------------------------------------------------------------------
14
14
15−{-# LANGUAGE GeneralizedNewtypeDeriving, FlexibleInstances #-}
15+{-# LANGUAGE GeneralizedNewtypeDeriving, FlexibleInstances, RankNTypes, DeriveDataTypeable,
16+ StandaloneDeriving, MultiParamTypeClasses, FlexibleContexts #-}
16
17
17module Language.PureScript.TypeChecker.Monad where
18module Language.PureScript.TypeChecker.Monad where
18
19
19import Language.PureScript.Types
20import Language.PureScript.Types
20import Language.PureScript.Kinds
21import Language.PureScript.Kinds
21import Language.PureScript.Names
22import Language.PureScript.Names
23+import Language.PureScript.Unknown
22
24
25+import Data.Data
26+import Data.Maybe
27+import Data.Monoid
28+import Data.Typeable
23import Control.Applicative
29import Control.Applicative
24import Control.Monad.State
30import Control.Monad.State
25import Control.Monad.Error
31import Control.Monad.Error
@@ -46,11 +52,62 @@ emptyEnvironment = Environment M.empty M.empty M.empty M.empty M.empty
46data CheckState = CheckState { checkEnv :: Environment
52data CheckState = CheckState { checkEnv :: Environment
47 , checkNextVar :: Int
53 , checkNextVar :: Int
48 , checkModulePath :: ModulePath
54 , checkModulePath :: ModulePath
49− } deriving (Show)
55+ }
50
56
51newtype Check a = Check { unCheck :: StateT CheckState (Either String) a }
57newtype Check a = Check { unCheck :: StateT CheckState (Either String) a }
52 deriving (Functor, Monad, Applicative, MonadPlus, MonadState CheckState, MonadError String)
58 deriving (Functor, Monad, Applicative, MonadPlus, MonadState CheckState, MonadError String)
53
59
60+newtype Substitution = Substitution { runSubstitution :: forall t. (Unifiable t) => Unknown t -> t }
61+
62+instance Monoid Substitution where
63+ mempty = Substitution unknown
64+ s1 `mappend` s2 = Substitution $ \u -> apply s1 (apply s2 (unknown u))
65+
66+newtype Subst m a = Subst { unSubst :: StateT Substitution m a }
67+ deriving (Functor, Monad, Applicative, MonadPlus, MonadTrans)
68+
69+deriving instance (MonadError String m) => MonadError String (Subst m)
70+
71+runSubst :: (Unifiable a, Monad m) => Subst m a -> m a
72+runSubst subst = do
73+ (a, s) <- flip runStateT mempty . unSubst $ subst
74+ return $ apply s a
75+
76+substituteWith :: (Typeable t) => (Unknown t -> t) -> Substitution
77+substituteWith f = Substitution $ \u -> fromMaybe (unknown u) $ do
78+ u1 <- cast u
79+ cast (f u1)
80+
81+substituteOne :: (Unifiable t) => Unknown t -> t -> Substitution
82+substituteOne u t = substituteWith $ \u1 ->
83+ case u1 of
84+ u2 | u2 == u -> t
85+ | otherwise -> unknown u2
86+
87+replace :: (Unifiable t) => Unknown t -> t -> Subst Check ()
88+replace u t' = do
89+ sub <- Subst get
90+ let t = apply sub t'
91+ occursCheck u t
92+ let current = apply sub $ unknown u
93+ case isUnknown current of
94+ Just u1 | u1 == u -> return ()
95+ _ -> current ~~ t
96+ Subst . modify $ \s -> substituteOne u t <> s
97+
98+class (Typeable t, Data t) => Unifiable t where
99+ unknown :: Unknown t -> t
100+ (~~) :: t -> t -> Subst Check ()
101+ isUnknown :: t -> Maybe (Unknown t)
102+ apply :: Substitution -> t -> t
103+ unknowns :: t -> [Int]
104+
105+occursCheck :: (Unifiable t) => Unknown s -> t -> Subst Check ()
106+occursCheck (Unknown u) t =
107+ case isUnknown t of
108+ Nothing -> guardWith "Occurs check fails" (u `notElem` unknowns t)
109+ _ -> return ()
110+
54getEnv :: Check Environment
111getEnv :: Check Environment
55getEnv = fmap checkEnv get
112getEnv = fmap checkEnv get
56
113
@@ -60,14 +117,19 @@ putEnv env = modify (\s -> s { checkEnv = env })
60modifyEnv :: (Environment -> Environment) -> Check ()
117modifyEnv :: (Environment -> Environment) -> Check ()
61modifyEnv f = modify (\s -> s { checkEnv = f (checkEnv s) })
118modifyEnv f = modify (\s -> s { checkEnv = f (checkEnv s) })
62
119
63−fresh :: Check Int
120+fresh' :: Subst Check Int
64−fresh = do
121+fresh' = do
65− st <- get
122+ n <- lift $ checkNextVar <$> get
66− put $ st { checkNextVar = checkNextVar st + 1 }
123+ lift . modify $ \s -> s { checkNextVar = succ (checkNextVar s) }
67− return $ checkNextVar st
124+ return n
125+
126+fresh :: (Unifiable t) => Subst Check t
127+fresh = unknown . Unknown <$> fresh'
68
128
69−check :: Check a -> Either String (a, Environment)
129+runCheck :: Check a -> Either String (a, Environment)
130+runCheck c = do
70−check = fmap (second checkEnv) . flip runStateT (CheckState emptyEnvironment 0 global) . unCheck
131+ (a, s) <- flip runStateT (CheckState emptyEnvironment 0 global) $ unCheck c
132+ return (a, checkEnv s)
71
133
72guardWith :: (MonadError e m) => e -> Bool -> m ()
134guardWith :: (MonadError e m) => e -> Bool -> m ()
73guardWith _ True = return ()
135guardWith _ True = return ()
src/Language/PureScript/TypeChecker/Types.hs+420−441
@@ -15,8 +15,6 @@
15{-# LANGUAGE DeriveDataTypeable #-}
15{-# LANGUAGE DeriveDataTypeable #-}
16
16
17module Language.PureScript.TypeChecker.Types (
17module Language.PureScript.TypeChecker.Types (
18− TypeConstraint(..),
19− TypeSolution(..),
20 typeOf
18 typeOf
21) where
19) where
22
20
@@ -35,56 +33,127 @@ import Language.PureScript.TypeChecker.Monad
35import Language.PureScript.TypeChecker.Kinds
33import Language.PureScript.TypeChecker.Kinds
36import Language.PureScript.TypeChecker.Synonyms
34import Language.PureScript.TypeChecker.Synonyms
37import Language.PureScript.Pretty
35import Language.PureScript.Pretty
36+import Language.PureScript.Unknown
38
37
39import Control.Monad.State
38import Control.Monad.State
40import Control.Monad.Error
39import Control.Monad.Error
41
40
42import Control.Applicative
41import Control.Applicative
43−import Control.Arrow (Kleisli(..), (***), (&&&), first)
42+import Control.Arrow (Arrow(..), Kleisli(..), (***), (&&&), second)
44import qualified Control.Category as C
43import qualified Control.Category as C
45
44
46import qualified Data.Map as M
45import qualified Data.Map as M
47
46
48−data TypeConstraintOrigin
47+instance Unifiable Type where
49− = ValueOrigin Value
48+ unknown = TUnknown
50− | BinderOrigin Binder
49+ isUnknown (TUnknown u) = Just u
51− | AssignmentTargetOrigin Ident deriving (Show, D.Data, D.Typeable)
50+ isUnknown _ = Nothing
52−
51+ TUnknown u1 ~~ TUnknown u2 | u1 == u2 = return ()
53−prettyPrintOrigin :: TypeConstraintOrigin -> String
52+ TUnknown u ~~ t = replace u t
54−prettyPrintOrigin (ValueOrigin val) = prettyPrintValue val
53+ t ~~ TUnknown u = replace u t
55−prettyPrintOrigin (BinderOrigin binder) = prettyPrintBinder binder
54+ SaturatedTypeSynonym name1 args1 ~~ SaturatedTypeSynonym name2 args2 | name1 == name2 =
56−prettyPrintOrigin (AssignmentTargetOrigin ident) = show ident
55+ zipWithM_ (~~) args1 args2
57−
56+ SaturatedTypeSynonym name args ~~ ty = do
58−data TypeConstraint
57+ env <- lift getEnv
59− = TypeConstraint Int Type TypeConstraintOrigin
58+ modulePath <- checkModulePath `fmap` lift get
60− | RowConstraint Int Row TypeConstraintOrigin deriving (Show, D.Data, D.Typeable)
59+ case M.lookup (qualify modulePath name) (typeSynonyms env) of
61−
60+ Just (synArgs, body) -> do
62−newtype TypeSolution = TypeSolution { runTypeSolution :: (Int -> Type, Int -> Row) }
61+ let m = M.fromList $ zip synArgs args
63−
62+ let replaced = replaceTypeVars m body
64−emptyTypeSolution :: TypeSolution
63+ replaced ~~ ty
65−emptyTypeSolution = TypeSolution (TUnknown, RUnknown)
64+ Nothing -> error "Type synonym was not defined"
65+ ty ~~ s@(SaturatedTypeSynonym _ _) = s ~~ ty
66+ ForAll idents ty1 ~~ ty2 = do
67+ sk <- skolemize idents ty1
68+ sk ~~ ty2
69+ ty ~~ f@(ForAll _ _) = f ~~ ty
70+ Number ~~ Number = return ()
71+ String ~~ String = return ()
72+ Boolean ~~ Boolean = return ()
73+ Array s ~~ Array t = s ~~ t
74+ Object row1 ~~ Object row2 = row1 ~~ row2
75+ Function args1 ret1 ~~ Function args2 ret2 = do
76+ guardWith "Function applied to incorrect number of args" $ length args1 == length args2
77+ zipWithM_ (~~) args1 args2
78+ ret1 ~~ ret2
79+ TypeVar v1 ~~ TypeVar v2 | v1 == v2 = return ()
80+ TypeConstructor c1 ~~ TypeConstructor c2 = do
81+ modulePath <- checkModulePath `fmap` lift get
82+ guardWith ("Cannot unify " ++ show c1 ++ " with " ++ show c2 ++ ".") (qualify modulePath c1 == qualify modulePath c2)
83+ TypeApp t1 t2 ~~ TypeApp t3 t4 = do
84+ t1 ~~ t3
85+ t2 ~~ t4
86+ Skolem s1 ~~ Skolem s2 | s1 == s2 = return ()
87+ t1 ~~ t2 = throwError $ "Cannot unify " ++ prettyPrintType t1 ++ " with " ++ prettyPrintType t2 ++ "."
88+ apply s (TUnknown u) = runSubstitution s u
89+ apply s (SaturatedTypeSynonym name tys) = SaturatedTypeSynonym name $ map (apply s) tys
90+ apply s (ForAll idents ty) = ForAll idents $ apply s ty
91+ apply s (Array t) = Array (apply s t)
92+ apply s (Object r) = Object (apply s r)
93+ apply s (Function args ret) = Function (map (apply s) args) (apply s ret)
94+ apply s (TypeApp t1 t2) = TypeApp (apply s t1) (apply s t2)
95+ apply _ t = t
96+ unknowns (TUnknown (Unknown u)) = [u]
97+ unknowns (SaturatedTypeSynonym _ tys) = concatMap unknowns tys
98+ unknowns (ForAll idents ty) = unknowns ty
99+ unknowns (Array t) = unknowns t
100+ unknowns (Object r) = unknowns r
101+ unknowns (Function args ret) = concatMap unknowns args ++ unknowns ret
102+ unknowns (TypeApp t1 t2) = unknowns t1 ++ unknowns t2
103+ unknowns _ = []
104+
105+instance Unifiable Row where
106+ unknown = RUnknown
107+ isUnknown (RUnknown u) = Just u
108+ isUnknown _ = Nothing
109+ r1 ~~ r2 =
110+ let
111+ (s1, r1') = rowToList r1
112+ (s2, r2') = rowToList r2
113+ int = [ (t1, t2) | (name, t1) <- s1, (name', t2) <- s2, name == name' ]
114+ sd1 = [ (name, t1) | (name, t1) <- s1, name `notElem` map fst s2 ]
115+ sd2 = [ (name, t2) | (name, t2) <- s2, name `notElem` map fst s1 ]
116+ in do
117+ forM_ int (uncurry (~~))
118+ unifyRows sd1 r1' sd2 r2'
119+ where
120+ unifyRows :: [(String, Type)] -> Row -> [(String, Type)] -> Row -> Subst Check ()
121+ unifyRows [] (RUnknown u) sd r = replace u (rowFromList (sd, r))
122+ unifyRows sd r [] (RUnknown u) = replace u (rowFromList (sd, r))
123+ unifyRows ns@((name, ty):row) r others u@(RUnknown un) = do
124+ occursCheck un ty
125+ forM row $ \(_, ty) -> occursCheck un ty
126+ u' <- fresh
127+ u ~~ RCons name ty u'
128+ unifyRows row r others u'
129+ unifyRows [] REmpty [] REmpty = return ()
130+ unifyRows [] (RowVar v1) [] (RowVar v2) | v1 == v2 = return ()
131+ unifyRows sd1 r1 sd2 r2 = throwError $ "Cannot unify " ++ prettyPrintRow (rowFromList (sd1, r1)) ++ " with " ++ prettyPrintRow (rowFromList (sd2, r2)) ++ "."
132+ apply s (RUnknown u) = runSubstitution s u
133+ apply s (RCons name ty r) = RCons name (apply s ty) (apply s r)
134+ apply _ r = r
135+ unknowns (RUnknown (Unknown u)) = [u]
136+ unknowns (RCons _ ty r) = unknowns ty ++ unknowns r
137+ unknowns _ = []
66
138
67isFunction :: Value -> Bool
139isFunction :: Value -> Bool
68isFunction (Abs _ _) = True
140isFunction (Abs _ _) = True
69isFunction (TypedValue untyped _) = isFunction untyped
141isFunction (TypedValue untyped _) = isFunction untyped
70isFunction _ = False
142isFunction _ = False
71
143
72−allConstraints :: Ident -> Value -> Check ([TypeConstraint], Int)
73−allConstraints name val | isFunction val = do
74− me <- fresh
75− (cs, n) <- typeConstraints (M.singleton name me) val
76− return (TypeConstraint me (TUnknown n) (ValueOrigin val): cs, n)
77−allConstraints _ val = typeConstraints M.empty val
78−
79−typeOf :: Ident -> Value -> Check Type
144+typeOf :: Maybe Ident -> Value -> Check Type
80typeOf name val = do
145typeOf name val = do
81− (cs, n) <- allConstraints name val
146+ ty <- runSubst $ case name of
147+ Just ident -> do me <- fresh
148+ ty <- infer (M.singleton ident me) val
149+ me ~~ ty
150+ return ty
151+ Nothing -> infer M.empty val
82− desugared <- replaceAllTypeSynonyms cs
152+ --desugared <- replaceAllTypeSynonyms cs
83− solution <- solveTypeConstraints desugared emptyTypeSolution
84− let ty = fst (runTypeSolution solution) n
85− allUnknownsBecameQuantified desugared solution ty
153+ --TODO: allUnknownsBecameQuantified desugared solution ty
86 return $ varIfUnknown $ desaturateAllTypeSynonyms $ setifyAll ty
154 return $ varIfUnknown $ desaturateAllTypeSynonyms $ setifyAll ty
87
155
156+{-
88allUnknownsBecameQuantified :: [TypeConstraint] -> TypeSolution -> Type -> Check ()
157allUnknownsBecameQuantified :: [TypeConstraint] -> TypeSolution -> Type -> Check ()
89allUnknownsBecameQuantified cs solution ty = do
158allUnknownsBecameQuantified cs solution ty = do
90 let
159 let
@@ -102,19 +171,27 @@ allUnknownsBecameQuantified cs solution ty = do
102 unsolvedRows = filter (\n -> RUnknown n == snd (runTypeSolution solution) n) unknownRows
171 unsolvedRows = filter (\n -> RUnknown n == snd (runTypeSolution solution) n) unknownRows
103 guardWith "Unsolved row variable" $ null $ unsolvedRows \\ rowsMentioned
172 guardWith "Unsolved row variable" $ null $ unsolvedRows \\ rowsMentioned
104
173
174+findUnknownTypes :: (D.Data d) => d -> [Unknown Type]
175+findUnknownTypes = everything (++) (mkQ [] f)
176+ where
177+ f :: Type -> [Unknown Type]
178+ f (TUnknown n) = [n]
179+ f _ = []
180+
181+findUnknownRows :: (D.Data d) => d -> [Unknown Row]
182+findUnknownRows = everything (++) (mkQ [] f)
183+ where
184+ f :: Row -> [Unknown Row]
185+ f (RUnknown n) = [n]
186+ f _ = []
187+-}
188+
105setify :: Row -> Row
189setify :: Row -> Row
106setify = rowFromList . first (M.toList . M.fromList) . rowToList
190setify = rowFromList . first (M.toList . M.fromList) . rowToList
107
191
108setifyAll :: (D.Data d) => d -> d
192setifyAll :: (D.Data d) => d -> d
109setifyAll = everywhere (mkT setify)
193setifyAll = everywhere (mkT setify)
110
194
111−findUnknownTypes :: (D.Data d) => d -> [Int]
112−findUnknownTypes = everything (++) (mkQ [] f)
113− where
114− f :: Type -> [Int]
115− f (TUnknown n) = [n]
116− f _ = []
117−
118findTypeVars :: (D.Data d) => d -> [String]
195findTypeVars :: (D.Data d) => d -> [String]
119findTypeVars = everything (++) (mkQ [] f)
196findTypeVars = everything (++) (mkQ [] f)
120 where
197 where
@@ -122,13 +199,6 @@ findTypeVars = everything (++) (mkQ [] f)
122 f (TypeVar v) = [v]
199 f (TypeVar v) = [v]
123 f _ = []
200 f _ = []
124
201
125−findUnknownRows :: (D.Data d) => d -> [Int]
126−findUnknownRows = everything (++) (mkQ [] f)
127− where
128− f :: Row -> [Int]
129− f (RUnknown n) = [n]
130− f _ = []
131−
132varIfUnknown :: Type -> Type
202varIfUnknown :: Type -> Type
133varIfUnknown ty =
203varIfUnknown ty =
134 let
204 let
@@ -137,7 +207,7 @@ varIfUnknown ty =
137 ForAll (sort $ nub $ M.elems m ++ findTypeVars ty) ty'
207 ForAll (sort $ nub $ M.elems m ++ findTypeVars ty) ty'
138 where
208 where
139 f :: Type -> State (M.Map Int String) Type
209 f :: Type -> State (M.Map Int String) Type
140− f (TUnknown n) = do
210+ f (TUnknown (Unknown n)) = do
141 m <- get
211 m <- get
142 case M.lookup n m of
212 case M.lookup n m of
143 Nothing -> do
213 Nothing -> do
@@ -147,7 +217,7 @@ varIfUnknown ty =
147 Just name -> return $ TypeVar name
217 Just name -> return $ TypeVar name
148 f t = return t
218 f t = return t
149 g :: Row -> State (M.Map Int String) Row
219 g :: Row -> State (M.Map Int String) Row
150− g (RUnknown n) = do
220+ g (RUnknown (Unknown n)) = do
151 m <- get
221 m <- get
152 case M.lookup n m of
222 case M.lookup n m of
153 Nothing -> do
223 Nothing -> do
@@ -165,28 +235,28 @@ replaceTypeVars m = everywhere (mkT replace)
165 _ -> TypeVar v
235 _ -> TypeVar v
166 replace t = t
236 replace t = t
167
237
168−replaceVarsWithUnknowns :: [String] -> Type -> Check Type
238+replaceVarsWithUnknowns :: [String] -> Type -> Subst Check Type
169replaceVarsWithUnknowns idents = flip evalStateT M.empty . everywhereM (flip extM f $ mkM g)
239replaceVarsWithUnknowns idents = flip evalStateT M.empty . everywhereM (flip extM f $ mkM g)
170 where
240 where
171− f :: Type -> StateT (M.Map String Int) Check Type
241+ f :: Type -> StateT (M.Map String Int) (Subst Check) Type
172 f (TypeVar var) | var `elem` idents = do
242 f (TypeVar var) | var `elem` idents = do
173 m <- get
243 m <- get
174− n <- lift fresh
244+ n <- lift fresh'
175 case M.lookup var m of
245 case M.lookup var m of
176 Nothing -> do
246 Nothing -> do
177 put (M.insert var n m)
247 put (M.insert var n m)
178− return $ TUnknown n
248+ return $ TUnknown (Unknown n)
179− Just u -> return $ TUnknown u
249+ Just u -> return $ TUnknown (Unknown u)
180 f t = return t
250 f t = return t
181− g :: Row -> StateT (M.Map String Int) Check Row
251+ g :: Row -> StateT (M.Map String Int) (Subst Check) Row
182 g (RowVar var) | var `elem` idents = do
252 g (RowVar var) | var `elem` idents = do
183 m <- get
253 m <- get
184− n <- lift fresh
254+ n <- lift fresh'
185 case M.lookup var m of
255 case M.lookup var m of
186 Nothing -> do
256 Nothing -> do
187 put (M.insert var n m)
257 put (M.insert var n m)
188− return $ RUnknown n
258+ return $ RUnknown (Unknown n)
189− Just u -> return $ RUnknown u
259+ Just u -> return $ RUnknown (Unknown u)
190 g r = return r
260 g r = return r
191
261
192replaceAllTypeSynonyms :: (D.Data d) => d -> Check d
262replaceAllTypeSynonyms :: (D.Data d) => d -> Check d
@@ -201,443 +271,352 @@ desaturateAllTypeSynonyms = everywhere (mkT replace)
201 replace (SaturatedTypeSynonym name args) = foldl TypeApp (TypeConstructor name) args
271 replace (SaturatedTypeSynonym name args) = foldl TypeApp (TypeConstructor name) args
202 replace t = t
272 replace t = t
203
273
204−replaceType :: (D.Data d) => Int -> Type -> d -> d
205−replaceType n t = everywhere (mkT go)
206− where
207− go (TUnknown m) | m == n = t
208− go t = t
209−
210−replaceRow :: (D.Data d) => Int -> Row -> d -> d
211−replaceRow n r = everywhere (mkT go)
212− where
213− go (RUnknown m) | m == n = r
214− go r = r
215−
216−typeOccursCheck :: Int -> Type -> Check ()
217−typeOccursCheck u (TUnknown _) = return ()
218−typeOccursCheck u t = when (occursCheck u t) $ throwError $ "Occurs check failed: " ++ show u ++ " = " ++ prettyPrintType t
219−
220−rowOccursCheck :: Int -> Row -> Check ()
221−rowOccursCheck u (RUnknown _) = return ()
222−rowOccursCheck u r = when (occursCheck u r) $ throwError $ "Occurs check failed: " ++ show u ++ " = " ++ prettyPrintRow r
223−
224−occursCheck :: (D.Data d) => Int -> d -> Bool
225−occursCheck u = everything (||) $ flip extQ g $ mkQ False f
226− where
227− f (TUnknown u') | u' == u = True
228− f _ = False
229− g (RUnknown u') | u' == u = True
230− g _ = False
231−
232ensureNoDuplicateProperties :: [(String, Value)] -> Check ()
274ensureNoDuplicateProperties :: [(String, Value)] -> Check ()
233ensureNoDuplicateProperties ps = guardWith "Duplicate property names" $ length (nub . map fst $ ps) == length ps
275ensureNoDuplicateProperties ps = guardWith "Duplicate property names" $ length (nub . map fst $ ps) == length ps
234
276
235−typeConstraints :: M.Map Ident Int -> Value -> Check ([TypeConstraint], Int)
277+infer :: M.Map Ident Type -> Value -> Subst Check Type
236−typeConstraints _ v@(NumericLiteral _) = do
278+infer _ (NumericLiteral _) = return Number
237− me <- fresh
238− return ([TypeConstraint me Number (ValueOrigin v)], me)
239−typeConstraints _ v@(StringLiteral _) = do
279+infer _ (StringLiteral _) = return String
240− me <- fresh
241− return ([TypeConstraint me String (ValueOrigin v)], me)
242−typeConstraints _ v@(BooleanLiteral _) = do
280+infer _ (BooleanLiteral _) = return Boolean
243− me <- fresh
244− return ([TypeConstraint me Boolean (ValueOrigin v)], me)
245−typeConstraints m v@(ArrayLiteral vals) = do
281+infer m (ArrayLiteral vals) = do
246− all <- mapM (typeConstraints m) vals
282+ ts <- mapM (infer m) vals
247− let (cs, ns) = (concatMap fst &&& map snd) all
248− me <- fresh
283+ arr <- fresh
249− return (cs ++ zipWith (\n el -> TypeConstraint me (Array $ TUnknown n) (ValueOrigin el)) ns vals, me)
284+ forM_ ts $ \t -> arr ~~ Array t
285+ return arr
250−typeConstraints m u@(Unary op val) = do
286+infer m (Unary op val) = do
251− (cs, n1) <- typeConstraints m val
287+ t <- infer m val
252− me <- fresh
288+ inferUnary op t
253− return (cs ++ unaryOperatorConstraints u op n1 me, me)
254−typeConstraints m b@(Binary op left right) = do
289+infer m (Binary op left right) = do
255− (cs1, n1) <- typeConstraints m left
290+ t1 <- infer m left
256− (cs2, n2) <- typeConstraints m right
291+ t2 <- infer m right
257− me <- fresh
292+ inferBinary op t1 t2
258− return (cs1 ++ cs2 ++ binaryOperatorConstraints b op n1 n2 me, me)
259−typeConstraints m v@(ObjectLiteral ps) = do
293+infer m (ObjectLiteral ps) = do
260− ensureNoDuplicateProperties ps
294+ lift $ ensureNoDuplicateProperties ps
261− all <- mapM (typeConstraints m . snd) ps
295+ ts <- mapM (infer m . snd) ps
262− let (cs, ns) = (concatMap fst &&& map snd) all
263− me <- fresh
264− let tys = zipWith (\(name, _) u -> (name, TUnknown u)) ps ns
296+ let fields = zipWith (\(name, _) t -> (name, t)) ps ts
265− return (TypeConstraint me (Object (typesToRow tys)) (ValueOrigin v) : cs, me)
297+ return $ Object $ typesToRow fields
266−typeConstraints m v@(ObjectUpdate o ps) = do
298+infer m (ObjectUpdate o ps) = do
267− ensureNoDuplicateProperties ps
299+ lift $ ensureNoDuplicateProperties ps
268− (cs1, n1) <- typeConstraints m o
300+ obj <- infer m o
269− all <- mapM (typeConstraints m . snd) ps
270− let (cs2, ns) = (concatMap fst &&& map snd) all
271 row <- fresh
301 row <- fresh
302+ ts <- mapM (infer m . snd) ps
272− let tys = zipWith (\(name, _) u -> (name, TUnknown u)) ps ns
303+ let tys = zipWith (\(name, _) t -> (name, t)) ps ts
273− return (TypeConstraint n1 (Object (rowFromList (tys, RUnknown row))) (ValueOrigin v) : cs1 ++ cs2, n1)
304+ obj ~~ Object (rowFromList (tys, row))
305+ return obj
274−typeConstraints m v@(Indexer index val) = do
306+infer m (Indexer index val) = do
275− (cs1, n1) <- typeConstraints m index
307+ el <- fresh
276− (cs2, n2) <- typeConstraints m val
308+ t1 <- infer m index
277− me <- fresh
309+ t2 <- infer m val
278− return (TypeConstraint n1 Number (ValueOrigin index) : TypeConstraint n2 (Array (TUnknown me)) (ValueOrigin v) : cs1 ++ cs2, me)
310+ t1 ~~ Number
311+ t2 ~~ Array el
312+ return el
279−typeConstraints m v@(Accessor prop val) = do
313+infer m (Accessor prop val) = do
280− (cs, n1) <- typeConstraints m val
314+ obj <- infer m val
281− me <- fresh
315+ field <- fresh
282 rest <- fresh
316 rest <- fresh
283− return (TypeConstraint n1 (Object (RCons prop (TUnknown me) (RUnknown rest))) (ValueOrigin v) : cs, me)
317+ obj ~~ Object (RCons prop field rest)
318+ return field
284−typeConstraints m v@(Abs args ret) = do
319+infer m v@(Abs args ret) = do
285− ns <- replicateM (length args) fresh
320+ ts <- replicateM (length args) fresh
286− let m' = m `M.union` M.fromList (zip args ns)
321+ let m' = m `M.union` M.fromList (zip args ts)
287− (cs, n') <- typeConstraints m' ret
322+ body <- infer m' ret
323+ return $ Function ts body
324+infer m v@(App f xs) = do
325+ t1 <- infer m f
326+ ts <- mapM (infer m) xs
288 me <- fresh
327 me <- fresh
289− return (TypeConstraint me (Function (map TUnknown ns) (TUnknown n')) (ValueOrigin v) : cs, me)
328+ t1 ~~ Function ts me
290−typeConstraints m v@(App f xs) = do
329+ return me
291− (cs1, n1) <- typeConstraints m f
292− all <- mapM (typeConstraints m) xs
293− let (cs2, ns) = (concatMap fst &&& map snd) all
294− me <- fresh
295− return (TypeConstraint n1 (Function (map TUnknown ns) (TUnknown me)) (ValueOrigin v) : cs1 ++ cs2, me)
296−typeConstraints m v@(Var var@(Qualified mp name)) = do
330+infer m v@(Var var@(Qualified mp name)) = do
297 case mp of
331 case mp of
298 ModulePath [] ->
332 ModulePath [] ->
299 case M.lookup name m of
333 case M.lookup name m of
300− Just u -> do
334+ Just ty -> lift $ replaceAllTypeSynonyms ty
301− me <- fresh
302− return ([TypeConstraint u (TUnknown me) (ValueOrigin v)], me)
303 Nothing -> lookupGlobal
335 Nothing -> lookupGlobal
304 _ -> lookupGlobal
336 _ -> lookupGlobal
305 where
337 where
306 lookupGlobal = do
338 lookupGlobal = do
307− env <- getEnv
339+ env <- lift getEnv
308− modulePath <- checkModulePath `fmap` get
340+ modulePath <- checkModulePath `fmap` lift get
309 case M.lookup (qualify modulePath var) (names env) of
341 case M.lookup (qualify modulePath var) (names env) of
310 Nothing -> throwError $ show var ++ " is undefined"
342 Nothing -> throwError $ show var ++ " is undefined"
311− Just (ForAll idents ty, _) -> do
343+ Just (ty, _) -> lift $ replaceAllTypeSynonyms ty
312− me <- fresh
313− replaced <- replaceVarsWithUnknowns idents ty
314− return ([TypeConstraint me replaced (ValueOrigin v)], me)
315−typeConstraints m (Block ss) = do
344+infer m (Block ss) = do
316 ret <- fresh
345 ret <- fresh
317− (cs, allCodePathsReturn, _) <- typeConstraintsForBlock m M.empty ret ss
346+ (allCodePathsReturn, _) <- checkBlock m M.empty ret ss
318 guardWith "Block is missing a return statement" allCodePathsReturn
347 guardWith "Block is missing a return statement" allCodePathsReturn
319− return (cs, ret)
348+ return ret
320−typeConstraints m v@(Constructor c) = do
349+infer m v@(Constructor c) = do
321− env <- getEnv
350+ env <- lift getEnv
322− modulePath <- checkModulePath `fmap` get
351+ modulePath <- checkModulePath `fmap` lift get
323 case M.lookup (qualify modulePath c) (dataConstructors env) of
352 case M.lookup (qualify modulePath c) (dataConstructors env) of
324 Nothing -> throwError $ "Constructor " ++ show c ++ " is undefined"
353 Nothing -> throwError $ "Constructor " ++ show c ++ " is undefined"
325− Just (ForAll idents ty) -> do
326− me <- fresh
327− replaced <- replaceVarsWithUnknowns idents ty
354+ Just (ForAll idents ty) -> replaceVarsWithUnknowns idents ty
328− return ([TypeConstraint me replaced (ValueOrigin v)], me)
329−typeConstraints m (Case val binders) = do
355+infer m (Case val binders) = do
330− (cs1, n1) <- typeConstraints m val
356+ t1 <- infer m val
331 ret <- fresh
357 ret <- fresh
332− cs2 <- typeConstraintsForBinders m n1 ret binders
358+ cs2 <- checkBinders m t1 ret binders
333− return (cs1 ++ cs2, ret)
359+ return ret
334−typeConstraints m v@(IfThenElse cond th el) = do
360+infer m v@(IfThenElse cond th el) = do
335− (cs1, n1) <- typeConstraints m cond
361+ t1 <- infer m cond
336− (cs2, n2) <- typeConstraints m th
362+ t2 <- infer m th
337− (cs3, n3) <- typeConstraints m el
363+ t3 <- infer m el
338− return (TypeConstraint n1 Boolean (ValueOrigin cond) : TypeConstraint n2 (TUnknown n3) (ValueOrigin v) : cs1 ++ cs2 ++ cs3, n2)
364+ t1 ~~ Boolean
365+ t2 ~~ t3
366+ return t2
339−typeConstraints m v@(TypedValue val ty) = do
367+infer m v@(TypedValue val ty) = do
340− kind <- kindOf ty
368+ kind <- lift $ kindOf ty
341 guardWith ("Expected type of kind *, was " ++ prettyPrintKind kind) $ kind == Star
369 guardWith ("Expected type of kind *, was " ++ prettyPrintKind kind) $ kind == Star
370+ ty' <- lift $ replaceAllTypeSynonyms ty
342− typeCheck m val ty
371+ cs <- check m val ty'
343− me <- fresh
372+ return ty'
344− return ([TypeConstraint me ty (ValueOrigin v)], me)
373+
345−
374+inferUnary :: UnaryOperator -> Type -> Subst Check Type
346−typeCheck :: M.Map Ident Int -> Value -> Type -> Check ()
375+inferUnary Negate val = do
347−typeCheck _ _ _ = return ()
376+ val ~~ Number
348−
377+ return Number
349−unaryOperatorConstraints :: Value -> UnaryOperator -> Int -> Int -> [TypeConstraint]
378+inferUnary Not val = do
350−unaryOperatorConstraints v Negate val result = [TypeConstraint val Number (ValueOrigin v), TypeConstraint result Number (ValueOrigin v)]
379+ val ~~ Boolean
351−unaryOperatorConstraints v Not val result = [TypeConstraint val Boolean (ValueOrigin v), TypeConstraint result Boolean (ValueOrigin v)]
380+ return Boolean
352−unaryOperatorConstraints v BitwiseNot val result = [TypeConstraint val Number (ValueOrigin v), TypeConstraint result Number (ValueOrigin v)]
381+inferUnary BitwiseNot val = do
353−
382+ val ~~ Number
354−binaryOperatorConstraints :: Value -> BinaryOperator -> Int -> Int -> Int -> [TypeConstraint]
383+ return Number
355−binaryOperatorConstraints v Add = symBinOpConstraints v Number
384+
356−binaryOperatorConstraints v Subtract = symBinOpConstraints v Number
385+inferBinary :: BinaryOperator -> Type -> Type -> Subst Check Type
357−binaryOperatorConstraints v Multiply = symBinOpConstraints v Number
386+inferBinary Add = inferSymBinary Number
358−binaryOperatorConstraints v Divide = symBinOpConstraints v Number
387+inferBinary Subtract = inferSymBinary Number
359−binaryOperatorConstraints v Modulus = symBinOpConstraints v Number
388+inferBinary Multiply = inferSymBinary Number
360−binaryOperatorConstraints v LessThan = asymBinOpConstraints v Number Boolean
389+inferBinary Divide = inferSymBinary Number
390+inferBinary Modulus = inferSymBinary Number
391+inferBinary LessThan = inferAsymBinary Number Boolean
361−binaryOperatorConstraints v LessThanOrEqualTo = asymBinOpConstraints v Number Boolean
392+inferBinary LessThanOrEqualTo = inferAsymBinary Number Boolean
362−binaryOperatorConstraints v GreaterThan = asymBinOpConstraints v Number Boolean
393+inferBinary GreaterThan = inferAsymBinary Number Boolean
363−binaryOperatorConstraints v GreaterThanOrEqualTo = asymBinOpConstraints v Number Boolean
394+inferBinary GreaterThanOrEqualTo = inferAsymBinary Number Boolean
364−binaryOperatorConstraints v BitwiseAnd = symBinOpConstraints v Number
395+inferBinary BitwiseAnd = inferSymBinary Number
365−binaryOperatorConstraints v BitwiseOr = symBinOpConstraints v Number
396+inferBinary BitwiseOr = inferSymBinary Number
366−binaryOperatorConstraints v BitwiseXor = symBinOpConstraints v Number
397+inferBinary BitwiseXor = inferSymBinary Number
367−binaryOperatorConstraints v ShiftLeft = symBinOpConstraints v Number
398+inferBinary ShiftLeft = inferSymBinary Number
368−binaryOperatorConstraints v ShiftRight = symBinOpConstraints v Number
399+inferBinary ShiftRight = inferSymBinary Number
369−binaryOperatorConstraints v ZeroFillShiftRight = symBinOpConstraints v Number
400+inferBinary ZeroFillShiftRight = inferSymBinary Number
370−binaryOperatorConstraints v EqualTo = equalityBinOpConstraints v
401+inferBinary EqualTo = inferEqBinary
371−binaryOperatorConstraints v NotEqualTo = equalityBinOpConstraints v
402+inferBinary NotEqualTo = inferEqBinary
372−binaryOperatorConstraints v And = symBinOpConstraints v Boolean
403+inferBinary And = inferSymBinary Boolean
373−binaryOperatorConstraints v Or = symBinOpConstraints v Boolean
404+inferBinary Or = inferSymBinary Boolean
374−binaryOperatorConstraints v Concat = symBinOpConstraints v String
405+inferBinary Concat = inferSymBinary String
375−
406+
376−equalityBinOpConstraints :: Value -> Int -> Int -> Int -> [TypeConstraint]
407+inferEqBinary :: Type -> Type -> Subst Check Type
377−equalityBinOpConstraints v left right result = [TypeConstraint left (TUnknown right) (ValueOrigin v), TypeConstraint result Boolean (ValueOrigin v)]
408+inferEqBinary left right = do
378−
409+ left ~~ right
379−symBinOpConstraints :: Value -> Type -> Int -> Int -> Int -> [TypeConstraint]
410+ return Boolean
380−symBinOpConstraints v ty = asymBinOpConstraints v ty ty
411+
381−
412+inferSymBinary :: Type -> Type -> Type -> Subst Check Type
382−asymBinOpConstraints :: Value -> Type -> Type -> Int -> Int -> Int -> [TypeConstraint]
413+inferSymBinary ty = inferAsymBinary ty ty
383−asymBinOpConstraints v ty res left right result = [TypeConstraint left ty (ValueOrigin v), TypeConstraint right ty (ValueOrigin v), TypeConstraint result res (ValueOrigin v)]
414+
384−
415+inferAsymBinary :: Type -> Type -> Type -> Type -> Subst Check Type
385−typeConstraintsForBinder :: Int -> Binder -> Check ([TypeConstraint], M.Map Ident Int)
416+inferAsymBinary input output left right = do
417+ left ~~ input
418+ right ~~ input
419+ return output
420+
421+inferBinder :: Type -> Binder -> Subst Check (M.Map Ident Type)
386−typeConstraintsForBinder _ NullBinder = return ([], M.empty)
422+inferBinder _ NullBinder = return M.empty
387−typeConstraintsForBinder val b@(StringBinder _) = constantBinder b val String
423+inferBinder val (StringBinder _) = val ~~ String >> return M.empty
388−typeConstraintsForBinder val b@(NumberBinder _) = constantBinder b val Number
424+inferBinder val (NumberBinder _) = val ~~ Number >> return M.empty
389−typeConstraintsForBinder val b@(BooleanBinder _) = constantBinder b val Boolean
425+inferBinder val (BooleanBinder _) = val ~~ Boolean >> return M.empty
390−typeConstraintsForBinder val b@(VarBinder name) = do
426+inferBinder val (VarBinder name) = return $ M.singleton name val
391− me <- fresh
392− return ([TypeConstraint me (TUnknown val) (BinderOrigin b)], M.singleton name me)
393−typeConstraintsForBinder val b@(NullaryBinder ctor) = do
427+inferBinder val (NullaryBinder ctor) = do
394− env <- getEnv
428+ env <- lift getEnv
395− modulePath <- checkModulePath `fmap` get
429+ modulePath <- checkModulePath `fmap` lift get
396 case M.lookup (qualify modulePath ctor) (dataConstructors env) of
430 case M.lookup (qualify modulePath ctor) (dataConstructors env) of
397 Just (ForAll args ret) -> do
431 Just (ForAll args ret) -> do
398 ret' <- replaceVarsWithUnknowns args ret
432 ret' <- replaceVarsWithUnknowns args ret
399− return ([TypeConstraint val ret' (BinderOrigin b)], M.empty)
433+ val ~~ ret'
434+ return M.empty
400 _ -> throwError $ "Constructor " ++ show ctor ++ " is not defined"
435 _ -> throwError $ "Constructor " ++ show ctor ++ " is not defined"
401−typeConstraintsForBinder val b@(UnaryBinder ctor binder) = do
436+inferBinder val b@(UnaryBinder ctor binder) = do
402− env <- getEnv
437+ env <- lift getEnv
403− modulePath <- checkModulePath `fmap` get
438+ modulePath <- checkModulePath `fmap` lift get
404 case M.lookup (qualify modulePath ctor) (dataConstructors env) of
439 case M.lookup (qualify modulePath ctor) (dataConstructors env) of
405 Just (ForAll idents f@(Function [_] _)) -> do
440 Just (ForAll idents f@(Function [_] _)) -> do
406 obj <- fresh
441 obj <- fresh
407 (Function [ty] ret) <- replaceVarsWithUnknowns idents f
442 (Function [ty] ret) <- replaceVarsWithUnknowns idents f
408− (cs, m1) <- typeConstraintsForBinder obj binder
443+ m1 <- inferBinder obj binder
409− return (TypeConstraint val ret (BinderOrigin b) : TypeConstraint obj ty (BinderOrigin b) : cs, m1)
444+ val ~~ ret
445+ obj ~~ ty
446+ return m1
410 Just _ -> throwError $ show ctor ++ " is not a unary constructor"
447 Just _ -> throwError $ show ctor ++ " is not a unary constructor"
411 _ -> throwError $ "Constructor " ++ show ctor ++ " is not defined"
448 _ -> throwError $ "Constructor " ++ show ctor ++ " is not defined"
412−typeConstraintsForBinder val b@(ObjectBinder props) = do
449+inferBinder val b@(ObjectBinder props) = do
413 row <- fresh
450 row <- fresh
414 rest <- fresh
451 rest <- fresh
415− (cs, m1) <- typeConstraintsForProperties row (RUnknown rest) props
452+ m1 <- inferRowProperties row rest props
416− return (TypeConstraint val (Object (RUnknown row)) (BinderOrigin b) : cs, m1)
453+ val ~~ Object row
454+ return m1
417 where
455 where
418− typeConstraintsForProperties :: Int -> Row -> [(String, Binder)] -> Check ([TypeConstraint], M.Map Ident Int)
456+ inferRowProperties :: Row -> Row -> [(String, Binder)] -> Subst Check (M.Map Ident Type)
419− typeConstraintsForProperties nrow row [] = return ([RowConstraint nrow row (BinderOrigin b)], M.empty)
457+ inferRowProperties nrow row [] = nrow ~~ row >> return M.empty
420− typeConstraintsForProperties nrow row ((name, binder):binders) = do
458+ inferRowProperties nrow row ((name, binder):binders) = do
421 propTy <- fresh
459 propTy <- fresh
422− (cs1, m1) <- typeConstraintsForBinder propTy binder
460+ m1 <- inferBinder propTy binder
423− (cs2, m2) <- typeConstraintsForProperties nrow (RCons name (TUnknown propTy) row) binders
461+ m2 <- inferRowProperties nrow (RCons name propTy row) binders
424− return (cs1 ++ cs2, m1 `M.union` m2)
462+ return $ m1 `M.union` m2
425−typeConstraintsForBinder val b@(ArrayBinder binders rest) = do
463+inferBinder val (ArrayBinder binders rest) = do
426 el <- fresh
464 el <- fresh
427− all <- mapM (typeConstraintsForBinder el) binders
465+ m1 <- M.unions <$> mapM (inferBinder el) binders
428− let (cs1, m1) = (concatMap fst &&& M.unions . map snd) all
466+ val ~~ Array el
429− let arrayConstraint = TypeConstraint val (Array (TUnknown el)) (BinderOrigin b)
430 case rest of
467 case rest of
431− Nothing -> return (arrayConstraint : cs1, m1)
468+ Nothing -> return m1
432 Just binder -> do
469 Just binder -> do
433− (cs2, m2) <- typeConstraintsForBinder val binder
470+ m2 <- inferBinder val binder
434− return (arrayConstraint : cs1 ++ cs2, m1 `M.union` m2)
471+ return $ m1 `M.union` m2
435−typeConstraintsForBinder val b@(NamedBinder name binder) = do
472+inferBinder val (NamedBinder name binder) = do
436− me <- fresh
473+ m <- inferBinder val binder
437− (cs, m) <- typeConstraintsForBinder val binder
438− return (TypeConstraint me (TUnknown val) (BinderOrigin b) : cs, M.insert name me m)
474+ return $ M.insert name val m
439−
475+
440−typeConstraintsForGuardedBinder :: M.Map Ident Int -> Int -> Binder -> Check ([TypeConstraint], M.Map Ident Int)
476+inferGuardedBinder :: M.Map Ident Type -> Type -> Binder -> Subst Check (M.Map Ident Type)
441−typeConstraintsForGuardedBinder m val b@(GuardedBinder cond binder) = do
477+inferGuardedBinder m val b@(GuardedBinder cond binder) = do
442− (cs1, m1) <- typeConstraintsForBinder val binder
478+ m1 <- inferBinder val binder
443− (cs2, n) <- typeConstraints (m `M.union` m1) cond
479+ ty <- infer (m `M.union` m1) cond
444− return (TypeConstraint n Boolean (ValueOrigin cond) : cs1 ++ cs2, m1)
480+ ty ~~ Boolean
445−typeConstraintsForGuardedBinder m val b = typeConstraintsForBinder val b >>= return
481+ return m1
446−
482+inferGuardedBinder m val b = inferBinder val b >>= return
447−constantBinder :: Binder -> Int -> Type -> Check ([TypeConstraint], M.Map Ident Int)
483+
448−constantBinder b val ty = return ([TypeConstraint val ty (BinderOrigin b)], M.empty)
484+checkBinders :: M.Map Ident Type -> Type -> Type -> [(Binder, Value)] -> Subst Check ()
449−
485+checkBinders _ _ _ [] = return ()
450−typeConstraintsForBinders :: M.Map Ident Int -> Int -> Int -> [(Binder, Value)] -> Check [TypeConstraint]
451−typeConstraintsForBinders _ _ _ [] = return []
452−typeConstraintsForBinders m nval ret ((binder, val):bs) = do
486+checkBinders m nval ret ((binder, val):bs) = do
453− (cs1, m1) <- typeConstraintsForGuardedBinder m nval binder
487+ m1 <- inferGuardedBinder m nval binder
454− (cs2, n2) <- typeConstraints (m `M.union` m1) val
488+ t <- infer (m `M.union` m1) val
455− cs3 <- typeConstraintsForBinders m nval ret bs
489+ t ~~ ret
456− return (TypeConstraint n2 (TUnknown ret) (BinderOrigin binder) : cs1 ++ cs2 ++ cs3)
490+ checkBinders m nval ret bs
457−
491+
458−assignVariable :: Ident -> M.Map Ident Int -> Check ()
492+assignVariable :: Ident -> M.Map Ident Type -> Subst Check ()
459assignVariable name m =
493assignVariable name m =
460 case M.lookup name m of
494 case M.lookup name m of
461 Nothing -> return ()
495 Nothing -> return ()
462 Just _ -> throwError $ "Variable with name " ++ show name ++ " already exists."
496 Just _ -> throwError $ "Variable with name " ++ show name ++ " already exists."
463
497
464−typeConstraintsForStatement :: M.Map Ident Int -> M.Map Ident Int -> Int -> Statement -> Check ([TypeConstraint], Bool, M.Map Ident Int)
498+checkStatement :: M.Map Ident Type -> M.Map Ident Type -> Type -> Statement -> Subst Check (Bool, M.Map Ident Type)
465−typeConstraintsForStatement m mass ret (VariableIntroduction name val) = do
499+checkStatement m mass ret (VariableIntroduction name val) = do
466 assignVariable name (m `M.union` mass)
500 assignVariable name (m `M.union` mass)
467− (cs1, n1) <- typeConstraints m val
501+ t <- infer m val
468− return (cs1, False, M.insert name n1 mass)
502+ return (False, M.insert name t mass)
469−typeConstraintsForStatement m mass ret (Assignment ident val) = do
503+checkStatement m mass ret (Assignment ident val) = do
470− (cs1, n1) <- typeConstraints m val
504+ t <- infer m val
471 case M.lookup ident mass of
505 case M.lookup ident mass of
472 Nothing -> throwError $ "No local variable with name " ++ show ident
506 Nothing -> throwError $ "No local variable with name " ++ show ident
473− Just ty ->
507+ Just ty -> do t ~~ ty
474− return (TypeConstraint n1 (TUnknown ty) (AssignmentTargetOrigin ident) : cs1, False, mass)
508+ return (False, mass)
475−typeConstraintsForStatement m mass ret (While val inner) = do
509+checkStatement m mass ret (While val inner) = do
476− (cs1, n1) <- typeConstraints m val
510+ t1 <- infer m val
511+ t1 ~~ Boolean
477− (cs2, allCodePathsReturn, _) <- typeConstraintsForBlock m mass ret inner
512+ (allCodePathsReturn, _) <- checkBlock m mass ret inner
478− return (TypeConstraint n1 Boolean (ValueOrigin val) : cs1 ++ cs2, allCodePathsReturn, mass)
513+ return (allCodePathsReturn, mass)
479−typeConstraintsForStatement m mass ret (If ifst) = do
514+checkStatement m mass ret (If ifst) = do
480− (cs, allCodePathsReturn) <- typeConstraintsForIfStatement m mass ret ifst
515+ allCodePathsReturn <- checkIfStatement m mass ret ifst
481− return (cs, allCodePathsReturn, mass)
516+ return (allCodePathsReturn, mass)
482−typeConstraintsForStatement m mass ret (For ident start end inner) = do
517+checkStatement m mass ret (For ident start end inner) = do
483 assignVariable ident (m `M.union` mass)
518 assignVariable ident (m `M.union` mass)
484− (cs1, n1) <- typeConstraints (m `M.union` mass) start
519+ t1 <- infer (m `M.union` mass) start
520+ t1 ~~ Number
485− (cs2, n2) <- typeConstraints (m `M.union` mass) end
521+ t2 <- infer (m `M.union` mass) end
522+ t2 ~~ Number
486− let mass1 = M.insert ident n1 mass
523+ let mass1 = M.insert ident Number mass
487− (cs3, allCodePathsReturn, _) <- typeConstraintsForBlock (m `M.union` mass1) mass1 ret inner
524+ (allCodePathsReturn, _) <- checkBlock (m `M.union` mass1) mass1 ret inner
488− return (TypeConstraint n1 Number (ValueOrigin start) : TypeConstraint n2 Number (ValueOrigin end) : cs1 ++ cs2 ++ cs3, allCodePathsReturn, mass)
525+ return (allCodePathsReturn, mass)
489−typeConstraintsForStatement m mass ret (ForEach ident vals inner) = do
526+checkStatement m mass ret (ForEach ident vals inner) = do
490 assignVariable ident (m `M.union` mass)
527 assignVariable ident (m `M.union` mass)
491 val <- fresh
528 val <- fresh
492− (cs1, n1) <- typeConstraints (m `M.union` mass) vals
529+ t1 <- infer (m `M.union` mass) vals
530+ t1 ~~ Array val
493 let mass1 = M.insert ident val mass
531 let mass1 = M.insert ident val mass
494− (cs2, allCodePathsReturn, _) <- typeConstraintsForBlock (m `M.union` mass1) mass1 ret inner
532+ (allCodePathsReturn, _) <- checkBlock (m `M.union` mass1) mass1 ret inner
495 guardWith "Cannot return from within a foreach block" $ not allCodePathsReturn
533 guardWith "Cannot return from within a foreach block" $ not allCodePathsReturn
496− return (TypeConstraint n1 (Array (TUnknown val)) (ValueOrigin vals) : cs1 ++ cs2, False, mass)
534+ return (False, mass)
497−typeConstraintsForStatement m mass ret (Return val) = do
535+checkStatement m mass ret (Return val) = do
498− (cs1, n1) <- typeConstraints (m `M.union` mass) val
536+ check (m `M.union` mass) val ret
499− return (TypeConstraint n1 (TUnknown ret) (ValueOrigin val) : cs1, True, mass)
537+ return (True, mass)
500−
538+
501−typeConstraintsForIfStatement :: M.Map Ident Int -> M.Map Ident Int -> Int -> IfStatement -> Check ([TypeConstraint], Bool)
539+checkIfStatement :: M.Map Ident Type -> M.Map Ident Type -> Type -> IfStatement -> Subst Check Bool
502−typeConstraintsForIfStatement m mass ret (IfStatement val thens Nothing) = do
540+checkIfStatement m mass ret (IfStatement val thens Nothing) = do
503− (cs1, n1) <- typeConstraints m val
541+ t1 <- infer m val
542+ t1 ~~ Boolean
504− (cs2, _, _) <- typeConstraintsForBlock m mass ret thens
543+ _ <- checkBlock m mass ret thens
505− return (TypeConstraint n1 Boolean (ValueOrigin val) : cs1 ++ cs2, False)
544+ return False
506−typeConstraintsForIfStatement m mass ret (IfStatement val thens (Just elses)) = do
545+checkIfStatement m mass ret (IfStatement val thens (Just elses)) = do
507− (cs1, n1) <- typeConstraints m val
546+ t1 <- infer m val
547+ t1 ~~ Boolean
508− (cs2, allCodePathsReturn1, _) <- typeConstraintsForBlock m mass ret thens
548+ (allCodePathsReturn1, _) <- checkBlock m mass ret thens
509− (cs3, allCodePathsReturn2) <- typeConstraintsForElseStatement m mass ret elses
549+ allCodePathsReturn2 <- checkElseStatement m mass ret elses
510− return (TypeConstraint n1 Boolean (ValueOrigin val) : cs1 ++ cs2 ++ cs3, allCodePathsReturn1 && allCodePathsReturn2)
550+ return $ allCodePathsReturn1 && allCodePathsReturn2
511−
551+
512−typeConstraintsForElseStatement :: M.Map Ident Int -> M.Map Ident Int -> Int -> ElseStatement -> Check ([TypeConstraint], Bool)
552+checkElseStatement :: M.Map Ident Type -> M.Map Ident Type -> Type -> ElseStatement -> Subst Check Bool
513−typeConstraintsForElseStatement m mass ret (Else elses) = do
553+checkElseStatement m mass ret (Else elses) = fst <$> checkBlock m mass ret elses
514− (cs, allCodePathsReturn, _) <- typeConstraintsForBlock m mass ret elses
554+checkElseStatement m mass ret (ElseIf ifst) = checkIfStatement m mass ret ifst
515− return (cs, allCodePathsReturn)
555+
516−typeConstraintsForElseStatement m mass ret (ElseIf ifst) = do
517− (cs, allCodePathsReturn) <- typeConstraintsForIfStatement m mass ret ifst
518− return (cs, allCodePathsReturn)
519−
520−typeConstraintsForBlock :: M.Map Ident Int -> M.Map Ident Int -> Int -> [Statement] -> Check ([TypeConstraint], Bool, M.Map Ident Int)
556+checkBlock :: M.Map Ident Type -> M.Map Ident Type -> Type -> [Statement] -> Subst Check (Bool, M.Map Ident Type)
521−typeConstraintsForBlock _ mass _ [] = return ([], False, mass)
557+checkBlock _ mass _ [] = return (False, mass)
522−typeConstraintsForBlock m mass ret (s:ss) = do
558+checkBlock m mass ret (s:ss) = do
523− (cs1, b1, mass1) <- typeConstraintsForStatement (m `M.union` mass) mass ret s
559+ (b1, mass1) <- checkStatement (m `M.union` mass) mass ret s
524 case (b1, ss) of
560 case (b1, ss) of
525− (True, []) -> return (cs1, True, mass1)
561+ (True, []) -> return (True, mass1)
526 (True, _) -> throwError "Unreachable code"
562 (True, _) -> throwError "Unreachable code"
527 (False, ss) -> do
563 (False, ss) -> do
528− (cs2, b2, mass2) <- typeConstraintsForBlock m mass1 ret ss
564+ (b2, mass2) <- checkBlock m mass1 ret ss
529− return (cs1 ++ cs2, b2, mass2)
565+ return (b2, mass2)
530−
566+
531−solveTypeConstraints :: [TypeConstraint] -> TypeSolution -> Check TypeSolution
567+skolemize :: [String] -> Type -> Subst Check Type
532−solveTypeConstraints [] s = return s
533−solveTypeConstraints all@(TypeConstraint n t o:cs) s = do
534− (cs', s') <- rethrow (\err -> "Error in " ++ prettyPrintOrigin o ++ ": " ++ err) $ do
535− typeOccursCheck n t
536− let s' = let (f, g) = runTypeSolution s
537− in TypeSolution (replaceType n t . f, replaceType n t . g)
538− cs' <- fmap concat $ mapM (substituteTypeInConstraint n t) cs
539− return (cs', s')
540− solveTypeConstraints cs' s'
541−solveTypeConstraints (RowConstraint n r o:cs) s = do
542− (cs', s') <- rethrow (\err -> "Error in " ++ prettyPrintOrigin o ++ ": " ++ err) $ do
543− rowOccursCheck n r
544− let s' = let (f, g) = runTypeSolution s
545− in TypeSolution (replaceRow n r . f, replaceRow n r . g)
546− cs' <- fmap concat $ mapM (substituteRowInConstraint n r) cs
547− return (cs', s')
548− solveTypeConstraints cs' s'
549−
550−substituteTypeInConstraint :: Int -> Type -> TypeConstraint -> Check [TypeConstraint]
551−substituteTypeInConstraint n s (TypeConstraint m t v)
552− | n == m = unifyTypes v s t
553− | otherwise = return [TypeConstraint m (replaceType n s t) v]
554−substituteTypeInConstraint n s (RowConstraint m r v)
555− = return [RowConstraint m (replaceType n s r) v]
556−
557−substituteRowInConstraint :: Int -> Row -> TypeConstraint -> Check [TypeConstraint]
558−substituteRowInConstraint n r (TypeConstraint m t v)
559− = return [TypeConstraint m (replaceRow n r t) v]
560−substituteRowInConstraint n r (RowConstraint m r1 v)
561− | m == n = unifyRows v r r1
562− | otherwise = return [RowConstraint m (replaceRow n r r1) v]
563−
564−unifyTypes :: TypeConstraintOrigin -> Type -> Type -> Check [TypeConstraint]
565−unifyTypes _ (TUnknown u1) (TUnknown u2) | u1 == u2 = return []
566−unifyTypes o (TUnknown u) t = do
567− typeOccursCheck u t
568− return [TypeConstraint u t o]
569−unifyTypes o t (TUnknown u) = do
570− typeOccursCheck u t
571− return [TypeConstraint u t o]
572−unifyTypes o (SaturatedTypeSynonym name1 args1) (SaturatedTypeSynonym name2 args2) | name1 == name2 =
573− fmap concat $ zipWithM (unifyTypes o) args1 args2
574−unifyTypes o (SaturatedTypeSynonym name args) ty = do
575− env <- getEnv
576− modulePath <- checkModulePath `fmap` get
577− case M.lookup (qualify modulePath name) (typeSynonyms env) of
578− Just (synArgs, body) -> do
579− let m = M.fromList $ zip synArgs args
580− let replaced = replaceTypeVars m body
581− unifyTypes o replaced ty
582− Nothing -> error "Type synonym was not defined"
583−unifyTypes o ty s@(SaturatedTypeSynonym _ _) = unifyTypes o s ty
584−unifyTypes o (ForAll idents ty1) ty2 =do
585− sk <- skolemize idents ty1
586− unifyTypes o sk ty2
587−unifyTypes o ty f@(ForAll _ _) = unifyTypes o f ty
588−unifyTypes _ Number Number = return []
589−unifyTypes _ String String = return []
590−unifyTypes _ Boolean Boolean = return []
591−unifyTypes o (Array s) (Array t) = unifyTypes o s t
592−unifyTypes o (Object row1) (Object row2) = unifyRows o row1 row2
593−unifyTypes o (Function args1 ret1) (Function args2 ret2) = do
594− guardWith "Function applied to incorrect number of args" $ length args1 == length args2
595− cs1 <- fmap concat $ zipWithM (unifyTypes o) args1 args2
596− cs2 <- unifyTypes o ret1 ret2
597− return $ cs1 ++ cs2
598−unifyTypes _ (TypeVar v1) (TypeVar v2) | v1 == v2 = return []
599−unifyTypes _ (TypeConstructor c1) (TypeConstructor c2) = do
600− modulePath <- checkModulePath `fmap` get
601− guardWith ("Cannot unify " ++ show c1 ++ " with " ++ show c2 ++ ".") (qualify modulePath c1 == qualify modulePath c2)
602− return []
603−unifyTypes o (TypeApp t1 t2) (TypeApp t3 t4) = do
604− cs1 <- unifyTypes o t1 t3
605− cs2 <- unifyTypes o t2 t4
606− return $ cs1 ++ cs2
607−unifyTypes _ (Skolem s1) (Skolem s2) | s1 == s2 = return []
608−unifyTypes _ t1 t2 = throwError $ "Cannot unify " ++ prettyPrintType t1 ++ " with " ++ prettyPrintType t2 ++ "."
609−
610−unifyRows :: TypeConstraintOrigin -> Row -> Row -> Check [TypeConstraint]
611−unifyRows o r1 r2 =
612− let
613− (s1, r1') = rowToList r1
614− (s2, r2') = rowToList r2
615− int = [ (t1, t2) | (name, t1) <- s1, (name', t2) <- s2, name == name' ]
616− sd1 = [ (name, t1) | (name, t1) <- s1, name `notElem` map fst s2 ]
617− sd2 = [ (name, t2) | (name, t2) <- s2, name `notElem` map fst s1 ]
618− in do
619− cs1 <- fmap concat $ mapM (uncurry $ unifyTypes o) int
620− cs2 <- unifyRows' o sd1 r1' sd2 r2'
621− return $ cs1 ++ cs2
622− where
623− unifyRows' :: TypeConstraintOrigin -> [(String, Type)] -> Row -> [(String, Type)] -> Row -> Check [TypeConstraint]
624− unifyRows' o [] (RUnknown u) sd r = do
625− rowOccursCheck u r
626− return [RowConstraint u (rowFromList (sd, r)) o]
627− unifyRows' o sd r [] (RUnknown u) = do
628− rowOccursCheck u r
629− return [RowConstraint u (rowFromList (sd, r)) o]
630− unifyRows' o ns@((name, ty):row) r others (RUnknown u) | not (occursCheck u (ty, row)) = do
631− u' <- fresh
632− cs <- unifyRows' o row r others (RUnknown u')
633− return (RowConstraint u (RCons name ty (RUnknown u')) o : cs)
634− unifyRows' _ [] REmpty [] REmpty = return []
635− unifyRows' _ [] (RowVar v1) [] (RowVar v2) | v1 == v2 = return []
636− unifyRows' _ sd1 r1 sd2 r2 = throwError $ "Cannot unify " ++ prettyPrintRow (rowFromList (sd1, r1)) ++ " with " ++ prettyPrintRow (rowFromList (sd2, r2)) ++ "."
637−
638−skolemize :: [String] -> Type -> Check Type
639skolemize idents ty = do
568skolemize idents ty = do
640− sks <- replicateM (length idents) fresh
569+ sks <- replicateM (length idents) fresh'
641 let m = M.fromList (zip idents (map Skolem sks))
570 let m = M.fromList (zip idents (map Skolem sks))
642 return $ replaceTypeVars m ty
571 return $ replaceTypeVars m ty
643
572
573+check :: M.Map Ident Type -> Value -> Type -> Subst Check ()
574+check m (NumericLiteral _) Number = return ()
575+check m (StringLiteral _) String = return ()
576+check m (BooleanLiteral _) Boolean = return ()
577+check m (Unary Negate val) Number = check m val Number
578+check m (Unary Not val) Boolean = check m val Boolean
579+check m (Unary BitwiseNot val) Number = check m val Number
580+check m (Binary _ t1 t2) Number = check m t1 Number >> check m t2 Number
581+check m (ArrayLiteral vals) (Array ty) = forM_ vals (\val -> check m val ty)
582+check m (Indexer index vals) ty = check m index Number >> check m vals (Array ty)
583+check m (Abs args ret) (Function argTys retTy) = do
584+ guardWith "Incorrect number of function arguments" (length args == length argTys)
585+ let bindings = M.fromList (zip args argTys)
586+ check (bindings `M.union` m) ret retTy
587+check m (App f xs) ret = do
588+ ft <- infer m f
589+ checkFunctionApplication m ft xs ret
590+check m val (ForAll idents ty) = do
591+ sk <- skolemize idents ty
592+ check m val sk
593+check m val u@(TUnknown _) = do
594+ t <- infer m val
595+ t ~~ u
596+check _ val ty = throwError $ prettyPrintValue val ++ " does not have type " ++ prettyPrintType ty
597+
598+checkFunctionApplication :: M.Map Ident Type -> Type -> [Value] -> Type -> Subst Check ()
599+checkFunctionApplication m (Function argTys retTy) args ret = do
600+ guardWith "Incorrect number of function arguments" (length args == length argTys)
601+ zipWithM (check m) args argTys
602+ ret ~~ retTy
603+checkFunctionApplication m (ForAll idents ty) args ret = do
604+ replaced <- replaceVarsWithUnknowns idents ty
605+ checkFunctionApplication m replaced args ret
606+checkFunctionApplication _ fnTy args ret = throwError $ "Cannot apply function of type "
607+ ++ prettyPrintType fnTy
608+ ++ " to arguments " ++ intercalate ", " (map prettyPrintValue args)
609+ ++ ". Expecting value of type " ++ prettyPrintType ret ++ "."
610+
611+{-
612+ | Binary BinaryOperator Value Value
613+ | ObjectLiteral [(String, Value)]
614+ | Accessor String Value
615+ | ObjectUpdate Value [(String, Value)]
616+ | Var (Qualified Ident)
617+ | IfThenElse Value Value Value
618+ | Block [Statement]
619+ | Constructor (Qualified ProperName)
620+ | Case Value [(Binder, Value)]
621+ | TypedValue Value PolyType
622+-}
src/Language/PureScript/Types.hs+3−2
@@ -18,9 +18,10 @@ module Language.PureScript.Types where
18
18
19import Data.Data
19import Data.Data
20import Language.PureScript.Names
20import Language.PureScript.Names
21+import Language.PureScript.Unknown (Unknown(..))
21
22
22data Type
23data Type
23− = TUnknown Int
24+ = TUnknown (Unknown Type)
24 | Number
25 | Number
25 | String
26 | String
26 | Boolean
27 | Boolean
@@ -37,7 +38,7 @@ data Type
37type PolyType = Type
38type PolyType = Type
38
39
39data Row
40data Row
40− = RUnknown Int
41+ = RUnknown (Unknown Row)
41 | RowVar String
42 | RowVar String
42 | REmpty
43 | REmpty
43 | RCons String Type Row deriving (Show, Eq, Data, Typeable)
44 | RCons String Type Row deriving (Show, Eq, Data, Typeable)
src/Language/PureScript/Unknown.hsnew file+25
@@ -0,0 +1,25 @@
1+-----------------------------------------------------------------------------
2+--
3+-- Module : Language.PureScript.Unknown
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+{-# LANGUAGE DeriveDataTypeable #-}
16+
17+module Language.PureScript.Unknown where
18+
19+import Data.Data
20+import Data.Typeable
21+
22+newtype Unknown t = Unknown { runUnknown :: Int } deriving (Show, Eq, Ord, Data, Typeable)
23+
24+
25+