How do I derive the free theorem for the type:
data F a = C1 Nat | C2 Bool Nat a
where Nat is simply data Nat = Z | S Nat?
In principle, this can be answered by the Haskell 'free-theorems' package, but it's too elderly to compile under any GHC version I can reasonably install.
There is an online generator for free theorems at, and when it was down a little while ago I created an alternative UI that runs completely in the browser (using reflex-dom).
But the deeper problem is that free theorems, in the sense of these packages, are properties of polymorphic functions, so in order to answer your question, you have to give a function (like map) whose free theorem you are interested in.