@@ -211,7 +211,7 @@ genAll i args
211211 let p = resugar (PApp fc (PRef fc n) (zipWith upd xs' xs))
212212 let tyn = getTy n (tt_ctxt i)
213213 case lookupCtxt tyn (idris_datatypes i) of
214− (TI ns _ _ _ : _) -> p : map (mkPat fc) (ns \\ [n])
214+ (TI ns _ _ _ _ : _) -> p : map (mkPat fc) (ns \\ [n])
215215 _ -> [p]
216216 ops fc n arg o = return Placeholder
217217
@@ -265,29 +265,38 @@ checkAllCovering fc done top n | not (n `elem` done)
265265 x -> return () -- stop if total
266266checkAllCovering _ _ _ _ = return ()
267267
268−-- Check if, in a given type n, the constructor cn : ty is strictly positive,
268+-- Check if, in a given group of type declarations mut_ns,
269+-- the constructor cn : ty is strictly positive,
269270-- and update the context accordingly
270271
271−checkPositive :: Name -> (Name, Type) -> Idris ()
272−checkPositive n (cn, ty')
273− = do let ty = delazy ty'
272+checkPositive :: [Name] -> (Name, Type) -> Idris Totality
273+checkPositive mut_ns (cn, ty')
274+ = do let ty = delazy' True ty'
274275 let p = cp ty
275276 i <- getIState
276277 let tot = if p then Total (args ty) else Partial NotPositive
277278 let ctxt' = setTotal cn tot (tt_ctxt i)
278279 putIState (i { tt_ctxt = ctxt' })
279− logLvl 5 $ "Constructor " ++ show cn ++ " is " ++ show tot
280+ logLvl 5 $ "Constructor " ++ show cn ++ " is " ++ show tot ++ " with " ++ show mut_ns
280281 addIBC (IBCTotal cn tot)
282+ return tot
281283 where
282284 args t = [0..length (getArgTys t)-1]
283285
284286 cp (Bind n (Pi aty) sc) = posArg aty && cp sc
285− cp t = True
287+ cp t | (P _ n' _, args) <- unApply t,
288+ n' `elem` mut_ns = all noRec args
289+ cp _ = True
286290
287291 posArg (Bind _ (Pi nty) sc)
288292 | (P _ n' _, args) <- unApply nty
289− = n /= n' && posArg sc
290− 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+
291300
292301calcProd :: IState -> FC -> Name -> [([Name], Term, Term)] -> Idris Totality
293302calcProd i fc topn pats
@@ -335,7 +344,7 @@ calcProd i fc topn pats
335344 cotype (DCon _ _) n ty
336345 | (P _ t _, _) <- unApply (getRetTy ty)
337346 = case lookupCtxt t (idris_datatypes i) of
338− [TI _ True _ _] -> True
347+ [TI _ True _ _ _] -> True
339348 _ -> False
340349 cotype nt n ty = False
341350
@@ -383,6 +392,14 @@ checkTotality path fc n
383392 setTotality n t'
384393 addIBC (IBCTotal n t')
385394 return t'
395+ [TyDecl (DCon _ _) ty] ->
396+ case unApply (getRetTy ty) of
397+ (P _ tyn _, _) -> do
398+ let ms = case lookupCtxt tyn (idris_datatypes i) of
399+ [TI _ _ _ _ xs@(_:_)] -> xs
400+ ts -> [tyn]
401+ checkPositive ms (n, ty)
402+ _-> return $ Total []
386403 _ -> return $ Total []
387404 x -> return x
388405 case t' of
@@ -556,7 +573,7 @@ buildSCG' ist pats args = nub $ concatMap scgPat pats where
556573
557574 isInductive (P _ nty _) (P _ nty' _) =
558575 let co = case lookupCtxt nty (idris_datatypes ist) of
559− [TI _ x _ _] -> x
576+ [TI _ x _ _ _] -> x
560577 _ -> False in
561578 nty == nty' && not co
562579 isInductive _ _ = False
@@ -639,7 +656,7 @@ checkMP ist i mp = if i > 0
639656 = case lookupTotal f (tt_ctxt ist) of
640657 [Total _] -> Unchecked -- okay so far
641658 [Partial _] -> Partial (Other [f])
642− x -> error (show x)
659+ x -> error $ "CAN'T HAPPEN: " ++ (show x)
643660 | [TyDecl (TCon _ _) _] <- lookupDef f (tt_ctxt ist)
644661 = Total []
645662 tryPath desc path (e@(f, args) : es) arg