git.iko.soy/rowtype-yoga/purescript-native
on golang help sign in
Fix #181 - implement capture avoiding type substitution properly
3fd4ea9Phil Freeman
examples/shouldpass/TypeClasses.purs → examples/passing/TypeClassesWithOverlappingTypeVariables.pursrenamed+2
compare with golang
unifiedsplit
@@ -6,3 +6,5 @@ module Main where
6 instance Prelude.Functor (Either a) where
6 instance Prelude.Functor (Either a) where
7 (<$>) _ (Left x) = Left x
7 (<$>) _ (Left x) = Left x
8 (<$>) f (Right y) = Right (f y)
8 (<$>) 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
31
31
32import Control.Applicative
32import Control.Applicative
33import Control.Monad.State
33import Control.Monad.State
34+import Control.Arrow ((***))
35+
34import Data.Maybe (fromMaybe)
36import Data.Maybe (fromMaybe)
35import Data.List (nub)
37import Data.List (nub)
36import Data.Generics (mkQ, everything)
38import Data.Generics (mkQ, everything)
@@ -120,7 +122,7 @@ typeInstanceDictionaryDeclaration mn deps name ty decls = do
120 m <- get
122 m <- get
121 (arg, instanceTys) <- lift $ maybe (Left $ "Type class " ++ show name ++ " is undefined. Type class names must be qualified.") Right
123 (arg, instanceTys) <- lift $ maybe (Left $ "Type class " ++ show name ++ " is undefined. Type class names must be qualified.") Right
122 $ M.lookup (qualify mn name) m
124 $ M.lookup (qualify mn name) m
123− let memberTypes = map (replaceTypeVars arg ty) instanceTys
125+ let memberTypes = map (id *** replaceTypeVars arg ty) instanceTys
124 entryName <- lift $ mkDictionaryValueName mn name ty
126 entryName <- lift $ mkDictionaryValueName mn name ty
125 memberNames <- mapM (memberToNameAndValue memberTypes) decls
127 memberNames <- mapM (memberToNameAndValue memberTypes) decls
126 return $ ValueDeclaration entryName [] Nothing
128 return $ ValueDeclaration entryName [] Nothing
src/Language/PureScript/TypeChecker/Kinds.hs+3−1
@@ -59,7 +59,9 @@ instance Unifiable Check Kind where
59-- Infer the kind of a single type
59-- Infer the kind of a single type
60--
60--
61kindOf :: ModuleName -> Type -> Check Kind
61kindOf :: ModuleName -> Type -> Check Kind
62+kindOf moduleName ty =
63+ rethrow (("Error checking kind of " ++ prettyPrintType ty ++ ":\n") ++) $
62−kindOf moduleName ty = fmap tidyUp . liftUnify $ starIfUnknown <$> infer ty
64+ fmap tidyUp . liftUnify $ starIfUnknown <$> infer ty
63 where
65 where
64 tidyUp (k, sub) = sub $? k
66 tidyUp (k, sub) = sub $? k
65
67
src/Language/PureScript/TypeChecker/Types.hs+4−4
@@ -282,7 +282,7 @@ entails moduleName context goal@(className, ty) = do
282 solveSubgoals :: Environment -> [(String, Type)] -> Maybe [(Qualified ProperName, Type)] -> [Maybe [Value]]
282 solveSubgoals :: Environment -> [(String, Type)] -> Maybe [(Qualified ProperName, Type)] -> [Maybe [Value]]
283 solveSubgoals _ _ Nothing = return Nothing
283 solveSubgoals _ _ Nothing = return Nothing
284 solveSubgoals env subst (Just subgoals) = do
284 solveSubgoals env subst (Just subgoals) = do
285− dict <- mapM (go env) (replaceAllTypeVars subst subgoals)
285+ dict <- mapM (go env) (map (id *** replaceAllTypeVars subst) subgoals)
286 return $ Just dict
286 return $ Just dict
287 -- Make a dictionary from subgoal dictionaries by applying the correct function
287 -- Make a dictionary from subgoal dictionaries by applying the correct function
288 mkDictionary :: Qualified Ident -> Maybe [Value] -> Value
288 mkDictionary :: Qualified Ident -> Maybe [Value] -> Value
@@ -399,7 +399,7 @@ varIfUnknown ty =
399-- |
399-- |
400-- Replace named type variables with types
400-- Replace named type variables with types
401--
401--
402−replaceAllTypeVars :: (D.Data d) => [(String, Type)] -> d -> d
402+replaceAllTypeVars :: [(String, Type)] -> Type -> Type
403replaceAllTypeVars = foldl' (\f (name, ty) -> replaceTypeVars name ty . f) id
403replaceAllTypeVars = foldl' (\f (name, ty) -> replaceTypeVars name ty . f) id
404
404
405-- |
405-- |
@@ -760,8 +760,8 @@ newSkolemScope = SkolemScope . runUnknown <$> fresh'
760-- |
760-- |
761-- Skolemize a type variable by replacing its instances with fresh skolem constants
761-- Skolemize a type variable by replacing its instances with fresh skolem constants
762--
762--
763−skolemize :: (D.Data d) => String -> Int -> SkolemScope -> d -> d
763+skolemize :: String -> Int -> SkolemScope -> Type -> Type
764−skolemize ident sko scope d = replaceTypeVars ident (Skolem sko scope) d
764+skolemize ident sko scope = replaceTypeVars ident (Skolem sko scope)
765
765
766-- |
766-- |
767-- Introduce skolem scope at every occurence of a ForAll
767-- Introduce skolem scope at every occurence of a ForAll
src/Language/PureScript/Types.hs+36−9
@@ -18,9 +18,11 @@
18module Language.PureScript.Types where
18module Language.PureScript.Types where
19
19
20import Data.Data
20import Data.Data
21+import Data.List (nub)
21−import Data.Generics (mkT, mkQ, everywhereBut)
22+import Data.Generics (everything, mkT, mkQ, everywhereBut)
22
23
23import Control.Monad.Unify
24import Control.Monad.Unify
25+import Control.Arrow ((***))
24
26
25import Language.PureScript.Names
27import Language.PureScript.Names
26
28
@@ -159,24 +161,49 @@ unit = Object REmpty
159-- |
161-- |
160-- Replace a type variable, taking into account variable shadowing
162-- Replace a type variable, taking into account variable shadowing
161--
163--
162−replaceTypeVars :: (Data d) => String -> Type -> d -> d
164+replaceTypeVars :: String -> Type -> Type -> Type
163−replaceTypeVars name t = everywhereBut (mkQ False isShadowed) (mkT replaceTypeVar)
165+replaceTypeVars = replaceTypeVars' []
164 where
166 where
167+ replaceTypeVars' bound name replacement = go bound
168+ where
169+ go :: [String] -> Type -> Type
170+ go bs (Object r) = Object $ go bs r
165− replaceTypeVar (TypeVar v) | v == name = t
171+ go bs (TypeVar v) | v == name = replacement
166− replaceTypeVar other = other
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
167− isShadowed (ForAll v _ _) | v == name = True
174+ go bs f@(ForAll v t sco) | v == name = f
168− isShadowed _ = False
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 _ = []
169
196
170-- |
197-- |
171-- Collect all free type variables appearing in a type
198-- Collect all free type variables appearing in a type
172--
199--
173freeTypeVariables :: Type -> [String]
200freeTypeVariables :: Type -> [String]
174−freeTypeVariables = go []
201+freeTypeVariables = nub . go []
175 where
202 where
176 go :: [String] -> Type -> [String]
203 go :: [String] -> Type -> [String]
177 go bound (Object r) = go bound r
204 go bound (Object r) = go bound r
178 go bound (TypeVar v) | v `notElem` bound = [v]
205 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
180 go bound (SaturatedTypeSynonym _ ts) = concatMap (go bound) ts
207 go bound (SaturatedTypeSynonym _ ts) = concatMap (go bound) ts
181 go bound (ForAll v t _) = go (v : bound) t
208 go bound (ForAll v t _) = go (v : bound) t
182 go bound (ConstrainedType cs t) = concatMap (go bound . snd) cs ++ go bound t
209 go bound (ConstrainedType cs t) = concatMap (go bound . snd) cs ++ go bound t