    {-# LANGUAGE LambdaCase #-}
    {-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}   -- See calls to mkTemplateTyVars

    module GHC.Builtin.Types.Literals
      ( tryInteractInertFam, tryInteractTopFam, tryMatchFam

      , typeNatTyCons
      , typeNatCoAxiomRules
      , BuiltInSynFamily(..)

        -- If you define a new built-in type family, make sure to export its TyCon
        -- from here as well.
        -- See Note [Adding built-in type families]
      , typeNatAddTyCon
      , typeNatMulTyCon
      , typeNatExpTyCon
      , typeNatSubTyCon
      , typeNatDivTyCon
      , typeNatModTyCon
      , typeNatLogTyCon
      , typeNatCmpTyCon
      , typeSymbolCmpTyCon
      , typeSymbolAppendTyCon
      , typeCharCmpTyCon
      , typeConsSymbolTyCon
      , typeUnconsSymbolTyCon
      , typeCharToNatTyCon
      , typeNatToCharTyCon
      ) where

    import GHC.Prelude

    import GHC.Core.Type
    import GHC.Core.Unify      ( tcMatchTys )
    import GHC.Data.Pair
    import GHC.Core.TyCon    ( TyCon, FamTyConFlav(..), mkFamilyTyCon, tyConArity
                             , Injectivity(..), isBuiltInSynFamTyCon_maybe )
    import GHC.Core.Coercion.Axiom
    import GHC.Core.TyCo.Compare   ( tcEqType )
    import GHC.Types.Name          ( Name, BuiltInSyntax(..) )
    import GHC.Types.Unique.FM
    import GHC.Builtin.Types
    import GHC.Builtin.Types.Prim  ( mkTemplateAnonTyConBinders, mkTemplateTyVars )
    import GHC.Builtin.Names
                      ( gHC_INTERNAL_TYPELITS
                      , gHC_INTERNAL_TYPELITS_INTERNAL
                      , gHC_INTERNAL_TYPENATS
                      , gHC_INTERNAL_TYPENATS_INTERNAL
                      , typeNatAddTyFamNameKey
                      , typeNatMulTyFamNameKey
                      , typeNatExpTyFamNameKey
                      , typeNatSubTyFamNameKey
                      , typeNatDivTyFamNameKey
                      , typeNatModTyFamNameKey
                      , typeNatLogTyFamNameKey
                      , typeNatCmpTyFamNameKey
                      , typeSymbolCmpTyFamNameKey
                      , typeSymbolAppendFamNameKey
                      , typeCharCmpTyFamNameKey
                      , typeConsSymbolTyFamNameKey
                      , typeUnconsSymbolTyFamNameKey
                      , typeCharToNatTyFamNameKey
                      , typeNatToCharTyFamNameKey
                      )
    import GHC.Data.FastString
    import GHC.Utils.Panic
    import GHC.Utils.Outputable

    import Control.Monad ( guard )
    import Data.List  ( isPrefixOf, isSuffixOf )
    import Data.Maybe ( listToMaybe )
    import qualified Data.Char as Char

    {-
    Note [Type-level literals]
    ~~~~~~~~~~~~~~~~~~~~~~~~~~
    There are currently three forms of type-level literals: natural numbers, symbols, and
    characters.

    Type-level literals are supported by CoAxiomRules (conditional axioms), which
    power the built-in type families (see Note [Adding built-in type families]).
    Currently, all built-in type families are for the express purpose of supporting
    type-level literals.

    See also the Wiki page:

        https://gitlab.haskell.org/ghc/ghc/wikis/type-nats

    Note [Adding built-in type families]
    ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    There are a few steps to adding a built-in type family:

    * Adding a unique for the type family TyCon

      These go in GHC.Builtin.Names. It will likely be of the form
      @myTyFamNameKey = mkPreludeTyConUnique xyz@, where @xyz@ is a number that
      has not been chosen before in GHC.Builtin.Names. There are several examples already
      in GHC.Builtin.Names—see, for instance, typeNatAddTyFamNameKey.

    * Adding the type family TyCon itself

      This goes in GHC.Builtin.Types.Literals. There are plenty of examples of how to define
      these -- see, for instance, typeNatAddTyCon.

      Once your TyCon has been defined, be sure to:

      - Export it from GHC.Builtin.Types.Literals. (Not doing so caused #14632.)
      - Include it in the typeNatTyCons list, defined in GHC.Builtin.Types.Literals.

    * Define the type family somewhere

      Finally, you will need to define the type family somewhere, likely in @base@.
      Currently, all of the built-in type families are defined in GHC.TypeLits or
      GHC.TypeNats, so those are likely candidates.

      Since the behavior of your built-in type family is specified in GHC.Builtin.Types.Literals,
      you should give an open type family definition with no instances, like so:

        type family MyTypeFam (m :: Nat) (n :: Nat) :: Nat

      Changing the argument and result kinds as appropriate.

    * Update the relevant test cases

      The GHC test suite will likely need to be updated after you add your built-in
      type family. For instance:

      - The T9181 test prints the :browse contents of GHC.TypeLits, so if you added
        a test there, the expected output of T9181 will need to change.
      - The TcTypeNatSimple and TcTypeSymbolSimple tests have compile-time unit
        tests, as well as TcTypeNatSimpleRun and TcTypeSymbolSimpleRun, which have
        runtime unit tests. Consider adding further unit tests to those if your
        built-in type family deals with Nats or Symbols, respectively.

    Note [Inlining axiom constructors]
    ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    We have a number of constructor functions with types like
       mkUnaryConstFoldAxiom :: TyCon -> String
                             -> (Type -> Maybe a)
                             -> (a -> Maybe Type)
                             -> BuiltInFamRewrite

    For very type-family-heavy code, these higher order argument are inefficient;
    e.g. the fourth argument might always return (Just ty) in the above. Inlining
    them is a bit brutal, but not bad, makes a few-percent difference in, say
    perf test T13386.

    These functions aren't exported, so the effect is very local.

    -}

    -------------------------------------------------------------------------------
    --     Key utility functions
    -------------------------------------------------------------------------------

    tryInteractTopFam :: BuiltInSynFamily -> TyCon -> [Type] -> Type
                      -> [(CoAxiomRule, TypeEqn)]
    -- The returned CoAxiomRule is always unary
    tryInteractTopFam :: BuiltInSynFamily
    -> TyCon -> [Type] -> Type -> [(CoAxiomRule, TypeEqn)]
    tryInteractTopFam BuiltInSynFamily
    fam TyCon
    fam_tc [Type]
    tys Type
    r
      = [(BuiltInFamInjectivity -> CoAxiomRule
    bifinj_axr BuiltInFamInjectivity
    bif, TypeEqn
    eqn_out) | BuiltInFamInjectivity
    bif  <- BuiltInSynFamily -> [BuiltInFamInjectivity]
    sfInteract BuiltInSynFamily
    fam
                                   , Just TypeEqn
    eqn_out <- [BuiltInFamInjectivity -> TypeEqn -> Maybe TypeEqn
    bifinj_proves BuiltInFamInjectivity
    bif TypeEqn
    eqn_in] ]
      where
        eqn_in :: TypeEqn
        eqn_in :: TypeEqn
    eqn_in = Type -> Type -> TypeEqn
    forall a. a -> a -> Pair a
    Pair (TyCon -> [Type] -> Type
    mkTyConApp TyCon
    fam_tc [Type]
    tys) Type
    r

    tryInteractInertFam :: BuiltInSynFamily -> TyCon
                        -> [Type] -> [Type] -- F tys1 ~ F tys2
                        -> [(CoAxiomRule, TypeEqn)]
    tryInteractInertFam :: BuiltInSynFamily
    -> TyCon -> [Type] -> [Type] -> [(CoAxiomRule, TypeEqn)]
    tryInteractInertFam BuiltInSynFamily
    builtin_fam TyCon
    fam_tc [Type]
    tys1 [Type]
    tys2
      = [(BuiltInFamInjectivity -> CoAxiomRule
    bifinj_axr BuiltInFamInjectivity
    bif, TypeEqn
    eqn_out) | BuiltInFamInjectivity
    bif <- BuiltInSynFamily -> [BuiltInFamInjectivity]
    sfInteract BuiltInSynFamily
    builtin_fam
                                   , Just TypeEqn
    eqn_out <- [BuiltInFamInjectivity -> TypeEqn -> Maybe TypeEqn
    bifinj_proves BuiltInFamInjectivity
    bif TypeEqn
    eqn_in] ]
      where
        eqn_in :: TypeEqn
    eqn_in = Type -> Type -> TypeEqn
    forall a. a -> a -> Pair a
    Pair (TyCon -> [Type] -> Type
    mkTyConApp TyCon
    fam_tc [Type]
    tys1) (TyCon -> [Type] -> Type
    mkTyConApp TyCon
    fam_tc [Type]
    tys2)

    tryMatchFam :: BuiltInSynFamily -> [Type]
                -> Maybe (CoAxiomRule, [Type], Type)
    -- Does this reduce on the given arguments?
    -- If it does, returns (CoAxiomRule, types to instantiate the rule at, rhs type)
    -- That is: mkAxiomCo (BuiltInFamRew ax) (map mkNomReflCo ts)
    --              :: F tys ~r rhs,
    tryMatchFam :: BuiltInSynFamily -> [Type] -> Maybe (CoAxiomRule, [Type], Type)
    tryMatchFam BuiltInSynFamily
    builtin_fam [Type]
    arg_tys
      = [(CoAxiomRule, [Type], Type)] -> Maybe (CoAxiomRule, [Type], Type)
    forall a. [a] -> Maybe a
    listToMaybe ([(CoAxiomRule, [Type], Type)]
     -> Maybe (CoAxiomRule, [Type], Type))
    -> [(CoAxiomRule, [Type], Type)]
    -> Maybe (CoAxiomRule, [Type], Type)
    forall a b. (a -> b) -> a -> b
    $   -- Pick first rule to match
        [ (BuiltInFamRewrite -> CoAxiomRule
    bifrw_axr BuiltInFamRewrite
    rw_ax, [Type]
    inst_tys, Type
    res_ty)
        | BuiltInFamRewrite
    rw_ax <- BuiltInSynFamily -> [BuiltInFamRewrite]
    sfMatchFam BuiltInSynFamily
    builtin_fam
        , Just ([Type]
    inst_tys,Type
    res_ty) <- [BuiltInFamRewrite -> [Type] -> Maybe ([Type], Type)
    bifrw_match BuiltInFamRewrite
    rw_ax [Type]
    arg_tys] ]

    -------------------------------------------------------------------------------
    --          Constructing BuiltInFamInjectivity, BuiltInFamRewrite
    -------------------------------------------------------------------------------

    mkUnaryConstFoldAxiom :: TyCon -> String
                          -> (Type -> Maybe a)
                          -> (a -> Maybe Type)
                          -> BuiltInFamRewrite
    -- For the definitional axioms, like  (3+4 --> 7)
    {-# INLINE mkUnaryConstFoldAxiom #-}  -- See Note [Inlining axiom constructors]
    mkUnaryConstFoldAxiom :: forall a.
    TyCon
    -> String
    -> (Type -> Maybe a)
    -> (a -> Maybe Type)
    -> BuiltInFamRewrite
    mkUnaryConstFoldAxiom TyCon
    fam_tc String
    str Type -> Maybe a
    isReqTy a -> Maybe Type
    f
      = BuiltInFamRewrite
    bif
      where
        bif :: BuiltInFamRewrite
    bif = BIF_Rewrite
          { bifrw_name :: FastString
    bifrw_name   = String -> FastString
    fsLit String
    str
          , bifrw_axr :: CoAxiomRule
    bifrw_axr    = BuiltInFamRewrite -> CoAxiomRule
    BuiltInFamRew BuiltInFamRewrite
    bif
          , bifrw_fam_tc :: TyCon
    bifrw_fam_tc = TyCon
    fam_tc
          , bifrw_arity :: Int
    bifrw_arity  = Int
    1
          , bifrw_match :: [Type] -> Maybe ([Type], Type)
    bifrw_match  = \[Type]
    ts -> do { [t1] <- [Type] -> Maybe [Type]
    forall a. a -> Maybe a
    forall (m :: * -> *) a. Monad m => a -> m a
    return [Type]
    ts
                                     ; t1' <- isReqTy t1
                                     ; res <- f t1'
                                     ; return ([t1], res) }
          , bifrw_proves :: [TypeEqn] -> Maybe TypeEqn
    bifrw_proves = \[TypeEqn]
    cs -> do { [Pair s1 s2] <- [TypeEqn] -> Maybe [TypeEqn]
    forall a. a -> Maybe a
    forall (m :: * -> *) a. Monad m => a -> m a
    return [TypeEqn]
    cs
                                     ; s2' <- isReqTy s2
                                     ; z   <- f s2'
                                     ; return (mkTyConApp fam_tc [s1] === z) }
          }

    mkBinConstFoldAxiom :: TyCon -> String
                        -> (Type -> Maybe a)
                        -> (Type -> Maybe b)
                        -> (a -> b -> Maybe Type)
                        -> BuiltInFamRewrite
    -- For the definitional axioms, like  (3+4 --> 7)
    {-# INLINE mkBinConstFoldAxiom #-}  -- See Note [Inlining axiom constructors]
    mkBinConstFoldAxiom :: forall a b.
    TyCon
    -> String
    -> (Type -> Maybe a)
    -> (Type -> Maybe b)
    -> (a -> b -> Maybe Type)
    -> BuiltInFamRewrite
    mkBinConstFoldAxiom TyCon
    fam_tc String
    str Type -> Maybe a
    isReqTy1 Type -> Maybe b
    isReqTy2 a -> b -> Maybe Type
    f
      = BuiltInFamRewrite
    bif
      where
        bif :: BuiltInFamRewrite
    bif = BIF_Rewrite
          { bifrw_name :: FastString
    bifrw_name   = String -> FastString
    fsLit String
    str
          , bifrw_axr :: CoAxiomRule
    bifrw_axr    = BuiltInFamRewrite -> CoAxiomRule
    BuiltInFamRew BuiltInFamRewrite
    bif
          , bifrw_fam_tc :: TyCon
    bifrw_fam_tc = TyCon
    fam_tc
          , bifrw_arity :: Int
    bifrw_arity  = Int
    2
          , bifrw_match :: [Type] -> Maybe ([Type], Type)
    bifrw_match  = \[Type]
    ts -> do { [t1,t2] <- [Type] -> Maybe [Type]
    forall a. a -> Maybe a
    forall (m :: * -> *) a. Monad m => a -> m a
    return [Type]
    ts
                                     ; t1' <- isReqTy1 t1
                                     ; t2' <- isReqTy2 t2
                                     ; res <- f t1' t2'
                                     ; return ([t1,t2], res) }
          , bifrw_proves :: [TypeEqn] -> Maybe TypeEqn
    bifrw_proves = \[TypeEqn]
    cs -> do { [Pair s1 s2, Pair t1 t2] <- [TypeEqn] -> Maybe [TypeEqn]
    forall a. a -> Maybe a
    forall (m :: * -> *) a. Monad m => a -> m a
    return [TypeEqn]
    cs
                                     ; s2' <- isReqTy1 s2
                                     ; t2' <- isReqTy2 t2
                                     ; z   <- f s2' t2'
                                     ; return (mkTyConApp fam_tc [s1,t1] === z) }
          }

    mkRewriteAxiom :: TyCon -> String
                   -> [TyVar] -> [Type]  -- LHS of axiom
                   -> Type               -- RHS of axiom
                   -> BuiltInFamRewrite
    -- Not higher order, no benefit in inlining
    -- See Note [Inlining axiom constructors]
    mkRewriteAxiom :: TyCon -> String -> [TyVar] -> [Type] -> Type -> BuiltInFamRewrite
    mkRewriteAxiom TyCon
    fam_tc String
    str [TyVar]
    tpl_tvs [Type]
    lhs_tys Type
    rhs_ty
      = Bool -> SDoc -> BuiltInFamRewrite -> BuiltInFamRewrite
    forall a. HasCallStack => Bool -> SDoc -> a -> a
    assertPpr (TyCon -> Int
    tyConArity TyCon
    fam_tc Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == [Type] -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [Type]
    lhs_tys) (String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    str SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> [Type] -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr [Type]
    lhs_tys) (BuiltInFamRewrite -> BuiltInFamRewrite)
    -> BuiltInFamRewrite -> BuiltInFamRewrite
    forall a b. (a -> b) -> a -> b
    $
        BuiltInFamRewrite
    bif
      where
        bif :: BuiltInFamRewrite
    bif = BIF_Rewrite
          { bifrw_name :: FastString
    bifrw_name   = String -> FastString
    fsLit String
    str
          , bifrw_axr :: CoAxiomRule
    bifrw_axr    = BuiltInFamRewrite -> CoAxiomRule
    BuiltInFamRew BuiltInFamRewrite
    bif
          , bifrw_fam_tc :: TyCon
    bifrw_fam_tc = TyCon
    fam_tc
          , bifrw_arity :: Int
    bifrw_arity  = Int
    bif_arity
          , bifrw_match :: [Type] -> Maybe ([Type], Type)
    bifrw_match  = [Type] -> Maybe ([Type], Type)
    match_fn
          , bifrw_proves :: [TypeEqn] -> Maybe TypeEqn
    bifrw_proves = [TypeEqn] -> Maybe TypeEqn
    inst_fn }

        bif_arity :: Int
    bif_arity = [TyVar] -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [TyVar]
    tpl_tvs

        match_fn :: [Type] -> Maybe ([Type],Type)
        match_fn :: [Type] -> Maybe ([Type], Type)
    match_fn [Type]
    arg_tys
          = Bool -> SDoc -> Maybe ([Type], Type) -> Maybe ([Type], Type)
    forall a. HasCallStack => Bool -> SDoc -> a -> a
    assertPpr (TyCon -> Int
    tyConArity TyCon
    fam_tc Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == [Type] -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [Type]
    arg_tys) (String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    str SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> [Type] -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr [Type]
    arg_tys) (Maybe ([Type], Type) -> Maybe ([Type], Type))
    -> Maybe ([Type], Type) -> Maybe ([Type], Type)
    forall a b. (a -> b) -> a -> b
    $
            case [Type] -> [Type] -> Maybe Subst
    tcMatchTys [Type]
    lhs_tys [Type]
    arg_tys of
              Maybe Subst
    Nothing    -> Maybe ([Type], Type)
    forall a. Maybe a
    Nothing
              Just Subst
    subst -> ([Type], Type) -> Maybe ([Type], Type)
    forall a. a -> Maybe a
    Just (Subst -> [TyVar] -> [Type]
    substTyVars Subst
    subst [TyVar]
    tpl_tvs, HasDebugCallStack => Subst -> Type -> Type
    Subst -> Type -> Type
    substTy Subst
    subst Type
    rhs_ty)

        inst_fn :: [TypeEqn] -> Maybe TypeEqn
        inst_fn :: [TypeEqn] -> Maybe TypeEqn
    inst_fn [TypeEqn]
    inst_eqns
          = Bool -> SDoc -> Maybe TypeEqn -> Maybe TypeEqn
    forall a. HasCallStack => Bool -> SDoc -> a -> a
    assertPpr ([TypeEqn] -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [TypeEqn]
    inst_eqns Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    bif_arity) (String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    str SDoc -> SDoc -> SDoc
    forall doc. IsDoc doc => doc -> doc -> doc
    $$ [TypeEqn] -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr [TypeEqn]
    inst_eqns) (Maybe TypeEqn -> Maybe TypeEqn) -> Maybe TypeEqn -> Maybe TypeEqn
    forall a b. (a -> b) -> a -> b
    $
            TypeEqn -> Maybe TypeEqn
    forall a. a -> Maybe a
    Just (TyCon -> [Type] -> Type
    mkTyConApp TyCon
    fam_tc (HasDebugCallStack => Subst -> [Type] -> [Type]
    Subst -> [Type] -> [Type]
    substTys ([TyVar] -> [Type] -> Subst
    HasDebugCallStack => [TyVar] -> [Type] -> Subst
    zipTCvSubst [TyVar]
    tpl_tvs [Type]
    tys1) [Type]
    lhs_tys)
                  Type -> Type -> TypeEqn
    ===
                  HasDebugCallStack => Subst -> Type -> Type
    Subst -> Type -> Type
    substTy ([TyVar] -> [Type] -> Subst
    HasDebugCallStack => [TyVar] -> [Type] -> Subst
    zipTCvSubst [TyVar]
    tpl_tvs [Type]
    tys2) Type
    rhs_ty)
          where
            ([Type]
    tys1, [Type]
    tys2) = [TypeEqn] -> ([Type], [Type])
    forall a. [Pair a] -> ([a], [a])
    unzipPairs [TypeEqn]
    inst_eqns

    mkTopUnaryFamDeduction :: String -> TyCon
                         -> (Type -> Type -> Maybe TypeEqn)
                         -> BuiltInFamInjectivity
    -- Deduction from (F s ~ r) where `F` is a unary type function
    {-# INLINE mkTopUnaryFamDeduction #-}  -- See Note [Inlining axiom constructors]
    mkTopUnaryFamDeduction :: String
    -> TyCon
    -> (Type -> Type -> Maybe TypeEqn)
    -> BuiltInFamInjectivity
    mkTopUnaryFamDeduction String
    str TyCon
    fam_tc Type -> Type -> Maybe TypeEqn
    f
      = BuiltInFamInjectivity
    bif
      where
        bif :: BuiltInFamInjectivity
    bif = BIF_Interact
          { bifinj_name :: FastString
    bifinj_name   = String -> FastString
    fsLit String
    str
          , bifinj_axr :: CoAxiomRule
    bifinj_axr    = BuiltInFamInjectivity -> CoAxiomRule
    BuiltInFamInj BuiltInFamInjectivity
    bif
          , bifinj_proves :: TypeEqn -> Maybe TypeEqn
    bifinj_proves = \(Pair Type
    lhs Type
    rhs)
                            -> do { (tc, [a]) <- HasDebugCallStack => Type -> Maybe (TyCon, [Type])
    Type -> Maybe (TyCon, [Type])
    splitTyConApp_maybe Type
    lhs
                                  ; massertPpr (tc == fam_tc) (ppr tc $$ ppr fam_tc)
                                  ; f a rhs } }

    mkTopBinFamDeduction :: String -> TyCon
                         -> (Type -> Type -> Type -> Maybe TypeEqn)
                         -> BuiltInFamInjectivity
    -- Deduction from (F s t  ~ r) where `F` is a binary type function
    {-# INLINE mkTopBinFamDeduction #-}  -- See Note [Inlining axiom constructors]
    mkTopBinFamDeduction :: String
    -> TyCon
    -> (Type -> Type -> Type -> Maybe TypeEqn)
    -> BuiltInFamInjectivity
    mkTopBinFamDeduction String
    str TyCon
    fam_tc Type -> Type -> Type -> Maybe TypeEqn
    f
      = BuiltInFamInjectivity
    bif
      where
        bif :: BuiltInFamInjectivity
    bif = BIF_Interact
          { bifinj_name :: FastString
    bifinj_name   = String -> FastString
    fsLit String
    str
          , bifinj_axr :: CoAxiomRule
    bifinj_axr    = BuiltInFamInjectivity -> CoAxiomRule
    BuiltInFamInj BuiltInFamInjectivity
    bif
          , bifinj_proves :: TypeEqn -> Maybe TypeEqn
    bifinj_proves = \(Pair Type
    lhs Type
    rhs) ->
                            do { (tc, [a,b]) <- HasDebugCallStack => Type -> Maybe (TyCon, [Type])
    Type -> Maybe (TyCon, [Type])
    splitTyConApp_maybe Type
    lhs
                               ; massertPpr (tc == fam_tc) (ppr tc $$ ppr fam_tc)
                               ; f a b rhs } }

    mkUnaryBIF :: String -> TyCon -> BuiltInFamInjectivity
    -- Not higher order, no benefit in inlining
    -- See Note [Inlining axiom constructors]
    mkUnaryBIF :: String -> TyCon -> BuiltInFamInjectivity
    mkUnaryBIF String
    str TyCon
    fam_tc
      = BuiltInFamInjectivity
    bif
      where
        bif :: BuiltInFamInjectivity
    bif = BIF_Interact { bifinj_name :: FastString
    bifinj_name   = String -> FastString
    fsLit String
    str
                           , bifinj_axr :: CoAxiomRule
    bifinj_axr    = BuiltInFamInjectivity -> CoAxiomRule
    BuiltInFamInj BuiltInFamInjectivity
    bif
                           , bifinj_proves :: TypeEqn -> Maybe TypeEqn
    bifinj_proves = TypeEqn -> Maybe TypeEqn
    proves }
        proves :: TypeEqn -> Maybe TypeEqn
    proves (Pair Type
    lhs Type
    rhs)
          = do { (tc2, [x2]) <- HasDebugCallStack => Type -> Maybe (TyCon, [Type])
    Type -> Maybe (TyCon, [Type])
    splitTyConApp_maybe Type
    rhs
               ; guard (tc2 == fam_tc)
               ; (tc1, [x1]) <- splitTyConApp_maybe lhs
               ; massertPpr (tc1 == fam_tc) (ppr tc1 $$ ppr fam_tc)
               ; return (Pair x1 x2) }

    mkBinBIF :: String -> TyCon
             -> WhichArg -> WhichArg
             -> (Type -> Bool)         -- The guard on the equal args, if any
             -> BuiltInFamInjectivity
    {-# INLINE mkBinBIF #-}  -- See Note [Inlining axiom constructors]
    mkBinBIF :: String
    -> TyCon
    -> WhichArg
    -> WhichArg
    -> (Type -> Bool)
    -> BuiltInFamInjectivity
    mkBinBIF String
    str TyCon
    fam_tc WhichArg
    eq1 WhichArg
    eq2 Type -> Bool
    check_me
      = BuiltInFamInjectivity
    bif
      where
        bif :: BuiltInFamInjectivity
    bif = BIF_Interact { bifinj_name :: FastString
    bifinj_name   = String -> FastString
    fsLit String
    str
                           , bifinj_axr :: CoAxiomRule
    bifinj_axr    = BuiltInFamInjectivity -> CoAxiomRule
    BuiltInFamInj BuiltInFamInjectivity
    bif
                           , bifinj_proves :: TypeEqn -> Maybe TypeEqn
    bifinj_proves = TypeEqn -> Maybe TypeEqn
    proves }
        proves :: TypeEqn -> Maybe TypeEqn
    proves (Pair Type
    lhs Type
    rhs)
          = do { (tc2, [x2,y2]) <- HasDebugCallStack => Type -> Maybe (TyCon, [Type])
    Type -> Maybe (TyCon, [Type])
    splitTyConApp_maybe Type
    rhs
               ; guard (tc2 == fam_tc)
               ; (tc1, [x1,y1]) <- splitTyConApp_maybe lhs
               ; massertPpr (tc1 == fam_tc) (ppr tc1 $$ ppr fam_tc)
               ; case (eq1, eq2) of
                   (WhichArg
    ArgX,WhichArg
    ArgX) -> Type -> Type -> Type -> Type -> Maybe TypeEqn
    do_it Type
    x1 Type
    x2 Type
    y1 Type
    y2
                   (WhichArg
    ArgX,WhichArg
    ArgY) -> Type -> Type -> Type -> Type -> Maybe TypeEqn
    do_it Type
    x1 Type
    y2 Type
    x2 Type
    y1
                   (WhichArg
    ArgY,WhichArg
    ArgX) -> Type -> Type -> Type -> Type -> Maybe TypeEqn
    do_it Type
    y1 Type
    x2 Type
    y2 Type
    x1
                   (WhichArg
    ArgY,WhichArg
    ArgY) -> Type -> Type -> Type -> Type -> Maybe TypeEqn
    do_it Type
    y1 Type
    y2 Type
    x1 Type
    x2 }

        do_it :: Type -> Type -> Type -> Type -> Maybe TypeEqn
    do_it Type
    a1 Type
    a2 Type
    b1 Type
    b2 = do { Type -> Type -> Maybe ()
    same Type
    a1 Type
    a2; Bool -> Maybe ()
    forall (f :: * -> *). Alternative f => Bool -> f ()
    guard (Type -> Bool
    check_me Type
    a1); TypeEqn -> Maybe TypeEqn
    forall a. a -> Maybe a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Type -> Type -> TypeEqn
    forall a. a -> a -> Pair a
    Pair Type
    b1 Type
    b2) }

    noGuard :: Type -> Bool
    noGuard :: Type -> Bool
    noGuard Type
    _ = Bool
    True

    numGuard :: (Integer -> Bool) -> Type -> Bool
    numGuard :: (Integer -> Bool) -> Type -> Bool
    numGuard Integer -> Bool
    pred Type
    ty = case Type -> Maybe Integer
    isNumLitTy Type
    ty of
                          Just Integer
    n  -> Integer -> Bool
    pred Integer
    n
                          Maybe Integer
    Nothing -> Bool
    False

    data WhichArg = ArgX | ArgY

    -------------------------------------------------------------------------------
    --     Built-in type constructors for functions on type-level nats
    -------------------------------------------------------------------------------

    -- The list of built-in type family TyCons that GHC uses.
    -- If you define a built-in type family, make sure to add it to this list.
    -- See Note [Adding built-in type families]
    typeNatTyCons :: [TyCon]
    typeNatTyCons :: [TyCon]
    typeNatTyCons =
      [ TyCon
    typeNatAddTyCon
      , TyCon
    typeNatMulTyCon
      , TyCon
    typeNatExpTyCon
      , TyCon
    typeNatSubTyCon
      , TyCon
    typeNatDivTyCon
      , TyCon
    typeNatModTyCon
      , TyCon
    typeNatLogTyCon
      , TyCon
    typeNatCmpTyCon
      , TyCon
    typeSymbolCmpTyCon
      , TyCon
    typeSymbolAppendTyCon
      , TyCon
    typeCharCmpTyCon
      , TyCon
    typeConsSymbolTyCon
      , TyCon
    typeUnconsSymbolTyCon
      , TyCon
    typeCharToNatTyCon
      , TyCon
    typeNatToCharTyCon
      ]

    -- The list of built-in type family axioms that GHC uses.
    -- If you define new axioms, make sure to include them in this list.
    -- See Note [Adding built-in type families]
    typeNatCoAxiomRules :: UniqFM FastString CoAxiomRule
    typeNatCoAxiomRules :: UniqFM FastString CoAxiomRule
    typeNatCoAxiomRules
      = [(FastString, CoAxiomRule)] -> UniqFM FastString CoAxiomRule
    forall key elt. Uniquable key => [(key, elt)] -> UniqFM key elt
    listToUFM ([(FastString, CoAxiomRule)] -> UniqFM FastString CoAxiomRule)
    -> [(FastString, CoAxiomRule)] -> UniqFM FastString CoAxiomRule
    forall a b. (a -> b) -> a -> b
    $
        [ (FastString, CoAxiomRule)
    pr | TyCon
    tc <- [TyCon]
    typeNatTyCons
             , Just BuiltInSynFamily
    ops <- [TyCon -> Maybe BuiltInSynFamily
    isBuiltInSynFamTyCon_maybe TyCon
    tc]
             , (FastString, CoAxiomRule)
    pr <- [ (BuiltInFamInjectivity -> FastString
    bifinj_name BuiltInFamInjectivity
    bif, BuiltInFamInjectivity -> CoAxiomRule
    bifinj_axr BuiltInFamInjectivity
    bif) | BuiltInFamInjectivity
    bif <- BuiltInSynFamily -> [BuiltInFamInjectivity]
    sfInteract BuiltInSynFamily
    ops ]
                  [(FastString, CoAxiomRule)]
    -> [(FastString, CoAxiomRule)] -> [(FastString, CoAxiomRule)]
    forall a. [a] -> [a] -> [a]
    ++ [ (BuiltInFamRewrite -> FastString
    bifrw_name BuiltInFamRewrite
    bif,  BuiltInFamRewrite -> CoAxiomRule
    bifrw_axr BuiltInFamRewrite
    bif)  | BuiltInFamRewrite
    bif <- BuiltInSynFamily -> [BuiltInFamRewrite]
    sfMatchFam BuiltInSynFamily
    ops ] ]

    -------------------------------------------------------------------------------
    --                   Addition (+)
    -------------------------------------------------------------------------------

    typeNatAddTyCon :: TyCon
    typeNatAddTyCon :: TyCon
    typeNatAddTyCon = Name -> BuiltInSynFamily -> TyCon
    mkTypeNatFunTyCon2 Name
    name
      BuiltInSynFamily
        { sfMatchFam :: [BuiltInFamRewrite]
    sfMatchFam  = [BuiltInFamRewrite]
    axAddRewrites
        , sfInteract :: [BuiltInFamInjectivity]
    sfInteract  = [BuiltInFamInjectivity]
    axAddInjectivity
        }
      where
        name :: Name
    name = BuiltInSyntax -> Module -> FastString -> Unique -> TyCon -> Name
    mkWiredInTyConName BuiltInSyntax
    UserSyntax Module
    gHC_INTERNAL_TYPENATS (String -> FastString
    fsLit String
    "+")
                  Unique
    typeNatAddTyFamNameKey TyCon
    typeNatAddTyCon

    sn,tn :: TyVar  -- Of kind Natural
    (TyVar
    sn: TyVar
    tn: [TyVar]
    _) = [Type] -> [TyVar]
    mkTemplateTyVars (Type -> [Type]
    forall a. a -> [a]
    repeat Type
    typeSymbolKind)

    axAddRewrites :: [BuiltInFamRewrite]
    axAddRewrites :: [BuiltInFamRewrite]
    axAddRewrites
      = [ TyCon -> String -> [TyVar] -> [Type] -> Type -> BuiltInFamRewrite
    mkRewriteAxiom   TyCon
    tc String
    "Add0L" [TyVar
    tn] [Integer -> Type
    num Integer
    0, TyVar -> Type
    var TyVar
    tn] (TyVar -> Type
    var TyVar
    tn)   -- 0 + t --> t
        , TyCon -> String -> [TyVar] -> [Type] -> Type -> BuiltInFamRewrite
    mkRewriteAxiom   TyCon
    tc String
    "Add0R" [TyVar
    sn] [TyVar -> Type
    var TyVar
    sn, Integer -> Type
    num Integer
    0] (TyVar -> Type
    var TyVar
    sn)   -- s + 0 --> s
        , TyCon
    -> String
    -> (Type -> Maybe Integer)
    -> (Type -> Maybe Integer)
    -> (Integer -> Integer -> Maybe Type)
    -> BuiltInFamRewrite
    forall a b.
    TyCon
    -> String
    -> (Type -> Maybe a)
    -> (Type -> Maybe b)
    -> (a -> b -> Maybe Type)
    -> BuiltInFamRewrite
    mkBinConstFoldAxiom TyCon
    tc String
    "AddDef" Type -> Maybe Integer
    isNumLitTy Type -> Maybe Integer
    isNumLitTy ((Integer -> Integer -> Maybe Type) -> BuiltInFamRewrite)
    -> (Integer -> Integer -> Maybe Type) -> BuiltInFamRewrite
    forall a b. (a -> b) -> a -> b
    $     -- 3 + 4 --> 7
          \Integer
    x Integer
    y -> Type -> Maybe Type
    forall a. a -> Maybe a
    Just (Type -> Maybe Type) -> Type -> Maybe Type
    forall a b. (a -> b) -> a -> b
    $ Integer -> Type
    num (Integer
    x Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    + Integer
    y) ]
      where
        tc :: TyCon
    tc = TyCon
    typeNatAddTyCon

    axAddInjectivity :: [BuiltInFamInjectivity]
    axAddInjectivity :: [BuiltInFamInjectivity]
    axAddInjectivity
      = [ -- (s + t ~ 0) => (s ~ 0)
          String
    -> TyCon
    -> (Type -> Type -> Type -> Maybe TypeEqn)
    -> BuiltInFamInjectivity
    mkTopBinFamDeduction String
    "AddT-0L" TyCon
    tc ((Type -> Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity)
    -> (Type -> Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity
    forall a b. (a -> b) -> a -> b
    $ \ Type
    a Type
    _b Type
    r ->
          do { _ <- Type -> (Integer -> Bool) -> Maybe Integer
    known Type
    r (Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == Integer
    0); return (Pair a (num 0)) }

        , -- (s + t ~ 0) => (t ~ 0)
          String
    -> TyCon
    -> (Type -> Type -> Type -> Maybe TypeEqn)
    -> BuiltInFamInjectivity
    mkTopBinFamDeduction String
    "AddT-0R" TyCon
    tc ((Type -> Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity)
    -> (Type -> Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity
    forall a b. (a -> b) -> a -> b
    $ \ Type
    _a Type
    b Type
    r ->
          do { _ <- Type -> (Integer -> Bool) -> Maybe Integer
    known Type
    r (Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == Integer
    0); return (Pair b (num 0)) }

        , -- (5 + t ~ 8) => (t ~ 3)
          String
    -> TyCon
    -> (Type -> Type -> Type -> Maybe TypeEqn)
    -> BuiltInFamInjectivity
    mkTopBinFamDeduction String
    "AddT-KKL" TyCon
    tc ((Type -> Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity)
    -> (Type -> Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity
    forall a b. (a -> b) -> a -> b
    $ \ Type
    a Type
    b Type
    r ->
          do { na <- Type -> Maybe Integer
    isNumLitTy Type
    a; nr <- known r (>= na); return (Pair b (num (nr-na))) }

        , -- (s + 5 ~ 8) => (s ~ 3)
          String
    -> TyCon
    -> (Type -> Type -> Type -> Maybe TypeEqn)
    -> BuiltInFamInjectivity
    mkTopBinFamDeduction String
    "AddT-KKR" TyCon
    tc ((Type -> Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity)
    -> (Type -> Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity
    forall a b. (a -> b) -> a -> b
    $ \ Type
    a Type
    b Type
    r ->
          do { nb <- Type -> Maybe Integer
    isNumLitTy Type
    b; nr <- known r (>= nb); return (Pair a (num (nr-nb))) }

        , String
    -> TyCon
    -> WhichArg
    -> WhichArg
    -> (Type -> Bool)
    -> BuiltInFamInjectivity
    mkBinBIF String
    "AddI-xx" TyCon
    tc WhichArg
    ArgX WhichArg
    ArgX Type -> Bool
    noGuard  -- x1+y1~x2+y2 {x1=x2}=> (y1 ~ y2)
        , String
    -> TyCon
    -> WhichArg
    -> WhichArg
    -> (Type -> Bool)
    -> BuiltInFamInjectivity
    mkBinBIF String
    "AddI-xy" TyCon
    tc WhichArg
    ArgX WhichArg
    ArgY Type -> Bool
    noGuard  -- x1+y1~x2+y2 {x1=y2}=> (x2 ~ y1)
        , String
    -> TyCon
    -> WhichArg
    -> WhichArg
    -> (Type -> Bool)
    -> BuiltInFamInjectivity
    mkBinBIF String
    "AddI-yx" TyCon
    tc WhichArg
    ArgY WhichArg
    ArgX Type -> Bool
    noGuard  -- x1+y1~x2+y2 {y1=x2}=> (x1 ~ y2)
        , String
    -> TyCon
    -> WhichArg
    -> WhichArg
    -> (Type -> Bool)
    -> BuiltInFamInjectivity
    mkBinBIF String
    "AddI-yy" TyCon
    tc WhichArg
    ArgY WhichArg
    ArgY Type -> Bool
    noGuard  -- x1+y1~x2+y2 {y1=y2}=> (x1 ~ x2)
        ]
      where
        tc :: TyCon
    tc = TyCon
    typeNatAddTyCon

    -------------------------------------------------------------------------------
    --                   Subtraction (-)
    -------------------------------------------------------------------------------

    typeNatSubTyCon :: TyCon
    typeNatSubTyCon :: TyCon
    typeNatSubTyCon = Name -> BuiltInSynFamily -> TyCon
    mkTypeNatFunTyCon2 Name
    name
      BuiltInSynFamily
        { sfMatchFam :: [BuiltInFamRewrite]
    sfMatchFam = [BuiltInFamRewrite]
    axSubRewrites
        , sfInteract :: [BuiltInFamInjectivity]
    sfInteract = [BuiltInFamInjectivity]
    axSubInjectivity
        }
      where
      name :: Name
    name = BuiltInSyntax -> Module -> FastString -> Unique -> TyCon -> Name
    mkWiredInTyConName BuiltInSyntax
    UserSyntax Module
    gHC_INTERNAL_TYPENATS (String -> FastString
    fsLit String
    "-")
                Unique
    typeNatSubTyFamNameKey TyCon
    typeNatSubTyCon

    axSubRewrites :: [BuiltInFamRewrite]
    axSubRewrites :: [BuiltInFamRewrite]
    axSubRewrites
      = [ TyCon -> String -> [TyVar] -> [Type] -> Type -> BuiltInFamRewrite
    mkRewriteAxiom   TyCon
    tc String
    "Sub0R" [TyVar
    sn] [TyVar -> Type
    var TyVar
    sn, Integer -> Type
    num Integer
    0] (TyVar -> Type
    var TyVar
    sn)   -- s - 0 --> s
        , TyCon
    -> String
    -> (Type -> Maybe Integer)
    -> (Type -> Maybe Integer)
    -> (Integer -> Integer -> Maybe Type)
    -> BuiltInFamRewrite
    forall a b.
    TyCon
    -> String
    -> (Type -> Maybe a)
    -> (Type -> Maybe b)
    -> (a -> b -> Maybe Type)
    -> BuiltInFamRewrite
    mkBinConstFoldAxiom TyCon
    tc String
    "SubDef" Type -> Maybe Integer
    isNumLitTy Type -> Maybe Integer
    isNumLitTy ((Integer -> Integer -> Maybe Type) -> BuiltInFamRewrite)
    -> (Integer -> Integer -> Maybe Type) -> BuiltInFamRewrite
    forall a b. (a -> b) -> a -> b
    $     -- 4 - 3 --> 1  if x>=y
          \Integer
    x Integer
    y -> (Integer -> Type) -> Maybe Integer -> Maybe Type
    forall a b. (a -> b) -> Maybe a -> Maybe b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Integer -> Type
    num (Integer -> Integer -> Maybe Integer
    minus Integer
    x Integer
    y) ]
      where
        tc :: TyCon
    tc = TyCon
    typeNatSubTyCon

    axSubInjectivity :: [BuiltInFamInjectivity]
    axSubInjectivity :: [BuiltInFamInjectivity]
    axSubInjectivity
      = [ -- (a - b ~ 5) => (5 + b ~ a)
          String
    -> TyCon
    -> (Type -> Type -> Type -> Maybe TypeEqn)
    -> BuiltInFamInjectivity
    mkTopBinFamDeduction String
    "SubT" TyCon
    tc ((Type -> Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity)
    -> (Type -> Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity
    forall a b. (a -> b) -> a -> b
    $ \ Type
    a Type
    b Type
    r ->
          do { _ <- Type -> Maybe Integer
    isNumLitTy Type
    r; return (Pair (r .+. b) a) }

        , String
    -> TyCon
    -> WhichArg
    -> WhichArg
    -> (Type -> Bool)
    -> BuiltInFamInjectivity
    mkBinBIF String
    "SubI-xx" TyCon
    tc WhichArg
    ArgX WhichArg
    ArgX Type -> Bool
    noGuard -- (x-y1 ~ x-y2) => (y1 ~ y2)
        , String
    -> TyCon
    -> WhichArg
    -> WhichArg
    -> (Type -> Bool)
    -> BuiltInFamInjectivity
    mkBinBIF String
    "SubI-yy" TyCon
    tc WhichArg
    ArgY WhichArg
    ArgY Type -> Bool
    noGuard -- (x1-y ~ x2-y) => (x1 ~ x2)
        ]
      where
        tc :: TyCon
    tc = TyCon
    typeNatSubTyCon

    {-
    Note [Weakened interaction rule for subtraction]
    ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    A simpler interaction here might be:

      `s - t ~ r` --> `t + r ~ s`

    This would enable us to reuse all the code for addition.
    Unfortunately, this works a little too well at the moment.
    Consider the following example:

        0 - 5 ~ r --> 5 + r ~ 0 --> (5 = 0, r = 0)

    This (correctly) spots that the constraint cannot be solved.

    However, this may be a problem if the constraint did not
    need to be solved in the first place!  Consider the following example:

    f :: Proxy (If (5 <=? 0) (0 - 5) (5 - 0)) -> Proxy 5
    f = id

    Currently, GHC is strict while evaluating functions, so this does not
    work, because even though the `If` should evaluate to `5 - 0`, we
    also evaluate the "then" branch which generates the constraint `0 - 5 ~ r`,
    which fails.

    So, for the time being, we only add an improvement when the RHS is a constant,
    which happens to work OK for the moment, although clearly we need to do
    something more general.
    -}

    -------------------------------------------------------------------------------
    --                   Multiplication (*)
    -------------------------------------------------------------------------------

    typeNatMulTyCon :: TyCon
    typeNatMulTyCon :: TyCon
    typeNatMulTyCon = Name -> BuiltInSynFamily -> TyCon
    mkTypeNatFunTyCon2 Name
    name
      BuiltInSynFamily { sfMatchFam :: [BuiltInFamRewrite]
    sfMatchFam = [BuiltInFamRewrite]
    axMulRewrites
                       , sfInteract :: [BuiltInFamInjectivity]
    sfInteract = [BuiltInFamInjectivity]
    axMulInjectivity  }
      where
        name :: Name
    name = BuiltInSyntax -> Module -> FastString -> Unique -> TyCon -> Name
    mkWiredInTyConName BuiltInSyntax
    UserSyntax Module
    gHC_INTERNAL_TYPENATS (String -> FastString
    fsLit String
    "*")
                  Unique
    typeNatMulTyFamNameKey TyCon
    typeNatMulTyCon

    axMulRewrites :: [BuiltInFamRewrite]
    axMulRewrites :: [BuiltInFamRewrite]
    axMulRewrites
      = [ TyCon -> String -> [TyVar] -> [Type] -> Type -> BuiltInFamRewrite
    mkRewriteAxiom   TyCon
    tc String
    "Mul0L" [TyVar
    tn] [Integer -> Type
    num Integer
    0, TyVar -> Type
    var TyVar
    tn] (Integer -> Type
    num Integer
    0)   -- 0 * t --> 0
        , TyCon -> String -> [TyVar] -> [Type] -> Type -> BuiltInFamRewrite
    mkRewriteAxiom   TyCon
    tc String
    "Mul0R" [TyVar
    sn] [TyVar -> Type
    var TyVar
    sn, Integer -> Type
    num Integer
    0] (Integer -> Type
    num Integer
    0)   -- s * 0 --> 0
        , TyCon -> String -> [TyVar] -> [Type] -> Type -> BuiltInFamRewrite
    mkRewriteAxiom   TyCon
    tc String
    "Mul1L" [TyVar
    tn] [Integer -> Type
    num Integer
    1, TyVar -> Type
    var TyVar
    tn] (TyVar -> Type
    var TyVar
    tn)  -- 1 * t --> t
        , TyCon -> String -> [TyVar] -> [Type] -> Type -> BuiltInFamRewrite
    mkRewriteAxiom   TyCon
    tc String
    "Mul1R" [TyVar
    sn] [TyVar -> Type
    var TyVar
    sn, Integer -> Type
    num Integer
    1] (TyVar -> Type
    var TyVar
    sn)  -- s * 1 --> s
        , TyCon
    -> String
    -> (Type -> Maybe Integer)
    -> (Type -> Maybe Integer)
    -> (Integer -> Integer -> Maybe Type)
    -> BuiltInFamRewrite
    forall a b.
    TyCon
    -> String
    -> (Type -> Maybe a)
    -> (Type -> Maybe b)
    -> (a -> b -> Maybe Type)
    -> BuiltInFamRewrite
    mkBinConstFoldAxiom TyCon
    tc String
    "MulDef" Type -> Maybe Integer
    isNumLitTy Type -> Maybe Integer
    isNumLitTy ((Integer -> Integer -> Maybe Type) -> BuiltInFamRewrite)
    -> (Integer -> Integer -> Maybe Type) -> BuiltInFamRewrite
    forall a b. (a -> b) -> a -> b
    $    -- 3 + 4 --> 12
          \Integer
    x Integer
    y -> Type -> Maybe Type
    forall a. a -> Maybe a
    Just (Type -> Maybe Type) -> Type -> Maybe Type
    forall a b. (a -> b) -> a -> b
    $ Integer -> Type
    num (Integer
    x Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    * Integer
    y) ]
      where
        tc :: TyCon
    tc = TyCon
    typeNatMulTyCon

    axMulInjectivity :: [BuiltInFamInjectivity]
    axMulInjectivity :: [BuiltInFamInjectivity]
    axMulInjectivity
      = [ -- (s * t ~ 1)  => (s ~ 1)
          String
    -> TyCon
    -> (Type -> Type -> Type -> Maybe TypeEqn)
    -> BuiltInFamInjectivity
    mkTopBinFamDeduction String
    "MulT1" TyCon
    tc ((Type -> Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity)
    -> (Type -> Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity
    forall a b. (a -> b) -> a -> b
    $ \ Type
    s Type
    _t Type
    r ->
          do { _ <- Type -> (Integer -> Bool) -> Maybe Integer
    known Type
    r (Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == Integer
    1); return (Pair s r) }

        , -- (s * t ~ 1)  => (t ~ 1)
          String
    -> TyCon
    -> (Type -> Type -> Type -> Maybe TypeEqn)
    -> BuiltInFamInjectivity
    mkTopBinFamDeduction String
    "MulT2" TyCon
    tc ((Type -> Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity)
    -> (Type -> Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity
    forall a b. (a -> b) -> a -> b
    $ \ Type
    _s Type
    t Type
    r ->
          do { _ <- Type -> (Integer -> Bool) -> Maybe Integer
    known Type
    r (Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == Integer
    1); return (Pair t r) }

        , -- (3 * t ~ 15) => (t ~ 5)
          String
    -> TyCon
    -> (Type -> Type -> Type -> Maybe TypeEqn)
    -> BuiltInFamInjectivity
    mkTopBinFamDeduction String
    "MulT3" TyCon
    tc ((Type -> Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity)
    -> (Type -> Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity
    forall a b. (a -> b) -> a -> b
    $ \ Type
    s Type
    t Type
    r ->
          do { ns <- Type -> Maybe Integer
    isNumLitTy Type
    s; nr <- isNumLitTy r; y <- divide nr ns; return (Pair t (num y)) }

        , -- (s * 3 ~ 15) => (s ~ 5)
          String
    -> TyCon
    -> (Type -> Type -> Type -> Maybe TypeEqn)
    -> BuiltInFamInjectivity
    mkTopBinFamDeduction String
    "MulT4" TyCon
    tc ((Type -> Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity)
    -> (Type -> Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity
    forall a b. (a -> b) -> a -> b
    $ \ Type
    s Type
    t Type
    r ->
          do { nt <- Type -> Maybe Integer
    isNumLitTy Type
    t; nr <- isNumLitTy r; y <- divide nr nt; return (Pair s (num y)) }

        , String
    -> TyCon
    -> WhichArg
    -> WhichArg
    -> (Type -> Bool)
    -> BuiltInFamInjectivity
    mkBinBIF String
    "MulI-xx" TyCon
    tc WhichArg
    ArgX WhichArg
    ArgX ((Integer -> Bool) -> Type -> Bool
    numGuard (Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Integer
    0))    -- (x*y1 ~ x*y2) {x/=0}=> (y1 ~ y2)
        , String
    -> TyCon
    -> WhichArg
    -> WhichArg
    -> (Type -> Bool)
    -> BuiltInFamInjectivity
    mkBinBIF String
    "MulI-yy" TyCon
    tc WhichArg
    ArgY WhichArg
    ArgY ((Integer -> Bool) -> Type -> Bool
    numGuard (Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Integer
    0))    -- (x1*y ~ x2*y) {y/=0}=> (x1 ~ x2)
        ]
      where
        tc :: TyCon
    tc = TyCon
    typeNatMulTyCon

    -------------------------------------------------------------------------------
    --                   Division: Div and Mod
    -------------------------------------------------------------------------------

    typeNatDivTyCon :: TyCon
    typeNatDivTyCon :: TyCon
    typeNatDivTyCon = Name -> BuiltInSynFamily -> TyCon
    mkTypeNatFunTyCon2 Name
    name
      BuiltInSynFamily { sfMatchFam :: [BuiltInFamRewrite]
    sfMatchFam = [BuiltInFamRewrite]
    axDivRewrites
                       , sfInteract :: [BuiltInFamInjectivity]
    sfInteract = [] }
      where
      name :: Name
    name = BuiltInSyntax -> Module -> FastString -> Unique -> TyCon -> Name
    mkWiredInTyConName BuiltInSyntax
    UserSyntax Module
    gHC_INTERNAL_TYPENATS (String -> FastString
    fsLit String
    "Div")
                Unique
    typeNatDivTyFamNameKey TyCon
    typeNatDivTyCon

    typeNatModTyCon :: TyCon
    typeNatModTyCon :: TyCon
    typeNatModTyCon = Name -> BuiltInSynFamily -> TyCon
    mkTypeNatFunTyCon2 Name
    name
      BuiltInSynFamily { sfMatchFam :: [BuiltInFamRewrite]
    sfMatchFam = [BuiltInFamRewrite]
    axModRewrites
                       , sfInteract :: [BuiltInFamInjectivity]
    sfInteract = [] }
      where
      name :: Name
    name = BuiltInSyntax -> Module -> FastString -> Unique -> TyCon -> Name
    mkWiredInTyConName BuiltInSyntax
    UserSyntax Module
    gHC_INTERNAL_TYPENATS (String -> FastString
    fsLit String
    "Mod")
                Unique
    typeNatModTyFamNameKey TyCon
    typeNatModTyCon

    axDivRewrites :: [BuiltInFamRewrite]
    axDivRewrites :: [BuiltInFamRewrite]
    axDivRewrites
      = [ TyCon -> String -> [TyVar] -> [Type] -> Type -> BuiltInFamRewrite
    mkRewriteAxiom   TyCon
    tc String
    "Div1" [TyVar
    sn] [TyVar -> Type
    var TyVar
    sn, Integer -> Type
    num Integer
    1] (TyVar -> Type
    var TyVar
    sn)   -- s `div` 1 --> s
        , TyCon
    -> String
    -> (Type -> Maybe Integer)
    -> (Type -> Maybe Integer)
    -> (Integer -> Integer -> Maybe Type)
    -> BuiltInFamRewrite
    forall a b.
    TyCon
    -> String
    -> (Type -> Maybe a)
    -> (Type -> Maybe b)
    -> (a -> b -> Maybe Type)
    -> BuiltInFamRewrite
    mkBinConstFoldAxiom TyCon
    tc String
    "DivDef" Type -> Maybe Integer
    isNumLitTy Type -> Maybe Integer
    isNumLitTy ((Integer -> Integer -> Maybe Type) -> BuiltInFamRewrite)
    -> (Integer -> Integer -> Maybe Type) -> BuiltInFamRewrite
    forall a b. (a -> b) -> a -> b
    $    -- 8 `div` 4 --> 2
          \Integer
    x Integer
    y -> do { Bool -> Maybe ()
    forall (f :: * -> *). Alternative f => Bool -> f ()
    guard (Integer
    y Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Integer
    0); Type -> Maybe Type
    forall a. a -> Maybe a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Integer -> Type
    num (Integer -> Integer -> Integer
    forall a. Integral a => a -> a -> a
    div Integer
    x Integer
    y)) } ]
      where
        tc :: TyCon
    tc = TyCon
    typeNatDivTyCon

    axModRewrites :: [BuiltInFamRewrite]
    axModRewrites :: [BuiltInFamRewrite]
    axModRewrites
      = [ TyCon -> String -> [TyVar] -> [Type] -> Type -> BuiltInFamRewrite
    mkRewriteAxiom   TyCon
    tc String
    "Mod1" [TyVar
    sn] [TyVar -> Type
    var TyVar
    sn, Integer -> Type
    num Integer
    1] (Integer -> Type
    num Integer
    0)   -- s `mod` 1 --> 0
        , TyCon
    -> String
    -> (Type -> Maybe Integer)
    -> (Type -> Maybe Integer)
    -> (Integer -> Integer -> Maybe Type)
    -> BuiltInFamRewrite
    forall a b.
    TyCon
    -> String
    -> (Type -> Maybe a)
    -> (Type -> Maybe b)
    -> (a -> b -> Maybe Type)
    -> BuiltInFamRewrite
    mkBinConstFoldAxiom TyCon
    tc String
    "ModDef" Type -> Maybe Integer
    isNumLitTy Type -> Maybe Integer
    isNumLitTy ((Integer -> Integer -> Maybe Type) -> BuiltInFamRewrite)
    -> (Integer -> Integer -> Maybe Type) -> BuiltInFamRewrite
    forall a b. (a -> b) -> a -> b
    $   -- 8 `mod` 3 --> 2
          \Integer
    x Integer
    y -> do { Bool -> Maybe ()
    forall (f :: * -> *). Alternative f => Bool -> f ()
    guard (Integer
    y Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Integer
    0); Type -> Maybe Type
    forall a. a -> Maybe a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Integer -> Type
    num (Integer -> Integer -> Integer
    forall a. Integral a => a -> a -> a
    mod Integer
    x Integer
    y)) } ]
      where
        tc :: TyCon
    tc = TyCon
    typeNatModTyCon

    -------------------------------------------------------------------------------
    --                   Exponentiation: Exp
    -------------------------------------------------------------------------------

    typeNatExpTyCon :: TyCon  -- Exponentiation
    typeNatExpTyCon :: TyCon
    typeNatExpTyCon = Name -> BuiltInSynFamily -> TyCon
    mkTypeNatFunTyCon2 Name
    name
      BuiltInSynFamily { sfMatchFam :: [BuiltInFamRewrite]
    sfMatchFam = [BuiltInFamRewrite]
    axExpRewrites
                       , sfInteract :: [BuiltInFamInjectivity]
    sfInteract = [BuiltInFamInjectivity]
    axExpInjectivity }
      where
      name :: Name
    name = BuiltInSyntax -> Module -> FastString -> Unique -> TyCon -> Name
    mkWiredInTyConName BuiltInSyntax
    UserSyntax Module
    gHC_INTERNAL_TYPENATS (String -> FastString
    fsLit String
    "^")
                    Unique
    typeNatExpTyFamNameKey TyCon
    typeNatExpTyCon

    axExpRewrites :: [BuiltInFamRewrite]
    axExpRewrites :: [BuiltInFamRewrite]
    axExpRewrites
      = [ TyCon -> String -> [TyVar] -> [Type] -> Type -> BuiltInFamRewrite
    mkRewriteAxiom   TyCon
    tc String
    "Exp0R" [TyVar
    sn] [TyVar -> Type
    var TyVar
    sn, Integer -> Type
    num Integer
    0] (Integer -> Type
    num Integer
    1)   -- s ^ 0 --> 1
        , TyCon -> String -> [TyVar] -> [Type] -> Type -> BuiltInFamRewrite
    mkRewriteAxiom   TyCon
    tc String
    "Exp1L" [TyVar
    tn] [Integer -> Type
    num Integer
    1, TyVar -> Type
    var TyVar
    tn] (Integer -> Type
    num Integer
    1)   -- 1 ^ t --> 1
        , TyCon -> String -> [TyVar] -> [Type] -> Type -> BuiltInFamRewrite
    mkRewriteAxiom   TyCon
    tc String
    "Exp1R" [TyVar
    sn] [TyVar -> Type
    var TyVar
    sn, Integer -> Type
    num Integer
    1] (TyVar -> Type
    var TyVar
    sn)  -- s ^ 1 --> s
        , TyCon
    -> String
    -> (Type -> Maybe Integer)
    -> (Type -> Maybe Integer)
    -> (Integer -> Integer -> Maybe Type)
    -> BuiltInFamRewrite
    forall a b.
    TyCon
    -> String
    -> (Type -> Maybe a)
    -> (Type -> Maybe b)
    -> (a -> b -> Maybe Type)
    -> BuiltInFamRewrite
    mkBinConstFoldAxiom TyCon
    tc String
    "ExpDef" Type -> Maybe Integer
    isNumLitTy Type -> Maybe Integer
    isNumLitTy ((Integer -> Integer -> Maybe Type) -> BuiltInFamRewrite)
    -> (Integer -> Integer -> Maybe Type) -> BuiltInFamRewrite
    forall a b. (a -> b) -> a -> b
    $    -- 2 ^ 3 --> 8
          \Integer
    x Integer
    y -> Type -> Maybe Type
    forall a. a -> Maybe a
    Just (Integer -> Type
    num (Integer
    x Integer -> Integer -> Integer
    forall a b. (Num a, Integral b) => a -> b -> a
    ^ Integer
    y)) ]
      where
        tc :: TyCon
    tc = TyCon
    typeNatExpTyCon

    axExpInjectivity :: [BuiltInFamInjectivity]
    axExpInjectivity :: [BuiltInFamInjectivity]
    axExpInjectivity
      = [ -- (s ^ t ~ 0) => (s ~ 0)
          String
    -> TyCon
    -> (Type -> Type -> Type -> Maybe TypeEqn)
    -> BuiltInFamInjectivity
    mkTopBinFamDeduction String
    "ExpT1" TyCon
    tc ((Type -> Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity)
    -> (Type -> Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity
    forall a b. (a -> b) -> a -> b
    $ \ Type
    s Type
    _t Type
    r ->
          do { Integer -> Maybe TypeEqn
    0 <- Type -> Maybe Integer
    isNumLitTy Type
    r; return (Pair s r) }

        , -- (2 ^ t ~ 8) => (t ~ 3)
          String
    -> TyCon
    -> (Type -> Type -> Type -> Maybe TypeEqn)
    -> BuiltInFamInjectivity
    mkTopBinFamDeduction String
    "ExpT2" TyCon
    tc ((Type -> Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity)
    -> (Type -> Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity
    forall a b. (a -> b) -> a -> b
    $ \ Type
    s Type
    t Type
    r ->
          do { ns <- Type -> Maybe Integer
    isNumLitTy Type
    s; nr <- isNumLitTy r; y <- logExact nr ns; return (Pair t (num y)) }

        , -- (s ^ 2 ~ 9) => (s ~ 3)
          String
    -> TyCon
    -> (Type -> Type -> Type -> Maybe TypeEqn)
    -> BuiltInFamInjectivity
    mkTopBinFamDeduction String
    "ExpT3" TyCon
    tc ((Type -> Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity)
    -> (Type -> Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity
    forall a b. (a -> b) -> a -> b
    $ \ Type
    s Type
    t Type
    r ->
          do { nt <- Type -> Maybe Integer
    isNumLitTy Type
    t; nr <- isNumLitTy r; y <- rootExact nr nt; return (Pair s (num y)) }

        , String
    -> TyCon
    -> WhichArg
    -> WhichArg
    -> (Type -> Bool)
    -> BuiltInFamInjectivity
    mkBinBIF String
    "ExpI-xx" TyCon
    tc WhichArg
    ArgX WhichArg
    ArgX ((Integer -> Bool) -> Type -> Bool
    numGuard (Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    > Integer
    1))    -- (x^y1 ~ x^y2) {x>1}=> (y1 ~ y2)
        , String
    -> TyCon
    -> WhichArg
    -> WhichArg
    -> (Type -> Bool)
    -> BuiltInFamInjectivity
    mkBinBIF String
    "ExpI-yy" TyCon
    tc WhichArg
    ArgY WhichArg
    ArgY ((Integer -> Bool) -> Type -> Bool
    numGuard (Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Integer
    0))   -- (x1*y ~ x2*y) {y/=0}=> (x1 ~ x2)
        ]
      where
        tc :: TyCon
    tc = TyCon
    typeNatExpTyCon

    -------------------------------------------------------------------------------
    --                   Logarithm: Log2
    -------------------------------------------------------------------------------

    typeNatLogTyCon :: TyCon
    typeNatLogTyCon :: TyCon
    typeNatLogTyCon = Name -> BuiltInSynFamily -> TyCon
    mkTypeNatFunTyCon1 Name
    name
      BuiltInSynFamily { sfMatchFam :: [BuiltInFamRewrite]
    sfMatchFam = [BuiltInFamRewrite]
    axLogRewrites
                       , sfInteract :: [BuiltInFamInjectivity]
    sfInteract = [] }
      where
      name :: Name
    name = BuiltInSyntax -> Module -> FastString -> Unique -> TyCon -> Name
    mkWiredInTyConName BuiltInSyntax
    UserSyntax Module
    gHC_INTERNAL_TYPENATS (String -> FastString
    fsLit String
    "Log2")
                Unique
    typeNatLogTyFamNameKey TyCon
    typeNatLogTyCon

    axLogRewrites :: [BuiltInFamRewrite]
    axLogRewrites :: [BuiltInFamRewrite]
    axLogRewrites
      = [ TyCon
    -> String
    -> (Type -> Maybe Integer)
    -> (Integer -> Maybe Type)
    -> BuiltInFamRewrite
    forall a.
    TyCon
    -> String
    -> (Type -> Maybe a)
    -> (a -> Maybe Type)
    -> BuiltInFamRewrite
    mkUnaryConstFoldAxiom TyCon
    tc String
    "LogDef" Type -> Maybe Integer
    isNumLitTy ((Integer -> Maybe Type) -> BuiltInFamRewrite)
    -> (Integer -> Maybe Type) -> BuiltInFamRewrite
    forall a b. (a -> b) -> a -> b
    $       -- log 8 --> 3
          \Integer
    x -> do { (a,_) <- Integer -> Integer -> Maybe (Integer, Bool)
    genLog Integer
    x Integer
    2; return (num a) } ]
      where
        tc :: TyCon
    tc = TyCon
    typeNatLogTyCon

    -------------------------------------------------------------------------------
    --               Comparision of Nats: CmpNat
    -------------------------------------------------------------------------------

    typeNatCmpTyCon :: TyCon
    typeNatCmpTyCon :: TyCon
    typeNatCmpTyCon
      = Name
    -> [TyConBinder]
    -> Type
    -> Maybe Name
    -> FamTyConFlav
    -> Maybe Class
    -> Injectivity
    -> TyCon
    mkFamilyTyCon Name
    name
          ([Type] -> [TyConBinder]
    mkTemplateAnonTyConBinders [ Type
    naturalTy, Type
    naturalTy ])
          Type
    orderingKind
          Maybe Name
    forall a. Maybe a
    Nothing
          (BuiltInSynFamily -> FamTyConFlav
    BuiltInSynFamTyCon BuiltInSynFamily
    ops)
          Maybe Class
    forall a. Maybe a
    Nothing
          Injectivity
    NotInjective

      where
        name :: Name
    name = BuiltInSyntax -> Module -> FastString -> Unique -> TyCon -> Name
    mkWiredInTyConName BuiltInSyntax
    UserSyntax Module
    gHC_INTERNAL_TYPENATS_INTERNAL (String -> FastString
    fsLit String
    "CmpNat")
                      Unique
    typeNatCmpTyFamNameKey TyCon
    typeNatCmpTyCon
        ops :: BuiltInSynFamily
    ops = BuiltInSynFamily { sfMatchFam :: [BuiltInFamRewrite]
    sfMatchFam = [BuiltInFamRewrite]
    axCmpNatRewrites
                               , sfInteract :: [BuiltInFamInjectivity]
    sfInteract = [BuiltInFamInjectivity]
    axCmpNatInjectivity }

    axCmpNatRewrites :: [BuiltInFamRewrite]
    axCmpNatRewrites :: [BuiltInFamRewrite]
    axCmpNatRewrites
      = [ TyCon -> String -> [TyVar] -> [Type] -> Type -> BuiltInFamRewrite
    mkRewriteAxiom   TyCon
    tc String
    "CmpNatRefl" [TyVar
    sn] [TyVar -> Type
    var TyVar
    sn, TyVar -> Type
    var TyVar
    sn] (Ordering -> Type
    ordering Ordering
    EQ)    -- s `cmp` s --> EQ
        , TyCon
    -> String
    -> (Type -> Maybe Integer)
    -> (Type -> Maybe Integer)
    -> (Integer -> Integer -> Maybe Type)
    -> BuiltInFamRewrite
    forall a b.
    TyCon
    -> String
    -> (Type -> Maybe a)
    -> (Type -> Maybe b)
    -> (a -> b -> Maybe Type)
    -> BuiltInFamRewrite
    mkBinConstFoldAxiom TyCon
    tc String
    "CmpNatDef" Type -> Maybe Integer
    isNumLitTy Type -> Maybe Integer
    isNumLitTy ((Integer -> Integer -> Maybe Type) -> BuiltInFamRewrite)
    -> (Integer -> Integer -> Maybe Type) -> BuiltInFamRewrite
    forall a b. (a -> b) -> a -> b
    $              -- 2 `cmp` 3 --> LT
          \Integer
    x Integer
    y -> Type -> Maybe Type
    forall a. a -> Maybe a
    Just (Ordering -> Type
    ordering (Integer -> Integer -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare Integer
    x Integer
    y)) ]
      where
        tc :: TyCon
    tc = TyCon
    typeNatCmpTyCon

    axCmpNatInjectivity :: [BuiltInFamInjectivity]
    axCmpNatInjectivity :: [BuiltInFamInjectivity]
    axCmpNatInjectivity
      = [ -- s `cmp` t ~ EQ   ==>   s ~ t
          String
    -> TyCon
    -> (Type -> Type -> Type -> Maybe TypeEqn)
    -> BuiltInFamInjectivity
    mkTopBinFamDeduction String
    "CmpNatT3" TyCon
    typeNatCmpTyCon ((Type -> Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity)
    -> (Type -> Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity
    forall a b. (a -> b) -> a -> b
    $ \ Type
    s Type
    t Type
    r ->
          do { Ordering -> Maybe TypeEqn
    EQ <- Type -> Maybe Ordering
    isOrderingLitTy Type
    r; return (Pair s t) } ]

    -------------------------------------------------------------------------------
    --              Comparsion of Symbols: CmpSymbol
    -------------------------------------------------------------------------------

    typeSymbolCmpTyCon :: TyCon
    typeSymbolCmpTyCon :: TyCon
    typeSymbolCmpTyCon =
      Name
    -> [TyConBinder]
    -> Type
    -> Maybe Name
    -> FamTyConFlav
    -> Maybe Class
    -> Injectivity
    -> TyCon
    mkFamilyTyCon Name
    name
        ([Type] -> [TyConBinder]
    mkTemplateAnonTyConBinders [Type
    typeSymbolKind, Type
    typeSymbolKind])
        Type
    orderingKind
        Maybe Name
    forall a. Maybe a
    Nothing
        (BuiltInSynFamily -> FamTyConFlav
    BuiltInSynFamTyCon BuiltInSynFamily
    ops)
        Maybe Class
    forall a. Maybe a
    Nothing
        Injectivity
    NotInjective

      where
      name :: Name
    name = BuiltInSyntax -> Module -> FastString -> Unique -> TyCon -> Name
    mkWiredInTyConName BuiltInSyntax
    UserSyntax Module
    gHC_INTERNAL_TYPELITS_INTERNAL (String -> FastString
    fsLit String
    "CmpSymbol")
                    Unique
    typeSymbolCmpTyFamNameKey TyCon
    typeSymbolCmpTyCon
      ops :: BuiltInSynFamily
    ops = BuiltInSynFamily { sfMatchFam :: [BuiltInFamRewrite]
    sfMatchFam = [BuiltInFamRewrite]
    axSymbolCmpRewrites
                             , sfInteract :: [BuiltInFamInjectivity]
    sfInteract = [BuiltInFamInjectivity]
    axSymbolCmpInjectivity }

    ss,ts :: TyVar  -- Of kind Symbol
    (TyVar
    ss: TyVar
    ts: [TyVar]
    _) = [Type] -> [TyVar]
    mkTemplateTyVars (Type -> [Type]
    forall a. a -> [a]
    repeat Type
    typeSymbolKind)

    axSymbolCmpRewrites :: [BuiltInFamRewrite]
    axSymbolCmpRewrites :: [BuiltInFamRewrite]
    axSymbolCmpRewrites
      = [ TyCon -> String -> [TyVar] -> [Type] -> Type -> BuiltInFamRewrite
    mkRewriteAxiom   TyCon
    tc String
    "CmpSymbolRefl" [TyVar
    ss] [TyVar -> Type
    var TyVar
    ss, TyVar -> Type
    var TyVar
    ss] (Ordering -> Type
    ordering Ordering
    EQ) -- s `cmp` s --> EQ
        , TyCon
    -> String
    -> (Type -> Maybe FastString)
    -> (Type -> Maybe FastString)
    -> (FastString -> FastString -> Maybe Type)
    -> BuiltInFamRewrite
    forall a b.
    TyCon
    -> String
    -> (Type -> Maybe a)
    -> (Type -> Maybe b)
    -> (a -> b -> Maybe Type)
    -> BuiltInFamRewrite
    mkBinConstFoldAxiom TyCon
    tc String
    "CmpSymbolDef" Type -> Maybe FastString
    isStrLitTy Type -> Maybe FastString
    isStrLitTy ((FastString -> FastString -> Maybe Type) -> BuiltInFamRewrite)
    -> (FastString -> FastString -> Maybe Type) -> BuiltInFamRewrite
    forall a b. (a -> b) -> a -> b
    $           -- "a" `cmp` "b" --> LT
          \FastString
    x FastString
    y -> Type -> Maybe Type
    forall a. a -> Maybe a
    Just (Ordering -> Type
    ordering (FastString -> FastString -> Ordering
    lexicalCompareFS FastString
    x FastString
    y)) ]
      where
        tc :: TyCon
    tc = TyCon
    typeSymbolCmpTyCon

    axSymbolCmpInjectivity :: [BuiltInFamInjectivity]
    axSymbolCmpInjectivity :: [BuiltInFamInjectivity]
    axSymbolCmpInjectivity
      = [ String
    -> TyCon
    -> (Type -> Type -> Type -> Maybe TypeEqn)
    -> BuiltInFamInjectivity
    mkTopBinFamDeduction String
    "CmpSymbolT" TyCon
    typeSymbolCmpTyCon ((Type -> Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity)
    -> (Type -> Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity
    forall a b. (a -> b) -> a -> b
    $ \ Type
    s Type
    t Type
    r ->
          do { Ordering -> Maybe TypeEqn
    EQ <- Type -> Maybe Ordering
    isOrderingLitTy Type
    r; return (Pair s t) } ]

    -------------------------------------------------------------------------------
    --            AppendSymbol
    -------------------------------------------------------------------------------

    typeSymbolAppendTyCon :: TyCon
    typeSymbolAppendTyCon :: TyCon
    typeSymbolAppendTyCon = Name -> BuiltInSynFamily -> TyCon
    mkTypeSymbolFunTyCon2 Name
    name
      BuiltInSynFamily { sfMatchFam :: [BuiltInFamRewrite]
    sfMatchFam = [BuiltInFamRewrite]
    axAppendRewrites
                       , sfInteract :: [BuiltInFamInjectivity]
    sfInteract = [BuiltInFamInjectivity]
    axAppendInjectivity }
      where
      name :: Name
    name = BuiltInSyntax -> Module -> FastString -> Unique -> TyCon -> Name
    mkWiredInTyConName BuiltInSyntax
    UserSyntax Module
    gHC_INTERNAL_TYPELITS (String -> FastString
    fsLit String
    "AppendSymbol")
                    Unique
    typeSymbolAppendFamNameKey TyCon
    typeSymbolAppendTyCon

    axAppendRewrites :: [BuiltInFamRewrite]
    axAppendRewrites :: [BuiltInFamRewrite]
    axAppendRewrites
      = [ TyCon -> String -> [TyVar] -> [Type] -> Type -> BuiltInFamRewrite
    mkRewriteAxiom   TyCon
    tc String
    "Concat0R" [TyVar
    ts] [Type
    nullStrLitTy, TyVar -> Type
    var TyVar
    ts] (TyVar -> Type
    var TyVar
    ts) -- "" ++ t --> t
        , TyCon -> String -> [TyVar] -> [Type] -> Type -> BuiltInFamRewrite
    mkRewriteAxiom   TyCon
    tc String
    "Concat0L" [TyVar
    ss] [TyVar -> Type
    var TyVar
    ss, Type
    nullStrLitTy] (TyVar -> Type
    var TyVar
    ss) -- s ++ "" --> s
        , TyCon
    -> String
    -> (Type -> Maybe FastString)
    -> (Type -> Maybe FastString)
    -> (FastString -> FastString -> Maybe Type)
    -> BuiltInFamRewrite
    forall a b.
    TyCon
    -> String
    -> (Type -> Maybe a)
    -> (Type -> Maybe b)
    -> (a -> b -> Maybe Type)
    -> BuiltInFamRewrite
    mkBinConstFoldAxiom TyCon
    tc String
    "AppendSymbolDef" Type -> Maybe FastString
    isStrLitTy Type -> Maybe FastString
    isStrLitTy ((FastString -> FastString -> Maybe Type) -> BuiltInFamRewrite)
    -> (FastString -> FastString -> Maybe Type) -> BuiltInFamRewrite
    forall a b. (a -> b) -> a -> b
    $    -- "a" ++ "b" --> "ab"
          \FastString
    x FastString
    y -> Type -> Maybe Type
    forall a. a -> Maybe a
    Just (FastString -> Type
    mkStrLitTy (FastString -> FastString -> FastString
    appendFS FastString
    x FastString
    y)) ]
      where
        tc :: TyCon
    tc = TyCon
    typeSymbolAppendTyCon

    axAppendInjectivity :: [BuiltInFamInjectivity]
    axAppendInjectivity :: [BuiltInFamInjectivity]
    axAppendInjectivity
     = [ -- (AppendSymbol a b ~ "") => (a ~ "")
         String
    -> TyCon
    -> (Type -> Type -> Type -> Maybe TypeEqn)
    -> BuiltInFamInjectivity
    mkTopBinFamDeduction String
    "AppendSymbolT1" TyCon
    tc ((Type -> Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity)
    -> (Type -> Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity
    forall a b. (a -> b) -> a -> b
    $ \ Type
    a Type
    _b Type
    r ->
         do { rs <- Type -> Maybe FastString
    isStrLitTy Type
    r; guard (nullFS rs); return (Pair a nullStrLitTy) }

       , -- (AppendSymbol a b ~ "") => (b ~ "")
         String
    -> TyCon
    -> (Type -> Type -> Type -> Maybe TypeEqn)
    -> BuiltInFamInjectivity
    mkTopBinFamDeduction String
    "AppendSymbolT2" TyCon
    tc ((Type -> Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity)
    -> (Type -> Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity
    forall a b. (a -> b) -> a -> b
    $ \ Type
    _a Type
    b Type
    r ->
         do { rs <- Type -> Maybe FastString
    isStrLitTy Type
    r; guard (nullFS rs); return (Pair b nullStrLitTy) }

       , -- (AppendSymbol "foo" b ~ "foobar") => (b ~ "bar")
         String
    -> TyCon
    -> (Type -> Type -> Type -> Maybe TypeEqn)
    -> BuiltInFamInjectivity
    mkTopBinFamDeduction String
    "AppendSymbolT3" TyCon
    tc ((Type -> Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity)
    -> (Type -> Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity
    forall a b. (a -> b) -> a -> b
    $ \ Type
    a Type
    b Type
    r ->
         do { as <- Type -> Maybe String
    isStrLitTyS Type
    a; rs <- isStrLitTyS r; guard (as `isPrefixOf` rs)
            ; return (Pair b (mkStrLitTyS (drop (length as) rs))) }

       , -- (AppendSymbol f "bar" ~ "foobar") => (f ~ "foo")
         String
    -> TyCon
    -> (Type -> Type -> Type -> Maybe TypeEqn)
    -> BuiltInFamInjectivity
    mkTopBinFamDeduction String
    "AppendSymbolT3" TyCon
    tc ((Type -> Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity)
    -> (Type -> Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity
    forall a b. (a -> b) -> a -> b
    $ \ Type
    a Type
    b Type
    r ->
         do { bs <- Type -> Maybe String
    isStrLitTyS Type
    b; rs <- isStrLitTyS r; guard (bs `isSuffixOf` rs)
            ; return (Pair a (mkStrLitTyS (take (length rs - length bs) rs))) }

        , String
    -> TyCon
    -> WhichArg
    -> WhichArg
    -> (Type -> Bool)
    -> BuiltInFamInjectivity
    mkBinBIF String
    "AppI-xx" TyCon
    tc WhichArg
    ArgX WhichArg
    ArgX Type -> Bool
    noGuard  -- (x++y1 ~ x++y2) => (y1 ~ y2)
        , String
    -> TyCon
    -> WhichArg
    -> WhichArg
    -> (Type -> Bool)
    -> BuiltInFamInjectivity
    mkBinBIF String
    "AppI-yy" TyCon
    tc WhichArg
    ArgY WhichArg
    ArgY Type -> Bool
    noGuard  -- (x1++y ~ x2++y) => (x1 ~ x2)
        ]
      where
        tc :: TyCon
    tc = TyCon
    typeSymbolAppendTyCon

    -------------------------------------------------------------------------------
    --            ConsSymbol
    -------------------------------------------------------------------------------

    typeConsSymbolTyCon :: TyCon
    typeConsSymbolTyCon :: TyCon
    typeConsSymbolTyCon =
      Name
    -> [TyConBinder]
    -> Type
    -> Maybe Name
    -> FamTyConFlav
    -> Maybe Class
    -> Injectivity
    -> TyCon
    mkFamilyTyCon Name
    name
        ([Type] -> [TyConBinder]
    mkTemplateAnonTyConBinders [ Type
    charTy, Type
    typeSymbolKind ])
        Type
    typeSymbolKind
        Maybe Name
    forall a. Maybe a
    Nothing
        (BuiltInSynFamily -> FamTyConFlav
    BuiltInSynFamTyCon BuiltInSynFamily
    ops)
        Maybe Class
    forall a. Maybe a
    Nothing
        ([Bool] -> Injectivity
    Injective [Bool
    True, Bool
    True])
      where
      name :: Name
    name = BuiltInSyntax -> Module -> FastString -> Unique -> TyCon -> Name
    mkWiredInTyConName BuiltInSyntax
    UserSyntax Module
    gHC_INTERNAL_TYPELITS (String -> FastString
    fsLit String
    "ConsSymbol")
                      Unique
    typeConsSymbolTyFamNameKey TyCon
    typeConsSymbolTyCon
      ops :: BuiltInSynFamily
    ops = BuiltInSynFamily  { sfMatchFam :: [BuiltInFamRewrite]
    sfMatchFam = [BuiltInFamRewrite]
    axConsRewrites
                              , sfInteract :: [BuiltInFamInjectivity]
    sfInteract = [BuiltInFamInjectivity]
    axConsInjectivity }

    axConsRewrites :: [BuiltInFamRewrite]
    axConsRewrites :: [BuiltInFamRewrite]
    axConsRewrites
      = [ TyCon
    -> String
    -> (Type -> Maybe Char)
    -> (Type -> Maybe FastString)
    -> (Char -> FastString -> Maybe Type)
    -> BuiltInFamRewrite
    forall a b.
    TyCon
    -> String
    -> (Type -> Maybe a)
    -> (Type -> Maybe b)
    -> (a -> b -> Maybe Type)
    -> BuiltInFamRewrite
    mkBinConstFoldAxiom TyCon
    tc String
    "ConsSymbolDef" Type -> Maybe Char
    isCharLitTy Type -> Maybe FastString
    isStrLitTy ((Char -> FastString -> Maybe Type) -> BuiltInFamRewrite)
    -> (Char -> FastString -> Maybe Type) -> BuiltInFamRewrite
    forall a b. (a -> b) -> a -> b
    $    -- 'a' : "bc" --> "abc"
          \Char
    x FastString
    y -> Type -> Maybe Type
    forall a. a -> Maybe a
    Just (Type -> Maybe Type) -> Type -> Maybe Type
    forall a b. (a -> b) -> a -> b
    $ FastString -> Type
    mkStrLitTy (Char -> FastString -> FastString
    consFS Char
    x FastString
    y) ]
      where
        tc :: TyCon
    tc = TyCon
    typeConsSymbolTyCon

    axConsInjectivity :: [BuiltInFamInjectivity]
    axConsInjectivity :: [BuiltInFamInjectivity]
    axConsInjectivity
      = [ -- ConsSymbol a b ~ "blah" => (a ~ 'b')
          String
    -> TyCon
    -> (Type -> Type -> Type -> Maybe TypeEqn)
    -> BuiltInFamInjectivity
    mkTopBinFamDeduction String
    "ConsSymbolT1" TyCon
    tc ((Type -> Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity)
    -> (Type -> Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity
    forall a b. (a -> b) -> a -> b
    $ \ Type
    a Type
    _b Type
    r ->
          do { rs <- Type -> Maybe FastString
    isStrLitTy Type
    r; (x,_) <- unconsFS rs; return (Pair a (mkCharLitTy x)) }

        , -- ConsSymbol a b ~ "blah" => (b ~ "lah")
          String
    -> TyCon
    -> (Type -> Type -> Type -> Maybe TypeEqn)
    -> BuiltInFamInjectivity
    mkTopBinFamDeduction String
    "ConsSymbolT2" TyCon
    tc ((Type -> Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity)
    -> (Type -> Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity
    forall a b. (a -> b) -> a -> b
    $ \ Type
    _a Type
    b Type
    r ->
          do { rs <- Type -> Maybe FastString
    isStrLitTy Type
    r; (_,xs) <- unconsFS rs; return (Pair b (mkStrLitTy xs)) }

        , String
    -> TyCon
    -> WhichArg
    -> WhichArg
    -> (Type -> Bool)
    -> BuiltInFamInjectivity
    mkBinBIF String
    "ConsI-xx" TyCon
    tc WhichArg
    ArgX WhichArg
    ArgX Type -> Bool
    noGuard  -- (x:y1 ~ x:y2) => (y1 ~ y2)
        , String
    -> TyCon
    -> WhichArg
    -> WhichArg
    -> (Type -> Bool)
    -> BuiltInFamInjectivity
    mkBinBIF String
    "ConsI-yy" TyCon
    tc WhichArg
    ArgY WhichArg
    ArgY Type -> Bool
    noGuard  -- (x1:y ~ x2:y) => (x1 ~ x2)
        ]
      where
        tc :: TyCon
    tc = TyCon
    typeConsSymbolTyCon

    -------------------------------------------------------------------------------
    --            UnconsSymbol
    -------------------------------------------------------------------------------

    typeUnconsSymbolTyCon :: TyCon
    typeUnconsSymbolTyCon :: TyCon
    typeUnconsSymbolTyCon =
      Name
    -> [TyConBinder]
    -> Type
    -> Maybe Name
    -> FamTyConFlav
    -> Maybe Class
    -> Injectivity
    -> TyCon
    mkFamilyTyCon Name
    name
        ([Type] -> [TyConBinder]
    mkTemplateAnonTyConBinders [ Type
    typeSymbolKind ])
        (Type -> Type
    mkMaybeTy Type
    charSymbolPairKind)
        Maybe Name
    forall a. Maybe a
    Nothing
        (BuiltInSynFamily -> FamTyConFlav
    BuiltInSynFamTyCon BuiltInSynFamily
    ops)
        Maybe Class
    forall a. Maybe a
    Nothing
        ([Bool] -> Injectivity
    Injective [Bool
    True])
      where
      name :: Name
    name = BuiltInSyntax -> Module -> FastString -> Unique -> TyCon -> Name
    mkWiredInTyConName BuiltInSyntax
    UserSyntax Module
    gHC_INTERNAL_TYPELITS (String -> FastString
    fsLit String
    "UnconsSymbol")
                      Unique
    typeUnconsSymbolTyFamNameKey TyCon
    typeUnconsSymbolTyCon
      ops :: BuiltInSynFamily
    ops = BuiltInSynFamily { sfMatchFam :: [BuiltInFamRewrite]
    sfMatchFam = [BuiltInFamRewrite]
    axUnconsRewrites
                             , sfInteract :: [BuiltInFamInjectivity]
    sfInteract = [BuiltInFamInjectivity]
    axUnconsInjectivity }

    computeUncons :: FastString -> Type
    computeUncons :: FastString -> Type
    computeUncons FastString
    str
      = Type -> Maybe Type -> Type
    mkPromotedMaybeTy Type
    charSymbolPairKind (((Char, FastString) -> Type)
    -> Maybe (Char, FastString) -> Maybe Type
    forall a b. (a -> b) -> Maybe a -> Maybe b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (Char, FastString) -> Type
    reify (FastString -> Maybe (Char, FastString)
    unconsFS FastString
    str))
      where
        reify :: (Char, FastString) -> Type
        reify :: (Char, FastString) -> Type
    reify (Char
    c, FastString
    s) = Type -> Type -> Type
    charSymbolPair (Char -> Type
    mkCharLitTy Char
    c) (FastString -> Type
    mkStrLitTy FastString
    s)

    axUnconsRewrites :: [BuiltInFamRewrite]
    axUnconsRewrites :: [BuiltInFamRewrite]
    axUnconsRewrites
      = [ TyCon
    -> String
    -> (Type -> Maybe FastString)
    -> (FastString -> Maybe Type)
    -> BuiltInFamRewrite
    forall a.
    TyCon
    -> String
    -> (Type -> Maybe a)
    -> (a -> Maybe Type)
    -> BuiltInFamRewrite
    mkUnaryConstFoldAxiom TyCon
    tc String
    "ConsSymbolDef" Type -> Maybe FastString
    isStrLitTy ((FastString -> Maybe Type) -> BuiltInFamRewrite)
    -> (FastString -> Maybe Type) -> BuiltInFamRewrite
    forall a b. (a -> b) -> a -> b
    $    -- 'a' : "bc" --> "abc"
          \FastString
    x -> Type -> Maybe Type
    forall a. a -> Maybe a
    Just (Type -> Maybe Type) -> Type -> Maybe Type
    forall a b. (a -> b) -> a -> b
    $ FastString -> Type
    computeUncons FastString
    x ]
      where
        tc :: TyCon
    tc = TyCon
    typeUnconsSymbolTyCon

    axUnconsInjectivity :: [BuiltInFamInjectivity]
    axUnconsInjectivity :: [BuiltInFamInjectivity]
    axUnconsInjectivity
      = [ -- (UnconsSymbol b ~ Nothing) => (b ~ "")
          String
    -> TyCon
    -> (Type -> Type -> Maybe TypeEqn)
    -> BuiltInFamInjectivity
    mkTopUnaryFamDeduction String
    "UnconsSymbolT1" TyCon
    tc ((Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity)
    -> (Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity
    forall a b. (a -> b) -> a -> b
    $ \Type
    b Type
    r ->
          do { Maybe Type -> Maybe TypeEqn
    Nothing  <- Type -> Maybe (Maybe Type)
    isPromotedMaybeTy Type
    r; return (Pair b nullStrLitTy) }

        , -- (UnconsSymbol b ~ Just ('f',"oobar")) => (b ~ "foobar")
          String
    -> TyCon
    -> (Type -> Type -> Maybe TypeEqn)
    -> BuiltInFamInjectivity
    mkTopUnaryFamDeduction String
    "UnconsSymbolT2" TyCon
    tc ((Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity)
    -> (Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity
    forall a b. (a -> b) -> a -> b
    $ \Type
    b Type
    r ->
          do { Just pr <- Type -> Maybe (Maybe Type)
    isPromotedMaybeTy Type
    r
             ; (c,s) <- isPromotedPairType pr
             ; chr <- isCharLitTy c
             ; str <- isStrLitTy s
             ; return (Pair b (mkStrLitTy (consFS chr str))) }

        , String -> TyCon -> BuiltInFamInjectivity
    mkUnaryBIF String
    "UnconsI1" TyCon
    tc  -- (UnconsSymbol x1 ~ z, UnconsSymbol x2 ~ z) => (x1 ~ x2)
        ]
      where
        tc :: TyCon
    tc = TyCon
    typeUnconsSymbolTyCon

    -------------------------------------------------------------------------------
    --            CharToNat
    -------------------------------------------------------------------------------

    typeCharToNatTyCon :: TyCon
    typeCharToNatTyCon :: TyCon
    typeCharToNatTyCon =
      Name
    -> [TyConBinder]
    -> Type
    -> Maybe Name
    -> FamTyConFlav
    -> Maybe Class
    -> Injectivity
    -> TyCon
    mkFamilyTyCon Name
    name
        ([Type] -> [TyConBinder]
    mkTemplateAnonTyConBinders [ Type
    charTy ])
        Type
    naturalTy
        Maybe Name
    forall a. Maybe a
    Nothing
        (BuiltInSynFamily -> FamTyConFlav
    BuiltInSynFamTyCon BuiltInSynFamily
    ops)
        Maybe Class
    forall a. Maybe a
    Nothing
        ([Bool] -> Injectivity
    Injective [Bool
    True])
      where
      name :: Name
    name = BuiltInSyntax -> Module -> FastString -> Unique -> TyCon -> Name
    mkWiredInTyConName BuiltInSyntax
    UserSyntax Module
    gHC_INTERNAL_TYPELITS (String -> FastString
    fsLit String
    "CharToNat")
                      Unique
    typeCharToNatTyFamNameKey TyCon
    typeCharToNatTyCon
      ops :: BuiltInSynFamily
    ops = BuiltInSynFamily { sfMatchFam :: [BuiltInFamRewrite]
    sfMatchFam = [BuiltInFamRewrite]
    axCharToNatRewrites
                             , sfInteract :: [BuiltInFamInjectivity]
    sfInteract = [BuiltInFamInjectivity]
    axCharToNatInjectivity }

    axCharToNatRewrites :: [BuiltInFamRewrite]
    axCharToNatRewrites :: [BuiltInFamRewrite]
    axCharToNatRewrites
      = [ TyCon
    -> String
    -> (Type -> Maybe Char)
    -> (Char -> Maybe Type)
    -> BuiltInFamRewrite
    forall a.
    TyCon
    -> String
    -> (Type -> Maybe a)
    -> (a -> Maybe Type)
    -> BuiltInFamRewrite
    mkUnaryConstFoldAxiom TyCon
    tc String
    "CharToNatDef" Type -> Maybe Char
    isCharLitTy ((Char -> Maybe Type) -> BuiltInFamRewrite)
    -> (Char -> Maybe Type) -> BuiltInFamRewrite
    forall a b. (a -> b) -> a -> b
    $    -- CharToNat 'a' --> 97
          \Char
    x -> Type -> Maybe Type
    forall a. a -> Maybe a
    Just (Type -> Maybe Type) -> Type -> Maybe Type
    forall a b. (a -> b) -> a -> b
    $ Integer -> Type
    num (Char -> Integer
    charToInteger Char
    x) ]
      where
        tc :: TyCon
    tc = TyCon
    typeCharToNatTyCon

    axCharToNatInjectivity :: [BuiltInFamInjectivity]
    axCharToNatInjectivity :: [BuiltInFamInjectivity]
    axCharToNatInjectivity
      = [ -- (CharToNat c ~ 122) => (c ~ 'z')
          String
    -> TyCon
    -> (Type -> Type -> Maybe TypeEqn)
    -> BuiltInFamInjectivity
    mkTopUnaryFamDeduction String
    "CharToNatT1" TyCon
    typeCharToNatTyCon ((Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity)
    -> (Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity
    forall a b. (a -> b) -> a -> b
    $ \Type
    c Type
    r ->
          do { nr <- Type -> Maybe Integer
    isNumLitTy Type
    r; chr <- integerToChar nr; return (Pair c (mkCharLitTy chr)) } ]

    -------------------------------------------------------------------------------
    --            NatToChar
    -------------------------------------------------------------------------------

    typeNatToCharTyCon :: TyCon
    typeNatToCharTyCon :: TyCon
    typeNatToCharTyCon =
      Name
    -> [TyConBinder]
    -> Type
    -> Maybe Name
    -> FamTyConFlav
    -> Maybe Class
    -> Injectivity
    -> TyCon
    mkFamilyTyCon Name
    name
        ([Type] -> [TyConBinder]
    mkTemplateAnonTyConBinders [ Type
    naturalTy ])
        Type
    charTy
        Maybe Name
    forall a. Maybe a
    Nothing
        (BuiltInSynFamily -> FamTyConFlav
    BuiltInSynFamTyCon BuiltInSynFamily
    ops)
        Maybe Class
    forall a. Maybe a
    Nothing
        ([Bool] -> Injectivity
    Injective [Bool
    True])
      where
      name :: Name
    name = BuiltInSyntax -> Module -> FastString -> Unique -> TyCon -> Name
    mkWiredInTyConName BuiltInSyntax
    UserSyntax Module
    gHC_INTERNAL_TYPELITS (String -> FastString
    fsLit String
    "NatToChar")
                      Unique
    typeNatToCharTyFamNameKey TyCon
    typeNatToCharTyCon
      ops :: BuiltInSynFamily
    ops = BuiltInSynFamily { sfMatchFam :: [BuiltInFamRewrite]
    sfMatchFam = [BuiltInFamRewrite]
    axNatToCharRewrites
                             , sfInteract :: [BuiltInFamInjectivity]
    sfInteract = [BuiltInFamInjectivity]
    axNatToCharInjectivity }

    axNatToCharRewrites :: [BuiltInFamRewrite]
    axNatToCharRewrites :: [BuiltInFamRewrite]
    axNatToCharRewrites
      = [ TyCon
    -> String
    -> (Type -> Maybe Integer)
    -> (Integer -> Maybe Type)
    -> BuiltInFamRewrite
    forall a.
    TyCon
    -> String
    -> (Type -> Maybe a)
    -> (a -> Maybe Type)
    -> BuiltInFamRewrite
    mkUnaryConstFoldAxiom TyCon
    tc String
    "NatToCharDef" Type -> Maybe Integer
    isNumLitTy ((Integer -> Maybe Type) -> BuiltInFamRewrite)
    -> (Integer -> Maybe Type) -> BuiltInFamRewrite
    forall a b. (a -> b) -> a -> b
    $    -- NatToChar 97 --> 'a'
          \Integer
    n -> (Char -> Type) -> Maybe Char -> Maybe Type
    forall a b. (a -> b) -> Maybe a -> Maybe b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Char -> Type
    mkCharLitTy (Integer -> Maybe Char
    integerToChar Integer
    n) ]
      where
        tc :: TyCon
    tc = TyCon
    typeNatToCharTyCon

    axNatToCharInjectivity :: [BuiltInFamInjectivity]
    axNatToCharInjectivity :: [BuiltInFamInjectivity]
    axNatToCharInjectivity
      = [ -- (NatToChar n ~ 'z') => (n ~ 122)
          String
    -> TyCon
    -> (Type -> Type -> Maybe TypeEqn)
    -> BuiltInFamInjectivity
    mkTopUnaryFamDeduction String
    "CharToNatT1" TyCon
    typeNatToCharTyCon ((Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity)
    -> (Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity
    forall a b. (a -> b) -> a -> b
    $ \Type
    n Type
    r ->
          do { c <- Type -> Maybe Char
    isCharLitTy Type
    r; return (Pair n (mkNumLitTy (charToInteger c))) } ]

    -----------------------------------------------------------------------------
    --                       CmpChar
    -----------------------------------------------------------------------------

    typeCharCmpTyCon :: TyCon
    typeCharCmpTyCon :: TyCon
    typeCharCmpTyCon =
      Name
    -> [TyConBinder]
    -> Type
    -> Maybe Name
    -> FamTyConFlav
    -> Maybe Class
    -> Injectivity
    -> TyCon
    mkFamilyTyCon Name
    name
        ([Type] -> [TyConBinder]
    mkTemplateAnonTyConBinders [ Type
    charTy, Type
    charTy ])
        Type
    orderingKind
        Maybe Name
    forall a. Maybe a
    Nothing
        (BuiltInSynFamily -> FamTyConFlav
    BuiltInSynFamTyCon BuiltInSynFamily
    ops)
        Maybe Class
    forall a. Maybe a
    Nothing
        Injectivity
    NotInjective
      where
      name :: Name
    name = BuiltInSyntax -> Module -> FastString -> Unique -> TyCon -> Name
    mkWiredInTyConName BuiltInSyntax
    UserSyntax Module
    gHC_INTERNAL_TYPELITS_INTERNAL (String -> FastString
    fsLit String
    "CmpChar")
                      Unique
    typeCharCmpTyFamNameKey TyCon
    typeCharCmpTyCon
      ops :: BuiltInSynFamily
    ops = BuiltInSynFamily { sfMatchFam :: [BuiltInFamRewrite]
    sfMatchFam = [BuiltInFamRewrite]
    axCharCmpRewrites
                             , sfInteract :: [BuiltInFamInjectivity]
    sfInteract = [BuiltInFamInjectivity]
    axCharCmpInjectivity }

    sc :: TyVar  -- Of kind Char
    (TyVar
    sc: [TyVar]
    _) = [Type] -> [TyVar]
    mkTemplateTyVars (Type -> [Type]
    forall a. a -> [a]
    repeat Type
    charTy)

    axCharCmpRewrites :: [BuiltInFamRewrite]
    axCharCmpRewrites :: [BuiltInFamRewrite]
    axCharCmpRewrites
      = [ TyCon -> String -> [TyVar] -> [Type] -> Type -> BuiltInFamRewrite
    mkRewriteAxiom   TyCon
    tc String
    "CmpCharRefl" [TyVar
    sc] [TyVar -> Type
    var TyVar
    sc, TyVar -> Type
    var TyVar
    sc] (Ordering -> Type
    ordering Ordering
    EQ) -- s `cmp` s --> EQ
        , TyCon
    -> String
    -> (Type -> Maybe Char)
    -> (Type -> Maybe Char)
    -> (Char -> Char -> Maybe Type)
    -> BuiltInFamRewrite
    forall a b.
    TyCon
    -> String
    -> (Type -> Maybe a)
    -> (Type -> Maybe b)
    -> (a -> b -> Maybe Type)
    -> BuiltInFamRewrite
    mkBinConstFoldAxiom TyCon
    tc String
    "CmpCharDef" Type -> Maybe Char
    isCharLitTy Type -> Maybe Char
    isCharLitTy ((Char -> Char -> Maybe Type) -> BuiltInFamRewrite)
    -> (Char -> Char -> Maybe Type) -> BuiltInFamRewrite
    forall a b. (a -> b) -> a -> b
    $         -- 'a' `cmp` 'b' --> LT
          \Char
    chr1 Char
    chr2 -> Type -> Maybe Type
    forall a. a -> Maybe a
    Just (Type -> Maybe Type) -> Type -> Maybe Type
    forall a b. (a -> b) -> a -> b
    $ Ordering -> Type
    ordering (Ordering -> Type) -> Ordering -> Type
    forall a b. (a -> b) -> a -> b
    $ Char -> Char -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare Char
    chr1 Char
    chr2 ]
      where
        tc :: TyCon
    tc = TyCon
    typeCharCmpTyCon

    axCharCmpInjectivity :: [BuiltInFamInjectivity]
    axCharCmpInjectivity :: [BuiltInFamInjectivity]
    axCharCmpInjectivity
      = [  -- (CmpChar s t ~ EQ) => s ~ t
          String
    -> TyCon
    -> (Type -> Type -> Type -> Maybe TypeEqn)
    -> BuiltInFamInjectivity
    mkTopBinFamDeduction String
    "CmpCharT" TyCon
    typeCharCmpTyCon ((Type -> Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity)
    -> (Type -> Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity
    forall a b. (a -> b) -> a -> b
    $ \ Type
    s Type
    t Type
    r ->
          do { Ordering -> Maybe TypeEqn
    EQ <- Type -> Maybe Ordering
    isOrderingLitTy Type
    r; return (Pair s t) } ]

    {-------------------------------------------------------------------------------
    Various utilities for making axioms and types
    -------------------------------------------------------------------------------}

    (===) :: Type -> Type -> Pair Type
    Type
    x === :: Type -> Type -> TypeEqn
    === Type
    y = Type -> Type -> TypeEqn
    forall a. a -> a -> Pair a
    Pair Type
    x Type
    y

    num :: Integer -> Type
    num :: Integer -> Type
    num = Integer -> Type
    mkNumLitTy

    var :: TyVar -> Type
    var :: TyVar -> Type
    var = TyVar -> Type
    mkTyVarTy

    (.+.) :: Type -> Type -> Type
    Type
    s .+. :: Type -> Type -> Type
    .+. Type
    t = TyCon -> [Type] -> Type
    mkTyConApp TyCon
    typeNatAddTyCon [Type
    s,Type
    t]

    {-
    (.-.) :: Type -> Type -> Type
    s .-. t = mkTyConApp typeNatSubTyCon [s,t]

    (.*.) :: Type -> Type -> Type
    s .*. t = mkTyConApp typeNatMulTyCon [s,t]

    tDiv :: Type -> Type -> Type
    tDiv s t = mkTyConApp typeNatDivTyCon [s,t]

    tMod :: Type -> Type -> Type
    tMod s t = mkTyConApp typeNatModTyCon [s,t]

    (.^.) :: Type -> Type -> Type
    s .^. t = mkTyConApp typeNatExpTyCon [s,t]

    cmpNat :: Type -> Type -> Type
    cmpNat s t = mkTyConApp typeNatCmpTyCon [s,t]

    cmpSymbol :: Type -> Type -> Type
    cmpSymbol s t = mkTyConApp typeSymbolCmpTyCon [s,t]

    appendSymbol :: Type -> Type -> Type
    appendSymbol s t = mkTyConApp typeSymbolAppendTyCon [s, t]
    -}

    nullStrLitTy :: Type  -- The type ""
    nullStrLitTy :: Type
    nullStrLitTy = FastString -> Type
    mkStrLitTy FastString
    nilFS

    isStrLitTyS :: Type -> Maybe String
    isStrLitTyS :: Type -> Maybe String
    isStrLitTyS Type
    ty = do { fs <- Type -> Maybe FastString
    isStrLitTy Type
    ty; return (unpackFS fs) }

    mkStrLitTyS :: String -> Type
    mkStrLitTyS :: String -> Type
    mkStrLitTyS String
    s = FastString -> Type
    mkStrLitTy (String -> FastString
    mkFastString String
    s)

    charSymbolPair :: Type -> Type -> Type
    charSymbolPair :: Type -> Type -> Type
    charSymbolPair = Type -> Type -> Type -> Type -> Type
    mkPromotedPairTy Type
    charTy Type
    typeSymbolKind

    charSymbolPairKind :: Kind
    charSymbolPairKind :: Type
    charSymbolPairKind = TyCon -> [Type] -> Type
    mkTyConApp TyCon
    pairTyCon [Type
    charTy, Type
    typeSymbolKind]

    orderingKind :: Kind
    orderingKind :: Type
    orderingKind = TyCon -> [Type] -> Type
    mkTyConApp TyCon
    orderingTyCon []

    ordering :: Ordering -> Type
    ordering :: Ordering -> Type
    ordering Ordering
    o =
      case Ordering
    o of
        Ordering
    LT -> TyCon -> [Type] -> Type
    mkTyConApp TyCon
    promotedLTDataCon []
        Ordering
    EQ -> TyCon -> [Type] -> Type
    mkTyConApp TyCon
    promotedEQDataCon []
        Ordering
    GT -> TyCon -> [Type] -> Type
    mkTyConApp TyCon
    promotedGTDataCon []

    isOrderingLitTy :: Type -> Maybe Ordering
    isOrderingLitTy :: Type -> Maybe Ordering
    isOrderingLitTy Type
    tc =
      do (tc1,[]) <- HasDebugCallStack => Type -> Maybe (TyCon, [Type])
    Type -> Maybe (TyCon, [Type])
    splitTyConApp_maybe Type
    tc
         case () of
           ()
    _ | TyCon
    tc1 TyCon -> TyCon -> Bool
    forall a. Eq a => a -> a -> Bool
    == TyCon
    promotedLTDataCon -> Ordering -> Maybe Ordering
    forall a. a -> Maybe a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Ordering
    LT
             | TyCon
    tc1 TyCon -> TyCon -> Bool
    forall a. Eq a => a -> a -> Bool
    == TyCon
    promotedEQDataCon -> Ordering -> Maybe Ordering
    forall a. a -> Maybe a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Ordering
    EQ
             | TyCon
    tc1 TyCon -> TyCon -> Bool
    forall a. Eq a => a -> a -> Bool
    == TyCon
    promotedGTDataCon -> Ordering -> Maybe Ordering
    forall a. a -> Maybe a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Ordering
    GT
             | Bool
    otherwise                -> Maybe Ordering
    forall a. Maybe a
    Nothing

    -- Make a unary built-in constructor of kind: Nat -> Nat
    mkTypeNatFunTyCon1 :: Name -> BuiltInSynFamily -> TyCon
    mkTypeNatFunTyCon1 :: Name -> BuiltInSynFamily -> TyCon
    mkTypeNatFunTyCon1 Name
    op BuiltInSynFamily
    tcb =
      Name
    -> [TyConBinder]
    -> Type
    -> Maybe Name
    -> FamTyConFlav
    -> Maybe Class
    -> Injectivity
    -> TyCon
    mkFamilyTyCon Name
    op
        ([Type] -> [TyConBinder]
    mkTemplateAnonTyConBinders [ Type
    naturalTy ])
        Type
    naturalTy
        Maybe Name
    forall a. Maybe a
    Nothing
        (BuiltInSynFamily -> FamTyConFlav
    BuiltInSynFamTyCon BuiltInSynFamily
    tcb)
        Maybe Class
    forall a. Maybe a
    Nothing
        Injectivity
    NotInjective

    -- Make a binary built-in constructor of kind: Nat -> Nat -> Nat
    mkTypeNatFunTyCon2 :: Name -> BuiltInSynFamily -> TyCon
    mkTypeNatFunTyCon2 :: Name -> BuiltInSynFamily -> TyCon
    mkTypeNatFunTyCon2 Name
    op BuiltInSynFamily
    tcb =
      Name
    -> [TyConBinder]
    -> Type
    -> Maybe Name
    -> FamTyConFlav
    -> Maybe Class
    -> Injectivity
    -> TyCon
    mkFamilyTyCon Name
    op
        ([Type] -> [TyConBinder]
    mkTemplateAnonTyConBinders [ Type
    naturalTy, Type
    naturalTy ])
        Type
    naturalTy
        Maybe Name
    forall a. Maybe a
    Nothing
        (BuiltInSynFamily -> FamTyConFlav
    BuiltInSynFamTyCon BuiltInSynFamily
    tcb)
        Maybe Class
    forall a. Maybe a
    Nothing
        Injectivity
    NotInjective

    -- Make a binary built-in constructor of kind: Symbol -> Symbol -> Symbol
    mkTypeSymbolFunTyCon2 :: Name -> BuiltInSynFamily -> TyCon
    mkTypeSymbolFunTyCon2 :: Name -> BuiltInSynFamily -> TyCon
    mkTypeSymbolFunTyCon2 Name
    op BuiltInSynFamily
    tcb =
      Name
    -> [TyConBinder]
    -> Type
    -> Maybe Name
    -> FamTyConFlav
    -> Maybe Class
    -> Injectivity
    -> TyCon
    mkFamilyTyCon Name
    op
        ([Type] -> [TyConBinder]
    mkTemplateAnonTyConBinders [ Type
    typeSymbolKind, Type
    typeSymbolKind ])
        Type
    typeSymbolKind
        Maybe Name
    forall a. Maybe a
    Nothing
        (BuiltInSynFamily -> FamTyConFlav
    BuiltInSynFamTyCon BuiltInSynFamily
    tcb)
        Maybe Class
    forall a. Maybe a
    Nothing
        Injectivity
    NotInjective

    same :: Type -> Type -> Maybe ()
    same :: Type -> Type -> Maybe ()
    same Type
    ty1 Type
    ty2 = Bool -> Maybe ()
    forall (f :: * -> *). Alternative f => Bool -> f ()
    guard (Type
    ty1 HasDebugCallStack => Type -> Type -> Bool
    Type -> Type -> Bool
    `tcEqType` Type
    ty2)

    known :: Type -> (Integer -> Bool) -> Maybe Integer
    known :: Type -> (Integer -> Bool) -> Maybe Integer
    known Type
    x Integer -> Bool
    p = do { nx <- Type -> Maybe Integer
    isNumLitTy Type
    x; guard (p nx); return nx }

    charToInteger :: Char -> Integer
    charToInteger :: Char -> Integer
    charToInteger Char
    c = Int -> Integer
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral (Char -> Int
    Char.ord Char
    c)

    integerToChar :: Integer -> Maybe Char
    integerToChar :: Integer -> Maybe Char
    integerToChar Integer
    n | Bool
    inBounds = Char -> Maybe Char
    forall a. a -> Maybe a
    Just (Int -> Char
    Char.chr (Integer -> Int
    forall a. Num a => Integer -> a
    fromInteger Integer
    n))
      where inBounds :: Bool
    inBounds = Integer
    n Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    >= Char -> Integer
    charToInteger Char
    forall a. Bounded a => a
    minBound Bool -> Bool -> Bool
    &&
                       Integer
    n Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Char -> Integer
    charToInteger Char
    forall a. Bounded a => a
    maxBound
    integerToChar Integer
    _ = Maybe Char
    forall a. Maybe a
    Nothing

    {- -----------------------------------------------------------------------------
    These inverse functions are used for simplifying propositions using
    concrete natural numbers.
    ----------------------------------------------------------------------------- -}

    -- | Subtract two natural numbers.
    minus :: Integer -> Integer -> Maybe Integer
    minus :: Integer -> Integer -> Maybe Integer
    minus Integer
    x Integer
    y = if Integer
    x Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    >= Integer
    y then Integer -> Maybe Integer
    forall a. a -> Maybe a
    Just (Integer
    x Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    y) else Maybe Integer
    forall a. Maybe a
    Nothing

    -- | Compute the exact logarithm of a natural number.
    -- The logarithm base is the second argument.
    logExact :: Integer -> Integer -> Maybe Integer
    logExact :: Integer -> Integer -> Maybe Integer
    logExact Integer
    x Integer
    y = do (z,True) <- Integer -> Integer -> Maybe (Integer, Bool)
    genLog Integer
    x Integer
    y
                      return z

    -- | Divide two natural numbers.
    divide :: Integer -> Integer -> Maybe Integer
    divide :: Integer -> Integer -> Maybe Integer
    divide Integer
    _ Integer
    0  = Maybe Integer
    forall a. Maybe a
    Nothing
    divide Integer
    x Integer
    y  = case Integer -> Integer -> (Integer, Integer)
    forall a. Integral a => a -> a -> (a, a)
    divMod Integer
    x Integer
    y of
                    (Integer
    a,Integer
    0) -> Integer -> Maybe Integer
    forall a. a -> Maybe a
    Just Integer
    a
                    (Integer, Integer)
    _     -> Maybe Integer
    forall a. Maybe a
    Nothing

    -- | Compute the exact root of a natural number.
    -- The second argument specifies which root we are computing.
    rootExact :: Integer -> Integer -> Maybe Integer
    rootExact :: Integer -> Integer -> Maybe Integer
    rootExact Integer
    x Integer
    y = do (z,True) <- Integer -> Integer -> Maybe (Integer, Bool)
    genRoot Integer
    x Integer
    y
                       return z

    {- | Compute the n-th root of a natural number, rounded down to
    the closest natural number.  The boolean indicates if the result
    is exact (i.e., True means no rounding was done, False means rounded down).
    The second argument specifies which root we are computing. -}
    genRoot :: Integer -> Integer -> Maybe (Integer, Bool)
    genRoot :: Integer -> Integer -> Maybe (Integer, Bool)
    genRoot Integer
    _  Integer
    0    = Maybe (Integer, Bool)
    forall a. Maybe a
    Nothing
    genRoot Integer
    x0 Integer
    1    = (Integer, Bool) -> Maybe (Integer, Bool)
    forall a. a -> Maybe a
    Just (Integer
    x0, Bool
    True)
    genRoot Integer
    x0 Integer
    root = (Integer, Bool) -> Maybe (Integer, Bool)
    forall a. a -> Maybe a
    Just (Integer -> Integer -> (Integer, Bool)
    search Integer
    0 (Integer
    x0Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    +Integer
    1))
      where
      search :: Integer -> Integer -> (Integer, Bool)
    search Integer
    from Integer
    to = let x :: Integer
    x = Integer
    from Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    + Integer -> Integer -> Integer
    forall a. Integral a => a -> a -> a
    div (Integer
    to Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    from) Integer
    2
                           a :: Integer
    a = Integer
    x Integer -> Integer -> Integer
    forall a b. (Num a, Integral b) => a -> b -> a
    ^ Integer
    root
                       in case Integer -> Integer -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare Integer
    a Integer
    x0 of
                            Ordering
    EQ              -> (Integer
    x, Bool
    True)
                            Ordering
    LT | Integer
    x Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Integer
    from  -> Integer -> Integer -> (Integer, Bool)
    search Integer
    x Integer
    to
                               | Bool
    otherwise  -> (Integer
    from, Bool
    False)
                            Ordering
    GT | Integer
    x Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Integer
    to    -> Integer -> Integer -> (Integer, Bool)
    search Integer
    from Integer
    x
                               | Bool
    otherwise  -> (Integer
    from, Bool
    False)

    {- | Compute the logarithm of a number in the given base, rounded down to the
    closest integer.  The boolean indicates if we the result is exact
    (i.e., True means no rounding happened, False means we rounded down).
    The logarithm base is the second argument. -}
    genLog :: Integer -> Integer -> Maybe (Integer, Bool)
    genLog :: Integer -> Integer -> Maybe (Integer, Bool)
    genLog Integer
    x Integer
    0    = if Integer
    x Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == Integer
    1 then (Integer, Bool) -> Maybe (Integer, Bool)
    forall a. a -> Maybe a
    Just (Integer
    0, Bool
    True) else Maybe (Integer, Bool)
    forall a. Maybe a
    Nothing
    genLog Integer
    _ Integer
    1    = Maybe (Integer, Bool)
    forall a. Maybe a
    Nothing
    genLog Integer
    0 Integer
    _    = Maybe (Integer, Bool)
    forall a. Maybe a
    Nothing
    genLog Integer
    x Integer
    base = (Integer, Bool) -> Maybe (Integer, Bool)
    forall a. a -> Maybe a
    Just (Integer -> Integer -> (Integer, Bool)
    exactLoop Integer
    0 Integer
    x)
      where
      exactLoop :: Integer -> Integer -> (Integer, Bool)
    exactLoop Integer
    s Integer
    i
        | Integer
    i Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == Integer
    1     = (Integer
    s,Bool
    True)
        | Integer
    i Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    < Integer
    base   = (Integer
    s,Bool
    False)
        | Bool
    otherwise  =
            let s1 :: Integer
    s1 = Integer
    s Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    + Integer
    1
            in Integer
    s1 Integer -> (Integer, Bool) -> (Integer, Bool)
    forall a b. a -> b -> b
    `seq` case Integer -> Integer -> (Integer, Integer)
    forall a. Integral a => a -> a -> (a, a)
    divMod Integer
    i Integer
    base of
                          (Integer
    j,Integer
    r)
                            | Integer
    r Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == Integer
    0    -> Integer -> Integer -> (Integer, Bool)
    exactLoop Integer
    s1 Integer
    j
                            | Bool
    otherwise -> (Integer -> Integer -> Integer
    underLoop Integer
    s1 Integer
    j, Bool
    False)

      underLoop :: Integer -> Integer -> Integer
    underLoop Integer
    s Integer
    i
        | Integer
    i Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    < Integer
    base  = Integer
    s
        | Bool
    otherwise = let s1 :: Integer
    s1 = Integer
    s Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    + Integer
    1 in Integer
    s1 Integer -> Integer -> Integer
    forall a b. a -> b -> b
    `seq` Integer -> Integer -> Integer
    underLoop Integer
    s1 (Integer -> Integer -> Integer
    forall a. Integral a => a -> a -> a
    div Integer
    i Integer
    base)