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