Don't reset totality for non-total things
We recheck everything at the end of checking a module, but if things
are currently known non-covering, we're not going to check that again,
so resetting means that that information is lost. So better only to
recheck things whcih are currently believed total, now that we have
complete information about the module.
Fixes #689
commite803aea54773241451081f82e3799480b22130de
authorEdwin Brady <ecb10@st-andrews.ac.uk>
dateSun 1 Dec 2013, 21:30 (13 years ago)
parent6c496b7
libs/base/Data/Vect/Quantifiers.idr+2−2
@@ -5,8 +5,8 @@ data Any : (P : a -> Type) -> Vect n a -> Type where
55 There : {P : a -> Type} -> {xs : Vect n a} -> Any P xs -> Any P (x :: xs)
66
77anyNilAbsurd : {P : a -> Type} -> Any P Nil -> _|_
8−anyNilAbsurd Here impossible
9−anyNilAbsurd There impossible
8+anyNilAbsurd (Here _) impossible
9+anyNilAbsurd (There _) impossible
1010
1111anyElim : {xs : Vect n a} -> {P : a -> Type} -> (Any P xs -> b) -> (P x -> b) -> Any P (x :: xs) -> b
1212anyElim _ f (Here p) = f p
src/Idris/Parser.hs+4−1
@@ -1054,7 +1054,10 @@ loadSource h lidr f
10541054 -- Redo totality check for deferred names
10551055 let deftots = idris_defertotcheck i
10561056 iLOG $ "Totality checking " ++ show deftots
1057− mapM_ (\x -> setTotality x Unchecked) (map snd deftots)
1057+ mapM_ (\x -> do tot <- getTotality x
1058+ case tot of
1059+ Total _ -> setTotality x Unchecked
1060+ _ -> return ()) (map snd deftots)
10581061 mapM_ buildSCG deftots
10591062 mapM_ checkDeclTotality deftots
10601063