kind polymorphism

Design of Kind Polymorphism

Implicit foralls are added by the renamer. Kind generalization (adding more kind foralls) is done by the type checker.

In types

Rules:

When there is an explicit forall, we don't add any foralls, which means:
- no implicit foralls even for kind variables
- no kind generalization, which means defaulting flexi meta kind variables to *
A kind variable mentioned explicitly in a type must always be bound by an explicit forall, unlike type variables for which Haskell adds an implicit forall.
When there is no explicit forall, we add an implicit forall for not-in-scope type variables in the renamer, and we kind generalize in the type checker.
In the context of a function signature, an explicit forall binds its variables (type or kind) in the function equations (as it is currently the case for type variables).

-- For the following examples, no type or kind variables are in scope

f1 :: f a -> Int                       -- forall k (f :: k -> *) (a :: k). f a -> Int

f2 :: f (a :: k) -> Int                -- Not in scope: kind variable `k'

f3 :: forall a. f a -> Int             -- Not in scope: type variable `f'

f4 :: forall f a. f a -> Int           -- forall (f :: * -> *) (a :: *). f a -> Int

f5 :: forall f (a :: k). f a -> Int    -- Not in scope: kind variable `k'
                                       -- We are a little unsure about this. Mabye we
                                       -- should kind-generalise

f6 :: forall k f a. f a -> Int         -- Warning: Unused quantified type variable `k'
                                       -- forall k (f :: * -> *) (a :: *). f a -> Int

f7 :: forall k f (a :: k). f a -> Int          -- forall k (f :: k -> *) (a :: k). f a -> Int

f8 :: forall k. forall f (a :: k). f a -> Int  -- forall k (f :: k -> *) (a :: k). f a -> Int


g1 :: (f a -> Int) -> Int                      -- forall (f :: k -> *) (a :: k). (f a -> Int) -> Int

g2 :: (forall f a. f a -> Int) -> Int          -- forall k. (forall (f :: k -> *) (a :: k). f a -> Int) -> Int

g3 :: (forall a. f a -> Int) -> Int            -- forall k (f :: k -> *). (forall (a :: k). f a -> Int) -> Int
 
g4 :: forall f. (forall a. f a -> Int) -> Int  -- forall (f :: * -> *). (forall (a :: *). f a -> Int) -> Int
 
g5 :: (forall f (a :: k). f a -> Int) -> Int   -- Not in scope: kind variable `k'


h :: forall k f (a :: k). f a -> Int
h x = ...k...f a...  -- k, f, and a are in scope

In kinds

Rules:

Any explicit kind variables are generalized over
We kind generalize flexi meta kind variables when possible

We need a notion of large scoping, which means that a variable in the signature can bind in the where clause. Only type classes have large scoping.

Type classes

Additionnal rules:

Large scoping: any type or kind variables appearing on left or right side of a :: in the signature is brought into scope

class C1 (f :: k1 -> *) (g :: k2 -> k1) where  -- forall k1 k2. (k1 -> *) -> (k2 -> k1) -> Constraint
  foo1 :: f (g a) -> (f :: k1 -> *) b          -- forall (a :: k2) (b :: k1). f (g a) -> f b
          -- Note that k1 and k2 scope over the type signatures
          -- just as f and g do.

class C2 f g where                             -- Same as C1
  foo2 :: f (g a) -> f b                       -- Same as foo1

class C3 (f :: k1 -> *) g where                -- Same as C1
  foo3 :: f (g a) -> f b                       -- Same as foo1

Data types

data T1 s as where                          -- forall k. (k -> *) -> [k] -> *
  Foo1 :: s a -> T1 s as -> T1 s (a ': as)  -- forall k (s :: k -> *) (a :: k) (as :: [k]). 
                                            --   s a -> T1 k s as -> T1 k s ((':) k a as)
    -- Note that s,a do not scope over the declaration of Foo1

data T2 s (as :: [k]) where                 -- Same as T1
  Foo2 : s a -> T1 s as -> T1 s (a ': as)   -- Same as Foo1
    -- Note that s,as,k do not scope over the declaration of Foo2

data T3 s (as :: [*]) where                 -- (* -> *) -> [*] -> *
  Foo3 : s a -> T1 s as -> T1 s (a ': as)   -- forall (s :: * -> *) (a :: *) (as :: [*]).
                                            --   s a -> T1 s as -> T1 s ((':) * a as)
    -- Note that s,as do not scope over the declaration of Foo2

Type families

Last rule becomes: Any missing kind signature defaults to *

-- Note (nothing to do with kind polymorphism) that we might want to say that only the Bool is an index.
type family F1 (b :: Bool) (true :: k) (false :: k) :: k  -- F1 :: forall k. Bool -> k -> k -> k

type family F2 b true false                               -- F2 :: * -> * -> * -> *

type family F3 b (true :: k) false                        -- F3 :: forall k. * -> k -> * -> *

For type families it just doesn't make any sense to not write the whole kind signature, since there is no inference at all.

Type synonyms

type S1 f g                             -- forall k1 k2. (k1 -> *) -> (k2 -> k1) -> *
  = forall a. f (g a)                   -- = forall (a :: k2). f (g a)

type S2 (f :: k1 -> *) g                -- Same as S1
  = forall a. f (g a)                   -- Same as S1

type S3 (f :: k1 -> *) (g :: k2 -> k1)  -- Same as S1
  = forall a. f (g a)                   -- Same as S1

type S4 f (g :: * -> *)                 -- (* -> *) -> (* -> *) -> *
  = forall a. f (g a)                   -- = forall (a :: *). f (g a)