Intuition of the problem
A good rule of thumb is to consider that in intensional type theory, coinductive types and function types share a lot of properties. In particular, equality over streams is equally as evil as equality over functions, in so far as it almost never holds without assuming additional extensionality principles. The only way to prove such an equality is essentially by reflexivity.
As observed in the question, the current typing rules of coinductive types allow proving eta-expansion as a theorem
Axiom Cons_hd_tl : forall A s, s = Cons A (hd A s) (tl A s).
which does not hold by reflexivity for any closed stream s, thus breaking subject reduction.
The deep root of the issue comes from the dependent elimination rule of coinductive types, since it allows proving that any coinductive term is necessarily a constructor. This is clearly breaking parametricity, as there are closed terms of coinductive types that do not even start with a constructor, namely cofixpoints. The SR failure is a consequence of this.
Why Subject Reduction?
There are various reasons to desire SR, some of them theoretical, some of them practical.
- On the theoretical side, it makes the semantics of the type theory hard to define naturally. The soundness of an implementation of a type-checker for such a theory becomes quite murky as a consequence. One has to defensively guard against SR breakages, or face weird ill-typed situations otherwise. The issue is much more important than in non-dependent type systems, because the typing rules themselves embed the runtime semantics of the program, hence any defect of the latter percolates into the former.
- On the practical side, this is not a black-and-white issue. It actually depends on the magnitude of SR breakage. One can survive within a locally broken system (case in point: Coq), but the more failures of SR, the less practical the proof assistant. Indeed, failure of SR means that type-checking is not stable by the equational theory of the language, a clear source of non-modularity. A perfectly fine proposition may become ill-typed after substituting a subterm by another convertible one. This is particularly infuriating when it happens because it is virtually impossible to debug, as one has to manually apply the typing rules to see where it fails.
Thankfully, in Coq, the practical issues of SR are exceedingly uncommon, for two reasons. First, the use of coinduction in Coq is somewhat marginal compared to the rest of the features of the system. Second, even developments using coinduction rarely rely on the computational content of the proofs and most coinduction is performed in opaque Prop proofs. Yet, the theoretical defects are still annoying. For instance, the MetaCoq formalization of CIC uses SR in critical parts. Thus implementing coinductive types as found in today's Coq will be problematic.
Solutions
There are two possible solutions to recover SR for positive coinductive types, a brutal one and a finer-grained one.
The not-reasonable one
The brutal one is to eschew decidability of type-checking altogether and allow infinite unfolding of (co)fixpoints. While fixing SR, this is not reasonable. Decidability of type-checking is pretty much the core of the claim of the foundational status of proof systems like CIC. Furthermore, any actual implementation of an undecidable type-system will eventually fail at some point, be it intentionally (e.g., if the system implements some kind of timeout) or unintentionally (e.g., because of stack overflow or out-of-memory errors). This is intuitively a failure of SR in disguise, and implicitly indicates that there are now two logical systems, the "ideal" one and the "implemented" one.
The reasonable one
The cleverer solution is to attack the problem at the root, which was argued above to be dependent elimination of positive coinductive types. It is evil to assume that a coinductive term is always a constructor, the only thing that is allowed is to depend on the observations that one can perform with it. In the case of negative coinductive types, observations are primitive notions defined to be the projections of that type, so this is guaranteed by construction. For their positive flavour, one has to be slightly more imaginative and stare at the typing rule of dependent elimination.
I have a proposal implemented as a PR that, to the best of my understanding, is enough to restore SR. The idea is to restrict the return type of coinductive pattern-matching in a way that is reminiscent of the restriction of inductive dependent pattern-matching in presence of side-effects.
The criterion is the following: assume w.l.o.g. an indexed coinductive type T : forall i : I, Type. A pattern-matching with return clause P : forall i : I, T i -> Type is valid iff it satisfies the following definitional equation:
i : I, x : T i ⊢ P i x ≡ P i (cofix F := x).
Now, to see why this prevents the SR failure, one has to peek into the semantics of (co)fixpoints. In Coq, you cannot unfold arbitrarily (co-)fixpoints, otherwise this leads to non-decidability of typechecking. There is thus a syntactic guard for (co-)fixpoint unfolding, namely:
- for inductive fixpoints, they only unfold when applied to something that starts with a constructor, e.g.
(fix F := t) (S n) ≡ t{F := (fix F := t)} (S n)
- for co-inductive cofixpoints, they only unfold when they are inside a pattern-matching, e.g.
match (cofix F := t) with p ≡ match t{F := (cofix F := t)} with p
The latter corresponds intuitively to the fact that the cofix is being forced.
Now, assume some dependent pattern-matching over a term of a coinductive type T. In general, this pattern-matching is of the shape match t as x return P x with p. Its type is thus P t. But now, assume that t ≡ (cofix F := t₀), in which case the unfolding rule mandates that expression is convertible to match t₀{F := (cofix F := t₀)} as x return P x with p, which now has type P (t₀{F := (cofix F := t₀)}).
Therefore, for SR to hold it is a necessary condition to have P (cofix F := t₀) ≡ P (t₀{F := (cofix F := t₀)}).
Because t₀ is arbitrary, this could very well be a variable as well. The criterion is based on this observation. While I have no mechanized proof of this, I convinced myself that this is actually a sufficient condition for SR to hold in general.
Consequences
If this PR gets merged into Coq, it will restore SR at the cost of making dependent elimination on positive coinductive types quite weird. This is expected, since one must not be able to prove the eta-expansion theorem in CIC. It is safe to add it as an axiom, still, just as function extensionality can be posited.
I am not sure it will be that practical because it also means that many proofs, e.g., the ones using destruct over coinductive terms without care for the convertibility criterion, will need to be ported at some point. The PR provide a flag to allow local breakage of SR, but eventually this flag will be removed. Also, this side-condition makes the elimination rule of coinductive types non-modular, because one cannot abstract over an arbitrary return predicate, since it would not satisfy the criterion.
Thus, I still believe that in the long run it is more natural to switch to negative coinductive types, even if we restored SR.
