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

git.iko.soy/Idris-dev

Extend rules for 'impossible' cases

If there's a unification failure due to an infinite cycle, then that's an impossible case rather than a valid one

commit6efe40b9acc22796ce77420cd176acd2804a1ab4 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSat 30 Jan 2016, 23:05 (11 years ago) parent7540bb3

2 files changed+4−3

unifiedsplit

libs/prelude/Prelude/Basics.idr+3−3

@@ -53,9 +53,9 @@ data Dec : Type -> Type where

5353

5454 ||| The case where the property holds

5555 ||| @ prf the proof

56− Yes : {A : Type} -> (prf : A) -> Dec A

56+ Yes : (prf : prop) -> Dec prop

5757

5858 ||| The case where the property holding would be a contradiction

59− ||| @ contra a demonstration that A would be a contradiction

60− No : {A : Type} -> (contra : A -> Void) -> Dec A

59+ ||| @ contra a demonstration that prop would be a contradiction

60+ No : (contra : prop -> Void) -> Dec prop

6161

src/Idris/Coverage.hs+1

@@ -135,6 +135,7 @@ validCoverageCase ctxt (CantUnify _ (topx, _) (topy, _) e _ _)

135135 = case (unApply topx, unApply topy) of

136136 ((P _ x _, _), (P _ y _, _)) -> x == y

137137 _ -> False

138+validCoverageCase ctxt (InfiniteUnify _ _ _) = False

138139validCoverageCase ctxt (CantConvert _ _ _) = False

139140validCoverageCase ctxt (At _ e) = validCoverageCase ctxt e

140141validCoverageCase ctxt (Elaborating _ _ _ e) = validCoverageCase ctxt e