Language/Symantic/Type/Common.hs

   1 {-# LANGUAGE ConstraintKinds #-}
   2 {-# LANGUAGE DataKinds #-}
   3 {-# LANGUAGE ExistentialQuantification #-}
   4 {-# LANGUAGE FlexibleContexts #-}
   5 {-# LANGUAGE FlexibleInstances #-}
   6 {-# LANGUAGE GADTs #-}
   7 {-# LANGUAGE MultiParamTypeClasses #-}
   8 {-# LANGUAGE Rank2Types #-}
   9 {-# LANGUAGE ScopedTypeVariables #-}
  10 {-# LANGUAGE TypeFamilies #-}
  11 {-# LANGUAGE TypeOperators #-}
  12 {-# LANGUAGE UndecidableInstances #-}
  13 module Language.Symantic.Type.Common where
  14
  15 import Data.Maybe (isJust)
  16 import Data.Proxy
  17 import Data.Type.Equality ((:~:)(Refl))
  18 import Language.Symantic.Lib.Data.Peano
  19 import GHC.Prim (Constraint)
  20
  21 -- * Class 'Eq_Type'
  22
  23 -- | Test two types for equality,
  24 -- returning an Haskell type-level proof
  25 -- of the equality when it holds.
  26 class Eq_Type (ty:: * -> *) where
  27         eq_type :: forall h1 h2. ty h1 -> ty h2 -> Maybe (h1 :~: h2)
  28
  29 -- * Class 'Constraint_Type'
  30 -- | Test if a type satisfies a given 'Constraint',
  31 -- returning an Haskell type-level proof
  32 -- of that satisfaction when it holds.
  33 class Constraint_Type (c:: * -> Constraint) (ty:: * -> *) where
  34         constraint_type :: forall h. Proxy c -> ty h -> Maybe (Dict (c h))
  35         constraint_type _c _ = Nothing
  36
  37 -- * Class 'Constraint1_Type'
  38 class Constraint1_Type (c:: (* -> *) -> Constraint) (ty:: * -> *) where
  39         constraint1_type :: forall f a. Proxy c -> ty (f a) -> Maybe (Dict (c f))
  40         constraint1_type _c _ = Nothing
  41
  42 -- ** Type 'Dict'
  43 -- | 'Dict' captures the dictionary of a 'Constraint':
  44 -- pattern matching on the 'Dict' constructor
  45 -- brings the 'Constraint' into scope.
  46 data Dict :: Constraint -> * where
  47         Dict :: c => Dict c
  48
  49 -- * Type 'Exists_Dict'
  50 data Exists_Dict
  51  = forall c. Exists_Dict (Dict c)
  52
  53 -- * Class 'Type_from'
  54 -- | Parse given @ast@ into a 'Root_of_Type',
  55 -- or return an 'Error_of_Type'.
  56 class Eq_Type ty => Type_from ast (ty:: * -> *) where
  57         type_from
  58          :: Proxy ty
  59          -> ast
  60          -> (forall h. Root_of_Type ty h
  61                     -> Either (Error_of_Type ast (Root_of_Type ty)) ret)
  62          ->            Either (Error_of_Type ast (Root_of_Type ty)) ret
  63
  64 -- ** Type family 'Root_of_Type'
  65 -- | Return the root type of a type.
  66 type family Root_of_Type (ty:: * -> *) :: * -> *
  67
  68 -- ** Type family 'Error_of_Type'
  69 -- | Return the error type of a type.
  70 type family Error_of_Type (ast:: *) (ty:: * -> *) :: *
  71
  72 -- * Type 'No_Type'
  73 -- | A discarded type.
  74 data No_Type (root:: * -> *) h
  75  =   No_Type (root h)
  76  deriving (Eq, Show)
  77
  78 -- * Type 'Type_Root'
  79 -- | The root type, passing itself as parameter to the given type.
  80 newtype Type_Root (ty:: (* -> *) -> * -> *) h
  81  =      Type_Root { unType_Root :: ty (Type_Root ty) h }
  82 type instance Root_of_Type (Type_Root ty) = Type_Root ty
  83 -- type instance Root_of_Type (ty (Type_Root ty)) = Type_Root ty
  84 type instance Error_of_Type ast (Type_Root ty)
  85  = Error_Type_Alt (Error_Type ast)
  86                   (Error_of_Type ast (ty (Type_Root ty)))
  87 instance -- Eq_Type
  88  Eq_Type (ty (Type_Root ty)) =>
  89  Eq_Type (Type_Root ty) where
  90         eq_type (Type_Root x) (Type_Root y) = x `eq_type` y
  91 instance -- Eq
  92  Eq_Type (Type_Root ty) =>
  93  Eq (Type_Root ty h) where
  94         x == y = isJust $ x `eq_type` y
  95 instance -- Constraint_Type c Type_Root
  96  Constraint_Type c (ty (Type_Root ty)) =>
  97  Constraint_Type c (Type_Root ty) where
  98         constraint_type c (Type_Root ty) = constraint_type c ty
  99 instance -- Constraint1_Type c Type_Root
 100  Constraint1_Type c (ty (Type_Root ty)) =>
 101  Constraint1_Type c (Type_Root ty) where
 102         constraint1_type c (Type_Root ty) = constraint1_type c ty
 103 instance -- Type_from
 104  ( Eq_Type (Type_Root ty)
 105  , Type_from ast (ty (Type_Root ty))
 106  , Root_of_Type (ty (Type_Root ty)) ~ Type_Root ty
 107  ) => Type_from ast (Type_Root ty) where
 108         type_from _ty = type_from (Proxy::Proxy (ty (Type_Root ty)))
 109 instance -- String_from_Type
 110  String_from_Type (ty (Type_Root ty)) =>
 111  String_from_Type (Type_Root ty) where
 112         string_from_type (Type_Root ty) = string_from_type ty
 113 instance -- Show
 114  String_from_Type (Type_Root ty) =>
 115  Show (Type_Root ty h) where
 116         show = string_from_type
 117
 118 -- ** Class 'Type_Root_Lift'
 119 -- | Lift a given type to a given root type.
 120 class Type_Root_Lift ty root where
 121         type_root_lift :: forall h. ty root h -> root h
 122 instance
 123  Type_Lift ty root =>
 124  Type_Root_Lift ty (Type_Root root) where
 125         type_root_lift = Type_Root . type_lift
 126
 127 -- * Type 'Type_Alt'
 128 -- | Type making an alternative between two types.
 129 data Type_Alt curr next (root:: * -> *) h
 130  =   Type_Alt_Curr (curr root h)
 131  |   Type_Alt_Next (next root h)
 132 -- | Convenient alias. Requires @TypeOperators@.
 133 type (:|:) = Type_Alt
 134 infixr 5 :|:
 135 type instance Root_of_Type (Type_Alt curr next root) = root
 136 type instance Error_of_Type ast (Type_Alt curr next root)
 137  = Error_of_Type_Alt ast (Error_of_Type ast (curr root))
 138                          (Error_of_Type ast (next root))
 139 -- ** Type family 'Error_of_Type_Alt'
 140 -- | Remove 'No_Type' type when building 'Error_of_Type'.
 141 type family Error_of_Type_Alt ast curr next where
 142         Error_of_Type_Alt ast curr          No_Error_Type = curr
 143         Error_of_Type_Alt ast No_Error_Type next          = next
 144         Error_of_Type_Alt ast curr          next          = Error_Type_Alt curr next
 145
 146 -- ** Type 'No_Error_Type'
 147 -- | A discarded error.
 148 data No_Error_Type
 149  =   No_Error_Type
 150  deriving (Eq, Show)
 151
 152 instance -- Eq_Type
 153  ( Eq_Type (curr root)
 154  , Eq_Type (next root)
 155  ) => Eq_Type (Type_Alt curr next root) where
 156         eq_type (Type_Alt_Curr x) (Type_Alt_Curr y) = x `eq_type` y
 157         eq_type (Type_Alt_Next x) (Type_Alt_Next y) = x `eq_type` y
 158         eq_type _ _ = Nothing
 159 instance -- Eq
 160  ( Eq_Type (curr root)
 161  , Eq_Type (next root)
 162  ) => Eq (Type_Alt curr next root h) where
 163         x == y = isJust $ x `eq_type` y
 164 instance -- Constraint_Type c Type_Alt
 165  ( Constraint_Type c (curr root)
 166  , Constraint_Type c (next root)
 167  ) => Constraint_Type c (Type_Alt curr next root) where
 168         constraint_type c (Type_Alt_Curr ty) = constraint_type c ty
 169         constraint_type c (Type_Alt_Next ty) = constraint_type c ty
 170 instance -- Constraint1_Type c Type_Alt
 171  ( Constraint1_Type c (curr root)
 172  , Constraint1_Type c (next root)
 173  ) => Constraint1_Type c (Type_Alt curr next root) where
 174         constraint1_type c (Type_Alt_Curr ty) = constraint1_type c ty
 175         constraint1_type c (Type_Alt_Next ty) = constraint1_type c ty
 176 instance -- Type_from
 177  ( Eq_Type (curr root)
 178  , Type_from ast (curr root)
 179  , Type_from ast (next root)
 180  , Root_of_Type (curr root) ~ root
 181  , Root_of_Type (next root) ~ root
 182  , Error_Type_Unlift (Error_Type ast) (Error_of_Type ast root)
 183  ) => Type_from ast (Type_Alt curr next root) where
 184         type_from _ty ast k =
 185                 case type_from (Proxy::Proxy (curr root)) ast (Right . k) of
 186                  Right ret -> ret
 187                  Left err ->
 188                         case error_type_unlift err of
 189                          Just (Error_Type_Unsupported_here (_::ast)) ->
 190                                 type_from (Proxy::Proxy (next root)) ast k
 191                          _ -> Left err
 192 instance -- String_from_Type
 193  ( String_from_Type (curr root)
 194  , String_from_Type (next root)
 195  ) => String_from_Type (Type_Alt curr next root) where
 196         string_from_type (Type_Alt_Curr t) = string_from_type t
 197         string_from_type (Type_Alt_Next t) = string_from_type t
 198
 199 -- ** Type 'Type_Lift'
 200 -- | Apply 'Peano_of_Type' on 'Type_LiftN'.
 201 type Type_Lift ty tys
 202  =   Type_LiftN (Peano_of_Type ty tys) ty tys
 203
 204 -- *** Type 'Peano_of_Type'
 205 -- | Return a 'Peano' number derived from the location
 206 -- of a given type within a given type stack,
 207 -- which is used to avoid @OverlappingInstances@.
 208 type family Peano_of_Type
 209  (ty::  (* -> *) -> * -> *)
 210  (tys:: (* -> *) -> * -> *) :: * where
 211         Peano_of_Type ty    ty                   = Zero
 212         Peano_of_Type ty    (Type_Alt ty   next) = Zero
 213         Peano_of_Type other (Type_Alt curr next) = Succ (Peano_of_Type other next)
 214
 215 -- *** Class 'Type_LiftN'
 216 -- | Lift a given type to the top of a given type stack including it,
 217 -- by constructing the appropriate sequence of 'Type_Alt_Curr' and 'Type_Alt_Next'.
 218 class Type_LiftN (p:: *) ty tys where
 219         type_liftN :: forall (root:: * -> *) h. Proxy p -> ty root h -> tys root h
 220 instance Type_LiftN Zero curr curr where
 221         type_liftN _ = id
 222 instance Type_LiftN Zero curr (Type_Alt curr next) where
 223         type_liftN _ = Type_Alt_Curr
 224 instance
 225  Type_LiftN p other next =>
 226  Type_LiftN (Succ p) other (Type_Alt curr next) where
 227         type_liftN _ = Type_Alt_Next . type_liftN (Proxy::Proxy p)
 228
 229 -- | Convenient wrapper around 'type_liftN',
 230 -- passing it the 'Peano' number from 'Peano_of_Type'.
 231 type_lift
 232  :: forall ty tys (root:: * -> *) h.
 233  Type_Lift ty tys =>
 234  ty root h -> tys root h
 235 type_lift = type_liftN (Proxy::Proxy (Peano_of_Type ty tys))
 236
 237 -- ** Type 'Type_Unlift'
 238 -- | Apply 'Peano_of_Type' on 'Type_UnliftN'.
 239 type Type_Unlift ty tys
 240  =   Type_UnliftN (Peano_of_Type ty tys) ty tys
 241
 242 -- *** Class 'Type_UnliftN'
 243 -- | Try to unlift a given type out of a given type stack including it,
 244 -- by deconstructing the appropriate sequence of 'Type_Alt_Curr' and 'Type_Alt_Next'.
 245 class Type_UnliftN (p:: *) ty tys where
 246         type_unliftN :: forall (root:: * -> *) h. Proxy p -> tys root h -> Maybe (ty root h)
 247 instance Type_UnliftN Zero curr curr where
 248         type_unliftN _ = Just
 249 instance Type_UnliftN Zero curr (Type_Alt curr next) where
 250         type_unliftN _ (Type_Alt_Curr x) = Just x
 251         type_unliftN _ (Type_Alt_Next _) = Nothing
 252 instance
 253  Type_UnliftN p other next =>
 254  Type_UnliftN (Succ p) other (Type_Alt curr next) where
 255         type_unliftN _ (Type_Alt_Next x) = type_unliftN (Proxy::Proxy p) x
 256         type_unliftN _ (Type_Alt_Curr _) = Nothing
 257
 258 -- | Convenient wrapper around 'type_unliftN',
 259 -- passing it the 'Peano' number from 'Peano_of_Type'.
 260 type_unlift
 261  :: forall ty tys (root:: * -> *) h.
 262  Type_Unlift ty tys =>
 263  tys root h -> Maybe (ty root h)
 264 type_unlift = type_unliftN (Proxy::Proxy (Peano_of_Type ty tys))
 265
 266 -- * Type 'Type_Type1'
 267 data Type_Type1 f (root:: * -> *) h where
 268         Type_Type1 :: Proxy f -> root a -> Type_Type1 f root (f a)
 269 type instance Root_of_Type      (Type_Type1 f root) = root
 270 type instance Error_of_Type ast (Type_Type1 f root) = No_Error_Type
 271
 272 instance -- Eq_Type
 273  Eq_Type root =>
 274  Eq_Type (Type_Type1 f root) where
 275         eq_type (Type_Type1 _f1 a1) (Type_Type1 _f2 a2)
 276          | Just Refl <- a1 `eq_type` a2
 277          = Just Refl
 278         eq_type _ _ = Nothing
 279 instance -- Eq
 280  Eq_Type root =>
 281  Eq (Type_Type1 f root h) where
 282         x == y = isJust $ eq_type x y
 283 instance -- Show
 284  String_from_Type (Type_Type1 f root) =>
 285  Show (Type_Type1 f root h) where
 286         show = string_from_type
 287
 288 -- * Type 'Type1_f'
 289 type Type1_f tys
 290  =   Type1_fN (Peano_of_Type1 tys) tys
 291
 292 -- ** Type 'Type1_fN'
 293 type family   Type1_fN (p:: *) (tys:: (* -> *) -> * -> *) :: * -> *
 294 type instance Type1_fN Zero     (Type_Type1 f)                 = f
 295 type instance Type1_fN Zero     (Type_Alt (Type_Type1 f) next) = f
 296 type instance Type1_fN (Succ p) (Type_Alt curr next)           = Type1_fN p next
 297
 298 -- ** Type 'Peano_of_Type1'
 299 type family Peano_of_Type1
 300  (tys:: (* -> *) -> * -> *) :: * where
 301         Peano_of_Type1 (Type_Type1 f)                 = Zero
 302         Peano_of_Type1 (Type_Alt (Type_Type1 f) next) = Zero
 303         Peano_of_Type1 (Type_Alt curr next)           = Succ (Peano_of_Type1 next)
 304
 305 -- ** Type 'Type_Unlift1'
 306 -- | Apply 'Peano_of_Type1' on 'Type_Unlift1N'.
 307 type Type_Unlift1 tys
 308  =   Type_Unlift1N (Peano_of_Type1 tys) tys
 309
 310 -- *** Class 'Type_Unlift1N'
 311 -- | Try to unlift1 a given type out of a given type stack including it,
 312 -- by deconstructing the appropriate sequence of 'Type_Alt_Curr' and 'Type_Alt_Next'.
 313 class Type_Unlift1N (p:: *) tys where
 314         type_unlift1N
 315          :: forall (root:: * -> *) h
 316          .  Proxy p
 317          -> tys root h
 318          -> Maybe ( Type_Type1 (Type1_fN p tys) root h
 319                   , Type_Lift1 (Type1_fN p tys) tys )
 320 data Type_Lift1 f tys
 321  =   Type_Lift1 ( forall (root:: * -> *) h
 322                 . Type_Type1 f root h -> tys root h
 323                 )
 324 instance Type_Unlift1N Zero (Type_Type1 f) where
 325         type_unlift1N _ ty = Just (ty, Type_Lift1 id)
 326 instance Type_Unlift1N Zero (Type_Alt (Type_Type1 f) next) where
 327         type_unlift1N _ (Type_Alt_Curr x) = Just (x, Type_Lift1 Type_Alt_Curr)
 328         type_unlift1N _ (Type_Alt_Next _) = Nothing
 329 instance
 330  Type_Unlift1N p next =>
 331  Type_Unlift1N (Succ p) (Type_Alt curr next) where
 332         type_unlift1N _ (Type_Alt_Next x) =
 333                 ((\(Type_Lift1 cons) -> Type_Lift1 $ Type_Alt_Next . cons) <$>) <$>
 334                 type_unlift1N (Proxy::Proxy p) x
 335         type_unlift1N _ (Type_Alt_Curr _) = Nothing
 336
 337 -- | Convenient wrapper around 'type_unlift1N',
 338 -- passing it the 'Peano' number from 'Peano_of_Type1'.
 339 type_unlift1
 340  :: forall tys (root:: * -> *) h
 341  .  Type_Unlift1 tys
 342  => tys root h
 343  -> Maybe ( Type_Type1 (Type1_fN (Peano_of_Type1 tys) tys) root h
 344           , Type_Lift1 (Type1_fN (Peano_of_Type1 tys) tys) tys )
 345 type_unlift1 = type_unlift1N (Proxy::Proxy (Peano_of_Type1 tys))
 346
 347 -- ** Type family 'Is_Last_Type'
 348 -- | Return whether a given type is the last one in a given type stack.
 349 --
 350 -- NOTE: each type parser uses this type family
 351 -- when it encounters unsupported syntax:
 352 -- to know if it is the last type parser component that will be tried
 353 -- (and thus return 'Error_Type_Unsupported')
 354 -- or if some other type parser component shall be tried
 355 -- (and thus return 'Error_Type_Unsupported_here',
 356 -- which is then handled accordingly by the 'Type_from' instance of 'Type_Alt').
 357 type family Is_Last_Type (ty:: * -> *) (tys:: * -> *) :: Bool where
 358         Is_Last_Type ty ty                               = 'True
 359         Is_Last_Type ty        (Type_Root tys)           = Is_Last_Type ty (tys (Type_Root tys))
 360         Is_Last_Type (ty root) (Type_Alt ty   next root) = 'False
 361         Is_Last_Type other     (Type_Alt curr next root) = Is_Last_Type other (next root)
 362
 363 -- * Type 'Error_Type_Alt'
 364 -- | Error type making an alternative between two error types.
 365 data Error_Type_Alt curr next
 366  =   Error_Type_Alt_Curr curr
 367  |   Error_Type_Alt_Next next
 368  deriving (Eq, Show)
 369
 370 -- ** Type 'Error_Type_Lift'
 371 type Error_Type_Lift err errs
 372  =   Error_Type_LiftN (Peano_of_Error_Type err errs) err errs
 373
 374 -- *** Type 'Peano_of_Error_Type'
 375 -- | Return a 'Peano' number derived from the location
 376 -- of a given error type within a given error type stack.
 377 type family Peano_of_Error_Type (err:: *) (errs:: *) :: * where
 378         Peano_of_Error_Type err   err                        = Zero
 379         Peano_of_Error_Type err   (Error_Type_Alt err  next) = Zero
 380         Peano_of_Error_Type other (Error_Type_Alt curr next) = Succ (Peano_of_Error_Type other next)
 381
 382 -- *** Class 'Error_Type_LiftN'
 383 -- | Lift a given error type to the top of a given error type stack including it,
 384 -- by constructing the appropriate sequence of 'Error_Type_Alt_Curr' and 'Error_Type_Alt_Next'.
 385 class Error_Type_LiftN (p:: *) err errs where
 386         error_type_liftN :: Proxy p -> err -> errs
 387 instance Error_Type_LiftN Zero curr curr where
 388         error_type_liftN _ = id
 389 instance Error_Type_LiftN Zero curr (Error_Type_Alt curr next) where
 390         error_type_liftN _ = Error_Type_Alt_Curr
 391 instance
 392  Error_Type_LiftN p other next =>
 393  Error_Type_LiftN (Succ p) other (Error_Type_Alt curr next) where
 394         error_type_liftN _ = Error_Type_Alt_Next . error_type_liftN (Proxy::Proxy p)
 395
 396 -- | Convenient wrapper around 'error_type_unliftN',
 397 -- passing it the 'Peano' number from 'Peano_of_Error_Type'.
 398 error_type_lift
 399  :: forall err errs.
 400  Error_Type_Lift err errs =>
 401  err -> errs
 402 error_type_lift = error_type_liftN (Proxy::Proxy (Peano_of_Error_Type err errs))
 403
 404 -- ** Type 'Error_Type_Unlift'
 405 -- | Apply 'Peano_of_Error_Type' on 'Error_Type_UnliftN'.
 406 type Error_Type_Unlift ty tys
 407  =   Error_Type_UnliftN (Peano_of_Error_Type ty tys) ty tys
 408
 409 -- | Convenient wrapper around 'error_type_unliftN',
 410 -- passing it the 'Peano' number from 'Peano_of_Error_Type'.
 411 error_type_unlift
 412  :: forall ty tys.
 413  Error_Type_Unlift ty tys =>
 414  tys -> Maybe ty
 415 error_type_unlift = error_type_unliftN (Proxy::Proxy (Peano_of_Error_Type ty tys))
 416
 417 -- *** Class 'Error_Type_UnliftN'
 418 -- | Try to unlift a given type error out of a given type error stack including it,
 419 -- by deconstructing the appropriate sequence of 'Error_Type_Alt_Curr' and 'Error_Type_Alt_Next'.
 420 class Error_Type_UnliftN (p:: *) ty tys where
 421         error_type_unliftN :: Proxy p -> tys -> Maybe ty
 422 instance Error_Type_UnliftN Zero curr curr where
 423         error_type_unliftN _ = Just
 424 instance Error_Type_UnliftN Zero curr (Error_Type_Alt curr next) where
 425         error_type_unliftN _ (Error_Type_Alt_Curr x) = Just x
 426         error_type_unliftN _ (Error_Type_Alt_Next _) = Nothing
 427 instance
 428  Error_Type_UnliftN p other next =>
 429  Error_Type_UnliftN (Succ p) other (Error_Type_Alt curr next) where
 430         error_type_unliftN _ (Error_Type_Alt_Next x) = error_type_unliftN (Proxy::Proxy p) x
 431         error_type_unliftN _ (Error_Type_Alt_Curr _) = Nothing
 432
 433 -- ** Type 'Error_Type_Read'
 434 -- | Common type errors.
 435 data Error_Type ast
 436  =   Error_Type_Unsupported ast
 437  -- ^ Given syntax is supported by none
 438  -- of the type parser components
 439  -- of the type stack.
 440  |   Error_Type_Unsupported_here ast
 441  -- ^ Given syntax not supported by the current type parser component.
 442  |   Error_Type_Wrong_number_of_arguments ast Int
 443  deriving (Eq, Show)
 444
 445 -- | Convenient wrapper around 'error_type_lift',
 446 -- passing the type family boilerplate.
 447 error_type
 448  :: Error_Type_Lift (Error_Type ast)
 449                     (Error_of_Type ast (Root_of_Type ty))
 450  => Proxy ty
 451  -> Error_Type ast
 452  -> Error_of_Type ast (Root_of_Type ty)
 453 error_type _ = error_type_lift
 454
 455 error_type_unsupported
 456  :: forall ast ty.
 457  ( Implicit_HBool (Is_Last_Type ty (Root_of_Type ty))
 458  , Error_Type_Lift (Error_Type ast) (Error_of_Type ast (Root_of_Type ty))
 459  ) => Proxy ty -> ast
 460  -> Error_of_Type ast (Root_of_Type ty)
 461 error_type_unsupported ty ast =
 462         case hbool :: HBool (Is_Last_Type ty (Root_of_Type ty)) of
 463          HTrue  -> error_type ty $ Error_Type_Unsupported ast
 464          HFalse -> error_type ty $ Error_Type_Unsupported_here ast
 465
 466 -- * Class 'String_from_Type'
 467 -- | Return a 'String' from a type.
 468 class String_from_Type ty where
 469         string_from_type :: ty h -> String
 470
 471 -- * Type 'Exists_Type'
 472 -- | Existential data type wrapping the index of a type.
 473 data Exists_Type ty
 474  = forall h. Exists_Type (ty h)
 475 instance -- Eq
 476  Eq_Type ty =>
 477  Eq (Exists_Type ty) where
 478         Exists_Type xh == Exists_Type yh =
 479                 isJust $ xh `eq_type` yh
 480 instance -- Show
 481  String_from_Type ty =>
 482  Show (Exists_Type ty) where
 483         show (Exists_Type ty) = string_from_type ty
 484
 485 -- * Type 'Exists_Type1'
 486 -- | Existential data type wrapping the index of a type1.
 487 data Exists_Type1 ty
 488  = forall h. Exists_Type1 (ty h -> ty h)
 489
 490 -- * Type 'Exists_Type_and_Repr'
 491 data Exists_Type_and_Repr ty repr
 492  =   forall h.
 493      Exists_Type_and_Repr (ty h) (repr h)
 494
 495 -- * Type family 'HBool'
 496 -- | Host-type equality.
 497 type family HEq x y :: Bool where
 498         HEq x x = 'True
 499         HEq x y = 'False
 500 -- ** Type 'HBool'
 501 -- | Boolean singleton.
 502 data HBool b where
 503         HTrue  :: HBool 'True
 504         HFalse :: HBool 'False
 505 -- ** Class 'Implicit_HBool'
 506 -- | Construct a host-term boolean singleton from a host-type boolean.
 507 class    Implicit_HBool b      where hbool :: HBool b
 508 instance Implicit_HBool 'True  where hbool = HTrue
 509 instance Implicit_HBool 'False where hbool = HFalse