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 -- ** Type 'Type'
  95 type Type = T
  96
  97 -- ** Type 'Term'
  98 type Term src cs h = T src cs (h::K.Type)
  99
 100 -- | Remove all top 'Term's.
 101 unTerm :: Type src cs (h::k) -> Type src cs (h::k)
 102 unTerm (Term _te x) = unTerm x
 103 unTerm t = t
 104
 105 -- | 'Type' constructor to be used with @TypeApplications@ and @NoMonomorphismRestriction@.
 106 ty :: forall c src cs. (Source src, Inj_TyConst cs c) => Type src cs c
 107 ty = TyConst sourceLess inj_TyConst
 108  -- NOTE: The forall brings @c@ first in the type variables,
 109  -- which is convenient to use @TypeApplications@.
 110
 111 (~>) :: Source src => Inj_TyConst cs (->)
 112  => Type src cs a -> Type src cs b -> Type src cs (a -> b)
 113 (~>) a b = (ty @(->) `tyApp` a) `tyApp` b
 114 infixr 5 ~>
 115
 116 -- | Like 'ty', but for a known 'Source'.
 117 tySourced :: forall c src cs. (Source src, Inj_TyConst cs c) => src -> Type src cs c
 118 tySourced src = TyConst src inj_TyConst
 119
 120 -- | Like 'TyApp', but 'sourceLess'.
 121 tyApp :: Source src => Type src cs f -> Type src cs a -> Type src cs (f a)
 122 tyApp = TyApp sourceLess
 123 infixl 9 `tyApp`
 124
 125 -- | Like 'TyQuant', but 'sourceLess'.
 126 tyQuant
 127  :: Source src
 128  => NameHint
 129  -> Kind src kv
 130  -> (forall (v::kv). Type src cs v -> KT src cs k)
 131  -> KT src cs k
 132 tyQuant n kv f = KT $ TyQuant sourceLess n kv f
 133
 134 -- | Return the 'Kind' of the given 'Type'.
 135 kindTy :: Inj_Source (EType src cs) src => Type src cs (h::k) -> Kind src k
 136 kindTy t = kindTyOS t `source` EType t
 137
 138 -- | Like 'kindTy' but keep the old 'Source'.
 139 kindTyOS :: Type src cs (h::k) -> Kind src k
 140 kindTyOS = go
 141         where
 142         go :: forall cs src k h. Type src cs (h::k) -> Kind src k
 143         go = \case
 144          TyConst _src c -> kindTyConst c
 145          TyApp _src f _x ->
 146                 case kindTyOS f of
 147                  KiArrow _src_kf _kx kf -> kf
 148          TyQuant src _n k f -> unKT kindTyOS $ f (TyVar src k 0)
 149          TyVar  _src k _v   -> k
 150          Term _te x         -> kindTyOS x
 151
 152 instance -- TestEquality
 153  Inj_Source (EType src cs) src
 154  => TestEquality (Type src cs) where
 155         testEquality = eqTy
 156 instance Eq (Type src cs h) where
 157         _x == _y = True
 158
 159 -- | Return a proof when two 'Type's are equals.
 160 --
 161 -- NOTE: 'TyQuant's are not compared:
 162 -- they first have to be monomorphized.
 163 eqTy :: Type src cs (x::k) -> Type src cs (y::k) -> Maybe (x:~:y)
 164 eqTy = go
 165         where
 166         go :: Type src cs (x::k) -> Type src cs (y::k) -> Maybe (x:~:y)
 167         go (TyConst _sx x) (TyConst _sy y)
 168          | Just Refl <- testEquality x y
 169          = Just Refl
 170         go (TyApp _sx fx xx) (TyApp _sy fy xy)
 171          | Just Refl <- eqKi (kindTyOS fx) (kindTyOS fy)
 172          , Just Refl <- go fx fy
 173          , Just Refl <- go xx xy
 174          = Just Refl
 175         go TyQuant{} TyQuant{} = Nothing
 176         {-
 177         go v (TyQuant sx _nx kx x::Type src cs vx)
 178              (TyQuant sy _ny ky y::Type src cs vy)
 179          | Just Refl <- eqKi kx ky
 180          , Just Refl <- go (v - 1) (x $ TyVar sx kx v) (y $ TyVar sy ky v)
 181          = Just Refl
 182         -}
 183         go (TyVar _sx kx x) (TyVar _sy ky y)
 184          | Just Refl <- eqKi kx ky
 185          , True <- x == y
 186          = Just Refl
 187         -- NOTE: 'Term' are transparent to 'eqTy'.
 188         go (Term _tx x) (Term _ty y) | Just Refl <- go x y = Just Refl
 189         go (Term _tx x) y            | Just Refl <- go x y = Just Refl
 190         go x            (Term _ty y) | Just Refl <- go x y = Just Refl
 191         go _x _y = Nothing
 192
 193 -- | Return two proofs when two 'Type's are equals:
 194 -- one for the type and one for the kind.
 195 eqKiTy :: Type src cs (x::kx) -> Type src cs (y::ky) -> Maybe (x:~~:y)
 196 eqKiTy = go
 197         where
 198         go :: Type src cs (x::kx) -> Type src cs (y::ky) -> Maybe (x:~~:y)
 199         go (TyConst _sx x) (TyConst _sy y) = eqKiTyConst x y
 200         go (TyApp _sx fx xx) (TyApp _sy fy xy)
 201          | Just KRefl <- go fx fy
 202          , Just KRefl <- go xx xy
 203          = Just KRefl
 204         go TyQuant{} TyQuant{} = Nothing
 205         go (TyVar _sx kx _x) (TyVar _sy ky _y)
 206          | Just Refl <- eqKi kx ky
 207          = Just KRefl
 208         go (Term _tx x) (Term _ty y) = go x y
 209         go _x _y = Nothing
 210
 211 -- * Type '(#>)'
 212 -- | 'TyConst' to qualify a 'Type'.
 213 data (#>) (q::Constraint) (a::K.Type)
 214
 215 (#>)
 216  :: Source src
 217  => Inj_TyConst cs (#>)
 218  => Type src cs a -> Type src cs b -> Type src cs (a #> b)
 219 (#>) a b = (ty @(#>) `tyApp` a) `tyApp` b
 220 infixr 0 #>
 221  -- NOTE: should actually be (-1)
 222  -- to compose well with @infixr 0 (->)@
 223  -- but this is not allowed by GHC.
 224
 225 instance
 226  ( Show_TyConst cs
 227  , Proj_TyConst cs (->)
 228  , Proj_TyConst cs (#>)
 229  ) => Show (Type src cs h) where
 230         showsPrec = showTy
 231
 232 showTy :: forall cs src h.
 233  ( Show_TyConst cs
 234  , Proj_TyConst cs (->)
 235  , Proj_TyConst cs (#>)
 236  ) => Int -> Type src cs h -> ShowS
 237 showTy pr typ = go Nothing (freeTyVar typ) (Map.empty, namesTy typ) pr typ
 238         where
 239         go :: forall p x.
 240             Maybe (Type src cs p) -- parent Type, used to prettify
 241          -> Var                   -- variable counter (DeBruijn)
 242          -> ( Map Var Name        -- names of bound variables
 243             , Names               -- used names : bound variables', free variables' and constants'
 244             )
 245          -> Int                   -- precedence
 246          -> Type src cs x
 247          -> ShowS
 248         go _prev _v _vs p (TyConst _src c) = showsPrec p c
 249         -- TODO: special infix case for (->), could be abstracted to handle others.
 250         go _prev v vs p t@(TyApp _ (TyApp _ (TyConst _ f) a) b)
 251          | Just KRefl <- projKiTyConst @_ @(->) f =
 252                 showParen (p > 0) $
 253                 go (Just t) v vs 1 a .
 254                 showString " -> " .
 255                 go (Just t) v vs 0 b
 256         -- TODO: special infix case for (#>), could be abstracted to handle others.
 257         go _prev v vs p t@(TyApp _ (TyApp _ (TyConst _ f) a) b)
 258          | Just KRefl <- projKiTyConst @_ @(#>) f =
 259                 showParen (p > 0) $
 260                 go (Just t) v vs 0 a .
 261                 showString " => " .
 262                 go (Just t) v vs 0 b
 263         go _prev v vs p t@(TyApp _src f a) =
 264                 showParen (p > 10) $
 265                 go (Just t) v vs 11 f .
 266                 showString " " .
 267                 go (Just t) v vs 11 a
 268         go prev v (vs, ns) p t@(TyQuant src nv kv f) =
 269                 let var = TyVar src kv v in
 270                 let n   = freshifyName ns nv in
 271                 let vs' = Map.insert v n vs in
 272                 let ns' = Set.insert n ns in
 273                 case f var of
 274                  KT x ->
 275                         showParen (p > 10) $
 276                         (case prev of
 277                          Just TyQuant{} -> id
 278                          _ -> showString "forall") .
 279                         showString " " .
 280                         go (Just t) v (vs', ns') p var .
 281                         (case x of
 282                          TyQuant{} -> id
 283                          _ -> showString ". ") .
 284                         go (Just t) (v + 1) (vs', ns') 0 x
 285         go _prev _v (vs, _ns) _p (TyVar _src _kv tv) =
 286                 case Map.lookup tv vs of
 287                  Nothing -> showString "#" . showsPrec 0 tv
 288                  Just n  -> showString $ Text.unpack n
 289         go _prev v vs _p t@(Term _te x) = showBracket True $ go (Just t) v vs 0 x
 290
 291 showBracket :: Bool -> ShowS -> ShowS
 292 showBracket b p =  if b then showChar '{' . p . showChar '}' else p
 293
 294 -- ** Type 'TyCon'
 295 -- | Captures the proof of a 'Constraint'
 296 -- (and its dictionaries when it contains type classes):
 297 -- pattern matching on the 'TyCon' constructor
 298 -- brings the 'Constraint' into scope.
 299 data TyCon c where
 300         Dict :: c => TyCon c
 301
 302 -- ** Type 'TyFamName'
 303 type TyFamName = Text
 304
 305 -- ** Class 'Sym'
 306 class Sym (term::K.Type -> K.Type) where
 307         sym_lam :: (term a -> term b) -> term (a -> b)
 308         sym_app :: term (a -> b) -> (term a -> term b)
 309         sym_int :: Int -> term Int
 310         sym_id  :: term (a -> a)
 311         sym_uc  :: term (Char -> Char)
 312         -- sym_bind :: Monad m => term (m a) -> term (a -> m b) -> term (m b)
 313         -- sym_bind :: term (Monad m #> (m a -> (a -> m b) -> m b))
 314         sym_bind :: Monad m => term (m a -> (a -> m b) -> m b)
 315         sym_const :: term a -> term b -> term a
 316         -- sym_comp :: term (b -> c) -> term (a -> c) -> term (a -> b)
 317         sym_comp :: term ((b -> c) -> (a -> b) -> a -> c)
 318
 319 -- ** Type 'TeSym'
 320 data TeSym (h::K.Type) = TeSym (forall term. Sym term => term h)
 321
 322 instance Source src => Sourced (Type src cs h) where
 323         type Source_of (Type src cs h) = src
 324
 325         source_of (TyConst src _c)        = src
 326         source_of (TyApp   src _f _x)     = src
 327         source_of (TyQuant src _n _kv _f) = src
 328         source_of (TyVar   src _kv _v)    = src
 329         source_of (Term  _te x)           = source_of x
 330
 331         source_is (TyConst _src c)      src = TyConst src c
 332         source_is (TyApp   _src f x)    src = TyApp   src f x
 333         source_is (TyQuant _src n kv f) src = TyQuant src n kv f
 334         source_is (TyVar   _src kv v)   src = TyVar   src kv v
 335         source_is (Term  te x)          src = Term te $ source_is x src
 336
 337 -- ** Type 'Var'
 338 type Var = Int
 339
 340 -- | Return the smallest 'Var' not used in given 'Type'.
 341 freeTyVar :: Type src cs (h::k) -> Var
 342 freeTyVar = (+ 1) . maxTyVar (-1)
 343         where
 344         maxTyVar :: Var -> Type src cs h -> Var
 345         maxTyVar m TyConst{}             = m
 346         maxTyVar m (TyApp   _src f a)    = maxTyVar m f `max` maxTyVar m a
 347         maxTyVar m (TyQuant src _n kv f) = ofKT (maxTyVar m) $ f $ TyVar src kv (-1)
 348         maxTyVar m (TyVar   _src _kv v)  = max m $ if v < 0 then -1 else v + 1
 349         maxTyVar m (Term  _te x)         = maxTyVar m x
 350
 351 -- ** Type 'Name'
 352 type Name     = Text
 353 type NameHint = Name
 354 type Names    = Set Name
 355
 356 namesTy :: Show_TyConst cs => Type src cs h -> Names
 357 namesTy (TyConst _src c)      = Set.singleton $ Text.pack $ show_TyConst c
 358 namesTy (TyApp   _src f x)    = namesTy f `Set.union` namesTy x
 359 namesTy (TyQuant src _n kv f) = ofKT namesTy $ f $ TyVar src kv (-1)
 360 namesTy (TyVar   _src _kv v)  | v < 0     = Set.empty
 361                               | otherwise = Set.singleton $ "#" <> Text.pack (show v)
 362 namesTy (Term  _te x) = namesTy x
 363
 364 -- | Infinite list of unique 'Name's:
 365 -- @a, b, .., z, a1, b1 .., z1, a2, ..@
 366 poolNames :: [Name]
 367 poolNames =
 368         [ Text.singleton n     | n <- ['a'..'z'] ] <>
 369         [ Text.pack (n:show i) | n <- ['a'..'z']
 370                                , i <- [1 :: Int ..] ]
 371
 372 -- | Return given 'Name' renamed a bit to avoid
 373 -- conflicting with any given 'Names'.
 374 freshifyName :: Names -> Name -> Name
 375 freshifyName ns "" = freshName ns
 376 freshifyName ns n =
 377         let ints = [1..] :: [Int] in
 378         List.head
 379          [ fresh
 380          | suffix <- "" : (show <$> ints)
 381          , fresh <- [n <> Text.pack suffix]
 382          , fresh `Set.notMember` ns
 383          ]
 384
 385 freshName :: Names -> Name
 386 freshName ns = List.head $ poolNames List.\\ Set.toList ns
 387
 388 -- * Type 'Con_Type'
 389 data Con_Type src cs
 390  =   Con_EqType  (EType src cs) (EType src cs)
 391  |   Con_TyApp   (EType src cs)
 392  |   Con_TyCon   (KT src cs Constraint)
 393  |   Con_TyFam   (At src TyFamName) [EType src cs]
 394 deriving instance
 395  ( Eq src
 396  , Inj_Source (EType src cs) src
 397  ) => Eq (Con_Type src cs)
 398 deriving instance
 399  ( Show src
 400  , Show_TyConst cs
 401  , Proj_TyConst cs (->)
 402  , Proj_TyConst cs (#>)
 403  ) => Show (Con_Type src cs)
 404
 405 if_TyApp
 406  :: ( Inj_Error (Con_Type src cs) err
 407     , Inj_Source (EType src cs) src )
 408  => Type src cs (fa::kfa)
 409  -> (forall ka f a. (fa :~: f a)
 410   -> Type src cs (f::ka -> kfa)
 411   -> Type src cs (a::ka)
 412   -> Either err ret)
 413  -> Either err ret
 414 if_TyApp typ k =
 415         case typ of
 416          TyApp _src a b -> k Refl (a `source` EType typ) (b `source` EType typ)
 417          _ -> Left $ inj_Error $ Con_TyApp (EType typ)
 418
 419 if_EqType
 420  :: Inj_Error (Con_Type src cs) err
 421  => Type src cs x
 422  -> Type src cs y
 423  -> ((x :~: y) -> Either err ret) -> Either err ret
 424 if_EqType x y k =
 425         case x `eqTy` y of
 426          Just Refl -> k Refl
 427          Nothing -> Left $ inj_Error $
 428                 Con_EqType (EType x) (EType y)
 429
 430 if_EqType1
 431  :: ( Inj_Error (Con_Type src cs) err
 432     , Inj_Error (Con_Kind src) err
 433     , Inj_Source (EType src cs) src
 434     )
 435  => Type src cs (f:: K.Type -> K.Type)
 436  -> Type src cs fa
 437  -> (forall a. (fa :~: f a)
 438   -> Type src cs a
 439   -> Either err ret)
 440  -> Either err ret
 441 if_EqType1 typ ty_fa k =
 442         if_TyApp ty_fa $ \Refl ty_f ty_a ->
 443         if_EqKind (kind @(K.Type -> K.Type))
 444                   (kindTy ty_f) $ \Refl ->
 445         if_EqType typ ty_f $ \Refl ->
 446         k Refl ty_a
 447
 448 if_EqType2
 449  :: ( Inj_Error (Con_Type src cs) err
 450     , Inj_Error (Con_Kind src) err
 451     , Inj_Source (EType src cs) src )
 452  => Type src cs (f:: K.Type -> K.Type -> K.Type)
 453  -> Type src cs fab
 454  -> (forall a b. (fab :~: f a b)
 455   -> Type src cs a
 456   -> Type src cs b
 457   -> Either err ret)
 458  -> Either err ret
 459 if_EqType2 typ ty_fab k =
 460         if_TyApp ty_fab $ \Refl ty_fa ty_b ->
 461         if_TyApp ty_fa  $ \Refl ty_f  ty_a ->
 462         if_EqKind (kind @(K.Type -> K.Type -> K.Type))
 463                   (kindTy ty_f) $ \Refl ->
 464         if_EqType typ ty_f $ \Refl ->
 465         k Refl ty_a ty_b
 466
 467 if_TyFun ::
 468  ( Inj_TyConst cs (->)
 469  , Inj_Source (EType src cs) src
 470  , Inj_Error (Con_Kind src) err
 471  , Inj_Error (Con_Type src cs) err
 472  ) => Type src cs fab
 473  -> (forall a b. (:~:) fab (a -> b)
 474     -> Type src cs a -> Type src cs b -> Either err ret)
 475  -> Either err ret
 476 if_TyFun = if_EqType2 (ty @(->))
 477
 478 -- * Type 'EType'
 479 -- | Existential for 'Type'.
 480 data EType src cs = forall h. EType (Type src cs h)
 481
 482 instance Inj_Source (EType src cs) src => Eq (EType src cs) where
 483         EType x == EType y = isJust $ eqKiTy x y
 484 instance
 485  ( Show_TyConst cs
 486  , Proj_TyConst cs (->)
 487  , Proj_TyConst cs (#>)
 488  ) => Show (EType src cs) where
 489         showsPrec p (EType t) = showsPrec p t
 490
 491 mapEType
 492  :: (forall k (h::k). Type src cs h -> Type src cs h)
 493  -> EType src cs
 494  -> EType src cs
 495 mapEType f (EType t) = EType (f t)
 496
 497 bindEType
 498  :: (forall k (h::k). Type src cs h -> EType src cs)
 499  -> EType src cs
 500  -> EType src cs
 501 bindEType f (EType t) = f t
 502
 503 -- * Type 'KT'
 504 -- | Existential for 'T' of a known 'Kind'.
 505 data KT src cs k = forall (h::k). KT (Type src cs h)
 506 type KType = KT
 507 type KTerm src cs = KT src cs K.Type
 508
 509 instance Eq (KT src cs ki) where
 510         KT x == KT y = isJust $ eqTy x y
 511 instance
 512  ( Show_TyConst cs
 513  , Proj_TyConst cs (->)
 514  , Proj_TyConst cs (#>)
 515  ) => Show (KT src cs ki) where
 516         showsPrec p (KT t) = showTy p t
 517 instance Inj_Source (EType src cs) src => Inj_Source (KT src cs k) src where
 518         inj_Source (KT t) = inj_Source $ EType t
 519
 520 unKT :: (forall (h::k). Type src cs h -> a k) -> KT src cs k -> a k
 521 unKT f (KT t) = f t
 522
 523 ofKT :: (forall (h::k). Type src cs h -> a) -> KT src cs k -> a
 524 ofKT f (KT t) = f t
 525
 526 mapKT
 527  :: (forall (h::k). Type src cs h -> Type src cs h)
 528  -> KT src cs k
 529  -> KT src cs k
 530 mapKT f (KT t) = KT (f t)
 531
 532 bindKT
 533  :: (forall (h::k). Type src cs h -> KT src cs k)
 534  -> KT src cs k
 535  -> KT src cs k
 536 bindKT f (KT t) = f t
 537
 538 bind2KT
 539  :: (forall (x::ka) (y::kb). Type src cs x -> Type src cs y -> KT src cs kxy)
 540  -> KT src cs ka
 541  -> KT src cs kb
 542  -> KT src cs kxy
 543 bind2KT f (KT x) (KT y) = f x y
 544
 545 -- * Type 'Types'
 546 data Types src cs (hs::[K.Type]) where
 547         TypesZ :: Types src cs '[]
 548         TypesS :: Type  src cs h
 549                -> Types src cs hs
 550                -> Types src cs (Proxy h ': hs)
 551 infixr 5 `TypesS`
 552
 553 showTys
 554  :: forall cs src hs.
 555     Show_TyConst cs
 556  => Proj_TyConst cs (->)
 557  => Proj_TyConst cs (#>)
 558  => Types src cs hs -> ShowS
 559 showTys ts = showString "[" . go ts . showString "]"
 560         where
 561         go :: forall xs. Types src cs xs -> ShowS
 562         go TypesZ = showString ""
 563         go (TypesS h0 (TypesS h1 hs)) = showTy 10 h0 . showString ", " . showTy 10 h1 . go hs
 564         go (TypesS h hs) = showTy 10 h . go hs
 565
 566 instance
 567  ( Show_TyConst cs
 568  , Proj_TyConst cs (->)
 569  , Proj_TyConst cs (#>)
 570  ) => Show (Types src cs hs) where
 571         showsPrec _p = showTys
 572
 573 eTypes :: Types src cs hs -> [EType src cs]
 574 eTypes TypesZ = []
 575 eTypes (TypesS t ts) = EType t : eTypes ts
 576
 577 {-
 578 -- * Type 'UnProxy'
 579 type family UnProxy (x::K.Type) :: k where
 580         UnProxy (Proxy x) = x
 581 -}