Finding a "free theorem"

Question

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.

Answer 1

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.