@@ -162,12 +162,6 @@ checkPositive n (cn, ty)
162162 = n /= n' && posArg sc
163163 posArg t = True
164164
165−-- Totality checking - check for structural recursion
166−-- (no mutual definitions yet)
167−
168−data LexOrder = LexXX | LexEQ | LexLT
169− deriving (Show, Eq, Ord)
170−
171165calcProd :: IState -> FC -> Name -> [([Name], Term, Term)] -> Idris Totality
172166calcProd i fc n pats = do patsprod <- mapM prodRec pats
173167 if (and patsprod)
@@ -175,15 +169,16 @@ calcProd i fc n pats = do patsprod <- mapM prodRec pats
175169 else return (Partial NotProductive)
176170 where
177171 -- every application of n must be in an argument of a coinductive
178− -- constructor
172+ -- constructor, in every function reachable from here in the
173+ -- call graph.
179174
180175 prodRec :: ([Name], Term, Term) -> Idris Bool
181176 prodRec (_, _, tm) = prod False tm
182177
183178 prod ok ap@(App _ _)
184179 | (P _ (UN "lazy") _, [_, arg]) <- unApply ap = prod ok arg
185− | (P _ f ty, args) <- unApply ap
186− = let co = cotype ty in
180+ | (P nt f ty, args) <- unApply ap
181+ = let co = cotype nt ty in
187182 if f == n
188183 then do argsprod <- mapM (prod co) args
189184 return (and (ok : argsprod) )
@@ -194,12 +189,12 @@ calcProd i fc n pats = do patsprod <- mapM prodRec pats
194189 prod ok (Bind _ b sc) = prod ok sc
195190 prod ok t = return True
196191
197− cotype ty
192+ cotype (DCon _ _) ty
198193 | (P _ t _, _) <- unApply (getRetTy ty)
199194 = case lookupCtxt t (idris_datatypes i) of
200195 [TI _ True _] -> True
201196 _ -> False
202− | otherwise = False
197+ cotype _ _ = False
203198
204199calcTotality :: [Name] -> FC -> Name -> [([Name], Term, Term)]
205200 -> Idris Totality