DataKinds and GADTs question?

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

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
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
participants (2)
-
coot@coot.me
-
Velichko Lefterov