d6a694d · rowtype-yoga/purescript-native

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

Capture avoiding substitution during skolemization

commitd6a694d2eb9a1608d7ea247c47aaeb7dfb8ebcfb authorPhil Freeman <paf31@cantab.net> dateWed 27 Nov 2013, 16:29 (13 years ago) parent38c685d

3 files changed+16−18

compare with golang

unifiedsplit

examples/passing/Auto.ps+1−1 examples/passing/Rank2Types.ps+1−1 src/Language/PureScript/TypeChecker/Types.hs+14−16

examples/passing/Auto.ps+1−1

@@ -2,7 +2,7 @@ data Auto s i o = Auto { state :: s, step :: s -> i -> o }

33type SomeAuto i o = forall r. (forall s. Auto s i o -> r) -> r

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

66exists = \state step f -> f (Auto { state: state, step: step })

88run :: forall i o. SomeAuto i o -> i -> o

examples/passing/Rank2Types.ps+1−1

@@ -11,7 +11,7 @@ testST = runST exampleST

1111

1212foreign import push :: forall el. el -> [el] -> [el]

1313

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]

1515replicateM = \ret bind n m -> case n of

1616 0 -> ret []

1717 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

2222import Data.Maybe (isJust, fromMaybe)

2323import Data.Function

2424import 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)

2626

2727import Language.PureScript.Values

2828import Language.PureScript.Types

@@ -185,27 +185,27 @@ setifyAll = everywhere (mkT setify)

185185varIfUnknown :: Type -> Type

186186varIfUnknown ty = mkForAll (sort . map ((:) 'u' . show) . nub $ unknowns ty) ty

187187

188−replaceTypeVars :: M.Map String Type -> Type -> Type

189−replaceTypeVars m = everywhere (mkT replace)

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

192+replaceTypeVars name t = everywhereBut (mkQ False isShadowed) (mkT replace)

190193 where

191− replace (TypeVar v) = case M.lookup v m of

192− Just ty -> ty

193− _ -> TypeVar v

194+ replace (TypeVar v) | v == name = t

194195 replace t = t

196+ isShadowed (ForAll v _) | v == name = True

197+ isShadowed _ = False

195198

196−replaceRowVars :: M.Map String Row -> Type -> Type

197−replaceRowVars m = everywhere (mkT replace)

199+replaceRowVars :: (D.Data d) => String -> Row -> d -> d

200+replaceRowVars name r = everywhere (mkT replace)

198201 where

199− replace (RowVar v) = case M.lookup v m of

200− Just r -> r

201− _ -> RowVar v

202+ replace (RowVar v) | v == name = r

202203 replace t = t

203204

204205replaceAllVarsWithUnknowns :: Type -> Subst Check Type

205206replaceAllVarsWithUnknowns (ForAll ident ty) = replaceVarsWithUnknowns [ident] ty >>= replaceAllVarsWithUnknowns

206207replaceAllVarsWithUnknowns ty = return ty

207208

208−-- TODO: need to be careful inside a forall, since variables might be renamed

209209replaceVarsWithUnknowns :: [String] -> Type -> Subst Check Type

210210replaceVarsWithUnknowns idents = flip evalStateT M.empty . everywhereM (flip extM f $ mkM g)

211211 where

@@ -251,9 +251,7 @@ expandTypeSynonym name args = do

251251 env <- lift getEnv

252252 modulePath <- checkModulePath `fmap` lift get

253253 case M.lookup (qualify modulePath name) (typeSynonyms env) of

254− Just (synArgs, body) -> do

255− let m = M.fromList $ zip synArgs args

256− return $ replaceTypeVars m body

254+ Just (synArgs, body) -> return $ replaceAllTypeVars (zip synArgs args) body

257255 Nothing -> error "Type synonym was not defined"

258256

259257ensureNoDuplicateProperties :: [(String, Value)] -> Check ()

@@ -581,7 +579,7 @@ skolemize :: String -> Type -> Subst Check Type

581579skolemize ident ty = do

582580 tsk <- Skolem <$> fresh'

583581 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

585583

586584check :: M.Map Ident Type -> Value -> Type -> Subst Check ()

587585check m val ty = rethrow errorMessage $ check' m val ty