@@ -126,35 +126,41 @@ mkForAll args ty = foldl (\t arg -> ForAll arg t Nothing) ty args
126126-- Replace a type variable, taking into account variable shadowing
127127--
128128replaceTypeVars :: String -> Type -> Type -> Type
129−replaceTypeVars = replaceTypeVars' []
129+replaceTypeVars v r = replaceAllTypeVars [(v, r)]
130+
131+-- |
132+-- Replace named type variables with types
133+--
134+replaceAllTypeVars :: [(String, Type)] -> Type -> Type
135+replaceAllTypeVars = go []
130136 where
131− replaceTypeVars' bound name replacement = go bound
137+
138+ go :: [String] -> [(String, Type)] -> Type -> Type
139+ go _ m (TypeVar v) =
140+ case v `lookup` m of
141+ Just r -> r
142+ Nothing -> TypeVar v
143+ go bs m (TypeApp t1 t2) = TypeApp (go bs m t1) (go bs m t2)
144+ go bs m (SaturatedTypeSynonym name' ts) = SaturatedTypeSynonym name' $ map (go bs m) ts
145+ go bs m f@(ForAll v t sco) | v `elem` keys = go bs (filter ((/= v) . fst) m) f
146+ | v `elem` usedVars =
147+ let v' = genName v (keys ++ bs ++ usedVars)
148+ t' = go bs [(v, TypeVar v')] t
149+ in ForAll v' (go (v' : bs) m t') sco
150+ | otherwise = ForAll v (go (v : bs) m t) sco
132151 where
133− go :: [String] -> Type -> Type
134− go _ (TypeVar v) | v == name = replacement
135− go bs (TypeApp t1 t2) = TypeApp (go bs t1) (go bs t2)
136− go bs (SaturatedTypeSynonym name' ts) = SaturatedTypeSynonym name' $ map (go bs) ts
137− go bs f@(ForAll v t sco) | v == name = f
138− | v `elem` usedTypeVariables replacement =
139− let v' = genName v (name : bs ++ usedTypeVariables replacement)
140− t' = replaceTypeVars' bs v (TypeVar v') t
141− in ForAll v' (go (v' : bs) t') sco
142− | otherwise = ForAll v (go (v : bs) t) sco
143− go bs (ConstrainedType cs t) = ConstrainedType (map (second $ map (go bs)) cs) (go bs t)
144− go bs (RCons name' t r) = RCons name' (go bs t) (go bs r)
145− go _ ty = ty
152+ keys = map fst m
153+ usedVars = concatMap (usedTypeVariables . snd) m
154+ go bs m (ConstrainedType cs t) = ConstrainedType (map (second $ map (go bs m)) cs) (go bs m t)
155+ go bs m (RCons name' t r) = RCons name' (go bs m t) (go bs m r)
156+ go _ _ ty = ty
157+
146158 genName orig inUse = try 0
147159 where
148160 try :: Integer -> String
149161 try n | (orig ++ show n) `elem` inUse = try (n + 1)
150162 | otherwise = orig ++ show n
151163
152−-- |
153−-- Replace named type variables with types
154−--
155−replaceAllTypeVars :: [(String, Type)] -> Type -> Type
156−replaceAllTypeVars = foldl (\f (name, ty) -> replaceTypeVars name ty . f) id
157−
158164-- |
159165-- Collect all type variables appearing in a type
160166--