Why do record based inductive types with primitive projections lack an eta law?

Question

In Coq there is ongoing work to shore up some weaknesses in subject reduction and coinductive types. Primitive projections are part of that effort for better behaviour.

I get why there might be complications with eta reduction for coinductive types with primitive projections but what's the problem with inductive types?

For context I'm playing with a minor variant of W types and I basically have to decide between

Inductive W {A: Set} (B: A -> Set) :=
| sup s (p: B s -> W B).

and

Inductive W {A: Set} (B: A -> Set) := sup {
  tag: A ;
  field (ix: B tag): W B ;
}.

With primitive projections the latter lacks an eta law. You can do a sort of variant of an induction principle here but it's more than a little awkward and I don't really understand the how and whys here.

I don't have any evidence for my intuition and the record encoding is a little awkward to use sometimes but my intuition just says the record encoding looks prettier. It definitely might not be the best choice though.

Answer 1

Reduction will not terminate if you give W an eta law. Fixpoints only reduce when applied to constructors. However, if you have F : W B -> C such that F (sup t f) reduces to F_step t f (fun x => F (f x)), then F x would reduce to F (sup x.(tag) x.(field)) which would reduce to F_step x.(tag) x.(field) (fun y => F (x.(field) y)). Reduction would then continue under binders ad infinitum.

---

We can also consider restricting our attention to just conversion. Consider a Turing Machine runner that uses @W unit (fun _ => unit) for termination fuel and computes whether the Turing Machine halts. Even though the type is uninhabited, fun fuel => does_it_halt TM fuel will be convertible with fun _ => true whenever TM halts. Hence the eta rule forces conversion to decide the halting problem.