1321173 · rowtype-yoga/purescript-native

git.iko.soy/rowtype-yoga/purescript-native

on golang help sign in

Merge pull request #866 from purescript/scoped-type-vars

1321173Phil Freeman12 years ago

examples/passing/ScopedTypeVariables.pursnew file+34

compare with golang

unifiedsplit

@@ -0,0 +1,34 @@

1+module Main where

3+test1 :: forall a. (a -> a) -> a -> a

4+test1 f x = g (g x)

5+ where

6+ g :: a -> a

7+ g y = f (f y)

9+test2 :: forall a. (a -> a) -> a -> a

10+test2 = h

11+ where

12+ h :: forall b. (b -> b) -> b -> b

13+ h f x = g (g x)

14+ where

15+ g :: b -> b

16+ g y = f (f y)

17+

18+test3 :: Number

19+test3 = ((\b -> b :: b) :: forall b. b -> b) 0

20+

21+test4 :: forall a. (a -> a) -> a -> a

22+test4 = h

23+ where

24+ h :: forall b. (b -> b) -> b -> b

25+ h f x = g (g x)

26+ where

27+ g :: b -> b

28+ g y = j (f (f y))

29+ where

30+ j :: forall b. b -> b

31+ j x = x

32+

33+

34+main = Debug.Trace.trace "Done"

src/Language/PureScript/Environment.hs+6−1

@@ -136,7 +136,12 @@ data TypeKind

136 -- |

137 -- A local type variable

138 --

139+ | LocalTypeVariable

140+ -- |

141+ -- A scoped type variable

142+ --

143+ | ScopedTypeVar

139− | LocalTypeVariable deriving (Show, Eq, Data, Typeable)

144+ deriving (Show, Eq, Data, Typeable)

140

145

141-- |

146-- |

142-- The type ('data' or 'newtype') of a data type declaration

147-- The type ('data' or 'newtype') of a data type declaration

src/Language/PureScript/TypeChecker/Kinds.hs+69−42

@@ -14,19 +14,22 @@

14-----------------------------------------------------------------------------

