wiki:GhcKinds/KindInference/AssociatedTypes

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 associated-family 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 alpha-conversion.


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
  1. (Simpler, but more kind annotations.) Kind-check the type instance declaration entirely independently from the class instance declaration. Then check the family instance consistency condition.
  1. (More complex, but fewer annotations.) Include family-instance consistency when kind-checking 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
    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 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

indexed-types/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 corresponding-argument info from the class declaration. You can't tell jsut from F's kind.

indexed-types/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)

indexed-types/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.

Last modified 9 months ago Last modified on Nov 19, 2018 11:33:03 PM