@@ -35,22 +35,24 @@ match_unify :: Context -> Env -> TT Name -> TT Name -> [Name] -> [Name] ->
3535 TC [(Name, TT Name)]
3636match_unify ctxt env topx topy dont holes =
3737 case runStateT (un [] topx topy) (UI 0 []) of
38− OK (v, UI _ []) -> return (trimSolutions v)
38+ OK (v, UI _ []) -> return (map (renameBinders env) (trimSolutions v))
3939 res ->
4040 let topxn = normalise ctxt env topx
4141 topyn = normalise ctxt env topy in
4242 case runStateT (un [] topxn topyn)
4343 (UI 0 []) of
4444 OK (v, UI _ fails) ->
45− return (trimSolutions v)
45+ return (map (renameBinders env) (trimSolutions v))
4646 Error e ->
4747 -- just normalise the term we're matching against
4848 case runStateT (un [] topxn topy)
4949 (UI 0 []) of
5050 OK (v, UI _ fails) ->
51− return (trimSolutions v)
51+ return (map (renameBinders env) (trimSolutions v))
5252 _ -> tfail e
5353 where
54+
55+
5456 un names (P _ x _) tm
5557 | holeIn env x || x `elem` holes
5658 = do sc 1; checkCycle names (x, tm)
@@ -127,6 +129,23 @@ match_unify ctxt env topx topy dont holes =
127129 (inst ns tm) (errEnv env))
128130 where inst [] tm = tm
129131 inst ((n, _) : ns) tm = inst ns (substV (P Bound n Erased) tm)
132+
133+renameBinders :: Env -> (Name, TT Name) -> (Name, TT Name)
134+renameBinders env (x, tm) = (x, uniqueBinders tm)
135+ where
136+ uniqueBinders (Bind n b sc)
137+ | n `elem` map fst env
138+ = let n' = uniqueName n (map fst env) in
139+ Bind n' (fmap uniqueBinders b)
140+ (uniqueBinders (rename n n' sc))
141+ | otherwise = Bind n (fmap uniqueBinders b) (uniqueBinders sc)
142+ uniqueBinders (App f a) = App (uniqueBinders f) (uniqueBinders a)
143+ uniqueBinders t = t
144+
145+ rename n n' (P nt x ty) | n == x = P nt n' ty
146+ rename n n' (Bind x b sc) = Bind x (fmap (rename n n') b) (rename n n' sc)
147+ rename n n' (App f a) = App (rename n n' f) (rename n n' a)
148+ rename n n' t = t
130149
131150trimSolutions ns = dropPairs ns
132151 where dropPairs [] = []
@@ -154,7 +173,7 @@ unify ctxt env topx topy dont holes =
154173-- trace ("Unifying " ++ show (topx, topy)) $
155174 -- don't bother if topx and topy are different at the head
156175 case runStateT (un False [] topx topy) (UI 0 []) of
157− OK (v, UI _ []) -> return (trimSolutions v,
176+ OK (v, UI _ []) -> return (map (renameBinders env) (trimSolutions v),
158177 [])
159178 res ->
160179 let topxn = normalise ctxt env topx
@@ -163,7 +182,8 @@ unify ctxt env topx topy dont holes =
163182 case runStateT (un False [] topxn topyn)
164183 (UI 0 []) of
165184 OK (v, UI _ fails) ->
166− return (trimSolutions v, reverse fails)
185+ return (map (renameBinders env) (trimSolutions v),
186+ reverse fails)
167187-- Error e@(CantUnify False _ _ _ _ _) -> tfail e
168188 Error e -> tfail e
169189 where