    {-# LANGUAGE DataKinds #-}
    {-# LANGUAGE GADTs #-}
    {-# LANGUAGE PatternSynonyms #-}
    {-# LANGUAGE PolyKinds #-}
    {-# LANGUAGE ScopedTypeVariables #-}
    {-# LANGUAGE TemplateHaskell #-}
    {-# LANGUAGE TypeFamilies #-}
    {-# LANGUAGE TypeOperators #-}

    {-|
    Module           : What4.SpecialFunctions
    Description      : Utilities relating to special functions
    Copyright        : (c) Galois, Inc 2021
    License          : BSD3
    Maintainer       : Rob Dockins <rdockins@galois.com>

    Utilties for representing and handling certain \"special\"
    functions arising from analysis. Although many of these
    functions are most properly understood as complex valued
    functions on complex arguments, here we are primarily interested
    in their restriction to real-valued functions or their
    floating-point approximations.

    The functions considered here include functions from
    standard and hyperbolic trigonometry, exponential
    and logarithmic functions, etc.  Some of these functions
    are defineable in terms of others (e.g. @tan(x) = sin(x)/cos(x)@
    or expm1(x) = exp(x) - 1@) but are commonly implemented
    separately in math libraries for increased precision.
    Some popular constant values are also included.
    -}

    module What4.SpecialFunctions
      ( -- * Representation of special functions
        R
      , SpecialFunction(..)

        -- ** Symmetry properties of special functions
      , FunctionSymmetry(..)
      , specialFnSymmetry

        -- ** Packaging arguments to special functions
      , SpecialFnArg(..)
      , traverseSpecialFnArg
      , SpecialFnArgs(..)
      , traverseSpecialFnArgs

        -- ** Interval data for domain and range
      , RealPoint(..)
      , RealBound(..)
      , RealInterval(..)
      , specialFnDomain
      , specialFnRange
      ) where

    import           Data.Kind (Type)
    import           Data.Parameterized.Classes
    import qualified Data.Parameterized.Context as Ctx
    import           Data.Parameterized.Context ( pattern (:>) )
    import           Data.Parameterized.Ctx
    import           Data.Parameterized.TH.GADT
    import           Data.Parameterized.TraversableFC

    -- | Some special functions exhibit useful symmetries in their arguments.
    --   A function @f@ is an odd function if @f(-x) = -f(x)@, and is even
    --   if @f(-x) = f(x)@.  We extend this notion to arguments of more than
    --   one function by saying that a function is even/odd in its @i@th
    --   argument if it is even/odd when the other arguments are fixed.
    data FunctionSymmetry r
      = NoSymmetry
      | EvenFunction
      | OddFunction
     deriving (Int -> FunctionSymmetry r -> ShowS
    [FunctionSymmetry r] -> ShowS
    FunctionSymmetry r -> String
    (Int -> FunctionSymmetry r -> ShowS)
    -> (FunctionSymmetry r -> String)
    -> ([FunctionSymmetry r] -> ShowS)
    -> Show (FunctionSymmetry r)
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    forall k (r :: k). Int -> FunctionSymmetry r -> ShowS
    forall k (r :: k). [FunctionSymmetry r] -> ShowS
    forall k (r :: k). FunctionSymmetry r -> String
    $cshowsPrec :: forall k (r :: k). Int -> FunctionSymmetry r -> ShowS
    showsPrec :: Int -> FunctionSymmetry r -> ShowS
    $cshow :: forall k (r :: k). FunctionSymmetry r -> String
    show :: FunctionSymmetry r -> String
    $cshowList :: forall k (r :: k). [FunctionSymmetry r] -> ShowS
    showList :: [FunctionSymmetry r] -> ShowS
    Show)

    -- | Phantom data index representing the real number line.
    --   Used for specifying the arity of special functions.
    data R

    -- | Data type for representing \"special\" functions.
    --   These include functions from standard and hyperbolic
    --   trigonometry, exponential and logarithmic functions,
    --   as well as other well-known mathematical functions.
    --
    --   Generally, little solver support exists for such functions
    --   (although systems like dReal and Metatarski can prove some
    --   properties).  Nonetheless, we may have some information about
    --   specific values these functions take, the domains on which they
    --   are defined, or the range of values their outputs may take, or
    --   specific relationships that may exists between these functions
    --   (e.g., trig identities).  This information may, in some
    --   circumstances, be sufficent to prove properties of interest, even
    --   if the functions cannot be represented in their entirety.
    data SpecialFunction (args :: Ctx Type) where
      -- constant values involving Pi
      Pi             :: SpecialFunction EmptyCtx -- pi
      HalfPi         :: SpecialFunction EmptyCtx -- pi/2
      QuarterPi      :: SpecialFunction EmptyCtx -- pi/4
      OneOverPi      :: SpecialFunction EmptyCtx -- 1/pi
      TwoOverPi      :: SpecialFunction EmptyCtx -- 2/pi
      TwoOverSqrt_Pi :: SpecialFunction EmptyCtx -- 2/sqrt(pi)

      -- constant root values
      Sqrt_2         :: SpecialFunction EmptyCtx -- sqrt(2)
      Sqrt_OneHalf   :: SpecialFunction EmptyCtx -- sqrt(1/2)

      -- constant values involving exponentials and logarithms
      E              :: SpecialFunction EmptyCtx  -- e = exp(1)
      Log2_E         :: SpecialFunction EmptyCtx  -- log_2(e)
      Log10_E        :: SpecialFunction EmptyCtx  -- log_10(e)
      Ln_2           :: SpecialFunction EmptyCtx  -- ln(2)
      Ln_10          :: SpecialFunction EmptyCtx  -- ln(10)

      -- circular trigonometry functions
      Sin    :: SpecialFunction (EmptyCtx ::> R) -- sin(x)
      Cos    :: SpecialFunction (EmptyCtx ::> R) -- cos(x)
      Tan    :: SpecialFunction (EmptyCtx ::> R) -- tan(x) = sin(x)/cos(x)
      Arcsin :: SpecialFunction (EmptyCtx ::> R) -- inverse sin
      Arccos :: SpecialFunction (EmptyCtx ::> R) -- inverse cos
      Arctan :: SpecialFunction (EmptyCtx ::> R) -- inverse tan

      -- hyperbolic trigonometry functions
      Sinh    :: SpecialFunction (EmptyCtx ::> R) -- sinh(x) (hyperbolic sine)
      Cosh    :: SpecialFunction (EmptyCtx ::> R) -- cosh(x)
      Tanh    :: SpecialFunction (EmptyCtx ::> R) -- tanh(x)
      Arcsinh :: SpecialFunction (EmptyCtx ::> R) -- inverse sinh
      Arccosh :: SpecialFunction (EmptyCtx ::> R) -- inverse cosh
      Arctanh :: SpecialFunction (EmptyCtx ::> R) -- inverse tanh

      -- rectangular to polar coordinate conversion
      Hypot   :: SpecialFunction (EmptyCtx ::> R ::> R) -- hypot(x,y) = sqrt(x^2 + y^2)
      Arctan2 :: SpecialFunction (EmptyCtx ::> R ::> R) -- atan2(y,x) = atan(y/x)

      -- exponential and logarithm functions
      Pow     :: SpecialFunction (EmptyCtx ::> R ::> R) -- x^y
      Exp     :: SpecialFunction (EmptyCtx ::> R) -- exp(x)
      Log     :: SpecialFunction (EmptyCtx ::> R) -- ln(x)
      Expm1   :: SpecialFunction (EmptyCtx ::> R) -- exp(x) - 1
      Log1p   :: SpecialFunction (EmptyCtx ::> R) -- ln(1+x)

      -- base 2 exponential and logarithm
      Exp2    :: SpecialFunction (EmptyCtx ::> R) -- 2^x
      Log2    :: SpecialFunction (EmptyCtx ::> R) -- log_2(x)

      -- base 10 exponential and logarithm
      Exp10   :: SpecialFunction (EmptyCtx ::> R) -- 10^x
      Log10   :: SpecialFunction (EmptyCtx ::> R) -- log_10(x)

    instance Show (SpecialFunction args) where
      show :: SpecialFunction args -> String
    show SpecialFunction args
    fn = case SpecialFunction args
    fn of
        SpecialFunction args
    Pi             -> String
    "pi"
        SpecialFunction args
    HalfPi         -> String
    "halfPi"
        SpecialFunction args
    QuarterPi      -> String
    "quaterPi"
        SpecialFunction args
    OneOverPi      -> String
    "oneOverPi"
        SpecialFunction args
    TwoOverPi      -> String
    "twoOverPi"
        SpecialFunction args
    TwoOverSqrt_Pi -> String
    "twoOverSqrt_Pi"
        SpecialFunction args
    Sqrt_2         -> String
    "sqrt_2"
        SpecialFunction args
    Sqrt_OneHalf   -> String
    "sqrt_oneHalf"

        SpecialFunction args
    E              -> String
    "e"
        SpecialFunction args
    Log2_E         -> String
    "log2_e"
        SpecialFunction args
    Log10_E        -> String
    "log10_e"
        SpecialFunction args
    Ln_2           -> String
    "ln_2"
        SpecialFunction args
    Ln_10          -> String
    "ln_10"

        SpecialFunction args
    Sin            -> String
    "sin"
        SpecialFunction args
    Cos            -> String
    "cos"
        SpecialFunction args
    Tan            -> String
    "tan"
        SpecialFunction args
    Arcsin         -> String
    "arcsin"
        SpecialFunction args
    Arccos         -> String
    "arccos"
        SpecialFunction args
    Arctan         -> String
    "arctan"

        SpecialFunction args
    Sinh           -> String
    "sinh"
        SpecialFunction args
    Cosh           -> String
    "cosh"
        SpecialFunction args
    Tanh           -> String
    "tanh"
        SpecialFunction args
    Arcsinh        -> String
    "arcsinh"
        SpecialFunction args
    Arccosh        -> String
    "arccosh"
        SpecialFunction args
    Arctanh        -> String
    "arctanh"

        SpecialFunction args
    Hypot          -> String
    "hypot"
        SpecialFunction args
    Arctan2        -> String
    "atan2"

        SpecialFunction args
    Pow            -> String
    "pow"
        SpecialFunction args
    Exp            -> String
    "exp"
        SpecialFunction args
    Log            -> String
    "ln"
        SpecialFunction args
    Expm1          -> String
    "expm1"
        SpecialFunction args
    Log1p          -> String
    "log1p"
        SpecialFunction args
    Exp2           -> String
    "exp2"
        SpecialFunction args
    Log2           -> String
    "log2"
        SpecialFunction args
    Exp10          -> String
    "exp10"
        SpecialFunction args
    Log10          -> String
    "log10"

    -- | Values that can appear in the definition of domain and
    --   range intervals for special functions.
    data RealPoint
      = Zero
      | NegOne
      | PosOne
      | NegInf
      | PosInf
      | NegPi
      | PosPi
      | NegHalfPi
      | PosHalfPi

    instance Show RealPoint where
      show :: RealPoint -> String
    show RealPoint
    Zero   = String
    "0"
      show RealPoint
    NegOne = String
    "-1"
      show RealPoint
    PosOne = String
    "+1"
      show RealPoint
    NegInf = String
    "-∞"
      show RealPoint
    PosInf = String
    "+∞"
      show RealPoint
    NegPi  = String
    "-π"
      show RealPoint
    PosPi  = String
    "+π"
      show RealPoint
    NegHalfPi = String
    "-π/2"
      show RealPoint
    PosHalfPi = String
    "+π/2"

    -- | The endpoint of an interval, which may be inclusive or exclusive.
    data RealBound
      = Incl RealPoint
      | Excl RealPoint

    -- | An interval on real values, or a point.
    data RealInterval r where
      RealPoint    :: SpecialFunction EmptyCtx -> RealInterval R
      RealInterval :: RealBound -> RealBound -> RealInterval R

    instance Show (RealInterval r) where
      show :: RealInterval r -> String
    show (RealPoint SpecialFunction 'EmptyCtx
    x) = SpecialFunction 'EmptyCtx -> String
    forall a. Show a => a -> String
    show SpecialFunction 'EmptyCtx
    x
      show (RealInterval RealBound
    lo RealBound
    hi) = String
    lostr String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    ", " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    histr
        where
          lostr :: String
    lostr = case RealBound
    lo of
                    Incl RealPoint
    x -> String
    "[" String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ RealPoint -> String
    forall a. Show a => a -> String
    show RealPoint
    x
                    Excl RealPoint
    x -> String
    "(" String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ RealPoint -> String
    forall a. Show a => a -> String
    show RealPoint
    x
          histr :: String
    histr = case RealBound
    hi of
                    Incl RealPoint
    x -> RealPoint -> String
    forall a. Show a => a -> String
    show RealPoint
    x String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    "]"
                    Excl RealPoint
    x -> RealPoint -> String
    forall a. Show a => a -> String
    show RealPoint
    x String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"

    -- | Compute function symmetry information for the given special function.
    specialFnSymmetry :: SpecialFunction args -> Ctx.Assignment FunctionSymmetry args
    specialFnSymmetry :: forall (args :: Ctx Type).
    SpecialFunction args -> Assignment FunctionSymmetry args
    specialFnSymmetry SpecialFunction args
    fn = case SpecialFunction args
    fn of
        SpecialFunction args
    Pi             -> Assignment FunctionSymmetry args
    forall {k} (ctx :: Ctx k) (f :: k -> Type).
    (ctx ~ EmptyCtx) =>
    Assignment f ctx
    Ctx.Empty
        SpecialFunction args
    HalfPi         -> Assignment FunctionSymmetry args
    forall {k} (ctx :: Ctx k) (f :: k -> Type).
    (ctx ~ EmptyCtx) =>
    Assignment f ctx
    Ctx.Empty
        SpecialFunction args
    QuarterPi      -> Assignment FunctionSymmetry args
    forall {k} (ctx :: Ctx k) (f :: k -> Type).
    (ctx ~ EmptyCtx) =>
    Assignment f ctx
    Ctx.Empty
        SpecialFunction args
    OneOverPi      -> Assignment FunctionSymmetry args
    forall {k} (ctx :: Ctx k) (f :: k -> Type).
    (ctx ~ EmptyCtx) =>
    Assignment f ctx
    Ctx.Empty
        SpecialFunction args
    TwoOverPi      -> Assignment FunctionSymmetry args
    forall {k} (ctx :: Ctx k) (f :: k -> Type).
    (ctx ~ EmptyCtx) =>
    Assignment f ctx
    Ctx.Empty
        SpecialFunction args
    TwoOverSqrt_Pi -> Assignment FunctionSymmetry args
    forall {k} (ctx :: Ctx k) (f :: k -> Type).
    (ctx ~ EmptyCtx) =>
    Assignment f ctx
    Ctx.Empty
        SpecialFunction args
    Sqrt_2         -> Assignment FunctionSymmetry args
    forall {k} (ctx :: Ctx k) (f :: k -> Type).
    (ctx ~ EmptyCtx) =>
    Assignment f ctx
    Ctx.Empty
        SpecialFunction args
    Sqrt_OneHalf   -> Assignment FunctionSymmetry args
    forall {k} (ctx :: Ctx k) (f :: k -> Type).
    (ctx ~ EmptyCtx) =>
    Assignment f ctx
    Ctx.Empty
        SpecialFunction args
    E              -> Assignment FunctionSymmetry args
    forall {k} (ctx :: Ctx k) (f :: k -> Type).
    (ctx ~ EmptyCtx) =>
    Assignment f ctx
    Ctx.Empty
        SpecialFunction args
    Log2_E         -> Assignment FunctionSymmetry args
    forall {k} (ctx :: Ctx k) (f :: k -> Type).
    (ctx ~ EmptyCtx) =>
    Assignment f ctx
    Ctx.Empty
        SpecialFunction args
    Log10_E        -> Assignment FunctionSymmetry args
    forall {k} (ctx :: Ctx k) (f :: k -> Type).
    (ctx ~ EmptyCtx) =>
    Assignment f ctx
    Ctx.Empty
        SpecialFunction args
    Ln_2           -> Assignment FunctionSymmetry args
    forall {k} (ctx :: Ctx k) (f :: k -> Type).
    (ctx ~ EmptyCtx) =>
    Assignment f ctx
    Ctx.Empty
        SpecialFunction args
    Ln_10          -> Assignment FunctionSymmetry args
    forall {k} (ctx :: Ctx k) (f :: k -> Type).
    (ctx ~ EmptyCtx) =>
    Assignment f ctx
    Ctx.Empty

        SpecialFunction args
    Sin            -> Assignment FunctionSymmetry 'EmptyCtx
    forall {k} (ctx :: Ctx k) (f :: k -> Type).
    (ctx ~ EmptyCtx) =>
    Assignment f ctx
    Ctx.Empty Assignment FunctionSymmetry 'EmptyCtx
    -> FunctionSymmetry R -> Assignment FunctionSymmetry args
    forall {k} (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k)
           (tp :: k).
    (ctx' ~ (ctx ::> tp)) =>
    Assignment f ctx -> f tp -> Assignment f ctx'
    :> FunctionSymmetry R
    forall {k} (r :: k). FunctionSymmetry r
    OddFunction
        SpecialFunction args
    Cos            -> Assignment FunctionSymmetry 'EmptyCtx
    forall {k} (ctx :: Ctx k) (f :: k -> Type).
    (ctx ~ EmptyCtx) =>
    Assignment f ctx
    Ctx.Empty Assignment FunctionSymmetry 'EmptyCtx
    -> FunctionSymmetry R -> Assignment FunctionSymmetry args
    forall {k} (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k)
           (tp :: k).
    (ctx' ~ (ctx ::> tp)) =>
    Assignment f ctx -> f tp -> Assignment f ctx'
    :> FunctionSymmetry R
    forall {k} (r :: k). FunctionSymmetry r
    EvenFunction
        SpecialFunction args
    Tan            -> Assignment FunctionSymmetry 'EmptyCtx
    forall {k} (ctx :: Ctx k) (f :: k -> Type).
    (ctx ~ EmptyCtx) =>
    Assignment f ctx
    Ctx.Empty Assignment FunctionSymmetry 'EmptyCtx
    -> FunctionSymmetry R -> Assignment FunctionSymmetry args
    forall {k} (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k)
           (tp :: k).
    (ctx' ~ (ctx ::> tp)) =>
    Assignment f ctx -> f tp -> Assignment f ctx'
    :> FunctionSymmetry R
    forall {k} (r :: k). FunctionSymmetry r
    OddFunction
        SpecialFunction args
    Arcsin         -> Assignment FunctionSymmetry 'EmptyCtx
    forall {k} (ctx :: Ctx k) (f :: k -> Type).
    (ctx ~ EmptyCtx) =>
    Assignment f ctx
    Ctx.Empty Assignment FunctionSymmetry 'EmptyCtx
    -> FunctionSymmetry R -> Assignment FunctionSymmetry args
    forall {k} (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k)
           (tp :: k).
    (ctx' ~ (ctx ::> tp)) =>
    Assignment f ctx -> f tp -> Assignment f ctx'
    :> FunctionSymmetry R
    forall {k} (r :: k). FunctionSymmetry r
    OddFunction
        SpecialFunction args
    Arccos         -> Assignment FunctionSymmetry 'EmptyCtx
    forall {k} (ctx :: Ctx k) (f :: k -> Type).
    (ctx ~ EmptyCtx) =>
    Assignment f ctx
    Ctx.Empty Assignment FunctionSymmetry 'EmptyCtx
    -> FunctionSymmetry R -> Assignment FunctionSymmetry args
    forall {k} (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k)
           (tp :: k).
    (ctx' ~ (ctx ::> tp)) =>
    Assignment f ctx -> f tp -> Assignment f ctx'
    :> FunctionSymmetry R
    forall {k} (r :: k). FunctionSymmetry r
    NoSymmetry
        SpecialFunction args
    Arctan         -> Assignment FunctionSymmetry 'EmptyCtx
    forall {k} (ctx :: Ctx k) (f :: k -> Type).
    (ctx ~ EmptyCtx) =>
    Assignment f ctx
    Ctx.Empty Assignment FunctionSymmetry 'EmptyCtx
    -> FunctionSymmetry R -> Assignment FunctionSymmetry args
    forall {k} (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k)
           (tp :: k).
    (ctx' ~ (ctx ::> tp)) =>
    Assignment f ctx -> f tp -> Assignment f ctx'
    :> FunctionSymmetry R
    forall {k} (r :: k). FunctionSymmetry r
    OddFunction

        SpecialFunction args
    Sinh           -> Assignment FunctionSymmetry 'EmptyCtx
    forall {k} (ctx :: Ctx k) (f :: k -> Type).
    (ctx ~ EmptyCtx) =>
    Assignment f ctx
    Ctx.Empty Assignment FunctionSymmetry 'EmptyCtx
    -> FunctionSymmetry R -> Assignment FunctionSymmetry args
    forall {k} (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k)
           (tp :: k).
    (ctx' ~ (ctx ::> tp)) =>
    Assignment f ctx -> f tp -> Assignment f ctx'
    :> FunctionSymmetry R
    forall {k} (r :: k). FunctionSymmetry r
    OddFunction
        SpecialFunction args
    Cosh           -> Assignment FunctionSymmetry 'EmptyCtx
    forall {k} (ctx :: Ctx k) (f :: k -> Type).
    (ctx ~ EmptyCtx) =>
    Assignment f ctx
    Ctx.Empty Assignment FunctionSymmetry 'EmptyCtx
    -> FunctionSymmetry R -> Assignment FunctionSymmetry args
    forall {k} (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k)
           (tp :: k).
    (ctx' ~ (ctx ::> tp)) =>
    Assignment f ctx -> f tp -> Assignment f ctx'
    :> FunctionSymmetry R
    forall {k} (r :: k). FunctionSymmetry r
    EvenFunction
        SpecialFunction args
    Tanh           -> Assignment FunctionSymmetry 'EmptyCtx
    forall {k} (ctx :: Ctx k) (f :: k -> Type).
    (ctx ~ EmptyCtx) =>
    Assignment f ctx
    Ctx.Empty Assignment FunctionSymmetry 'EmptyCtx
    -> FunctionSymmetry R -> Assignment FunctionSymmetry args
    forall {k} (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k)
           (tp :: k).
    (ctx' ~ (ctx ::> tp)) =>
    Assignment f ctx -> f tp -> Assignment f ctx'
    :> FunctionSymmetry R
    forall {k} (r :: k). FunctionSymmetry r
    OddFunction
        SpecialFunction args
    Arcsinh        -> Assignment FunctionSymmetry 'EmptyCtx
    forall {k} (ctx :: Ctx k) (f :: k -> Type).
    (ctx ~ EmptyCtx) =>
    Assignment f ctx
    Ctx.Empty Assignment FunctionSymmetry 'EmptyCtx
    -> FunctionSymmetry R -> Assignment FunctionSymmetry args
    forall {k} (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k)
           (tp :: k).
    (ctx' ~ (ctx ::> tp)) =>
    Assignment f ctx -> f tp -> Assignment f ctx'
    :> FunctionSymmetry R
    forall {k} (r :: k). FunctionSymmetry r
    OddFunction
        SpecialFunction args
    Arccosh        -> Assignment FunctionSymmetry 'EmptyCtx
    forall {k} (ctx :: Ctx k) (f :: k -> Type).
    (ctx ~ EmptyCtx) =>
    Assignment f ctx
    Ctx.Empty Assignment FunctionSymmetry 'EmptyCtx
    -> FunctionSymmetry R -> Assignment FunctionSymmetry args
    forall {k} (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k)
           (tp :: k).
    (ctx' ~ (ctx ::> tp)) =>
    Assignment f ctx -> f tp -> Assignment f ctx'
    :> FunctionSymmetry R
    forall {k} (r :: k). FunctionSymmetry r
    NoSymmetry
        SpecialFunction args
    Arctanh        -> Assignment FunctionSymmetry 'EmptyCtx
    forall {k} (ctx :: Ctx k) (f :: k -> Type).
    (ctx ~ EmptyCtx) =>
    Assignment f ctx
    Ctx.Empty Assignment FunctionSymmetry 'EmptyCtx
    -> FunctionSymmetry R -> Assignment FunctionSymmetry args
    forall {k} (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k)
           (tp :: k).
    (ctx' ~ (ctx ::> tp)) =>
    Assignment f ctx -> f tp -> Assignment f ctx'
    :> FunctionSymmetry R
    forall {k} (r :: k). FunctionSymmetry r
    OddFunction

        SpecialFunction args
    Pow            -> Assignment FunctionSymmetry 'EmptyCtx
    forall {k} (ctx :: Ctx k) (f :: k -> Type).
    (ctx ~ EmptyCtx) =>
    Assignment f ctx
    Ctx.Empty Assignment FunctionSymmetry 'EmptyCtx
    -> FunctionSymmetry R
    -> Assignment FunctionSymmetry ('EmptyCtx '::> R)
    forall {k} (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k)
           (tp :: k).
    (ctx' ~ (ctx ::> tp)) =>
    Assignment f ctx -> f tp -> Assignment f ctx'
    :> FunctionSymmetry R
    forall {k} (r :: k). FunctionSymmetry r
    NoSymmetry Assignment FunctionSymmetry ('EmptyCtx '::> R)
    -> FunctionSymmetry R -> Assignment FunctionSymmetry args
    forall {k} (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k)
           (tp :: k).
    (ctx' ~ (ctx ::> tp)) =>
    Assignment f ctx -> f tp -> Assignment f ctx'
    :> FunctionSymmetry R
    forall {k} (r :: k). FunctionSymmetry r
    NoSymmetry
        SpecialFunction args
    Exp            -> Assignment FunctionSymmetry 'EmptyCtx
    forall {k} (ctx :: Ctx k) (f :: k -> Type).
    (ctx ~ EmptyCtx) =>
    Assignment f ctx
    Ctx.Empty Assignment FunctionSymmetry 'EmptyCtx
    -> FunctionSymmetry R -> Assignment FunctionSymmetry args
    forall {k} (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k)
           (tp :: k).
    (ctx' ~ (ctx ::> tp)) =>
    Assignment f ctx -> f tp -> Assignment f ctx'
    :> FunctionSymmetry R
    forall {k} (r :: k). FunctionSymmetry r
    NoSymmetry
        SpecialFunction args
    Log            -> Assignment FunctionSymmetry 'EmptyCtx
    forall {k} (ctx :: Ctx k) (f :: k -> Type).
    (ctx ~ EmptyCtx) =>
    Assignment f ctx
    Ctx.Empty Assignment FunctionSymmetry 'EmptyCtx
    -> FunctionSymmetry R -> Assignment FunctionSymmetry args
    forall {k} (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k)
           (tp :: k).
    (ctx' ~ (ctx ::> tp)) =>
    Assignment f ctx -> f tp -> Assignment f ctx'
    :> FunctionSymmetry R
    forall {k} (r :: k). FunctionSymmetry r
    NoSymmetry
        SpecialFunction args
    Expm1          -> Assignment FunctionSymmetry 'EmptyCtx
    forall {k} (ctx :: Ctx k) (f :: k -> Type).
    (ctx ~ EmptyCtx) =>
    Assignment f ctx
    Ctx.Empty Assignment FunctionSymmetry 'EmptyCtx
    -> FunctionSymmetry R -> Assignment FunctionSymmetry args
    forall {k} (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k)
           (tp :: k).
    (ctx' ~ (ctx ::> tp)) =>
    Assignment f ctx -> f tp -> Assignment f ctx'
    :> FunctionSymmetry R
    forall {k} (r :: k). FunctionSymmetry r
    NoSymmetry
        SpecialFunction args
    Log1p          -> Assignment FunctionSymmetry 'EmptyCtx
    forall {k} (ctx :: Ctx k) (f :: k -> Type).
    (ctx ~ EmptyCtx) =>
    Assignment f ctx
    Ctx.Empty Assignment FunctionSymmetry 'EmptyCtx
    -> FunctionSymmetry R -> Assignment FunctionSymmetry args
    forall {k} (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k)
           (tp :: k).
    (ctx' ~ (ctx ::> tp)) =>
    Assignment f ctx -> f tp -> Assignment f ctx'
    :> FunctionSymmetry R
    forall {k} (r :: k). FunctionSymmetry r
    NoSymmetry
        SpecialFunction args
    Exp2           -> Assignment FunctionSymmetry 'EmptyCtx
    forall {k} (ctx :: Ctx k) (f :: k -> Type).
    (ctx ~ EmptyCtx) =>
    Assignment f ctx
    Ctx.Empty Assignment FunctionSymmetry 'EmptyCtx
    -> FunctionSymmetry R -> Assignment FunctionSymmetry args
    forall {k} (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k)
           (tp :: k).
    (ctx' ~ (ctx ::> tp)) =>
    Assignment f ctx -> f tp -> Assignment f ctx'
    :> FunctionSymmetry R
    forall {k} (r :: k). FunctionSymmetry r
    NoSymmetry
        SpecialFunction args
    Log2           -> Assignment FunctionSymmetry 'EmptyCtx
    forall {k} (ctx :: Ctx k) (f :: k -> Type).
    (ctx ~ EmptyCtx) =>
    Assignment f ctx
    Ctx.Empty Assignment FunctionSymmetry 'EmptyCtx
    -> FunctionSymmetry R -> Assignment FunctionSymmetry args
    forall {k} (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k)
           (tp :: k).
    (ctx' ~ (ctx ::> tp)) =>
    Assignment f ctx -> f tp -> Assignment f ctx'
    :> FunctionSymmetry R
    forall {k} (r :: k). FunctionSymmetry r
    NoSymmetry
        SpecialFunction args
    Exp10          -> Assignment FunctionSymmetry 'EmptyCtx
    forall {k} (ctx :: Ctx k) (f :: k -> Type).
    (ctx ~ EmptyCtx) =>
    Assignment f ctx
    Ctx.Empty Assignment FunctionSymmetry 'EmptyCtx
    -> FunctionSymmetry R -> Assignment FunctionSymmetry args
    forall {k} (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k)
           (tp :: k).
    (ctx' ~ (ctx ::> tp)) =>
    Assignment f ctx -> f tp -> Assignment f ctx'
    :> FunctionSymmetry R
    forall {k} (r :: k). FunctionSymmetry r
    NoSymmetry
        SpecialFunction args
    Log10          -> Assignment FunctionSymmetry 'EmptyCtx
    forall {k} (ctx :: Ctx k) (f :: k -> Type).
    (ctx ~ EmptyCtx) =>
    Assignment f ctx
    Ctx.Empty Assignment FunctionSymmetry 'EmptyCtx
    -> FunctionSymmetry R -> Assignment FunctionSymmetry args
    forall {k} (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k)
           (tp :: k).
    (ctx' ~ (ctx ::> tp)) =>
    Assignment f ctx -> f tp -> Assignment f ctx'
    :> FunctionSymmetry R
    forall {k} (r :: k). FunctionSymmetry r
    NoSymmetry

        SpecialFunction args
    Hypot          -> Assignment FunctionSymmetry 'EmptyCtx
    forall {k} (ctx :: Ctx k) (f :: k -> Type).
    (ctx ~ EmptyCtx) =>
    Assignment f ctx
    Ctx.Empty Assignment FunctionSymmetry 'EmptyCtx
    -> FunctionSymmetry R
    -> Assignment FunctionSymmetry ('EmptyCtx '::> R)
    forall {k} (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k)
           (tp :: k).
    (ctx' ~ (ctx ::> tp)) =>
    Assignment f ctx -> f tp -> Assignment f ctx'
    :> FunctionSymmetry R
    forall {k} (r :: k). FunctionSymmetry r
    EvenFunction Assignment FunctionSymmetry ('EmptyCtx '::> R)
    -> FunctionSymmetry R -> Assignment FunctionSymmetry args
    forall {k} (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k)
           (tp :: k).
    (ctx' ~ (ctx ::> tp)) =>
    Assignment f ctx -> f tp -> Assignment f ctx'
    :> FunctionSymmetry R
    forall {k} (r :: k). FunctionSymmetry r
    EvenFunction
        SpecialFunction args
    Arctan2        -> Assignment FunctionSymmetry 'EmptyCtx
    forall {k} (ctx :: Ctx k) (f :: k -> Type).
    (ctx ~ EmptyCtx) =>
    Assignment f ctx
    Ctx.Empty Assignment FunctionSymmetry 'EmptyCtx
    -> FunctionSymmetry R
    -> Assignment FunctionSymmetry ('EmptyCtx '::> R)
    forall {k} (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k)
           (tp :: k).
    (ctx' ~ (ctx ::> tp)) =>
    Assignment f ctx -> f tp -> Assignment f ctx'
    :> FunctionSymmetry R
    forall {k} (r :: k). FunctionSymmetry r
    OddFunction Assignment FunctionSymmetry ('EmptyCtx '::> R)
    -> FunctionSymmetry R -> Assignment FunctionSymmetry args
    forall {k} (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k)
           (tp :: k).
    (ctx' ~ (ctx ::> tp)) =>
    Assignment f ctx -> f tp -> Assignment f ctx'
    :> FunctionSymmetry R
    forall {k} (r :: k). FunctionSymmetry r
    NoSymmetry

    -- | Compute the range of values that may be returned by the given special function
    --   as its arguments take on the possible values of its domain.  This may include
    --   limiting values if the function's domain includes infinities; for example
    --   @exp(-inf) = 0@.
    specialFnRange :: SpecialFunction args -> RealInterval R
    specialFnRange :: forall (args :: Ctx Type). SpecialFunction args -> RealInterval R
    specialFnRange SpecialFunction args
    fn = case SpecialFunction args
    fn of
        SpecialFunction args
    Pi             -> SpecialFunction 'EmptyCtx -> RealInterval R
    RealPoint SpecialFunction 'EmptyCtx
    Pi
        SpecialFunction args
    HalfPi         -> SpecialFunction 'EmptyCtx -> RealInterval R
    RealPoint SpecialFunction 'EmptyCtx
    HalfPi
        SpecialFunction args
    QuarterPi      -> SpecialFunction 'EmptyCtx -> RealInterval R
    RealPoint SpecialFunction 'EmptyCtx
    QuarterPi
        SpecialFunction args
    OneOverPi      -> SpecialFunction 'EmptyCtx -> RealInterval R
    RealPoint SpecialFunction 'EmptyCtx
    OneOverPi
        SpecialFunction args
    TwoOverPi      -> SpecialFunction 'EmptyCtx -> RealInterval R
    RealPoint SpecialFunction 'EmptyCtx
    TwoOverPi
        SpecialFunction args
    TwoOverSqrt_Pi -> SpecialFunction 'EmptyCtx -> RealInterval R
    RealPoint SpecialFunction 'EmptyCtx
    TwoOverSqrt_Pi
        SpecialFunction args
    Sqrt_2         -> SpecialFunction 'EmptyCtx -> RealInterval R
    RealPoint SpecialFunction 'EmptyCtx
    Sqrt_2
        SpecialFunction args
    Sqrt_OneHalf   -> SpecialFunction 'EmptyCtx -> RealInterval R
    RealPoint SpecialFunction 'EmptyCtx
    Sqrt_OneHalf
        SpecialFunction args
    E              -> SpecialFunction 'EmptyCtx -> RealInterval R
    RealPoint SpecialFunction 'EmptyCtx
    E
        SpecialFunction args
    Log2_E         -> SpecialFunction 'EmptyCtx -> RealInterval R
    RealPoint SpecialFunction 'EmptyCtx
    Log2_E
        SpecialFunction args
    Log10_E        -> SpecialFunction 'EmptyCtx -> RealInterval R
    RealPoint SpecialFunction 'EmptyCtx
    Log10_E
        SpecialFunction args
    Ln_2           -> SpecialFunction 'EmptyCtx -> RealInterval R
    RealPoint SpecialFunction 'EmptyCtx
    Ln_2
        SpecialFunction args
    Ln_10          -> SpecialFunction 'EmptyCtx -> RealInterval R
    RealPoint SpecialFunction 'EmptyCtx
    Ln_10

        SpecialFunction args
    Sin            -> RealBound -> RealBound -> RealInterval R
    RealInterval (RealPoint -> RealBound
    Incl RealPoint
    NegOne) (RealPoint -> RealBound
    Incl RealPoint
    PosOne)
        SpecialFunction args
    Cos            -> RealBound -> RealBound -> RealInterval R
    RealInterval (RealPoint -> RealBound
    Incl RealPoint
    NegOne) (RealPoint -> RealBound
    Incl RealPoint
    PosOne)
        SpecialFunction args
    Tan            -> RealBound -> RealBound -> RealInterval R
    RealInterval (RealPoint -> RealBound
    Incl RealPoint
    NegInf) (RealPoint -> RealBound
    Incl RealPoint
    PosInf)

        SpecialFunction args
    Arcsin         -> RealBound -> RealBound -> RealInterval R
    RealInterval (RealPoint -> RealBound
    Incl RealPoint
    NegHalfPi) (RealPoint -> RealBound
    Incl RealPoint
    PosHalfPi)
        SpecialFunction args
    Arccos         -> RealBound -> RealBound -> RealInterval R
    RealInterval (RealPoint -> RealBound
    Incl RealPoint
    Zero)      (RealPoint -> RealBound
    Incl RealPoint
    PosPi)
        SpecialFunction args
    Arctan         -> RealBound -> RealBound -> RealInterval R
    RealInterval (RealPoint -> RealBound
    Incl RealPoint
    NegHalfPi) (RealPoint -> RealBound
    Incl RealPoint
    PosHalfPi)

        SpecialFunction args
    Sinh           -> RealBound -> RealBound -> RealInterval R
    RealInterval (RealPoint -> RealBound
    Incl RealPoint
    NegInf) (RealPoint -> RealBound
    Incl RealPoint
    PosInf)
        SpecialFunction args
    Cosh           -> RealBound -> RealBound -> RealInterval R
    RealInterval (RealPoint -> RealBound
    Incl RealPoint
    PosOne) (RealPoint -> RealBound
    Incl RealPoint
    PosInf)
        SpecialFunction args
    Tanh           -> RealBound -> RealBound -> RealInterval R
    RealInterval (RealPoint -> RealBound
    Incl RealPoint
    NegOne) (RealPoint -> RealBound
    Incl RealPoint
    PosOne)
        SpecialFunction args
    Arcsinh        -> RealBound -> RealBound -> RealInterval R
    RealInterval (RealPoint -> RealBound
    Incl RealPoint
    NegInf) (RealPoint -> RealBound
    Incl RealPoint
    PosInf)
        SpecialFunction args
    Arccosh        -> RealBound -> RealBound -> RealInterval R
    RealInterval (RealPoint -> RealBound
    Incl RealPoint
    Zero)   (RealPoint -> RealBound
    Incl RealPoint
    PosInf)
        SpecialFunction args
    Arctanh        -> RealBound -> RealBound -> RealInterval R
    RealInterval (RealPoint -> RealBound
    Incl RealPoint
    NegInf) (RealPoint -> RealBound
    Incl RealPoint
    PosInf)

        SpecialFunction args
    Pow            -> RealBound -> RealBound -> RealInterval R
    RealInterval (RealPoint -> RealBound
    Incl RealPoint
    NegInf) (RealPoint -> RealBound
    Incl RealPoint
    PosInf)
        SpecialFunction args
    Exp            -> RealBound -> RealBound -> RealInterval R
    RealInterval (RealPoint -> RealBound
    Incl RealPoint
    Zero)   (RealPoint -> RealBound
    Incl RealPoint
    PosInf)
        SpecialFunction args
    Log            -> RealBound -> RealBound -> RealInterval R
    RealInterval (RealPoint -> RealBound
    Incl RealPoint
    NegInf) (RealPoint -> RealBound
    Incl RealPoint
    PosInf)
        SpecialFunction args
    Expm1          -> RealBound -> RealBound -> RealInterval R
    RealInterval (RealPoint -> RealBound
    Incl RealPoint
    NegOne) (RealPoint -> RealBound
    Incl RealPoint
    PosInf)
        SpecialFunction args
    Log1p          -> RealBound -> RealBound -> RealInterval R
    RealInterval (RealPoint -> RealBound
    Incl RealPoint
    NegInf) (RealPoint -> RealBound
    Incl RealPoint
    PosInf)
        SpecialFunction args
    Exp2           -> RealBound -> RealBound -> RealInterval R
    RealInterval (RealPoint -> RealBound
    Incl RealPoint
    Zero)   (RealPoint -> RealBound
    Incl RealPoint
    PosInf)
        SpecialFunction args
    Log2           -> RealBound -> RealBound -> RealInterval R
    RealInterval (RealPoint -> RealBound
    Incl RealPoint
    NegInf) (RealPoint -> RealBound
    Incl RealPoint
    PosInf)
        SpecialFunction args
    Exp10          -> RealBound -> RealBound -> RealInterval R
    RealInterval (RealPoint -> RealBound
    Incl RealPoint
    Zero)   (RealPoint -> RealBound
    Incl RealPoint
    PosInf)
        SpecialFunction args
    Log10          -> RealBound -> RealBound -> RealInterval R
    RealInterval (RealPoint -> RealBound
    Incl RealPoint
    NegInf) (RealPoint -> RealBound
    Incl RealPoint
    PosInf)

        SpecialFunction args
    Hypot          -> RealBound -> RealBound -> RealInterval R
    RealInterval (RealPoint -> RealBound
    Incl RealPoint
    Zero) (RealPoint -> RealBound
    Incl RealPoint
    PosInf)
        SpecialFunction args
    Arctan2        -> RealBound -> RealBound -> RealInterval R
    RealInterval (RealPoint -> RealBound
    Incl RealPoint
    NegPi) (RealPoint -> RealBound
    Incl RealPoint
    PosPi)

    -- | Compute the domain of the given special function.  As a mathematical
    --   entity, the value of the given function is not well-defined outside
    --   its domain. In floating-point terms, a special function will return
    --   a @NaN@ when evaluated on arguments outside its domain.
    specialFnDomain :: SpecialFunction args -> Ctx.Assignment RealInterval args
    specialFnDomain :: forall (args :: Ctx Type).
    SpecialFunction args -> Assignment RealInterval args
    specialFnDomain SpecialFunction args
    fn = case SpecialFunction args
    fn of
        SpecialFunction args
    Pi             -> Assignment RealInterval args
    forall {k} (ctx :: Ctx k) (f :: k -> Type).
    (ctx ~ EmptyCtx) =>
    Assignment f ctx
    Ctx.Empty
        SpecialFunction args
    HalfPi         -> Assignment RealInterval args
    forall {k} (ctx :: Ctx k) (f :: k -> Type).
    (ctx ~ EmptyCtx) =>
    Assignment f ctx
    Ctx.Empty
        SpecialFunction args
    QuarterPi      -> Assignment RealInterval args
    forall {k} (ctx :: Ctx k) (f :: k -> Type).
    (ctx ~ EmptyCtx) =>
    Assignment f ctx
    Ctx.Empty
        SpecialFunction args
    OneOverPi      -> Assignment RealInterval args
    forall {k} (ctx :: Ctx k) (f :: k -> Type).
    (ctx ~ EmptyCtx) =>
    Assignment f ctx
    Ctx.Empty
        SpecialFunction args
    TwoOverPi      -> Assignment RealInterval args
    forall {k} (ctx :: Ctx k) (f :: k -> Type).
    (ctx ~ EmptyCtx) =>
    Assignment f ctx
    Ctx.Empty
        SpecialFunction args
    TwoOverSqrt_Pi -> Assignment RealInterval args
    forall {k} (ctx :: Ctx k) (f :: k -> Type).
    (ctx ~ EmptyCtx) =>
    Assignment f ctx
    Ctx.Empty
        SpecialFunction args
    Sqrt_2         -> Assignment RealInterval args
    forall {k} (ctx :: Ctx k) (f :: k -> Type).
    (ctx ~ EmptyCtx) =>
    Assignment f ctx
    Ctx.Empty
        SpecialFunction args
    Sqrt_OneHalf   -> Assignment RealInterval args
    forall {k} (ctx :: Ctx k) (f :: k -> Type).
    (ctx ~ EmptyCtx) =>
    Assignment f ctx
    Ctx.Empty
        SpecialFunction args
    E              -> Assignment RealInterval args
    forall {k} (ctx :: Ctx k) (f :: k -> Type).
    (ctx ~ EmptyCtx) =>
    Assignment f ctx
    Ctx.Empty
        SpecialFunction args
    Log2_E         -> Assignment RealInterval args
    forall {k} (ctx :: Ctx k) (f :: k -> Type).
    (ctx ~ EmptyCtx) =>
    Assignment f ctx
    Ctx.Empty
        SpecialFunction args
    Log10_E        -> Assignment RealInterval args
    forall {k} (ctx :: Ctx k) (f :: k -> Type).
    (ctx ~ EmptyCtx) =>
    Assignment f ctx
    Ctx.Empty
        SpecialFunction args
    Ln_2           -> Assignment RealInterval args
    forall {k} (ctx :: Ctx k) (f :: k -> Type).
    (ctx ~ EmptyCtx) =>
    Assignment f ctx
    Ctx.Empty
        SpecialFunction args
    Ln_10          -> Assignment RealInterval args
    forall {k} (ctx :: Ctx k) (f :: k -> Type).
    (ctx ~ EmptyCtx) =>
    Assignment f ctx
    Ctx.Empty

        SpecialFunction args
    Sin            -> Assignment RealInterval 'EmptyCtx
    forall {k} (ctx :: Ctx k) (f :: k -> Type).
    (ctx ~ EmptyCtx) =>
    Assignment f ctx
    Ctx.Empty Assignment RealInterval 'EmptyCtx
    -> RealInterval R -> Assignment RealInterval args
    forall {k} (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k)
           (tp :: k).
    (ctx' ~ (ctx ::> tp)) =>
    Assignment f ctx -> f tp -> Assignment f ctx'
    :> RealBound -> RealBound -> RealInterval R
    RealInterval (RealPoint -> RealBound
    Excl RealPoint
    NegInf) (RealPoint -> RealBound
    Excl RealPoint
    PosInf)
        SpecialFunction args
    Cos            -> Assignment RealInterval 'EmptyCtx
    forall {k} (ctx :: Ctx k) (f :: k -> Type).
    (ctx ~ EmptyCtx) =>
    Assignment f ctx
    Ctx.Empty Assignment RealInterval 'EmptyCtx
    -> RealInterval R -> Assignment RealInterval args
    forall {k} (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k)
           (tp :: k).
    (ctx' ~ (ctx ::> tp)) =>
    Assignment f ctx -> f tp -> Assignment f ctx'
    :> RealBound -> RealBound -> RealInterval R
    RealInterval (RealPoint -> RealBound
    Excl RealPoint
    NegInf) (RealPoint -> RealBound
    Excl RealPoint
    PosInf)
        SpecialFunction args
    Tan            -> Assignment RealInterval 'EmptyCtx
    forall {k} (ctx :: Ctx k) (f :: k -> Type).
    (ctx ~ EmptyCtx) =>
    Assignment f ctx
    Ctx.Empty Assignment RealInterval 'EmptyCtx
    -> RealInterval R -> Assignment RealInterval args
    forall {k} (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k)
           (tp :: k).
    (ctx' ~ (ctx ::> tp)) =>
    Assignment f ctx -> f tp -> Assignment f ctx'
    :> RealBound -> RealBound -> RealInterval R
    RealInterval (RealPoint -> RealBound
    Excl RealPoint
    NegInf) (RealPoint -> RealBound
    Excl RealPoint
    PosInf)
        SpecialFunction args
    Arcsin         -> Assignment RealInterval 'EmptyCtx
    forall {k} (ctx :: Ctx k) (f :: k -> Type).
    (ctx ~ EmptyCtx) =>
    Assignment f ctx
    Ctx.Empty Assignment RealInterval 'EmptyCtx
    -> RealInterval R -> Assignment RealInterval args
    forall {k} (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k)
           (tp :: k).
    (ctx' ~ (ctx ::> tp)) =>
    Assignment f ctx -> f tp -> Assignment f ctx'
    :> RealBound -> RealBound -> RealInterval R
    RealInterval (RealPoint -> RealBound
    Incl RealPoint
    NegOne) (RealPoint -> RealBound
    Incl RealPoint
    PosOne)
        SpecialFunction args
    Arccos         -> Assignment RealInterval 'EmptyCtx
    forall {k} (ctx :: Ctx k) (f :: k -> Type).
    (ctx ~ EmptyCtx) =>
    Assignment f ctx
    Ctx.Empty Assignment RealInterval 'EmptyCtx
    -> RealInterval R -> Assignment RealInterval args
    forall {k} (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k)
           (tp :: k).
    (ctx' ~ (ctx ::> tp)) =>
    Assignment f ctx -> f tp -> Assignment f ctx'
    :> RealBound -> RealBound -> RealInterval R
    RealInterval (RealPoint -> RealBound
    Incl RealPoint
    NegOne) (RealPoint -> RealBound
    Incl RealPoint
    PosOne)
        SpecialFunction args
    Arctan         -> Assignment RealInterval 'EmptyCtx
    forall {k} (ctx :: Ctx k) (f :: k -> Type).
    (ctx ~ EmptyCtx) =>
    Assignment f ctx
    Ctx.Empty Assignment RealInterval 'EmptyCtx
    -> RealInterval R -> Assignment RealInterval args
    forall {k} (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k)
           (tp :: k).
    (ctx' ~ (ctx ::> tp)) =>
    Assignment f ctx -> f tp -> Assignment f ctx'
    :> RealBound -> RealBound -> RealInterval R
    RealInterval (RealPoint -> RealBound
    Incl RealPoint
    NegInf) (RealPoint -> RealBound
    Incl RealPoint
    PosInf)

        SpecialFunction args
    Sinh           -> Assignment RealInterval 'EmptyCtx
    forall {k} (ctx :: Ctx k) (f :: k -> Type).
    (ctx ~ EmptyCtx) =>
    Assignment f ctx
    Ctx.Empty Assignment RealInterval 'EmptyCtx
    -> RealInterval R -> Assignment RealInterval args
    forall {k} (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k)
           (tp :: k).
    (ctx' ~ (ctx ::> tp)) =>
    Assignment f ctx -> f tp -> Assignment f ctx'
    :> RealBound -> RealBound -> RealInterval R
    RealInterval (RealPoint -> RealBound
    Incl RealPoint
    NegInf) (RealPoint -> RealBound
    Incl RealPoint
    PosInf)
        SpecialFunction args
    Cosh           -> Assignment RealInterval 'EmptyCtx
    forall {k} (ctx :: Ctx k) (f :: k -> Type).
    (ctx ~ EmptyCtx) =>
    Assignment f ctx
    Ctx.Empty Assignment RealInterval 'EmptyCtx
    -> RealInterval R -> Assignment RealInterval args
    forall {k} (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k)
           (tp :: k).
    (ctx' ~ (ctx ::> tp)) =>
    Assignment f ctx -> f tp -> Assignment f ctx'
    :> RealBound -> RealBound -> RealInterval R
    RealInterval (RealPoint -> RealBound
    Incl RealPoint
    NegInf) (RealPoint -> RealBound
    Incl RealPoint
    PosInf)
        SpecialFunction args
    Tanh           -> Assignment RealInterval 'EmptyCtx
    forall {k} (ctx :: Ctx k) (f :: k -> Type).
    (ctx ~ EmptyCtx) =>
    Assignment f ctx
    Ctx.Empty Assignment RealInterval 'EmptyCtx
    -> RealInterval R -> Assignment RealInterval args
    forall {k} (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k)
           (tp :: k).
    (ctx' ~ (ctx ::> tp)) =>
    Assignment f ctx -> f tp -> Assignment f ctx'
    :> RealBound -> RealBound -> RealInterval R
    RealInterval (RealPoint -> RealBound
    Incl RealPoint
    NegInf) (RealPoint -> RealBound
    Incl RealPoint
    PosInf)
        SpecialFunction args
    Arcsinh        -> Assignment RealInterval 'EmptyCtx
    forall {k} (ctx :: Ctx k) (f :: k -> Type).
    (ctx ~ EmptyCtx) =>
    Assignment f ctx
    Ctx.Empty Assignment RealInterval 'EmptyCtx
    -> RealInterval R -> Assignment RealInterval args
    forall {k} (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k)
           (tp :: k).
    (ctx' ~ (ctx ::> tp)) =>
    Assignment f ctx -> f tp -> Assignment f ctx'
    :> RealBound -> RealBound -> RealInterval R
    RealInterval (RealPoint -> RealBound
    Incl RealPoint
    NegInf) (RealPoint -> RealBound
    Incl RealPoint
    PosInf)
        SpecialFunction args
    Arccosh        -> Assignment RealInterval 'EmptyCtx
    forall {k} (ctx :: Ctx k) (f :: k -> Type).
    (ctx ~ EmptyCtx) =>
    Assignment f ctx
    Ctx.Empty Assignment RealInterval 'EmptyCtx
    -> RealInterval R -> Assignment RealInterval args
    forall {k} (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k)
           (tp :: k).
    (ctx' ~ (ctx ::> tp)) =>
    Assignment f ctx -> f tp -> Assignment f ctx'
    :> RealBound -> RealBound -> RealInterval R
    RealInterval (RealPoint -> RealBound
    Incl RealPoint
    PosOne) (RealPoint -> RealBound
    Incl RealPoint
    PosInf)
        SpecialFunction args
    Arctanh        -> Assignment RealInterval 'EmptyCtx
    forall {k} (ctx :: Ctx k) (f :: k -> Type).
    (ctx ~ EmptyCtx) =>
    Assignment f ctx
    Ctx.Empty Assignment RealInterval 'EmptyCtx
    -> RealInterval R -> Assignment RealInterval args
    forall {k} (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k)
           (tp :: k).
    (ctx' ~ (ctx ::> tp)) =>
    Assignment f ctx -> f tp -> Assignment f ctx'
    :> RealBound -> RealBound -> RealInterval R
    RealInterval (RealPoint -> RealBound
    Incl RealPoint
    NegOne) (RealPoint -> RealBound
    Incl RealPoint
    PosOne)

        SpecialFunction args
    Pow            -> Assignment RealInterval 'EmptyCtx
    forall {k} (ctx :: Ctx k) (f :: k -> Type).
    (ctx ~ EmptyCtx) =>
    Assignment f ctx
    Ctx.Empty Assignment RealInterval 'EmptyCtx
    -> RealInterval R -> Assignment RealInterval ('EmptyCtx '::> R)
    forall {k} (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k)
           (tp :: k).
    (ctx' ~ (ctx ::> tp)) =>
    Assignment f ctx -> f tp -> Assignment f ctx'
    :> RealBound -> RealBound -> RealInterval R
    RealInterval (RealPoint -> RealBound
    Incl RealPoint
    NegInf) (RealPoint -> RealBound
    Incl RealPoint
    PosInf)
                                    Assignment RealInterval ('EmptyCtx '::> R)
    -> RealInterval R -> Assignment RealInterval args
    forall {k} (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k)
           (tp :: k).
    (ctx' ~ (ctx ::> tp)) =>
    Assignment f ctx -> f tp -> Assignment f ctx'
    :> RealBound -> RealBound -> RealInterval R
    RealInterval (RealPoint -> RealBound
    Incl RealPoint
    NegInf) (RealPoint -> RealBound
    Incl RealPoint
    PosInf)
        SpecialFunction args
    Exp            -> Assignment RealInterval 'EmptyCtx
    forall {k} (ctx :: Ctx k) (f :: k -> Type).
    (ctx ~ EmptyCtx) =>
    Assignment f ctx
    Ctx.Empty Assignment RealInterval 'EmptyCtx
    -> RealInterval R -> Assignment RealInterval args
    forall {k} (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k)
           (tp :: k).
    (ctx' ~ (ctx ::> tp)) =>
    Assignment f ctx -> f tp -> Assignment f ctx'
    :> RealBound -> RealBound -> RealInterval R
    RealInterval (RealPoint -> RealBound
    Incl RealPoint
    NegInf) (RealPoint -> RealBound
    Incl RealPoint
    PosInf)
        SpecialFunction args
    Log            -> Assignment RealInterval 'EmptyCtx
    forall {k} (ctx :: Ctx k) (f :: k -> Type).
    (ctx ~ EmptyCtx) =>
    Assignment f ctx
    Ctx.Empty Assignment RealInterval 'EmptyCtx
    -> RealInterval R -> Assignment RealInterval args
    forall {k} (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k)
           (tp :: k).
    (ctx' ~ (ctx ::> tp)) =>
    Assignment f ctx -> f tp -> Assignment f ctx'
    :> RealBound -> RealBound -> RealInterval R
    RealInterval (RealPoint -> RealBound
    Incl RealPoint
    Zero)   (RealPoint -> RealBound
    Incl RealPoint
    PosInf)
        SpecialFunction args
    Expm1          -> Assignment RealInterval 'EmptyCtx
    forall {k} (ctx :: Ctx k) (f :: k -> Type).
    (ctx ~ EmptyCtx) =>
    Assignment f ctx
    Ctx.Empty Assignment RealInterval 'EmptyCtx
    -> RealInterval R -> Assignment RealInterval args
    forall {k} (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k)
           (tp :: k).
    (ctx' ~ (ctx ::> tp)) =>
    Assignment f ctx -> f tp -> Assignment f ctx'
    :> RealBound -> RealBound -> RealInterval R
    RealInterval (RealPoint -> RealBound
    Incl RealPoint
    NegInf) (RealPoint -> RealBound
    Incl RealPoint
    PosInf)
        SpecialFunction args
    Log1p          -> Assignment RealInterval 'EmptyCtx
    forall {k} (ctx :: Ctx k) (f :: k -> Type).
    (ctx ~ EmptyCtx) =>
    Assignment f ctx
    Ctx.Empty Assignment RealInterval 'EmptyCtx
    -> RealInterval R -> Assignment RealInterval args
    forall {k} (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k)
           (tp :: k).
    (ctx' ~ (ctx ::> tp)) =>
    Assignment f ctx -> f tp -> Assignment f ctx'
    :> RealBound -> RealBound -> RealInterval R
    RealInterval (RealPoint -> RealBound
    Incl RealPoint
    NegOne) (RealPoint -> RealBound
    Incl RealPoint
    PosInf)
        SpecialFunction args
    Exp2           -> Assignment RealInterval 'EmptyCtx
    forall {k} (ctx :: Ctx k) (f :: k -> Type).
    (ctx ~ EmptyCtx) =>
    Assignment f ctx
    Ctx.Empty Assignment RealInterval 'EmptyCtx
    -> RealInterval R -> Assignment RealInterval args
    forall {k} (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k)
           (tp :: k).
    (ctx' ~ (ctx ::> tp)) =>
    Assignment f ctx -> f tp -> Assignment f ctx'
    :> RealBound -> RealBound -> RealInterval R
    RealInterval (RealPoint -> RealBound
    Incl RealPoint
    NegInf) (RealPoint -> RealBound
    Incl RealPoint
    PosInf)
        SpecialFunction args
    Log2           -> Assignment RealInterval 'EmptyCtx
    forall {k} (ctx :: Ctx k) (f :: k -> Type).
    (ctx ~ EmptyCtx) =>
    Assignment f ctx
    Ctx.Empty Assignment RealInterval 'EmptyCtx
    -> RealInterval R -> Assignment RealInterval args
    forall {k} (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k)
           (tp :: k).
    (ctx' ~ (ctx ::> tp)) =>
    Assignment f ctx -> f tp -> Assignment f ctx'
    :> RealBound -> RealBound -> RealInterval R
    RealInterval (RealPoint -> RealBound
    Incl RealPoint
    Zero)   (RealPoint -> RealBound
    Incl RealPoint
    PosInf)
        SpecialFunction args
    Exp10          -> Assignment RealInterval 'EmptyCtx
    forall {k} (ctx :: Ctx k) (f :: k -> Type).
    (ctx ~ EmptyCtx) =>
    Assignment f ctx
    Ctx.Empty Assignment RealInterval 'EmptyCtx
    -> RealInterval R -> Assignment RealInterval args
    forall {k} (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k)
           (tp :: k).
    (ctx' ~ (ctx ::> tp)) =>
    Assignment f ctx -> f tp -> Assignment f ctx'
    :> RealBound -> RealBound -> RealInterval R
    RealInterval (RealPoint -> RealBound
    Incl RealPoint
    NegInf) (RealPoint -> RealBound
    Incl RealPoint
    PosInf)
        SpecialFunction args
    Log10          -> Assignment RealInterval 'EmptyCtx
    forall {k} (ctx :: Ctx k) (f :: k -> Type).
    (ctx ~ EmptyCtx) =>
    Assignment f ctx
    Ctx.Empty Assignment RealInterval 'EmptyCtx
    -> RealInterval R -> Assignment RealInterval args
    forall {k} (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k)
           (tp :: k).
    (ctx' ~ (ctx ::> tp)) =>
    Assignment f ctx -> f tp -> Assignment f ctx'
    :> RealBound -> RealBound -> RealInterval R
    RealInterval (RealPoint -> RealBound
    Incl RealPoint
    Zero)   (RealPoint -> RealBound
    Incl RealPoint
    PosInf)

        SpecialFunction args
    Hypot          -> Assignment RealInterval 'EmptyCtx
    forall {k} (ctx :: Ctx k) (f :: k -> Type).
    (ctx ~ EmptyCtx) =>
    Assignment f ctx
    Ctx.Empty Assignment RealInterval 'EmptyCtx
    -> RealInterval R -> Assignment RealInterval ('EmptyCtx '::> R)
    forall {k} (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k)
           (tp :: k).
    (ctx' ~ (ctx ::> tp)) =>
    Assignment f ctx -> f tp -> Assignment f ctx'
    :> RealBound -> RealBound -> RealInterval R
    RealInterval (RealPoint -> RealBound
    Incl RealPoint
    NegInf) (RealPoint -> RealBound
    Incl RealPoint
    PosInf)
                                    Assignment RealInterval ('EmptyCtx '::> R)
    -> RealInterval R -> Assignment RealInterval args
    forall {k} (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k)
           (tp :: k).
    (ctx' ~ (ctx ::> tp)) =>
    Assignment f ctx -> f tp -> Assignment f ctx'
    :> RealBound -> RealBound -> RealInterval R
    RealInterval (RealPoint -> RealBound
    Incl RealPoint
    NegInf) (RealPoint -> RealBound
    Incl RealPoint
    PosInf)
        SpecialFunction args
    Arctan2        -> Assignment RealInterval 'EmptyCtx
    forall {k} (ctx :: Ctx k) (f :: k -> Type).
    (ctx ~ EmptyCtx) =>
    Assignment f ctx
    Ctx.Empty Assignment RealInterval 'EmptyCtx
    -> RealInterval R -> Assignment RealInterval ('EmptyCtx '::> R)
    forall {k} (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k)
           (tp :: k).
    (ctx' ~ (ctx ::> tp)) =>
    Assignment f ctx -> f tp -> Assignment f ctx'
    :> RealBound -> RealBound -> RealInterval R
    RealInterval (RealPoint -> RealBound
    Incl RealPoint
    NegInf) (RealPoint -> RealBound
    Incl RealPoint
    PosInf)
                                    Assignment RealInterval ('EmptyCtx '::> R)
    -> RealInterval R -> Assignment RealInterval args
    forall {k} (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k)
           (tp :: k).
    (ctx' ~ (ctx ::> tp)) =>
    Assignment f ctx -> f tp -> Assignment f ctx'
    :> RealBound -> RealBound -> RealInterval R
    RealInterval (RealPoint -> RealBound
    Incl RealPoint
    NegInf) (RealPoint -> RealBound
    Incl RealPoint
    PosInf)

    -- | Data type for wrapping the actual arguments to special functions.
    data SpecialFnArg (e :: k -> Type) (tp::k) (r::Type) where
      SpecialFnArg :: e tp -> SpecialFnArg e tp R

    -- | Data type for wrapping a collction of actual arguments to special functions.
    newtype SpecialFnArgs (e :: k -> Type) (tp :: k) args =
      SpecialFnArgs (Ctx.Assignment (SpecialFnArg e tp) args)

    $(return [])

    instance HashableF SpecialFunction where
      hashWithSaltF :: forall (tp :: Ctx Type). Int -> SpecialFunction tp -> Int
    hashWithSaltF = $(structuralHashWithSalt [t|SpecialFunction|] [])

    instance Hashable (SpecialFunction args) where
      hashWithSalt :: Int -> SpecialFunction args -> Int
    hashWithSalt = Int -> SpecialFunction args -> Int
    forall k (f :: k -> Type) (tp :: k).
    HashableF f =>
    Int -> f tp -> Int
    forall (tp :: Ctx Type). Int -> SpecialFunction tp -> Int
    hashWithSaltF

    instance TestEquality SpecialFunction where
      testEquality :: forall (a :: Ctx Type) (b :: Ctx Type).
    SpecialFunction a -> SpecialFunction b -> Maybe (a :~: b)
    testEquality = $(structuralTypeEquality [t|SpecialFunction|] [])

    instance Eq (SpecialFunction args) where
      SpecialFunction args
    x == :: SpecialFunction args -> SpecialFunction args -> Bool
    == SpecialFunction args
    y = Maybe (args :~: args) -> Bool
    forall a. Maybe a -> Bool
    isJust (SpecialFunction args
    -> SpecialFunction args -> Maybe (args :~: args)
    forall {k} (f :: k -> Type) (a :: k) (b :: k).
    TestEquality f =>
    f a -> f b -> Maybe (a :~: b)
    forall (a :: Ctx Type) (b :: Ctx Type).
    SpecialFunction a -> SpecialFunction b -> Maybe (a :~: b)
    testEquality SpecialFunction args
    x SpecialFunction args
    y)

    instance OrdF SpecialFunction where
      compareF :: forall (x :: Ctx Type) (y :: Ctx Type).
    SpecialFunction x -> SpecialFunction y -> OrderingF x y
    compareF = $(structuralTypeOrd [t|SpecialFunction|] [])

    instance OrdF e => TestEquality (SpecialFnArg e tp) where
      testEquality :: forall a b.
    SpecialFnArg e tp a -> SpecialFnArg e tp b -> Maybe (a :~: b)
    testEquality (SpecialFnArg e tp
    x) (SpecialFnArg e tp
    y) =
        do tp :~: tp
    Refl <- e tp -> e tp -> Maybe (tp :~: tp)
    forall (a :: k) (b :: k). e a -> e b -> Maybe (a :~: b)
    forall {k} (f :: k -> Type) (a :: k) (b :: k).
    TestEquality f =>
    f a -> f b -> Maybe (a :~: b)
    testEquality e tp
    x e tp
    y
           (a :~: b) -> Maybe (a :~: b)
    forall a. a -> Maybe a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return a :~: a
    a :~: b
    forall {k} (a :: k). a :~: a
    Refl

    instance OrdF e => OrdF (SpecialFnArg e tp) where
      compareF :: forall x y.
    SpecialFnArg e tp x -> SpecialFnArg e tp y -> OrderingF x y
    compareF (SpecialFnArg e tp
    x) (SpecialFnArg e tp
    y) =
        case e tp -> e tp -> OrderingF tp tp
    forall (x :: k) (y :: k). e x -> e y -> OrderingF x y
    forall k (ktp :: k -> Type) (x :: k) (y :: k).
    OrdF ktp =>
    ktp x -> ktp y -> OrderingF x y
    compareF e tp
    x e tp
    y of
          OrderingF tp tp
    LTF -> OrderingF x y
    forall {k} (x :: k) (y :: k). OrderingF x y
    LTF
          OrderingF tp tp
    EQF -> OrderingF x x
    OrderingF x y
    forall {k} (x :: k). OrderingF x x
    EQF
          OrderingF tp tp
    GTF -> OrderingF x y
    forall {k} (x :: k) (y :: k). OrderingF x y
    GTF

    instance HashableF e => HashableF (SpecialFnArg e tp) where
      hashWithSaltF :: forall tp. Int -> SpecialFnArg e tp tp -> Int
    hashWithSaltF Int
    s (SpecialFnArg e tp
    x) = Int -> e tp -> Int
    forall (tp :: k). Int -> e tp -> Int
    forall k (f :: k -> Type) (tp :: k).
    HashableF f =>
    Int -> f tp -> Int
    hashWithSaltF Int
    s e tp
    x

    instance OrdF e => Eq (SpecialFnArgs e tp r) where
      SpecialFnArgs Assignment (SpecialFnArg e tp) r
    xs == :: SpecialFnArgs e tp r -> SpecialFnArgs e tp r -> Bool
    == SpecialFnArgs Assignment (SpecialFnArg e tp) r
    ys = Assignment (SpecialFnArg e tp) r
    xs Assignment (SpecialFnArg e tp) r
    -> Assignment (SpecialFnArg e tp) r -> Bool
    forall a. Eq a => a -> a -> Bool
    == Assignment (SpecialFnArg e tp) r
    ys

    instance OrdF e => Ord (SpecialFnArgs e tp r) where
      compare :: SpecialFnArgs e tp r -> SpecialFnArgs e tp r -> Ordering
    compare (SpecialFnArgs Assignment (SpecialFnArg e tp) r
    xs) (SpecialFnArgs Assignment (SpecialFnArg e tp) r
    ys) = Assignment (SpecialFnArg e tp) r
    -> Assignment (SpecialFnArg e tp) r -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare Assignment (SpecialFnArg e tp) r
    xs Assignment (SpecialFnArg e tp) r
    ys

    instance (HashableF e, OrdF e) => Hashable (SpecialFnArgs e tp args) where
      hashWithSalt :: Int -> SpecialFnArgs e tp args -> Int
    hashWithSalt Int
    s (SpecialFnArgs Assignment (SpecialFnArg e tp) args
    xs) = Int -> Assignment (SpecialFnArg e tp) args -> Int
    forall k (f :: k -> Type) (tp :: k).
    HashableF f =>
    Int -> f tp -> Int
    forall (tp :: Ctx Type).
    Int -> Assignment (SpecialFnArg e tp) tp -> Int
    hashWithSaltF Int
    s Assignment (SpecialFnArg e tp) args
    xs

    traverseSpecialFnArg :: Applicative m =>
      (e tp -> m (f tp)) ->
      SpecialFnArg e tp r -> m (SpecialFnArg f tp r)
    traverseSpecialFnArg :: forall {k} (m :: Type -> Type) (e :: k -> Type) (tp :: k)
           (f :: k -> Type) r.
    Applicative m =>
    (e tp -> m (f tp))
    -> SpecialFnArg e tp r -> m (SpecialFnArg f tp r)
    traverseSpecialFnArg e tp -> m (f tp)
    f (SpecialFnArg e tp
    x) = f tp -> SpecialFnArg f tp r
    f tp -> SpecialFnArg f tp R
    forall {k} (e :: k -> Type) (tp :: k). e tp -> SpecialFnArg e tp R
    SpecialFnArg (f tp -> SpecialFnArg f tp r)
    -> m (f tp) -> m (SpecialFnArg f tp r)
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> e tp -> m (f tp)
    f e tp
    x

    traverseSpecialFnArgs :: Applicative m =>
      (e tp -> m (f tp)) ->
      SpecialFnArgs e tp r -> m (SpecialFnArgs f tp r)
    traverseSpecialFnArgs :: forall {k} (m :: Type -> Type) (e :: k -> Type) (tp :: k)
           (f :: k -> Type) (r :: Ctx Type).
    Applicative m =>
    (e tp -> m (f tp))
    -> SpecialFnArgs e tp r -> m (SpecialFnArgs f tp r)
    traverseSpecialFnArgs e tp -> m (f tp)
    f (SpecialFnArgs Assignment (SpecialFnArg e tp) r
    xs) =
      Assignment (SpecialFnArg f tp) r -> SpecialFnArgs f tp r
    forall k (e :: k -> Type) (tp :: k) (args :: Ctx Type).
    Assignment (SpecialFnArg e tp) args -> SpecialFnArgs e tp args
    SpecialFnArgs (Assignment (SpecialFnArg f tp) r -> SpecialFnArgs f tp r)
    -> m (Assignment (SpecialFnArg f tp) r) -> m (SpecialFnArgs f tp r)
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> (forall x. SpecialFnArg e tp x -> m (SpecialFnArg f tp x))
    -> forall (x :: Ctx Type).
       Assignment (SpecialFnArg e tp) x
       -> m (Assignment (SpecialFnArg f tp) x)
    forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type)
           (g :: k -> Type) (m :: Type -> Type).
    (TraversableFC t, Applicative m) =>
    (forall (x :: k). f x -> m (g x))
    -> forall (x :: l). t f x -> m (t g x)
    forall (f :: Type -> Type) (g :: Type -> Type) (m :: Type -> Type).
    Applicative m =>
    (forall x. f x -> m (g x))
    -> forall (x :: Ctx Type). Assignment f x -> m (Assignment g x)
    traverseFC ((e tp -> m (f tp))
    -> SpecialFnArg e tp x -> m (SpecialFnArg f tp x)
    forall {k} (m :: Type -> Type) (e :: k -> Type) (tp :: k)
           (f :: k -> Type) r.
    Applicative m =>
    (e tp -> m (f tp))
    -> SpecialFnArg e tp r -> m (SpecialFnArg f tp r)
    traverseSpecialFnArg e tp -> m (f tp)
    f) Assignment (SpecialFnArg e tp) r
    xs