Language/Symantic/Type/Common.hs

   1 {-# LANGUAGE ConstraintKinds #-}
   2 {-# LANGUAGE DataKinds #-}
   3 {-# LANGUAGE DefaultSignatures #-}
   4 {-# LANGUAGE ExistentialQuantification #-}
   5 {-# LANGUAGE FlexibleContexts #-}
   6 {-# LANGUAGE FlexibleInstances #-}
   7 {-# LANGUAGE GADTs #-}
   8 {-# LANGUAGE MultiParamTypeClasses #-}
   9 {-# LANGUAGE Rank2Types #-}
  10 {-# LANGUAGE ScopedTypeVariables #-}
  11 {-# LANGUAGE TypeFamilies #-}
  12 {-# LANGUAGE TypeOperators #-}
  13 {-# LANGUAGE UndecidableInstances #-}
  14 module Language.Symantic.Type.Common where
  15
  16 import Data.Maybe (isJust, fromMaybe)
  17 import Data.Proxy
  18 import Data.Type.Equality ((:~:)(Refl))
  19 import Language.Symantic.Lib.Data.Peano
  20 import GHC.Prim (Constraint)
  21
  22 -- * Class 'Eq_Type'
  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 'Eq_Type1'
  30 -- | Test two type constructors for equality,
  31 -- returning an Haskell type-level proof
  32 -- of the equality when it holds.
  33 class Eq_Type1 (ty:: * -> *) where
  34         eq_type1 :: forall h1 h2 a1 a2. ty (h1 a1) -> ty (h2 a2) -> Maybe (h1 :~: h2)
  35         eq_type1 = error "eq_type1"
  36
  37 -- * Class 'Constraint_Type'
  38 -- | Test if a type satisfies a given 'Constraint',
  39 -- returning an Haskell type-level proof
  40 -- of that satisfaction when it holds.
  41 class Constraint_Type (c:: * -> Constraint) (ty:: * -> *) where
  42         constraint_type :: forall h. Proxy c -> ty h -> Maybe (Dict (c h))
  43         constraint_type _c _ = Nothing
  44
  45 -- * Class 'Constraint_Type1'
  46 -- | Test if a type constructor satisfies a given 'Constraint',
  47 -- returning an Haskell type-level proof
  48 -- of that satisfaction when it holds.
  49 class Constraint_Type1 (c:: (* -> *) -> Constraint) (ty:: * -> *) where
  50         constraint_type1 :: forall h1 h. Proxy c -> ty (h1 h) -> Maybe (Dict (c h1))
  51         constraint_type1 _c _ = Nothing
  52
  53 -- ** Type 'Dict'
  54 -- | 'Dict' captures the dictionary of a 'Constraint':
  55 -- pattern matching on the 'Dict' constructor
  56 -- brings the 'Constraint' into scope.
  57 data Dict :: Constraint -> * where
  58         Dict :: c => Dict c
  59
  60 -- * Type 'Exists_Dict'
  61 data Exists_Dict
  62  = forall c. Exists_Dict (Dict c)
  63
  64 -- * Class 'Type_from'
  65 -- | Parse given @ast@ into a 'Root_of_Type',
  66 -- or return an 'Error_of_Type'.
  67 --
  68 -- NOTE: making a distinction between @ty@ and 'Root_of_Type'@ ty@,
  69 -- instead of having only a @root@ variable
  70 -- is what enables to define many instances, one per type.
  71 class Type_from ast (ty:: * -> *) where
  72         type_from
  73          :: Proxy ty
  74          -> ast
  75          -> (forall h. Root_of_Type ty h
  76                     -> Either (Error_of_Type ast (Root_of_Type ty)) ret)
  77          ->            Either (Error_of_Type ast (Root_of_Type ty)) ret
  78
  79 -- * Class 'Type1_from'
  80 -- | Parse given @ast@ into a 'Root_of_Type' constructor,
  81 -- or return an 'Error_of_Type'.
  82 class Type1_from ast (ty:: * -> *) where
  83         type1_from
  84          :: Proxy ty
  85          -> ast
  86          -> (forall (f:: * -> *). Proxy f
  87                     -> (forall h. Root_of_Type ty h -> Root_of_Type ty (f h))
  88                     -> Either (Error_of_Type ast (Root_of_Type ty)) ret)
  89          ->            Either (Error_of_Type ast (Root_of_Type ty)) ret
  90         default type1_from ::
  91          ( Lift_Error_Type (Error_Type ast) (Error_of_Type ast (Root_of_Type ty))
  92          , Implicit_HBool (Is_Last_Type ty (Root_of_Type ty))
  93          ) => Proxy ty
  94          -> ast
  95          -> (forall (f:: * -> *). Proxy f
  96                     -> (forall h. Root_of_Type ty h -> Root_of_Type ty (f h))
  97                     -> Either (Error_of_Type ast (Root_of_Type ty)) ret)
  98          ->            Either (Error_of_Type ast (Root_of_Type ty)) ret
  99         type1_from ty ast _k =
 100                 Left $ error_type_unsupported ty ast
 101
 102 {-
 103 class Type1_f_from (ty:: * -> *) where
 104         type1_f_from
 105          :: Proxy ty
 106          -> (Root_of_Type ty) h_any
 107          -> (forall (f:: * -> *). Proxy f
 108                     -> (forall h. (Root_of_Type ty) h -> (Root_of_Type ty) (f h))
 109                     -> Either ({-Error_of_Type ast (Root_of_Type ty)-}) ret)
 110          ->            Either ({-Error_of_Type ast (Root_of_Type ty)-}) ret
 111 instance -- Type1_f_from
 112  ( Eq_Type (curr root)
 113  , Type1_f_from ast (curr root)
 114  , Type1_f_from ast (next root)
 115  , Root_of_Type (curr root) ~ root
 116  , Root_of_Type (next root) ~ root
 117  -- , Unlift_Error_Type (Error_Type ast) (Error_of_Type ast root)
 118  ) => Type1_from ast (Type_Alt curr next root) where
 119         type1_from _ty ast k =
 120                 case type1_from (Proxy::Proxy (curr root)) ast (\f ty -> Right $ k f ty) of
 121                  Right ret -> ret
 122                  Left err ->
 123                         case unlift_error_type err of
 124                          Just (Error_Type_Unsupported_here (_::ast)) ->
 125                                 type1_from (Proxy::Proxy (next root)) ast k
 126                          _ -> Left err
 127 -}
 128
 129 -- ** Type family 'Root_of_Type'
 130 -- | Return the root type of a type.
 131 type family Root_of_Type (ty:: * -> *) :: * -> *
 132
 133 -- ** Type family 'Error_of_Type'
 134 -- | Return the error type of a type.
 135 type family Error_of_Type (ast:: *) (ty:: * -> *) :: *
 136
 137 -- * Type 'No_Type'
 138 -- | A discarded type.
 139 data No_Type (root:: * -> *) h
 140  =   No_Type (root h)
 141  deriving (Eq, Show)
 142
 143 -- * Type 'Type_Root'
 144 -- | The root type, passing itself as parameter to the given type.
 145 newtype Type_Root (ty:: (* -> *) -> * -> *) h
 146  =      Type_Root { unType_Root :: ty (Type_Root ty) h }
 147 type instance Root_of_Type (Type_Root ty) = Type_Root ty
 148 -- type instance Root_of_Type (ty (Type_Root ty)) = Type_Root ty
 149 type instance Error_of_Type ast (Type_Root ty)
 150  = Error_Type_Alt (Error_Type ast)
 151                   (Error_of_Type ast (ty (Type_Root ty)))
 152 instance -- Eq_Type
 153  Eq_Type (ty (Type_Root ty)) =>
 154  Eq_Type (Type_Root ty) where
 155         eq_type (Type_Root x) (Type_Root y) = x `eq_type` y
 156 instance -- Eq_Type1
 157  Eq_Type1 (ty (Type_Root ty)) =>
 158  Eq_Type1 (Type_Root ty) where
 159         eq_type1 (Type_Root x) (Type_Root y) = x `eq_type1` y
 160 instance -- Eq
 161  Eq_Type (Type_Root ty) =>
 162  Eq (Type_Root ty h) where
 163         x == y = isJust $ x `eq_type` y
 164 instance -- Constraint_Type c Type_Root
 165  Constraint_Type c (ty (Type_Root ty)) =>
 166  Constraint_Type c (Type_Root ty) where
 167         constraint_type c (Type_Root ty) = constraint_type c ty
 168 instance -- Constraint_Type1 c Type_Root
 169  Constraint_Type1 c (ty (Type_Root ty)) =>
 170  Constraint_Type1 c (Type_Root ty) where
 171         constraint_type1 c (Type_Root ty) = constraint_type1 c ty
 172 instance -- Type_from
 173  ( Eq_Type (Type_Root ty)
 174  , Type_from ast (ty (Type_Root ty))
 175  , Root_of_Type (ty (Type_Root ty)) ~ Type_Root ty
 176  ) => Type_from ast (Type_Root ty) where
 177         type_from _ty = type_from (Proxy::Proxy (ty (Type_Root ty)))
 178 instance -- Type1_from
 179  ( Eq_Type (Type_Root ty)
 180  , Type1_from ast (ty (Type_Root ty))
 181  , Root_of_Type (ty (Type_Root ty)) ~ Type_Root ty
 182  ) => Type1_from ast (Type_Root ty) where
 183         type1_from _ty = type1_from (Proxy::Proxy (ty (Type_Root ty)))
 184 instance -- String_from_Type
 185  String_from_Type (ty (Type_Root ty)) =>
 186  String_from_Type (Type_Root ty) where
 187         string_from_type (Type_Root ty) = string_from_type ty
 188 instance -- Show
 189  String_from_Type (Type_Root ty) =>
 190  Show (Type_Root ty h) where
 191         show = string_from_type
 192
 193 -- ** Class 'Lift_Type_Root'
 194 -- | Lift a given type to a given root type.
 195 class Lift_Type_Root ty root where
 196         lift_type_root :: forall h. ty root h -> root h
 197 instance
 198  Lift_Type ty root =>
 199  Lift_Type_Root ty (Type_Root root) where
 200         lift_type_root = Type_Root . lift_type
 201
 202 -- * Type 'Type_Alt'
 203 -- | Type making an alternative between two types.
 204 data Type_Alt curr next (root:: * -> *) h
 205  =   Type_Alt_Curr (curr root h)
 206  |   Type_Alt_Next (next root h)
 207 -- | Convenient alias. Requires @TypeOperators@.
 208 type (:|:) = Type_Alt
 209 infixr 5 :|:
 210 type instance Root_of_Type (Type_Alt curr next root) = root
 211 type instance Error_of_Type ast (Type_Alt curr next root)
 212  = Error_of_Type_Alt ast (Error_of_Type ast (curr root))
 213                          (Error_of_Type ast (next root))
 214 -- ** Type family 'Error_of_Type_Alt'
 215 -- | Remove 'No_Error_Type' type when building 'Error_of_Type'.
 216 type family Error_of_Type_Alt ast curr next where
 217         Error_of_Type_Alt ast curr          No_Error_Type = curr
 218         Error_of_Type_Alt ast No_Error_Type next          = next
 219         Error_of_Type_Alt ast curr          next          = Error_Type_Alt curr next
 220
 221 -- ** Type 'No_Error_Type'
 222 -- | A discarded error.
 223 data No_Error_Type
 224  =   No_Error_Type
 225  deriving (Eq, Show)
 226
 227 instance -- Eq_Type
 228  ( Eq_Type (curr root)
 229  , Eq_Type (next root)
 230  ) => Eq_Type (Type_Alt curr next root) where
 231         eq_type (Type_Alt_Curr x) (Type_Alt_Curr y) = x `eq_type` y
 232         eq_type (Type_Alt_Next x) (Type_Alt_Next y) = x `eq_type` y
 233         eq_type _ _ = Nothing
 234 instance -- Eq_Type1
 235  ( Eq_Type1 (curr root)
 236  , Eq_Type1 (next root)
 237  ) => Eq_Type1 (Type_Alt curr next root) where
 238         eq_type1 (Type_Alt_Curr x) (Type_Alt_Curr y) = x `eq_type1` y
 239         eq_type1 (Type_Alt_Next x) (Type_Alt_Next y) = x `eq_type1` y
 240         eq_type1 _ _ = Nothing
 241 instance -- Eq
 242  ( Eq_Type (curr root)
 243  , Eq_Type (next root)
 244  ) => Eq (Type_Alt curr next root h) where
 245         x == y = isJust $ x `eq_type` y
 246 instance -- Constraint_Type c Type_Alt
 247  ( Constraint_Type c (curr root)
 248  , Constraint_Type c (next root)
 249  ) => Constraint_Type c (Type_Alt curr next root) where
 250         constraint_type c (Type_Alt_Curr ty) = constraint_type c ty
 251         constraint_type c (Type_Alt_Next ty) = constraint_type c ty
 252 instance -- Constraint_Type1 c Type_Alt
 253  ( Constraint_Type1 c (curr root)
 254  , Constraint_Type1 c (next root)
 255  ) => Constraint_Type1 c (Type_Alt curr next root) where
 256         constraint_type1 c (Type_Alt_Curr ty) = constraint_type1 c ty
 257         constraint_type1 c (Type_Alt_Next ty) = constraint_type1 c ty
 258 instance -- Type_from
 259  ( Eq_Type (curr root)
 260  , Type_from ast (curr root)
 261  , Type_from ast (next root)
 262  , Root_of_Type (curr root) ~ root
 263  , Root_of_Type (next root) ~ root
 264  , Unlift_Error_Type (Error_Type ast) (Error_of_Type ast root)
 265  ) => Type_from ast (Type_Alt curr next root) where
 266         type_from _ty ast k =
 267                 case type_from (Proxy::Proxy (curr root)) ast (Right . k) of
 268                  Right ret -> ret
 269                  Left err ->
 270                         case unlift_error_type err of
 271                          Just (Error_Type_Unsupported_here (_::ast)) ->
 272                                 type_from (Proxy::Proxy (next root)) ast k
 273                          _ -> Left err
 274 instance -- Type1_from
 275  ( Eq_Type (curr root)
 276  , Type1_from ast (curr root)
 277  , Type1_from ast (next root)
 278  , Root_of_Type (curr root) ~ root
 279  , Root_of_Type (next root) ~ root
 280  , Unlift_Error_Type (Error_Type ast) (Error_of_Type ast root)
 281  ) => Type1_from ast (Type_Alt curr next root) where
 282         type1_from _ty ast k =
 283                 case type1_from (Proxy::Proxy (curr root)) ast (\f ty -> Right $ k f ty) of
 284                  Right ret -> ret
 285                  Left err ->
 286                         case unlift_error_type err of
 287                          Just (Error_Type_Unsupported_here (_::ast)) ->
 288                                 type1_from (Proxy::Proxy (next root)) ast k
 289                          _ -> Left err
 290 instance -- String_from_Type
 291  ( String_from_Type (curr root)
 292  , String_from_Type (next root)
 293  ) => String_from_Type (Type_Alt curr next root) where
 294         string_from_type (Type_Alt_Curr t) = string_from_type t
 295         string_from_type (Type_Alt_Next t) = string_from_type t
 296
 297 type family Host_of px :: *
 298 type instance Host_of (Proxy h0) = h0
 299
 300 -- * Type 'Type_Type0'
 301 data Type_Type0 px (root:: * -> *) h where
 302         Type_Type0 :: px -> Type_Type0 px root (Host_of px)
 303
 304 type instance Root_of_Type      (Type_Type0 px root) = root
 305 type instance Error_of_Type ast (Type_Type0 px root) = No_Error_Type
 306
 307 instance -- Eq_Type
 308  Eq_Type (Type_Type0 (Proxy h0) root) where
 309         eq_type Type_Type0{} Type_Type0{} = Just Refl
 310 instance -- Eq_Type
 311  Eq_Type (Type_Type0 EPeano root) where
 312         eq_type (Type_Type0 p1)
 313                 (Type_Type0 p2)
 314          | p1 == p2
 315          = Just Refl
 316         eq_type _ _ = Nothing
 317 instance -- Eq
 318  Eq_Type (Type_Type0 px root) =>
 319  Eq (Type_Type0 px root h) where
 320         x == y = isJust $ x `eq_type` y
 321 instance -- Show
 322  String_from_Type (Type_Type0 (Proxy h0) root) =>
 323  Show (Type_Type0 (Proxy h0) root h0) where
 324         show = string_from_type
 325 instance Eq h0 => Constraint_Type Eq (Type_Type0 (Proxy h0) root) where
 326         constraint_type _c Type_Type0{} = Just Dict
 327 instance Ord h0 => Constraint_Type Ord (Type_Type0 (Proxy h0) root) where
 328         constraint_type _c Type_Type0{} = Just Dict
 329 instance Unlift_Type1 (Type_Type0 px)
 330 instance Eq_Type1 (Type_Type0 (Proxy h0) root)
 331
 332 -- | Convenient alias to include a 'Type_Bool' within a type.
 333 type_type0 :: forall root h0. Lift_Type_Root (Type_Type0 (Proxy h0)) root => root h0
 334 type_type0 = lift_type_root (Type_Type0 (Proxy::Proxy h0))
 335
 336 -- ** Type 'Lift_Type'
 337 -- | Apply 'Peano_of_Type' on 'Lift_TypeP'.
 338 type Lift_Type ty tys
 339  =   Lift_TypeP (Peano_of_Type ty tys) ty tys
 340
 341 -- *** Type 'Peano_of_Type'
 342 -- | Return a 'Peano' number derived from the location
 343 -- of a given type within a given type stack,
 344 -- which is used to avoid @OverlappingInstances@.
 345 type family Peano_of_Type
 346  (ty::  (* -> *) -> * -> *)
 347  (tys:: (* -> *) -> * -> *) :: * where
 348         Peano_of_Type ty    ty                   = Zero
 349         Peano_of_Type ty    (Type_Alt ty   next) = Zero
 350         Peano_of_Type other (Type_Alt curr next) = Succ (Peano_of_Type other next)
 351
 352 -- *** Class 'Lift_TypeP'
 353 -- | Lift a given type to the top of a given type stack including it,
 354 -- by constructing the appropriate sequence of 'Type_Alt_Curr' and 'Type_Alt_Next'.
 355 class Lift_TypeP (p:: *) ty tys where
 356         lift_typeP :: forall (root:: * -> *) h. Proxy p -> ty root h -> tys root h
 357 instance Lift_TypeP Zero curr curr where
 358         lift_typeP _ = id
 359 instance Lift_TypeP Zero curr (Type_Alt curr next) where
 360         lift_typeP _ = Type_Alt_Curr
 361 instance
 362  Lift_TypeP p other next =>
 363  Lift_TypeP (Succ p) other (Type_Alt curr next) where
 364         lift_typeP _ = Type_Alt_Next . lift_typeP (Proxy::Proxy p)
 365
 366 -- | Convenient wrapper around 'lift_typeP',
 367 -- passing it the 'Peano' number from 'Peano_of_Type'.
 368 lift_type
 369  :: forall ty tys (root:: * -> *) h.
 370  Lift_Type ty tys =>
 371  ty root h -> tys root h
 372 lift_type = lift_typeP (Proxy::Proxy (Peano_of_Type ty tys))
 373
 374 -- ** Type 'Unlift_Type'
 375 -- | Apply 'Peano_of_Type' on 'Unlift_TypeP'.
 376 type Unlift_Type ty tys
 377  =   Unlift_TypeP (Peano_of_Type ty tys) ty tys
 378
 379 -- *** Class 'Unlift_TypeP'
 380 -- | Try to unlift a given type out of a given type stack including it,
 381 -- by deconstructing the appropriate sequence of 'Type_Alt_Curr' and 'Type_Alt_Next'.
 382 class Unlift_TypeP (p:: *) ty tys where
 383         type_unliftN :: forall (root:: * -> *) h. Proxy p -> tys root h -> Maybe (ty root h)
 384 instance Unlift_TypeP Zero curr curr where
 385         type_unliftN _ = Just
 386 instance Unlift_TypeP Zero curr (Type_Alt curr next) where
 387         type_unliftN _ (Type_Alt_Curr x) = Just x
 388         type_unliftN _ (Type_Alt_Next _) = Nothing
 389 instance
 390  Unlift_TypeP p other next =>
 391  Unlift_TypeP (Succ p) other (Type_Alt curr next) where
 392         type_unliftN _ (Type_Alt_Next x) = type_unliftN (Proxy::Proxy p) x
 393         type_unliftN _ (Type_Alt_Curr _) = Nothing
 394
 395 -- | Convenient wrapper around 'type_unliftN',
 396 -- passing it the 'Peano' number from 'Peano_of_Type'.
 397 unlift_type
 398  :: forall ty tys (root:: * -> *) h.
 399  Unlift_Type ty tys =>
 400  tys root h -> Maybe (ty root h)
 401 unlift_type = type_unliftN (Proxy::Proxy (Peano_of_Type ty tys))
 402
 403 -- * Type 'Type_Type1'
 404 data Type_Type1 px (root:: * -> *) h where
 405         Type_Type1 :: px -> root a -> Type_Type1 px root ((Host1_of px) a)
 406 type instance Root_of_Type      (Type_Type1 px root) = root
 407 type instance Error_of_Type ast (Type_Type1 px root) = No_Error_Type
 408
 409 instance Constraint_Type Eq  (Type_Type1 (Proxy h1) root)
 410 instance Constraint_Type Ord (Type_Type1 (Proxy h1) root)
 411
 412 instance -- Eq_Type
 413  Eq_Type root =>
 414  Eq_Type (Type_Type1 (Proxy h1) root) where
 415         eq_type (Type_Type1 _px1 a1) (Type_Type1 _px2 a2)
 416          | Just Refl <- a1 `eq_type` a2
 417          = Just Refl
 418         eq_type _ _ = Nothing
 419 instance -- Eq_Type
 420  Eq_Type root =>
 421  Eq_Type (Type_Type1 EPeano root) where
 422         eq_type (Type_Type1 p1 a1)
 423                 (Type_Type1 p2 a2)
 424          | p1 == p2
 425          , Just Refl <- a1 `eq_type` a2
 426          = Just Refl
 427         eq_type _ _ = Nothing
 428 instance -- Eq
 429  Eq_Type root =>
 430  Eq (Type_Type1 (Proxy h1) root h) where
 431         x == y = isJust $ eq_type x y
 432 instance -- Eq
 433  Eq_Type root =>
 434  Eq (Type_Type1 EPeano root h) where
 435         x == y = isJust $ eq_type x y
 436 instance -- Eq_Type1
 437  Eq_Type1 (Type_Type1 (Proxy t1) root) where
 438         eq_type1 Type_Type1{} Type_Type1{}
 439          = Just Refl
 440 instance -- Show
 441  String_from_Type (Type_Type1 px root) =>
 442  Show (Type_Type1 px root h) where
 443         show = string_from_type
 444
 445 -- ** Type 'Host1_of'
 446 type family Host1_of px :: * -> *
 447 type instance Host1_of (Proxy h1) = h1
 448
 449 -- ** Type family 'May_be_Type1'
 450 type family May_be_Type1
 451  (ty:: (* -> *) -> * -> *) :: Bool where
 452         May_be_Type1 (Type_Type1 px)                 = 'True
 453         May_be_Type1 (Type_Alt (Type_Type1 px) next) = 'True
 454         May_be_Type1 (Type_Alt curr next)            = May_be_Type1 next
 455         May_be_Type1 ty                              = 'False
 456
 457 -- ** Type 'Lift_Type1'
 458 data Lift_Type1 px tys
 459  =   Lift_Type1 ( forall (root:: * -> *) h
 460                 . Type_Type1 px root h -> tys root h
 461                 )
 462
 463 -- ** Type  'Unlift_Type1'
 464 class Unlift_Type1 ty where
 465         unlift_type1
 466          :: forall (root:: * -> *) ret h.
 467          ty root h
 468          -> (forall (px:: *).
 469              ( Type_Type1 px root h
 470              , Lift_Type1 px ty
 471              ) -> Maybe ret)
 472          -> Maybe ret
 473         unlift_type1 _ty _k = Nothing
 474 instance Unlift_Type1 (Type_Type1 px) where
 475         unlift_type1 ty k = k (ty, Lift_Type1 id)
 476 instance -- Type_Alt
 477  ( Unlift_Type1 curr
 478  , Unlift_Type1 next
 479  ) => Unlift_Type1 (Type_Alt curr next) where
 480         unlift_type1 (Type_Alt_Curr ty) k =
 481                 fromMaybe Nothing $ unlift_type1 ty $ \(t, Lift_Type1 l) ->
 482                         Just $ k (t, Lift_Type1 $ Type_Alt_Curr . l)
 483         unlift_type1 (Type_Alt_Next ty) k =
 484                 fromMaybe Nothing $ unlift_type1 ty $ \(t, Lift_Type1 l) ->
 485                         Just $ k (t, Lift_Type1 $ Type_Alt_Next . l)
 486
 487 -- * Type 'Type_Type2'
 488 data Type_Type2 px (root:: * -> *) h where
 489         Type_Type2
 490          :: (Constraint2_of px) a b
 491          => px -> root a -> root b
 492          -> Type_Type2 px root ((Host2_of px) a b)
 493 class Constraint2_Empty a b
 494 instance Constraint2_Empty a b
 495
 496 type instance Root_of_Type      (Type_Type2 px root) = root
 497 type instance Error_of_Type ast (Type_Type2 px root) = No_Error_Type
 498
 499 instance -- Eq_Type
 500  Eq_Type root =>
 501  Eq_Type (Type_Type2 (Proxy h2) root) where
 502         eq_type
 503          (Type_Type2 _ arg1 res1)
 504          (Type_Type2 _ arg2 res2)
 505          | Just Refl <- arg1 `eq_type` arg2
 506          , Just Refl <- res1 `eq_type` res2
 507          = Just Refl
 508         eq_type _ _ = Nothing
 509 instance -- Eq_Type
 510  Eq_Type root =>
 511  Eq_Type (Type_Type2 EPeano root) where
 512         eq_type (Type_Type2 p1 arg1 res1)
 513                 (Type_Type2 p2 arg2 res2)
 514          | p1 == p2
 515          , Just Refl <- arg1 `eq_type` arg2
 516          , Just Refl <- res1 `eq_type` res2
 517          = Just Refl
 518         eq_type _ _ = Nothing
 519 instance -- Eq
 520  Eq_Type root =>
 521  Eq (Type_Type2 (Proxy h2) root h) where
 522         x == y = isJust $ x `eq_type` y
 523 instance -- Eq
 524  Eq_Type root =>
 525  Eq (Type_Type2 EPeano root h) where
 526         x == y = isJust $ x `eq_type` y
 527 instance -- Show
 528  ( String_from_Type root
 529  , String_from_Type (Type_Type2 px root)
 530  ) => Show (Type_Type2 px root h) where
 531         show = string_from_type
 532 instance Constraint_Type Eq  (Type_Type2 px root)
 533 instance Constraint_Type Ord (Type_Type2 px root)
 534 instance Unlift_Type1 (Type_Type2 px)  -- FIXME: should be doable
 535 instance Eq_Type1 (Type_Type2 px root) -- FIXME: should be doable
 536
 537 -- ** Type 'Host2_of'
 538 type family Host2_of px :: * -> * -> *
 539 type instance Host2_of (Proxy h2) = h2
 540
 541 -- ** Type 'Constraint2_of'
 542 type family Constraint2_of px :: (* -> * -> Constraint)
 543
 544 -- * Type family 'Is_Last_Type'
 545 -- | Return whether a given type is the last one in a given type stack.
 546 --
 547 -- NOTE: each type parser uses this type family
 548 -- when it encounters unsupported syntax:
 549 -- to know if it is the last type parser component that will be tried
 550 -- (and thus return 'Error_Type_Unsupported')
 551 -- or if some other type parser component shall be tried
 552 -- (and thus return 'Error_Type_Unsupported_here',
 553 -- which is then handled accordingly by the 'Type_from' instance of 'Type_Alt').
 554 type family Is_Last_Type (ty:: * -> *) (tys:: * -> *) :: Bool where
 555         Is_Last_Type ty ty                               = 'True
 556         Is_Last_Type ty        (Type_Root tys)           = Is_Last_Type ty (tys (Type_Root tys))
 557         Is_Last_Type (ty root) (Type_Alt ty   next root) = 'False
 558         Is_Last_Type other     (Type_Alt curr next root) = Is_Last_Type other (next root)
 559
 560 -- * Type 'Error_Type_Alt'
 561 -- | Error type making an alternative between two error types.
 562 data Error_Type_Alt curr next
 563  =   Error_Type_Alt_Curr curr
 564  |   Error_Type_Alt_Next next
 565  deriving (Eq, Show)
 566
 567 -- ** Type 'Lift_Error_Type'
 568 type Lift_Error_Type err errs
 569  =   Lift_Error_TypeP (Peano_of_Error_Type err errs) err errs
 570
 571 -- *** Type 'Peano_of_Error_Type'
 572 -- | Return a 'Peano' number derived from the location
 573 -- of a given error type within a given error type stack.
 574 type family Peano_of_Error_Type (err:: *) (errs:: *) :: * where
 575         Peano_of_Error_Type err   err                        = Zero
 576         Peano_of_Error_Type err   (Error_Type_Alt err  next) = Zero
 577         Peano_of_Error_Type other (Error_Type_Alt curr next) = Succ (Peano_of_Error_Type other next)
 578
 579 -- *** Class 'Lift_Error_TypeP'
 580 -- | Lift a given error type to the top of a given error type stack including it,
 581 -- by constructing the appropriate sequence of 'Error_Type_Alt_Curr' and 'Error_Type_Alt_Next'.
 582 class Lift_Error_TypeP (p:: *) err errs where
 583         lift_error_typeP :: Proxy p -> err -> errs
 584 instance Lift_Error_TypeP Zero curr curr where
 585         lift_error_typeP _ = id
 586 instance Lift_Error_TypeP Zero curr (Error_Type_Alt curr next) where
 587         lift_error_typeP _ = Error_Type_Alt_Curr
 588 instance
 589  Lift_Error_TypeP p other next =>
 590  Lift_Error_TypeP (Succ p) other (Error_Type_Alt curr next) where
 591         lift_error_typeP _ = Error_Type_Alt_Next . lift_error_typeP (Proxy::Proxy p)
 592
 593 -- | Convenient wrapper around 'error_type_unliftN',
 594 -- passing it the 'Peano' number from 'Peano_of_Error_Type'.
 595 lift_error_type
 596  :: forall err errs.
 597  Lift_Error_Type err errs =>
 598  err -> errs
 599 lift_error_type = lift_error_typeP (Proxy::Proxy (Peano_of_Error_Type err errs))
 600
 601 -- ** Type 'Unlift_Error_Type'
 602 -- | Apply 'Peano_of_Error_Type' on 'Error_Type_UnliftN'.
 603 type Unlift_Error_Type ty tys
 604  =   Error_Type_UnliftN (Peano_of_Error_Type ty tys) ty tys
 605
 606 -- | Convenient wrapper around 'error_type_unliftN',
 607 -- passing it the 'Peano' number from 'Peano_of_Error_Type'.
 608 unlift_error_type
 609  :: forall ty tys.
 610  Unlift_Error_Type ty tys =>
 611  tys -> Maybe ty
 612 unlift_error_type = error_type_unliftN (Proxy::Proxy (Peano_of_Error_Type ty tys))
 613
 614 -- *** Class 'Error_Type_UnliftN'
 615 -- | Try to unlift a given type error out of a given type error stack including it,
 616 -- by deconstructing the appropriate sequence of 'Error_Type_Alt_Curr' and 'Error_Type_Alt_Next'.
 617 class Error_Type_UnliftN (p:: *) ty tys where
 618         error_type_unliftN :: Proxy p -> tys -> Maybe ty
 619 instance Error_Type_UnliftN Zero curr curr where
 620         error_type_unliftN _ = Just
 621 instance Error_Type_UnliftN Zero curr (Error_Type_Alt curr next) where
 622         error_type_unliftN _ (Error_Type_Alt_Curr x) = Just x
 623         error_type_unliftN _ (Error_Type_Alt_Next _) = Nothing
 624 instance
 625  Error_Type_UnliftN p other next =>
 626  Error_Type_UnliftN (Succ p) other (Error_Type_Alt curr next) where
 627         error_type_unliftN _ (Error_Type_Alt_Next x) = error_type_unliftN (Proxy::Proxy p) x
 628         error_type_unliftN _ (Error_Type_Alt_Curr _) = Nothing
 629
 630 -- ** Type 'Error_Type_Read'
 631 -- | Common type errors.
 632 data Error_Type ast
 633  =   Error_Type_Unsupported ast
 634  -- ^ Given syntax is supported by none
 635  -- of the type parser components
 636  -- of the type stack.
 637  |   Error_Type_Unsupported_here ast
 638  -- ^ Given syntax not supported by the current type parser component.
 639  |   Error_Type_Wrong_number_of_arguments ast Int
 640  deriving (Eq, Show)
 641
 642 -- | Convenient wrapper around 'lift_error_type',
 643 -- passing the type family boilerplate.
 644 error_type
 645  :: Lift_Error_Type (Error_Type ast)
 646                     (Error_of_Type ast (Root_of_Type ty))
 647  => Proxy ty
 648  -> Error_Type ast
 649  -> Error_of_Type ast (Root_of_Type ty)
 650 error_type _ = lift_error_type
 651
 652 error_type_unsupported
 653  :: forall ast ty.
 654  ( Implicit_HBool (Is_Last_Type ty (Root_of_Type ty))
 655  , Lift_Error_Type (Error_Type ast) (Error_of_Type ast (Root_of_Type ty))
 656  ) => Proxy ty -> ast
 657  -> Error_of_Type ast (Root_of_Type ty)
 658 error_type_unsupported ty ast =
 659         case hbool :: HBool (Is_Last_Type ty (Root_of_Type ty)) of
 660          HTrue  -> error_type ty $ Error_Type_Unsupported ast
 661          HFalse -> error_type ty $ Error_Type_Unsupported_here ast
 662
 663 -- * Class 'String_from_Type'
 664 -- | Return a 'String' from a type.
 665 class String_from_Type ty where
 666         string_from_type :: ty h -> String
 667
 668 -- * Type 'Exists_Type'
 669 -- | Existential data type wrapping the index of a type.
 670 data Exists_Type ty
 671  = forall h. Exists_Type (ty h)
 672 instance -- Eq
 673  Eq_Type ty =>
 674  Eq (Exists_Type ty) where
 675         Exists_Type xh == Exists_Type yh =
 676                 isJust $ xh `eq_type` yh
 677 instance -- Show
 678  String_from_Type ty =>
 679  Show (Exists_Type ty) where
 680         show (Exists_Type ty) = string_from_type ty
 681
 682 -- * Type 'Exists_Type1'
 683 -- | Existential data type wrapping the index of a type1.
 684 data Exists_Type1 ty
 685  = forall h. Exists_Type1 (ty h -> ty h)
 686
 687 -- * Type 'Exists_Type_and_Repr'
 688 data Exists_Type_and_Repr ty repr
 689  =   forall h.
 690      Exists_Type_and_Repr (ty h) (repr h)
 691
 692 -- * Type family 'HBool'
 693 -- | Host-type equality.
 694 type family HEq x y :: Bool where
 695         HEq x x = 'True
 696         HEq x y = 'False
 697 -- ** Type 'HBool'
 698 -- | Boolean singleton.
 699 data HBool b where
 700         HTrue  :: HBool 'True
 701         HFalse :: HBool 'False
 702 -- ** Class 'Implicit_HBool'
 703 -- | Construct a host-term boolean singleton from a host-type boolean.
 704 class    Implicit_HBool b      where hbool :: HBool b
 705 instance Implicit_HBool 'True  where hbool = HTrue
 706 instance Implicit_HBool 'False where hbool = HFalse