{-| Support for subkinds of kind @*@, including subkind polymorphism. Imagine, we had a language extension for declaring subkinds of kind @*@ where a subkind declaration would be written as follows: @ subkind /K/ = /C_1/ => /t_1/ | ... | /C_n/ => /t_n/ @ Thereby, @/K/@ would be a kind identifier, the @/t_i/@ would be types and the @/C_i/@ would be contexts. This subkind declaration would introduce a subkind @/K/@ that covers all types that match one of the @/t_i/@ and fulfill the corresponding context. For example, the declaration @ subkind Map = (Ord key) => Map key val | IntMap val @ would declare the subkind @Map@ of all types whose values are maps. Note that the subkind @Map@ would be different from the type @Map@. We will now see how a subkind declaration @ subkind /K/ = /C_1/ => /t_1/ | ... | /C_n/ => /t_n/ @ can be emulated using this module. First, we declare a type @Kind/K/@ with a nullary data constructor of the same name for representing the subkind. Then we add the following instance declaration: @ instance Kind Kind/K/ where   data All Kind/K/ item = All/K/ (forall /A_1/. /C_1/ => item /t_1/) ... (forall /A_n/. /C_n/ => item /t_n/)   closed item = All/K/ item ... item @ Thereby, each @/A_i/@ stands for a whitespace-separated sequence of the free variables of @/t_i/@. Finally, we add the following instance declaration for every @/i/@ between @1@ and @/n/@: @ instance /C_i/ => Inhabitant Kind/K/ /t_i/ where   specialize (All/K/ _ ... _ item _ ... _) = item @ Thereby, the number of wildcard patterns before and after @item@ is @/i/ - 1@ and @/n/ - /i/@, respectively. The above subkind declaration for @Map@ can be emulated with the following code: @ data KindMap = KindMap   instance Kind KindMap where   data All KindMap item = AllMap (forall key val. (Ord key) => item (Map key val)) (forall val. item (IntMap val))   closed item = AllMap item item   instance (Ord key) => Inhabitant KindMap (Map key val) where   specialize (AllMap item _) = item   instance Inhabitant KindMap (IntMap val) where   specialize (AllMap _ item) = item @ -} module Data.Kind ( -- * Subkinds in general Kind (type All, closed), Inhabitant (specialize), -- * Kind @*@ as a subkind of itself KindStar (KindStar) ) where -- * Subkinds in general -- |The class of subkind representations. class Kind kind where {-| Universal quantification over the types of the subkind. For a subkind representation @Kind/K/@ of a subkind @/K/@ and a type @/f/@ of kind @* -> *@, @All Kind/K/ /f/@ is isomorphic to @forall val :: /K/. /f/ val@. -} data All kind :: (* -> *) -> * {-| Conversion from a type that uses normal universal quantification into one that uses subkind-specific universal quantification. -} closed :: (forall inhabitant. (Inhabitant kind inhabitant) => item inhabitant) -> All kind item -- |Specifies what types are inhabitants of what subkinds. class (Kind kind) => Inhabitant kind inhabitant where {-| Conversion from a universally quantified type into a type that is fixed to a specific inhabitant. This method exists to ensure that one cannot extend the subkind. If one would try to add a new inhabitant, one would have to provide an implementation of @specialize@. -} specialize :: All kind item -> item inhabitant -- * Kind @*@ as a subkind of itself -- |Represents kind @*@ itself. data KindStar = KindStar instance Kind KindStar where data All KindStar item = AllStar (forall val. item val) closed item = AllStar item instance Inhabitant KindStar val where specialize (AllStar item) = item