symantic/Language/Symantic/Typing/Type.hs

   1 {-# LANGUAGE ConstraintKinds #-}
   2 {-# LANGUAGE GADTs #-}
   3 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
   4 {-# LANGUAGE TypeInType #-}
   5 {-# LANGUAGE NoMonomorphismRestriction #-}
   6 {-# LANGUAGE UndecidableInstances #-}
   7 {-# OPTIONS_GHC -fno-warn-orphans #-}
   8 module Language.Symantic.Typing.Type
   9  ( module Language.Symantic.Typing.Type
  10  -- , Any
  11  , Proxy(..)
  12  , (:~:)(..)
  13  , (:~~:)(..)
  14  ) where
  15
  16 import Data.Maybe (isJust)
  17 import Data.Proxy
  18 import Data.Text (Text)
  19 import Data.Type.Equality
  20 import GHC.Exts (Constraint)
  21 import GHC.Prim (Any)
  22 import Data.String (IsString(..))
  23 -- import Data.Typeable (Typeable, eqT)
  24 import qualified Data.Kind as K
  25
  26 import Language.Symantic.Helper.Data.Type.Equality
  27 import Language.Symantic.Grammar
  28 import Language.Symantic.Typing.Kind
  29 import Language.Symantic.Typing.Constant
  30 import Language.Symantic.Parsing
  31 import Language.Symantic.Transforming
  32
  33 -- * Type 'T', for both 'Type' and 'Term'
  34
  35 -- | /Type of terms/, also embedding… /terms/ to be able
  36 -- to have /polymorphic terms/ (ie. handle /type variables/).
  37 --
  38 -- Parameters:
  39 --
  40 -- * @src@: /source/.
  41 -- * @cs@: /type constants/, fixed at compile time.
  42 -- * @h@: indexed Haskell type.
  43 -- * @k@: indexed Haskell kind of @h@.
  44 --
  45 -- Constructors:
  46 --
  47 -- * 'TyConst': /type constant/, selected amongst @cs@.
  48 --
  49 -- * 'TyApp': /type parameter application/.
  50 --
  51 -- * 'TyQuant': /universal type quantification/ (aka. /type abstraction/):
  52 --   used to introduce (and bind) a /type variable/.
  53 --
  54 --   Note that the type indexing is lost (though not the kind @k@),
  55 --   because GHC cannot represent a quantified type in a type
  56 --   aka. /impredicative polymorphism/.
  57 --
  58 -- * 'TyVar': /type variable/:,
  59 --   used to represent a /bounded type variable/,
  60 --   when passing through a 'TyQuant'.
  61 --
  62 --   Note that only the kind @k@ is flexible,
  63 --   @h@ being set to 'Any' to loose the type indexing
  64 --   and enabling the return of a type equality when the 'Var's are the same.
  65 --
  66 --   Note also that there is no DeBruijn encoding done to link 'TyQuant's and 'TyVar's.
  67 --
  68 -- * 'Term': /term/, useful to embed a term
  69 --   requiring quantifications and qualifications.
  70 --
  71 -- * 'TyFam': /type family/.
  72 --
  73 -- See also: https://ghc.haskell.org/trac/ghc/wiki/Typeable
  74 -- which currently concludes:
  75 -- "Why kind equalities, then? Given the fact that Richard's branch
  76 -- doesn't solve this problem, what is it good for?
  77 -- It still works wonders in the mono-kinded case,
  78 -- such as for decomposing ->.
  79 -- It's just that poly-kinded constructors are still a pain."
  80 data T (src::K.Type)
  81        (ctx::[K.Type])
  82        -- (ss::([K.Type],[K.Type],[K.Type]))
  83        (ss::[K.Type])
  84        (cs::[K.Type])
  85        (h::k) where
  86         TyConst :: src -> TyConst src cs c
  87                        -> Type src ctx ss cs c
  88         TyApp   :: src -> Type src ctx ss cs f
  89                        -> Type src ctx ss cs a
  90                        -> Type src ctx ss cs (f a)
  91                        -- NOTE: @f a@ decomposition made possible
  92                        -- at the cost of requiring @TypeInType@.
  93         TyQuant :: src -> NameHint
  94                        -> Kind src kv
  95                        -> (forall (v::kv). Type src ctx ss cs v -> KType src ctx ss cs k)
  96                        -> Type src ctx ss cs (h::k)
  97         TyVar   :: src -> Kind src kv
  98                        -> Var
  99                        -> Type src ctx ss cs (Any::kv)
 100         TyFam   :: src -> TyConst src cs fam
 101                        -> Types src ctx ss cs hs
 102                        -> Type src ctx ss cs (TyFam fam hs)
 103         Term    :: Type src ctx ss cs h
 104                 -> TeSym ctx ss h
 105                 -> Term src ctx ss cs h
 106
 107 -- ** Type 'Type'
 108 type Type = T
 109
 110 -- ** Type 'Name'
 111 type Name     = Text
 112 type NameHint = Name
 113
 114 -- ** Type 'Term'
 115 type Term src ctx ss cs h = T src ctx ss cs (h::K.Type)
 116
 117 -- | Remove all top 'Term's.
 118 --
 119 -- Useful before pattern-matching.
 120 unTerm :: Type src ctx ss cs (h::k) -> Type src ctx ss cs (h::k)
 121 unTerm (Term x _te) = unTerm x
 122 unTerm t = t
 123
 124 -- | Remove all 'Term's.
 125 --
 126 -- Useful before pattern-matching, or to reset the context.
 127 unTerms :: Type src ctx ss cs (h::k) -> Type src ctx' ss cs (h::k)
 128 unTerms (TyConst src c)      = TyConst src c
 129 unTerms (TyApp src f a)      = TyApp src (unTerms f) (unTerms a)
 130 unTerms (TyQuant src n kv f) = TyQuant src n kv $ \v -> case f (unTerms v) of KT t -> KT $ unTerms t
 131 unTerms (TyVar src kv v)     = TyVar src kv v
 132 unTerms (TyFam src f hs)     = TyFam src f (unTerms `mapTys` hs)
 133 unTerms (Term x _te)         = unTerms x
 134
 135 unCtxTe :: T src ctx ss cs h -> T src '[] ss cs h
 136 unCtxTe = unTerms
 137
 138 -- | Like 'TyConst', but 'sourceLess'.
 139 --
 140 -- NOTE: to be used with @TypeApplications@ and @NoMonomorphismRestriction@.
 141 ty :: forall c ss cs src ctx.
 142       Source src
 143    => Inj_TyConst cs c
 144    => Type src ctx ss cs c
 145 ty = TyConst sourceLess inj_TyConst
 146  -- NOTE: The forall brings @c@ first in the type variables,
 147  -- which is convenient to use @TypeApplications@.
 148
 149 -- | Like 'ty', but for a known 'Source'.
 150 tySourced
 151  :: forall c ss cs src ctx.
 152     Source src
 153  => Inj_TyConst cs c
 154  => src
 155  -> Type src ctx ss cs c
 156 tySourced src = TyConst src inj_TyConst
 157
 158 -- | Like 'TyApp', but 'sourceLess'.
 159 tyApp :: Source src
 160       => Type src ctx ss cs f
 161       -> Type src ctx ss cs a
 162       -> Type src ctx ss cs (f a)
 163 tyApp = TyApp sourceLess
 164 infixl 9 `tyApp`
 165
 166 -- | Like 'TyQuant', but 'sourceLess'.
 167 tyQuant
 168  :: forall src ctx ss cs kv k.
 169     Source src
 170  => Inj_Kind kv
 171  => NameHint
 172  -> (forall (v::kv). Type src ctx ss cs v -> KT src ctx ss cs k)
 173  -> KT src ctx ss cs k
 174 tyQuant n f = KT $ TyQuant sourceLess n inj_Kind f
 175
 176 -- | Return the 'Kind' of the given 'Type'.
 177 kindTy
 178  :: Inj_Source (EType src '[] ss cs) src
 179  => Type src ctx ss cs (h::k)
 180  -> Kind src k
 181 kindTy t = kindTyOS t `source` EType (unCtxTe t)
 182
 183 -- | Like 'kindTy' but keep the old 'Source'.
 184 kindTyOS :: Type src ctx ss cs (h::k) -> Kind src k
 185 kindTyOS = go
 186         where
 187         go :: Type src ctx ss cs (h::k) -> Kind src k
 188         go = \case
 189          TyConst _src c -> kindTyConst c
 190          TyApp _src f _x ->
 191                 case kindTyOS f of
 192                  KiArrow _src_kf _kx kf -> kf
 193          TyQuant src _n k f -> kindTyOS `unKT` f (TyVar src k 0)
 194          TyVar  _src k _v   -> k
 195          TyFam _src f _hs   -> kindTyConst f
 196          Term x _te         -> kindTyOS x
 197
 198 instance -- TestEquality
 199  Inj_Source (EType src ctx ss cs) src
 200  => TestEquality (Type src ctx ss cs) where
 201         testEquality = eqTy
 202 instance Eq (Type src ctx ss cs h) where
 203         _x == _y = True
 204
 205 -- | Return a proof when two 'Type's are equals.
 206 --
 207 -- NOTE: 'TyQuant's are not compared:
 208 -- they first have to be monomorphized.
 209 eqTy :: Type src ctx ss cs (x::k) -> Type src ctx ss cs (y::k) -> Maybe (x:~:y)
 210 eqTy = go
 211         where
 212         go :: Type src ctx ss cs (x::k) -> Type src ctx ss cs (y::k) -> Maybe (x:~:y)
 213         go (TyConst _sx x) (TyConst _sy y)
 214          | Just Refl <- testEquality x y
 215          = Just Refl
 216         go (TyApp _sx fx xx) (TyApp _sy fy xy)
 217          | Just Refl <- eqKi (kindTyOS fx) (kindTyOS fy)
 218          , Just Refl <- go fx fy
 219          , Just Refl <- go xx xy
 220          = Just Refl
 221         go TyQuant{} TyQuant{} = Nothing
 222         {-
 223         go v (TyQuant sx _nx kx x::Type src ctx ss cs vx)
 224              (TyQuant sy _ny ky y::Type src ctx ss cs vy)
 225          | Just Refl <- eqKi kx ky
 226          , Just Refl <- go (v - 1) (x $ TyVar sx kx v) (y $ TyVar sy ky v)
 227          = Just Refl
 228         -}
 229         go (TyVar _sx kx x) (TyVar _sy ky y)
 230          | Just Refl <- eqKi kx ky
 231          , True <- x == y
 232          = Just Refl
 233         -- NOTE: 'Term' are transparent to 'eqTy'.
 234         go (Term x _tx) (Term y _ty) | Just Refl <- go x y = Just Refl
 235         go (Term x _tx) y            | Just Refl <- go x y = Just Refl
 236         go x            (Term y _ty) | Just Refl <- go x y = Just Refl
 237         go _x _y = Nothing
 238
 239 -- | Return two proofs when two 'Type's are equals:
 240 -- one for the type and one for the kind.
 241 eqKiTy :: Type src ctx ss cs (x::kx) -> Type src ctx ss cs (y::ky) -> Maybe (x:~~:y)
 242 eqKiTy = go
 243         where
 244         go :: Type src ctx ss cs (x::kx) -> Type src ctx ss cs (y::ky) -> Maybe (x:~~:y)
 245         go (TyConst _sx x) (TyConst _sy y) = eqKiTyConst x y
 246         go (TyApp _sx fx xx) (TyApp _sy fy xy)
 247          | Just KRefl <- go fx fy
 248          , Just KRefl <- go xx xy
 249          = Just KRefl
 250         go TyQuant{} TyQuant{} = Nothing
 251         go (TyVar _sx kx _x) (TyVar _sy ky _y)
 252          | Just Refl <- eqKi kx ky
 253          = Just KRefl
 254         go (Term x _tx) (Term y _ty) = go x y
 255         go _x _y = Nothing
 256
 257 -- * Type @(#>)@
 258 -- | 'TyConst' to qualify a 'Type'.
 259 data (#>) (q::Constraint) (a::K.Type)
 260 instance Fixity_TyConstC (#>) where
 261         fixity_TyConstC _ = FixityInfix $ infixR 0
 262
 263 (#>) :: Source src
 264      => Inj_TyConst cs (#>)
 265      => Type src ctx ss cs a
 266      -> Type src ctx ss cs b
 267      -> Type src ctx ss cs (a #> b)
 268 (#>) a b = (ty @(#>) `tyApp` a) `tyApp` b
 269 infixr 0 #>
 270  -- NOTE: should actually be (-1)
 271  -- to compose well with @infixr 0 (->)@
 272  -- but this is not allowed by GHC.
 273
 274 -- * Type family 'TyFam'
 275 -- | Apply the /type family/ selected by @fam@
 276 -- to a list of types (within a 'Proxy').
 277 type family TyFam (fam::k) (hs::[K.Type]) :: k
 278 type family TyFamKi fam :: K.Type
 279
 280 -- ** Type 'TyFamName'
 281 type TyFamName = Text
 282
 283 -- * Type 'TeSym'
 284 data TeSym ctx ss (h::K.Type)
 285  =   TeSym
 286  ( forall term. Syms ss term =>
 287                 Sym_Lambda term =>
 288                 CtxTe term ctx -> term h )
 289
 290 -- * Class 'Sym_Lambda'
 291 class Sym_Lambda term where
 292         -- | /Function application/.
 293         apply :: term ((a -> b) -> a -> b)
 294
 295         -- | /Lambda application/.
 296         app :: term (a -> b) -> (term a -> term b); infixr 0 `app`
 297         default app :: Trans t term => t term (arg -> res) -> t term arg -> t term res
 298         app f x = trans_lift (app (trans_apply f) (trans_apply x))
 299
 300         -- | /Lambda abstraction/.
 301         lam :: (term a -> term b) -> term (a -> b)
 302         default lam :: Trans t term => (t term arg -> t term res) -> t term (arg -> res)
 303         lam f = trans_lift (lam (trans_apply . f . trans_lift))
 304
 305         -- | Convenient 'lam' and 'app' wrapper.
 306         let_ :: term var -> (term var -> term res) -> term res
 307         let_ x y = lam y `app` x
 308
 309 -- * Type 'TeName'
 310 newtype TeName = TeName Text
 311  deriving (Eq, Ord, Show)
 312 instance IsString TeName where
 313         fromString = TeName . fromString
 314
 315 -- * Type 'CtxTe'
 316 -- | GADT for an /interpreting context/:
 317 -- accumulating at each /lambda abstraction/
 318 -- the @term@ of the introduced variable.
 319 data CtxTe (term::K.Type -> K.Type) (hs::[K.Type]) where
 320         CtxTeZ :: CtxTe term '[]
 321         CtxTeS :: term h
 322                -> CtxTe term hs
 323                -> CtxTe term (h ': hs)
 324 infixr 5 `CtxTeS`
 325
 326 -- ** Type family 'Sym'
 327 type family Sym (s::K.Type) :: {-term-}(K.Type -> K.Type) -> Constraint
 328
 329 -- ** Type family 'Syms'
 330 type family Syms (ss::[K.Type]) (term:: K.Type -> K.Type) :: Constraint where
 331         Syms '[] term = ()
 332         Syms (s ': ss) term = (Sym s term, Syms ss term)
 333
 334
 335 instance Source src => Sourced (Type src ctx ss cs h) where
 336         type Source_of (Type src ctx ss cs h) = src
 337
 338         source_of (TyConst src _c)        = src
 339         source_of (TyApp   src _f _x)     = src
 340         source_of (TyQuant src _n _kv _f) = src
 341         source_of (TyVar   src _kv _v)    = src
 342         source_of (TyFam   src _f _hs)    = src
 343         source_of (Term x _te)            = source_of x
 344
 345         source_is (TyConst _src c)      src = TyConst src c
 346         source_is (TyApp   _src f x)    src = TyApp   src f x
 347         source_is (TyQuant _src n kv f) src = TyQuant src n kv f
 348         source_is (TyVar   _src kv v)   src = TyVar   src kv v
 349         source_is (TyFam   _src f hs)   src = TyFam   src f hs
 350         source_is (Term x te)           src = Term (source_is x src) te
 351
 352 -- ** Type 'Var'
 353 type Var = Int
 354
 355 -- * Type 'Con_Type'
 356 data Con_Type src ctx ss cs
 357  =   Con_EqType  (EType src ctx ss cs) (EType src ctx ss cs)
 358  |   Con_TyApp   (EType src ctx ss cs)
 359  |   Con_TyCon   (KT src ctx ss cs Constraint)
 360  |   Con_TyFam   (At src TyFamName) [EType src ctx ss cs]
 361 deriving instance
 362  ( Eq src
 363  , Inj_Source (EType src ctx ss cs) src
 364  ) => Eq (Con_Type src ctx ss cs)
 365 deriving instance
 366  ( Show src
 367  , Show_TyConst cs
 368  , Show (EType src ctx ss cs)
 369  , Show (KT    src ctx ss cs Constraint)
 370  , Fixity_TyConst cs
 371  ) => Show (Con_Type src ctx ss cs)
 372
 373 if_TyApp
 374  :: ( Inj_Error (Con_Type src '[] ss cs) err
 375     , Inj_Source (EType src '[] ss cs) src )
 376  => Type src ctx ss cs (fa::kfa)
 377  -> (forall ka f a. (fa :~: f a)
 378   -> Type src ctx ss cs (f::ka -> kfa)
 379   -> Type src ctx ss cs (a::ka)
 380   -> Either err ret)
 381  -> Either err ret
 382 if_TyApp typ k =
 383         case typ of
 384          TyApp _src a b -> k Refl (a `source` EType (unCtxTe typ)) (b `source` EType (unCtxTe typ))
 385          _ -> Left $ inj_Error $ Con_TyApp (EType (unCtxTe typ))
 386
 387 if_EqType
 388  :: Inj_Error (Con_Type src '[] ss cs) err
 389  => Type src ctx ss cs x
 390  -> Type src ctx ss cs y
 391  -> ((x :~: y) -> Either err ret) -> Either err ret
 392 if_EqType x y k =
 393         case x `eqTy` y of
 394          Just Refl -> k Refl
 395          Nothing -> Left $ inj_Error $
 396                 Con_EqType (EType (unCtxTe x)) (EType (unCtxTe y))
 397
 398 if_EqType1
 399  :: ( Inj_Error (Con_Type src '[] ss cs) err
 400     , Inj_Error (Con_Kind src) err
 401     , Inj_Source (EType src '[] ss cs) src
 402     )
 403  => Type src ctx ss cs (f:: K.Type -> K.Type)
 404  -> Type src ctx ss cs fa
 405  -> (forall a. (fa :~: f a)
 406   -> Type src ctx ss cs a
 407   -> Either err ret)
 408  -> Either err ret
 409 if_EqType1 typ ty_fa k =
 410         if_TyApp ty_fa $ \Refl ty_f ty_a ->
 411         if_EqKind (inj_Kind @(K.Type -> K.Type))
 412                   (kindTy ty_f) $ \Refl ->
 413         if_EqType typ ty_f $ \Refl ->
 414         k Refl ty_a
 415
 416 if_EqType2
 417  :: ( Inj_Error (Con_Type src '[] ss cs) err
 418     , Inj_Error (Con_Kind src) err
 419     , Inj_Source (EType src '[] ss cs) src )
 420  => Type src ctx ss cs (f:: K.Type -> K.Type -> K.Type)
 421  -> Type src ctx ss cs fab
 422  -> (forall a b. (fab :~: f a b)
 423   -> Type src ctx ss cs a
 424   -> Type src ctx ss cs b
 425   -> Either err ret)
 426  -> Either err ret
 427 if_EqType2 typ ty_fab k =
 428         if_TyApp ty_fab $ \Refl ty_fa ty_b ->
 429         if_TyApp ty_fa  $ \Refl ty_f  ty_a ->
 430         if_EqKind (inj_Kind @(K.Type -> K.Type -> K.Type))
 431                   (kindTy ty_f) $ \Refl ->
 432         if_EqType typ ty_f $ \Refl ->
 433         k Refl ty_a ty_b
 434
 435 if_TyFun ::
 436  ( Inj_TyConst cs (->)
 437  , Inj_Source (EType src '[] ss cs) src
 438  , Inj_Error (Con_Kind src) err
 439  , Inj_Error (Con_Type src '[] ss cs) err
 440  ) => Type src ctx ss cs fab
 441  -> (forall a b. (:~:) fab (a -> b)
 442     -> Type src ctx ss cs a -> Type src ctx ss cs b -> Either err ret)
 443  -> Either err ret
 444 if_TyFun = if_EqType2 (ty @(->))
 445
 446 -- * Type 'EType'
 447 -- | Existential for 'Type'.
 448 data EType src ctx ss cs
 449  = forall h. EType (Type src ctx ss cs h)
 450
 451 instance
 452  Inj_Source (EType src ctx ss cs) src =>
 453  Eq (EType src ctx ss cs) where
 454         EType x == EType y = isJust $ eqKiTy x y
 455
 456 mapEType
 457  :: (forall k (h::k). Type src ctx ss cs h -> Type src ctx ss cs h)
 458  -> EType src ctx ss cs
 459  -> EType src ctx ss cs
 460 mapEType f (EType t) = EType (f t)
 461
 462 bindEType
 463  :: (forall k (h::k). Type src ctx ss cs h -> EType src ctx ss cs)
 464  -> EType src ctx ss cs
 465  -> EType src ctx ss cs
 466 bindEType f (EType t) = f t
 467
 468 -- * Type 'KT'
 469 -- | Existential for 'T' of a known 'Kind'.
 470 data KT src ctx ss cs k = forall (h::k). KT (Type src ctx ss cs h)
 471 type KType = KT
 472 type KTerm src ctx ss cs = KT src ctx ss cs K.Type
 473
 474 instance Eq (KT src ctx ss cs ki) where
 475         KT x == KT y = isJust $ eqTy x y
 476 instance
 477  Inj_Source (EType src ctx ss cs) src =>
 478  Inj_Source (KT src ctx ss cs k) src where
 479         inj_Source (KT t) = inj_Source $ EType t
 480
 481 unKT :: (forall (h::k). Type src ctx ss cs h -> a k) -> KT src ctx ss cs k -> a k
 482 unKT f (KT t) = f t
 483
 484 ofKT :: (forall (h::k). Type src ctx ss cs h -> a) -> KT src ctx ss cs k -> a
 485 ofKT f (KT t) = f t
 486
 487 mapKT
 488  :: (forall (h::k). Type src ctx ss cs h -> Type src ctx ss cs h)
 489  -> KT src ctx ss cs k
 490  -> KT src ctx ss cs k
 491 mapKT f (KT t) = KT (f t)
 492
 493 bindKT
 494  :: (forall (h::k). Type src ctx ss cs h -> KT src ctx ss cs k)
 495  -> KT src ctx ss cs k
 496  -> KT src ctx ss cs k
 497 bindKT f (KT t) = f t
 498
 499 bind2KT
 500  :: (forall (x::ka) (y::kb). Type src ctx ss cs x -> Type src ctx ss cs y -> KT src ctx ss cs kxy)
 501  -> KT src ctx ss cs ka
 502  -> KT src ctx ss cs kb
 503  -> KT src ctx ss cs kxy
 504 bind2KT f (KT x) (KT y) = f x y
 505
 506 -- * Type 'Types'
 507 data Types src ctx ss cs (hs::[K.Type]) where
 508         TypesZ :: Types src ctx ss cs '[]
 509         TypesS :: Type  src ctx ss cs h
 510                -> Types src ctx ss cs hs
 511                -> Types src ctx ss cs (Proxy h ': hs)
 512 infixr 5 `TypesS`
 513
 514 eTypes :: Types src ctx ss cs hs -> [EType src ctx ss cs]
 515 eTypes TypesZ = []
 516 eTypes (TypesS t ts) = EType t : eTypes ts
 517
 518 mapTys
 519  :: (forall k (h::k). Type src ctx ss cs h -> Type src ctx' ss cs h)
 520  -> Types src ctx ss cs hs
 521  -> Types src ctx' ss cs hs
 522 mapTys _f TypesZ = TypesZ
 523 mapTys f (TypesS h hs) = TypesS (f h) (mapTys f hs)
 524
 525 foldlTys
 526  :: (forall k (h::k). Type src ctx ss cs h -> acc -> acc)
 527  -> Types src ctx ss cs hs
 528  -> acc -> acc
 529 foldlTys _f TypesZ acc = acc
 530 foldlTys f (TypesS h hs) acc = foldlTys f hs (f h acc)
 531
 532 foldrTys
 533  :: (forall k (h::k). Type src ctx ss cs h -> acc -> acc)
 534  -> Types src ctx ss cs hs
 535  -> acc -> acc
 536 foldrTys _f TypesZ acc = acc
 537 foldrTys f (TypesS h hs) acc = f h (foldrTys f hs acc)
 538
 539 {-
 540 traverseTys :: (Traversable t, Applicative f) => (a -> f b) -> t a -> f (t b)
 541 traverseTys f TypesZ        = TypesZ
 542 traverseTys f (TypesS h hs) = TypesS <$> f h <*> traverseTys f hs
 543 -}
 544
 545 -- * Type 'TypesKi'
 546 data TypesKi src ctx ss cs hs where
 547         TypesKiZ :: TypesKi src ctx ss cs '[]
 548         TypesKiS :: Type src ctx ss cs (h::k)
 549                  -> TypesKi src ctx ss cs hs
 550                  -> TypesKi src ctx ss cs ((Proxy h, k) ': hs)
 551 infixr 5 `TypesKiS`
 552
 553 eTypesKi :: TypesKi src ctx ss cs hs -> [EType src ctx ss cs]
 554 eTypesKi TypesKiZ = []
 555 eTypesKi (TypesKiS t ts) = EType t : eTypesKi ts
 556
 557 -- * Type 'UnProxy'
 558 type family UnProxy (x::K.Type) :: k where
 559         UnProxy (Proxy x) = x