Kind equalities ignored with dependent GADTs
Summary
Consider the following:
{-# LANGUAGE GADTs #-}
{-# LANGUAGE NoStarIsType #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE StandaloneKindSignatures #-}
import Data.Kind (Type)
type Weird :: forall k -> k -> Type
data Weird k (a :: k) where
Weird :: a -> Weird Type a
This compiles, but fails if standalone kind signature is removed:
weird.hs:11:28: error:
• Expected kind ‘k’, but ‘a’ has kind ‘Type’
• In the second argument of ‘Weird’, namely ‘a’
In the type ‘Weird Type a’
In the definition of data constructor ‘Weird’
|
11 | Weird :: a -> Weird Type a
Also,
fromWeird_Ok :: forall a. Weird Type a -> a
fromWeird_Ok (Weird a) = a
compiles, but
fromWeird_Error :: forall k (a :: k). k ~ Type => Weird k a -> a
fromWeird_Error (Weird a) = a
fails with
weird.hs:13:64: error:
• Expected a type, but ‘a’ has kind ‘k’
• In the type signature:
fromWeird_Error :: forall k (a :: k). k ~ Type => Weird k a -> a
|
13 | fromWeird_Error :: forall k (a :: k). k ~ Type => Weird k a -> a
I'm not sure what's going on here.
Environment
- GHC version used: 8.10.1