git.iko.soy/rowtype-yoga/purescript-native
on 73a773e help sign in
rowtype-yoga/purescript-native/src/PureScript/TypeChecker/Kinds.hs
169 lines 6.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-----------------------------------------------------------------------------
15module PureScript.TypeChecker.Kinds (
16 KindConstraint(..),
17 KindSolution(..),
18 kindsOf,
19 kindOf
20) where
22import Data.List
23import Data.Maybe (fromMaybe)
24import Data.Function
26import PureScript.Types
27import PureScript.Kinds
28import PureScript.Declarations
29import PureScript.TypeChecker.Monad
30import PureScript.CodeGen.Pretty.Kinds
32import Control.Monad.State
33import Control.Monad.Error
35import Control.Applicative
36import Control.Arrow (Kleisli(..), (***))
37import qualified Control.Category as C
39import qualified Data.Map as M
41data KindConstraint = KindConstraint Int Kind
43instance Show KindConstraint where
44 show (KindConstraint n k) = show n ++ " = " ++ show k
46newtype KindSolution = KindSolution { runKindSolution :: Int -> Kind }
48emptyKindSolution :: KindSolution
49emptyKindSolution = KindSolution KUnknown
51kindOf :: PolyType -> Check Kind
52kindOf (PolyType idents ty) = do
53 ns <- replicateM (length idents) fresh
54 (cs, n, m) <- kindConstraints (M.fromList (zip idents ns)) ty
55 solution <- solveKindConstraints cs emptyKindSolution
56 return $ starIfUnknown $ runKindSolution solution n
58kindsOf :: Maybe String -> [String] -> [Type] -> Check Kind
59kindsOf name args ts = do
60 tyCon <- fresh
61 nargs <- replicateM (length args) fresh
62 (cs, ns, m) <- kindConstraintsAll (maybe id (flip M.insert tyCon) name $ M.fromList (zipWith (,) args nargs)) ts
63 let extraConstraints = KindConstraint tyCon (foldr FunKind Star (map KUnknown nargs)) : map (flip KindConstraint Star) ns
64 solution <- solveKindConstraints (extraConstraints ++ cs) emptyKindSolution
65 return $ starIfUnknown $ runKindSolution solution tyCon
67starIfUnknown :: Kind -> Kind
68starIfUnknown (KUnknown _) = Star
69starIfUnknown (FunKind k1 k2) = FunKind (starIfUnknown k1) (starIfUnknown k2)
70starIfUnknown k = k
72kindConstraintsAll :: M.Map String Int -> [Type] -> Check ([KindConstraint], [Int], M.Map String Int)
73kindConstraintsAll m [] = return ([], [], m)
74kindConstraintsAll m (t:ts) = do
75 (cs, n1, m') <- kindConstraints m t
76 (cs', ns, m'') <- kindConstraintsAll m' ts
77 return ((KindConstraint n1 Star) : cs ++ cs', n1:ns, m'')
79kindConstraints :: M.Map String Int -> Type -> Check ([KindConstraint], Int, M.Map String Int)
80kindConstraints m (Array t) = do
81 me <- fresh
82 (cs, n1, m') <- kindConstraints m t
83 return ((KindConstraint n1 Star) : (KindConstraint me Star) : cs, me, m')
84kindConstraints m (Object row) = do
85 me <- fresh
86 (cs, row, m') <- kindConstraintsForRow m row
87 return ((KindConstraint me Star) : (KindConstraint row Row) : cs, me, m')
88kindConstraints m (Function args ret) = do
89 me <- fresh
90 (cs, ns, m') <- kindConstraintsAll m args
91 (cs', retN, m'') <- kindConstraints m' ret
92 return ((KindConstraint retN Star) : (KindConstraint me Star) : (map (flip KindConstraint Star) ns) ++ cs, me, m'')
93kindConstraints m (TypeVar v) = do
94 case M.lookup v m of
95 Just u -> return ([], u, m)
96 Nothing -> throwError $ "Unbound type variable " ++ v
97kindConstraints m (TypeConstructor v) = do
98 env <- getEnv
99 me <- fresh
100 case M.lookup v m of
101 Nothing -> case M.lookup v (types env) of
102 Nothing -> throwError $ "Unknown type constructor '" ++ v ++ "'"
103 Just (kind, _) -> return ([KindConstraint me kind], me, m)
104 Just u -> do
105 return ([KindConstraint me (KUnknown u)], me, m)
106kindConstraints m (TypeApp t1 t2) = do
107 me <- fresh
108 (cs1, n1, m1) <- kindConstraints m t1
109 (cs2, n2, m2) <- kindConstraints m1 t2
110 return ((KindConstraint n1 (FunKind (KUnknown n2) (KUnknown me))) : cs1 ++ cs2, me, m2)
111kindConstraints m _ = do
112 me <- fresh
113 return ([KindConstraint me Star], me, m)
115kindConstraintsForRow :: M.Map String Int -> Row -> Check ([KindConstraint], Int, M.Map String Int)
116kindConstraintsForRow m (RowVar v) = do
117 me <- case M.lookup v m of
118 Just u -> return u
119 Nothing -> fresh
120 return ([KindConstraint me Row], me, M.insert v me m)
121kindConstraintsForRow m REmpty = do
122 me <- fresh
123 return ([KindConstraint me Row], me, m)
124kindConstraintsForRow m (RCons _ ty row) = do
125 me <- fresh
126 (cs1, n1, m1) <- kindConstraints m ty
127 (cs2, n2, m2) <- kindConstraintsForRow m1 row
128 return ((KindConstraint me Row) : (KindConstraint n1 Star) : (KindConstraint n2 Row) : cs1 ++ cs2, me, m2)
130solveKindConstraints :: [KindConstraint] -> KindSolution -> Check KindSolution
131solveKindConstraints [] s = return s
132solveKindConstraints all@(KindConstraint n k:cs) s = do
133 guardWith "Occurs check failed" $ not $ kindOccursCheck False n k
134 let s' = KindSolution $ replaceUnknownKind n k . runKindSolution s
135 cs' <- fmap concat $ mapM (substituteKindConstraint n k) cs
136 solveKindConstraints cs' s'
138substituteKindConstraint :: Int -> Kind -> KindConstraint -> Check [KindConstraint]
139substituteKindConstraint n k (KindConstraint m l)
140 | n == m = unifyKinds k l
141 | otherwise = return [KindConstraint m (replaceUnknownKind n k l)]
143replaceUnknownKind :: Int -> Kind -> Kind -> Kind
144replaceUnknownKind n k = f
145 where
146 f (KUnknown m) | m == n = k
147 f (FunKind k1 k2) = FunKind (f k2) (f k2)
148 f other = other
150unifyKinds :: Kind -> Kind -> Check [KindConstraint]
151unifyKinds (KUnknown u1) (KUnknown u2) | u1 == u2 = return []
152unifyKinds (KUnknown u) k = do
153 guardWith "Occurs check failed" $ not $ kindOccursCheck False u k
154 return [KindConstraint u k]
155unifyKinds k (KUnknown u) = do
156 guardWith "Occurs check failed" $ not $ kindOccursCheck False u k
157 return [KindConstraint u k]
158unifyKinds Star Star = return []
159unifyKinds Row Row = return []
160unifyKinds (FunKind k1 k2) (FunKind k3 k4) = do
161 cs1 <- unifyKinds k1 k3
162 cs2 <- unifyKinds k2 k4
163 return $ cs1 ++ cs2
164unifyKinds k1 k2 = throwError $ "Cannot unify " ++ prettyPrintKind k1 ++ " with " ++ prettyPrintKind k2 ++ "."
166kindOccursCheck :: Bool -> Int -> Kind -> Bool
167kindOccursCheck b u (KUnknown u') | u == u' = b
168kindOccursCheck _ u (FunKind k1 k2) = kindOccursCheck True u k1 || kindOccursCheck True u k2
169kindOccursCheck _ _ _ = False