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'

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


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

The story is more complicated since we have several ways of talking about kinds: data types, type classes, type families, and type synonyms.

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

Type classes

Rules:

• Large scoping: any type or kind variables appearing on left or right side of a :: in the signature is brought into scope
• Any explicit kind variables are generalized over
• Defaulting for flexi meta kind variables

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

Rules:

• No large scoping
• Any explicit kind variables are generalized over
• Defaulting for flexi meta kind variables

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'