Associated type consistency
The basic setup
Consider this, ignoring kind polymorphism for now
class C b where
type F a b c
instance C [x] where
type F p [x] q = blah
In the class decl, the second parameter of F is the same as the first parameter of C.
We'll call these the corresponding parameter positions of C and F. For each associated
type F
in a class C
, we can (based on the class declaration alone) make a list of
corresponding argument positions, such as:
 Arg 1 of C corresponds to Arg 2 of F
There may be any number of these pairs. (Although zero would suggest it is not really an associated type at all.)
Note that both C and F can have other, unrelated parameters.
The basic consistency property for associatedfamily instances is this
 In an instance decl, we want C and F to have the same arguments in their corresponding argument positions.
Kind polymorphism
Where kind polymorphism is involved, we think of ``argument position* as applying uniformly to both visible and invisible arguments. For example: *
class C (a :: k) where
type T k :: Type
Here C
has an invisible k
argument, thus:
class C @k (a :: k) where
type T k :: Type
So the first (invisible) argument position of C
corresponds to the first (visible) argument
position of T
.
Alpha conversion
Should we allow this?
instance C [x] where
type F p [y] q = blah
Here we have chosen a different name for the argument to F, but we could relax our criterion a bit, to say
 In an instance decl, we want C and F to have the same arguments in their corresponding argument positions,
modulo alphaconversion.
Two possible positions
There seem to be two possible approaches to kindchecking an instance declaration for an associated types. Here is a running example:
instance C [x] where
type F p [y] q = blah

(Simpler, but more kind annotations.) Kindcheck the
type instance
declaration entirely independently from the classinstance
declaration. Then check the family instance consistency condition. 
(More complex, but fewer annotations.) Include familyinstance consistency when kindchecking the
type instance
decl. This may or may not make a subsequent family instance consistency check redundant.
Note that if we adopt (B) we should do so consistently in other related situations. For example:

Trac #15895 (closed)
class Ríki ob where type Arr :: ob > ob > Type io :: forall (a :: ob). Arr a a instance Ríki Type where type Arr = (>)  type Arr @Type = (>) io :: Arr a a  Does this meean forall k (a::k). Arr @k a a io a = a  or forall (a::Type). Arr @Type a a

Trac #14111 (closed) comment:2
data family F (a :: k) data instance F (a :: Bool) where MkF :: F a
This is currently rejected but under (B) perhaps it should not be.
Examples
indexedtypes/should_compile/T10815
type family Any :: k
class C (a :: k) where  C :: forall k. k > Constraint
type F (b :: k)  F :: forall k. k > Type
 Corresponding positions: first arg position of Funct and Codomain
 (But the second argument position does not correspond.)
instance C 'True where
type F x = Int
Looked at in isolation, there is nothing to say that x :: Bool
. But arguably
we want to infer
class C @k (a :: k) where
type F @k (b :: k)
 Corresponding positions: first arg of C and F
instance C @Bool 'True where
type F @Bool (x :: Bool) = Int
It's a bit indirect: you can only tell that x::Bool
by looking at the
correspondingargument info from the class declaration. You can't tell
jsut from F
's kind.
indexedtypes/should_fail/T13972
class C (a :: k) where
type T k :: Type
instance C Left where
type T (a > Either a b) = Int
This should obviously be accepted. If we write out the invisible bits we have:
class C @k (a :: k) where
type T k :: Type
instance C @(p > Either p q) (Left @p @q) where
type T (a > Either a b) = Int
The instantiation of T
is the same as that for C
, in the first arg position of each.
polykinds/T9574
data KProxy (t :: Type) = KProxy  KProxy :: Type > Type
data Proxy p  Proxy :: forall k. k > Type
data NatTr (c :: o > Type)  NatTr :: forall o. (o > Type) > Type
class Funct f where  Funct :: forall k. k > Constraint
type Codomain f :: Type  Codomain :: forall k. k > Type
 Corresponding positions: first two arg positions of Funct and Codomain
instance Funct ('KProxy :: KProxy o) where
type Codomain 'KProxy = NatTr (Proxy :: o > Type)
One question is whether o
even scopes over the associated type.
To make this typecheck we need
instance Funct @(KProxy o) ('KProxy :: KProxy o) where
type Codomain @(KProxy o) 'KProxy = NatTr (Proxy :: o > Type)
indexedtypes/should_fail/T12041
class Category (p :: i > i > Type) where
 Category :: forall i. (i>i>Type) > Constraint
type Ob p :: i > Constraint  Ob :: forall i. (i>i>Type) > i > Constraint
data I a b  I :: forall k1 k2. k1 > k2 > Type
instance Category I where
type Ob I = (~) Int
 NB: (~) Int :: Type > Type
Perhaps we should reject with
T12041.hs:15:8: error:
Type indexes must match class instance head
Expected: Ob i (I i i)
Actual: Ob * (I * *)
In the type instance declaration for Ob
Or I suppose we could even say that the nested type instance influences
the kind at which Category
is intantiated in the instance.