What will go wrong if a recursive record type has a negative eta rule?

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?

• Note that out is an empty type in Agda. – András Kovács Mar 30 at 15:25
• @AndrásKovács Yes this is explained in the issue. So if Agda permits this eta rule, where can I found a semantical justification? or is it trivial? – molikto Mar 30 at 15:41

Having a recursive record type with eta-equality wouldn't destroy consistency of the theory, but it would destroy decidability of typechecking.

For example, let's define your out type as a record type in Agda:

record Out : Set where
inductive
constructor cons
field
in : Out


Agda doesn't use eta-equality for this type. Suppose it did, then Agda's typechecker would loop whenever it tries to solve an equation of the form x = y : Out (where x and y are two variables or neutral terms): x = y iff in x = in y iff in (in x) = in (in y) iff in (in (in x)) = in (in (in y)) ...

• Is this just true for Agda or generally all implementations? If we don't have meta variable and unification, can we don't eta-expand when both side are generic value, and just return x != y? – molikto Mar 31 at 2:23
• This argument only shows that a certain typechecking strategy isn’t termination, but it doesn’t seem to prove that typechecking is undecidable, or do I miss something? @molikto even without type inference, type checking needs to decide if terms are judgmentally/definitionally equal. – Blaisorblade Mar 31 at 17:21
• This is true in general, see this paper by Berger and Setzer. – Henning Basold Apr 6 at 10:24
• @HenningBasold I don't think this paper is related. it deals with coinductive types without eta rules, the recursive record type I mentioned is a special case of inductive type – molikto Apr 7 at 10:52
• I now understand that the above is even true without meta variables. The "equations" is just type directed conversion checking algorithm. But still, one choice is turn off eta for non-guarded recursive record. Another one is simply say all items of a non-guarded recursive record is equal. They are empty anyway. Not sure if this is sound. (practically this doesn't matter, because these types has not much use?) – molikto Apr 19 at 11:29