74fd10a · Idris-dev · git.iko.soy

src/Idris/Coverage.hs+1−1

@@ -143,7 +143,7 @@ recoverableCoverage :: Context -> Err -> Bool

143recoverableCoverage ctxt (CantUnify r (topx, _) (topy, _) e _ _)

144 = let topx' = normalise ctxt [] topx

145 topy' = normalise ctxt [] topy in

146− checkRec topx' topy'

146+ r || checkRec topx' topy'

147 where -- different notion of recoverable than in unification, since we

148 -- have no metavars -- just looking to see if a constructor is failing

149 -- to unify with a function that may be reduced later

test/totality006/totality006b.idr+2−2

@@ -7,8 +7,8 @@ import Data.So

7-- case but not on test006.idr, due to the extra computation.

8total

9blargh : (xs, ys : List a) -> So (length xs > length ys) -> GT (length xs) (length ys)

10−blargh [] [] Oh impossible

11blargh [] (y :: xs) so = absurd so

10blargh [] (y :: xs) so = absurd so

12blargh (y :: xs) [] Oh = LTESucc LTEZero

11blargh (y :: xs) [] Oh = LTESucc LTEZero

13

12

14−-- Missing: blargh (y :: xs) (z :: ys) x = ?blargh_rhs_3

13+-- Missing: blargh (y :: xs) (z :: ys) p = ?blargh_rhs_3

14+-- blargh [] [] p = ?foo -- impossible

test/totality009/TestLambdaImpossible.idr−3

@@ -24,6 +24,3 @@ decElem x (y :: xs) with (decEq x y)

24 decElem x (y :: xs) | (No notHere) | (Yes prf) = Yes (There prf)

25 decElem x (y :: xs) | (No notHere) | (No notThere) = No $ notHereNotThere notHere notThere

26

27−notEta : ((a : Type) -> (b : Type) -> (f : a -> b) -> f = (\x => f x)) -> Void

28−notEta eta = case eta Nat Nat id of

29− Refl impossible