data M2 (a :: Type) :: String -> Type where
  Value2 :: a -> forall m . M2 a m

data M3 (a :: Type) :: String -> Type where
  Value3 :: a -> forall m . M2 a m