@@ -151,10 +151,10 @@ match_unify' ctxt env topx topy =
151151 let dont = dontunify ps
152152 let inj = injective ps
153153 traceWhen (unifylog ps)
154− ("Matching " ++ show (topx, topy) ++
154+ ("Matching " ++ show (topx, topy) ++
155155 " in " ++ show env ++
156156 "\nHoles: " ++ show (holes ps)
157− ++ "\n"
157+ ++ "\n"
158158 ++ "\n" ++ show (getProofTerm (pterm ps)) ++ "\n\n"
159159 ) $
160160 case match_unify ctxt env topx topy inj (holes ps) while of
@@ -170,7 +170,7 @@ match_unify' ctxt env topx topy =
170170 return []
171171-- traceWhen (unifylog ps)
172172-- ("Matched " ++ show (topx, topy) ++ " without " ++ show dont ++
173−-- "\nSolved: " ++ show u
173+-- "\nSolved: " ++ show u
174174-- ++ "\nCurrent problems:\n" ++ qshow (problems ps)
175175-- -- ++ show (pterm ps)
176176-- ++ "\n----------") $
@@ -203,7 +203,7 @@ unify' ctxt env topx topy =
203203 "\nHoles: " ++ show (holes ps)
204204 ++ "\nInjective: " ++ show (injective ps)
205205 ++ "\n") $
206− lift $ unify ctxt env topx topy inj (holes ps)
206+ lift $ unify ctxt env topx topy inj (holes ps)
207207 (map fst (notunified ps)) while
208208 let notu = filter (\ (n, t) -> case t of
209209 P _ _ _ -> False
@@ -416,7 +416,7 @@ deferType n fty_in args ctxt env (Bind x (Hole t) (P nt x' ty)) | x == x' =
416416 Nothing -> error ("deferType can't find " ++ show n)
417417
418418regret :: RunTactic
419−regret ctxt env (Bind x (Hole t) sc) | noOccurrence x sc =
419+regret ctxt env (Bind x (Hole t) sc) | noOccurrence x sc =
420420 do action (\ps -> let hs = holes ps in
421421 ps { holes = hs \\ [x] })
422422 return sc
@@ -495,7 +495,7 @@ solve ctxt env (Bind x (Guess ty val) sc)
495495 notunified = updateNotunified [(x,val)]
496496 (notunified ps),
497497 instances = instances ps \\ [x] })
498− let tm' = subst x val sc in
498+ let tm' = subst x val sc in
499499 return tm'
500500solve _ _ h@(Bind x t sc)
501501 = do ps <- get
@@ -504,7 +504,7 @@ solve _ _ h@(Bind x t sc)
504504 _ -> lift $ tfail (IncompleteTerm h)
505505 where findType x (Bind n (Let t v) sc)
506506 = findType x v `mplus` findType x sc
507− findType x (Bind n t sc)
507+ findType x (Bind n t sc)
508508 | P _ x' _ <- binderTy t, x == x' = Just n
509509 | otherwise = findType x sc
510510 findType x _ = Nothing
@@ -553,7 +553,7 @@ forall n ty ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
553553forall n ty ctxt env _ = fail "Can't pi bind here"
554554
555555patvar :: Name -> RunTactic
556−patvar n ctxt env (Bind x (Hole t) sc) =
556+patvar n ctxt env (Bind x (Hole t) sc) =
557557 do action (\ps -> ps { holes = traceWhen (unifylog ps) ("Dropping pattern hole " ++ show x) $
558558 holes ps \\ [x],
559559 solved = Just (x, P Bound n t),
@@ -590,7 +590,7 @@ rewrite tm ctxt env (Bind x (Hole t) xp@(P _ x' _)) | x == x' =
590590 [lt, l, r, p, tmv, xp]))
591591 (scv, sct) <- lift $ check ctxt env sc
592592 return scv
593− _ -> lift $ tfail (NotEquality tmv tmt')
593+ _ -> lift $ tfail (NotEquality tmv tmt')
594594 where rname = sMN 0 "replaced"
595595rewrite _ _ _ _ = fail "Can't rewrite here"
596596
@@ -769,7 +769,7 @@ updateEnv ns ((n, b) : env) = (n, fmap (updateSolvedTerm ns) b) : updateEnv ns e
769769updateError [] err = err
770770updateError ns (At f e) = At f (updateError ns e)
771771updateError ns (Elaborating s n e) = Elaborating s n (updateError ns e)
772−updateError ns (ElaboratingArg f a env e)
772+updateError ns (ElaboratingArg f a env e)
773773 = ElaboratingArg f a env (updateError ns e)
774774updateError ns (CantUnify b l r e xs sc)
775775 = CantUnify b (updateSolvedTerm ns l) (updateSolvedTerm ns r) (updateError ns e) xs sc
@@ -777,7 +777,7 @@ updateError ns e = e
777777
778778solveInProblems x val [] = []
779779solveInProblems x val ((l, r, env, err) : ps)
780− = ((psubst x val l, psubst x val r,
780+ = ((psubst x val l, psubst x val r,
781781 updateEnv [(x, val)] env, err) : solveInProblems x val ps)
782782
783783mergeNotunified :: Env -> [(Name, Term)] -> ([(Name, Term)], Fails)
@@ -785,7 +785,7 @@ mergeNotunified env ns = mnu ns [] [] where
785785 mnu [] ns_acc ps_acc = (reverse ns_acc, reverse ps_acc)
786786 mnu ((n, t):ns) ns_acc ps_acc
787787 | Just t' <- lookup n ns, t /= t'
788− = mnu ns ((n,t') : ns_acc)
788+ = mnu ns ((n,t') : ns_acc)
789789 ((t,t',env,CantUnify True t t' (Msg "") [] 0, [],Match) : ps_acc)
790790 | otherwise = mnu ns ((n,t) : ns_acc) ps_acc
791791
@@ -796,6 +796,8 @@ updateNotunified ns nu = up nu where
796796 ((n, t') : up nus)
797797
798798-- FIXME: Why not just pass the whole proof state?
799+-- Issue #1716 on the issue tracker.
800+-- https://github.com/idris-lang/Idris-dev/issues/1716
799801updateProblems :: Context -> [(Name, TT Name)] -> Fails -> [Name] -> [Name] -> [Name]
800802 -> ([(Name, TT Name)], Fails)
801803-- updateProblems ctxt [] ps inj holes = ([], ps)
@@ -806,7 +808,7 @@ updateProblems ctxt ns ps inj holes usupp = up ns ps where
806808 y' = updateSolvedTerm ns y
807809 err' = updateError ns err
808810 env' = updateEnv ns env in
809−-- trace ("Updating " ++ show (x',y')) $
811+-- trace ("Updating " ++ show (x',y')) $
810812 case unify ctxt env' x' y' inj holes usupp while of
811813 OK (v, []) -> -- trace ("Added " ++ show v ++ " from " ++ show (x', y')) $
812814 up (ns ++ v) ps
@@ -867,7 +869,7 @@ processTactic (Reorder n) ps
867869 return (ps' { previous = Just ps, plog = "" }, plog ps')
868870processTactic (ComputeLet n) ps
869871 = return (ps { pterm = mkProofTerm $
870− computeLet (context ps) n
872+ computeLet (context ps) n
871873 (getProofTerm (pterm ps)) }, "")
872874processTactic UnifyProblems ps
873875 = let (ns', probs') = updateProblems (context ps) []