@@ -529,18 +529,28 @@ getNatLikeCtors ist =
529 $ lookupCtxtExact n
529 $ lookupCtxtExact n
530 $ idris_callgraph ist
530 $ idris_callgraph ist
532+ isRecursive :: Name -> Name -> Bool
534+ | Just (Bind _ Pi{binderTy = P _ argTyN _} _) <- lookupTyExact cn $ tt_ctxt ist
532 natLikeTypes :: [(Name, Name)]
540 natLikeTypes :: [(Name, Name)]
533 natLikeTypes = do
541 natLikeTypes = do
534− (_typeName, TI{con_names}) <- toAlist $ idris_datatypes ist
542+ (typeName, TI{con_names}) <- toAlist $ idris_datatypes ist
535 case con_names of
543 case con_names of
537 | getUsedCount z == 0
545 | getUsedCount z == 0
538 , getUsedCount s == 1
546 , getUsedCount s == 1
547+ , isRecursive typeName s
539 -> [(z, s)]
548 -> [(z, s)]
542 | getUsedCount z == 0
551 | getUsedCount z == 0
543 , getUsedCount s == 1
552 , getUsedCount s == 1
553+ , isRecursive typeName s
544 -> [(z, s)]
554 -> [(z, s)]
546 _ -> [] -- not a 2-constructor family
556 _ -> [] -- not a 2-constructor family