data Something (n :: Nat) = Something

data Format (k :: *) (k' :: *) (k'' :: *)