62705e4 · Idris-dev · git.iko.soy

src/Idris/Core/Elaborate.hs+1

@@ -646,6 +646,7 @@ no_errors tac err

646 Error _ -> lift $ Error e

647 OK (a, s') -> do put s'

648 return a

649+ unifyProblems

649 ps' <- get_probs

650 ps' <- get_probs

650 if (length ps' > length ps) then

651 if (length ps' > length ps) then

651 case reverse ps' of

652 case reverse ps' of

src/Idris/Core/ProofState.hs+3−2

@@ -817,8 +817,9 @@ mergeNotunified :: Env -> [(Name, Term)] -> ([(Name, Term)], Fails)

817mergeNotunified env ns = mnu ns [] [] where

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

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

820− | Just t' <- lookup n ns = mnu ns ((n,t) : ns_acc)

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

821+ = mnu ns ((n,t') : ns_acc)

821− ((t,t',env,Msg "", [],Match) : ps_acc)

822+ ((t,t',env,Msg "", [],Unify) : ps_acc)

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

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

823

824

824updateNotunified [] nu = nu

825updateNotunified [] nu = nu

src/Idris/Prover.hs+1

@@ -85,6 +85,7 @@ prove opt ctxt lit n ty

85 [([], P Ref n ty, ptm)]

86 [([], P Ref n ty, ptm')] ty)

87 solveDeferred n

88+

88elabStep :: ElabState [PDecl] -> ElabD a -> Idris (a, ElabState [PDecl])

89elabStep :: ElabState [PDecl] -> ElabD a -> Idris (a, ElabState [PDecl])

89elabStep st e = case runStateT eCheck st of

90elabStep st e = case runStateT eCheck st of

90 OK (a, st') -> return (a, st')

91 OK (a, st') -> return (a, st')