Instantly share code, notes, and snippets.

# RyanGlScott/KindOf.md Last active Mar 20, 2019

KindOf is a crazy, crazy type.

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
[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
[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.