6b6aae0 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Avoid retrying unification problems constantly

6b6aae0Edwin Brady12 years ago

src/Idris/Core/Elaborate.hs+3−3

compare with master

unifiedsplit

@@ -687,7 +687,7 @@ no_errors tac err

687 ps' <- get_probs

688 if (length ps' > length ps) then

689 case reverse ps' of

690− ((x, y, env, inerr, while, _) : _) ->

690+ ((x, y, _, env, inerr, while, _) : _) ->

691 let env' = map (\(x, b) -> (x, binderTy b)) env in

692 lift $ tfail $

693 case err of

@@ -796,12 +796,12 @@ prunStateT pmax zok ps x s

796 newpmax = if newps < 0 then 0 else newps in

797 if (newpmax > pmax || (not zok && newps > 0)) -- length ps == 0 && newpmax > 0))

798 then case reverse (problems p) of

799− ((_,_,_,e,_,_):_) -> Error e

799+ ((_,_,_,_,e,_,_):_) -> Error e

800 else OK ((v, newpmax, problems p), s')

801 Error e -> Error e

802

803qshow :: Fails -> String

804−qshow fs = show (map (\ (x, y, _, _, _, _) -> (x, y)) fs)

804+qshow fs = show (map (\ (x, y, _, _, _, _, _) -> (x, y)) fs)

805

806dumpprobs [] = ""

807dumpprobs ((_,_,_,e):es) = show e ++ "\n" ++ dumpprobs es

src/Idris/Core/ProofState.hs+47−54

@@ -144,7 +144,7 @@ instance Pretty ProofState OutputAnnotation where

144holeName i = sMN i "hole"

145

146qshow :: Fails -> String

147−qshow fs = show (map (\ (x, y, _, _, _, t) -> (t, x, y)) fs)

147+qshow fs = show (map (\ (x, y, hs, _, _, _, t) -> (t, x, y, hs)) fs)

148

149match_unify' :: Context -> Env -> TT Name -> TT Name ->

150 StateT TState TC [(Name, TT Name)]

@@ -168,7 +168,8 @@ match_unify' ctxt env topx topy =

168 return u

169 Error e -> traceWhen (unifylog ps)

170 ("No match " ++ show e) $

171− do put (ps { problems = (topx, topy, env, e, while, Match) :

171+ do put (ps { problems = (topx, topy, True,

172+ env, e, while, Match) :

172 problems ps })

173 problems ps })

173 return []

174 return []

174-- traceWhen (unifylog ps)

175-- traceWhen (unifylog ps)

@@ -186,7 +187,7 @@ mergeSolutions env ns = merge [] ns

186 | Just t' <- lookup n ns

187 | Just t' <- lookup n ns

187 = do ps <- get

188 = do ps <- get

188 let probs = problems ps

189 let probs = problems ps

189− put (ps { problems = probs ++ [(t,t',env,Msg "New problem",

190+ put (ps { problems = probs ++ [(t,t',True,env,Msg "New problem",

190 [], Unify)] })

191 [], Unify)] })

191 merge acc ns

192 merge acc ns

192 | otherwise = merge ((n, t): acc) ns

193 | otherwise = merge ((n, t): acc) ns

@@ -225,12 +226,8 @@ unify' ctxt env topx topy =

225 -- problem for each.

226 -- problem for each.

226 uns <- mergeSolutions env (u' ++ ns)

227 uns <- mergeSolutions env (u' ++ ns)

227 ps <- get

228 ps <- get

228− let (ns', probs') = updateProblems (context ps) uns

229+ let (ns', probs') = updateProblems ps uns (fails ++ problems ps)

229− (fails ++ problems ps)

230− (injective ps)

231− (holes ps)

232− (map fst (notunified ps))

233− let (notu', probs_notu) = mergeNotunified env (notu ++ notunified ps)

230+ let (notu', probs_notu) = mergeNotunified env (holes ps) (notu ++ notunified ps)

234 traceWhen (unifylog ps)

231 traceWhen (unifylog ps)

235 ("Now solved: " ++ show ns' ++

232 ("Now solved: " ++ show ns' ++

236 "\nNow problems: " ++ qshow (probs' ++ probs_notu)) $

233 "\nNow problems: " ++ qshow (probs' ++ probs_notu)) $

@@ -780,7 +777,8 @@ keepGiven du (u : us) hs = keepGiven du us hs

780

777

781updateEnv [] e = e

778updateEnv [] e = e

782updateEnv ns [] = []

779updateEnv ns [] = []

780+updateEnv ns ((n, b) : env)

783−updateEnv ns ((n, b) : env) = (n, fmap (updateSolvedTerm ns) b) : updateEnv ns env

781+ = (n, fmap (updateSolvedTerm ns) b) : updateEnv ns env

784

782

785updateError [] err = err

783updateError [] err = err

786updateError ns (At f e) = At f (updateError ns e)

784updateError ns (At f e) = At f (updateError ns e)

@@ -796,13 +794,13 @@ solveInProblems x val ((l, r, env, err) : ps)

796 = ((psubst x val l, psubst x val r,

794 = ((psubst x val l, psubst x val r,

797 updateEnv [(x, val)] env, err) : solveInProblems x val ps)

795 updateEnv [(x, val)] env, err) : solveInProblems x val ps)

798

796

799−mergeNotunified :: Env -> [(Name, Term)] -> ([(Name, Term)], Fails)

797+mergeNotunified :: Env -> [Name] -> [(Name, Term)] -> ([(Name, Term)], Fails)

800−mergeNotunified env ns = mnu ns [] [] where

798+mergeNotunified env holes ns = mnu ns [] [] where

801 mnu [] ns_acc ps_acc = (reverse ns_acc, reverse ps_acc)

799 mnu [] ns_acc ps_acc = (reverse ns_acc, reverse ps_acc)

802 mnu ((n, t):ns) ns_acc ps_acc

800 mnu ((n, t):ns) ns_acc ps_acc

803 | Just t' <- lookup n ns, t /= t'

801 | Just t' <- lookup n ns, t /= t'

804 = mnu ns ((n,t') : ns_acc)

802 = mnu ns ((n,t') : ns_acc)

805− ((t,t',env,CantUnify True t t' (Msg "") [] 0, [],Match) : ps_acc)

803+ ((t,t',True, env,CantUnify True t t' (Msg "") [] 0, [],Match) : ps_acc)

806 | otherwise = mnu ns ((n,t) : ns_acc) ps_acc

804 | otherwise = mnu ns ((n,t) : ns_acc) ps_acc

807

805

808updateNotunified [] nu = nu

806updateNotunified [] nu = nu

@@ -811,42 +809,53 @@ updateNotunified ns nu = up nu where

811 up ((n, t) : nus) = let t' = updateSolvedTerm ns t in

809 up ((n, t) : nus) = let t' = updateSolvedTerm ns t in

812 ((n, t') : up nus)

810 ((n, t') : up nus)

813

811

814−-- FIXME: Why not just pass the whole proof state?

815−-- Issue #1716 on the issue tracker.

816−-- https://github.com/idris-lang/Idris-dev/issues/1716

817−updateProblems :: Context -> [(Name, TT Name)] -> Fails -> [Name] -> [Name] -> [Name]

812+updateProblems :: ProofState -> [(Name, TT Name)] -> Fails

818− -> ([(Name, TT Name)], Fails)

813+ -> ([(Name, TT Name)], Fails)

819-- updateProblems ctxt [] ps inj holes = ([], ps)

814-- updateProblems ctxt [] ps inj holes = ([], ps)

820−updateProblems ctxt ns ps inj holes usupp = up ns ps where

815+updateProblems ps updates probs = up updates probs where

816+ hs = holes ps

817+ inj = injective ps

818+ ctxt = context ps

819+ usupp = map fst (notunified ps)

820+

821 up ns [] = (ns, [])

822− up ns ((x, y, env, err, while, um) : ps) =

822+ up ns (prob@(x, y, ready, env, err, while, um) : ps) =

823− let x' = updateSolvedTerm ns x

823+ let (x', newx) = updateSolvedTerm' ns x

824− y' = updateSolvedTerm ns y

824+ (y', newy) = updateSolvedTerm' ns y

825 err' = updateError ns err

826 env' = updateEnv ns env in

827−-- trace ("Updating " ++ show (x',y')) $

827+ if newx || newy || ready ||

828+ any (\n -> n `elem` inj) (refsIn x ++ refsIn y) then

828− case unify ctxt env' x' y' inj holes usupp while of

829+ case unify ctxt env' x' y' inj hs usupp while of

829− OK (v, []) -> -- trace ("Added " ++ show v ++ " from " ++ show (x', y')) $

830+ OK (v, []) -> -- trace ("DID " ++ show (x',y',ready,v)) $

830 up (ns ++ v) ps

831 up (ns ++ v) ps

831− e -> -- trace ("Failed " ++ show e) $

832+ e -> -- trace ("FAILED " ++ show (x',y',ready,e)) $

833+ let (ns', ps') = up ns ps in

834+ (ns', (x',y', False, env',err', while, um) : ps')

835+ else -- trace ("SKIPPING " ++ show (x,y,ready)) $

832− let (ns', ps') = up ns ps in

836+ let (ns', ps') = up ns ps in

833− (ns', (x',y',env',err', while, um) : ps')

837+ (ns', (x',y', False, env',err', while, um) : ps')

834

838

835-- attempt to solve remaining problems with match_unify

839-- attempt to solve remaining problems with match_unify

836−-- matchProblems :: Bool -> Elab' aux ()

840+matchProblems :: Bool -> ProofState -> [(Name, TT Name)] -> Fails

841+ -> ([(Name, TT Name)], Fails)

837−matchProblems all ns ctxt ps inj holes = up ns ps where

842+matchProblems all ps updates probs = up updates probs where

843+ hs = holes ps

844+ inj = injective ps

845+ ctxt = context ps

846+

838 up ns [] = (ns, [])

847 up ns [] = (ns, [])

839− up ns ((x, y, env, err, while, um) : ps)

848+ up ns ((x, y, ready, env, err, while, um) : ps)

840 | all || um == Match =

849 | all || um == Match =

841 let x' = updateSolvedTerm ns x

850 let x' = updateSolvedTerm ns x

842 y' = updateSolvedTerm ns y

851 y' = updateSolvedTerm ns y

843 err' = updateError ns err

852 err' = updateError ns err

844 env' = updateEnv ns env in

853 env' = updateEnv ns env in

845− case match_unify ctxt env' x' y' inj holes while of

854+ case match_unify ctxt env' x' y' inj hs while of

846 OK v -> -- trace ("Added " ++ show v ++ " from " ++ show (x', y')) $

855 OK v -> -- trace ("Added " ++ show v ++ " from " ++ show (x', y')) $

847 up (ns ++ v) ps

856 up (ns ++ v) ps

848 _ -> let (ns', ps') = up ns ps in

857 _ -> let (ns', ps') = up ns ps in

849− (ns', (x', y', env', err', while, um) : ps')

858+ (ns', (x', y', True, env', err', while, um) : ps')

850 up ns (p : ps) = let (ns', ps') = up ns ps in

859 up ns (p : ps) = let (ns', ps') = up ns ps in

851 (ns', p : ps')

860 (ns', p : ps')

852

861

@@ -865,9 +874,7 @@ processTactic EndUnify ps

865 = let (h, ns_in) = unified ps

874 = let (h, ns_in) = unified ps

866 ns = dropGiven (dontunify ps) ns_in (holes ps)

875 ns = dropGiven (dontunify ps) ns_in (holes ps)

867 ns' = map (\ (n, t) -> (n, updateSolvedTerm ns t)) ns

876 ns' = map (\ (n, t) -> (n, updateSolvedTerm ns t)) ns

868− (ns'', probs') = updateProblems (context ps) ns' (problems ps)

877+ (ns'', probs') = updateProblems ps ns' (problems ps)

869− (injective ps) (holes ps)

870− (map fst (notunified ps))

871 tm' = updateSolved ns'' (pterm ps) in

878 tm' = updateSolved ns'' (pterm ps) in

872 traceWhen (unifylog ps) ("Dropping holes: " ++ show (map fst ns'')) $

879 traceWhen (unifylog ps) ("Dropping holes: " ++ show (map fst ns'')) $

873 return (ps { pterm = tm',

880 return (ps { pterm = tm',

@@ -890,11 +897,7 @@ processTactic (ComputeLet n) ps

890 computeLet (context ps) n

897 computeLet (context ps) n

891 (getProofTerm (pterm ps)) }, "")

898 (getProofTerm (pterm ps)) }, "")

892processTactic UnifyProblems ps

899processTactic UnifyProblems ps

893− = let (ns', probs') = updateProblems (context ps) []

900+ = let (ns', probs') = updateProblems ps [] (problems ps)

894− (problems ps)

895− (injective ps)

896− (holes ps)

897− (map fst (notunified ps))

898 pterm' = updateSolved ns' (pterm ps) in

901 pterm' = updateSolved ns' (pterm ps) in

899 traceWhen (unifylog ps) ("Dropping holes: " ++ show (map fst ns')) $

902 traceWhen (unifylog ps) ("Dropping holes: " ++ show (map fst ns')) $

900 return (ps { pterm = pterm', solved = Nothing, problems = probs',

903 return (ps { pterm = pterm', solved = Nothing, problems = probs',

@@ -903,14 +906,8 @@ processTactic UnifyProblems ps

903 recents = recents ps ++ map fst ns',

906 recents = recents ps ++ map fst ns',

904 holes = holes ps \\ (map fst ns') }, plog ps)

907 holes = holes ps \\ (map fst ns') }, plog ps)

905processTactic (MatchProblems all) ps

908processTactic (MatchProblems all) ps

906− = let (ns', probs') = matchProblems all [] (context ps)

909+ = let (ns', probs') = matchProblems all ps [] (problems ps)

907− (problems ps)

908− (injective ps)

909− (holes ps)

910− (ns'', probs'') = matchProblems all ns' (context ps)

910+ (ns'', probs'') = matchProblems all ps ns' probs'

911− probs'

912− (injective ps)

913− (holes ps)

914 pterm' = updateSolved ns'' (pterm ps) in

911 pterm' = updateSolved ns'' (pterm ps) in

915 traceWhen (unifylog ps) ("Dropping holes: " ++ show (map fst ns'')) $

912 traceWhen (unifylog ps) ("Dropping holes: " ++ show (map fst ns'')) $

916 return (ps { pterm = pterm', solved = Nothing, problems = probs'',

913 return (ps { pterm = pterm', solved = Nothing, problems = probs'',

@@ -926,11 +923,7 @@ processTactic t ps

926 = case solved ps' of

923 = case solved ps' of

927 Just s -> traceWhen (unifylog ps')

924 Just s -> traceWhen (unifylog ps')

928 ("SOLVED " ++ show s) $

925 ("SOLVED " ++ show s) $

929− updateProblems (context ps')

930− [s] (problems ps')

926+ updateProblems ps [s] (problems ps')

931− (injective ps')

932− (holes ps')

933− (map fst (notunified ps))

934 _ -> ([], problems ps')

927 _ -> ([], problems ps')

935 -- rechecking problems may find more solutions, so

928 -- rechecking problems may find more solutions, so

936 -- apply them here

929 -- apply them here

src/Idris/Core/ProofTerm.hs+6−4

@@ -5,7 +5,7 @@

5 evaluation/checking inside the proof system, etc. --}

7module Idris.Core.ProofTerm(ProofTerm, Goal(..), mkProofTerm, getProofTerm,

8− updateSolved, updateSolvedTerm,

8+ updateSolved, updateSolvedTerm, updateSolvedTerm',

9 bound_in, bound_in_term, refocus,

10 Hole, RunTactic',

11 goal, atHole) where

@@ -124,13 +124,15 @@ hole (Guess _ _) = True

124hole _ = False

125

126updateSolvedTerm :: [(Name, Term)] -> Term -> Term

127−updateSolvedTerm [] x = x

127+updateSolvedTerm xs x = fst $ updateSolvedTerm' xs x

128+

129+updateSolvedTerm' [] x = (x, False)

128−updateSolvedTerm xs x = -- updateSolved' xs x where

130+updateSolvedTerm' xs x = -- updateSolved' xs x where

129-- This version below saves allocations, because it doesn't need to reallocate

131-- This version below saves allocations, because it doesn't need to reallocate

130-- the term if there are no updates to do.

132-- the term if there are no updates to do.

131-- The Bool is ugly, and probably 'Maybe' would be less ugly, but >>= is

133-- The Bool is ugly, and probably 'Maybe' would be less ugly, but >>= is

132-- the wrong combinator. Feel free to tidy up as long as it's still as cheap :).

134-- the wrong combinator. Feel free to tidy up as long as it's still as cheap :).

133− fst $ updateSolved' xs x where

135+ updateSolved' xs x where

134 updateSolved' [] x = (x, False)

136 updateSolved' [] x = (x, False)

135 updateSolved' xs (Bind n (Hole ty) t)

137 updateSolved' xs (Bind n (Hole ty) t)

136 | Just v <- lookup n xs

138 | Just v <- lookup n xs

src/Idris/Core/Unify.hs+15−9

@@ -29,11 +29,13 @@ data FailContext = FailContext { fail_sourceloc :: FC,

29 deriving (Eq, Show)

31type Injs = [(TT Name, TT Name, TT Name)]

32+type Fails = [(TT Name, TT Name, -- unification error

33+ Bool, -- ready to retry yet

32−type Fails = [(TT Name, TT Name, Env, Err, [FailContext], FailAt)]

34+ Env, Err, [FailContext], FailAt)]

34unrecoverable :: Fails -> Bool

36unrecoverable :: Fails -> Bool

35unrecoverable = any bad

37unrecoverable = any bad

36− where bad (_,_,_, err, _, _) = unrec err

38+ where bad (_,_,_,_, err, _, _) = unrec err

38 unrec (CantUnify r _ _ _ _ _) = not r

40 unrec (CantUnify r _ _ _ _ _) = not r

39 unrec (At _ e) = unrec e

41 unrec (At _ e) = unrec e

@@ -129,7 +131,7 @@ match_unify ctxt env topx topy inj holes from =

129 let err = cantUnify from r

131 let err = cantUnify from r

130 topx topy (CantUnify r x y (Msg "") (errEnv env) s) (errEnv env) s

132 topx topy (CantUnify r x y (Msg "") (errEnv env) s) (errEnv env) s

131 if (not r) then lift $ tfail err

133 if (not r) then lift $ tfail err

132− else do put (UI s ((x, y, env, err, from, Match) : f))

134+ else do put (UI s ((x, y, True, env, err, from, Match) : f))

133 lift $ tfail err

135 lift $ tfail err

134

136

135

137

@@ -144,7 +146,9 @@ match_unify ctxt env topx topy inj holes from =

144 let err = cantUnify from r topx topy

146 let err = cantUnify from r topx topy

145 (CantUnify r (binderTy x) (binderTy y) (Msg "") (errEnv env) s)

147 (CantUnify r (binderTy x) (binderTy y) (Msg "") (errEnv env) s)

146 (errEnv env) s

148 (errEnv env) s

147− put (UI s ((binderTy x, binderTy y, env, err, from, Match) : f))

149+ put (UI s ((binderTy x, binderTy y,

150+ False,

151+ env, err, from, Match) : f))

148 return []

152 return []

149

153

150 notHole (Hole _) = False

154 notHole (Hole _) = False

@@ -162,7 +166,7 @@ match_unify ctxt env topx topy inj holes from =

162 (normalise ctxt env y)

166 (normalise ctxt env y)

163 let err = cantUnify from r

167 let err = cantUnify from r

164 topx topy (CantUnify r x y (Msg "") (errEnv env) s) (errEnv env) s

168 topx topy (CantUnify r x y (Msg "") (errEnv env) s) (errEnv env) s

165− put (UI s ((x, y, env, err, from, Match) : f))

169+ put (UI s ((x, y, True, env, err, from, Match) : f))

166 lift $ tfail err

170 lift $ tfail err

167 combine bnames as [] = return as

171 combine bnames as [] = return as

168 combine bnames as ((n, t) : bs)

172 combine bnames as ((n, t) : bs)

@@ -446,7 +450,7 @@ unify ctxt env topx topy inj holes usersupp from =

446 let err = cantUnify from r

450 let err = cantUnify from r

447 topx topy (CantUnify r x y (Msg "") (errEnv env) s) (errEnv env) s

451 topx topy (CantUnify r x y (Msg "") (errEnv env) s) (errEnv env) s

448 if (not r) then lift $ tfail err

452 if (not r) then lift $ tfail err

449− else do put (UI s ((x, y, env, err, from, Unify) : f))

453+ else do put (UI s ((x, y, True, env, err, from, Unify) : f))

450 return [] -- lift $ tfail err

454 return [] -- lift $ tfail err

451

455

452 unApp fn bnames appx@(App fx ax) appy@(App fy ay)

456 unApp fn bnames appx@(App fx ax) appy@(App fy ay)

@@ -540,7 +544,7 @@ unify ctxt env topx topy inj holes usersupp from =

540 let r = recoverable (normalise ctxt env x) (normalise ctxt env y)

544 let r = recoverable (normalise ctxt env x) (normalise ctxt env y)

541 let err = cantUnify from r

545 let err = cantUnify from r

542 topx topy (CantUnify r x y (Msg "") (errEnv env) s) (errEnv env) s

546 topx topy (CantUnify r x y (Msg "") (errEnv env) s) (errEnv env) s

543− put (UI s ((topx, topy, env, err, from, Unify) : f))

547+ put (UI s ((topx, topy, True, env, err, from, Unify) : f))

544 return []

548 return []

545

549

546 -- shortcut failure, if we *know* nothing can fix it

550 -- shortcut failure, if we *know* nothing can fix it

@@ -548,7 +552,7 @@ unify ctxt env topx topy inj holes usersupp from =

548 let r = recoverable (normalise ctxt env x) (normalise ctxt env y)

552 let r = recoverable (normalise ctxt env x) (normalise ctxt env y)

549 let err = cantUnify from r

553 let err = cantUnify from r

550 topx topy (CantUnify r x y (Msg "") (errEnv env) s) (errEnv env) s

554 topx topy (CantUnify r x y (Msg "") (errEnv env) s) (errEnv env) s

551− put (UI s ((topx, topy, env, err, from, Unify) : f))

555+ put (UI s ((topx, topy, True, env, err, from, Unify) : f))

552 lift $ tfail err

556 lift $ tfail err

553

557

554

558

@@ -572,7 +576,9 @@ unify ctxt env topx topy inj holes usersupp from =

572 let err = cantUnify from r topx topy

576 let err = cantUnify from r topx topy

573 (CantUnify r (binderTy x) (binderTy y) (Msg "") (errEnv env) s)

577 (CantUnify r (binderTy x) (binderTy y) (Msg "") (errEnv env) s)

574 (errEnv env) s

578 (errEnv env) s

575− put (UI s ((binderTy x, binderTy y, env, err, from, Unify) : f))

579+ put (UI s ((binderTy x, binderTy y,

580+ False,

581+ env, err, from, Unify) : f))

576 return [] -- lift $ tfail err

582 return [] -- lift $ tfail err

577

583

578 checkCycle ns p@(x, P _ _ _) = return [p]

584 checkCycle ns p@(x, P _ _ _) = return [p]

src/Idris/Elab/Clause.hs+2−2

@@ -573,7 +573,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)

573 inj <- get_inj

574 return (res, probs, inj))

575

576− when inf $ addTyInfConstraints fc (map (\(x,y,_,_,_,_) -> (x,y)) probs)

576+ when inf $ addTyInfConstraints fc (map (\(x,y,_,_,_,_,_) -> (x,y)) probs)

577

578 let lhs_tm = orderPats (getInferTerm lhs')

579 let lhs_ty = getInferType lhs'

@@ -656,7 +656,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)

656 probs <- get_probs

657 return (tm, ds, is, probs))

658

659− when inf $ addTyInfConstraints fc (map (\(x,y,_,_,_,_) -> (x,y)) probs)

659+ when inf $ addTyInfConstraints fc (map (\(x,y,_,_,_,_,_) -> (x,y)) probs)

660

661 logLvl 5 "DONE CHECK"

662 logLvl 2 $ "---> " ++ show rhs'

src/Idris/ElabTerm.hs+5−5

@@ -87,9 +87,9 @@ build ist info emode opts fn tm

87 probs <- get_probs

88 case probs of

89 [] -> return ()

90− ((_,_,_,e,_,_):es) -> traceWhen u ("Final problems:\n" ++ show probs) $

90+ ((_,_,_,_,e,_,_):es) -> traceWhen u ("Final problems:\n" ++ show probs) $

91− if inf then return ()

91+ if inf then return ()

92− else lift (Error e)

92+ else lift (Error e)

94 when tydecl (do update_term orderPats

95 mkPat)

@@ -128,8 +128,8 @@ buildTC ist info emode opts fn tm

128 tm <- get_term

129 case probs of

130 [] -> return ()

131− ((_,_,_,e,_,_):es) -> if inf then return ()

131+ ((_,_,_,_,e,_,_):es) -> if inf then return ()

132− else lift (Error e)

132+ else lift (Error e)

133 is <- getAux

134 tt <- get_term

135 let (tm, ds) = runState (collectDeferred (Just fn) tt) []

src/Idris/Prover.hs+1−1

@@ -111,7 +111,7 @@ elabStep st e = case runStateT eCheck st of

111 ctxt <- get_context

112 lift $ check ctxt [] (forget tm)

113 return res

114− ((_,_,_,e,_,_):_) -> lift $ Error e

114+ ((_,_,_,_,e,_,_):_) -> lift $ Error e

115

116dumpState :: IState -> ProofState -> Idris ()

117dumpState ist (PS nm [] _ _ tm _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) =