    {-# OPTIONS_GHC -fno-warn-orphans #-}

    module Agda.TypeChecking.Serialise.Instances.Internal where

    import qualified Data.HashSet as HashSet
    import Control.Monad
    import Control.Monad.IO.Class

    import Agda.Syntax.Internal as I
    import Agda.Syntax.Position as P

    import Agda.TypeChecking.Serialise.Base
    import Agda.TypeChecking.Serialise.Instances.Compilers () --instance only

    import Agda.TypeChecking.Monad
    import Agda.TypeChecking.CompiledClause
    import Agda.TypeChecking.Positivity.Occurrence
    import Agda.TypeChecking.Coverage.SplitTree
    import Agda.TypeChecking.DiscrimTree.Types

    import Agda.Utils.Functor
    import Agda.Utils.Permutation

    import Agda.Utils.Impossible

    instance EmbPrj a => EmbPrj (Dom a) where
      icod_ :: Dom a -> S Word32
    icod_ (Dom ArgInfo
    a Maybe NamedName
    c Bool
    d Maybe Term
    e a
    f) = (ArgInfo -> Maybe NamedName -> Bool -> Maybe Term -> a -> Dom a)
    -> Arrows
         (Domains
            (ArgInfo -> Maybe NamedName -> Bool -> Maybe Term -> a -> Dom a))
         (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Domains t) (S Word32)
    icodeN' ArgInfo -> Maybe NamedName -> Bool -> Maybe Term -> a -> Dom a
    forall t e.
    ArgInfo -> Maybe NamedName -> Bool -> Maybe t -> e -> Dom' t e
    Dom ArgInfo
    a Maybe NamedName
    c Bool
    d Maybe Term
    e a
    f

      value :: Word32 -> R (Dom a)
    value = (ArgInfo -> Maybe NamedName -> Bool -> Maybe Term -> a -> Dom a)
    -> Word32
    -> R (CoDomain
            (ArgInfo -> Maybe NamedName -> Bool -> Maybe Term -> a -> Dom a))
    forall t.
    (VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
    t -> Word32 -> R (CoDomain t)
    valueN ArgInfo -> Maybe NamedName -> Bool -> Maybe Term -> a -> Dom a
    forall t e.
    ArgInfo -> Maybe NamedName -> Bool -> Maybe t -> e -> Dom' t e
    Dom

    instance EmbPrj Signature where
      icod_ :: Signature -> S Word32
    icod_ (Sig Sections
    a Definitions
    b RewriteRuleMap
    c InstanceTable
    d) = (Sections
     -> Definitions -> RewriteRuleMap -> InstanceTable -> Signature)
    -> Arrows
         (Domains
            (Sections
             -> Definitions -> RewriteRuleMap -> InstanceTable -> Signature))
         (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Domains t) (S Word32)
    icodeN' Sections
    -> Definitions -> RewriteRuleMap -> InstanceTable -> Signature
    Sig Sections
    a Definitions
    b RewriteRuleMap
    c InstanceTable
    d

      value :: Word32 -> R Signature
    value = (Sections
     -> Definitions -> RewriteRuleMap -> InstanceTable -> Signature)
    -> Word32
    -> R (CoDomain
            (Sections
             -> Definitions -> RewriteRuleMap -> InstanceTable -> Signature))
    forall t.
    (VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
    t -> Word32 -> R (CoDomain t)
    valueN Sections
    -> Definitions -> RewriteRuleMap -> InstanceTable -> Signature
    Sig

    instance EmbPrj InstanceTable where
      icod_ :: InstanceTable -> S Word32
    icod_ (InstanceTable DiscrimTree QName
    a Map QName Int
    b) = (DiscrimTree QName -> Map QName Int -> InstanceTable)
    -> Arrows
         (Domains (DiscrimTree QName -> Map QName Int -> InstanceTable))
         (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Domains t) (S Word32)
    icodeN' DiscrimTree QName -> Map QName Int -> InstanceTable
    InstanceTable DiscrimTree QName
    a Map QName Int
    b

      value :: Word32 -> R InstanceTable
    value = (DiscrimTree QName -> Map QName Int -> InstanceTable)
    -> Word32
    -> R (CoDomain
            (DiscrimTree QName -> Map QName Int -> InstanceTable))
    forall t.
    (VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
    t -> Word32 -> R (CoDomain t)
    valueN DiscrimTree QName -> Map QName Int -> InstanceTable
    InstanceTable

    instance EmbPrj Section where
      icod_ :: Section -> S Word32
    icod_ (Section Telescope
    a) = (Telescope -> Section)
    -> Arrows (Domains (Telescope -> Section)) (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Domains t) (S Word32)
    icodeN' Telescope -> Section
    Section Telescope
    a

      value :: Word32 -> R Section
    value = (Telescope -> Section)
    -> Word32 -> R (CoDomain (Telescope -> Section))
    forall t.
    (VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
    t -> Word32 -> R (CoDomain t)
    valueN Telescope -> Section
    Section

    instance EmbPrj a => EmbPrj (Tele a) where
      icod_ :: Tele a -> S Word32
    icod_ Tele a
    EmptyTel        = Tele (ZonkAny 23)
    -> Arrows (Domains (Tele (ZonkAny 23))) (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Domains t) (S Word32)
    icodeN' Tele (ZonkAny 23)
    forall a. Tele a
    EmptyTel
      icod_ (ExtendTel a
    a Abs (Tele a)
    b) = (a -> Abs (Tele a) -> Tele a)
    -> Arrows (Domains (a -> Abs (Tele a) -> Tele a)) (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Domains t) (S Word32)
    icodeN' a -> Abs (Tele a) -> Tele a
    forall a. a -> Abs (Tele a) -> Tele a
    ExtendTel a
    a Abs (Tele a)
    b

      value :: Word32 -> R (Tele a)
    value = ([Word32] -> R (Tele a)) -> Word32 -> R (Tele a)
    forall a. EmbPrj a => ([Word32] -> R a) -> Word32 -> R a
    vcase [Word32] -> R (Tele a)
    forall {a}. EmbPrj a => [Word32] -> StateT St IO (Tele a)
    valu where
        valu :: [Word32]
    -> Arrows
         (Constant Word32 (Domains (Tele a))) (R (CoDomain (Tele a)))
    valu []     = Tele a
    -> Arrows
         (Constant Word32 (Domains (Tele a))) (R (CoDomain (Tele a)))
    forall t.
    (VALU t (IsBase t),
     StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
    valuN Tele a
    forall a. Tele a
    EmptyTel
        valu [Word32
    a, Word32
    b] = (a -> Abs (Tele a) -> Tele a)
    -> Arrows
         (Constant Word32 (Domains (a -> Abs (Tele a) -> Tele a)))
         (R (CoDomain (a -> Abs (Tele a) -> Tele a)))
    forall t.
    (VALU t (IsBase t),
     StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
    valuN a -> Abs (Tele a) -> Tele a
    forall a. a -> Abs (Tele a) -> Tele a
    ExtendTel Word32
    a Word32
    b
        valu [Word32]
    _      = StateT St IO (Tele a)
    Arrows (Constant Word32 (Domains (Tele a))) (R (CoDomain (Tele a)))
    forall a. R a
    malformed

    instance EmbPrj Permutation where
      icod_ :: Permutation -> S Word32
    icod_ (Perm Int
    a [Int]
    b) = (Int -> [Int] -> Permutation)
    -> Arrows (Domains (Int -> [Int] -> Permutation)) (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Domains t) (S Word32)
    icodeN' Int -> [Int] -> Permutation
    Perm Int
    a [Int]
    b

      value :: Word32 -> R Permutation
    value = (Int -> [Int] -> Permutation)
    -> Word32 -> R (CoDomain (Int -> [Int] -> Permutation))
    forall t.
    (VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
    t -> Word32 -> R (CoDomain t)
    valueN Int -> [Int] -> Permutation
    Perm

    instance EmbPrj a => EmbPrj (Drop a) where
      icod_ :: Drop a -> S Word32
    icod_ (Drop Int
    a a
    b) = (Int -> a -> Drop a)
    -> Arrows (Domains (Int -> a -> Drop a)) (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Domains t) (S Word32)
    icodeN' Int -> a -> Drop a
    forall a. Int -> a -> Drop a
    Drop Int
    a a
    b

      value :: Word32 -> R (Drop a)
    value = (Int -> a -> Drop a) -> Word32 -> R (CoDomain (Int -> a -> Drop a))
    forall t.
    (VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
    t -> Word32 -> R (CoDomain t)
    valueN Int -> a -> Drop a
    forall a. Int -> a -> Drop a
    Drop

    instance EmbPrj a => EmbPrj (Elim' a) where
      icod_ :: Elim' a -> S Word32
    icod_ (Apply Arg a
    a)      = (Arg a -> Elim' a)
    -> Arrows (Domains (Arg a -> Elim' a)) (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Domains t) (S Word32)
    icodeN' Arg a -> Elim' a
    forall a. Arg a -> Elim' a
    Apply Arg a
    a
      icod_ (IApply a
    x a
    y a
    a) = Word32
    -> (a -> a -> a -> Elim' a)
    -> Arrows (Domains (a -> a -> a -> Elim' a)) (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    Word32 -> t -> Arrows (Domains t) (S Word32)
    icodeN Word32
    0 a -> a -> a -> Elim' a
    forall a. a -> a -> a -> Elim' a
    IApply a
    x a
    y a
    a
      icod_ (Proj ProjOrigin
    a QName
    b)     = Word32
    -> (ProjOrigin -> QName -> Elim' (ZonkAny 22))
    -> Arrows
         (Domains (ProjOrigin -> QName -> Elim' (ZonkAny 22))) (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    Word32 -> t -> Arrows (Domains t) (S Word32)
    icodeN Word32
    0 ProjOrigin -> QName -> Elim' (ZonkAny 22)
    forall a. ProjOrigin -> QName -> Elim' a
    Proj ProjOrigin
    a QName
    b

      value :: Word32 -> R (Elim' a)
    value = ([Word32] -> R (Elim' a)) -> Word32 -> R (Elim' a)
    forall a. EmbPrj a => ([Word32] -> R a) -> Word32 -> R a
    vcase [Word32] -> R (Elim' a)
    forall {a}. EmbPrj a => [Word32] -> R (Elim' a)
    valu where
        valu :: [Word32] -> R (Elim' a)
    valu [Word32
    a]       = (Arg a -> Elim' a)
    -> Arrows
         (Constant Word32 (Domains (Arg a -> Elim' a)))
         (R (CoDomain (Arg a -> Elim' a)))
    forall t.
    (VALU t (IsBase t),
     StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
    valuN Arg a -> Elim' a
    forall a. Arg a -> Elim' a
    Apply Word32
    a
        valu [Word32
    0,Word32
    x,Word32
    y,Word32
    a] = (a -> a -> a -> Elim' a)
    -> Arrows
         (Constant Word32 (Domains (a -> a -> a -> Elim' a)))
         (R (CoDomain (a -> a -> a -> Elim' a)))
    forall t.
    (VALU t (IsBase t),
     StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
    valuN a -> a -> a -> Elim' a
    forall a. a -> a -> a -> Elim' a
    IApply Word32
    x Word32
    y Word32
    a
        valu [Word32
    0, Word32
    a, Word32
    b] = (ProjOrigin -> QName -> Elim' a)
    -> Arrows
         (Constant Word32 (Domains (ProjOrigin -> QName -> Elim' a)))
         (R (CoDomain (ProjOrigin -> QName -> Elim' a)))
    forall t.
    (VALU t (IsBase t),
     StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
    valuN ProjOrigin -> QName -> Elim' a
    forall a. ProjOrigin -> QName -> Elim' a
    Proj Word32
    a Word32
    b
        valu [Word32]
    _         = R (Elim' a)
    forall a. R a
    malformed

    instance EmbPrj I.DataOrRecord where
      icod_ :: DataOrRecord -> S Word32
    icod_ = \case
        DataOrRecord
    IsData      -> DataOrRecord' (ZonkAny 21)
    -> Arrows (Domains (DataOrRecord' (ZonkAny 21))) (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Domains t) (S Word32)
    icodeN' DataOrRecord' (ZonkAny 21)
    forall p. DataOrRecord' p
    IsData
        IsRecord PatternOrCopattern
    pm -> (PatternOrCopattern -> DataOrRecord)
    -> Arrows (Domains (PatternOrCopattern -> DataOrRecord)) (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Domains t) (S Word32)
    icodeN' PatternOrCopattern -> DataOrRecord
    forall p. p -> DataOrRecord' p
    IsRecord PatternOrCopattern
    pm

      value :: Word32 -> R DataOrRecord
    value = ([Word32] -> R DataOrRecord) -> Word32 -> R DataOrRecord
    forall a. EmbPrj a => ([Word32] -> R a) -> Word32 -> R a
    vcase (([Word32] -> R DataOrRecord) -> Word32 -> R DataOrRecord)
    -> ([Word32] -> R DataOrRecord) -> Word32 -> R DataOrRecord
    forall a b. (a -> b) -> a -> b
    $ \case
        []   -> DataOrRecord
    -> Arrows
         (Constant Word32 (Domains DataOrRecord))
         (R (CoDomain DataOrRecord))
    forall t.
    (VALU t (IsBase t),
     StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
    valuN DataOrRecord
    forall p. DataOrRecord' p
    IsData
        [Word32
    pm] -> (PatternOrCopattern -> DataOrRecord)
    -> Arrows
         (Constant Word32 (Domains (PatternOrCopattern -> DataOrRecord)))
         (R (CoDomain (PatternOrCopattern -> DataOrRecord)))
    forall t.
    (VALU t (IsBase t),
     StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
    valuN PatternOrCopattern -> DataOrRecord
    forall p. p -> DataOrRecord' p
    IsRecord Word32
    pm
        [Word32]
    _    -> R DataOrRecord
    forall a. R a
    malformed

    instance EmbPrj I.ConHead where
      icod_ :: ConHead -> S Word32
    icod_ (ConHead QName
    a DataOrRecord
    b Induction
    c [Arg QName]
    d) = (QName -> DataOrRecord -> Induction -> [Arg QName] -> ConHead)
    -> Arrows
         (Domains
            (QName -> DataOrRecord -> Induction -> [Arg QName] -> ConHead))
         (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Domains t) (S Word32)
    icodeN' QName -> DataOrRecord -> Induction -> [Arg QName] -> ConHead
    ConHead QName
    a DataOrRecord
    b Induction
    c [Arg QName]
    d

      value :: Word32 -> R ConHead
    value = (QName -> DataOrRecord -> Induction -> [Arg QName] -> ConHead)
    -> Word32
    -> R (CoDomain
            (QName -> DataOrRecord -> Induction -> [Arg QName] -> ConHead))
    forall t.
    (VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
    t -> Word32 -> R (CoDomain t)
    valueN QName -> DataOrRecord -> Induction -> [Arg QName] -> ConHead
    ConHead

    instance (EmbPrj a) => EmbPrj (I.Type' a) where
      icod_ :: Type' a -> S Word32
    icod_ (El Sort' Term
    a a
    b) = (Sort' Term -> a -> Type' a)
    -> Arrows (Domains (Sort' Term -> a -> Type' a)) (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Domains t) (S Word32)
    icodeN' Sort' Term -> a -> Type' a
    forall t a. Sort' t -> a -> Type'' t a
    El Sort' Term
    a a
    b

      value :: Word32 -> R (Type' a)
    value = (Sort' Term -> a -> Type' a)
    -> Word32 -> R (CoDomain (Sort' Term -> a -> Type' a))
    forall t.
    (VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
    t -> Word32 -> R (CoDomain t)
    valueN Sort' Term -> a -> Type' a
    forall t a. Sort' t -> a -> Type'' t a
    El

    instance EmbPrj a => EmbPrj (I.Abs a) where
      icod_ :: Abs a -> S Word32
    icod_ (NoAbs ArgName
    a a
    b) = Word32
    -> (ArgName -> a -> Abs a)
    -> Arrows (Domains (ArgName -> a -> Abs a)) (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    Word32 -> t -> Arrows (Domains t) (S Word32)
    icodeN Word32
    0 ArgName -> a -> Abs a
    forall a. ArgName -> a -> Abs a
    NoAbs ArgName
    a a
    b
      icod_ (Abs ArgName
    a a
    b)   = (ArgName -> a -> Abs a)
    -> Arrows (Domains (ArgName -> a -> Abs a)) (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Domains t) (S Word32)
    icodeN' ArgName -> a -> Abs a
    forall a. ArgName -> a -> Abs a
    Abs ArgName
    a a
    b

      value :: Word32 -> R (Abs a)
    value = ([Word32] -> R (Abs a)) -> Word32 -> R (Abs a)
    forall a. EmbPrj a => ([Word32] -> R a) -> Word32 -> R a
    vcase [Word32] -> R (Abs a)
    forall {a}. EmbPrj a => [Word32] -> R (Abs a)
    valu where
        valu :: [Word32] -> R (Abs a)
    valu [Word32
    a, Word32
    b]    = (ArgName -> a -> Abs a)
    -> Arrows
         (Constant Word32 (Domains (ArgName -> a -> Abs a)))
         (R (CoDomain (ArgName -> a -> Abs a)))
    forall t.
    (VALU t (IsBase t),
     StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
    valuN ArgName -> a -> Abs a
    forall a. ArgName -> a -> Abs a
    Abs Word32
    a Word32
    b
        valu [Word32
    0, Word32
    a, Word32
    b] = (ArgName -> a -> Abs a)
    -> Arrows
         (Constant Word32 (Domains (ArgName -> a -> Abs a)))
         (R (CoDomain (ArgName -> a -> Abs a)))
    forall t.
    (VALU t (IsBase t),
     StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
    valuN ArgName -> a -> Abs a
    forall a. ArgName -> a -> Abs a
    NoAbs Word32
    a Word32
    b
        valu [Word32]
    _         = R (Abs a)
    forall a. R a
    malformed

    instance EmbPrj I.Term where
      icod_ :: Term -> S Word32
    icod_ (Var     Int
    a []) = (Int -> Term) -> Arrows (Domains (Int -> Term)) (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Domains t) (S Word32)
    icodeN' (\ Int
    a -> Int -> Elims -> Term
    Var Int
    a []) Int
    a
      icod_ (Var      Int
    a Elims
    b) = Word32
    -> (Int -> Elims -> Term)
    -> Arrows (Domains (Int -> Elims -> Term)) (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    Word32 -> t -> Arrows (Domains t) (S Word32)
    icodeN Word32
    0 Int -> Elims -> Term
    Var Int
    a Elims
    b
      icod_ (Lam      ArgInfo
    a Abs Term
    b) = Word32
    -> (ArgInfo -> Abs Term -> Term)
    -> Arrows (Domains (ArgInfo -> Abs Term -> Term)) (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    Word32 -> t -> Arrows (Domains t) (S Word32)
    icodeN Word32
    1 ArgInfo -> Abs Term -> Term
    Lam ArgInfo
    a Abs Term
    b
      icod_ (Lit      Literal
    a  ) = Word32
    -> (Literal -> Term)
    -> Arrows (Domains (Literal -> Term)) (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    Word32 -> t -> Arrows (Domains t) (S Word32)
    icodeN Word32
    2 Literal -> Term
    Lit Literal
    a
      icod_ (Def      QName
    a Elims
    b) = Word32
    -> (QName -> Elims -> Term)
    -> Arrows (Domains (QName -> Elims -> Term)) (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    Word32 -> t -> Arrows (Domains t) (S Word32)
    icodeN Word32
    3 QName -> Elims -> Term
    Def QName
    a Elims
    b
      icod_ (Con    ConHead
    a ConInfo
    b Elims
    c) = Word32
    -> (ConHead -> ConInfo -> Elims -> Term)
    -> Arrows
         (Domains (ConHead -> ConInfo -> Elims -> Term)) (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    Word32 -> t -> Arrows (Domains t) (S Word32)
    icodeN Word32
    4 ConHead -> ConInfo -> Elims -> Term
    Con ConHead
    a ConInfo
    b Elims
    c
      icod_ (Pi       Dom' Term Type
    a Abs Type
    b) = Word32
    -> (Dom' Term Type -> Abs Type -> Term)
    -> Arrows (Domains (Dom' Term Type -> Abs Type -> Term)) (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    Word32 -> t -> Arrows (Domains t) (S Word32)
    icodeN Word32
    5 Dom' Term Type -> Abs Type -> Term
    Pi Dom' Term Type
    a Abs Type
    b
      icod_ (MetaV    MetaId
    a Elims
    b) = Word32
    -> (MetaId -> Elims -> Term)
    -> Arrows (Domains (MetaId -> Elims -> Term)) (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    Word32 -> t -> Arrows (Domains t) (S Word32)
    icodeN Word32
    6 MetaId -> Elims -> Term
    MetaV MetaId
    a Elims
    b
      icod_ (Sort     Sort' Term
    a  ) = Word32
    -> (Sort' Term -> Term)
    -> Arrows (Domains (Sort' Term -> Term)) (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    Word32 -> t -> Arrows (Domains t) (S Word32)
    icodeN Word32
    7 Sort' Term -> Term
    Sort Sort' Term
    a
      icod_ (DontCare Term
    a  ) = Word32
    -> (Term -> Term) -> Arrows (Domains (Term -> Term)) (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    Word32 -> t -> Arrows (Domains t) (S Word32)
    icodeN Word32
    8 Term -> Term
    DontCare Term
    a
      icod_ (Level    Level
    a  ) = Word32
    -> (Level -> Term) -> Arrows (Domains (Level -> Term)) (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    Word32 -> t -> Arrows (Domains t) (S Word32)
    icodeN Word32
    9 Level -> Term
    Level Level
    a
      icod_ (Dummy    ArgName
    a Elims
    b) = Word32
    -> (ArgName -> Elims -> Term)
    -> Arrows (Domains (ArgName -> Elims -> Term)) (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    Word32 -> t -> Arrows (Domains t) (S Word32)
    icodeN Word32
    10 ArgName -> Elims -> Term
    Dummy ArgName
    a Elims
    b

      value :: Word32 -> R Term
    value = ([Word32] -> R Term) -> Word32 -> R Term
    forall a. EmbPrj a => ([Word32] -> R a) -> Word32 -> R a
    vcase [Word32] -> R Term
    valu where
        valu :: [Word32] -> R Term
    valu [Word32
    a]       = (Int -> Term)
    -> Arrows
         (Constant Word32 (Domains (Int -> Term)))
         (R (CoDomain (Int -> Term)))
    forall t.
    (VALU t (IsBase t),
     StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
    valuN Int -> Term
    var   Word32
    a
        valu [Word32
    0, Word32
    a, Word32
    b] = (Int -> Elims -> Term)
    -> Arrows
         (Constant Word32 (Domains (Int -> Elims -> Term)))
         (R (CoDomain (Int -> Elims -> Term)))
    forall t.
    (VALU t (IsBase t),
     StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
    valuN Int -> Elims -> Term
    Var   Word32
    a Word32
    b
        valu [Word32
    1, Word32
    a, Word32
    b] = (ArgInfo -> Abs Term -> Term)
    -> Arrows
         (Constant Word32 (Domains (ArgInfo -> Abs Term -> Term)))
         (R (CoDomain (ArgInfo -> Abs Term -> Term)))
    forall t.
    (VALU t (IsBase t),
     StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
    valuN ArgInfo -> Abs Term -> Term
    Lam   Word32
    a Word32
    b
        valu [Word32
    2, Word32
    a]    = (Literal -> Term)
    -> Arrows
         (Constant Word32 (Domains (Literal -> Term)))
         (R (CoDomain (Literal -> Term)))
    forall t.
    (VALU t (IsBase t),
     StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
    valuN Literal -> Term
    Lit   Word32
    a
        valu [Word32
    3, Word32
    a, Word32
    b] = (QName -> Elims -> Term)
    -> Arrows
         (Constant Word32 (Domains (QName -> Elims -> Term)))
         (R (CoDomain (QName -> Elims -> Term)))
    forall t.
    (VALU t (IsBase t),
     StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
    valuN QName -> Elims -> Term
    Def   Word32
    a Word32
    b
        valu [Word32
    4, Word32
    a, Word32
    b, Word32
    c] = (ConHead -> ConInfo -> Elims -> Term)
    -> Arrows
         (Constant Word32 (Domains (ConHead -> ConInfo -> Elims -> Term)))
         (R (CoDomain (ConHead -> ConInfo -> Elims -> Term)))
    forall t.
    (VALU t (IsBase t),
     StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
    valuN ConHead -> ConInfo -> Elims -> Term
    Con Word32
    a Word32
    b Word32
    c
        valu [Word32
    5, Word32
    a, Word32
    b] = (Dom' Term Type -> Abs Type -> Term)
    -> Arrows
         (Constant Word32 (Domains (Dom' Term Type -> Abs Type -> Term)))
         (R (CoDomain (Dom' Term Type -> Abs Type -> Term)))
    forall t.
    (VALU t (IsBase t),
     StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
    valuN Dom' Term Type -> Abs Type -> Term
    Pi    Word32
    a Word32
    b
        valu [Word32
    6, Word32
    a, Word32
    b] = (MetaId -> Elims -> Term)
    -> Arrows
         (Constant Word32 (Domains (MetaId -> Elims -> Term)))
         (R (CoDomain (MetaId -> Elims -> Term)))
    forall t.
    (VALU t (IsBase t),
     StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
    valuN MetaId -> Elims -> Term
    MetaV Word32
    a Word32
    b
        valu [Word32
    7, Word32
    a]    = (Sort' Term -> Term)
    -> Arrows
         (Constant Word32 (Domains (Sort' Term -> Term)))
         (R (CoDomain (Sort' Term -> Term)))
    forall t.
    (VALU t (IsBase t),
     StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
    valuN Sort' Term -> Term
    Sort  Word32
    a
        valu [Word32
    8, Word32
    a]    = (Term -> Term)
    -> Arrows
         (Constant Word32 (Domains (Term -> Term)))
         (R (CoDomain (Term -> Term)))
    forall t.
    (VALU t (IsBase t),
     StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
    valuN Term -> Term
    DontCare Word32
    a
        valu [Word32
    9, Word32
    a]    = (Level -> Term)
    -> Arrows
         (Constant Word32 (Domains (Level -> Term)))
         (R (CoDomain (Level -> Term)))
    forall t.
    (VALU t (IsBase t),
     StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
    valuN Level -> Term
    Level Word32
    a
        valu [Word32
    10, Word32
    a, Word32
    b] = (ArgName -> Elims -> Term)
    -> Arrows
         (Constant Word32 (Domains (ArgName -> Elims -> Term)))
         (R (CoDomain (ArgName -> Elims -> Term)))
    forall t.
    (VALU t (IsBase t),
     StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
    valuN ArgName -> Elims -> Term
    Dummy Word32
    a Word32
    b
        valu [Word32]
    _         = R Term
    forall a. R a
    malformed

    instance EmbPrj Level where
      icod_ :: Level -> S Word32
    icod_ (Max Integer
    a [PlusLevel' Term]
    b) = (Integer -> [PlusLevel' Term] -> Level)
    -> Arrows
         (Domains (Integer -> [PlusLevel' Term] -> Level)) (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Domains t) (S Word32)
    icodeN' Integer -> [PlusLevel' Term] -> Level
    forall t. Integer -> [PlusLevel' t] -> Level' t
    Max Integer
    a [PlusLevel' Term]
    b

      value :: Word32 -> R Level
    value = (Integer -> [PlusLevel' Term] -> Level)
    -> Word32 -> R (CoDomain (Integer -> [PlusLevel' Term] -> Level))
    forall t.
    (VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
    t -> Word32 -> R (CoDomain t)
    valueN Integer -> [PlusLevel' Term] -> Level
    forall t. Integer -> [PlusLevel' t] -> Level' t
    Max

    instance EmbPrj PlusLevel where
      icod_ :: PlusLevel' Term -> S Word32
    icod_ (Plus Integer
    a Term
    b) = (Integer -> Term -> PlusLevel' Term)
    -> Arrows (Domains (Integer -> Term -> PlusLevel' Term)) (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Domains t) (S Word32)
    icodeN' Integer -> Term -> PlusLevel' Term
    forall t. Integer -> t -> PlusLevel' t
    Plus Integer
    a Term
    b

      value :: Word32 -> R (PlusLevel' Term)
    value = (Integer -> Term -> PlusLevel' Term)
    -> Word32 -> R (CoDomain (Integer -> Term -> PlusLevel' Term))
    forall t.
    (VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
    t -> Word32 -> R (CoDomain t)
    valueN Integer -> Term -> PlusLevel' Term
    forall t. Integer -> t -> PlusLevel' t
    Plus

    instance EmbPrj IsFibrant where
      icod_ :: IsFibrant -> S Word32
    icod_ IsFibrant
    IsFibrant = Word32 -> S Word32
    forall a. a -> ReaderT Dict IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Word32
    0
      icod_ IsFibrant
    IsStrict  = Word32 -> S Word32
    forall a. a -> ReaderT Dict IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Word32
    1

      value :: Word32 -> R IsFibrant
    value Word32
    0 = IsFibrant -> R IsFibrant
    forall a. a -> StateT St IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return IsFibrant
    IsFibrant
      value Word32
    1 = IsFibrant -> R IsFibrant
    forall a. a -> StateT St IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return IsFibrant
    IsStrict
      value Word32
    _ = R IsFibrant
    forall a. R a
    malformed

    instance EmbPrj Univ where

    instance EmbPrj I.Sort where
      icod_ :: Sort' Term -> S Word32
    icod_ = \case
        Univ Univ
    a Level
    b     -> Word32
    -> (Univ -> Level -> Sort' Term)
    -> Arrows (Domains (Univ -> Level -> Sort' Term)) (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    Word32 -> t -> Arrows (Domains t) (S Word32)
    icodeN Word32
    0  Univ -> Level -> Sort' Term
    forall t. Univ -> Level' t -> Sort' t
    Univ Univ
    a Level
    b
        Sort' Term
    SizeUniv     -> Word32
    -> Sort' (ZonkAny 15)
    -> Arrows (Domains (Sort' (ZonkAny 15))) (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    Word32 -> t -> Arrows (Domains t) (S Word32)
    icodeN Word32
    2  Sort' (ZonkAny 15)
    forall t. Sort' t
    SizeUniv
        Inf Univ
    a Integer
    b      -> Word32
    -> (Univ -> Integer -> Sort' (ZonkAny 16))
    -> Arrows
         (Domains (Univ -> Integer -> Sort' (ZonkAny 16))) (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    Word32 -> t -> Arrows (Domains t) (S Word32)
    icodeN Word32
    3  Univ -> Integer -> Sort' (ZonkAny 16)
    forall t. Univ -> Integer -> Sort' t
    Inf Univ
    a Integer
    b
        PiSort Dom' Term Term
    a Sort' Term
    b Abs (Sort' Term)
    c -> Word32
    -> (Dom' Term Term -> Sort' Term -> Abs (Sort' Term) -> Sort' Term)
    -> Arrows
         (Domains
            (Dom' Term Term -> Sort' Term -> Abs (Sort' Term) -> Sort' Term))
         (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    Word32 -> t -> Arrows (Domains t) (S Word32)
    icodeN Word32
    4  Dom' Term Term -> Sort' Term -> Abs (Sort' Term) -> Sort' Term
    forall t. Dom' t t -> Sort' t -> Abs (Sort' t) -> Sort' t
    PiSort Dom' Term Term
    a Sort' Term
    b Abs (Sort' Term)
    c
        FunSort Sort' Term
    a Sort' Term
    b  -> Word32
    -> (Sort' Term -> Sort' Term -> Sort' Term)
    -> Arrows
         (Domains (Sort' Term -> Sort' Term -> Sort' Term)) (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    Word32 -> t -> Arrows (Domains t) (S Word32)
    icodeN Word32
    5  Sort' Term -> Sort' Term -> Sort' Term
    forall t. Sort' t -> Sort' t -> Sort' t
    FunSort Sort' Term
    a Sort' Term
    b
        UnivSort Sort' Term
    a   -> Word32
    -> (Sort' Term -> Sort' Term)
    -> Arrows (Domains (Sort' Term -> Sort' Term)) (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    Word32 -> t -> Arrows (Domains t) (S Word32)
    icodeN Word32
    6  Sort' Term -> Sort' Term
    forall t. Sort' t -> Sort' t
    UnivSort Sort' Term
    a
        DefS QName
    a Elims
    b     -> Word32
    -> (QName -> Elims -> Sort' Term)
    -> Arrows (Domains (QName -> Elims -> Sort' Term)) (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    Word32 -> t -> Arrows (Domains t) (S Word32)
    icodeN Word32
    7  QName -> Elims -> Sort' Term
    forall t. QName -> [Elim' t] -> Sort' t
    DefS QName
    a Elims
    b
        Sort' Term
    LockUniv     -> Word32
    -> Sort' (ZonkAny 17)
    -> Arrows (Domains (Sort' (ZonkAny 17))) (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    Word32 -> t -> Arrows (Domains t) (S Word32)
    icodeN Word32
    9  Sort' (ZonkAny 17)
    forall t. Sort' t
    LockUniv
        Sort' Term
    IntervalUniv -> Word32
    -> Sort' (ZonkAny 18)
    -> Arrows (Domains (Sort' (ZonkAny 18))) (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    Word32 -> t -> Arrows (Domains t) (S Word32)
    icodeN Word32
    10 Sort' (ZonkAny 18)
    forall t. Sort' t
    IntervalUniv
        MetaS MetaId
    a Elims
    b    -> Word32
    -> (MetaId -> Elims -> Sort' Term)
    -> Arrows (Domains (MetaId -> Elims -> Sort' Term)) (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    Word32 -> t -> Arrows (Domains t) (S Word32)
    icodeN Word32
    11 MetaId -> Elims -> Sort' Term
    forall t. MetaId -> [Elim' t] -> Sort' t
    MetaS MetaId
    a Elims
    b
        DummyS ArgName
    s     -> Word32
    -> (ArgName -> Sort' (ZonkAny 19))
    -> Arrows (Domains (ArgName -> Sort' (ZonkAny 19))) (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    Word32 -> t -> Arrows (Domains t) (S Word32)
    icodeN Word32
    12 ArgName -> Sort' (ZonkAny 19)
    forall t. ArgName -> Sort' t
    DummyS ArgName
    s
        Sort' Term
    LevelUniv    -> Word32
    -> Sort' (ZonkAny 20)
    -> Arrows (Domains (Sort' (ZonkAny 20))) (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    Word32 -> t -> Arrows (Domains t) (S Word32)
    icodeN Word32
    13 Sort' (ZonkAny 20)
    forall t. Sort' t
    LevelUniv

      value :: Word32 -> R (Sort' Term)
    value = ([Word32] -> R (Sort' Term)) -> Word32 -> R (Sort' Term)
    forall a. EmbPrj a => ([Word32] -> R a) -> Word32 -> R a
    vcase [Word32] -> R (Sort' Term)
    forall {t}.
    (EmbPrj t, EmbPrj (Dom' t t), EmbPrj (Level' t),
     EmbPrj (Sort' t)) =>
    [Word32] -> R (Sort' t)
    valu where
        valu :: [Word32] -> R (Sort' t)
    valu [Word32
    0, Word32
    a, Word32
    b] = (Univ -> Level' t -> Sort' t)
    -> Arrows
         (Constant Word32 (Domains (Univ -> Level' t -> Sort' t)))
         (R (CoDomain (Univ -> Level' t -> Sort' t)))
    forall t.
    (VALU t (IsBase t),
     StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
    valuN Univ -> Level' t -> Sort' t
    forall t. Univ -> Level' t -> Sort' t
    Univ Word32
    a Word32
    b
        valu [Word32
    2]       = Sort' t
    -> Arrows
         (Constant Word32 (Domains (Sort' t))) (R (CoDomain (Sort' t)))
    forall t.
    (VALU t (IsBase t),
     StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
    valuN Sort' t
    forall t. Sort' t
    SizeUniv
        valu [Word32
    3, Word32
    a, Word32
    b] = (Univ -> Integer -> Sort' t)
    -> Arrows
         (Constant Word32 (Domains (Univ -> Integer -> Sort' t)))
         (R (CoDomain (Univ -> Integer -> Sort' t)))
    forall t.
    (VALU t (IsBase t),
     StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
    valuN Univ -> Integer -> Sort' t
    forall t. Univ -> Integer -> Sort' t
    Inf Word32
    a Word32
    b
        valu [Word32
    4, Word32
    a, Word32
    b, Word32
    c] = (Dom' t t -> Sort' t -> Abs (Sort' t) -> Sort' t)
    -> Arrows
         (Constant
            Word32 (Domains (Dom' t t -> Sort' t -> Abs (Sort' t) -> Sort' t)))
         (R (CoDomain (Dom' t t -> Sort' t -> Abs (Sort' t) -> Sort' t)))
    forall t.
    (VALU t (IsBase t),
     StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
    valuN Dom' t t -> Sort' t -> Abs (Sort' t) -> Sort' t
    forall t. Dom' t t -> Sort' t -> Abs (Sort' t) -> Sort' t
    PiSort Word32
    a Word32
    b Word32
    c
        valu [Word32
    5, Word32
    a, Word32
    b] = (Sort' t -> Sort' t -> Sort' t)
    -> Arrows
         (Constant Word32 (Domains (Sort' t -> Sort' t -> Sort' t)))
         (R (CoDomain (Sort' t -> Sort' t -> Sort' t)))
    forall t.
    (VALU t (IsBase t),
     StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
    valuN Sort' t -> Sort' t -> Sort' t
    forall t. Sort' t -> Sort' t -> Sort' t
    FunSort Word32
    a Word32
    b
        valu [Word32
    6, Word32
    a]    = (Sort' t -> Sort' t)
    -> Arrows
         (Constant Word32 (Domains (Sort' t -> Sort' t)))
         (R (CoDomain (Sort' t -> Sort' t)))
    forall t.
    (VALU t (IsBase t),
     StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
    valuN Sort' t -> Sort' t
    forall t. Sort' t -> Sort' t
    UnivSort Word32
    a
        valu [Word32
    7, Word32
    a, Word32
    b] = (QName -> [Elim' t] -> Sort' t)
    -> Arrows
         (Constant Word32 (Domains (QName -> [Elim' t] -> Sort' t)))
         (R (CoDomain (QName -> [Elim' t] -> Sort' t)))
    forall t.
    (VALU t (IsBase t),
     StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
    valuN QName -> [Elim' t] -> Sort' t
    forall t. QName -> [Elim' t] -> Sort' t
    DefS Word32
    a Word32
    b
        valu [Word32
    9]       = Sort' t
    -> Arrows
         (Constant Word32 (Domains (Sort' t))) (R (CoDomain (Sort' t)))
    forall t.
    (VALU t (IsBase t),
     StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
    valuN Sort' t
    forall t. Sort' t
    LockUniv
        valu [Word32
    10]      = Sort' t
    -> Arrows
         (Constant Word32 (Domains (Sort' t))) (R (CoDomain (Sort' t)))
    forall t.
    (VALU t (IsBase t),
     StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
    valuN Sort' t
    forall t. Sort' t
    IntervalUniv
        valu [Word32
    11, Word32
    a, Word32
    b] = (MetaId -> [Elim' t] -> Sort' t)
    -> Arrows
         (Constant Word32 (Domains (MetaId -> [Elim' t] -> Sort' t)))
         (R (CoDomain (MetaId -> [Elim' t] -> Sort' t)))
    forall t.
    (VALU t (IsBase t),
     StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
    valuN MetaId -> [Elim' t] -> Sort' t
    forall t. MetaId -> [Elim' t] -> Sort' t
    MetaS Word32
    a Word32
    b
        valu [Word32
    12, Word32
    s]   = (ArgName -> Sort' t)
    -> Arrows
         (Constant Word32 (Domains (ArgName -> Sort' t)))
         (R (CoDomain (ArgName -> Sort' t)))
    forall t.
    (VALU t (IsBase t),
     StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
    valuN ArgName -> Sort' t
    forall t. ArgName -> Sort' t
    DummyS Word32
    s
        valu [Word32
    13]      = Sort' t
    -> Arrows
         (Constant Word32 (Domains (Sort' t))) (R (CoDomain (Sort' t)))
    forall t.
    (VALU t (IsBase t),
     StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
    valuN Sort' t
    forall t. Sort' t
    LevelUniv
        valu [Word32]
    _         = R (Sort' t)
    forall a. R a
    malformed

    instance EmbPrj DisplayForm where
      icod_ :: DisplayForm -> S Word32
    icod_ (Display Int
    a Elims
    b DisplayTerm
    c) = (Int -> Elims -> DisplayTerm -> DisplayForm)
    -> Arrows
         (Domains (Int -> Elims -> DisplayTerm -> DisplayForm)) (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Domains t) (S Word32)
    icodeN' Int -> Elims -> DisplayTerm -> DisplayForm
    Display Int
    a Elims
    b DisplayTerm
    c

      value :: Word32 -> R DisplayForm
    value = (Int -> Elims -> DisplayTerm -> DisplayForm)
    -> Word32
    -> R (CoDomain (Int -> Elims -> DisplayTerm -> DisplayForm))
    forall t.
    (VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
    t -> Word32 -> R (CoDomain t)
    valueN Int -> Elims -> DisplayTerm -> DisplayForm
    Display

    instance EmbPrj a => EmbPrj (Open a) where
      icod_ :: Open a -> S Word32
    icod_ (OpenThing CheckpointId
    a Map CheckpointId Substitution
    b ModuleNameHash
    c a
    d) = (CheckpointId
     -> Map CheckpointId Substitution -> ModuleNameHash -> a -> Open a)
    -> Arrows
         (Domains
            (CheckpointId
             -> Map CheckpointId Substitution -> ModuleNameHash -> a -> Open a))
         (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Domains t) (S Word32)
    icodeN' CheckpointId
    -> Map CheckpointId Substitution -> ModuleNameHash -> a -> Open a
    forall a.
    CheckpointId
    -> Map CheckpointId Substitution -> ModuleNameHash -> a -> Open a
    OpenThing CheckpointId
    a Map CheckpointId Substitution
    b ModuleNameHash
    c a
    d

      value :: Word32 -> R (Open a)
    value = (CheckpointId
     -> Map CheckpointId Substitution -> ModuleNameHash -> a -> Open a)
    -> Word32
    -> R (CoDomain
            (CheckpointId
             -> Map CheckpointId Substitution -> ModuleNameHash -> a -> Open a))
    forall t.
    (VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
    t -> Word32 -> R (CoDomain t)
    valueN CheckpointId
    -> Map CheckpointId Substitution -> ModuleNameHash -> a -> Open a
    forall a.
    CheckpointId
    -> Map CheckpointId Substitution -> ModuleNameHash -> a -> Open a
    OpenThing

    instance EmbPrj CheckpointId where
      icod_ :: CheckpointId -> S Word32
    icod_ (CheckpointId Int
    a) = Int -> S Word32
    forall a. EmbPrj a => a -> S Word32
    icode Int
    a
      value :: Word32 -> R CheckpointId
    value Word32
    n                = Int -> CheckpointId
    CheckpointId (Int -> CheckpointId) -> StateT St IO Int -> R CheckpointId
    forall (m :: * -> *) a b. Monad m => (a -> b) -> m a -> m b
    <$!> Word32 -> StateT St IO Int
    forall a. EmbPrj a => Word32 -> R a
    value Word32
    n

    instance EmbPrj DisplayTerm where
      icod_ :: DisplayTerm -> S Word32
    icod_ (DTerm'   Term
    a Elims
    b)   = (Term -> Elims -> DisplayTerm)
    -> Arrows (Domains (Term -> Elims -> DisplayTerm)) (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Domains t) (S Word32)
    icodeN' Term -> Elims -> DisplayTerm
    DTerm' Term
    a Elims
    b
      icod_ (DDot'    Term
    a Elims
    b)   = Word32
    -> (Term -> Elims -> DisplayTerm)
    -> Arrows (Domains (Term -> Elims -> DisplayTerm)) (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    Word32 -> t -> Arrows (Domains t) (S Word32)
    icodeN Word32
    1 Term -> Elims -> DisplayTerm
    DDot' Term
    a Elims
    b
      icod_ (DCon     ConHead
    a ConInfo
    b [Arg DisplayTerm]
    c) = Word32
    -> (ConHead -> ConInfo -> [Arg DisplayTerm] -> DisplayTerm)
    -> Arrows
         (Domains (ConHead -> ConInfo -> [Arg DisplayTerm] -> DisplayTerm))
         (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    Word32 -> t -> Arrows (Domains t) (S Word32)
    icodeN Word32
    2 ConHead -> ConInfo -> [Arg DisplayTerm] -> DisplayTerm
    DCon ConHead
    a ConInfo
    b [Arg DisplayTerm]
    c
      icod_ (DDef     QName
    a [Elim' DisplayTerm]
    b)   = Word32
    -> (QName -> [Elim' DisplayTerm] -> DisplayTerm)
    -> Arrows
         (Domains (QName -> [Elim' DisplayTerm] -> DisplayTerm)) (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    Word32 -> t -> Arrows (Domains t) (S Word32)
    icodeN Word32
    3 QName -> [Elim' DisplayTerm] -> DisplayTerm
    DDef QName
    a [Elim' DisplayTerm]
    b
      icod_ (DWithApp DisplayTerm
    a List1 DisplayTerm
    b Elims
    c) = Word32
    -> (DisplayTerm -> List1 DisplayTerm -> Elims -> DisplayTerm)
    -> Arrows
         (Domains
            (DisplayTerm -> List1 DisplayTerm -> Elims -> DisplayTerm))
         (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    Word32 -> t -> Arrows (Domains t) (S Word32)
    icodeN Word32
    4 DisplayTerm -> List1 DisplayTerm -> Elims -> DisplayTerm
    DWithApp DisplayTerm
    a List1 DisplayTerm
    b Elims
    c

      value :: Word32 -> R DisplayTerm
    value = ([Word32] -> R DisplayTerm) -> Word32 -> R DisplayTerm
    forall a. EmbPrj a => ([Word32] -> R a) -> Word32 -> R a
    vcase [Word32] -> R DisplayTerm
    valu where
        valu :: [Word32] -> R DisplayTerm
    valu [Word32
    a, Word32
    b]       = (Term -> Elims -> DisplayTerm)
    -> Arrows
         (Constant Word32 (Domains (Term -> Elims -> DisplayTerm)))
         (R (CoDomain (Term -> Elims -> DisplayTerm)))
    forall t.
    (VALU t (IsBase t),
     StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
    valuN Term -> Elims -> DisplayTerm
    DTerm' Word32
    a Word32
    b
        valu [Word32
    1, Word32
    a, Word32
    b]    = (Term -> Elims -> DisplayTerm)
    -> Arrows
         (Constant Word32 (Domains (Term -> Elims -> DisplayTerm)))
         (R (CoDomain (Term -> Elims -> DisplayTerm)))
    forall t.
    (VALU t (IsBase t),
     StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
    valuN Term -> Elims -> DisplayTerm
    DDot' Word32
    a Word32
    b
        valu [Word32
    2, Word32
    a, Word32
    b, Word32
    c] = (ConHead -> ConInfo -> [Arg DisplayTerm] -> DisplayTerm)
    -> Arrows
         (Constant
            Word32
            (Domains (ConHead -> ConInfo -> [Arg DisplayTerm] -> DisplayTerm)))
         (R (CoDomain
               (ConHead -> ConInfo -> [Arg DisplayTerm] -> DisplayTerm)))
    forall t.
    (VALU t (IsBase t),
     StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
    valuN ConHead -> ConInfo -> [Arg DisplayTerm] -> DisplayTerm
    DCon Word32
    a Word32
    b Word32
    c
        valu [Word32
    3, Word32
    a, Word32
    b]    = (QName -> [Elim' DisplayTerm] -> DisplayTerm)
    -> Arrows
         (Constant
            Word32 (Domains (QName -> [Elim' DisplayTerm] -> DisplayTerm)))
         (R (CoDomain (QName -> [Elim' DisplayTerm] -> DisplayTerm)))
    forall t.
    (VALU t (IsBase t),
     StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
    valuN QName -> [Elim' DisplayTerm] -> DisplayTerm
    DDef Word32
    a Word32
    b
        valu [Word32
    4, Word32
    a, Word32
    b, Word32
    c] = (DisplayTerm -> List1 DisplayTerm -> Elims -> DisplayTerm)
    -> Arrows
         (Constant
            Word32
            (Domains
               (DisplayTerm -> List1 DisplayTerm -> Elims -> DisplayTerm)))
         (R (CoDomain
               (DisplayTerm -> List1 DisplayTerm -> Elims -> DisplayTerm)))
    forall t.
    (VALU t (IsBase t),
     StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
    valuN DisplayTerm -> List1 DisplayTerm -> Elims -> DisplayTerm
    DWithApp Word32
    a Word32
    b Word32
    c
        valu [Word32]
    _            = R DisplayTerm
    forall a. R a
    malformed

    instance EmbPrj MutualId where
      icod_ :: MutualId -> S Word32
    icod_ (MutualId Word32
    a) = Word32 -> S Word32
    forall a. EmbPrj a => a -> S Word32
    icode Word32
    a
      value :: Word32 -> R MutualId
    value Word32
    n            = Word32 -> MutualId
    MutualId (Word32 -> MutualId) -> StateT St IO Word32 -> R MutualId
    forall (m :: * -> *) a b. Monad m => (a -> b) -> m a -> m b
    <$!> Word32 -> StateT St IO Word32
    forall a. EmbPrj a => Word32 -> R a
    value Word32
    n

    instance EmbPrj CompKit where
      icod_ :: CompKit -> S Word32
    icod_ (CompKit Maybe QName
    a Maybe QName
    b) = (Maybe QName -> Maybe QName -> CompKit)
    -> Arrows
         (Domains (Maybe QName -> Maybe QName -> CompKit)) (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Domains t) (S Word32)
    icodeN' Maybe QName -> Maybe QName -> CompKit
    CompKit Maybe QName
    a Maybe QName
    b
      value :: Word32 -> R CompKit
    value = (Maybe QName -> Maybe QName -> CompKit)
    -> Word32 -> R (CoDomain (Maybe QName -> Maybe QName -> CompKit))
    forall t.
    (VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
    t -> Word32 -> R (CoDomain t)
    valueN Maybe QName -> Maybe QName -> CompKit
    CompKit

    instance EmbPrj InstanceInfo where
      icod_ :: InstanceInfo -> S Word32
    icod_ (InstanceInfo QName
    a OverlapMode
    b) = (QName -> OverlapMode -> InstanceInfo)
    -> Arrows
         (Domains (QName -> OverlapMode -> InstanceInfo)) (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Domains t) (S Word32)
    icodeN' QName -> OverlapMode -> InstanceInfo
    InstanceInfo QName
    a OverlapMode
    b
      value :: Word32 -> R InstanceInfo
    value = (QName -> OverlapMode -> InstanceInfo)
    -> Word32 -> R (CoDomain (QName -> OverlapMode -> InstanceInfo))
    forall t.
    (VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
    t -> Word32 -> R (CoDomain t)
    valueN QName -> OverlapMode -> InstanceInfo
    InstanceInfo

    instance EmbPrj Definition where
      icod_ :: Definition -> S Word32
    icod_ (Defn ArgInfo
    a QName
    b Type
    c [Polarity]
    d [Occurrence]
    e [Maybe Name]
    f [LocalDisplayForm]
    g MutualId
    h CompiledRepresentation
    i Maybe InstanceInfo
    j Bool
    k Set QName
    l Bool
    m Bool
    n Bool
    o Blocked_
    blocked Language
    r Defn
    s) =
        (ArgInfo
     -> QName
     -> Type
     -> [Polarity]
     -> [Occurrence]
     -> [Maybe Name]
     -> [LocalDisplayForm]
     -> MutualId
     -> CompiledRepresentation
     -> Maybe InstanceInfo
     -> Bool
     -> Set QName
     -> Bool
     -> Bool
     -> Bool
     -> Blocked_
     -> Language
     -> Defn
     -> Definition)
    -> Arrows
         (Domains
            (ArgInfo
             -> QName
             -> Type
             -> [Polarity]
             -> [Occurrence]
             -> [Maybe Name]
             -> [LocalDisplayForm]
             -> MutualId
             -> CompiledRepresentation
             -> Maybe InstanceInfo
             -> Bool
             -> Set QName
             -> Bool
             -> Bool
             -> Bool
             -> Blocked_
             -> Language
             -> Defn
             -> Definition))
         (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Domains t) (S Word32)
    icodeN' ArgInfo
    -> QName
    -> Type
    -> [Polarity]
    -> [Occurrence]
    -> [Maybe Name]
    -> [LocalDisplayForm]
    -> MutualId
    -> CompiledRepresentation
    -> Maybe InstanceInfo
    -> Bool
    -> Set QName
    -> Bool
    -> Bool
    -> Bool
    -> Blocked_
    -> Language
    -> Defn
    -> Definition
    Defn ArgInfo
    a QName
    b (KillRangeT Type
    forall a. KillRange a => KillRangeT a
    P.killRange Type
    c) [Polarity]
    d [Occurrence]
    e [Maybe Name]
    f [LocalDisplayForm]
    g MutualId
    h CompiledRepresentation
    i Maybe InstanceInfo
    j Bool
    k Set QName
    l Bool
    m Bool
    n Bool
    o (Blocked_ -> Blocked_
    ossify Blocked_
    blocked) Language
    r Defn
    s
        where
          -- Andreas, 2024-01-02, issue #7044:
          -- After serialization, a definition can never be unblocked,
          -- since all metas are ossified.
          -- Thus, we turn any blocker into 'neverUnblock'.
          ossify :: Blocked_ -> Blocked_
          ossify :: Blocked_ -> Blocked_
    ossify = \case
            b :: Blocked_
    b@NotBlocked{} -> Blocked_
    b
            Blocked Blocker
    b () -> Blocker -> () -> Blocked_
    forall t a. Blocker -> a -> Blocked' t a
    Blocked Blocker
    neverUnblock ()
      value :: Word32 -> R Definition
    value = (ArgInfo
     -> QName
     -> Type
     -> [Polarity]
     -> [Occurrence]
     -> [Maybe Name]
     -> [LocalDisplayForm]
     -> MutualId
     -> CompiledRepresentation
     -> Maybe InstanceInfo
     -> Bool
     -> Set QName
     -> Bool
     -> Bool
     -> Bool
     -> Blocked_
     -> Language
     -> Defn
     -> Definition)
    -> Word32
    -> R (CoDomain
            (ArgInfo
             -> QName
             -> Type
             -> [Polarity]
             -> [Occurrence]
             -> [Maybe Name]
             -> [LocalDisplayForm]
             -> MutualId
             -> CompiledRepresentation
             -> Maybe InstanceInfo
             -> Bool
             -> Set QName
             -> Bool
             -> Bool
             -> Bool
             -> Blocked_
             -> Language
             -> Defn
             -> Definition))
    forall t.
    (VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
    t -> Word32 -> R (CoDomain t)
    valueN ArgInfo
    -> QName
    -> Type
    -> [Polarity]
    -> [Occurrence]
    -> [Maybe Name]
    -> [LocalDisplayForm]
    -> MutualId
    -> CompiledRepresentation
    -> Maybe InstanceInfo
    -> Bool
    -> Set QName
    -> Bool
    -> Bool
    -> Bool
    -> Blocked_
    -> Language
    -> Defn
    -> Definition
    Defn

    instance EmbPrj NotBlocked where
      icod_ :: NotBlocked -> S Word32
    icod_ NotBlocked
    ReallyNotBlocked = NotBlocked' (ZonkAny 11)
    -> Arrows (Domains (NotBlocked' (ZonkAny 11))) (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Domains t) (S Word32)
    icodeN' NotBlocked' (ZonkAny 11)
    forall t. NotBlocked' t
    ReallyNotBlocked
      icod_ (StuckOn Elim' Term
    a)      = Word32
    -> (Elim' Term -> NotBlocked)
    -> Arrows (Domains (Elim' Term -> NotBlocked)) (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    Word32 -> t -> Arrows (Domains t) (S Word32)
    icodeN Word32
    0 Elim' Term -> NotBlocked
    forall t. Elim' t -> NotBlocked' t
    StuckOn Elim' Term
    a
      icod_ NotBlocked
    Underapplied     = Word32
    -> NotBlocked' (ZonkAny 12)
    -> Arrows (Domains (NotBlocked' (ZonkAny 12))) (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    Word32 -> t -> Arrows (Domains t) (S Word32)
    icodeN Word32
    1 NotBlocked' (ZonkAny 12)
    forall t. NotBlocked' t
    Underapplied
      icod_ NotBlocked
    AbsurdMatch      = Word32
    -> NotBlocked' (ZonkAny 13)
    -> Arrows (Domains (NotBlocked' (ZonkAny 13))) (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    Word32 -> t -> Arrows (Domains t) (S Word32)
    icodeN Word32
    2 NotBlocked' (ZonkAny 13)
    forall t. NotBlocked' t
    AbsurdMatch
      icod_ (MissingClauses QName
    a) = Word32
    -> (QName -> NotBlocked' (ZonkAny 14))
    -> Arrows (Domains (QName -> NotBlocked' (ZonkAny 14))) (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    Word32 -> t -> Arrows (Domains t) (S Word32)
    icodeN Word32
    3 QName -> NotBlocked' (ZonkAny 14)
    forall t. QName -> NotBlocked' t
    MissingClauses QName
    a

      value :: Word32 -> R NotBlocked
    value = ([Word32] -> R NotBlocked) -> Word32 -> R NotBlocked
    forall a. EmbPrj a => ([Word32] -> R a) -> Word32 -> R a
    vcase [Word32] -> R NotBlocked
    forall {t}. EmbPrj t => [Word32] -> StateT St IO (NotBlocked' t)
    valu where
        valu :: [Word32]
    -> Arrows
         (Constant Word32 (Domains (NotBlocked' t)))
         (R (CoDomain (NotBlocked' t)))
    valu []     = NotBlocked' t
    -> Arrows
         (Constant Word32 (Domains (NotBlocked' t)))
         (R (CoDomain (NotBlocked' t)))
    forall t.
    (VALU t (IsBase t),
     StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
    valuN NotBlocked' t
    forall t. NotBlocked' t
    ReallyNotBlocked
        valu [Word32
    0, Word32
    a] = (Elim' t -> NotBlocked' t)
    -> Arrows
         (Constant Word32 (Domains (Elim' t -> NotBlocked' t)))
         (R (CoDomain (Elim' t -> NotBlocked' t)))
    forall t.
    (VALU t (IsBase t),
     StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
    valuN Elim' t -> NotBlocked' t
    forall t. Elim' t -> NotBlocked' t
    StuckOn Word32
    a
        valu [Word32
    1]    = NotBlocked' t
    -> Arrows
         (Constant Word32 (Domains (NotBlocked' t)))
         (R (CoDomain (NotBlocked' t)))
    forall t.
    (VALU t (IsBase t),
     StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
    valuN NotBlocked' t
    forall t. NotBlocked' t
    Underapplied
        valu [Word32
    2]    = NotBlocked' t
    -> Arrows
         (Constant Word32 (Domains (NotBlocked' t)))
         (R (CoDomain (NotBlocked' t)))
    forall t.
    (VALU t (IsBase t),
     StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
    valuN NotBlocked' t
    forall t. NotBlocked' t
    AbsurdMatch
        valu [Word32
    3, Word32
    a] = (QName -> NotBlocked' t)
    -> Arrows
         (Constant Word32 (Domains (QName -> NotBlocked' t)))
         (R (CoDomain (QName -> NotBlocked' t)))
    forall t.
    (VALU t (IsBase t),
     StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
    valuN QName -> NotBlocked' t
    forall t. QName -> NotBlocked' t
    MissingClauses Word32
    a
        valu [Word32]
    _      = StateT St IO (NotBlocked' t)
    Arrows
      (Constant Word32 (Domains (NotBlocked' t)))
      (R (CoDomain (NotBlocked' t)))
    forall a. R a
    malformed

    -- Andreas, 2024-01-02, issue #7044.
    -- We only serialize 'neverUnblock';
    -- other than that, there should not be any blockers left at serialization time.
    blockedToMaybe :: Blocked_ -> Maybe NotBlocked
    blockedToMaybe :: Blocked_ -> Maybe NotBlocked
    blockedToMaybe = \case
      NotBlocked NotBlocked
    a ()       -> NotBlocked -> Maybe NotBlocked
    forall a. a -> Maybe a
    Just NotBlocked
    a
      Blocked Blocker
    a ()
        | Blocker
    a Blocker -> Blocker -> Bool
    forall a. Eq a => a -> a -> Bool
    == Blocker
    neverUnblock -> Maybe NotBlocked
    forall a. Maybe a
    Nothing
        | Bool
    otherwise         -> Maybe NotBlocked
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    blockedFromMaybe :: Maybe NotBlocked -> Blocked_
    blockedFromMaybe :: Maybe NotBlocked -> Blocked_
    blockedFromMaybe = Blocked_
    -> (NotBlocked -> Blocked_) -> Maybe NotBlocked -> Blocked_
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe (Blocker -> () -> Blocked_
    forall t a. Blocker -> a -> Blocked' t a
    Blocked Blocker
    neverUnblock ()) (NotBlocked -> () -> Blocked_
    forall t a. NotBlocked' t -> a -> Blocked' t a
    `NotBlocked` ())

    instance EmbPrj Blocked_ where
      icod_ :: Blocked_ -> S Word32
    icod_ = Maybe NotBlocked -> S Word32
    forall a. EmbPrj a => a -> S Word32
    icod_ (Maybe NotBlocked -> S Word32)
    -> (Blocked_ -> Maybe NotBlocked) -> Blocked_ -> S Word32
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Blocked_ -> Maybe NotBlocked
    blockedToMaybe
      value :: Word32 -> R Blocked_
    value = Maybe NotBlocked -> Blocked_
    blockedFromMaybe (Maybe NotBlocked -> Blocked_)
    -> (Word32 -> StateT St IO (Maybe NotBlocked))
    -> Word32
    -> R Blocked_
    forall (m :: * -> *) b c a.
    Functor m =>
    (b -> c) -> (a -> m b) -> a -> m c
    <.> Word32 -> StateT St IO (Maybe NotBlocked)
    forall a. EmbPrj a => Word32 -> R a
    value

    instance EmbPrj NLPat where
      icod_ :: NLPat -> S Word32
    icod_ (PVar Int
    a [Arg Int]
    b)      = Word32
    -> (Int -> [Arg Int] -> NLPat)
    -> Arrows (Domains (Int -> [Arg Int] -> NLPat)) (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    Word32 -> t -> Arrows (Domains t) (S Word32)
    icodeN Word32
    0 Int -> [Arg Int] -> NLPat
    PVar Int
    a [Arg Int]
    b
      icod_ (PDef QName
    a PElims
    b)      = Word32
    -> (QName -> PElims -> NLPat)
    -> Arrows (Domains (QName -> PElims -> NLPat)) (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    Word32 -> t -> Arrows (Domains t) (S Word32)
    icodeN Word32
    1 QName -> PElims -> NLPat
    PDef QName
    a PElims
    b
      icod_ (PLam ArgInfo
    a Abs NLPat
    b)      = Word32
    -> (ArgInfo -> Abs NLPat -> NLPat)
    -> Arrows (Domains (ArgInfo -> Abs NLPat -> NLPat)) (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    Word32 -> t -> Arrows (Domains t) (S Word32)
    icodeN Word32
    2 ArgInfo -> Abs NLPat -> NLPat
    PLam ArgInfo
    a Abs NLPat
    b
      icod_ (PPi Dom NLPType
    a Abs NLPType
    b)       = Word32
    -> (Dom NLPType -> Abs NLPType -> NLPat)
    -> Arrows
         (Domains (Dom NLPType -> Abs NLPType -> NLPat)) (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    Word32 -> t -> Arrows (Domains t) (S Word32)
    icodeN Word32
    3 Dom NLPType -> Abs NLPType -> NLPat
    PPi Dom NLPType
    a Abs NLPType
    b
      icod_ (PSort NLPSort
    a)       = Word32
    -> (NLPSort -> NLPat)
    -> Arrows (Domains (NLPSort -> NLPat)) (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    Word32 -> t -> Arrows (Domains t) (S Word32)
    icodeN Word32
    4 NLPSort -> NLPat
    PSort NLPSort
    a
      icod_ (PBoundVar Int
    a PElims
    b) = Word32
    -> (Int -> PElims -> NLPat)
    -> Arrows (Domains (Int -> PElims -> NLPat)) (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    Word32 -> t -> Arrows (Domains t) (S Word32)
    icodeN Word32
    5 Int -> PElims -> NLPat
    PBoundVar Int
    a PElims
    b
      icod_ (PTerm Term
    a)       = Word32
    -> (Term -> NLPat) -> Arrows (Domains (Term -> NLPat)) (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    Word32 -> t -> Arrows (Domains t) (S Word32)
    icodeN Word32
    6 Term -> NLPat
    PTerm Term
    a

      value :: Word32 -> R NLPat
    value = ([Word32] -> R NLPat) -> Word32 -> R NLPat
    forall a. EmbPrj a => ([Word32] -> R a) -> Word32 -> R a
    vcase [Word32] -> R NLPat
    valu where
        valu :: [Word32] -> R NLPat
    valu [Word32
    0, Word32
    a, Word32
    b]    = (Int -> [Arg Int] -> NLPat)
    -> Arrows
         (Constant Word32 (Domains (Int -> [Arg Int] -> NLPat)))
         (R (CoDomain (Int -> [Arg Int] -> NLPat)))
    forall t.
    (VALU t (IsBase t),
     StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
    valuN Int -> [Arg Int] -> NLPat
    PVar Word32
    a Word32
    b
        valu [Word32
    1, Word32
    a, Word32
    b]    = (QName -> PElims -> NLPat)
    -> Arrows
         (Constant Word32 (Domains (QName -> PElims -> NLPat)))
         (R (CoDomain (QName -> PElims -> NLPat)))
    forall t.
    (VALU t (IsBase t),
     StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
    valuN QName -> PElims -> NLPat
    PDef Word32
    a Word32
    b
        valu [Word32
    2, Word32
    a, Word32
    b]    = (ArgInfo -> Abs NLPat -> NLPat)
    -> Arrows
         (Constant Word32 (Domains (ArgInfo -> Abs NLPat -> NLPat)))
         (R (CoDomain (ArgInfo -> Abs NLPat -> NLPat)))
    forall t.
    (VALU t (IsBase t),
     StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
    valuN ArgInfo -> Abs NLPat -> NLPat
    PLam Word32
    a Word32
    b
        valu [Word32
    3, Word32
    a, Word32
    b]    = (Dom NLPType -> Abs NLPType -> NLPat)
    -> Arrows
         (Constant Word32 (Domains (Dom NLPType -> Abs NLPType -> NLPat)))
         (R (CoDomain (Dom NLPType -> Abs NLPType -> NLPat)))
    forall t.
    (VALU t (IsBase t),
     StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
    valuN Dom NLPType -> Abs NLPType -> NLPat
    PPi Word32
    a Word32
    b
        valu [Word32
    4, Word32
    a]       = (NLPSort -> NLPat)
    -> Arrows
         (Constant Word32 (Domains (NLPSort -> NLPat)))
         (R (CoDomain (NLPSort -> NLPat)))
    forall t.
    (VALU t (IsBase t),
     StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
    valuN NLPSort -> NLPat
    PSort Word32
    a
        valu [Word32
    5, Word32
    a, Word32
    b]    = (Int -> PElims -> NLPat)
    -> Arrows
         (Constant Word32 (Domains (Int -> PElims -> NLPat)))
         (R (CoDomain (Int -> PElims -> NLPat)))
    forall t.
    (VALU t (IsBase t),
     StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
    valuN Int -> PElims -> NLPat
    PBoundVar Word32
    a Word32
    b
        valu [Word32
    6, Word32
    a]       = (Term -> NLPat)
    -> Arrows
         (Constant Word32 (Domains (Term -> NLPat)))
         (R (CoDomain (Term -> NLPat)))
    forall t.
    (VALU t (IsBase t),
     StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
    valuN Term -> NLPat
    PTerm Word32
    a
        valu [Word32]
    _            = R NLPat
    forall a. R a
    malformed

    instance EmbPrj NLPType where
      icod_ :: NLPType -> S Word32
    icod_ (NLPType NLPSort
    a NLPat
    b) = (NLPSort -> NLPat -> NLPType)
    -> Arrows (Domains (NLPSort -> NLPat -> NLPType)) (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Domains t) (S Word32)
    icodeN' NLPSort -> NLPat -> NLPType
    NLPType NLPSort
    a NLPat
    b

      value :: Word32 -> R NLPType
    value = (NLPSort -> NLPat -> NLPType)
    -> Word32 -> R (CoDomain (NLPSort -> NLPat -> NLPType))
    forall t.
    (VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
    t -> Word32 -> R (CoDomain t)
    valueN NLPSort -> NLPat -> NLPType
    NLPType

    instance EmbPrj NLPSort where
      icod_ :: NLPSort -> S Word32
    icod_ (PType NLPat
    a)   = Word32
    -> (NLPat -> NLPSort)
    -> Arrows (Domains (NLPat -> NLPSort)) (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    Word32 -> t -> Arrows (Domains t) (S Word32)
    icodeN Word32
    0 NLPat -> NLPSort
    PType NLPat
    a
      icod_ (PProp NLPat
    a)   = Word32
    -> (NLPat -> NLPSort)
    -> Arrows (Domains (NLPat -> NLPSort)) (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    Word32 -> t -> Arrows (Domains t) (S Word32)
    icodeN Word32
    1 NLPat -> NLPSort
    PProp NLPat
    a
      icod_ (PInf Univ
    f Integer
    a)  = Word32
    -> (Univ -> Integer -> NLPSort)
    -> Arrows (Domains (Univ -> Integer -> NLPSort)) (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    Word32 -> t -> Arrows (Domains t) (S Word32)
    icodeN Word32
    2 Univ -> Integer -> NLPSort
    PInf Univ
    f Integer
    a
      icod_ NLPSort
    PSizeUniv   = Word32 -> NLPSort -> Arrows (Domains NLPSort) (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    Word32 -> t -> Arrows (Domains t) (S Word32)
    icodeN Word32
    3 NLPSort
    PSizeUniv
      icod_ NLPSort
    PLockUniv   = Word32 -> NLPSort -> Arrows (Domains NLPSort) (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    Word32 -> t -> Arrows (Domains t) (S Word32)
    icodeN Word32
    4 NLPSort
    PLockUniv
      icod_ NLPSort
    PIntervalUniv = Word32 -> NLPSort -> Arrows (Domains NLPSort) (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    Word32 -> t -> Arrows (Domains t) (S Word32)
    icodeN Word32
    5 NLPSort
    PIntervalUniv
      icod_ (PSSet NLPat
    a)   = Word32
    -> (NLPat -> NLPSort)
    -> Arrows (Domains (NLPat -> NLPSort)) (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    Word32 -> t -> Arrows (Domains t) (S Word32)
    icodeN Word32
    6 NLPat -> NLPSort
    PSSet NLPat
    a
      icod_ NLPSort
    PLevelUniv = Word32 -> NLPSort -> Arrows (Domains NLPSort) (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    Word32 -> t -> Arrows (Domains t) (S Word32)
    icodeN Word32
    7 NLPSort
    PLevelUniv

      value :: Word32 -> R NLPSort
    value = ([Word32] -> R NLPSort) -> Word32 -> R NLPSort
    forall a. EmbPrj a => ([Word32] -> R a) -> Word32 -> R a
    vcase [Word32] -> R NLPSort
    valu where
        valu :: [Word32] -> R NLPSort
    valu [Word32
    0, Word32
    a] = (NLPat -> NLPSort)
    -> Arrows
         (Constant Word32 (Domains (NLPat -> NLPSort)))
         (R (CoDomain (NLPat -> NLPSort)))
    forall t.
    (VALU t (IsBase t),
     StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
    valuN NLPat -> NLPSort
    PType Word32
    a
        valu [Word32
    1, Word32
    a] = (NLPat -> NLPSort)
    -> Arrows
         (Constant Word32 (Domains (NLPat -> NLPSort)))
         (R (CoDomain (NLPat -> NLPSort)))
    forall t.
    (VALU t (IsBase t),
     StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
    valuN NLPat -> NLPSort
    PProp Word32
    a
        valu [Word32
    2, Word32
    f, Word32
    a] = (Univ -> Integer -> NLPSort)
    -> Arrows
         (Constant Word32 (Domains (Univ -> Integer -> NLPSort)))
         (R (CoDomain (Univ -> Integer -> NLPSort)))
    forall t.
    (VALU t (IsBase t),
     StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
    valuN Univ -> Integer -> NLPSort
    PInf Word32
    f Word32
    a
        valu [Word32
    3]    = NLPSort
    -> Arrows
         (Constant Word32 (Domains NLPSort)) (R (CoDomain NLPSort))
    forall t.
    (VALU t (IsBase t),
     StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
    valuN NLPSort
    PSizeUniv
        valu [Word32
    4]    = NLPSort
    -> Arrows
         (Constant Word32 (Domains NLPSort)) (R (CoDomain NLPSort))
    forall t.
    (VALU t (IsBase t),
     StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
    valuN NLPSort
    PLockUniv
        valu [Word32
    5]    = NLPSort
    -> Arrows
         (Constant Word32 (Domains NLPSort)) (R (CoDomain NLPSort))
    forall t.
    (VALU t (IsBase t),
     StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
    valuN NLPSort
    PIntervalUniv
        valu [Word32
    6, Word32
    a] = (NLPat -> NLPSort)
    -> Arrows
         (Constant Word32 (Domains (NLPat -> NLPSort)))
         (R (CoDomain (NLPat -> NLPSort)))
    forall t.
    (VALU t (IsBase t),
     StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
    valuN NLPat -> NLPSort
    PSSet Word32
    a
        valu [Word32
    7]    = NLPSort
    -> Arrows
         (Constant Word32 (Domains NLPSort)) (R (CoDomain NLPSort))
    forall t.
    (VALU t (IsBase t),
     StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
    valuN NLPSort
    PLevelUniv
        valu [Word32]
    _      = R NLPSort
    forall a. R a
    malformed

    instance EmbPrj RewriteRule where
      icod_ :: RewriteRule -> S Word32
    icod_ (RewriteRule QName
    a Telescope
    b QName
    c PElims
    d Term
    e Type
    f Bool
    g TopLevelModuleName
    h) = (QName
     -> Telescope
     -> QName
     -> PElims
     -> Term
     -> Type
     -> Bool
     -> TopLevelModuleName
     -> RewriteRule)
    -> Arrows
         (Domains
            (QName
             -> Telescope
             -> QName
             -> PElims
             -> Term
             -> Type
             -> Bool
             -> TopLevelModuleName
             -> RewriteRule))
         (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Domains t) (S Word32)
    icodeN' QName
    -> Telescope
    -> QName
    -> PElims
    -> Term
    -> Type
    -> Bool
    -> TopLevelModuleName
    -> RewriteRule
    RewriteRule QName
    a Telescope
    b QName
    c PElims
    d Term
    e Type
    f Bool
    g TopLevelModuleName
    h

      value :: Word32 -> R RewriteRule
    value = (QName
     -> Telescope
     -> QName
     -> PElims
     -> Term
     -> Type
     -> Bool
     -> TopLevelModuleName
     -> RewriteRule)
    -> Word32
    -> R (CoDomain
            (QName
             -> Telescope
             -> QName
             -> PElims
             -> Term
             -> Type
             -> Bool
             -> TopLevelModuleName
             -> RewriteRule))
    forall t.
    (VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
    t -> Word32 -> R (CoDomain t)
    valueN QName
    -> Telescope
    -> QName
    -> PElims
    -> Term
    -> Type
    -> Bool
    -> TopLevelModuleName
    -> RewriteRule
    RewriteRule

    instance EmbPrj Projection where
      icod_ :: Projection -> S Word32
    icod_ (Projection Maybe QName
    a QName
    b Arg QName
    c Int
    d ProjLams
    e) = (Maybe QName
     -> QName -> Arg QName -> Int -> ProjLams -> Projection)
    -> Arrows
         (Domains
            (Maybe QName
             -> QName -> Arg QName -> Int -> ProjLams -> Projection))
         (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Domains t) (S Word32)
    icodeN' Maybe QName -> QName -> Arg QName -> Int -> ProjLams -> Projection
    Projection Maybe QName
    a QName
    b Arg QName
    c Int
    d ProjLams
    e

      value :: Word32 -> R Projection
    value = (Maybe QName
     -> QName -> Arg QName -> Int -> ProjLams -> Projection)
    -> Word32
    -> R (CoDomain
            (Maybe QName
             -> QName -> Arg QName -> Int -> ProjLams -> Projection))
    forall t.
    (VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
    t -> Word32 -> R (CoDomain t)
    valueN Maybe QName -> QName -> Arg QName -> Int -> ProjLams -> Projection
    Projection

    instance EmbPrj ProjLams where
      icod_ :: ProjLams -> S Word32
    icod_ (ProjLams [Arg ArgName]
    a) = ([Arg ArgName] -> ProjLams)
    -> Arrows (Domains ([Arg ArgName] -> ProjLams)) (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Domains t) (S Word32)
    icodeN' [Arg ArgName] -> ProjLams
    ProjLams [Arg ArgName]
    a

      value :: Word32 -> R ProjLams
    value = ([Arg ArgName] -> ProjLams)
    -> Word32 -> R (CoDomain ([Arg ArgName] -> ProjLams))
    forall t.
    (VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
    t -> Word32 -> R (CoDomain t)
    valueN [Arg ArgName] -> ProjLams
    ProjLams

    instance EmbPrj System where
      icod_ :: System -> S Word32
    icod_ (System Telescope
    a [(Face, Term)]
    b) = (Telescope -> [(Face, Term)] -> System)
    -> Arrows
         (Domains (Telescope -> [(Face, Term)] -> System)) (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Domains t) (S Word32)
    icodeN' Telescope -> [(Face, Term)] -> System
    System Telescope
    a [(Face, Term)]
    b

      value :: Word32 -> R System
    value = (Telescope -> [(Face, Term)] -> System)
    -> Word32 -> R (CoDomain (Telescope -> [(Face, Term)] -> System))
    forall t.
    (VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
    t -> Word32 -> R (CoDomain t)
    valueN Telescope -> [(Face, Term)] -> System
    System

    instance EmbPrj ExtLamInfo where
      icod_ :: ExtLamInfo -> S Word32
    icod_ (ExtLamInfo ModuleName
    a Bool
    b Maybe System
    c) = (ModuleName -> Bool -> Maybe System -> ExtLamInfo)
    -> Arrows
         (Domains (ModuleName -> Bool -> Maybe System -> ExtLamInfo))
         (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Domains t) (S Word32)
    icodeN' ModuleName -> Bool -> Maybe System -> ExtLamInfo
    ExtLamInfo ModuleName
    a Bool
    b Maybe System
    c

      value :: Word32 -> R ExtLamInfo
    value = (ModuleName -> Bool -> Maybe System -> ExtLamInfo)
    -> Word32
    -> R (CoDomain (ModuleName -> Bool -> Maybe System -> ExtLamInfo))
    forall t.
    (VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
    t -> Word32 -> R (CoDomain t)
    valueN ModuleName -> Bool -> Maybe System -> ExtLamInfo
    ExtLamInfo

    instance EmbPrj Polarity where
      icod_ :: Polarity -> S Word32
    icod_ Polarity
    Covariant     = Word32 -> S Word32
    forall a. a -> ReaderT Dict IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Word32
    0
      icod_ Polarity
    Contravariant = Word32 -> S Word32
    forall a. a -> ReaderT Dict IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Word32
    1
      icod_ Polarity
    Invariant     = Word32 -> S Word32
    forall a. a -> ReaderT Dict IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Word32
    2
      icod_ Polarity
    Nonvariant    = Word32 -> S Word32
    forall a. a -> ReaderT Dict IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Word32
    3

      value :: Word32 -> R Polarity
    value Word32
    0 = Polarity -> R Polarity
    forall a. a -> StateT St IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Polarity
    Covariant
      value Word32
    1 = Polarity -> R Polarity
    forall a. a -> StateT St IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Polarity
    Contravariant
      value Word32
    2 = Polarity -> R Polarity
    forall a. a -> StateT St IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Polarity
    Invariant
      value Word32
    3 = Polarity -> R Polarity
    forall a. a -> StateT St IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Polarity
    Nonvariant
      value Word32
    _ = R Polarity
    forall a. R a
    malformed

    instance EmbPrj IsForced where
      icod_ :: IsForced -> S Word32
    icod_ IsForced
    Forced    = Word32 -> S Word32
    forall a. a -> ReaderT Dict IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Word32
    0
      icod_ IsForced
    NotForced = Word32 -> S Word32
    forall a. a -> ReaderT Dict IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Word32
    1

      value :: Word32 -> R IsForced
    value Word32
    0 = IsForced -> R IsForced
    forall a. a -> StateT St IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return IsForced
    Forced
      value Word32
    1 = IsForced -> R IsForced
    forall a. a -> StateT St IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return IsForced
    NotForced
      value Word32
    _ = R IsForced
    forall a. R a
    malformed

    instance EmbPrj NumGeneralizableArgs where
      icod_ :: NumGeneralizableArgs -> S Word32
    icod_ NumGeneralizableArgs
    NoGeneralizableArgs       = NumGeneralizableArgs
    -> Arrows (Domains NumGeneralizableArgs) (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Domains t) (S Word32)
    icodeN' NumGeneralizableArgs
    NoGeneralizableArgs
      icod_ (SomeGeneralizableArgs Int
    a) = (Int -> NumGeneralizableArgs)
    -> Arrows (Domains (Int -> NumGeneralizableArgs)) (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Domains t) (S Word32)
    icodeN' Int -> NumGeneralizableArgs
    SomeGeneralizableArgs Int
    a

      value :: Word32 -> R NumGeneralizableArgs
    value = ([Word32] -> R NumGeneralizableArgs)
    -> Word32 -> R NumGeneralizableArgs
    forall a. EmbPrj a => ([Word32] -> R a) -> Word32 -> R a
    vcase [Word32] -> R NumGeneralizableArgs
    valu where
        valu :: [Word32]
    -> Arrows
         (Constant Word32 (Domains NumGeneralizableArgs))
         (R (CoDomain NumGeneralizableArgs))
    valu []  = NumGeneralizableArgs
    -> Arrows
         (Constant Word32 (Domains NumGeneralizableArgs))
         (R (CoDomain NumGeneralizableArgs))
    forall t.
    (VALU t (IsBase t),
     StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
    valuN NumGeneralizableArgs
    NoGeneralizableArgs
        valu [Word32
    a] = (Int -> NumGeneralizableArgs)
    -> Arrows
         (Constant Word32 (Domains (Int -> NumGeneralizableArgs)))
         (R (CoDomain (Int -> NumGeneralizableArgs)))
    forall t.
    (VALU t (IsBase t),
     StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
    valuN Int -> NumGeneralizableArgs
    SomeGeneralizableArgs Word32
    a
        valu [Word32]
    _   = R NumGeneralizableArgs
    Arrows
      (Constant Word32 (Domains NumGeneralizableArgs))
      (R (CoDomain NumGeneralizableArgs))
    forall a. R a
    malformed

    instance EmbPrj DoGeneralize where
      icod_ :: DoGeneralize -> S Word32
    icod_ DoGeneralize
    YesGeneralizeVar  = Word32 -> S Word32
    forall a. a -> ReaderT Dict IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Word32
    0
      icod_ DoGeneralize
    YesGeneralizeMeta = Word32 -> S Word32
    forall a. a -> ReaderT Dict IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Word32
    1
      icod_ DoGeneralize
    NoGeneralize      = Word32 -> S Word32
    forall a. a -> ReaderT Dict IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Word32
    2

      value :: Word32 -> R DoGeneralize
    value Word32
    0 = DoGeneralize -> R DoGeneralize
    forall a. a -> StateT St IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return DoGeneralize
    YesGeneralizeVar
      value Word32
    1 = DoGeneralize -> R DoGeneralize
    forall a. a -> StateT St IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return DoGeneralize
    YesGeneralizeMeta
      value Word32
    2 = DoGeneralize -> R DoGeneralize
    forall a. a -> StateT St IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return DoGeneralize
    NoGeneralize
      value Word32
    _ = R DoGeneralize
    forall a. R a
    malformed

    instance EmbPrj Occurrence where
      icod_ :: Occurrence -> S Word32
    icod_ Occurrence
    StrictPos = Word32 -> S Word32
    forall a. a -> ReaderT Dict IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Word32
    0
      icod_ Occurrence
    Mixed     = Word32 -> S Word32
    forall a. a -> ReaderT Dict IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Word32
    1
      icod_ Occurrence
    Unused    = Word32 -> S Word32
    forall a. a -> ReaderT Dict IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Word32
    2
      icod_ Occurrence
    GuardPos  = Word32 -> S Word32
    forall a. a -> ReaderT Dict IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Word32
    3
      icod_ Occurrence
    JustPos   = Word32 -> S Word32
    forall a. a -> ReaderT Dict IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Word32
    4
      icod_ Occurrence
    JustNeg   = Word32 -> S Word32
    forall a. a -> ReaderT Dict IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Word32
    5

      value :: Word32 -> R Occurrence
    value Word32
    0 = Occurrence -> R Occurrence
    forall a. a -> StateT St IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Occurrence
    StrictPos
      value Word32
    1 = Occurrence -> R Occurrence
    forall a. a -> StateT St IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Occurrence
    Mixed
      value Word32
    2 = Occurrence -> R Occurrence
    forall a. a -> StateT St IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Occurrence
    Unused
      value Word32
    3 = Occurrence -> R Occurrence
    forall a. a -> StateT St IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Occurrence
    GuardPos
      value Word32
    4 = Occurrence -> R Occurrence
    forall a. a -> StateT St IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Occurrence
    JustPos
      value Word32
    5 = Occurrence -> R Occurrence
    forall a. a -> StateT St IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Occurrence
    JustNeg
      value Word32
    _ = R Occurrence
    forall a. R a
    malformed

    instance EmbPrj EtaEquality where
      icod_ :: EtaEquality -> S Word32
    icod_ (Specified HasEta
    a) = Word32
    -> (HasEta -> EtaEquality)
    -> Arrows (Domains (HasEta -> EtaEquality)) (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    Word32 -> t -> Arrows (Domains t) (S Word32)
    icodeN Word32
    0 HasEta -> EtaEquality
    Specified HasEta
    a
      icod_ (Inferred HasEta
    a)  = Word32
    -> (HasEta -> EtaEquality)
    -> Arrows (Domains (HasEta -> EtaEquality)) (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    Word32 -> t -> Arrows (Domains t) (S Word32)
    icodeN Word32
    1 HasEta -> EtaEquality
    Inferred HasEta
    a

      value :: Word32 -> R EtaEquality
    value = ([Word32] -> R EtaEquality) -> Word32 -> R EtaEquality
    forall a. EmbPrj a => ([Word32] -> R a) -> Word32 -> R a
    vcase [Word32] -> R EtaEquality
    valu where
        valu :: [Word32] -> R EtaEquality
    valu [Word32
    0,Word32
    a] = (HasEta -> EtaEquality)
    -> Arrows
         (Constant Word32 (Domains (HasEta -> EtaEquality)))
         (R (CoDomain (HasEta -> EtaEquality)))
    forall t.
    (VALU t (IsBase t),
     StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
    valuN HasEta -> EtaEquality
    Specified Word32
    a
        valu [Word32
    1,Word32
    a] = (HasEta -> EtaEquality)
    -> Arrows
         (Constant Word32 (Domains (HasEta -> EtaEquality)))
         (R (CoDomain (HasEta -> EtaEquality)))
    forall t.
    (VALU t (IsBase t),
     StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
    valuN HasEta -> EtaEquality
    Inferred Word32
    a
        valu [Word32]
    _     = R EtaEquality
    forall a. R a
    malformed

    instance EmbPrj ProjectionLikenessMissing

    instance EmbPrj BuiltinSort where
      icod_ :: BuiltinSort -> S Word32
    icod_ = \case
        SortUniv  Univ
    a      -> Word32
    -> (Univ -> BuiltinSort)
    -> Arrows (Domains (Univ -> BuiltinSort)) (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    Word32 -> t -> Arrows (Domains t) (S Word32)
    icodeN Word32
    0 Univ -> BuiltinSort
    SortUniv  Univ
    a
        SortOmega Univ
    a      -> Word32
    -> (Univ -> BuiltinSort)
    -> Arrows (Domains (Univ -> BuiltinSort)) (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    Word32 -> t -> Arrows (Domains t) (S Word32)
    icodeN Word32
    1 Univ -> BuiltinSort
    SortOmega Univ
    a
        BuiltinSort
    SortIntervalUniv -> Word32 -> BuiltinSort -> Arrows (Domains BuiltinSort) (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    Word32 -> t -> Arrows (Domains t) (S Word32)
    icodeN Word32
    2 BuiltinSort
    SortIntervalUniv
        BuiltinSort
    SortLevelUniv    -> Word32 -> BuiltinSort -> Arrows (Domains BuiltinSort) (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    Word32 -> t -> Arrows (Domains t) (S Word32)
    icodeN Word32
    3 BuiltinSort
    SortLevelUniv

      value :: Word32 -> R BuiltinSort
    value = ([Word32] -> R BuiltinSort) -> Word32 -> R BuiltinSort
    forall a. EmbPrj a => ([Word32] -> R a) -> Word32 -> R a
    vcase \case
        [Word32
    0, Word32
    a] -> (Univ -> BuiltinSort)
    -> Arrows
         (Constant Word32 (Domains (Univ -> BuiltinSort)))
         (R (CoDomain (Univ -> BuiltinSort)))
    forall t.
    (VALU t (IsBase t),
     StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
    valuN Univ -> BuiltinSort
    SortUniv  Word32
    a
        [Word32
    1, Word32
    a] -> (Univ -> BuiltinSort)
    -> Arrows
         (Constant Word32 (Domains (Univ -> BuiltinSort)))
         (R (CoDomain (Univ -> BuiltinSort)))
    forall t.
    (VALU t (IsBase t),
     StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
    valuN Univ -> BuiltinSort
    SortOmega Word32
    a
        [Word32
    2]    -> BuiltinSort
    -> Arrows
         (Constant Word32 (Domains BuiltinSort)) (R (CoDomain BuiltinSort))
    forall t.
    (VALU t (IsBase t),
     StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
    valuN BuiltinSort
    SortIntervalUniv
        [Word32
    3]    -> BuiltinSort
    -> Arrows
         (Constant Word32 (Domains BuiltinSort)) (R (CoDomain BuiltinSort))
    forall t.
    (VALU t (IsBase t),
     StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
    valuN BuiltinSort
    SortLevelUniv
        [Word32]
    _ -> R BuiltinSort
    forall a. R a
    malformed

    instance EmbPrj Defn where
      icod_ :: Defn -> S Word32
    icod_ (Axiom       Bool
    a)                                 = Word32
    -> (Bool -> Defn) -> Arrows (Domains (Bool -> Defn)) (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    Word32 -> t -> Arrows (Domains t) (S Word32)
    icodeN Word32
    0 Bool -> Defn
    Axiom Bool
    a
      icod_ (Function    [Clause]
    a Maybe CompiledClauses
    b Maybe SplitTree
    s Maybe Compiled
    t [Clause]
    u FunctionInverse
    c Maybe [QName]
    d Either ProjectionLikenessMissing Projection
    e SmallSet FunctionFlag
    f Maybe Bool
    g Maybe ExtLamInfo
    h Maybe QName
    i Maybe QName
    j IsOpaque
    k)       = Word32
    -> ([Clause]
        -> Maybe CompiledClauses
        -> Maybe SplitTree
        -> [Clause]
        -> FunctionInverse
        -> Maybe [QName]
        -> Either ProjectionLikenessMissing Projection
        -> SmallSet FunctionFlag
        -> Maybe Bool
        -> Maybe ExtLamInfo
        -> Maybe QName
        -> Maybe QName
        -> IsOpaque
        -> Defn)
    -> Arrows
         (Domains
            ([Clause]
             -> Maybe CompiledClauses
             -> Maybe SplitTree
             -> [Clause]
             -> FunctionInverse
             -> Maybe [QName]
             -> Either ProjectionLikenessMissing Projection
             -> SmallSet FunctionFlag
             -> Maybe Bool
             -> Maybe ExtLamInfo
             -> Maybe QName
             -> Maybe QName
             -> IsOpaque
             -> Defn))
         (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    Word32 -> t -> Arrows (Domains t) (S Word32)
    icodeN Word32
    1 (\ [Clause]
    a Maybe CompiledClauses
    b Maybe SplitTree
    s -> [Clause]
    -> Maybe CompiledClauses
    -> Maybe SplitTree
    -> Maybe Compiled
    -> [Clause]
    -> FunctionInverse
    -> Maybe [QName]
    -> Either ProjectionLikenessMissing Projection
    -> SmallSet FunctionFlag
    -> Maybe Bool
    -> Maybe ExtLamInfo
    -> Maybe QName
    -> Maybe QName
    -> IsOpaque
    -> Defn
    Function [Clause]
    a Maybe CompiledClauses
    b Maybe SplitTree
    s Maybe Compiled
    t) [Clause]
    a Maybe CompiledClauses
    b Maybe SplitTree
    s [Clause]
    u FunctionInverse
    c Maybe [QName]
    d Either ProjectionLikenessMissing Projection
    e SmallSet FunctionFlag
    f Maybe Bool
    g Maybe ExtLamInfo
    h Maybe QName
    i Maybe QName
    j IsOpaque
    k
      icod_ (Datatype    Int
    a Int
    b Maybe Clause
    c [QName]
    d Sort' Term
    e Maybe [QName]
    f IsAbstract
    g [QName]
    h Maybe QName
    i Maybe QName
    j)               = Word32
    -> (Int
        -> Int
        -> Maybe Clause
        -> [QName]
        -> Sort' Term
        -> Maybe [QName]
        -> IsAbstract
        -> [QName]
        -> Maybe QName
        -> Maybe QName
        -> Defn)
    -> Arrows
         (Domains
            (Int
             -> Int
             -> Maybe Clause
             -> [QName]
             -> Sort' Term
             -> Maybe [QName]
             -> IsAbstract
             -> [QName]
             -> Maybe QName
             -> Maybe QName
             -> Defn))
         (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    Word32 -> t -> Arrows (Domains t) (S Word32)
    icodeN Word32
    2 Int
    -> Int
    -> Maybe Clause
    -> [QName]
    -> Sort' Term
    -> Maybe [QName]
    -> IsAbstract
    -> [QName]
    -> Maybe QName
    -> Maybe QName
    -> Defn
    Datatype Int
    a Int
    b Maybe Clause
    c [QName]
    d Sort' Term
    e Maybe [QName]
    f IsAbstract
    g [QName]
    h Maybe QName
    i Maybe QName
    j
      icod_ (Record      Int
    a Maybe Clause
    b ConHead
    c Bool
    d [Dom QName]
    e Telescope
    f Maybe [QName]
    g EtaEquality
    h PatternOrCopattern
    i Maybe Induction
    j Maybe Bool
    k IsAbstract
    l CompKit
    m)         = Word32
    -> (Int
        -> Maybe Clause
        -> ConHead
        -> Bool
        -> [Dom QName]
        -> Telescope
        -> Maybe [QName]
        -> EtaEquality
        -> PatternOrCopattern
        -> Maybe Induction
        -> Maybe Bool
        -> IsAbstract
        -> CompKit
        -> Defn)
    -> Arrows
         (Domains
            (Int
             -> Maybe Clause
             -> ConHead
             -> Bool
             -> [Dom QName]
             -> Telescope
             -> Maybe [QName]
             -> EtaEquality
             -> PatternOrCopattern
             -> Maybe Induction
             -> Maybe Bool
             -> IsAbstract
             -> CompKit
             -> Defn))
         (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    Word32 -> t -> Arrows (Domains t) (S Word32)
    icodeN Word32
    3 Int
    -> Maybe Clause
    -> ConHead
    -> Bool
    -> [Dom QName]
    -> Telescope
    -> Maybe [QName]
    -> EtaEquality
    -> PatternOrCopattern
    -> Maybe Induction
    -> Maybe Bool
    -> IsAbstract
    -> CompKit
    -> Defn
    Record Int
    a Maybe Clause
    b ConHead
    c Bool
    d [Dom QName]
    e Telescope
    f Maybe [QName]
    g EtaEquality
    h PatternOrCopattern
    i Maybe Induction
    j Maybe Bool
    k IsAbstract
    l CompKit
    m
      icod_ (Constructor Int
    a Int
    b ConHead
    c QName
    d IsAbstract
    e CompKit
    f Maybe [QName]
    g [IsForced]
    h Maybe [Bool]
    i Bool
    j Bool
    k)             = Word32
    -> (Int
        -> Int
        -> ConHead
        -> QName
        -> IsAbstract
        -> CompKit
        -> Maybe [QName]
        -> [IsForced]
        -> Maybe [Bool]
        -> Bool
        -> Bool
        -> Defn)
    -> Arrows
         (Domains
            (Int
             -> Int
             -> ConHead
             -> QName
             -> IsAbstract
             -> CompKit
             -> Maybe [QName]
             -> [IsForced]
             -> Maybe [Bool]
             -> Bool
             -> Bool
             -> Defn))
         (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    Word32 -> t -> Arrows (Domains t) (S Word32)
    icodeN Word32
    4 Int
    -> Int
    -> ConHead
    -> QName
    -> IsAbstract
    -> CompKit
    -> Maybe [QName]
    -> [IsForced]
    -> Maybe [Bool]
    -> Bool
    -> Bool
    -> Defn
    Constructor Int
    a Int
    b ConHead
    c QName
    d IsAbstract
    e CompKit
    f Maybe [QName]
    g [IsForced]
    h Maybe [Bool]
    i Bool
    j Bool
    k
      icod_ (Primitive   IsAbstract
    a PrimitiveId
    b [Clause]
    c FunctionInverse
    d Maybe CompiledClauses
    e IsOpaque
    f)                       = Word32
    -> (IsAbstract
        -> PrimitiveId
        -> [Clause]
        -> FunctionInverse
        -> Maybe CompiledClauses
        -> IsOpaque
        -> Defn)
    -> Arrows
         (Domains
            (IsAbstract
             -> PrimitiveId
             -> [Clause]
             -> FunctionInverse
             -> Maybe CompiledClauses
             -> IsOpaque
             -> Defn))
         (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    Word32 -> t -> Arrows (Domains t) (S Word32)
    icodeN Word32
    5 IsAbstract
    -> PrimitiveId
    -> [Clause]
    -> FunctionInverse
    -> Maybe CompiledClauses
    -> IsOpaque
    -> Defn
    Primitive IsAbstract
    a PrimitiveId
    b [Clause]
    c FunctionInverse
    d Maybe CompiledClauses
    e IsOpaque
    f
      icod_ (PrimitiveSort BuiltinSort
    a Sort' Term
    b)                             = Word32
    -> (BuiltinSort -> Sort' Term -> Defn)
    -> Arrows (Domains (BuiltinSort -> Sort' Term -> Defn)) (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    Word32 -> t -> Arrows (Domains t) (S Word32)
    icodeN Word32
    6 BuiltinSort -> Sort' Term -> Defn
    PrimitiveSort BuiltinSort
    a Sort' Term
    b
      icod_ AbstractDefn{}                                  = S Word32
    forall a. HasCallStack => a
    __IMPOSSIBLE__
      icod_ (GeneralizableVar NumGeneralizableArgs
    a)                            = Word32
    -> (NumGeneralizableArgs -> Defn)
    -> Arrows (Domains (NumGeneralizableArgs -> Defn)) (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    Word32 -> t -> Arrows (Domains t) (S Word32)
    icodeN Word32
    7 NumGeneralizableArgs -> Defn
    GeneralizableVar NumGeneralizableArgs
    a
      icod_ (DataOrRecSig Int
    a)                                = Word32
    -> (Int -> Defn) -> Arrows (Domains (Int -> Defn)) (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    Word32 -> t -> Arrows (Domains t) (S Word32)
    icodeN Word32
    8 Int -> Defn
    DataOrRecSig Int
    a
        -- Andreas, 2024-10-27
        -- DataOrRecSig is possible via unquoteDecl in meta-programming, see #7576

      value :: Word32 -> R Defn
    value = ([Word32] -> R Defn) -> Word32 -> R Defn
    forall a. EmbPrj a => ([Word32] -> R a) -> Word32 -> R a
    vcase [Word32] -> R Defn
    valu where
        valu :: [Word32] -> R Defn
    valu [Word32
    0, Word32
    a]                                        = (Bool -> Defn)
    -> Arrows
         (Constant Word32 (Domains (Bool -> Defn)))
         (R (CoDomain (Bool -> Defn)))
    forall t.
    (VALU t (IsBase t),
     StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
    valuN Bool -> Defn
    Axiom Word32
    a
        valu [Word32
    1, Word32
    a, Word32
    b, Word32
    s, Word32
    u, Word32
    c, Word32
    d, Word32
    e, Word32
    f, Word32
    g, Word32
    h, Word32
    i, Word32
    j, Word32
    k]
                                                           = ([Clause]
     -> Maybe CompiledClauses
     -> Maybe SplitTree
     -> [Clause]
     -> FunctionInverse
     -> Maybe [QName]
     -> Either ProjectionLikenessMissing Projection
     -> SmallSet FunctionFlag
     -> Maybe Bool
     -> Maybe ExtLamInfo
     -> Maybe QName
     -> Maybe QName
     -> IsOpaque
     -> Defn)
    -> Arrows
         (Constant
            Word32
            (Domains
               ([Clause]
                -> Maybe CompiledClauses
                -> Maybe SplitTree
                -> [Clause]
                -> FunctionInverse
                -> Maybe [QName]
                -> Either ProjectionLikenessMissing Projection
                -> SmallSet FunctionFlag
                -> Maybe Bool
                -> Maybe ExtLamInfo
                -> Maybe QName
                -> Maybe QName
                -> IsOpaque
                -> Defn)))
         (R (CoDomain
               ([Clause]
                -> Maybe CompiledClauses
                -> Maybe SplitTree
                -> [Clause]
                -> FunctionInverse
                -> Maybe [QName]
                -> Either ProjectionLikenessMissing Projection
                -> SmallSet FunctionFlag
                -> Maybe Bool
                -> Maybe ExtLamInfo
                -> Maybe QName
                -> Maybe QName
                -> IsOpaque
                -> Defn)))
    forall t.
    (VALU t (IsBase t),
     StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
    valuN (\ [Clause]
    a Maybe CompiledClauses
    b Maybe SplitTree
    s -> [Clause]
    -> Maybe CompiledClauses
    -> Maybe SplitTree
    -> Maybe Compiled
    -> [Clause]
    -> FunctionInverse
    -> Maybe [QName]
    -> Either ProjectionLikenessMissing Projection
    -> SmallSet FunctionFlag
    -> Maybe Bool
    -> Maybe ExtLamInfo
    -> Maybe QName
    -> Maybe QName
    -> IsOpaque
    -> Defn
    Function [Clause]
    a Maybe CompiledClauses
    b Maybe SplitTree
    s Maybe Compiled
    forall a. Maybe a
    Nothing) Word32
    a Word32
    b Word32
    s Word32
    u Word32
    c Word32
    d Word32
    e Word32
    f Word32
    g Word32
    h Word32
    i Word32
    j Word32
    k
        valu [Word32
    2, Word32
    a, Word32
    b, Word32
    c, Word32
    d, Word32
    e, Word32
    f, Word32
    g, Word32
    h, Word32
    i, Word32
    j]             = (Int
     -> Int
     -> Maybe Clause
     -> [QName]
     -> Sort' Term
     -> Maybe [QName]
     -> IsAbstract
     -> [QName]
     -> Maybe QName
     -> Maybe QName
     -> Defn)
    -> Arrows
         (Constant
            Word32
            (Domains
               (Int
                -> Int
                -> Maybe Clause
                -> [QName]
                -> Sort' Term
                -> Maybe [QName]
                -> IsAbstract
                -> [QName]
                -> Maybe QName
                -> Maybe QName
                -> Defn)))
         (R (CoDomain
               (Int
                -> Int
                -> Maybe Clause
                -> [QName]
                -> Sort' Term
                -> Maybe [QName]
                -> IsAbstract
                -> [QName]
                -> Maybe QName
                -> Maybe QName
                -> Defn)))
    forall t.
    (VALU t (IsBase t),
     StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
    valuN Int
    -> Int
    -> Maybe Clause
    -> [QName]
    -> Sort' Term
    -> Maybe [QName]
    -> IsAbstract
    -> [QName]
    -> Maybe QName
    -> Maybe QName
    -> Defn
    Datatype Word32
    a Word32
    b Word32
    c Word32
    d Word32
    e Word32
    f Word32
    g Word32
    h Word32
    i Word32
    j
        valu [Word32
    3, Word32
    a, Word32
    b, Word32
    c, Word32
    d, Word32
    e, Word32
    f, Word32
    g, Word32
    h, Word32
    i, Word32
    j, Word32
    k, Word32
    l, Word32
    m]    = (Int
     -> Maybe Clause
     -> ConHead
     -> Bool
     -> [Dom QName]
     -> Telescope
     -> Maybe [QName]
     -> EtaEquality
     -> PatternOrCopattern
     -> Maybe Induction
     -> Maybe Bool
     -> IsAbstract
     -> CompKit
     -> Defn)
    -> Arrows
         (Constant
            Word32
            (Domains
               (Int
                -> Maybe Clause
                -> ConHead
                -> Bool
                -> [Dom QName]
                -> Telescope
                -> Maybe [QName]
                -> EtaEquality
                -> PatternOrCopattern
                -> Maybe Induction
                -> Maybe Bool
                -> IsAbstract
                -> CompKit
                -> Defn)))
         (R (CoDomain
               (Int
                -> Maybe Clause
                -> ConHead
                -> Bool
                -> [Dom QName]
                -> Telescope
                -> Maybe [QName]
                -> EtaEquality
                -> PatternOrCopattern
                -> Maybe Induction
                -> Maybe Bool
                -> IsAbstract
                -> CompKit
                -> Defn)))
    forall t.
    (VALU t (IsBase t),
     StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
    valuN Int
    -> Maybe Clause
    -> ConHead
    -> Bool
    -> [Dom QName]
    -> Telescope
    -> Maybe [QName]
    -> EtaEquality
    -> PatternOrCopattern
    -> Maybe Induction
    -> Maybe Bool
    -> IsAbstract
    -> CompKit
    -> Defn
    Record   Word32
    a Word32
    b Word32
    c Word32
    d Word32
    e Word32
    f Word32
    g Word32
    h Word32
    i Word32
    j Word32
    k Word32
    l Word32
    m
        valu [Word32
    4, Word32
    a, Word32
    b, Word32
    c, Word32
    d, Word32
    e, Word32
    f, Word32
    g, Word32
    h, Word32
    i, Word32
    j, Word32
    k]          = (Int
     -> Int
     -> ConHead
     -> QName
     -> IsAbstract
     -> CompKit
     -> Maybe [QName]
     -> [IsForced]
     -> Maybe [Bool]
     -> Bool
     -> Bool
     -> Defn)
    -> Arrows
         (Constant
            Word32
            (Domains
               (Int
                -> Int
                -> ConHead
                -> QName
                -> IsAbstract
                -> CompKit
                -> Maybe [QName]
                -> [IsForced]
                -> Maybe [Bool]
                -> Bool
                -> Bool
                -> Defn)))
         (R (CoDomain
               (Int
                -> Int
                -> ConHead
                -> QName
                -> IsAbstract
                -> CompKit
                -> Maybe [QName]
                -> [IsForced]
                -> Maybe [Bool]
                -> Bool
                -> Bool
                -> Defn)))
    forall t.
    (VALU t (IsBase t),
     StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
    valuN Int
    -> Int
    -> ConHead
    -> QName
    -> IsAbstract
    -> CompKit
    -> Maybe [QName]
    -> [IsForced]
    -> Maybe [Bool]
    -> Bool
    -> Bool
    -> Defn
    Constructor Word32
    a Word32
    b Word32
    c Word32
    d Word32
    e Word32
    f Word32
    g Word32
    h Word32
    i Word32
    j Word32
    k
        valu [Word32
    5, Word32
    a, Word32
    b, Word32
    c, Word32
    d, Word32
    e, Word32
    f]                         = (IsAbstract
     -> PrimitiveId
     -> [Clause]
     -> FunctionInverse
     -> Maybe CompiledClauses
     -> IsOpaque
     -> Defn)
    -> Arrows
         (Constant
            Word32
            (Domains
               (IsAbstract
                -> PrimitiveId
                -> [Clause]
                -> FunctionInverse
                -> Maybe CompiledClauses
                -> IsOpaque
                -> Defn)))
         (R (CoDomain
               (IsAbstract
                -> PrimitiveId
                -> [Clause]
                -> FunctionInverse
                -> Maybe CompiledClauses
                -> IsOpaque
                -> Defn)))
    forall t.
    (VALU t (IsBase t),
     StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
    valuN IsAbstract
    -> PrimitiveId
    -> [Clause]
    -> FunctionInverse
    -> Maybe CompiledClauses
    -> IsOpaque
    -> Defn
    Primitive   Word32
    a Word32
    b Word32
    c Word32
    d Word32
    e Word32
    f
        valu [Word32
    6, Word32
    a, Word32
    b]                                     = (BuiltinSort -> Sort' Term -> Defn)
    -> Arrows
         (Constant Word32 (Domains (BuiltinSort -> Sort' Term -> Defn)))
         (R (CoDomain (BuiltinSort -> Sort' Term -> Defn)))
    forall t.
    (VALU t (IsBase t),
     StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
    valuN BuiltinSort -> Sort' Term -> Defn
    PrimitiveSort Word32
    a Word32
    b
        valu [Word32
    7, Word32
    a]                                        = (NumGeneralizableArgs -> Defn)
    -> Arrows
         (Constant Word32 (Domains (NumGeneralizableArgs -> Defn)))
         (R (CoDomain (NumGeneralizableArgs -> Defn)))
    forall t.
    (VALU t (IsBase t),
     StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
    valuN NumGeneralizableArgs -> Defn
    GeneralizableVar Word32
    a
        valu [Word32
    8, Word32
    a]                                        = (Int -> Defn)
    -> Arrows
         (Constant Word32 (Domains (Int -> Defn)))
         (R (CoDomain (Int -> Defn)))
    forall t.
    (VALU t (IsBase t),
     StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
    valuN Int -> Defn
    DataOrRecSig Word32
    a
        valu [Word32]
    _                                             = R Defn
    forall a. R a
    malformed

    instance EmbPrj LazySplit where
      icod_ :: LazySplit -> S Word32
    icod_ LazySplit
    StrictSplit = LazySplit -> Arrows (Domains LazySplit) (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Domains t) (S Word32)
    icodeN' LazySplit
    StrictSplit
      icod_ LazySplit
    LazySplit   = Word32 -> LazySplit -> Arrows (Domains LazySplit) (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    Word32 -> t -> Arrows (Domains t) (S Word32)
    icodeN Word32
    0 LazySplit
    LazySplit

      value :: Word32 -> R LazySplit
    value = ([Word32] -> R LazySplit) -> Word32 -> R LazySplit
    forall a. EmbPrj a => ([Word32] -> R a) -> Word32 -> R a
    vcase [Word32] -> R LazySplit
    forall {a}. (Eq a, Num a) => [a] -> R LazySplit
    valu where
        valu :: [a]
    -> Arrows
         (Constant Word32 (Domains LazySplit)) (R (CoDomain LazySplit))
    valu []  = LazySplit
    -> Arrows
         (Constant Word32 (Domains LazySplit)) (R (CoDomain LazySplit))
    forall t.
    (VALU t (IsBase t),
     StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
    valuN LazySplit
    StrictSplit
        valu [a
    0] = LazySplit
    -> Arrows
         (Constant Word32 (Domains LazySplit)) (R (CoDomain LazySplit))
    forall t.
    (VALU t (IsBase t),
     StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
    valuN LazySplit
    LazySplit
        valu [a]
    _   = R LazySplit
    Arrows
      (Constant Word32 (Domains LazySplit)) (R (CoDomain LazySplit))
    forall a. R a
    malformed

    instance EmbPrj SplitTag where
      icod_ :: SplitTag -> S Word32
    icod_ (SplitCon QName
    c)  = Word32
    -> (QName -> SplitTag)
    -> Arrows (Domains (QName -> SplitTag)) (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    Word32 -> t -> Arrows (Domains t) (S Word32)
    icodeN Word32
    0 QName -> SplitTag
    SplitCon QName
    c
      icod_ (SplitLit Literal
    l)  = Word32
    -> (Literal -> SplitTag)
    -> Arrows (Domains (Literal -> SplitTag)) (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    Word32 -> t -> Arrows (Domains t) (S Word32)
    icodeN Word32
    1 Literal -> SplitTag
    SplitLit Literal
    l
      icod_ SplitTag
    SplitCatchall = SplitTag -> Arrows (Domains SplitTag) (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Domains t) (S Word32)
    icodeN' SplitTag
    SplitCatchall

      value :: Word32 -> R SplitTag
    value = ([Word32] -> R SplitTag) -> Word32 -> R SplitTag
    forall a. EmbPrj a => ([Word32] -> R a) -> Word32 -> R a
    vcase [Word32] -> R SplitTag
    valu where
        valu :: [Word32]
    -> Arrows
         (Constant Word32 (Domains SplitTag)) (R (CoDomain SplitTag))
    valu []     = SplitTag
    -> Arrows
         (Constant Word32 (Domains SplitTag)) (R (CoDomain SplitTag))
    forall t.
    (VALU t (IsBase t),
     StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
    valuN SplitTag
    SplitCatchall
        valu [Word32
    0, Word32
    c] = (QName -> SplitTag)
    -> Arrows
         (Constant Word32 (Domains (QName -> SplitTag)))
         (R (CoDomain (QName -> SplitTag)))
    forall t.
    (VALU t (IsBase t),
     StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
    valuN QName -> SplitTag
    SplitCon Word32
    c
        valu [Word32
    1, Word32
    l] = (Literal -> SplitTag)
    -> Arrows
         (Constant Word32 (Domains (Literal -> SplitTag)))
         (R (CoDomain (Literal -> SplitTag)))
    forall t.
    (VALU t (IsBase t),
     StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
    valuN Literal -> SplitTag
    SplitLit Word32
    l
        valu [Word32]
    _      = R SplitTag
    Arrows (Constant Word32 (Domains SplitTag)) (R (CoDomain SplitTag))
    forall a. R a
    malformed

    instance EmbPrj a => EmbPrj (SplitTree' a) where
      icod_ :: SplitTree' a -> S Word32
    icod_ (SplittingDone Int
    a) = (Int -> SplitTree' (ZonkAny 10))
    -> Arrows (Domains (Int -> SplitTree' (ZonkAny 10))) (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Domains t) (S Word32)
    icodeN' Int -> SplitTree' (ZonkAny 10)
    forall a. Int -> SplitTree' a
    SplittingDone Int
    a
      icod_ (SplitAt Arg Int
    a LazySplit
    b SplitTrees' a
    c)   = Word32
    -> (Arg Int -> LazySplit -> SplitTrees' a -> SplitTree' a)
    -> Arrows
         (Domains (Arg Int -> LazySplit -> SplitTrees' a -> SplitTree' a))
         (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    Word32 -> t -> Arrows (Domains t) (S Word32)
    icodeN Word32
    0 Arg Int -> LazySplit -> SplitTrees' a -> SplitTree' a
    forall a. Arg Int -> LazySplit -> SplitTrees' a -> SplitTree' a
    SplitAt Arg Int
    a LazySplit
    b SplitTrees' a
    c

      value :: Word32 -> R (SplitTree' a)
    value = ([Word32] -> R (SplitTree' a)) -> Word32 -> R (SplitTree' a)
    forall a. EmbPrj a => ([Word32] -> R a) -> Word32 -> R a
    vcase [Word32] -> R (SplitTree' a)
    forall {a}. EmbPrj a => [Word32] -> R (SplitTree' a)
    valu where
        valu :: [Word32] -> R (SplitTree' a)
    valu [Word32
    a]          = (Int -> SplitTree' a)
    -> Arrows
         (Constant Word32 (Domains (Int -> SplitTree' a)))
         (R (CoDomain (Int -> SplitTree' a)))
    forall t.
    (VALU t (IsBase t),
     StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
    valuN Int -> SplitTree' a
    forall a. Int -> SplitTree' a
    SplittingDone Word32
    a
        valu [Word32
    0, Word32
    a, Word32
    b, Word32
    c] = (Arg Int -> LazySplit -> SplitTrees' a -> SplitTree' a)
    -> Arrows
         (Constant
            Word32
            (Domains (Arg Int -> LazySplit -> SplitTrees' a -> SplitTree' a)))
         (R (CoDomain
               (Arg Int -> LazySplit -> SplitTrees' a -> SplitTree' a)))
    forall t.
    (VALU t (IsBase t),
     StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
    valuN Arg Int -> LazySplit -> SplitTrees' a -> SplitTree' a
    forall a. Arg Int -> LazySplit -> SplitTrees' a -> SplitTree' a
    SplitAt Word32
    a Word32
    b Word32
    c
        valu [Word32]
    _            = R (SplitTree' a)
    forall a. R a
    malformed

    instance EmbPrj FunctionFlag

    instance EmbPrj a => EmbPrj (WithArity a) where
      icod_ :: WithArity a -> S Word32
    icod_ (WithArity Int
    a a
    b) = (Int -> a -> WithArity a)
    -> Arrows (Domains (Int -> a -> WithArity a)) (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Domains t) (S Word32)
    icodeN' Int -> a -> WithArity a
    forall c. Int -> c -> WithArity c
    WithArity Int
    a a
    b

      value :: Word32 -> R (WithArity a)
    value = (Int -> a -> WithArity a)
    -> Word32 -> R (CoDomain (Int -> a -> WithArity a))
    forall t.
    (VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
    t -> Word32 -> R (CoDomain t)
    valueN Int -> a -> WithArity a
    forall c. Int -> c -> WithArity c
    WithArity

    instance EmbPrj a => EmbPrj (Case a) where
      icod_ :: Case a -> S Word32
    icod_ (Branches Bool
    a Map QName (WithArity a)
    b Maybe (ConHead, WithArity a)
    c Map Literal a
    d Maybe a
    e Maybe Bool
    f Bool
    g) = (Bool
     -> Map QName (WithArity a)
     -> Maybe (ConHead, WithArity a)
     -> Map Literal a
     -> Maybe a
     -> Maybe Bool
     -> Bool
     -> Case a)
    -> Arrows
         (Domains
            (Bool
             -> Map QName (WithArity a)
             -> Maybe (ConHead, WithArity a)
             -> Map Literal a
             -> Maybe a
             -> Maybe Bool
             -> Bool
             -> Case a))
         (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Domains t) (S Word32)
    icodeN' Bool
    -> Map QName (WithArity a)
    -> Maybe (ConHead, WithArity a)
    -> Map Literal a
    -> Maybe a
    -> Maybe Bool
    -> Bool
    -> Case a
    forall c.
    Bool
    -> Map QName (WithArity c)
    -> Maybe (ConHead, WithArity c)
    -> Map Literal c
    -> Maybe c
    -> Maybe Bool
    -> Bool
    -> Case c
    Branches Bool
    a Map QName (WithArity a)
    b Maybe (ConHead, WithArity a)
    c Map Literal a
    d Maybe a
    e Maybe Bool
    f Bool
    g

      value :: Word32 -> R (Case a)
    value = (Bool
     -> Map QName (WithArity a)
     -> Maybe (ConHead, WithArity a)
     -> Map Literal a
     -> Maybe a
     -> Maybe Bool
     -> Bool
     -> Case a)
    -> Word32
    -> R (CoDomain
            (Bool
             -> Map QName (WithArity a)
             -> Maybe (ConHead, WithArity a)
             -> Map Literal a
             -> Maybe a
             -> Maybe Bool
             -> Bool
             -> Case a))
    forall t.
    (VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
    t -> Word32 -> R (CoDomain t)
    valueN Bool
    -> Map QName (WithArity a)
    -> Maybe (ConHead, WithArity a)
    -> Map Literal a
    -> Maybe a
    -> Maybe Bool
    -> Bool
    -> Case a
    forall c.
    Bool
    -> Map QName (WithArity c)
    -> Maybe (ConHead, WithArity c)
    -> Map Literal c
    -> Maybe c
    -> Maybe Bool
    -> Bool
    -> Case c
    Branches

    -- Opaque blocks are serialised in an abbreviated manner: We only need
    -- the enclosed definitions (3rd argument) and parent (4th argument) to
    -- compute the transitive closure during scope checking, never
    -- afterwards.
    instance EmbPrj OpaqueBlock where
      icod_ :: OpaqueBlock -> S Word32
    icod_ (OpaqueBlock OpaqueId
    id HashSet QName
    uf HashSet QName
    _ Maybe OpaqueId
    _ Range
    r) =
        (OpaqueId -> [QName] -> Range -> OpaqueBlock)
    -> Arrows
         (Domains (OpaqueId -> [QName] -> Range -> OpaqueBlock)) (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Domains t) (S Word32)
    icodeN' (\OpaqueId
    id [QName]
    uf ->
          let !unfolding :: HashSet QName
    unfolding = [QName] -> HashSet QName
    forall a. (Eq a, Hashable a) => [a] -> HashSet a
    HashSet.fromList [QName]
    uf
          in OpaqueId
    -> HashSet QName
    -> HashSet QName
    -> Maybe OpaqueId
    -> Range
    -> OpaqueBlock
    OpaqueBlock OpaqueId
    id HashSet QName
    unfolding HashSet QName
    forall a. Monoid a => a
    mempty Maybe OpaqueId
    forall a. Maybe a
    Nothing)
        OpaqueId
    id (HashSet QName -> [QName]
    forall a. HashSet a -> [a]
    HashSet.toList HashSet QName
    uf) Range
    r

      value :: Word32 -> R OpaqueBlock
    value = (OpaqueId -> [QName] -> Range -> OpaqueBlock)
    -> Word32
    -> R (CoDomain (OpaqueId -> [QName] -> Range -> OpaqueBlock))
    forall t.
    (VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
    t -> Word32 -> R (CoDomain t)
    valueN (\OpaqueId
    id [QName]
    uf -> let !unfolding :: HashSet QName
    unfolding = [QName] -> HashSet QName
    forall a. (Eq a, Hashable a) => [a] -> HashSet a
    HashSet.fromList [QName]
    uf
                                in OpaqueId
    -> HashSet QName
    -> HashSet QName
    -> Maybe OpaqueId
    -> Range
    -> OpaqueBlock
    OpaqueBlock OpaqueId
    id HashSet QName
    unfolding HashSet QName
    forall a. Monoid a => a
    mempty Maybe OpaqueId
    forall a. Maybe a
    Nothing)

    instance EmbPrj CompiledClauses where
      icod_ :: CompiledClauses -> S Word32
    icod_ (Fail [Arg ArgName]
    a)   = ([Arg ArgName] -> CompiledClauses' (ZonkAny 9))
    -> Arrows
         (Domains ([Arg ArgName] -> CompiledClauses' (ZonkAny 9)))
         (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Domains t) (S Word32)
    icodeN' [Arg ArgName] -> CompiledClauses' (ZonkAny 9)
    forall a. [Arg ArgName] -> CompiledClauses' a
    Fail [Arg ArgName]
    a
      icod_ (Done [Arg ArgName]
    a Term
    b) = ([Arg ArgName] -> Term -> CompiledClauses)
    -> Arrows
         (Domains ([Arg ArgName] -> Term -> CompiledClauses)) (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Domains t) (S Word32)
    icodeN' [Arg ArgName] -> Term -> CompiledClauses
    forall a. [Arg ArgName] -> a -> CompiledClauses' a
    Done [Arg ArgName]
    a (Term -> Term
    forall a. KillRange a => KillRangeT a
    P.killRange Term
    b)
      icod_ (Case Arg Int
    a Case CompiledClauses
    b) = Word32
    -> (Arg Int -> Case CompiledClauses -> CompiledClauses)
    -> Arrows
         (Domains (Arg Int -> Case CompiledClauses -> CompiledClauses))
         (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    Word32 -> t -> Arrows (Domains t) (S Word32)
    icodeN Word32
    2 Arg Int -> Case CompiledClauses -> CompiledClauses
    forall a.
    Arg Int -> Case (CompiledClauses' a) -> CompiledClauses' a
    Case Arg Int
    a Case CompiledClauses
    b

      value :: Word32 -> R CompiledClauses
    value = ([Word32] -> R CompiledClauses) -> Word32 -> R CompiledClauses
    forall a. EmbPrj a => ([Word32] -> R a) -> Word32 -> R a
    vcase [Word32] -> R CompiledClauses
    forall {a}.
    (EmbPrj a, EmbPrj (CompiledClauses' a)) =>
    [Word32] -> R (CompiledClauses' a)
    valu where
        valu :: [Word32] -> R (CompiledClauses' a)
    valu [Word32
    a]       = ([Arg ArgName] -> CompiledClauses' a)
    -> Arrows
         (Constant Word32 (Domains ([Arg ArgName] -> CompiledClauses' a)))
         (R (CoDomain ([Arg ArgName] -> CompiledClauses' a)))
    forall t.
    (VALU t (IsBase t),
     StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
    valuN [Arg ArgName] -> CompiledClauses' a
    forall a. [Arg ArgName] -> CompiledClauses' a
    Fail Word32
    a
        valu [Word32
    a, Word32
    b]    = ([Arg ArgName] -> a -> CompiledClauses' a)
    -> Arrows
         (Constant
            Word32 (Domains ([Arg ArgName] -> a -> CompiledClauses' a)))
         (R (CoDomain ([Arg ArgName] -> a -> CompiledClauses' a)))
    forall t.
    (VALU t (IsBase t),
     StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
    valuN [Arg ArgName] -> a -> CompiledClauses' a
    forall a. [Arg ArgName] -> a -> CompiledClauses' a
    Done Word32
    a Word32
    b
        valu [Word32
    2, Word32
    a, Word32
    b] = (Arg Int -> Case (CompiledClauses' a) -> CompiledClauses' a)
    -> Arrows
         (Constant
            Word32
            (Domains
               (Arg Int -> Case (CompiledClauses' a) -> CompiledClauses' a)))
         (R (CoDomain
               (Arg Int -> Case (CompiledClauses' a) -> CompiledClauses' a)))
    forall t.
    (VALU t (IsBase t),
     StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
    valuN Arg Int -> Case (CompiledClauses' a) -> CompiledClauses' a
    forall a.
    Arg Int -> Case (CompiledClauses' a) -> CompiledClauses' a
    Case Word32
    a Word32
    b
        valu [Word32]
    _         = R (CompiledClauses' a)
    forall a. R a
    malformed

    instance EmbPrj a => EmbPrj (FunctionInverse' a) where
      icod_ :: FunctionInverse' a -> S Word32
    icod_ FunctionInverse' a
    NotInjective = FunctionInverse' (ZonkAny 8)
    -> Arrows (Domains (FunctionInverse' (ZonkAny 8))) (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Domains t) (S Word32)
    icodeN' FunctionInverse' (ZonkAny 8)
    forall c. FunctionInverse' c
    NotInjective
      icod_ (Inverse InversionMap a
    a)  = (InversionMap a -> FunctionInverse' a)
    -> Arrows
         (Domains (InversionMap a -> FunctionInverse' a)) (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Domains t) (S Word32)
    icodeN' InversionMap a -> FunctionInverse' a
    forall c. InversionMap c -> FunctionInverse' c
    Inverse InversionMap a
    a

      value :: Word32 -> R (FunctionInverse' a)
    value = ([Word32] -> R (FunctionInverse' a))
    -> Word32 -> R (FunctionInverse' a)
    forall a. EmbPrj a => ([Word32] -> R a) -> Word32 -> R a
    vcase [Word32] -> R (FunctionInverse' a)
    forall {c}.
    (EmbPrj [c], Typeable c) =>
    [Word32] -> StateT St IO (FunctionInverse' c)
    valu where
        valu :: [Word32]
    -> Arrows
         (Constant Word32 (Domains (FunctionInverse' c)))
         (R (CoDomain (FunctionInverse' c)))
    valu []  = FunctionInverse' c
    -> Arrows
         (Constant Word32 (Domains (FunctionInverse' c)))
         (R (CoDomain (FunctionInverse' c)))
    forall t.
    (VALU t (IsBase t),
     StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
    valuN FunctionInverse' c
    forall c. FunctionInverse' c
    NotInjective
        valu [Word32
    a] = (InversionMap c -> FunctionInverse' c)
    -> Arrows
         (Constant Word32 (Domains (InversionMap c -> FunctionInverse' c)))
         (R (CoDomain (InversionMap c -> FunctionInverse' c)))
    forall t.
    (VALU t (IsBase t),
     StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
    valuN InversionMap c -> FunctionInverse' c
    forall c. InversionMap c -> FunctionInverse' c
    Inverse Word32
    a
        valu [Word32]
    _   = StateT St IO (FunctionInverse' c)
    Arrows
      (Constant Word32 (Domains (FunctionInverse' c)))
      (R (CoDomain (FunctionInverse' c)))
    forall a. R a
    malformed

    instance EmbPrj TermHead where
      icod_ :: TermHead -> S Word32
    icod_ TermHead
    SortHead     = TermHead -> Arrows (Domains TermHead) (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Domains t) (S Word32)
    icodeN' TermHead
    SortHead
      icod_ TermHead
    PiHead       = Word32 -> TermHead -> Arrows (Domains TermHead) (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    Word32 -> t -> Arrows (Domains t) (S Word32)
    icodeN Word32
    1 TermHead
    PiHead
      icod_ (ConsHead QName
    a) = Word32
    -> (QName -> TermHead)
    -> Arrows (Domains (QName -> TermHead)) (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    Word32 -> t -> Arrows (Domains t) (S Word32)
    icodeN Word32
    2 QName -> TermHead
    ConsHead QName
    a
      icod_ (VarHead Int
    a)  = Word32
    -> (Int -> TermHead)
    -> Arrows (Domains (Int -> TermHead)) (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    Word32 -> t -> Arrows (Domains t) (S Word32)
    icodeN Word32
    3 Int -> TermHead
    VarHead Int
    a
      icod_ TermHead
    UnknownHead  = Word32 -> TermHead -> Arrows (Domains TermHead) (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    Word32 -> t -> Arrows (Domains t) (S Word32)
    icodeN Word32
    4 TermHead
    UnknownHead

      value :: Word32 -> R TermHead
    value = ([Word32] -> R TermHead) -> Word32 -> R TermHead
    forall a. EmbPrj a => ([Word32] -> R a) -> Word32 -> R a
    vcase [Word32] -> R TermHead
    valu where
        valu :: [Word32]
    -> Arrows
         (Constant Word32 (Domains TermHead)) (R (CoDomain TermHead))
    valu []     = TermHead
    -> Arrows
         (Constant Word32 (Domains TermHead)) (R (CoDomain TermHead))
    forall t.
    (VALU t (IsBase t),
     StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
    valuN TermHead
    SortHead
        valu [Word32
    1]    = TermHead
    -> Arrows
         (Constant Word32 (Domains TermHead)) (R (CoDomain TermHead))
    forall t.
    (VALU t (IsBase t),
     StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
    valuN TermHead
    PiHead
        valu [Word32
    2, Word32
    a] = (QName -> TermHead)
    -> Arrows
         (Constant Word32 (Domains (QName -> TermHead)))
         (R (CoDomain (QName -> TermHead)))
    forall t.
    (VALU t (IsBase t),
     StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
    valuN QName -> TermHead
    ConsHead Word32
    a
        valu [Word32
    3, Word32
    a] = (Int -> TermHead)
    -> Arrows
         (Constant Word32 (Domains (Int -> TermHead)))
         (R (CoDomain (Int -> TermHead)))
    forall t.
    (VALU t (IsBase t),
     StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
    valuN Int -> TermHead
    VarHead Word32
    a
        valu [Word32
    4]    = TermHead
    -> Arrows
         (Constant Word32 (Domains TermHead)) (R (CoDomain TermHead))
    forall t.
    (VALU t (IsBase t),
     StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
    valuN TermHead
    UnknownHead
        valu [Word32]
    _      = R TermHead
    Arrows (Constant Word32 (Domains TermHead)) (R (CoDomain TermHead))
    forall a. R a
    malformed

    instance EmbPrj I.Clause where
      icod_ :: Clause -> S Word32
    icod_ (Clause Range
    a Range
    b Telescope
    c NAPs
    d Maybe Term
    e Maybe (Arg Type)
    f Catchall
    g Maybe Bool
    h Maybe Bool
    i ExpandedEllipsis
    j Maybe ModuleName
    k) = (Range
     -> Range
     -> Telescope
     -> NAPs
     -> Maybe Term
     -> Maybe (Arg Type)
     -> Catchall
     -> Maybe Bool
     -> Maybe Bool
     -> ExpandedEllipsis
     -> Maybe ModuleName
     -> Clause)
    -> Arrows
         (Domains
            (Range
             -> Range
             -> Telescope
             -> NAPs
             -> Maybe Term
             -> Maybe (Arg Type)
             -> Catchall
             -> Maybe Bool
             -> Maybe Bool
             -> ExpandedEllipsis
             -> Maybe ModuleName
             -> Clause))
         (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Domains t) (S Word32)
    icodeN' Range
    -> Range
    -> Telescope
    -> NAPs
    -> Maybe Term
    -> Maybe (Arg Type)
    -> Catchall
    -> Maybe Bool
    -> Maybe Bool
    -> ExpandedEllipsis
    -> Maybe ModuleName
    -> Clause
    Clause Range
    a Range
    b Telescope
    c NAPs
    d Maybe Term
    e Maybe (Arg Type)
    f Catchall
    g Maybe Bool
    h Maybe Bool
    i ExpandedEllipsis
    j Maybe ModuleName
    k

      value :: Word32 -> R Clause
    value = (Range
     -> Range
     -> Telescope
     -> NAPs
     -> Maybe Term
     -> Maybe (Arg Type)
     -> Catchall
     -> Maybe Bool
     -> Maybe Bool
     -> ExpandedEllipsis
     -> Maybe ModuleName
     -> Clause)
    -> Word32
    -> R (CoDomain
            (Range
             -> Range
             -> Telescope
             -> NAPs
             -> Maybe Term
             -> Maybe (Arg Type)
             -> Catchall
             -> Maybe Bool
             -> Maybe Bool
             -> ExpandedEllipsis
             -> Maybe ModuleName
             -> Clause))
    forall t.
    (VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
    t -> Word32 -> R (CoDomain t)
    valueN Range
    -> Range
    -> Telescope
    -> NAPs
    -> Maybe Term
    -> Maybe (Arg Type)
    -> Catchall
    -> Maybe Bool
    -> Maybe Bool
    -> ExpandedEllipsis
    -> Maybe ModuleName
    -> Clause
    Clause

    instance EmbPrj I.ConPatternInfo where
      icod_ :: ConPatternInfo -> S Word32
    icod_ (ConPatternInfo PatternInfo
    a Bool
    b Bool
    c Maybe (Arg Type)
    d Bool
    e) = (PatternInfo
     -> Bool -> Bool -> Maybe (Arg Type) -> Bool -> ConPatternInfo)
    -> Arrows
         (Domains
            (PatternInfo
             -> Bool -> Bool -> Maybe (Arg Type) -> Bool -> ConPatternInfo))
         (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Domains t) (S Word32)
    icodeN' PatternInfo
    -> Bool -> Bool -> Maybe (Arg Type) -> Bool -> ConPatternInfo
    ConPatternInfo PatternInfo
    a Bool
    b Bool
    c Maybe (Arg Type)
    d Bool
    e

      value :: Word32 -> R ConPatternInfo
    value = (PatternInfo
     -> Bool -> Bool -> Maybe (Arg Type) -> Bool -> ConPatternInfo)
    -> Word32
    -> R (CoDomain
            (PatternInfo
             -> Bool -> Bool -> Maybe (Arg Type) -> Bool -> ConPatternInfo))
    forall t.
    (VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
    t -> Word32 -> R (CoDomain t)
    valueN PatternInfo
    -> Bool -> Bool -> Maybe (Arg Type) -> Bool -> ConPatternInfo
    ConPatternInfo

    instance EmbPrj I.DBPatVar where
      icod_ :: DBPatVar -> S Word32
    icod_ (DBPatVar ArgName
    a Int
    b) = (ArgName -> Int -> DBPatVar)
    -> Arrows (Domains (ArgName -> Int -> DBPatVar)) (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Domains t) (S Word32)
    icodeN' ArgName -> Int -> DBPatVar
    DBPatVar ArgName
    a Int
    b

      value :: Word32 -> R DBPatVar
    value = (ArgName -> Int -> DBPatVar)
    -> Word32 -> R (CoDomain (ArgName -> Int -> DBPatVar))
    forall t.
    (VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
    t -> Word32 -> R (CoDomain t)
    valueN ArgName -> Int -> DBPatVar
    DBPatVar

    instance EmbPrj I.PatternInfo where
      icod_ :: PatternInfo -> S Word32
    icod_ (PatternInfo PatOrigin
    a [Name]
    b) = (PatOrigin -> [Name] -> PatternInfo)
    -> Arrows (Domains (PatOrigin -> [Name] -> PatternInfo)) (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Domains t) (S Word32)
    icodeN' PatOrigin -> [Name] -> PatternInfo
    PatternInfo PatOrigin
    a [Name]
    b

      value :: Word32 -> R PatternInfo
    value = (PatOrigin -> [Name] -> PatternInfo)
    -> Word32 -> R (CoDomain (PatOrigin -> [Name] -> PatternInfo))
    forall t.
    (VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
    t -> Word32 -> R (CoDomain t)
    valueN PatOrigin -> [Name] -> PatternInfo
    PatternInfo

    instance EmbPrj I.PatOrigin where
      icod_ :: PatOrigin -> S Word32
    icod_ PatOrigin
    PatOSystem  = PatOrigin -> Arrows (Domains PatOrigin) (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Domains t) (S Word32)
    icodeN' PatOrigin
    PatOSystem
      icod_ PatOrigin
    PatOSplit   = Word32 -> PatOrigin -> Arrows (Domains PatOrigin) (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    Word32 -> t -> Arrows (Domains t) (S Word32)
    icodeN Word32
    1 PatOrigin
    PatOSplit
      icod_ (PatOVar Name
    a) = Word32
    -> (Name -> PatOrigin)
    -> Arrows (Domains (Name -> PatOrigin)) (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    Word32 -> t -> Arrows (Domains t) (S Word32)
    icodeN Word32
    2 Name -> PatOrigin
    PatOVar Name
    a
      icod_ PatOrigin
    PatODot     = Word32 -> PatOrigin -> Arrows (Domains PatOrigin) (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    Word32 -> t -> Arrows (Domains t) (S Word32)
    icodeN Word32
    3 PatOrigin
    PatODot
      icod_ PatOrigin
    PatOWild    = Word32 -> PatOrigin -> Arrows (Domains PatOrigin) (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    Word32 -> t -> Arrows (Domains t) (S Word32)
    icodeN Word32
    4 PatOrigin
    PatOWild
      icod_ PatOrigin
    PatOCon     = Word32 -> PatOrigin -> Arrows (Domains PatOrigin) (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    Word32 -> t -> Arrows (Domains t) (S Word32)
    icodeN Word32
    5 PatOrigin
    PatOCon
      icod_ PatOrigin
    PatORec     = Word32 -> PatOrigin -> Arrows (Domains PatOrigin) (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    Word32 -> t -> Arrows (Domains t) (S Word32)
    icodeN Word32
    6 PatOrigin
    PatORec
      icod_ PatOrigin
    PatOLit     = Word32 -> PatOrigin -> Arrows (Domains PatOrigin) (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    Word32 -> t -> Arrows (Domains t) (S Word32)
    icodeN Word32
    7 PatOrigin
    PatOLit
      icod_ PatOrigin
    PatOAbsurd  = Word32 -> PatOrigin -> Arrows (Domains PatOrigin) (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    Word32 -> t -> Arrows (Domains t) (S Word32)
    icodeN Word32
    8 PatOrigin
    PatOAbsurd
      icod_ (PatOSplitArg ArgName
    a) = Word32
    -> (ArgName -> PatOrigin)
    -> Arrows (Domains (ArgName -> PatOrigin)) (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    Word32 -> t -> Arrows (Domains t) (S Word32)
    icodeN Word32
    9 ArgName -> PatOrigin
    PatOSplitArg ArgName
    a

      value :: Word32 -> R PatOrigin
    value = ([Word32] -> R PatOrigin) -> Word32 -> R PatOrigin
    forall a. EmbPrj a => ([Word32] -> R a) -> Word32 -> R a
    vcase [Word32] -> R PatOrigin
    valu where
        valu :: [Word32]
    -> Arrows
         (Constant Word32 (Domains PatOrigin)) (R (CoDomain PatOrigin))
    valu []     = PatOrigin
    -> Arrows
         (Constant Word32 (Domains PatOrigin)) (R (CoDomain PatOrigin))
    forall t.
    (VALU t (IsBase t),
     StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
    valuN PatOrigin
    PatOSystem
        valu [Word32
    1]    = PatOrigin
    -> Arrows
         (Constant Word32 (Domains PatOrigin)) (R (CoDomain PatOrigin))
    forall t.
    (VALU t (IsBase t),
     StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
    valuN PatOrigin
    PatOSplit
        valu [Word32
    2, Word32
    a] = (Name -> PatOrigin)
    -> Arrows
         (Constant Word32 (Domains (Name -> PatOrigin)))
         (R (CoDomain (Name -> PatOrigin)))
    forall t.
    (VALU t (IsBase t),
     StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
    valuN Name -> PatOrigin
    PatOVar Word32
    a
        valu [Word32
    3]    = PatOrigin
    -> Arrows
         (Constant Word32 (Domains PatOrigin)) (R (CoDomain PatOrigin))
    forall t.
    (VALU t (IsBase t),
     StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
    valuN PatOrigin
    PatODot
        valu [Word32
    4]    = PatOrigin
    -> Arrows
         (Constant Word32 (Domains PatOrigin)) (R (CoDomain PatOrigin))
    forall t.
    (VALU t (IsBase t),
     StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
    valuN PatOrigin
    PatOWild
        valu [Word32
    5]    = PatOrigin
    -> Arrows
         (Constant Word32 (Domains PatOrigin)) (R (CoDomain PatOrigin))
    forall t.
    (VALU t (IsBase t),
     StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
    valuN PatOrigin
    PatOCon
        valu [Word32
    6]    = PatOrigin
    -> Arrows
         (Constant Word32 (Domains PatOrigin)) (R (CoDomain PatOrigin))
    forall t.
    (VALU t (IsBase t),
     StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
    valuN PatOrigin
    PatORec
        valu [Word32
    7]    = PatOrigin
    -> Arrows
         (Constant Word32 (Domains PatOrigin)) (R (CoDomain PatOrigin))
    forall t.
    (VALU t (IsBase t),
     StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
    valuN PatOrigin
    PatOLit
        valu [Word32
    8]    = PatOrigin
    -> Arrows
         (Constant Word32 (Domains PatOrigin)) (R (CoDomain PatOrigin))
    forall t.
    (VALU t (IsBase t),
     StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
    valuN PatOrigin
    PatOAbsurd
        valu [Word32
    9, Word32
    a] = (ArgName -> PatOrigin)
    -> Arrows
         (Constant Word32 (Domains (ArgName -> PatOrigin)))
         (R (CoDomain (ArgName -> PatOrigin)))
    forall t.
    (VALU t (IsBase t),
     StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
    valuN ArgName -> PatOrigin
    PatOSplitArg Word32
    a
        valu [Word32]
    _      = R PatOrigin
    Arrows
      (Constant Word32 (Domains PatOrigin)) (R (CoDomain PatOrigin))
    forall a. R a
    malformed

    instance EmbPrj a => EmbPrj (I.Pattern' a) where
      icod_ :: Pattern' a -> S Word32
    icod_ (VarP PatternInfo
    a a
    b  ) = Word32
    -> (PatternInfo -> a -> Pattern' a)
    -> Arrows (Domains (PatternInfo -> a -> Pattern' a)) (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    Word32 -> t -> Arrows (Domains t) (S Word32)
    icodeN Word32
    0 PatternInfo -> a -> Pattern' a
    forall x. PatternInfo -> x -> Pattern' x
    VarP PatternInfo
    a a
    b
      icod_ (ConP ConHead
    a ConPatternInfo
    b [NamedArg (Pattern' a)]
    c) = Word32
    -> (ConHead
        -> ConPatternInfo -> [NamedArg (Pattern' a)] -> Pattern' a)
    -> Arrows
         (Domains
            (ConHead
             -> ConPatternInfo -> [NamedArg (Pattern' a)] -> Pattern' a))
         (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    Word32 -> t -> Arrows (Domains t) (S Word32)
    icodeN Word32
    1 ConHead -> ConPatternInfo -> [NamedArg (Pattern' a)] -> Pattern' a
    forall x.
    ConHead -> ConPatternInfo -> [NamedArg (Pattern' x)] -> Pattern' x
    ConP ConHead
    a ConPatternInfo
    b [NamedArg (Pattern' a)]
    c
      icod_ (LitP PatternInfo
    a Literal
    b  ) = Word32
    -> (PatternInfo -> Literal -> Pattern' (ZonkAny 5))
    -> Arrows
         (Domains (PatternInfo -> Literal -> Pattern' (ZonkAny 5)))
         (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    Word32 -> t -> Arrows (Domains t) (S Word32)
    icodeN Word32
    2 PatternInfo -> Literal -> Pattern' (ZonkAny 5)
    forall x. PatternInfo -> Literal -> Pattern' x
    LitP PatternInfo
    a Literal
    b
      icod_ (DotP PatternInfo
    a Term
    b  ) = Word32
    -> (PatternInfo -> Term -> Pattern' (ZonkAny 6))
    -> Arrows
         (Domains (PatternInfo -> Term -> Pattern' (ZonkAny 6))) (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    Word32 -> t -> Arrows (Domains t) (S Word32)
    icodeN Word32
    3 PatternInfo -> Term -> Pattern' (ZonkAny 6)
    forall x. PatternInfo -> Term -> Pattern' x
    DotP PatternInfo
    a Term
    b
      icod_ (ProjP ProjOrigin
    a QName
    b ) = Word32
    -> (ProjOrigin -> QName -> Pattern' (ZonkAny 7))
    -> Arrows
         (Domains (ProjOrigin -> QName -> Pattern' (ZonkAny 7))) (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    Word32 -> t -> Arrows (Domains t) (S Word32)
    icodeN Word32
    4 ProjOrigin -> QName -> Pattern' (ZonkAny 7)
    forall x. ProjOrigin -> QName -> Pattern' x
    ProjP ProjOrigin
    a QName
    b
      icod_ (IApplyP PatternInfo
    a Term
    b Term
    c a
    d) = Word32
    -> (PatternInfo -> Term -> Term -> a -> Pattern' a)
    -> Arrows
         (Domains (PatternInfo -> Term -> Term -> a -> Pattern' a))
         (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    Word32 -> t -> Arrows (Domains t) (S Word32)
    icodeN Word32
    5 PatternInfo -> Term -> Term -> a -> Pattern' a
    forall x. PatternInfo -> Term -> Term -> x -> Pattern' x
    IApplyP PatternInfo
    a Term
    b Term
    c a
    d
      icod_ (DefP PatternInfo
    a QName
    b [NamedArg (Pattern' a)]
    c) = Word32
    -> (PatternInfo -> QName -> [NamedArg (Pattern' a)] -> Pattern' a)
    -> Arrows
         (Domains
            (PatternInfo -> QName -> [NamedArg (Pattern' a)] -> Pattern' a))
         (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    Word32 -> t -> Arrows (Domains t) (S Word32)
    icodeN Word32
    6 PatternInfo -> QName -> [NamedArg (Pattern' a)] -> Pattern' a
    forall x.
    PatternInfo -> QName -> [NamedArg (Pattern' x)] -> Pattern' x
    DefP PatternInfo
    a QName
    b [NamedArg (Pattern' a)]
    c

      value :: Word32 -> R (Pattern' a)
    value = ([Word32] -> R (Pattern' a)) -> Word32 -> R (Pattern' a)
    forall a. EmbPrj a => ([Word32] -> R a) -> Word32 -> R a
    vcase [Word32] -> R (Pattern' a)
    forall {x}. EmbPrj x => [Word32] -> R (Pattern' x)
    valu where
        valu :: [Word32] -> R (Pattern' x)
    valu [Word32
    0, Word32
    a, Word32
    b] = (PatternInfo -> x -> Pattern' x)
    -> Arrows
         (Constant Word32 (Domains (PatternInfo -> x -> Pattern' x)))
         (R (CoDomain (PatternInfo -> x -> Pattern' x)))
    forall t.
    (VALU t (IsBase t),
     StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
    valuN PatternInfo -> x -> Pattern' x
    forall x. PatternInfo -> x -> Pattern' x
    VarP Word32
    a Word32
    b
        valu [Word32
    1, Word32
    a, Word32
    b, Word32
    c] = (ConHead
     -> ConPatternInfo -> [NamedArg (Pattern' x)] -> Pattern' x)
    -> Arrows
         (Constant
            Word32
            (Domains
               (ConHead
                -> ConPatternInfo -> [NamedArg (Pattern' x)] -> Pattern' x)))
         (R (CoDomain
               (ConHead
                -> ConPatternInfo -> [NamedArg (Pattern' x)] -> Pattern' x)))
    forall t.
    (VALU t (IsBase t),
     StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
    valuN ConHead -> ConPatternInfo -> [NamedArg (Pattern' x)] -> Pattern' x
    forall x.
    ConHead -> ConPatternInfo -> [NamedArg (Pattern' x)] -> Pattern' x
    ConP Word32
    a Word32
    b Word32
    c
        valu [Word32
    2, Word32
    a, Word32
    b] = (PatternInfo -> Literal -> Pattern' x)
    -> Arrows
         (Constant Word32 (Domains (PatternInfo -> Literal -> Pattern' x)))
         (R (CoDomain (PatternInfo -> Literal -> Pattern' x)))
    forall t.
    (VALU t (IsBase t),
     StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
    valuN PatternInfo -> Literal -> Pattern' x
    forall x. PatternInfo -> Literal -> Pattern' x
    LitP Word32
    a Word32
    b
        valu [Word32
    3, Word32
    a, Word32
    b] = (PatternInfo -> Term -> Pattern' x)
    -> Arrows
         (Constant Word32 (Domains (PatternInfo -> Term -> Pattern' x)))
         (R (CoDomain (PatternInfo -> Term -> Pattern' x)))
    forall t.
    (VALU t (IsBase t),
     StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
    valuN PatternInfo -> Term -> Pattern' x
    forall x. PatternInfo -> Term -> Pattern' x
    DotP Word32
    a Word32
    b
        valu [Word32
    4, Word32
    a, Word32
    b] = (ProjOrigin -> QName -> Pattern' x)
    -> Arrows
         (Constant Word32 (Domains (ProjOrigin -> QName -> Pattern' x)))
         (R (CoDomain (ProjOrigin -> QName -> Pattern' x)))
    forall t.
    (VALU t (IsBase t),
     StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
    valuN ProjOrigin -> QName -> Pattern' x
    forall x. ProjOrigin -> QName -> Pattern' x
    ProjP Word32
    a Word32
    b
        valu [Word32
    5, Word32
    a, Word32
    b, Word32
    c, Word32
    d] = (PatternInfo -> Term -> Term -> x -> Pattern' x)
    -> Arrows
         (Constant
            Word32 (Domains (PatternInfo -> Term -> Term -> x -> Pattern' x)))
         (R (CoDomain (PatternInfo -> Term -> Term -> x -> Pattern' x)))
    forall t.
    (VALU t (IsBase t),
     StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
    valuN PatternInfo -> Term -> Term -> x -> Pattern' x
    forall x. PatternInfo -> Term -> Term -> x -> Pattern' x
    IApplyP Word32
    a Word32
    b Word32
    c Word32
    d
        valu [Word32
    6, Word32
    a, Word32
    b, Word32
    c] = (PatternInfo -> QName -> [NamedArg (Pattern' x)] -> Pattern' x)
    -> Arrows
         (Constant
            Word32
            (Domains
               (PatternInfo -> QName -> [NamedArg (Pattern' x)] -> Pattern' x)))
         (R (CoDomain
               (PatternInfo -> QName -> [NamedArg (Pattern' x)] -> Pattern' x)))
    forall t.
    (VALU t (IsBase t),
     StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
    valuN PatternInfo -> QName -> [NamedArg (Pattern' x)] -> Pattern' x
    forall x.
    PatternInfo -> QName -> [NamedArg (Pattern' x)] -> Pattern' x
    DefP Word32
    a Word32
    b Word32
    c
        valu [Word32]
    _         = R (Pattern' x)
    forall a. R a
    malformed

    instance EmbPrj a => EmbPrj (Builtin a) where
      icod_ :: Builtin a -> S Word32
    icod_ (Prim    a
    a) = (a -> Builtin a) -> Arrows (Domains (a -> Builtin a)) (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Domains t) (S Word32)
    icodeN' a -> Builtin a
    forall pf. pf -> Builtin pf
    Prim a
    a
      icod_ (Builtin Term
    a) = Word32
    -> (Term -> Builtin (ZonkAny 3))
    -> Arrows (Domains (Term -> Builtin (ZonkAny 3))) (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    Word32 -> t -> Arrows (Domains t) (S Word32)
    icodeN Word32
    1 Term -> Builtin (ZonkAny 3)
    forall pf. Term -> Builtin pf
    Builtin Term
    a
      icod_ (BuiltinRewriteRelations Set QName
    a) = Word32
    -> (Set QName -> Builtin (ZonkAny 4))
    -> Arrows (Domains (Set QName -> Builtin (ZonkAny 4))) (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    Word32 -> t -> Arrows (Domains t) (S Word32)
    icodeN Word32
    2 Set QName -> Builtin (ZonkAny 4)
    forall pf. Set QName -> Builtin pf
    BuiltinRewriteRelations Set QName
    a

      value :: Word32 -> R (Builtin a)
    value = ([Word32] -> R (Builtin a)) -> Word32 -> R (Builtin a)
    forall a. EmbPrj a => ([Word32] -> R a) -> Word32 -> R a
    vcase [Word32] -> R (Builtin a)
    forall {pf}. EmbPrj pf => [Word32] -> R (Builtin pf)
    valu where
        valu :: [Word32] -> R (Builtin pf)
    valu [Word32
    a]    = (pf -> Builtin pf)
    -> Arrows
         (Constant Word32 (Domains (pf -> Builtin pf)))
         (R (CoDomain (pf -> Builtin pf)))
    forall t.
    (VALU t (IsBase t),
     StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
    valuN pf -> Builtin pf
    forall pf. pf -> Builtin pf
    Prim    Word32
    a
        valu [Word32
    1, Word32
    a] = (Term -> Builtin pf)
    -> Arrows
         (Constant Word32 (Domains (Term -> Builtin pf)))
         (R (CoDomain (Term -> Builtin pf)))
    forall t.
    (VALU t (IsBase t),
     StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
    valuN Term -> Builtin pf
    forall pf. Term -> Builtin pf
    Builtin Word32
    a
        valu [Word32
    2, Word32
    a] = (Set QName -> Builtin pf)
    -> Arrows
         (Constant Word32 (Domains (Set QName -> Builtin pf)))
         (R (CoDomain (Set QName -> Builtin pf)))
    forall t.
    (VALU t (IsBase t),
     StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
    valuN Set QName -> Builtin pf
    forall pf. Set QName -> Builtin pf
    BuiltinRewriteRelations Word32
    a
        valu [Word32]
    _      = R (Builtin pf)
    forall a. R a
    malformed

    instance EmbPrj a => EmbPrj (Substitution' a) where
      icod_ :: Substitution' a -> S Word32
    icod_ Substitution' a
    IdS                = Substitution' (ZonkAny 1)
    -> Arrows (Domains (Substitution' (ZonkAny 1))) (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Domains t) (S Word32)
    icodeN' Substitution' (ZonkAny 1)
    forall a. Substitution' a
    IdS
      icod_ (EmptyS Impossible
    a)         = (Impossible -> Substitution' (ZonkAny 2))
    -> Arrows
         (Domains (Impossible -> Substitution' (ZonkAny 2))) (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Domains t) (S Word32)
    icodeN' Impossible -> Substitution' (ZonkAny 2)
    forall a. Impossible -> Substitution' a
    EmptyS Impossible
    a
      icod_ (a
    a :# Substitution' a
    b)           = (a -> Substitution' a -> Substitution' a)
    -> Arrows
         (Domains (a -> Substitution' a -> Substitution' a)) (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Domains t) (S Word32)
    icodeN' a -> Substitution' a -> Substitution' a
    forall a. a -> Substitution' a -> Substitution' a
    (:#) a
    a Substitution' a
    b
      icod_ (Strengthen Impossible
    a Int
    b Substitution' a
    c) = Word32
    -> (Impossible -> Int -> Substitution' a -> Substitution' a)
    -> Arrows
         (Domains (Impossible -> Int -> Substitution' a -> Substitution' a))
         (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    Word32 -> t -> Arrows (Domains t) (S Word32)
    icodeN Word32
    0 Impossible -> Int -> Substitution' a -> Substitution' a
    forall a. Impossible -> Int -> Substitution' a -> Substitution' a
    Strengthen Impossible
    a Int
    b Substitution' a
    c
      icod_ (Wk Int
    a Substitution' a
    b)           = Word32
    -> (Int -> Substitution' a -> Substitution' a)
    -> Arrows
         (Domains (Int -> Substitution' a -> Substitution' a)) (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    Word32 -> t -> Arrows (Domains t) (S Word32)
    icodeN Word32
    1 Int -> Substitution' a -> Substitution' a
    forall a. Int -> Substitution' a -> Substitution' a
    Wk Int
    a Substitution' a
    b
      icod_ (Lift Int
    a Substitution' a
    b)         = Word32
    -> (Int -> Substitution' a -> Substitution' a)
    -> Arrows
         (Domains (Int -> Substitution' a -> Substitution' a)) (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    Word32 -> t -> Arrows (Domains t) (S Word32)
    icodeN Word32
    2 Int -> Substitution' a -> Substitution' a
    forall a. Int -> Substitution' a -> Substitution' a
    Lift Int
    a Substitution' a
    b

      value :: Word32 -> R (Substitution' a)
    value = ([Word32] -> R (Substitution' a)) -> Word32 -> R (Substitution' a)
    forall a. EmbPrj a => ([Word32] -> R a) -> Word32 -> R a
    vcase [Word32] -> R (Substitution' a)
    forall {a}. EmbPrj a => [Word32] -> StateT St IO (Substitution' a)
    valu where
        valu :: [Word32]
    -> Arrows
         (Constant Word32 (Domains (Substitution' a)))
         (R (CoDomain (Substitution' a)))
    valu []           = Substitution' a
    -> Arrows
         (Constant Word32 (Domains (Substitution' a)))
         (R (CoDomain (Substitution' a)))
    forall t.
    (VALU t (IsBase t),
     StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
    valuN Substitution' a
    forall a. Substitution' a
    IdS
        valu [Word32
    a]          = (Impossible -> Substitution' a)
    -> Arrows
         (Constant Word32 (Domains (Impossible -> Substitution' a)))
         (R (CoDomain (Impossible -> Substitution' a)))
    forall t.
    (VALU t (IsBase t),
     StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
    valuN Impossible -> Substitution' a
    forall a. Impossible -> Substitution' a
    EmptyS Word32
    a
        valu [Word32
    a, Word32
    b]       = (a -> Substitution' a -> Substitution' a)
    -> Arrows
         (Constant
            Word32 (Domains (a -> Substitution' a -> Substitution' a)))
         (R (CoDomain (a -> Substitution' a -> Substitution' a)))
    forall t.
    (VALU t (IsBase t),
     StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
    valuN a -> Substitution' a -> Substitution' a
    forall a. a -> Substitution' a -> Substitution' a
    (:#) Word32
    a Word32
    b
        valu [Word32
    0, Word32
    a, Word32
    b, Word32
    c] = (Impossible -> Int -> Substitution' a -> Substitution' a)
    -> Arrows
         (Constant
            Word32
            (Domains
               (Impossible -> Int -> Substitution' a -> Substitution' a)))
         (R (CoDomain
               (Impossible -> Int -> Substitution' a -> Substitution' a)))
    forall t.
    (VALU t (IsBase t),
     StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
    valuN Impossible -> Int -> Substitution' a -> Substitution' a
    forall a. Impossible -> Int -> Substitution' a -> Substitution' a
    Strengthen Word32
    a Word32
    b Word32
    c
        valu [Word32
    1, Word32
    a, Word32
    b]    = (Int -> Substitution' a -> Substitution' a)
    -> Arrows
         (Constant
            Word32 (Domains (Int -> Substitution' a -> Substitution' a)))
         (R (CoDomain (Int -> Substitution' a -> Substitution' a)))
    forall t.
    (VALU t (IsBase t),
     StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
    valuN Int -> Substitution' a -> Substitution' a
    forall a. Int -> Substitution' a -> Substitution' a
    Wk Word32
    a Word32
    b
        valu [Word32
    2, Word32
    a, Word32
    b]    = (Int -> Substitution' a -> Substitution' a)
    -> Arrows
         (Constant
            Word32 (Domains (Int -> Substitution' a -> Substitution' a)))
         (R (CoDomain (Int -> Substitution' a -> Substitution' a)))
    forall t.
    (VALU t (IsBase t),
     StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
    valuN Int -> Substitution' a -> Substitution' a
    forall a. Int -> Substitution' a -> Substitution' a
    Lift Word32
    a Word32
    b
        valu [Word32]
    _            = StateT St IO (Substitution' a)
    Arrows
      (Constant Word32 (Domains (Substitution' a)))
      (R (CoDomain (Substitution' a)))
    forall a. R a
    malformed

    instance EmbPrj Instantiation where
      icod_ :: Instantiation -> S Word32
    icod_ (Instantiation [Arg ArgName]
    a Term
    b) = ([Arg ArgName] -> Term -> Instantiation)
    -> Arrows
         (Domains ([Arg ArgName] -> Term -> Instantiation)) (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Domains t) (S Word32)
    icodeN' [Arg ArgName] -> Term -> Instantiation
    Instantiation [Arg ArgName]
    a Term
    b
      value :: Word32 -> R Instantiation
    value = ([Arg ArgName] -> Term -> Instantiation)
    -> Word32 -> R (CoDomain ([Arg ArgName] -> Term -> Instantiation))
    forall t.
    (VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
    t -> Word32 -> R (CoDomain t)
    valueN [Arg ArgName] -> Term -> Instantiation
    Instantiation

    instance EmbPrj Comparison where
      icod_ :: Comparison -> S Word32
    icod_ Comparison
    CmpEq  = Comparison -> Arrows (Domains Comparison) (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Domains t) (S Word32)
    icodeN' Comparison
    CmpEq
      icod_ Comparison
    CmpLeq = Word32 -> Comparison -> Arrows (Domains Comparison) (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    Word32 -> t -> Arrows (Domains t) (S Word32)
    icodeN Word32
    0 Comparison
    CmpLeq

      value :: Word32 -> R Comparison
    value = ([Word32] -> R Comparison) -> Word32 -> R Comparison
    forall a. EmbPrj a => ([Word32] -> R a) -> Word32 -> R a
    vcase [Word32] -> R Comparison
    forall {a}. (Eq a, Num a) => [a] -> R Comparison
    valu
        where
        valu :: [a]
    -> Arrows
         (Constant Word32 (Domains Comparison)) (R (CoDomain Comparison))
    valu []  = Comparison
    -> Arrows
         (Constant Word32 (Domains Comparison)) (R (CoDomain Comparison))
    forall t.
    (VALU t (IsBase t),
     StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
    valuN Comparison
    CmpEq
        valu [a
    0] = Comparison
    -> Arrows
         (Constant Word32 (Domains Comparison)) (R (CoDomain Comparison))
    forall t.
    (VALU t (IsBase t),
     StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
    valuN Comparison
    CmpLeq
        valu [a]
    _   = R Comparison
    Arrows
      (Constant Word32 (Domains Comparison)) (R (CoDomain Comparison))
    forall a. R a
    malformed

    instance EmbPrj a => EmbPrj (Judgement a) where
      icod_ :: Judgement a -> S Word32
    icod_ (HasType a
    a Comparison
    b Type
    c) = (a -> Comparison -> Type -> Judgement a)
    -> Arrows
         (Domains (a -> Comparison -> Type -> Judgement a)) (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Domains t) (S Word32)
    icodeN' a -> Comparison -> Type -> Judgement a
    forall a. a -> Comparison -> Type -> Judgement a
    HasType a
    a Comparison
    b Type
    c
      icod_ (IsSort a
    a Type
    b)    = (a -> Type -> Judgement a)
    -> Arrows (Domains (a -> Type -> Judgement a)) (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Domains t) (S Word32)
    icodeN' a -> Type -> Judgement a
    forall a. a -> Type -> Judgement a
    IsSort a
    a Type
    b

      value :: Word32 -> R (Judgement a)
    value = ([Word32] -> R (Judgement a)) -> Word32 -> R (Judgement a)
    forall a. EmbPrj a => ([Word32] -> R a) -> Word32 -> R a
    vcase [Word32] -> R (Judgement a)
    forall {a}. EmbPrj a => [Word32] -> R (Judgement a)
    valu
        where
        valu :: [Word32] -> R (Judgement a)
    valu [Word32
    a, Word32
    b, Word32
    c] = (a -> Comparison -> Type -> Judgement a)
    -> Arrows
         (Constant
            Word32 (Domains (a -> Comparison -> Type -> Judgement a)))
         (R (CoDomain (a -> Comparison -> Type -> Judgement a)))
    forall t.
    (VALU t (IsBase t),
     StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
    valuN a -> Comparison -> Type -> Judgement a
    forall a. a -> Comparison -> Type -> Judgement a
    HasType Word32
    a Word32
    b Word32
    c
        valu [Word32
    a, Word32
    b]    = (a -> Type -> Judgement a)
    -> Arrows
         (Constant Word32 (Domains (a -> Type -> Judgement a)))
         (R (CoDomain (a -> Type -> Judgement a)))
    forall t.
    (VALU t (IsBase t),
     StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
    valuN a -> Type -> Judgement a
    forall a. a -> Type -> Judgement a
    IsSort Word32
    a Word32
    b
        valu [Word32]
    _         = R (Judgement a)
    forall a. R a
    malformed

    instance EmbPrj RemoteMetaVariable where
      icod_ :: RemoteMetaVariable -> S Word32
    icod_ (RemoteMetaVariable Instantiation
    a Modality
    b Judgement MetaId
    c) = (Instantiation
     -> Modality -> Judgement MetaId -> RemoteMetaVariable)
    -> Arrows
         (Domains
            (Instantiation
             -> Modality -> Judgement MetaId -> RemoteMetaVariable))
         (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Domains t) (S Word32)
    icodeN' Instantiation -> Modality -> Judgement MetaId -> RemoteMetaVariable
    RemoteMetaVariable Instantiation
    a Modality
    b Judgement MetaId
    c
      value :: Word32 -> R RemoteMetaVariable
    value = (Instantiation
     -> Modality -> Judgement MetaId -> RemoteMetaVariable)
    -> Word32
    -> R (CoDomain
            (Instantiation
             -> Modality -> Judgement MetaId -> RemoteMetaVariable))
    forall t.
    (VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
    t -> Word32 -> R (CoDomain t)
    valueN Instantiation -> Modality -> Judgement MetaId -> RemoteMetaVariable
    RemoteMetaVariable

    instance EmbPrj Key where
      icod_ :: Key -> S Word32
    icod_ (RigidK QName
    x Int
    y) = Word32
    -> (QName -> Int -> Key)
    -> Arrows (Domains (QName -> Int -> Key)) (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    Word32 -> t -> Arrows (Domains t) (S Word32)
    icodeN Word32
    0 QName -> Int -> Key
    RigidK QName
    x Int
    y
      icod_ (LocalK Int
    x Int
    y) = Word32
    -> (Int -> Int -> Key)
    -> Arrows (Domains (Int -> Int -> Key)) (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    Word32 -> t -> Arrows (Domains t) (S Word32)
    icodeN Word32
    1 Int -> Int -> Key
    LocalK Int
    x Int
    y
      icod_ (PiK Hiding
    h)      = Word32
    -> (Hiding -> Key) -> Arrows (Domains (Hiding -> Key)) (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    Word32 -> t -> Arrows (Domains t) (S Word32)
    icodeN Word32
    2 Hiding -> Key
    PiK Hiding
    h
      icod_ Key
    FlexK        = Word32 -> Key -> Arrows (Domains Key) (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    Word32 -> t -> Arrows (Domains t) (S Word32)
    icodeN Word32
    3 Key
    FlexK
      icod_ Key
    ConstK       = Word32 -> Key -> Arrows (Domains Key) (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    Word32 -> t -> Arrows (Domains t) (S Word32)
    icodeN Word32
    4 Key
    ConstK
      icod_ Key
    SortK        = Word32 -> Key -> Arrows (Domains Key) (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    Word32 -> t -> Arrows (Domains t) (S Word32)
    icodeN Word32
    5 Key
    SortK

      value :: Word32 -> R Key
    value = ([Word32] -> R Key) -> Word32 -> R Key
    forall a. EmbPrj a => ([Word32] -> R a) -> Word32 -> R a
    vcase [Word32] -> R Key
    valu where
        valu :: [Word32] -> R Key
    valu [Word32
    0, Word32
    x, Word32
    y] = (QName -> Int -> Key)
    -> Arrows
         (Constant Word32 (Domains (QName -> Int -> Key)))
         (R (CoDomain (QName -> Int -> Key)))
    forall t.
    (VALU t (IsBase t),
     StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
    valuN QName -> Int -> Key
    RigidK Word32
    x Word32
    y
        valu [Word32
    1, Word32
    x, Word32
    y] = (Int -> Int -> Key)
    -> Arrows
         (Constant Word32 (Domains (Int -> Int -> Key)))
         (R (CoDomain (Int -> Int -> Key)))
    forall t.
    (VALU t (IsBase t),
     StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
    valuN Int -> Int -> Key
    LocalK Word32
    x Word32
    y
        valu [Word32
    2, Word32
    h]    = (Hiding -> Key)
    -> Arrows
         (Constant Word32 (Domains (Hiding -> Key)))
         (R (CoDomain (Hiding -> Key)))
    forall t.
    (VALU t (IsBase t),
     StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
    valuN Hiding -> Key
    PiK Word32
    h
        valu [Word32
    3]       = Key -> Arrows (Constant Word32 (Domains Key)) (R (CoDomain Key))
    forall t.
    (VALU t (IsBase t),
     StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
    valuN Key
    FlexK
        valu [Word32
    4]       = Key -> Arrows (Constant Word32 (Domains Key)) (R (CoDomain Key))
    forall t.
    (VALU t (IsBase t),
     StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
    valuN Key
    ConstK
        valu [Word32
    5]       = Key -> Arrows (Constant Word32 (Domains Key)) (R (CoDomain Key))
    forall t.
    (VALU t (IsBase t),
     StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
    valuN Key
    SortK
        valu [Word32]
    _         = R Key
    forall a. R a
    malformed

    instance (EmbPrj a, Ord a) => EmbPrj (DiscrimTree a) where
      icod_ :: DiscrimTree a -> S Word32
    icod_ DiscrimTree a
    EmptyDT        = DiscrimTree (ZonkAny 0)
    -> Arrows (Domains (DiscrimTree (ZonkAny 0))) (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Domains t) (S Word32)
    icodeN' DiscrimTree (ZonkAny 0)
    forall a. DiscrimTree a
    EmptyDT
      icod_ (DoneDT Set a
    s)     = (Set a -> DiscrimTree a)
    -> Arrows (Domains (Set a -> DiscrimTree a)) (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Domains t) (S Word32)
    icodeN' Set a -> DiscrimTree a
    forall a. Set a -> DiscrimTree a
    DoneDT Set a
    s
      icod_ (CaseDT Int
    i Map Key (DiscrimTree a)
    k DiscrimTree a
    s) = (Int -> Map Key (DiscrimTree a) -> DiscrimTree a -> DiscrimTree a)
    -> Arrows
         (Domains
            (Int -> Map Key (DiscrimTree a) -> DiscrimTree a -> DiscrimTree a))
         (S Word32)
    forall t.
    (ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Domains t) (S Word32)
    icodeN' Int -> Map Key (DiscrimTree a) -> DiscrimTree a -> DiscrimTree a
    forall a.
    Int -> Map Key (DiscrimTree a) -> DiscrimTree a -> DiscrimTree a
    CaseDT Int
    i Map Key (DiscrimTree a)
    k DiscrimTree a
    s

      value :: Word32 -> R (DiscrimTree a)
    value = ([Word32] -> R (DiscrimTree a)) -> Word32 -> R (DiscrimTree a)
    forall a. EmbPrj a => ([Word32] -> R a) -> Word32 -> R a
    vcase [Word32] -> R (DiscrimTree a)
    forall {a}.
    (Ord a, EmbPrj a) =>
    [Word32] -> StateT St IO (DiscrimTree a)
    valu where
        valu :: [Word32]
    -> Arrows
         (Constant Word32 (Domains (DiscrimTree a)))
         (R (CoDomain (DiscrimTree a)))
    valu []        = DiscrimTree a
    -> Arrows
         (Constant Word32 (Domains (DiscrimTree a)))
         (R (CoDomain (DiscrimTree a)))
    forall t.
    (VALU t (IsBase t),
     StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
    valuN DiscrimTree a
    forall a. DiscrimTree a
    EmptyDT
        valu [Word32
    a]       = (Set a -> DiscrimTree a)
    -> Arrows
         (Constant Word32 (Domains (Set a -> DiscrimTree a)))
         (R (CoDomain (Set a -> DiscrimTree a)))
    forall t.
    (VALU t (IsBase t),
     StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
    valuN Set a -> DiscrimTree a
    forall a. Set a -> DiscrimTree a
    DoneDT Word32
    a
        valu [Word32
    i, Word32
    k, Word32
    s] = (Int -> Map Key (DiscrimTree a) -> DiscrimTree a -> DiscrimTree a)
    -> Arrows
         (Constant
            Word32
            (Domains
               (Int
                -> Map Key (DiscrimTree a) -> DiscrimTree a -> DiscrimTree a)))
         (R (CoDomain
               (Int
                -> Map Key (DiscrimTree a) -> DiscrimTree a -> DiscrimTree a)))
    forall t.
    (VALU t (IsBase t),
     StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
     All EmbPrj (Domains t)) =>
    t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
    valuN Int -> Map Key (DiscrimTree a) -> DiscrimTree a -> DiscrimTree a
    forall a.
    Int -> Map Key (DiscrimTree a) -> DiscrimTree a -> DiscrimTree a
    CaseDT Word32
    i Word32
    k Word32
    s
        valu [Word32]
    _         = StateT St IO (DiscrimTree a)
    Arrows
      (Constant Word32 (Domains (DiscrimTree a)))
      (R (CoDomain (DiscrimTree a)))
    forall a. R a
    malformed