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

git.iko.soy/Idris-dev

Fix 'impossible' check

It should never reject recoverable unification errors as impossible. This fixes the eta is inconsistent "proof".

commit74fd10acf4a60190bfa7aa4d7fca823428f39c91 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSat 9 May 2015, 19:15 (11 years ago) parentcbb86b2

3 files changed+3−6

unifiedsplit

src/Idris/Coverage.hs+1−1

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

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

144144 = let topx' = normalise ctxt [] topx

145145 topy' = normalise ctxt [] topy in

146− checkRec topx' topy'

146+ r || checkRec topx' topy'

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

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

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

test/totality006/totality006b.idr+2−2

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

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

88total

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

10−blargh [] [] Oh impossible

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

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

1312

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)

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

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

2626

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