Summary

When kind checking associated type declarations in an instance declaration, the instance context seems to be ignored.

Steps to reproduce

Minimal complete example:

{-# LANGUAGE DataKinds, PolyKinds, TypeFamilies, FlexibleContexts, FlexibleInstances, MultiParamTypeClasses, TypeApplications #-}
class C (k :: *) (a :: *) where
  type F k a :: k

data D k (x :: k)

instance C k (D k x) where
  type F k (D k x) = x -- good

instance (k ~ l) => C l (D k x) where
  type F l (D k x) = x -- bad
{-
b.hs:11:22: error:
    • Expected kind ‘l’, but ‘x’ has kind ‘k’
    • In the type ‘x’
      In the type instance declaration for ‘F’
      In the instance declaration for ‘C l (D k x)’
   |
11 |   type F l (D k x) = x -- bad
   |                      ^
-}

Expected behavior

The second instance should kind-check (it has better instance resolution properties than the first which is why we want it).

Environment

Tested on GHC 8.6.5 and GHC HEAD