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
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 associated-family instances is this
- In an instance decl, we want C and F to have the same arguments in their corresponding argument positions.
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
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
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,
Two possible positions
There seem to be two possible approaches to kind-checking 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.) Kind-check the
type instancedeclaration entirely independently from the class
instancedeclaration. Then check the family instance consistency condition.
(More complex, but fewer annotations.) Include family-instance consistency when kind-checking the
type instancedecl. 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.
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
corresponding-argument info from the class declaration. You can't tell
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.
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)
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.