I've been meaning to file this for a year, but better late than never I guess...
While we haven't encountered a need so far, we need a way to represent mutually-recursive types[1]. I'm assuming we can just go for the normal OCaml/SML:
type odd 'z =
| OddS : even 'n -> odd (S 'n)
and even 'z =
| EvenZ : even Z
| EvenS : odd 'n -> even (S 'n)
I assume, while doing this, it may also be useful to add support for mutually-recursive class instances.
[1] So technically you can represent mutually-recursive types as an inductive type indexed by a "which type is this" type, but I'd rather not.
I've been meaning to file this for a year, but better late than never I guess...
While we haven't encountered a need so far, we need a way to represent mutually-recursive types[1]. I'm assuming we can just go for the normal OCaml/SML:
I assume, while doing this, it may also be useful to add support for mutually-recursive class instances.
[1] So technically you can represent mutually-recursive types as an inductive type indexed by a "which type is this" type, but I'd rather not.