:k fails with higher-rank kind

goldfirere commented 9 years ago

{-# LANGUAGE PolyKinds, DataKinds, GADTs, TypeOperators,
             RankNTypes, MultiParamTypeClasses, ConstraintKinds #-}

module Typeable where

data (a :: k1) :~: (b :: k2) where
  Refl :: forall k (a :: k). a :~: a

class EqT (t1 :: k1 -> *) (t2 :: k2 -> *) where
  eqT :: t1 a -> t2 b -> Maybe (a :~: b)

type EqT' k1 k2 (t :: forall k. k -> *) = EqT (t :: k1 -> *) (t :: k2 -> *)

class EqT1 (t :: forall k. k -> *) where
  eqT1 :: t a -> t b -> Maybe (a :~: b)

and then

:k EqT1

yields

<interactive>:1:1:
    Expecting one more argument to ‘EqT1’
    Expected kind ‘k0’,
      but ‘EqT1’ has kind ‘(forall k. k -> *) -> Constraint’
    In a type in a GHCi command: EqT1

It should just work.

int-index commented 8 years ago

Works fine on GHC 8.0.0.20160330

*Typeable> :k EqT1
EqT1 :: (forall k. k -> Type) -> Constraint

goldfirere commented 8 years ago

Hooray! Thanks for checking this.

goldfirere / ghc

:k fails with higher-rank kind #49