@@ -35,65 +35,82 @@ import qualified Control.Category as C
3535
3636import qualified Data.Map as M
3737
38−data KindConstraint = KindConstraint Int Kind deriving Show
38+data KindConstraint = KindConstraint Int Kind
39+
40+instance Show KindConstraint where
41+ show (KindConstraint n k) = show n ++ " = " ++ show k
3942
4043newtype KindSolution = KindSolution { runKindSolution :: Int -> Kind }
4144
4245emptyKindSolution :: KindSolution
4346emptyKindSolution = KindSolution KUnknown
4447
45−kindsOf :: [String] -> [Type] -> Check [Kind]
46−kindsOf args ts = do
47− (cs, _, m) <- kindConstraintsAll 0 M.empty ts
48− solution <- solveKindConstraints cs emptyKindSolution
49− return $ map (maybe Star starIfUnknown . fmap (runKindSolution solution) . flip M.lookup m) args
48+kindsOf :: String -> [String] -> [Type] -> Check Kind
49+kindsOf name args ts = do
50+ let tyCon = 0
51+ let nargs = [1..length args]
52+ (cs, ns, _, m) <- kindConstraintsAll (length args + 1) (M.insert name tyCon $ M.fromList (zipWith (,) args nargs)) ts
53+ let extraConstraints = KindConstraint tyCon (foldr FunKind Star (map KUnknown nargs)) : map (flip KindConstraint Star) ns
54+ solution <- solveKindConstraints (extraConstraints ++ cs) emptyKindSolution
55+ return $ starIfUnknown $ runKindSolution solution 0
5056
5157starIfUnknown :: Kind -> Kind
5258starIfUnknown (KUnknown _) = Star
5359starIfUnknown (FunKind k1 k2) = FunKind (starIfUnknown k1) (starIfUnknown k2)
5460starIfUnknown k = k
5561
56−kindConstraintsAll :: Int -> M.Map String Int -> [Type] -> Check ([KindConstraint], [Int], M.Map String Int)
57−kindConstraintsAll _ m [] = return ([], [], m)
62+kindConstraintsAll :: Int -> M.Map String Int -> [Type] -> Check ([KindConstraint], [Int], Int, M.Map String Int)
63+kindConstraintsAll n m [] = return ([], [], n, m)
5864kindConstraintsAll n m (t:ts) = do
59− (cs, n', m') <- kindConstraints n m t
60− (cs', ns, m'') <- kindConstraintsAll (n' + 1) m' ts
61− return ((KindConstraint n' Star) : cs ++ cs', n':ns, m'')
65+ (cs, n1, max1, m') <- kindConstraints n m t
66+ (cs', ns, max2, m'') <- kindConstraintsAll (max1 + 1) m' ts
67+ return ((KindConstraint n1 Star) : cs ++ cs', n1:ns, max2, m'')
6268
63−kindConstraints :: Int -> M.Map String Int -> Type -> Check ([KindConstraint], Int, M.Map String Int)
69+kindConstraints :: Int -> M.Map String Int -> Type -> Check ([KindConstraint], Int, Int, M.Map String Int)
6470kindConstraints n m (Array t) = do
65− (cs, n', m') <- kindConstraints n m t
66− return ((KindConstraint n' Star) : (KindConstraint (n' + 1) Star) : cs, n' + 1, m')
71+ let me = n
72+ (cs, n1, max1, m') <- kindConstraints (n + 1) m t
73+ return ((KindConstraint n1 Star) : (KindConstraint me Star) : cs, me, max1, m')
6774kindConstraints n m (Object row) = do
6875 let me = n
69− (cs, row, m') <- kindConstraintsForRow (n + 2) m row
70− return ((KindConstraint me Star) : (KindConstraint row Row) : cs, me, m')
76+ (cs, row, max1, m') <- kindConstraintsForRow (n + 1) m row
77+ return ((KindConstraint me Star) : (KindConstraint row Row) : cs, me, max1, m')
7178kindConstraints n m (Function args ret) = do
72− (cs, ns, m') <- kindConstraintsAll n m args
73− let next = maximum ns + 1
74− (cs', retN, m'') <- kindConstraints next m' ret
75− let me = retN + 1
76− return ((KindConstraint retN Star) : (KindConstraint me Star) : (map (flip KindConstraint Star) ns) ++ cs, me, m'')
79+ let me = n
80+ (cs, ns, max1, m') <- kindConstraintsAll (n + 1) m args
81+ (cs', retN, max2, m'') <- kindConstraints (max1 + 1) m' ret
82+ return ((KindConstraint retN Star) : (KindConstraint me Star) : (map (flip KindConstraint Star) ns) ++ cs, me, max2, m'')
7783kindConstraints n m (TypeVar v) =
78− let
79− n' = maybe n id (M.lookup v m)
80− in return ([], n', M.insert v n' m)
84+ let n' = maybe n id (M.lookup v m)
85+ in return ([], n', n, M.insert v n' m)
8186kindConstraints n m (TypeConstructor v) = do
8287 env <- get
83− kind <- maybe (throwError "Unknown type constructor") return (M.lookup v (types env))
84− return ([KindConstraint n kind], n, m)
88+ kind <- case M.lookup v m of
89+ Nothing -> case M.lookup v (types env) of
90+ Nothing -> throwError $ "Unknown type constructor '" ++ v ++ "'"
91+ Just k -> return k
92+ Just u -> return (KUnknown u)
93+ return ([KindConstraint n kind], n, n, m)
8594kindConstraints n m (TypeApp t1 t2) = do
86− (cs1, n1, m1) <- kindConstraints n m t1
87− (cs2, n2, m2) <- kindConstraints (n1 + 1) m1 t2
88− return ((KindConstraint n1 (FunKind (KUnknown n2) (KUnknown (n2 + 1)))) : cs1 ++ cs2, n2 + 1, m2)
89−kindConstraints n m _ = return ([KindConstraint n Star], n, m)
90−
91−kindConstraintsForRow :: Int -> M.Map String Int -> Row -> Check ([KindConstraint], Int, M.Map String Int)
92−kindConstraintsForRow = undefined
95+ let me = n
96+ (cs1, n1, max1, m1) <- kindConstraints (n + 1) m t1
97+ (cs2, n2, max2, m2) <- kindConstraints (max1 + 1) m1 t2
98+ return ((KindConstraint n1 (FunKind (KUnknown n2) (KUnknown me))) : cs1 ++ cs2, me, max2, m2)
99+kindConstraints n m _ = return ([KindConstraint n Star], n, n, m)
100+
101+kindConstraintsForRow :: Int -> M.Map String Int -> Row -> Check ([KindConstraint], Int, Int, M.Map String Int)
102+kindConstraintsForRow n m (RowVar v) =
103+ let n' = maybe n id (M.lookup v m)
104+ in return ([KindConstraint n' Row], n', n, M.insert v n' m)
105+kindConstraintsForRow n m REmpty = return ([KindConstraint n Row], n, n, m)
106+kindConstraintsForRow n m (RCons _ ty row) = do
107+ (cs1, n1, max1, m1) <- kindConstraints (n + 1) m ty
108+ (cs2, n2, max2, m2) <- kindConstraintsForRow (max1 + 1) m1 row
109+ return ((KindConstraint n Row) : (KindConstraint n1 Star) : (KindConstraint n2 Row) : cs1 ++ cs2, n, max2, m2)
93110
94111solveKindConstraints :: [KindConstraint] -> KindSolution -> Check KindSolution
95112solveKindConstraints [] s = return s
96−solveKindConstraints (KindConstraint n k:cs) s = do
113+solveKindConstraints all@(KindConstraint n k:cs) s = do
97114 guardWith "Occurs check failed" $ not $ kindOccursCheck n k
98115 let s' = KindSolution $ replaceUnknownKind n k . runKindSolution s
99116 cs' <- fmap concat $ mapM (substituteKindConstraint n k) cs
@@ -112,6 +129,7 @@ replaceUnknownKind n k = f
112129 f other = other
113130
114131unifyKinds :: Kind -> Kind -> Check [KindConstraint]
132+unifyKinds (KUnknown u1) (KUnknown u2) | u1 == u2 = return []
115133unifyKinds (KUnknown u) k = do
116134 guardWith "Occurs check failed" $ not $ kindOccursCheck u k
117135 return [KindConstraint u k]
@@ -119,6 +137,7 @@ unifyKinds k (KUnknown u) = do
119137 guardWith "Occurs check failed" $ not $ kindOccursCheck u k
120138 return [KindConstraint u k]
121139unifyKinds Star Star = return []
140+unifyKinds Row Row = return []
122141unifyKinds (FunKind k1 k2) (FunKind k3 k4) = do
123142 cs1 <- unifyKinds k1 k3
124143 cs2 <- unifyKinds k2 k4