Remove dubious matching rule

IIRC this was a hack for scoped implicits, but whatever it did isn't
tripped up in the tests any more and it's a horrible hack anyway, so off
it goes.

src/Idris/Core/ProofState.hs

@@ -1022,13 +1022,16 @@ processTactic UnifyProblems ps
 processTactic (MatchProblems all) ps
     = do let (ns', probs') = matchProblems all ps [] (problems ps)
              (ns'', probs'') = matchProblems all ps ns' probs'
-             pterm' = updateSolved ns'' (pterm ps)
-         traceWhen (unifylog ps) ("(MatchProblems) Dropping holes: " ++ show (map fst ns'')) $
+             pterm' = orderUpdateSolved ns'' (resetProofTerm (pterm ps))
+         traceWhen (unifylog ps) ("(MatchProblems) Dropping holes: " ++ show ns'') $
           return (ps { pterm = pterm', solved = Nothing, problems = probs'',
                        previous = Just ps, plog = "",
                        notunified = updateNotunified ns'' (notunified ps),
                        recents = recents ps ++ map fst ns'',
                        holes = holes ps \\ (map fst ns'') }, plog ps)
+  where
+    orderUpdateSolved [] t = t
+    orderUpdateSolved (n : ns) t = orderUpdateSolved ns (updateSolved [n] t)
 processTactic t ps
     = case holes ps of
         [] -> case t of

src/Idris/Core/ProofTerm.hs

@@ -6,6 +6,7 @@ evaluation/checking inside the proof system, etc.
 -}
 
 module Idris.Core.ProofTerm(ProofTerm, Goal(..), mkProofTerm, getProofTerm,
+                            resetProofTerm,
                             updateSolved, updateSolvedTerm, updateSolvedTerm',
                             bound_in, bound_in_term, refocus, updsubst,
                             Hole, RunTactic',
@@ -129,6 +130,9 @@ mkProofTerm tm = PT Top [] tm []
 getProofTerm :: ProofTerm -> Term
 getProofTerm (PT path _ sub ups) = rebuildTerm sub (updateSolvedPath ups path) 
 
+resetProofTerm :: ProofTerm -> ProofTerm
+resetProofTerm = mkProofTerm . getProofTerm
+
 same :: Eq a => Maybe a -> a -> Bool
 same Nothing n  = True
 same (Just x) n = x == n

src/Idris/Core/Unify.hs

@@ -92,31 +92,6 @@ match_unify ctxt env (topx, xfrom) (topy, yfrom) inj holes from =
           StateT UInfo
           TC [(Name, TT Name)]
 
-    -- This rule is highly dubious... it certainly produces a valid answer
-    -- but it scares me. However, matching is never guaranteed to give a unique
-    -- answer, merely a valid one, so perhaps we're okay.
-    -- In other words: it may vanish without warning some day :)
-    un names x tm@(App _ (P _ f (Bind fn (Pi _ t _) sc)) a)
-        | (P (TCon _ _) _ _, _) <- unApply x,
-          holeIn env f || f `elem` holes
-           = let n' = uniqueName (sMN 0 "mv") (map fst env) in
-             checkCycle names (f, Bind n' (Lam t) x)
-    un names tm@(App _ (P _ f (Bind fn (Pi _ t _) sc)) a) x
-        | (P (TCon _ _) _ _, _) <- unApply x,
-          holeIn env f || f `elem` holes
-           = let n' = uniqueName fn (map fst env) in
-                 checkCycle names (f, Bind n' (Lam t) x)
-    un names x tm@(App _ (P _ f (Bind fn (Pi _ t _) sc)) a)
-        | (P (DCon _ _ _) _ _, _) <- unApply x,
-          holeIn env f || f `elem` holes
-           = let n' = uniqueName (sMN 0 "mv") (map fst env) in
-             checkCycle names (f, Bind n' (Lam t) x)
-    un names tm@(App _ (P _ f (Bind fn (Pi _ t _) sc)) a) x
-        | (P (DCon _ _ _) _ _, _) <- unApply x,
-          holeIn env f || f `elem` holes
-           = let n' = uniqueName fn (map fst env) in
-                 checkCycle names (f, Bind n' (Lam t) x)
-
     un names tx@(P _ x _) tm
         | tx /= tm && holeIn env x || x `elem` holes
             = do sc 1; checkCycle names (x, tm)