There isn't. GHC will infer kind `Type -> Type` for `MyType2`.  You can check that in `ghci` with `:kind MyType` and `:kind MyType2`.  There's also third way to write it by adding a standalone kind signature: ``` {-# LANGUAGE StandalondKindSignatures, GADTs #-} type MyType3 :: Type -> Type data MyType3 a where   MkT3 :: Int -> MyType3 Int ``` A polykinded version would look like this: ``` {-# LANGUAGE PolyKinds #-} type MyType4 :: forall a -> Type data MyType4 a where   MkT3 :: MyType4 Int ``` in `ghci` the kind of `MyType4` is: ``` :kind MyType4 MyType4 :: forall k. forall (a :: k) -> Type ``` Best regards, Marcin Sent with ProtonMail Secure Email. ‐‐‐‐‐‐‐ Original Message ‐‐‐‐‐‐‐ On Thursday, June 10th, 2021 at 13:15, Velichko Lefterov <velichko.lefterov@gmail.com> wrote:

I tried to understand DataKinds and GADTs...Is there a difference between:

data MyType :: Type -> Type where

  MyTypeConstructor :: Int -> MyType Int

data MyType2 a where

  MyTypeConstructor2 :: Int -> MyType2 Int