16{-# OPTIONS_GHC -fno-warn-orphans #-}

17−{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}

17+{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, TupleSections #-}

19module Language.PureScript.TypeChecker.Kinds (

20 kindOf,

21+ kindOfWithScopedVars,

21 kindsOf,

22 kindsOf,

22 kindsOfAll

23 kindsOfAll

23) where

24) where

25import Data.Maybe (fromMaybe)

26import Data.Maybe (fromMaybe)

26import Data.Monoid ((<>))

27import Data.Monoid ((<>))

28+

27import qualified Data.HashMap.Strict as H

29import qualified Data.HashMap.Strict as H

28import qualified Data.Map as M

30import qualified Data.Map as M

32+import Control.Arrow (second)

30import Control.Applicative

33import Control.Applicative

31import Control.Monad.Error

34import Control.Monad.Error

32import Control.Monad.State

35import Control.Monad.State

@@ -69,11 +72,19 @@ instance Unifiable Check Kind where

69-- Infer the kind of a single type

72-- Infer the kind of a single type

70--

73--

71kindOf :: ModuleName -> Type -> Check Kind

74kindOf :: 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 =

73 rethrow (mkErrorStack "Error checking kind" (Just (TypeError ty)) <>) $

82 rethrow (mkErrorStack "Error checking kind" (Just (TypeError ty)) <>) $

74− fmap (starIfUnknown . tidyUp) . liftUnify $ infer ty

83+ fmap tidyUp . liftUnify $ infer ty

75 where

84 where

76− tidyUp (k, sub) = sub $? k

85+ tidyUp ((k, args), sub) = ( starIfUnknown (sub $? k)

86+ , map (second (starIfUnknown . (sub $?))) args

87+ )

78-- |

89-- |

79-- Infer the kind of a type constructor with a collection of arguments and a collection of associated data constructors

90-- 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

125--

136--

126solveTypes :: Bool -> [Type] -> [Kind] -> Kind -> UnifyT Kind Check Kind

137solveTypes :: Bool -> [Type] -> [Kind] -> Kind -> UnifyT Kind Check Kind

127solveTypes isData ts kargs tyCon = do

138solveTypes isData ts kargs tyCon = do

128− ks <- mapM infer ts

139+ ks <- mapM (fmap fst . infer) ts

129 when isData $ do

140 when isData $ do

130 tyCon =?= foldr FunKind Star kargs

141 tyCon =?= foldr FunKind Star kargs

131 forM_ ks $ \k -> k =?= Star

142 forM_ ks $ \k -> k =?= Star

@@ -145,48 +156,64 @@ starIfUnknown k = k

145-- |

156-- |

146-- Infer a kind for a type

157-- Infer a kind for a type

147--

158--

148−infer :: Type -> UnifyT Kind Check Kind

159+infer :: Type -> UnifyT Kind Check (Kind, [(String, Kind)])

149infer ty = rethrow (mkErrorStack "Error inferring type of value" (Just (TypeError ty)) <>) $ infer' ty

160infer ty = rethrow (mkErrorStack "Error inferring type of value" (Just (TypeError ty)) <>) $ infer' ty

150

161

151−infer' :: Type -> UnifyT Kind Check Kind

162+infer' :: Type -> UnifyT Kind Check (Kind, [(String, 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

167infer' (ForAll ident ty _) = do

163infer' (ForAll ident ty _) = do

168 k1 <- fresh

164 k1 <- fresh

169 Just moduleName <- checkCurrentModule <$> get

165 Just moduleName <- checkCurrentModule <$> get

170− k2 <- bindLocalTypeVariables moduleName [(ProperName ident, k1)] $ infer ty

166+ (k2, args) <- bindLocalTypeVariables moduleName [(ProperName ident, k1)] $ infer ty

171 k2 =?= Star

167 k2 =?= Star

172− return Star

168+ return (Star, (ident, k1) : args)

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

188infer' (KindedType ty k) = do

169infer' (KindedType ty k) = do

189− k' <- infer ty

170+ (k', args) <- infer ty

190 k =?= k'

171 k =?= k'

191− return k'

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

192−infer' _ = error "Invalid argument to infer"

219+ go _ = error "Invalid argument to infer"

src/Language/PureScript/TypeChecker/Monad.hs+6

@@ -56,6 +56,12 @@ bindTypes newNames action = do

56 modify $ \st -> st { checkEnv = (checkEnv st) { types = types . checkEnv $ orig } }

57 return a

59+-- |

60+-- Temporarily bind a collection of names to types

61+--

62+withScopedTypeVars :: (Functor m, MonadState CheckState m) => ModuleName -> [(String, Kind)] -> m a -> m a

63+withScopedTypeVars mn ks = bindTypes (M.fromList (map (\(name, k) -> (Qualified (Just mn) (ProperName name), (k, ScopedTypeVar))) ks))

64+

59-- |

65-- |

60-- Temporarily make a collection of type class dictionaries available

66-- Temporarily make a collection of type class dictionaries available

61--

67--

src/Language/PureScript/TypeChecker/Skolems.hs+1

@@ -71,6 +71,7 @@ skolemizeTypesInValue :: String -> Int -> SkolemScope -> Expr -> Expr

71skolemizeTypesInValue ident sko scope = let (_, f, _) = everywhereOnValues id go id in f

72 where

73 go (SuperClassDictionary c ts) = SuperClassDictionary c (map (skolemize ident sko scope) ts)

74+ go (TypedValue check val ty) = TypedValue check val (skolemize ident sko scope ty)

74 go other = other

75 go other = other

76-- |

77-- |

src/Language/PureScript/TypeChecker/Types.hs+16−15

@@ -129,16 +129,16 @@ typeDictionaryForBindingGroup moduleName vals = do

129 return (untyped, typed, dict, untypedDict)

130

131checkTypedBindingGroupElement :: ModuleName -> (Ident, (Expr, Type, Bool)) -> TypeData -> UnifyT Type Check (Ident, (Expr, Type))

132−checkTypedBindingGroupElement moduleName (ident, (val', ty, checkType)) dict = do

132+checkTypedBindingGroupElement mn (ident, (val', ty, checkType)) dict = do

133 -- Replace type wildcards

134 ty' <- replaceTypeWildcards ty

135 -- Kind check

136− kind <- liftCheck $ kindOf moduleName ty

136+ (kind, args) <- liftCheck $ kindOfWithScopedVars ty

137− guardWith (strMsg $ "Expected type of kind *, was " ++ prettyPrintKind kind) $ kind == Star

137+ checkTypeKind kind

138 -- Check the type with the new names in scope

139 ty'' <- introduceSkolemScope <=< replaceAllTypeSynonyms <=< replaceTypeWildcards $ ty'

140 val'' <- if checkType

141− then bindNames dict $ TypedValue True <$> check val' ty'' <*> pure ty''

141+ then withScopedTypeVars mn args $ bindNames dict $ TypedValue True <$> check val' ty'' <*> pure ty''

142 else return (TypedValue False val' ty'')

143 return (ident, (val'', ty''))

144

@@ -183,10 +183,8 @@ replaceTypeClassDictionaries mn =

183-- |

184-- Check the kind of a type, failing if it is not of kind *.

185--

186−checkTypeKind :: ModuleName -> Type -> UnifyT t Check ()

186+checkTypeKind :: Kind -> UnifyT t Check ()

187−checkTypeKind moduleName ty = do

188− kind <- liftCheck $ kindOf moduleName ty

189− guardWith (strMsg $ "Expected type of kind *, was " ++ prettyPrintKind kind) $ kind == Star

187+checkTypeKind kind = guardWith (strMsg $ "Expected type of kind *, was " ++ prettyPrintKind kind) $ kind == Star

190

188

191-- |

189-- |

192-- Remove any ForAlls and ConstrainedType constructors in a type by introducing new unknowns

190-- Remove any ForAlls and ConstrainedType constructors in a type by introducing new unknowns

@@ -293,9 +291,10 @@ infer' (SuperClassDictionary className tys) = do

293 return $ TypeClassDictionary False (className, tys) dicts

291 return $ TypeClassDictionary False (className, tys) dicts

294infer' (TypedValue checkType val ty) = do

292infer' (TypedValue checkType val ty) = do

295 Just moduleName <- checkCurrentModule <$> get

293 Just moduleName <- checkCurrentModule <$> get

296− checkTypeKind moduleName ty

294+ (kind, args) <- liftCheck $ kindOfWithScopedVars ty

295+ checkTypeKind kind

297 ty' <- introduceSkolemScope <=< replaceAllTypeSynonyms <=< replaceTypeWildcards $ ty

296 ty' <- introduceSkolemScope <=< replaceAllTypeSynonyms <=< replaceTypeWildcards $ ty

298− val' <- if checkType then check val ty' else return val

297+ val' <- if checkType then withScopedTypeVars moduleName args (check val ty') else return val

299 return $ TypedValue True val' ty'

298 return $ TypedValue True val' ty'

300infer' (PositionedValue pos _ val) = rethrowWithPosition pos $ infer' val

299infer' (PositionedValue pos _ val) = rethrowWithPosition pos $ infer' val

301infer' _ = error "Invalid argument to infer"

300infer' _ = error "Invalid argument to infer"

@@ -304,10 +303,11 @@ inferLetBinding :: [Declaration] -> [Declaration] -> Expr -> (Expr -> UnifyT Typ

304inferLetBinding seen [] ret j = (,) seen <$> makeBindingGroupVisible (j ret)

303inferLetBinding seen [] ret j = (,) seen <$> makeBindingGroupVisible (j ret)

305inferLetBinding seen (ValueDeclaration ident nameKind [] (Right (tv@(TypedValue checkType val ty))) : rest) ret j = do

304inferLetBinding seen (ValueDeclaration ident nameKind [] (Right (tv@(TypedValue checkType val ty))) : rest) ret j = do

306 Just moduleName <- checkCurrentModule <$> get

305 Just moduleName <- checkCurrentModule <$> get

307− checkTypeKind moduleName ty

306+ (kind, args) <- liftCheck $ kindOfWithScopedVars ty

307+ checkTypeKind kind

308 let dict = M.singleton (moduleName, ident) (ty, nameKind, Undefined)

309 ty' <- introduceSkolemScope <=< replaceAllTypeSynonyms <=< replaceTypeWildcards $ ty

310− TypedValue _ val' ty'' <- if checkType then bindNames dict (check val ty') else return tv

310+ TypedValue _ val' ty'' <- if checkType then withScopedTypeVars moduleName args (bindNames dict (check val ty')) else return tv

311 bindNames (M.singleton (moduleName, ident) (ty'', nameKind, Defined)) $ inferLetBinding (seen ++ [ValueDeclaration ident nameKind [] (Right (TypedValue checkType val' ty''))]) rest ret j

312inferLetBinding seen (ValueDeclaration ident nameKind [] (Right val) : rest) ret j = do

313 valTy <- fresh

@@ -507,14 +507,15 @@ check' (SuperClassDictionary className tys) _ = do

507 return $ TypeClassDictionary False (className, tys) dicts

508check' (TypedValue checkType val ty1) ty2 = do

509 Just moduleName <- checkCurrentModule <$> get

510− checkTypeKind moduleName ty1

510+ (kind, args) <- liftCheck $ kindOfWithScopedVars ty1

511+ checkTypeKind kind

511 ty1' <- introduceSkolemScope <=< replaceAllTypeSynonyms <=< replaceTypeWildcards $ ty1

512 ty1' <- introduceSkolemScope <=< replaceAllTypeSynonyms <=< replaceTypeWildcards $ ty1

512 ty2' <- introduceSkolemScope <=< replaceAllTypeSynonyms <=< replaceTypeWildcards $ ty2

513 ty2' <- introduceSkolemScope <=< replaceAllTypeSynonyms <=< replaceTypeWildcards $ ty2

513 val' <- subsumes (Just val) ty1' ty2'

514 val' <- subsumes (Just val) ty1' ty2'

514 case val' of

515 case val' of

515 Nothing -> throwError . strMsg $ "Unable to check type subsumption"

516 Nothing -> throwError . strMsg $ "Unable to check type subsumption"

516 Just val'' -> do

517 Just val'' -> do

517− val''' <- if checkType then check val'' ty2' else return val''

518+ val''' <- if checkType then withScopedTypeVars moduleName args (check val'' ty2') else return val''

518 return $ TypedValue checkType (TypedValue True val''' ty1') ty2'

519 return $ TypedValue checkType (TypedValue True val''' ty1') ty2'

519check' (Case vals binders) ret = do

520check' (Case vals binders) ret = do

520 vals' <- mapM infer vals

521 vals' <- mapM infer vals

@@ -562,7 +563,7 @@ check' val ty | containsTypeSynonyms ty = do

562 ty' <- introduceSkolemScope <=< expandAllTypeSynonyms <=< replaceTypeWildcards $ ty

563 ty' <- introduceSkolemScope <=< expandAllTypeSynonyms <=< replaceTypeWildcards $ ty

563 check val ty'

564 check val ty'

564check' val kt@(KindedType ty kind) = do

565check' val kt@(KindedType ty kind) = do

565− guardWith (strMsg $ "Expected type of kind *, was " ++ prettyPrintKind kind) $ kind == Star

566+ checkTypeKind kind

566 val' <- check' val ty

567 val' <- check' val ty

567 return $ TypedValue True val' kt

568 return $ TypedValue True val' kt

568check' (PositionedValue pos _ val) ty =

569check' (PositionedValue pos _ val) ty =