{-# LANGUAGE GADTs #-}
 
import Control.Arrow
import Data.Function
 
data Sized a where
  Unit ::                        Sized ()
  Int  ::                        Sized Int
  Char ::                        Sized Char
  Sum  :: Sized a -> Sized b  -> Sized (Either a b)
  Prod :: Sized a -> Sized b  -> Sized (a, b)
  Iso  :: Sized a -> (b -> a) -> Sized b
 
size :: Sized a -> a -> Int
size  Unit      = const 0
size  Int       = const 1
size  Char      = const 1
size (Sum  f g) = size f ||| size g
size (Prod f g) = size f *** size g >>> uncurry (+)
size (Iso  f g) = size f . g
 
conv []     = Left  ()
conv (x:xs) = Right (x, xs)
 
list x = fix $ \y -> Iso (Sum Unit $ Prod x y) conv
 
main = print $ list Int `size` [1..5]

ey0jIExBTkdVQUdFIEdBRFRzICMtfQoKaW1wb3J0IENvbnRyb2wuQXJyb3cKaW1wb3J0IERhdGEuRnVuY3Rpb24KCmRhdGEgU2l6ZWQgYSB3aGVyZQogIFVuaXQgOjogICAgICAgICAgICAgICAgICAgICAgICBTaXplZCAoKQogIEludCAgOjogICAgICAgICAgICAgICAgICAgICAgICBTaXplZCBJbnQKICBDaGFyIDo6ICAgICAgICAgICAgICAgICAgICAgICAgU2l6ZWQgQ2hhcgogIFN1bSAgOjogU2l6ZWQgYSAtPiBTaXplZCBiICAtPiBTaXplZCAoRWl0aGVyIGEgYikKICBQcm9kIDo6IFNpemVkIGEgLT4gU2l6ZWQgYiAgLT4gU2l6ZWQgKGEsIGIpCiAgSXNvICA6OiBTaXplZCBhIC0+IChiIC0+IGEpIC0+IFNpemVkIGIKCnNpemUgOjogU2l6ZWQgYSAtPiBhIC0+IEludApzaXplICBVbml0ICAgICAgPSBjb25zdCAwCnNpemUgIEludCAgICAgICA9IGNvbnN0IDEKc2l6ZSAgQ2hhciAgICAgID0gY29uc3QgMQpzaXplIChTdW0gIGYgZykgPSBzaXplIGYgfHx8IHNpemUgZwpzaXplIChQcm9kIGYgZykgPSBzaXplIGYgKioqIHNpemUgZyA+Pj4gdW5jdXJyeSAoKykKc2l6ZSAoSXNvICBmIGcpID0gc2l6ZSBmIC4gZwoKY29udiBbXSAgICAgPSBMZWZ0ICAoKQpjb252ICh4OnhzKSA9IFJpZ2h0ICh4LCB4cykKCmxpc3QgeCA9IGZpeCAkIFx5IC0+IElzbyAoU3VtIFVuaXQgJCBQcm9kIHggeSkgY29udgoKbWFpbiA9IHByaW50ICQgbGlzdCBJbnQgYHNpemVgIFsxLi41XQ==