In the context of Agda like dependent type theory:
This short paper https://jesper.sikanda.be/files/vectors-are-records-too.pdf says some inductive type can be seen as records, for example
Vector of fixed-length list can be seen as inductively-defined family of non-recursive types.
But they argue that for example natural number type should not have a eta rule because it is a recursive type (the original paper says
N = Unit \/ N is non-terminating.)
So what will go wrong if we have this type:
data out where cons : out => out in : out => out in (cons a) = a
and give it a negative eta-rule:
(a: out) then
a = cons (in a) judgementally
Can it proof
False? Or just this is a bad idea....?
edit: It seems Agda has eta-rule for recursive records? but not for the one previously defined, see this issue https://github.com/agda/agda/issues/402 . but the previously defined one is ruled out I think by implementation issues, not theoretical one?