@@ -180,6 +180,19 @@ match_unify' ctxt env topx topy =
180180-- -- ++ show (pterm ps)
181181-- ++ "\n----------") $
182182
183+mergeSolutions :: Env -> [(Name, TT Name)] -> StateT TState TC [(Name, TT Name)]
184+mergeSolutions env ns = merge [] ns
185+ where
186+ merge acc [] = return (reverse acc)
187+ merge acc ((n, t) : ns)
188+ | Just t' <- lookup n ns
189+ = do ps <- get
190+ let probs = problems ps
191+ put (ps { problems = probs ++ [(t,t',env,Msg "New problem",
192+ [], Unify)] })
193+ merge acc ns
194+ | otherwise = merge ((n, t): acc) ns
195+
183196unify' :: Context -> Env -> TT Name -> TT Name ->
184197 StateT TState TC [(Name, TT Name)]
185198unify' ctxt env topx topy =
@@ -206,17 +219,22 @@ unify' ctxt env topx topy =
206219 ++ "\nCurrent problems:\n" ++ qshow (problems ps)
207220-- ++ show (pterm ps)
208221 ++ "\n----------") $
209− do ps <- get
210− let (h, ns) = unified ps
211− let (ns', probs') = updateProblems (context ps) (u ++ ns)
222+ do let (h, ns) = unified ps
223+ -- if a metavar has multiple solutions, make a new unification
224+ -- problem for each.
225+ uns <- mergeSolutions env (u ++ ns)
226+ ps <- get
227+ let (ns', probs') = updateProblems (context ps) uns
212228 (fails ++ problems ps)
213229 (injective ps)
214230 (holes ps)
215231 let (notu', probs_notu) = mergeNotunified env (notu ++ notunified ps)
216− put (ps { problems = probs' ++ probs_notu,
217− unified = (h, ns'),
218− injective = updateInj u (injective ps),
219− notunified = notu' })
232+ traceWhen (unifylog ps)
233+ ("Now solved: " ++ show ns') $
234+ put (ps { problems = probs' ++ probs_notu,
235+ unified = (h, ns'),
236+ injective = updateInj u (injective ps),
237+ notunified = notu' })
220238 return u
221239 where updateInj ((n, a) : us) inj
222240 | (P _ n' _, _) <- unApply a,