In §3 of Polytypic values possess polykinded types, Ralf Hinze described a calculus of types with higher-kinded recursive types. There is a fixed-point combinator $$\mu_\kappa : (\kappa \rightarrow \kappa) \rightarrow \kappa$$ for every kind $\kappa$. Furthermore, there is a convertibility rule $(\mu)$, which says recursive types and their expansions are interconvertible: $$\mu_\kappa t \leftrightarrow t\;(\mu_\kappa t)\qquad\qquad(\mu)$$ Together with the congruence convertibility rules, $(\mu)$ means that recursive types and their expansions are interchangeable in all contexts. In other words, the system has equirecursive types.
My question is: Can one decide whether two types in Hinze's system are interconvertible?
The question is related to the equality of Böhm trees; it seems two types are interconvertible iff their Böhm trees are equal. Gérard Huet* showed the decidability of equality between regular Böhm trees, i. e., those with a finite number of distinct subtrees. However, types in Hinze's system can have nonregular Böhm trees; the following type is an example (it is related to the Sequ datatype in Hinze's paper):
$$\lambda g.~\mu f.~\lambda a.~g~a~(f~(g~a~a))$$
Is anything known about the decidability of equality between nonregular Böhm trees?
- Huet, Gérard. "Regular böhm trees." Mathematical Structures in Computer Science 8.06 (1998): 671-680.
