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