@@ -529,18 +529,28 @@ getNatLikeCtors ist =
529529 $ lookupCtxtExact n
530530 $ idris_callgraph ist
531531
532+ isRecursive :: Name -> Name -> Bool
533+ isRecursive tyN cn
534+ | Just (Bind _ Pi{binderTy = P _ argTyN _} _) <- lookupTyExact cn $ tt_ctxt ist
535+ , argTyN == tyN
536+ = True
537+
538+ | otherwise = False
539+
532540 natLikeTypes :: [(Name, Name)]
533541 natLikeTypes = do
534− (_typeName, TI{con_names}) <- toAlist $ idris_datatypes ist
542+ (typeName, TI{con_names}) <- toAlist $ idris_datatypes ist
535543 case con_names of
536544 [z, s]
537545 | getUsedCount z == 0
538546 , getUsedCount s == 1
547+ , isRecursive typeName s
539548 -> [(z, s)]
540549
541550 [s, z]
542551 | getUsedCount z == 0
543552 , getUsedCount s == 1
553+ , isRecursive typeName s
544554 -> [(z, s)]
545555
546556 _ -> [] -- not a 2-constructor family