5eaf1f5 · Idris-dev · git.iko.soy

src/Core/Elaborate.hs+1−1

compare with master

unifiedsplit

@@ -601,7 +601,7 @@ try' t1 t2 proofSearch

601 then lift (tfail e1)

602 else lift (tfail e2)

603 else lift (tfail e1)

604− where recoverableErr err@(CantUnify r _ _ _ _ _)

604+ where recoverableErr err@(CantUnify r x y _ _ _)

605 = -- traceWhen r (show err) $

606 r || proofSearch

607 recoverableErr (ProofSearchFail _) = False

src/Core/Unify.hs+6

@@ -508,6 +508,12 @@ recoverable p@(P _ n _) (App f a) = recoverable p f

508-- recoverable (App f a) p@(P _ _ _) = recoverable f p

509recoverable (App f a) (App f' a')

510 = recoverable f f' -- && recoverable a a'

511+recoverable f (Bind _ (Pi _) sc)

512+ | (P (DCon _ _) _ _, _) <- unApply f = False

513+ | (P (TCon _ _) _ _, _) <- unApply f = False

514+recoverable (Bind _ (Pi _) sc) f

515+ | (P (DCon _ _) _ _, _) <- unApply f = False

516+ | (P (TCon _ _) _ _, _) <- unApply f = False

511recoverable _ _ = True

517recoverable _ _ = True

512

518

513errEnv = map (\(x, b) -> (x, binderTy b))

519errEnv = map (\(x, b) -> (x, binderTy b))

src/Idris/AbsSyntax.hs+2−2

@@ -135,10 +135,10 @@ getCoercionsTo i ty =

135 where findCoercions t [] = []

136 findCoercions t (n : ns) =

137 let ps = case lookupTy n (tt_ctxt i) of

138− [ty] -> case unApply (getRetTy ty) of

138+ [ty'] -> case unApply (getRetTy ty') of

139 (t', _) ->

140 if t == t' then [n] else []

141− _ -> [] in

141+ _ -> [] in

142 ps ++ findCoercions t ns

143

144addToCG :: Name -> CGInfo -> Idris ()

src/Idris/ElabTerm.hs+2

@@ -139,6 +139,7 @@ elab ist info pattern tcgen fn tm

139-- ++ "\nholes " ++ show hs

140-- ++ "\nproblems " ++ show ps

141-- ++ "\n-----------\n") $

142+-- trace ("ELAB " ++ show t') $

142 elab' ina t'

143 elab' ina t'

143

144

144 local f = do e <- get_env

145 local f = do e <- get_env

@@ -208,6 +209,7 @@ elab ist info pattern tcgen fn tm

208-- as -> lift $ tfail $ CantResolveAlts (map showHd as)

209-- as -> lift $ tfail $ CantResolveAlts (map showHd as)

209-- trace ("Original " ++ show (length as, as) ++ "\n" ++

210-- trace ("Original " ++ show (length as, as) ++ "\n" ++

210-- "New " ++ show (length as', as)) $

211-- "New " ++ show (length as', as)) $

212+-- traceWhen (length as' > 1) (show as') $

211 tryAll (zip (map (elab' ina) as') (map showHd as'))

213 tryAll (zip (map (elab' ina) as') (map showHd as'))

212 where showHd (PApp _ h _) = show h

214 where showHd (PApp _ h _) = show h

213 showHd x = show x

215 showHd x = show x