Skip to content

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
Edited by Andrzej Rybczak
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information