| 49 | |

| 50 | === In kinds === |

| 51 | |

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

| 53 | |

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

| 55 | |

| 56 | ==== Type classes ==== |

| 57 | |

| 58 | Rules: |

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

| 60 | * Any explicit kind variables are generalized over |

| 61 | * Defaulting for flexi meta kind variables |

| 62 | |

| 63 | {{{ |

| 64 | class C1 (f :: k1 -> *) (g :: k2 -> k1) where -- forall k1 k2. (k1 -> *) -> (k2 -> k1) -> Constraint |

| 65 | foo :: f (g a) -> f b -- forall (a :: k2) (b :: k1). f (g a) -> f b |

| 66 | |

| 67 | -- C2 looks much easier with defaulting |

| 68 | class C2 f g where -- (* -> *) -> (* -> *) -> Constraint |

| 69 | foo :: f (g a) -> f b -- forall (a :: *) (b :: *). f (g a) -> f b |

| 70 | |

| 71 | class C3 (f :: k1 -> *) g where -- forall k1. (k1 -> *) -> (* -> k1) -> Constraint |

| 72 | foo :: f (g a) -> f b -- forall (a :: k1) (b :: *) -> f (g a) -> f b |

| 73 | }}} |

| 74 | |

| 75 | ==== Data types ==== |

| 76 | |

| 77 | Rules: |

| 78 | * No large scoping |

| 79 | * Any explicit kind variables are generalized over |

| 80 | * Defaulting for flexi meta kind variables |

| 81 | |

| 82 | {{{ |

| 83 | data T1 s as where -- (* -> *) -> [*] -> * |

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

| 85 | |

| 86 | data T1 s (as :: [k]) where -- forall k. (k -> *) -> [k] -> * |

| 87 | 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' |

| 88 | }}} |

| 89 | |