# With equirecursive types are there downsides to making all types potentially recursive?

By this I mean to ask, is it a bad idea to have all type constructor term expressions abstracted with $\mu$ just in case they need to be recursive? For example,

$Bool : Type;$

$Bool = (\mu Bool' . (Unit \lor Unit));$

The value constructors would still just be $(inj_0 unit)$ and $(inj_1 unit)$ in a system with equirecursive types, right? It seems like it would just be $O(x + 1)$ for an $O(x)$ type checking algorithm using unification, or maybe not even that.

I understand why $Bool$ is not written this way by default, especially considering recursive types are usually added to a theory after-the-fact and therefore the value constructors would differ depending on the variant of the recursive type theory. It's much less intuitive to read $(\mu X . \tau)$ than just $\tau$ when programming or proving theorems but are there any reasons of real consequence for not doing this? I can't find any.

The reason I ask this question is because I am writing a program to translate a functional programming language into a core dependent type theory with equirecursive types.

My advice would be to make sure that your translation function is compositional and straightforward, i.e., for a typical construct $A * B$ the translation function $t$ should have the form $t(A * B) = s(t(A), t(B))$, where $s$ is the translation of $*$. Thus the translation should follow the syntax of the input language. If you want to perform any "optimizations", those should come as convinient tactics that get used after the translation phase. This will make it easier to pove that your translation works correctly.
Concretely, if your input language has a construct for defining recursive types, such as data in Haskell, then you should translate those to $\mu \cdots$ even if they are not actually using the recursion, because that is what they are. You can always have a simple lemma afterwards which shows that $\mu$ can be omitted in certain cases. If you set up your tactics the right way, the theorem prover will simplify things by itself (and do much more if needed). But you should not put $\mu$ in front of a definition that cannot be recursive, such as newtype. In other languages, for example in Ocaml, the only way to introduce a new type is with type, which may be recursive, so there you'd put $\mu$ in front of everything.