Kind-checking associated types
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