Design of Kind Polymorphism

This is a simple proposal, that would allow us to do better later, but still allow us to go on step 3.

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 *
• When there is no explicit foralls, 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
• Defaulting for flexi meta kind variables

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
  foo :: f (g a) -> f b                        -- forall (a :: k2) (b :: k1). f (g a) -> f b

-- C2 looks much easier with defaulting
class C2 f g where                             -- (* -> *) -> (* -> *) -> Constraint
  foo :: f (g a) -> f b                        -- forall (a :: *) (b :: *). f (g a) -> f b

class C3 (f :: k1 -> *) g where                -- forall k1. (k1 -> *) -> (* -> k1) -> Constraint
  foo :: f (g a) -> f b                        -- forall (a :: k1) (b :: *) -> f (g a) -> f b

Data types

data T1 s as where                         -- (* -> *) -> [*] -> *
  Foo :: s a -> T1 s as -> T1 s (a ': as)  -- forall (s :: * -> *) (a :: *) (as :: [*]). the same

data T1 s (as :: [k]) where                -- forall k. (k -> *) -> [k] -> *
  Foo : s a -> T1 s as -> T1 s (a ': as)   -- forall k (s :: k -> *) (a :: k) (as :: [k]). the same where `T1' becomes `T1 k'

Type families

Last rule becomes: Any missing kind signature defaults to *

-- Note (nothing to do with kind polymorphism): 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 a. f (g a)                   -- = forall (a :: *). f (g a)

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

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

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