Post #1865894

@jnkrtech How "wild"? I've got some non-uniform recursion in an Idris library I recently published. https://stefan-hoeck.github.io/idris2-pack-db/docs/type-aligned/docs/docs/TypeAligned.src.html#line270 I've also got recursion across multiple types (merged into a single indexed family) "fully" generalized in the Haskell version of another published Idris library (the Haskell version is not published). https://gitlab.com/bss03/nested/-/blob/31f74ced9067ff04b80fbe22ab5b5f153436f6ea/test/hs/Main.hs#L133