symantic/Language/Symantic/Typing/Type.hs

   1 {-# LANGUAGE ConstraintKinds #-}
   2 {-# LANGUAGE GADTs #-}
   3 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
   4 {-# LANGUAGE TypeInType #-}
   5 {-# LANGUAGE UndecidableInstances #-}
   6 {-# OPTIONS_GHC -fno-warn-orphans #-}
   7 module Language.Symantic.Typing.Type
   8  ( module Language.Symantic.Typing.Type
   9  , Any
  10  , Proxy(..)
  11  , (:~:)(..)
  12  ) where
  13
  14 import Data.Map.Strict (Map)
  15 import Data.Maybe (isJust)
  16 import Data.Proxy
  17 import Data.Semigroup ((<>))
  18 import Data.Set (Set)
  19 import Data.Text (Text)
  20 import Data.Type.Equality
  21 import GHC.Exts (Constraint)
  22 import GHC.Prim (Any)
  23 -- import Data.Typeable (Typeable, eqT)
  24 import qualified Data.Kind as K
  25 import qualified Data.List as List
  26 import qualified Data.Map.Strict as Map
  27 import qualified Data.Set as Set
  28 import qualified Data.Text as Text
  29
  30 import Language.Symantic.Typing.Kind
  31 import Language.Symantic.Typing.Constant
  32 import Language.Symantic.Parsing
  33
  34 -- * Type 'T', for both 'Type' and 'Term'
  35
  36 -- | /Type of terms/ and… /term/ to be able
  37 -- to have polymorphic terms (ie. handle quantified variables).
  38 --
  39 -- * @src@: /source/.
  40 -- * @cs@: /type constants/, fixed at compile time.
  41 -- * @h@: indexed Haskell type.
  42 -- * @k@: indexed Haskell kind of @h@.
  43 --
  44 -- * 'TyConst': /type constant/, selected amongst @cs@.
  45 --
  46 -- * 'TyApp': /type parameter application/.
  47 --
  48 -- * 'TyQuant': /type universal quantification/ (aka. /type abstraction/):
  49 --   used to introduce (and bind) a /type variable/.
  50 --
  51 --   Note that the type indexing is lost (though not kind @k@),
  52 --   because GHC cannot represent a quantified type in a type
  53 --   aka. impredicative polymorphism.
  54 --
  55 -- * 'TyVar': /type variable/:,
  56 --   used to represent a /bounded type variable/,
  57 --   when passing through a 'TyQuant'.
  58 --
  59 --   Note that only the kind @k@ is flexible,
  60 --   @h@ being set to 'Any' to loose the type indexing
  61 --   and enabling the return of a type equality when the 'Var's are the same.
  62 --
  63 --   Note also that there is no DeBruijn encoding done to link 'TyQuant's and 'TyVar's.
  64 --
  65 -- * 'Term': /term/, useful to embed a term
  66 --   requiring quantifications and qualifications.
  67 --
  68 -- See also: https://ghc.haskell.org/trac/ghc/wiki/Typeable
  69 -- Which currently concludes:
  70 -- "Why kind equalities, then? Given the fact that Richard's branch
  71 -- doesn't solve this problem, what is it good for?
  72 -- It still works wonders in the mono-kinded case,
  73 -- such as for decomposing ->.
  74 -- It's just that poly-kinded constructors are still a pain."
  75 data T (src::K.Type) (cs::[K.Type]) (h::k) where
  76         TyConst :: src -> TyConst src cs c
  77                        -> Type src cs c
  78         TyApp   :: src -> Type src cs f
  79                        -> Type src cs x
  80                        -> Type src cs (f x)
  81                        -- NOTE: @f x@ decomposition made possible
  82                        -- at the cost of requiring @TypeInType@.
  83         TyQuant :: src -> NameHint
  84                        -> Kind src kv
  85                        -> (forall (v::kv). T src cs v -> KT src cs k)
  86                        -> Type src cs (h::k)
  87         TyVar   :: src -> Kind src kv
  88                        -> Var
  89                        -> Type src cs (Any::kv)
  90         Term    :: TeSym h
  91                        -> Type src cs h
  92                        -> Term src cs h
  93         {-
  94         TeVar :: src -> Name
  95                      -> Type src cs (h::K.Type)
  96                      -> Type src cs (h::K.Type)
  97         TeQuant :: src -> NameHint
  98                        -> Type src cs arg
  99                        -> (Term src cs arg -> Term src cs res)
 100                        -> Term src cs res
 101         -}
 102         {-
 103         TyTeApp :: src -> Type src cs (a -> b)
 104                        -> Type src cs a
 105                        -> Type src cs b
 106         -}
 107
 108 -- ** Type 'Type'
 109 type Type = T
 110
 111 -- ** Type 'Term'
 112 type Term src cs h = T src cs (h::K.Type)
 113
 114 -- | Remove all top 'Term's.
 115 unTerm :: Type src cs (h::k) -> Type src cs (h::k)
 116 unTerm (Term _te x) = unTerm x
 117 unTerm t = t
 118
 119 -- | 'Type' constructor to be used with @TypeApplications@ and @NoMonomorphismRestriction@.
 120 ty :: forall c src cs. (Source src, Inj_TyConst cs c) => Type src cs c
 121 ty = TyConst sourceLess inj_TyConst
 122  -- NOTE: The forall brings @c@ first in the type variables,
 123  -- which is convenient to use @TypeApplications@.
 124
 125 (~>) :: Source src => Inj_TyConst cs (->)
 126  => Type src cs a -> Type src cs b -> Type src cs (a -> b)
 127 (~>) a b = (ty @(->) `tyApp` a) `tyApp` b
 128 infixr 5 ~>
 129
 130
 131 -- | Like 'ty', but for a known 'Source'.
 132 tySourced :: forall c src cs. (Source src, Inj_TyConst cs c) => src -> Type src cs c
 133 tySourced src = TyConst src inj_TyConst
 134
 135 -- | Like 'TyApp', but 'sourceLess'.
 136 tyApp :: Source src => Type src cs f -> Type src cs a -> Type src cs (f a)
 137 tyApp = TyApp sourceLess
 138 infixl 9 `tyApp`
 139
 140 -- | Like 'TyQuant', but 'sourceLess'.
 141 tyQuant
 142  :: Source src
 143  => NameHint
 144  -> Kind src kv
 145  -> (forall (v::kv). Type src cs v -> KT src cs k)
 146  -> KT src cs k
 147 tyQuant n kv f = KT $ TyQuant sourceLess n kv f
 148
 149 -- | Return the 'Kind' of the given 'Type'.
 150 kindTy :: Inj_Source (EType src cs) src => Type src cs (h::k) -> Kind src k
 151 kindTy t = kindTyOS t `source` EType t
 152
 153 -- | Like 'kindTy' but keep the old 'Source'.
 154 kindTyOS :: Type src cs (h::k) -> Kind src k
 155 kindTyOS = go
 156         where
 157         go :: forall cs src k h. Type src cs (h::k) -> Kind src k
 158         go = \case
 159          TyConst _src c -> kindTyConst c
 160          TyApp _src f _x ->
 161                 case kindTyOS f of
 162                  KiArrow _src_kf _kx kf -> kf
 163          TyQuant src _n k f -> unKT kindTyOS $ f (TyVar src k 0)
 164          TyVar  _src k _v   -> k
 165          Term _te x         -> kindTyOS x
 166
 167 instance -- TestEquality
 168  Inj_Source (EType src cs) src
 169  => TestEquality (Type src cs) where
 170         testEquality = eqTy
 171 instance Eq (Type src cs h) where
 172         _x == _y = True
 173
 174 -- | Return a proof when two 'Type's are equals.
 175 --
 176 -- NOTE: 'TyQuant's are not compared:
 177 -- they first have to be monomorphized.
 178 eqTy :: Type src cs (x::k) -> Type src cs (y::k) -> Maybe (x:~:y)
 179 eqTy = go
 180         where
 181         go :: Type src cs (x::k) -> Type src cs (y::k) -> Maybe (x:~:y)
 182         go (TyConst _sx x) (TyConst _sy y)
 183          | Just Refl <- testEquality x y
 184          = Just Refl
 185         go (TyApp _sx fx xx) (TyApp _sy fy xy)
 186          | Just Refl <- eqKi (kindTyOS fx) (kindTyOS fy)
 187          , Just Refl <- go fx fy
 188          , Just Refl <- go xx xy
 189          = Just Refl
 190         go TyQuant{} TyQuant{} = Nothing
 191         {-
 192         go v (TyQuant sx _nx kx x::Type src cs vx)
 193              (TyQuant sy _ny ky y::Type src cs vy)
 194          | Just Refl <- eqKi kx ky
 195          , Just Refl <- go (v - 1) (x $ TyVar sx kx v) (y $ TyVar sy ky v)
 196          = Just Refl
 197         -}
 198         go (TyVar _sx kx x) (TyVar _sy ky y)
 199          | Just Refl <- eqKi kx ky
 200          , True <- x == y
 201          = Just Refl
 202         -- NOTE: 'Term' are transparent to 'eqTy'.
 203         go (Term _tx x) (Term _ty y) | Just Refl <- go x y = Just Refl
 204         go (Term _tx x) y            | Just Refl <- go x y = Just Refl
 205         go x            (Term _ty y) | Just Refl <- go x y = Just Refl
 206         go _x _y = Nothing
 207
 208 -- | Return two proofs when two 'Type's are equals:
 209 -- one for the type and one for the kind.
 210 eqKiTy :: Type src cs (x::kx) -> Type src cs (y::ky) -> Maybe (x:~~:y)
 211 eqKiTy = go
 212         where
 213         go :: Type src cs (x::kx) -> Type src cs (y::ky) -> Maybe (x:~~:y)
 214         go (TyConst _sx x) (TyConst _sy y) = eqKiTyConst x y
 215         go (TyApp _sx fx xx) (TyApp _sy fy xy)
 216          | Just KRefl <- go fx fy
 217          , Just KRefl <- go xx xy
 218          = Just KRefl
 219         go TyQuant{} TyQuant{} = Nothing
 220         go (TyVar _sx kx _x) (TyVar _sy ky _y)
 221          | Just Refl <- eqKi kx ky
 222          = Just KRefl
 223         go (Term _tx x) (Term _ty y) = go x y
 224         go _x _y = Nothing
 225
 226 -- * Type '(#>)'
 227 -- | 'TyConst' to qualify a 'Type'.
 228 data (#>) (q::Constraint) (a::K.Type)
 229
 230 (#>)
 231  :: Source src
 232  => Inj_TyConst cs (#>)
 233  => Type src cs a -> Type src cs b -> Type src cs (a #> b)
 234 (#>) a b = (ty @(#>) `tyApp` a) `tyApp` b
 235 infixr 0 #>
 236  -- NOTE: should actually be (-1)
 237  -- to compose well with @infixr 0 (->)@
 238  -- but this is not allowed by GHC.
 239
 240 instance
 241  ( Show_TyConst cs
 242  , Proj_TyConst cs (->)
 243  , Proj_TyConst cs (#>)
 244  ) => Show (Type src cs h) where
 245         showsPrec = showTy
 246
 247 showTy :: forall cs src h.
 248  ( Show_TyConst cs
 249  , Proj_TyConst cs (->)
 250  , Proj_TyConst cs (#>)
 251  ) => Int -> Type src cs h -> ShowS
 252 showTy pr typ = go Nothing (freeTyVar typ) (Map.empty, namesTy typ) pr typ
 253         where
 254         go :: forall p x.
 255             Maybe (Type src cs p) -- parent Type, used to prettify
 256          -> Var                   -- variable counter (DeBruijn)
 257          -> ( Map Var Name        -- names of bound variables
 258             , Names               -- used names : bound variables', free variables' and constants'
 259             )
 260          -> Int                   -- precedence
 261          -> Type src cs x
 262          -> ShowS
 263         go _prev _v _vs p (TyConst _src c) = showsPrec p c
 264         -- TODO: special infix case for (->), could be abstracted to handle others.
 265         go _prev v vs p t@(TyApp _ (TyApp _ (TyConst _ f) a) b)
 266          | Just KRefl <- projKiTyConst @_ @(->) f =
 267                 showParen (p > 0) $
 268                 go (Just t) v vs 1 a .
 269                 showString " -> " .
 270                 go (Just t) v vs 0 b
 271         -- TODO: special infix case for (#>), could be abstracted to handle others.
 272         go _prev v vs p t@(TyApp _ (TyApp _ (TyConst _ f) a) b)
 273          | Just KRefl <- projKiTyConst @_ @(#>) f =
 274                 showParen (p > 0) $
 275                 go (Just t) v vs 0 a .
 276                 showString " => " .
 277                 go (Just t) v vs 0 b
 278         go _prev v vs p t@(TyApp _src f a) =
 279                 showParen (p > 10) $
 280                 go (Just t) v vs 11 f .
 281                 showString " " .
 282                 go (Just t) v vs 11 a
 283         go prev v (vs, ns) p t@(TyQuant src nv kv f) =
 284                 let var = TyVar src kv v in
 285                 let n   = freshifyName ns nv in
 286                 let vs' = Map.insert v n vs in
 287                 let ns' = Set.insert n ns in
 288                 case f var of
 289                  KT x ->
 290                         showParen (p > 10) $
 291                         (case prev of
 292                          Just TyQuant{} -> id
 293                          _ -> showString "forall") .
 294                         showString " " .
 295                         go (Just t) v (vs', ns') p var .
 296                         (case x of
 297                          TyQuant{} -> id
 298                          _ -> showString ". ") .
 299                         go (Just t) (v + 1) (vs', ns') 0 x
 300         go _prev _v (vs, _ns) _p (TyVar _src _kv tv) =
 301                 case Map.lookup tv vs of
 302                  Nothing -> showString "#" . showsPrec 0 tv
 303                  Just n  -> showString $ Text.unpack n
 304         go _prev v vs _p t@(Term _te x) = showBracket True $ go (Just t) v vs 0 x
 305
 306 showBracket :: Bool -> ShowS -> ShowS
 307 showBracket b p =  if b then showChar '{' . p . showChar '}' else p
 308
 309 -- ** Type 'TyCon'
 310 -- | Captures the proof of a 'Constraint'
 311 -- (and its dictionaries when it contains type classes):
 312 -- pattern matching on the 'TyCon' constructor
 313 -- brings the 'Constraint' into scope.
 314 data TyCon c where
 315         Dict :: c => TyCon c
 316
 317 -- ** Type 'TyFamName'
 318 type TyFamName = Text
 319
 320 -- ** Class 'Sym'
 321 class Sym (term::K.Type -> K.Type) where
 322         sym_lam :: (term a -> term b) -> term (a -> b)
 323         sym_app :: term (a -> b) -> (term a -> term b)
 324         sym_int :: Int -> term Int
 325         sym_id  :: term (a -> a)
 326         sym_uc  :: term (Char -> Char)
 327         -- sym_bind :: Monad m => term (m a) -> term (a -> m b) -> term (m b)
 328         -- sym_bind :: term (Monad m #> (m a -> (a -> m b) -> m b))
 329         sym_bind :: Monad m => term (m a -> (a -> m b) -> m b)
 330         sym_const :: term a -> term b -> term a
 331         -- sym_comp :: term (b -> c) -> term (a -> c) -> term (a -> b)
 332         sym_comp :: term ((b -> c) -> (a -> b) -> a -> c)
 333
 334 -- ** Type 'TeSym'
 335 data TeSym (h::K.Type) = TeSym (forall term. Sym term => term h)
 336
 337 instance Source src => Sourced (Type src cs h) where
 338         type Source_of (Type src cs h) = src
 339
 340         source_of (TyConst src _c)        = src
 341         source_of (TyApp   src _f _x)     = src
 342         source_of (TyQuant src _n _kv _f) = src
 343         source_of (TyVar   src _kv _v)    = src
 344         source_of (Term  _te x)           = source_of x
 345
 346         source_is (TyConst _src c)      src = TyConst src c
 347         source_is (TyApp   _src f x)    src = TyApp   src f x
 348         source_is (TyQuant _src n kv f) src = TyQuant src n kv f
 349         source_is (TyVar   _src kv v)   src = TyVar   src kv v
 350         source_is (Term  te x)          src = Term te $ source_is x src
 351
 352 -- ** Type 'Var'
 353 type Var = Int
 354
 355 -- | Return the smallest 'Var' not used in given 'Type'.
 356 freeTyVar :: Type src cs (h::k) -> Var
 357 freeTyVar = (+ 1) . maxTyVar (-1)
 358         where
 359         maxTyVar :: Var -> Type src cs h -> Var
 360         maxTyVar m TyConst{}             = m
 361         maxTyVar m (TyApp   _src f a)    = maxTyVar m f `max` maxTyVar m a
 362         maxTyVar m (TyQuant src _n kv f) = ofKT (maxTyVar m) $ f $ TyVar src kv (-1)
 363         maxTyVar m (TyVar   _src _kv v)  = max m $ if v < 0 then -1 else v + 1
 364         maxTyVar m (Term  _te x)         = maxTyVar m x
 365
 366 -- ** Type 'Name'
 367 type Name     = Text
 368 type NameHint = Name
 369 type Names    = Set Name
 370
 371 namesTy :: Show_TyConst cs => Type src cs h -> Names
 372 namesTy (TyConst _src c)      = Set.singleton $ Text.pack $ show_TyConst c
 373 namesTy (TyApp   _src f x)    = namesTy f `Set.union` namesTy x
 374 namesTy (TyQuant src _n kv f) = ofKT namesTy $ f $ TyVar src kv (-1)
 375 namesTy (TyVar   _src _kv v)  | v < 0     = Set.empty
 376                               | otherwise = Set.singleton $ "#" <> Text.pack (show v)
 377 namesTy (Term  _te x) = namesTy x
 378
 379 -- | Infinite list of unique 'Name's:
 380 -- @a, b, .., z, a1, b1 .., z1, a2, ..@
 381 poolNames :: [Name]
 382 poolNames =
 383         [ Text.singleton n     | n <- ['a'..'z'] ] <>
 384         [ Text.pack (n:show i) | n <- ['a'..'z']
 385                                , i <- [1 :: Int ..] ]
 386
 387 -- | Return given 'Name' renamed a bit to avoid
 388 -- conflicting with any given 'Names'.
 389 freshifyName :: Names -> Name -> Name
 390 freshifyName ns "" = freshName ns
 391 freshifyName ns n =
 392         let ints = [1..] :: [Int] in
 393         List.head
 394          [ fresh
 395          | suffix <- "" : (show <$> ints)
 396          , fresh <- [n <> Text.pack suffix]
 397          , fresh `Set.notMember` ns
 398          ]
 399
 400 freshName :: Names -> Name
 401 freshName ns = List.head $ poolNames List.\\ Set.toList ns
 402
 403 {-
 404 -- | Drop the type index.
 405 --
 406 -- Useful when the type index cannot represent the wanted type,
 407 -- like a polymorphic type.
 408 tyVoid :: Type src cs (a::k) -> Type src cs (Any::Void)
 409 tyVoid = unsafeCoerce
 410 kindVoid :: Kind src k -> Kind src Void
 411 kindVoid = unsafeCoerce
 412 reflVoid :: (x::Void) :~: (y::Void)
 413 reflVoid = unsafeCoerce Refl
 414 -}
 415
 416 -- * Type 'Con_Type'
 417 data Con_Type src cs
 418  =   Con_EqType  (EType src cs) (EType src cs)
 419  |   Con_TyApp   (EType src cs)
 420  |   Con_TyCon   (KT src cs Constraint)
 421  |   Con_TyFam   (At src TyFamName) [EType src cs]
 422 deriving instance
 423  ( Eq src
 424  , Inj_Source (EType src cs) src
 425  ) => Eq (Con_Type src cs)
 426 deriving instance
 427  ( Show src
 428  , Show_TyConst cs
 429  , Proj_TyConst cs (->)
 430  , Proj_TyConst cs (#>)
 431  ) => Show (Con_Type src cs)
 432
 433 if_TyApp
 434  :: ( Inj_Error (Con_Type src cs) err
 435     , Inj_Source (EType src cs) src )
 436  => Type src cs (fa::kfa)
 437  -> (forall ka f a. (fa :~: f a)
 438   -> Type src cs (f::ka -> kfa)
 439   -> Type src cs (a::ka)
 440   -> Either err ret)
 441  -> Either err ret
 442 if_TyApp typ k =
 443         case typ of
 444          TyApp _src a b -> k Refl (a `source` EType typ) (b `source` EType typ)
 445          _ -> Left $ inj_Error $ Con_TyApp (EType typ)
 446
 447 if_EqType
 448  :: Inj_Error (Con_Type src cs) err
 449  => Type src cs x
 450  -> Type src cs y
 451  -> ((x :~: y) -> Either err ret) -> Either err ret
 452 if_EqType x y k =
 453         case x `eqTy` y of
 454          Just Refl -> k Refl
 455          Nothing -> Left $ inj_Error $
 456                 Con_EqType (EType x) (EType y)
 457
 458 if_EqType1
 459  :: ( Inj_Error (Con_Type src cs) err
 460     , Inj_Error (Con_Kind src) err
 461     , Inj_Source (EType src cs) src
 462     )
 463  => Type src cs (f:: K.Type -> K.Type)
 464  -> Type src cs fa
 465  -> (forall a. (fa :~: f a)
 466   -> Type src cs a
 467   -> Either err ret)
 468  -> Either err ret
 469 if_EqType1 typ ty_fa k =
 470         if_TyApp ty_fa $ \Refl ty_f ty_a ->
 471         if_EqKind (kind @(K.Type -> K.Type))
 472                   (kindTy ty_f) $ \Refl ->
 473         if_EqType typ ty_f $ \Refl ->
 474         k Refl ty_a
 475
 476 if_EqType2
 477  :: ( Inj_Error (Con_Type src cs) err
 478     , Inj_Error (Con_Kind src) err
 479     , Inj_Source (EType src cs) src )
 480  => Type src cs (f:: K.Type -> K.Type -> K.Type)
 481  -> Type src cs fab
 482  -> (forall a b. (fab :~: f a b)
 483   -> Type src cs a
 484   -> Type src cs b
 485   -> Either err ret)
 486  -> Either err ret
 487 if_EqType2 typ ty_fab k =
 488         if_TyApp ty_fab $ \Refl ty_fa ty_b ->
 489         if_TyApp ty_fa  $ \Refl ty_f  ty_a ->
 490         if_EqKind (kind @(K.Type -> K.Type -> K.Type))
 491                   (kindTy ty_f) $ \Refl ->
 492         if_EqType typ ty_f $ \Refl ->
 493         k Refl ty_a ty_b
 494
 495 if_TyFun ::
 496  ( Inj_TyConst cs (->)
 497  , Inj_Source (EType src cs) src
 498  , Inj_Error (Con_Kind src) err
 499  , Inj_Error (Con_Type src cs) err
 500  ) => Type src cs fab
 501  -> (forall a b. (:~:) fab (a -> b)
 502     -> Type src cs a -> Type src cs b -> Either err ret)
 503  -> Either err ret
 504 if_TyFun = if_EqType2 (ty @(->))
 505
 506 -- * Type 'EType'
 507 -- | Existential for 'Type'.
 508 data EType src cs = forall h. EType (Type src cs h)
 509
 510 instance Inj_Source (EType src cs) src => Eq (EType src cs) where
 511         EType x == EType y = isJust $ eqKiTy x y
 512 instance
 513  ( Show_TyConst cs
 514  , Proj_TyConst cs (->)
 515  , Proj_TyConst cs (#>)
 516  ) => Show (EType src cs) where
 517         showsPrec p (EType t) = showsPrec p t
 518
 519 mapEType
 520  :: (forall k (h::k). Type src cs h -> Type src cs h)
 521  -> EType src cs
 522  -> EType src cs
 523 mapEType f (EType t) = EType (f t)
 524
 525 bindEType
 526  :: (forall k (h::k). Type src cs h -> EType src cs)
 527  -> EType src cs
 528  -> EType src cs
 529 bindEType f (EType t) = f t
 530
 531 -- * Type 'KT'
 532 -- | Existential for 'T' of a known 'Kind'.
 533 data KT src cs k = forall (h::k). KT (Type src cs h)
 534 type KType = KT
 535 type KTerm src cs = KT src cs K.Type
 536
 537 instance Eq (KT src cs ki) where
 538         KT x == KT y = isJust $ eqTy x y
 539 instance
 540  ( Show_TyConst cs
 541  , Proj_TyConst cs (->)
 542  , Proj_TyConst cs (#>)
 543  ) => Show (KT src cs ki) where
 544         showsPrec p (KT t) = showTy p t
 545 instance Inj_Source (EType src cs) src => Inj_Source (KT src cs k) src where
 546         inj_Source (KT t) = inj_Source $ EType t
 547
 548 unKT :: (forall (h::k). Type src cs h -> a k) -> KT src cs k -> a k
 549 unKT f (KT t) = f t
 550
 551 ofKT :: (forall (h::k). Type src cs h -> a) -> KT src cs k -> a
 552 ofKT f (KT t) = f t
 553
 554 mapKT
 555  :: (forall (h::k). Type src cs h -> Type src cs h)
 556  -> KT src cs k
 557  -> KT src cs k
 558 mapKT f (KT t) = KT (f t)
 559
 560 bindKT
 561  :: (forall (h::k). Type src cs h -> KT src cs k)
 562  -> KT src cs k
 563  -> KT src cs k
 564 bindKT f (KT t) = f t
 565
 566 bind2KT
 567  :: (forall (x::ka) (y::kb). Type src cs x -> Type src cs y -> KT src cs kxy)
 568  -> KT src cs ka
 569  -> KT src cs kb
 570  -> KT src cs kxy
 571 bind2KT f (KT x) (KT y) = f x y
 572
 573 -- * Type 'Types'
 574 data Types src cs (hs::[K.Type]) where
 575         TypesZ :: Types src cs '[]
 576         TypesS :: Type  src cs h
 577                -> Types src cs hs
 578                -> Types src cs (Proxy h ': hs)
 579 infixr 5 `TypesS`
 580
 581 showTys
 582  :: forall cs src hs.
 583     Show_TyConst cs
 584  => Proj_TyConst cs (->)
 585  => Proj_TyConst cs (#>)
 586  => Types src cs hs -> ShowS
 587 showTys ts = showString "[" . go ts . showString "]"
 588         where
 589         go :: forall xs. Types src cs xs -> ShowS
 590         go TypesZ = showString ""
 591         go (TypesS h0 (TypesS h1 hs)) = showTy 10 h0 . showString ", " . showTy 10 h1 . go hs
 592         go (TypesS h hs) = showTy 10 h . go hs
 593
 594 instance
 595  ( Show_TyConst cs
 596  , Proj_TyConst cs (->)
 597  , Proj_TyConst cs (#>)
 598  ) => Show (Types src cs hs) where
 599         showsPrec _p = showTys
 600
 601 eTypes :: Types src cs hs -> [EType src cs]
 602 eTypes TypesZ = []
 603 eTypes (TypesS t ts) = EType t : eTypes ts
 604
 605 {-
 606 -- * Type 'UnProxy'
 607 type family UnProxy (x::K.Type) :: k where
 608         UnProxy (Proxy x) = x
 609 -}