git.iko.soy/rowtype-yoga/purescript-native
on golang help sign in
Fix #181 - implement capture avoiding type substitution properly
commit3fd4ea9a20dd5d4b7699f2e3fe80a8244011da48 authorPhil Freeman <paf31@cantab.net> dateSun 9 Feb 2014, 13:46 (13 years ago) parent7604b66
5 files changed+48−15
compare with golang
unifiedsplit
examples/shouldpass/TypeClasses.purs → examples/passing/TypeClassesWithOverlappingTypeVariables.purs+2 src/Language/PureScript/Sugar/TypeClasses.hs+3−1 src/Language/PureScript/TypeChecker/Kinds.hs+3−1 src/Language/PureScript/TypeChecker/Types.hs+4−4 src/Language/PureScript/Types.hs+36−9
examples/shouldpass/TypeClasses.purs → examples/passing/TypeClassesWithOverlappingTypeVariables.pursrenamed+2
@@ -6,3 +6,5 @@ module Main where
66 instance Prelude.Functor (Either a) where
77 (<$>) _ (Left x) = Left x
88 (<$>) f (Right y) = Right (f y)
9+
10+ main = Trace.trace "Done"
src/Language/PureScript/Sugar/TypeClasses.hs+3−1
@@ -31,6 +31,8 @@ import qualified Data.Map as M
3131
3232import Control.Applicative
3333import Control.Monad.State
34+import Control.Arrow ((***))
35+
3436import Data.Maybe (fromMaybe)
3537import Data.List (nub)
3638import Data.Generics (mkQ, everything)
@@ -120,7 +122,7 @@ typeInstanceDictionaryDeclaration mn deps name ty decls = do
120122 m <- get
121123 (arg, instanceTys) <- lift $ maybe (Left $ "Type class " ++ show name ++ " is undefined. Type class names must be qualified.") Right
122124 $ M.lookup (qualify mn name) m
123− let memberTypes = map (replaceTypeVars arg ty) instanceTys
125+ let memberTypes = map (id *** replaceTypeVars arg ty) instanceTys
124126 entryName <- lift $ mkDictionaryValueName mn name ty
125127 memberNames <- mapM (memberToNameAndValue memberTypes) decls
126128 return $ ValueDeclaration entryName [] Nothing
src/Language/PureScript/TypeChecker/Kinds.hs+3−1
@@ -59,7 +59,9 @@ instance Unifiable Check Kind where
5959-- Infer the kind of a single type
6060--
6161kindOf :: ModuleName -> Type -> Check Kind
62−kindOf moduleName ty = fmap tidyUp . liftUnify $ starIfUnknown <$> infer ty
62+kindOf moduleName ty =
63+ rethrow (("Error checking kind of " ++ prettyPrintType ty ++ ":\n") ++) $
64+ fmap tidyUp . liftUnify $ starIfUnknown <$> infer ty
6365 where
6466 tidyUp (k, sub) = sub $? k
6567
src/Language/PureScript/TypeChecker/Types.hs+4−4
@@ -282,7 +282,7 @@ entails moduleName context goal@(className, ty) = do
282282 solveSubgoals :: Environment -> [(String, Type)] -> Maybe [(Qualified ProperName, Type)] -> [Maybe [Value]]
283283 solveSubgoals _ _ Nothing = return Nothing
284284 solveSubgoals env subst (Just subgoals) = do
285− dict <- mapM (go env) (replaceAllTypeVars subst subgoals)
285+ dict <- mapM (go env) (map (id *** replaceAllTypeVars subst) subgoals)
286286 return $ Just dict
287287 -- Make a dictionary from subgoal dictionaries by applying the correct function
288288 mkDictionary :: Qualified Ident -> Maybe [Value] -> Value
@@ -399,7 +399,7 @@ varIfUnknown ty =
399399-- |
400400-- Replace named type variables with types
401401--
402−replaceAllTypeVars :: (D.Data d) => [(String, Type)] -> d -> d
402+replaceAllTypeVars :: [(String, Type)] -> Type -> Type
403403replaceAllTypeVars = foldl' (\f (name, ty) -> replaceTypeVars name ty . f) id
404404
405405-- |
@@ -760,8 +760,8 @@ newSkolemScope = SkolemScope . runUnknown <$> fresh'
760760-- |
761761-- Skolemize a type variable by replacing its instances with fresh skolem constants
762762--
763−skolemize :: (D.Data d) => String -> Int -> SkolemScope -> d -> d
764−skolemize ident sko scope d = replaceTypeVars ident (Skolem sko scope) d
763+skolemize :: String -> Int -> SkolemScope -> Type -> Type
764+skolemize ident sko scope = replaceTypeVars ident (Skolem sko scope)
765765
766766-- |
767767-- Introduce skolem scope at every occurence of a ForAll
src/Language/PureScript/Types.hs+36−9
@@ -18,9 +18,11 @@
1818module Language.PureScript.Types where
1919
2020import Data.Data
21−import Data.Generics (mkT, mkQ, everywhereBut)
21+import Data.List (nub)
22+import Data.Generics (everything, mkT, mkQ, everywhereBut)
2223
2324import Control.Monad.Unify
25+import Control.Arrow ((***))
2426
2527import Language.PureScript.Names
2628
@@ -159,24 +161,49 @@ unit = Object REmpty
159161-- |
160162-- Replace a type variable, taking into account variable shadowing
161163--
162−replaceTypeVars :: (Data d) => String -> Type -> d -> d
163−replaceTypeVars name t = everywhereBut (mkQ False isShadowed) (mkT replaceTypeVar)
164+replaceTypeVars :: String -> Type -> Type -> Type
165+replaceTypeVars = replaceTypeVars' []
164166 where
165− replaceTypeVar (TypeVar v) | v == name = t
166− replaceTypeVar other = other
167− isShadowed (ForAll v _ _) | v == name = True
168− isShadowed _ = False
167+ replaceTypeVars' bound name replacement = go bound
168+ where
169+ go :: [String] -> Type -> Type
170+ go bs (Object r) = Object $ go bs r
171+ go bs (TypeVar v) | v == name = replacement
172+ go bs (TypeApp t1 t2) = TypeApp (go bs t1) (go bs t2)
173+ go bs (SaturatedTypeSynonym name ts) = SaturatedTypeSynonym name $ map (go bs) ts
174+ go bs f@(ForAll v t sco) | v == name = f
175+ | v `elem` usedTypeVariables replacement =
176+ let v' = genName v (name : bs ++ usedTypeVariables replacement)
177+ t' = replaceTypeVars' bs v (TypeVar v') t
178+ in ForAll v' (go (v' : bs) t') sco
179+ | otherwise = ForAll v (go (v : bs) t) sco
180+ go bs (ConstrainedType cs t) = ConstrainedType (map (id *** go bs) cs) (go bs t)
181+ go bs (RCons name t r) = RCons name (go bs t) (go bs r)
182+ go _ ty = ty
183+ genName orig inUse = try 0
184+ where
185+ try n | (orig ++ show n) `elem` inUse = try (n + 1)
186+ | otherwise = orig ++ show n
187+
188+-- |
189+-- Collect all type variables appearing in a type
190+--
191+usedTypeVariables :: Type -> [String]
192+usedTypeVariables = nub . everything (++) (mkQ [] go)
193+ where
194+ go (TypeVar v) = [v]
195+ go _ = []
169196
170197-- |
171198-- Collect all free type variables appearing in a type
172199--
173200freeTypeVariables :: Type -> [String]
174−freeTypeVariables = go []
201+freeTypeVariables = nub . go []
175202 where
176203 go :: [String] -> Type -> [String]
177204 go bound (Object r) = go bound r
178205 go bound (TypeVar v) | v `notElem` bound = [v]
179− go bound (TypeApp t1 t2) = go bound t1 ++ go bound t2
206+ go bound (TypeApp t1 t2) = go bound t1 ++ go bound t2
180207 go bound (SaturatedTypeSynonym _ ts) = concatMap (go bound) ts
181208 go bound (ForAll v t _) = go (v : bound) t
182209 go bound (ConstrainedType cs t) = concatMap (go bound . snd) cs ++ go bound t