git.iko.soy/rowtype-yoga/purescript-native
on golang help sign in
Capture avoiding substitution during skolemization
d6a694dPhil Freeman
examples/passing/Auto.ps+1−1
compare with golang
unifiedsplit
@@ -2,7 +2,7 @@ data Auto s i o = Auto { state :: s, step :: s -> i -> o }
2
2
3type SomeAuto i o = forall r. (forall s. Auto s i o -> r) -> r
3type SomeAuto i o = forall r. (forall s. Auto s i o -> r) -> r
4
4
5−exists :: forall s1 i o. s1 -> (s1 -> i -> o) -> SomeAuto i o
5+exists :: forall s i o. s -> (s -> i -> o) -> SomeAuto i o
6exists = \state step f -> f (Auto { state: state, step: step })
6exists = \state step f -> f (Auto { state: state, step: step })
7
7
8run :: forall i o. SomeAuto i o -> i -> o
8run :: forall i o. SomeAuto i o -> i -> o
examples/passing/Rank2Types.ps+1−1
@@ -11,7 +11,7 @@ testST = runST exampleST
11
11
12foreign import push :: forall el. el -> [el] -> [el]
12foreign import push :: forall el. el -> [el] -> [el]
13
13
14−replicateM :: forall m a. (forall x. x -> m x) -> (forall x y. m x -> (x -> m y) -> m y) -> Number -> m a -> m [a]
14+replicateM :: forall m a. (forall a. a -> m a) -> (forall a b. m a -> (a -> m b) -> m b) -> Number -> m a -> m [a]
15replicateM = \ret bind n m -> case n of
15replicateM = \ret bind n m -> case n of
16 0 -> ret []
16 0 -> ret []
17 n -> bind m (\x -> bind (replicateM ret bind (n - 1) m) (\xs -> ret (push x xs)))
17 n -> bind m (\x -> bind (replicateM ret bind (n - 1) m) (\xs -> ret (push x xs)))
src/Language/PureScript/TypeChecker/Types.hs+14−16
@@ -22,7 +22,7 @@ import Data.List
22import Data.Maybe (isJust, fromMaybe)
22import Data.Maybe (isJust, fromMaybe)
23import Data.Function
23import Data.Function
24import qualified Data.Data as D
24import qualified Data.Data as D
25−import Data.Generics (everywhere, everywhereM, everything, mkT, mkM, mkQ, extM, extQ)
25+import Data.Generics (everywhere, everywhereM, everything, everywhereBut, mkT, mkM, mkQ, extM, extQ)
26
26
27import Language.PureScript.Values
27import Language.PureScript.Values
28import Language.PureScript.Types
28import Language.PureScript.Types
@@ -185,27 +185,27 @@ setifyAll = everywhere (mkT setify)
185varIfUnknown :: Type -> Type
185varIfUnknown :: Type -> Type
186varIfUnknown ty = mkForAll (sort . map ((:) 'u' . show) . nub $ unknowns ty) ty
186varIfUnknown ty = mkForAll (sort . map ((:) 'u' . show) . nub $ unknowns ty) ty
187
187
188−replaceTypeVars :: M.Map String Type -> Type -> Type
188+replaceAllTypeVars :: (D.Data d) => [(String, Type)] -> d -> d
189+replaceAllTypeVars = foldl' (\f (name, ty) -> replaceTypeVars name ty . f) id
190+
191+replaceTypeVars :: (D.Data d) => String -> Type -> d -> d
189−replaceTypeVars m = everywhere (mkT replace)
192+replaceTypeVars name t = everywhereBut (mkQ False isShadowed) (mkT replace)
190 where
193 where
191− replace (TypeVar v) = case M.lookup v m of
194+ replace (TypeVar v) | v == name = t
192− Just ty -> ty
193− _ -> TypeVar v
194 replace t = t
195 replace t = t
196+ isShadowed (ForAll v _) | v == name = True
197+ isShadowed _ = False
195
198
196−replaceRowVars :: M.Map String Row -> Type -> Type
199+replaceRowVars :: (D.Data d) => String -> Row -> d -> d
197−replaceRowVars m = everywhere (mkT replace)
200+replaceRowVars name r = everywhere (mkT replace)
198 where
201 where
199− replace (RowVar v) = case M.lookup v m of
202+ replace (RowVar v) | v == name = r
200− Just r -> r
201− _ -> RowVar v
202 replace t = t
203 replace t = t
203
204
204replaceAllVarsWithUnknowns :: Type -> Subst Check Type
205replaceAllVarsWithUnknowns :: Type -> Subst Check Type
205replaceAllVarsWithUnknowns (ForAll ident ty) = replaceVarsWithUnknowns [ident] ty >>= replaceAllVarsWithUnknowns
206replaceAllVarsWithUnknowns (ForAll ident ty) = replaceVarsWithUnknowns [ident] ty >>= replaceAllVarsWithUnknowns
206replaceAllVarsWithUnknowns ty = return ty
207replaceAllVarsWithUnknowns ty = return ty
207
208
208−-- TODO: need to be careful inside a forall, since variables might be renamed
209replaceVarsWithUnknowns :: [String] -> Type -> Subst Check Type
209replaceVarsWithUnknowns :: [String] -> Type -> Subst Check Type
210replaceVarsWithUnknowns idents = flip evalStateT M.empty . everywhereM (flip extM f $ mkM g)
210replaceVarsWithUnknowns idents = flip evalStateT M.empty . everywhereM (flip extM f $ mkM g)
211 where
211 where
@@ -251,9 +251,7 @@ expandTypeSynonym name args = do
251 env <- lift getEnv
251 env <- lift getEnv
252 modulePath <- checkModulePath `fmap` lift get
252 modulePath <- checkModulePath `fmap` lift get
253 case M.lookup (qualify modulePath name) (typeSynonyms env) of
253 case M.lookup (qualify modulePath name) (typeSynonyms env) of
254− Just (synArgs, body) -> do
254+ Just (synArgs, body) -> return $ replaceAllTypeVars (zip synArgs args) body
255− let m = M.fromList $ zip synArgs args
256− return $ replaceTypeVars m body
257 Nothing -> error "Type synonym was not defined"
255 Nothing -> error "Type synonym was not defined"
258
256
259ensureNoDuplicateProperties :: [(String, Value)] -> Check ()
257ensureNoDuplicateProperties :: [(String, Value)] -> Check ()
@@ -581,7 +579,7 @@ skolemize :: String -> Type -> Subst Check Type
581skolemize ident ty = do
579skolemize ident ty = do
582 tsk <- Skolem <$> fresh'
580 tsk <- Skolem <$> fresh'
583 rsk <- RSkolem <$> fresh'
581 rsk <- RSkolem <$> fresh'
584− return $ replaceRowVars (M.singleton ident rsk) $ replaceTypeVars (M.singleton ident tsk) ty
582+ return $ replaceRowVars ident rsk $ replaceTypeVars ident tsk ty
585
583
586check :: M.Map Ident Type -> Value -> Type -> Subst Check ()
584check :: M.Map Ident Type -> Value -> Type -> Subst Check ()
587check m val ty = rethrow errorMessage $ check' m val ty
585check m val ty = rethrow errorMessage $ check' m val ty