An inliner might break NotAdd, but why would it need to preserve it? Presumably an inliner is meant to be a homomorphism, not an isomorphism - i.e., it only goes one way.
Also, FreeBool[A] (the example given) actually handles substitution quite well. The `flatMap` operation will properly flatten things out:
If you're not careful about how you encode a property, the type system will _require_ you to preserve that property throughout each step of the computation, regardless of what sort of morphism that computation is. (It's an endomorphism.) Now that may be simple and straightforward when dealing with structural recursion over a boolean language, but if you want to write an inliner for Haskell, for example, it's probably a better idea to drop invariants from types (but not from the computation, of course), run the algorithm, and reintroduce invariants to the types afterwards.
Again, that example's way overshooting the complexity needed to prove the point. Even a seemingly simple invariant like the red-black balancing property is one that is impractical to preserve in this fashion without a proof assistant. And even then its practicality is still dubious.
Also, FreeBool[A] (the example given) actually handles substitution quite well. The `flatMap` operation will properly flatten things out:
Yes, the compiler did help me get that right.