@@ -14,19 +14,22 @@
1414-----------------------------------------------------------------------------
1515
1616{-# OPTIONS_GHC -fno-warn-orphans #-}
17−{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}
17+{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, TupleSections #-}
1818
1919module Language.PureScript.TypeChecker.Kinds (
2020 kindOf,
21+ kindOfWithScopedVars,
2122 kindsOf,
2223 kindsOfAll
2324) where
2425
2526import Data.Maybe (fromMaybe)
2627import Data.Monoid ((<>))
28+
2729import qualified Data.HashMap.Strict as H
2830import qualified Data.Map as M
2931
32+import Control.Arrow (second)
3033import Control.Applicative
3134import Control.Monad.Error
3235import Control.Monad.State
@@ -69,11 +72,19 @@ instance Unifiable Check Kind where
6972-- Infer the kind of a single type
7073--
7174kindOf :: ModuleName -> Type -> Check Kind
72−kindOf _ ty =
75+kindOf _ ty = fst <$> kindOfWithScopedVars ty
76+
77+-- |
78+-- Infer the kind of a single type, returning the kinds of any scoped type variables
79+--
80+kindOfWithScopedVars :: Type -> Check (Kind, [(String, Kind)])
81+kindOfWithScopedVars ty =
7382 rethrow (mkErrorStack "Error checking kind" (Just (TypeError ty)) <>) $
74− fmap (starIfUnknown . tidyUp) . liftUnify $ infer ty
83+ fmap tidyUp . liftUnify $ infer ty
7584 where
76− tidyUp (k, sub) = sub $? k
85+ tidyUp ((k, args), sub) = ( starIfUnknown (sub $? k)
86+ , map (second (starIfUnknown . (sub $?))) args
87+ )
7788
7889-- |
7990-- Infer the kind of a type constructor with a collection of arguments and a collection of associated data constructors
@@ -125,7 +136,7 @@ kindsOfAll moduleName syns tys = fmap tidyUp . liftUnify $ do
125136--
126137solveTypes :: Bool -> [Type] -> [Kind] -> Kind -> UnifyT Kind Check Kind
127138solveTypes isData ts kargs tyCon = do
128− ks <- mapM infer ts
139+ ks <- mapM (fmap fst . infer) ts
129140 when isData $ do
130141 tyCon =?= foldr FunKind Star kargs
131142 forM_ ks $ \k -> k =?= Star
@@ -145,48 +156,64 @@ starIfUnknown k = k
145156-- |
146157-- Infer a kind for a type
147158--
148−infer :: Type -> UnifyT Kind Check Kind
159+infer :: Type -> UnifyT Kind Check (Kind, [(String, Kind)])
149160infer ty = rethrow (mkErrorStack "Error inferring type of value" (Just (TypeError ty)) <>) $ infer' ty
150161
151−infer' :: Type -> UnifyT Kind Check Kind
152−infer' TypeWildcard = fresh
153−infer' (TypeVar v) = do
154− Just moduleName <- checkCurrentModule <$> get
155− UnifyT . lift $ lookupTypeVariable moduleName (Qualified Nothing (ProperName v))
156−infer' c@(TypeConstructor v) = do
157− env <- liftCheck getEnv
158− case M.lookup v (types env) of
159− Nothing -> UnifyT . lift . throwError $ mkErrorStack "Unknown type constructor" (Just (TypeError c))
160− Just (kind, _) -> return kind
161−infer' (TypeApp t1 t2) = do
162− k0 <- fresh
163− k1 <- infer t1
164− k2 <- infer t2
165− k1 =?= FunKind k2 k0
166− return k0
162+infer' :: Type -> UnifyT Kind Check (Kind, [(String, Kind)])
167163infer' (ForAll ident ty _) = do
168164 k1 <- fresh
169165 Just moduleName <- checkCurrentModule <$> get
170− k2 <- bindLocalTypeVariables moduleName [(ProperName ident, k1)] $ infer ty
166+ (k2, args) <- bindLocalTypeVariables moduleName [(ProperName ident, k1)] $ infer ty
171167 k2 =?= Star
172− return Star
173−infer' REmpty = do
174− k <- fresh
175− return $ Row k
176−infer' (RCons _ ty row) = do
177− k1 <- infer ty
178− k2 <- infer row
179− k2 =?= Row k1
180− return $ Row k1
181−infer' (ConstrainedType deps ty) = do
182− forM_ deps $ \(className, tys) -> do
183− _ <- infer $ foldl TypeApp (TypeConstructor className) tys
184− return ()
185− k <- infer ty
186− k =?= Star
187− return Star
168+ return (Star, (ident, k1) : args)
188169infer' (KindedType ty k) = do
189− k' <- infer ty
170+ (k', args) <- infer ty
190171 k =?= k'
191− return k'
192−infer' _ = error "Invalid argument to infer"
172+ return (k', args)
173+infer' other = (, []) <$> go other
174+ where
175+ go :: Type -> UnifyT Kind Check Kind
176+ go (ForAll ident ty _) = do
177+ k1 <- fresh
178+ Just moduleName <- checkCurrentModule <$> get
179+ k2 <- bindLocalTypeVariables moduleName [(ProperName ident, k1)] $ go ty
180+ k2 =?= Star
181+ return Star
182+ go (KindedType ty k) = do
183+ k' <- go ty
184+ k =?= k'
185+ return k'
186+ go TypeWildcard = fresh
187+ go (TypeVar v) = do
188+ Just moduleName <- checkCurrentModule <$> get
189+ UnifyT . lift $ lookupTypeVariable moduleName (Qualified Nothing (ProperName v))
190+ go (Skolem v _ _) = do
191+ Just moduleName <- checkCurrentModule <$> get
192+ UnifyT . lift $ lookupTypeVariable moduleName (Qualified Nothing (ProperName v))
193+ go c@(TypeConstructor v) = do
194+ env <- liftCheck getEnv
195+ case M.lookup v (types env) of
196+ Nothing -> UnifyT . lift . throwError $ mkErrorStack "Unknown type constructor" (Just (TypeError c))
197+ Just (kind, _) -> return kind
198+ go (TypeApp t1 t2) = do
199+ k0 <- fresh
200+ k1 <- go t1
201+ k2 <- go t2
202+ k1 =?= FunKind k2 k0
203+ return k0
204+ go REmpty = do
205+ k <- fresh
206+ return $ Row k
207+ go (RCons _ ty row) = do
208+ k1 <- go ty
209+ k2 <- go row
210+ k2 =?= Row k1
211+ return $ Row k1
212+ go (ConstrainedType deps ty) = do
213+ forM_ deps $ \(className, tys) -> do
214+ _ <- go $ foldl TypeApp (TypeConstructor className) tys
215+ return ()
216+ k <- go ty
217+ k =?= Star
218+ return Star
219+ go _ = error "Invalid argument to infer"