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.

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.