## Failure of bidirectional type inference at the kind level

I'm feeling particularly sadistic towards GHC at the moment, and so I fed it this:

```
import Data.Kind
data Proxy :: forall k. k -> Type where
MkProxy :: forall k (a :: k). Proxy a
data X where
MkX :: forall (k :: Type) (a :: k). Proxy a -> X
type Expr = (MkX :: forall (a :: Bool). Proxy a -> X)
type family Foo (x :: forall (a :: k). Proxy a -> X) where
Foo (MkX :: forall (a :: k). Proxy a -> X) = (MkProxy :: Proxy k)
```

Incredibly, GHC accepts it! And it even means what I wish it to, with GHCi telling me the following (with `-fprint-explicit-kinds`

):

```
λ> :i Foo
type family Foo k (x :: forall (a :: k). Proxy k a -> X)
:: Proxy * k
where [k] Foo k ('MkX k) = 'MkProxy * k
```

That is, I wished to extract the kind parameter to `MkK`

, matching against a partially-applied `MkX`

, and GHC understood that intention.

However, sadly, writing `Foo Expr`

produces

```
• Expected kind ‘forall (a :: k0). Proxy k0 a -> X’,
but ‘Expr a0’ has kind ‘Proxy Bool a0 -> X’
• In the first argument of ‘Foo’, namely ‘Expr’
In the type ‘Foo Expr’
In the type family declaration for ‘XXX’
```

For some reason, `Expr`

is getting instantiated when it shouldn't be.

Perhaps there's a simpler test case demonstrating the bug, but I feel so gleeful that this chicanery is accepted at all that I wanted to post.

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information