While the Generic representation of a data type expresses strictness of constructors/selectors in its Meta data, it appears that the constructors of the representation itself are always lazy, e.g. the two constructors of (:+:).
That means that the representation potentially contains more elements than the original type, so that (from,to) is an embedding-projection pair rather than an isomorphism. Is that on purpose? Or just the price we pay for not having four variants each of (:+:) and (:*:)?
Consider
module Natural where
import GHC.Generics
data Natural = Zero | Succ !Natural deriving (Show,Generic)
bottom :: Natural
bottom = Succ bottom
s :: Natural -> Rep Natural ()
s = M1 . R1 . M1 . M1 . K1 -- R1 is lazy, M1 and K1 are strict
leq :: Natural -> Rep Natural () -> Bool
leq n p = case (n, p) of
(Zero, _) -> True
(Succ _, M1 (L1 _)) -> False
(Succ n',M1 (R1 (M1 (M1 (K1 p'))))) -> leq n' (from p')
We can observe that
(Succ Zero) `leq` (s bottom) == True
but
(Succ Zero) `leq` (from bottom)
diverges. Hence s bottom is an element of Rep Natural () that is not in the image of from.