## Clarify error messages when there is a kind mismatch

Create a module with the following code:

```
{-# LANGUAGE PolyKinds, TypeFamilies #-}
module T9171 where
data Base
type family GetParam (p::k1) (t::k2) :: k3
type instance GetParam Base t = t
```

It loads into GHCi just fine. But when we run:

`ghci> :t undefined :: GetParam Base (GetParam Base Int)`

we get an error

```
<interactive>:1:14:
Couldn't match expected type ‘GetParam Base (GetParam Base Int)’
with actual type ‘GetParam Base (GetParam Base Int)’
NB: ‘GetParam’ is a type function, and may not be injective
The type variable ‘k0’ is ambiguous
In the ambiguity check for: GetParam Base (GetParam Base Int)
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
In an expression type signature: GetParam Base (GetParam Base Int)
In the expression: undefined :: GetParam Base (GetParam Base Int)
```

If we modify the module by either

- set
`k3`

to`k2`

,`k1`

, or any concrete kind

or

- set
`k2`

to any concrete kind

then the ghci snippet will type check just fine.

I assume that this is a mistake, and that the original code should work just fine. If there is some reason, however, why the program would be unsound, then the error message should be made a bit more informative. The claim is that the kind `k0`

is ambiguous, but it doesn't appear anywhere in my code! In my full program, it took me a long time to narrow down that this was the source of the problem.