git.iko.soy/rowtype-yoga/purescript-native
on e7dfe87 help sign in
rowtype-yoga/purescript-native/src/PureScript/TypeChecker/Kinds.hs
184 lines 7.3 kB history raw
1-----------------------------------------------------------------------------
2--
3-- Module : PureScript.TypeChecker.Kinds
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-----------------------------------------------------------------------------
15{-# LANGUAGE DeriveDataTypeable #-}
17module PureScript.TypeChecker.Kinds (
18 KindConstraint(..),
19 KindSolution(..),
20 kindsOf,
21 kindOf
22) where
24import Data.List
25import Data.Maybe (fromMaybe)
26import Data.Function
27import Data.Data
29import PureScript.Types
30import PureScript.Kinds
31import PureScript.Declarations
32import PureScript.TypeChecker.Monad
33import PureScript.CodeGen.Pretty.Kinds
34import PureScript.CodeGen.Pretty.Types
36import Control.Monad.State
37import Control.Monad.Error
39import Control.Applicative
40import Control.Arrow (Kleisli(..), (***))
41import qualified Control.Category as C
43import qualified Data.Map as M
45data KindConstraintOrigin
46 = DataDeclOrigin
47 | TypeOrigin Type
48 | RowOrigin Row deriving (Show, Data, Typeable)
50prettyPrintKindConstraintOrigin :: KindConstraintOrigin -> String
51prettyPrintKindConstraintOrigin (DataDeclOrigin) = "data declaration"
52prettyPrintKindConstraintOrigin (TypeOrigin ty) = prettyPrintType ty
53prettyPrintKindConstraintOrigin (RowOrigin row) = prettyPrintRow row
55data KindConstraint = KindConstraint Int Kind KindConstraintOrigin deriving (Show, Data, Typeable)
57newtype KindSolution = KindSolution { runKindSolution :: Int -> Kind }
59emptyKindSolution :: KindSolution
60emptyKindSolution = KindSolution KUnknown
62kindOf :: PolyType -> Check Kind
63kindOf (PolyType idents ty) = do
64 ns <- replicateM (length idents) fresh
65 (cs, n, m) <- kindConstraints (M.fromList (zip idents ns)) ty
66 solution <- solveKindConstraints cs emptyKindSolution
67 return $ starIfUnknown $ runKindSolution solution n
69kindsOf :: Maybe String -> [String] -> [Type] -> Check Kind
70kindsOf name args ts = do
71 tyCon <- fresh
72 nargs <- replicateM (length args) fresh
73 (cs, ns, m) <- kindConstraintsAll (maybe id (flip M.insert tyCon) name $ M.fromList (zipWith (,) args nargs)) ts
74 let extraConstraints =
75 KindConstraint tyCon (foldr FunKind Star (map KUnknown nargs)) DataDeclOrigin
76 : zipWith (\n arg -> KindConstraint n Star (TypeOrigin arg)) ns ts
77 solution <- solveKindConstraints (extraConstraints ++ cs) emptyKindSolution
78 return $ starIfUnknown $ runKindSolution solution tyCon
80starIfUnknown :: Kind -> Kind
81starIfUnknown (KUnknown _) = Star
82starIfUnknown (FunKind k1 k2) = FunKind (starIfUnknown k1) (starIfUnknown k2)
83starIfUnknown k = k
85kindConstraintsAll :: M.Map String Int -> [Type] -> Check ([KindConstraint], [Int], M.Map String Int)
86kindConstraintsAll m [] = return ([], [], m)
87kindConstraintsAll m (t:ts) = do
88 (cs, n1, m') <- kindConstraints m t
89 (cs', ns, m'') <- kindConstraintsAll m' ts
90 return ((KindConstraint n1 Star (TypeOrigin t)) : cs ++ cs', n1:ns, m'')
92kindConstraints :: M.Map String Int -> Type -> Check ([KindConstraint], Int, M.Map String Int)
93kindConstraints m a@(Array t) = do
94 me <- fresh
95 (cs, n1, m') <- kindConstraints m t
96 return ((KindConstraint n1 Star (TypeOrigin t)) : (KindConstraint me Star (TypeOrigin a)) : cs, me, m')
97kindConstraints m o@(Object row) = do
98 me <- fresh
99 (cs, r, m') <- kindConstraintsForRow m row
100 return ((KindConstraint me Star (TypeOrigin o)) : (KindConstraint r Row (RowOrigin row)) : cs, me, m')
101kindConstraints m f@(Function args ret) = do
102 me <- fresh
103 (cs, ns, m') <- kindConstraintsAll m args
104 (cs', retN, m'') <- kindConstraints m' ret
105 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'')
106kindConstraints m (TypeVar v) = do
107 case M.lookup v m of
108 Just u -> return ([], u, m)
109 Nothing -> throwError $ "Unbound type variable " ++ v
110kindConstraints m c@(TypeConstructor v) = do
111 env <- getEnv
112 me <- fresh
113 case M.lookup v m of
114 Nothing -> case M.lookup v (types env) of
115 Nothing -> throwError $ "Unknown type constructor '" ++ v ++ "'"
116 Just (kind, _) -> return ([KindConstraint me kind (TypeOrigin c)], me, m)
117 Just u -> do
118 return ([KindConstraint me (KUnknown u) (TypeOrigin c)], me, m)
119kindConstraints m a@(TypeApp t1 t2) = do
120 me <- fresh
121 (cs1, n1, m1) <- kindConstraints m t1
122 (cs2, n2, m2) <- kindConstraints m1 t2
123 return ((KindConstraint n1 (FunKind (KUnknown n2) (KUnknown me)) (TypeOrigin a)) : cs1 ++ cs2, me, m2)
124kindConstraints m t = do
125 me <- fresh
126 return ([KindConstraint me Star (TypeOrigin t)], me, m)
128kindConstraintsForRow :: M.Map String Int -> Row -> Check ([KindConstraint], Int, M.Map String Int)
129kindConstraintsForRow m r@(RowVar v) = do
130 me <- case M.lookup v m of
131 Just u -> return u
132 Nothing -> fresh
133 return ([KindConstraint me Row (RowOrigin r)], me, M.insert v me m)
134kindConstraintsForRow m r@REmpty = do
135 me <- fresh
136 return ([KindConstraint me Row (RowOrigin r)], me, m)
137kindConstraintsForRow m r@(RCons _ ty row) = do
138 me <- fresh
139 (cs1, n1, m1) <- kindConstraints m ty
140 (cs2, n2, m2) <- kindConstraintsForRow m1 row
141 return ((KindConstraint me Row (RowOrigin r)) : (KindConstraint n1 Star (TypeOrigin ty)) : (KindConstraint n2 Row (RowOrigin r)) : cs1 ++ cs2, me, m2)
143solveKindConstraints :: [KindConstraint] -> KindSolution -> Check KindSolution
144solveKindConstraints [] s = return s
145solveKindConstraints all@(KindConstraint n k t : cs) s = do
146 (cs', s') <- rethrow (\err -> "Error in " ++ prettyPrintKindConstraintOrigin t ++ ": " ++ err) $ do
147 guardWith "Occurs check failed" $ not $ kindOccursCheck False n k
148 let s' = KindSolution $ replaceUnknownKind n k . runKindSolution s
149 cs' <- fmap concat $ mapM (substituteKindConstraint n k) cs
150 return (cs', s')
151 solveKindConstraints cs' s'
153substituteKindConstraint :: Int -> Kind -> KindConstraint -> Check [KindConstraint]
154substituteKindConstraint n k (KindConstraint m l t)
155 | n == m = unifyKinds t k l
156 | otherwise = return [KindConstraint m (replaceUnknownKind n k l) t]
158replaceUnknownKind :: Int -> Kind -> Kind -> Kind
159replaceUnknownKind n k = f
160 where
161 f (KUnknown m) | m == n = k
162 f (FunKind k1 k2) = FunKind (f k2) (f k2)
163 f other = other
165unifyKinds :: KindConstraintOrigin -> Kind -> Kind -> Check [KindConstraint]
166unifyKinds _ (KUnknown u1) (KUnknown u2) | u1 == u2 = return []
167unifyKinds t (KUnknown u) k = do
168 guardWith "Occurs check failed" $ not $ kindOccursCheck False u k
169 return [KindConstraint u k t]
170unifyKinds t k (KUnknown u) = do
171 guardWith "Occurs check failed" $ not $ kindOccursCheck False u k
172 return [KindConstraint u k t]
173unifyKinds _ Star Star = return []
174unifyKinds _ Row Row = return []
175unifyKinds t (FunKind k1 k2) (FunKind k3 k4) = do
176 cs1 <- unifyKinds t k1 k3
177 cs2 <- unifyKinds t k2 k4
178 return $ cs1 ++ cs2
179unifyKinds _ k1 k2 = throwError $ "Cannot unify " ++ prettyPrintKind k1 ++ " with " ++ prettyPrintKind k2 ++ "."
181kindOccursCheck :: Bool -> Int -> Kind -> Bool
182kindOccursCheck b u (KUnknown u') | u == u' = b
183kindOccursCheck _ u (FunKind k1 k2) = kindOccursCheck True u k1 || kindOccursCheck True u k2
184kindOccursCheck _ _ _ = False