## Support induction recursion

Now that we have `-XTypeInType`

, let's take it a step further and allow induction recursion. This feature exists in Agda and Idris. Here is a short example of what can be done in Agda:

```
mutual
-- Codes for types.
data U : Set where
nat : U
pi : (a : U) → (El a → U) → U
-- A function that interprets codes as actual types.
El : U → Set
El nat = ℕ
El (pi a b) = (x : El a) → El (b x)
```

Note that the `U`

datatype and the `El`

function depend on each other. But if you look more closely, the header for `U`

does not depend on `El`

; only the constructors of `U`

depend on `El`

. So if we typecheck `U : Set`

first, then `El : U → Set`

, then the constructors of `U`

, then the equations of `El`

, we're OK.

Translation into Haskell:

```
import Data.Kind
data family Sing (a :: k) -- we still require singletons
data U :: Type where
Nat :: U
Pi :: Sing (a :: U) -> (El a -> U) -> U
type family El (u :: U) :: Type where
El 'Nat = Int
El (Pi a b) = forall (x :: El a). Sing x -> El (b x)
```

This currently errors with

```
• Type constructor ‘U’ cannot be used here
(it is defined and used in the same recursive group)
• In the kind ‘U’
```

It needn't error. (I'm cheating a bit here, because for unrelated reasons, we can't return a `forall`

on the right-hand side of a type family. But that's not the issue at hand.)

I have some very sketchy notes on how we might do this here.

## Trac metadata

Trac field | Value |
---|---|

Version | 8.1 |

Type | FeatureRequest |

TypeOfFailure | OtherFailure |

Priority | normal |

Resolution | Unresolved |

Component | Compiler |

Test case | |

Differential revisions | |

BlockedBy | |

Related | |

Blocking | |

CC | |

Operating system | |

Architecture |