I have updated description ("Order of inhabitants in infinite lists won't be tested."), hope it clarifies it. It was complementary task, so I think strictness is unnecessary.

I'm very confused by one of the tests: pred (successor x) == Just x

But pred = nat Nothing Just. How can this possibly be true for any x?

In addition, according to the approach, mentioned in that paper, you could implement set of all subsets in haskell as

powerset :: [a] -> [[a]]
powerset = filterM $ const [False, True]

Good question)
Yes, when count @t is infinity we could not conclude, that t is countable (in mathematical sense).

So ℵ₀ = count @Nat < count @[Nat] = 2^ℵ₀ in terms of cardinal numbers,
and type/set t is countable iff count @t == count @Nat.

We can not express such things in haskell, so when infinity, we just write all formally.

Also if count @x >= 2 then type Nat -> x is not countable.

Is Listable c => Listable [c] actually true? I have some sort of feeling that this implies that the reals are enumerable.

Consider http://faculty.washington.edu/keyt/reals.pdf. Briefly this says:

• An enumeration of the real numbers will give rise immediately to an enumeration of the set of all sets of natural numbers.
• But the set of all sets of natural numbers is not enumerable.
• Hence, the set of real numbers is not enumerable.

The second bullet is important. We show in the kata that the natural numbers are enumerable. So, if we have Listable c => Listable [c], then we violate the second bullet, don't we?

Yeh, same for me. First couple of submits timed out, then eventually came in just under 12s.

Anyone got any advice for optimisation in Haskell? I'm stuck timing out on the slow programs.