Improve "unification involving polytypes" message

As pointed out [here](https://gitlab.haskell.org/ghc/ghc/-/issues/18748#note_302270), attempting to unify a metavariable with a polytype can lead to rather confusing error messages, which often mention type variables which are nowhere to be seen in the user's program:

```haskell
{-# LANGUAGE RankNTypes, DataKinds #-}

import Data.Kind

type D :: forall (a :: Bool) -> Type
data D a = MkD

type E = D
```

```
* Expected kind `k0', but `D' has kind `forall (a :: Bool) -> *'
Cannot instantiate unification variable `k0'
with a kind involving polytypes: forall (a :: Bool) -> *
```

It would be nice to augment the error message with some more helpful information, perhaps asking the user to add more arguments, as the following is OK:

```haskell
type E a = D a
```

Maybe @goldfirere has some suggestion about possible improvements?

Start by reproducing the Haskell example in the issue and read the linked GHC discussion for the context behind the current diagnostic. Trace where unification of a metavariable with a polytype produces the message, then compare it with the accepted `type E a = D a` form. Done means the diagnostic gives more useful guidance and the example is covered by a regression test.

Written by the indexing model from the issue text.