@@ -35,12 +35,11 @@ checkAllCovering fc done top n | not (n `elem` done)
3535 do let msg = show top ++ " is " ++ show tot ++ " due to " ++ show n
3636 putIState i { idris_totcheckfail = (fc, msg) : idris_totcheckfail i }
3737 addIBC (IBCTotCheckErr fc msg)
38− [Partial _] ->
39− case lookupCtxt n (idris_callgraph i) of
40− [cg] -> mapM_ (checkAllCovering fc (n : done) top)
41− (calls cg)
42− _ -> return ()
43− x -> return () -- stop if total
38+ [Partial (Other ns)] ->
39+ -- Check that none of the partial functions it relies
40+ -- on are partial due to missing cases
41+ mapM_ (checkAllCovering fc (n : done) top) ns
42+ x -> return () -- stop if total, or partial due to recursion
4443checkAllCovering _ _ _ _ = return ()
4544
4645-- | Check whether all 'Inf' arguments to the name end up guaranteed to be