git.iko.soy/rowtype-yoga/purescript-native
on ea83764 help sign in
rowtype-yoga/purescript-native/src/PureScript/TypeChecker/Kinds.hs
183 lines 7.2 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 (`M.insert` tyCon) name $ M.fromList (zip args nargs)) ts
74 let extraConstraints =
75 KindConstraint tyCon (foldr (FunKind . KUnknown) Star 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) =
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 -> return ([KindConstraint me (KUnknown u) (TypeOrigin c)], me, m)
118kindConstraints m a@(TypeApp t1 t2) = do
119 me <- fresh
120 (cs1, n1, m1) <- kindConstraints m t1
121 (cs2, n2, m2) <- kindConstraints m1 t2
122 return (KindConstraint n1 (FunKind (KUnknown n2) (KUnknown me)) (TypeOrigin a) : cs1 ++ cs2, me, m2)
123kindConstraints m t = do
124 me <- fresh
125 return ([KindConstraint me Star (TypeOrigin t)], me, m)
127kindConstraintsForRow :: M.Map String Int -> Row -> Check ([KindConstraint], Int, M.Map String Int)
128kindConstraintsForRow m r@(RowVar v) = do
129 me <- case M.lookup v m of
130 Just u -> return u
131 Nothing -> fresh
132 return ([KindConstraint me Row (RowOrigin r)], me, M.insert v me m)
133kindConstraintsForRow m r@REmpty = do
134 me <- fresh
135 return ([KindConstraint me Row (RowOrigin r)], me, m)
136kindConstraintsForRow m r@(RCons _ ty row) = do
137 me <- fresh
138 (cs1, n1, m1) <- kindConstraints m ty
139 (cs2, n2, m2) <- kindConstraintsForRow m1 row
140 return (KindConstraint me Row (RowOrigin r) : KindConstraint n1 Star (TypeOrigin ty) : KindConstraint n2 Row (RowOrigin r) : cs1 ++ cs2, me, m2)
142solveKindConstraints :: [KindConstraint] -> KindSolution -> Check KindSolution
143solveKindConstraints [] s = return s
144solveKindConstraints all@(KindConstraint n k t : cs) s = do
145 (cs', s') <- rethrow (\err -> "Error in " ++ prettyPrintKindConstraintOrigin t ++ ": " ++ err) $ do
146 guardWith "Occurs check failed" $ not $ kindOccursCheck False n k
147 let s' = KindSolution $ replaceUnknownKind n k . runKindSolution s
148 cs' <- fmap concat $ mapM (substituteKindConstraint n k) cs
149 return (cs', s')
150 solveKindConstraints cs' s'
152substituteKindConstraint :: Int -> Kind -> KindConstraint -> Check [KindConstraint]
153substituteKindConstraint n k (KindConstraint m l t)
154 | n == m = unifyKinds t k l
155 | otherwise = return [KindConstraint m (replaceUnknownKind n k l) t]
157replaceUnknownKind :: Int -> Kind -> Kind -> Kind
158replaceUnknownKind n k = f
159 where
160 f (KUnknown m) | m == n = k
161 f (FunKind k1 k2) = FunKind (f k2) (f k2)
162 f other = other
164unifyKinds :: KindConstraintOrigin -> Kind -> Kind -> Check [KindConstraint]
165unifyKinds _ (KUnknown u1) (KUnknown u2) | u1 == u2 = return []
166unifyKinds t (KUnknown u) k = do
167 guardWith "Occurs check failed" $ not $ kindOccursCheck False u k
168 return [KindConstraint u k t]
169unifyKinds t k (KUnknown u) = do
170 guardWith "Occurs check failed" $ not $ kindOccursCheck False u k
171 return [KindConstraint u k t]
172unifyKinds _ Star Star = return []
173unifyKinds _ Row Row = return []
174unifyKinds t (FunKind k1 k2) (FunKind k3 k4) = do
175 cs1 <- unifyKinds t k1 k3
176 cs2 <- unifyKinds t k2 k4
177 return $ cs1 ++ cs2
178unifyKinds _ k1 k2 = throwError $ "Cannot unify " ++ prettyPrintKind k1 ++ " with " ++ prettyPrintKind k2 ++ "."
180kindOccursCheck :: Bool -> Int -> Kind -> Bool
181kindOccursCheck b u (KUnknown u') | u == u' = b
182kindOccursCheck _ u (FunKind k1 k2) = kindOccursCheck True u k1 || kindOccursCheck True u k2
183kindOccursCheck _ _ _ = False