@@ -271,7 +271,7 @@ checkAllCovering _ _ _ _ = return ()
271271
272272checkPositive :: [Name] -> (Name, Type) -> Idris Totality
273273checkPositive mut_ns (cn, ty')
274− = do let ty = delazy ty'
274+ = do let ty = delazy' True ty'
275275 let p = cp ty
276276 i <- getIState
277277 let tot = if p then Total (args ty) else Partial NotPositive
@@ -284,12 +284,19 @@ checkPositive mut_ns (cn, ty')
284284 args t = [0..length (getArgTys t)-1]
285285
286286 cp (Bind n (Pi aty) sc) = posArg aty && cp sc
287− cp t = True
287+ cp t | (P _ n' _, args) <- unApply t,
288+ n' `elem` mut_ns = all noRec args
289+ cp _ = True
288290
289291 posArg (Bind _ (Pi nty) sc)
290292 | (P _ n' _, args) <- unApply nty
291− = n' `notElem` mut_ns && posArg sc
292− posArg t = True
293+ = n' `notElem` mut_ns && all noRec args && posArg sc
294+ posArg t | (P _ n' _, args) <- unApply t,
295+ n' `elem` mut_ns = all noRec args
296+ posArg _ = True
297+
298+ noRec arg = all (\x -> x `notElem` mut_ns) (allTTNames arg)
299+
293300
294301calcProd :: IState -> FC -> Name -> [([Name], Term, Term)] -> Idris Totality
295302calcProd i fc topn pats