KindOf is a crazy, crazy type.

KindOf.md

I've discovered something how to do something that GHC never intended you to be able to do, and I'm wondering if there's a way to abuse this to do interesting things.

It's known that you can express visible, dependent quantification at the kind level:

data A a :: a -> Type

λ> :kind A
A :: forall a -> a -> Type

However, you can't express visible, dependent quantification at the type level... or so I thought. There's this interesting type that you can write which is often called KindOf:

type family KindOf (a :: k) :: Type where
  KindOf (a :: k) = k

Here's an interesting question: what is KindOf A? Normally, this is a thought that GHC won't let you think:

λ> :kind KindOf A

<interactive>:1:8: error:
    • Expected kind ‘k0’, but ‘A’ has kind ‘forall a -> a -> Type’
    • In the first argument of ‘KindOf’, namely ‘A’
      In the type ‘KindOf A’

However, this is only a small hurdle. It turns out that we can lift this restriction by enabling the ImpredicativeTypes extension!

λ> :set -XImpredicativeTypes
λ> :kind! KindOf A
KindOf A :: Type
= forall a -> a -> Type

One consequence of this is that we can use KindOf A at the type level. That is to say, we can have visible, dependent quantification at the type level, despite my earlier claim to the contrary!

f :: KindOf A
f = undefined

λ> :type +v f
f :: forall a -> a -> Type
λ> :type f
f :: forall a -> a -> Type

This is pretty interesting, since GHC certainly never intended for this to be possible (at least, not at the moment). The question is: can we abuse this feature to make GHC do crazy things?

So far, I haven't been able to come up with anything terribly interesting. Here are the two things of (minor) note that I've discovered so far:

1. Let's say you define two functions on top of f like so:

   f :: KindOf A
   f = undefined
   
   g = f
   
   h = g

   What are the types of g and h? To my surprise, they're actually different:

   $ ghci Bug.hs -fprint-explicit-foralls -XNoStarIsType
   GHCi, version 8.6.1: http://www.haskell.org/ghc/  :? for help
   Loaded GHCi configuration from /home/rgscott/.ghci
   [1 of 1] Compiling Main             ( Bug.hs, interpreted )
   
   Bug.hs:24:1: warning: [-Wmissing-signatures]
       Top-level binding with no type signature:
         g :: forall a -> a -> Type
      |
   24 | g = f
      | ^
   
   Bug.hs:26:1: warning: [-Wmissing-signatures]
       Top-level binding with no type signature:
         h :: forall {a}. a -> Type
      |
   26 | h = g
      | ^
   

   Kind of weird.

2. Are there any other implementations of f? Unfortunately, it appears that the answer is "no". Here's another thing that I half-heartedly expected to typecheck:

   f :: KindOf A
   f _ = undefined

   Alas, GHC doesn't play along with me:

       • Couldn't match type ‘p0 -> a0’ with ‘forall a -> a -> Type’
         Expected type: KindOf A
           Actual type: p0 -> a0
       • The equation(s) for ‘f’ have one argument,
         but its type ‘KindOf A’ has none
      |
   22 | f _ = undefined
      | ^^^^^^^^^^^^^^^
   

   However, this isn't the full story. It turns out that the way that KindOf is defined is important here. In the example above, I was using a KindOf type family (whose definition I showed earlier). On the other hand, if you define KindOf as a type synonym:

   type KindOf (a :: k) = k

   Then you actually can implement f _ = undefined! What's more, its type seems to change in a subtle way... at least, according to GHCi:

   λ> :type +v f
   f :: KindOf A
   λ> :type f
   f :: forall {a}. a -> Type
   

   Also, the type of g apparently changes:

   $ ghci Bug.hs -fprint-explicit-foralls -XNoStarIsType
   GHCi, version 8.6.1: http://www.haskell.org/ghc/  :? for help
   Loaded GHCi configuration from /home/rgscott/.ghci
   [1 of 1] Compiling Main             ( Bug.hs, interpreted )
   
   Bug.hs:26:1: warning: [-Wmissing-signatures]
       Top-level binding with no type signature:
         g :: forall {a}. a -> Type
      |
   26 | g = f
      | ^
   
   Bug.hs:28:1: warning: [-Wmissing-signatures]
       Top-level binding with no type signature:
         h :: forall {a}. a -> Type
      |
   28 | h = g
      | ^
   

   Odd stuff.

Despite my best efforts, these are the only interesting things that I'm able to do with this trick. I feel like I've only scratched the surface here, though, and perhaps more creative minds can put this idea to better use.