    {-# LANGUAGE ExistentialQuantification #-}
    {-# LANGUAGE GADTs                     #-}
    {-# LANGUAGE LambdaCase                #-}
    {-# LANGUAGE RankNTypes                #-}
    {-# LANGUAGE Safe                      #-}
    {-# LANGUAGE ScopedTypeVariables       #-}

    -- | Operators in modular transition systems and their translation.
    module Copilot.Theorem.TransSys.Operators where

    import qualified Copilot.Core as C
    import Copilot.Theorem.TransSys.Cast
    import Copilot.Theorem.TransSys.Type

    import Copilot.Theorem.Misc.Error as Err

    -- | Unary operators.
    data Op1 a where
      Not   :: Op1 Bool
      Neg   :: Op1 a
      Abs   :: Op1 a
      Exp   :: Op1 a
      Sqrt  :: Op1 a
      Log   :: Op1 a
      Sin   :: Op1 a
      Tan   :: Op1 a
      Cos   :: Op1 a
      Asin  :: Op1 a
      Atan  :: Op1 a
      Acos  :: Op1 a
      Sinh  :: Op1 a
      Tanh  :: Op1 a
      Cosh  :: Op1 a
      Asinh :: Op1 a
      Atanh :: Op1 a
      Acosh :: Op1 a

    -- | Binary operators.
    data Op2 a b where
      Eq     :: Op2 a    Bool
      And    :: Op2 Bool Bool
      Or     :: Op2 Bool Bool

      Le     :: (Num a) => Op2 a Bool
      Lt     :: (Num a) => Op2 a Bool
      Ge     :: (Num a) => Op2 a Bool
      Gt     :: (Num a) => Op2 a Bool

      Add    :: (Num a) => Op2 a a
      Sub    :: (Num a) => Op2 a a
      Mul    :: (Num a) => Op2 a a
      Mod    :: (Num a) => Op2 a a
      Fdiv   :: (Num a) => Op2 a a

      Pow    :: (Num a) => Op2 a a

    instance Show (Op1 a) where
      show :: Op1 a -> String
    show Op1 a
    op = case Op1 a
    op of
        Op1 a
    Neg   -> String
    "-"
        Op1 a
    Not   -> String
    "not"
        Op1 a
    Abs   -> String
    "abs"
        Op1 a
    Exp   -> String
    "exp"
        Op1 a
    Sqrt  -> String
    "sqrt"
        Op1 a
    Log   -> String
    "log"
        Op1 a
    Sin   -> String
    "sin"
        Op1 a
    Tan   -> String
    "tan"
        Op1 a
    Cos   -> String
    "cos"
        Op1 a
    Asin  -> String
    "asin"
        Op1 a
    Atan  -> String
    "atan"
        Op1 a
    Acos  -> String
    "acos"
        Op1 a
    Sinh  -> String
    "sinh"
        Op1 a
    Tanh  -> String
    "tanh"
        Op1 a
    Cosh  -> String
    "cosh"
        Op1 a
    Asinh -> String
    "asinh"
        Op1 a
    Atanh -> String
    "atanh"
        Op1 a
    Acosh -> String
    "acosh"

    instance Show (Op2 a b) where
      show :: Op2 a b -> String
    show Op2 a b
    op = case Op2 a b
    op of
        Op2 a b
    Eq   -> String
    "="
        Op2 a b
    Le   -> String
    "<="
        Op2 a b
    Lt   -> String
    "<"
        Op2 a b
    Ge   -> String
    ">="
        Op2 a b
    Gt   -> String
    ">"
        Op2 a b
    And  -> String
    "and"
        Op2 a b
    Or   -> String
    "or"
        Op2 a b
    Add  -> String
    "+"
        Op2 a b
    Sub  -> String
    "-"
        Op2 a b
    Mul  -> String
    "*"
        Op2 a b
    Mod  -> String
    "mod"
        Op2 a b
    Fdiv -> String
    "/"
        Op2 a b
    Pow  -> String
    "^"

    -- | Unhandled unary operator.
    --
    --   Unhandled operators are monomorphic, and their names are labeled so that
    --   each name corresponds to a unique uninterpreted function with a
    --   monomorphic type.
    data UnhandledOp1 = forall a b .
      UnhandledOp1 String (Type a) (Type b)

    -- | Unhandled binary operator.
    --
    --   Unhandled operators are monomorphic, and their names are labeled so that
    --   each name corresponds to a unique uninterpreted function with a
    --   monomorphic type.
    data UnhandledOp2 = forall a b c .
      UnhandledOp2 String (Type a) (Type b) (Type c)

    -- | Translate an Op1.
    --
    -- This function is parameterized so that it can be used to translate
    -- in different contexts and with different targets.
    --
    -- 'm' is the monad in which the computation is made
    --
    -- 'resT' is the desired return type of the expression being translated
    handleOp1 ::
      forall m expr _a _b resT. (Functor m)

      => Type resT
         -- ^ The desired return type

      -> (C.Op1 _a _b, C.Expr _a)
         -- ^ The unary operator encountered and its argument

      -> (forall t t'. Type t -> C.Expr t' -> m (expr t))
         -- ^ The monadic function to translate an expression

      -> (UnhandledOp1 -> m (expr resT))
          -- ^ A function to deal with a operators not handled

      -> (forall t . Type t -> Op1 t -> expr t -> expr t)
         -- ^ The Op1 constructor of the 'expr' type

      -> m (expr resT)

    handleOp1 :: forall (m :: * -> *) (expr :: * -> *) _a _b resT.
    Functor m =>
    Type resT
    -> (Op1 _a _b, Expr _a)
    -> (forall t t'. Type t -> Expr t' -> m (expr t))
    -> (UnhandledOp1 -> m (expr resT))
    -> (forall t. Type t -> Op1 t -> expr t -> expr t)
    -> m (expr resT)
    handleOp1 Type resT
    resT (Op1 _a _b
    op, Expr _a
    e) forall t t'. Type t -> Expr t' -> m (expr t)
    handleExpr UnhandledOp1 -> m (expr resT)
    notHandledF forall t. Type t -> Op1 t -> expr t -> expr t
    mkOp = case Op1 _a _b
    op of

      Op1 _a _b
    C.Not      -> Op1 Bool -> m (expr Bool) -> m (expr resT)
    boolOp Op1 Bool
    Not (Type Bool -> Expr _a -> m (expr Bool)
    forall t t'. Type t -> Expr t' -> m (expr t)
    handleExpr Type Bool
    Bool Expr _a
    e)

      -- Numeric operators
      C.Abs Type _a
    _    -> Op1 resT -> m (expr resT)
    numOp Op1 resT
    forall a. Op1 a
    Abs
      C.Sign Type _a
    ta  -> Type _a -> String -> m (expr resT)
    forall a. Type a -> String -> m (expr resT)
    notHandled Type _a
    ta String
    "sign"

      -- Fractional operators
      C.Recip Type _a
    ta -> Type _a -> String -> m (expr resT)
    forall a. Type a -> String -> m (expr resT)
    notHandled Type _a
    ta String
    "recip"

      -- Floating operators
      C.Exp Type _a
    _    -> Op1 resT -> m (expr resT)
    numOp Op1 resT
    forall a. Op1 a
    Exp
      C.Sqrt Type _a
    _   -> Op1 resT -> m (expr resT)
    numOp Op1 resT
    forall a. Op1 a
    Sqrt
      C.Log Type _a
    _    -> Op1 resT -> m (expr resT)
    numOp Op1 resT
    forall a. Op1 a
    Log
      C.Sin Type _a
    _    -> Op1 resT -> m (expr resT)
    numOp Op1 resT
    forall a. Op1 a
    Sin
      C.Tan Type _a
    _    -> Op1 resT -> m (expr resT)
    numOp Op1 resT
    forall a. Op1 a
    Tan
      C.Cos Type _a
    _    -> Op1 resT -> m (expr resT)
    numOp Op1 resT
    forall a. Op1 a
    Cos
      C.Asin Type _a
    _   -> Op1 resT -> m (expr resT)
    numOp Op1 resT
    forall a. Op1 a
    Asin
      C.Atan Type _a
    _   -> Op1 resT -> m (expr resT)
    numOp Op1 resT
    forall a. Op1 a
    Atan
      C.Acos Type _a
    _   -> Op1 resT -> m (expr resT)
    numOp Op1 resT
    forall a. Op1 a
    Acos
      C.Sinh Type _a
    _   -> Op1 resT -> m (expr resT)
    numOp Op1 resT
    forall a. Op1 a
    Sinh
      C.Tanh Type _a
    _   -> Op1 resT -> m (expr resT)
    numOp Op1 resT
    forall a. Op1 a
    Tanh
      C.Cosh Type _a
    _   -> Op1 resT -> m (expr resT)
    numOp Op1 resT
    forall a. Op1 a
    Cosh
      C.Asinh Type _a
    _  -> Op1 resT -> m (expr resT)
    numOp Op1 resT
    forall a. Op1 a
    Asinh
      C.Atanh Type _a
    _  -> Op1 resT -> m (expr resT)
    numOp Op1 resT
    forall a. Op1 a
    Atanh
      C.Acosh Type _a
    _  -> Op1 resT -> m (expr resT)
    numOp Op1 resT
    forall a. Op1 a
    Acosh

      -- Bitwise operators.
      C.BwNot Type _a
    ta -> Type _a -> String -> m (expr resT)
    forall a. Type a -> String -> m (expr resT)
    notHandled Type _a
    ta String
    "bwnot"

      -- Casting operator.
      C.Cast Type _a
    _ Type _b
    tb -> Type _b -> m (expr resT)
    forall ctb. Type ctb -> m (expr resT)
    castTo Type _b
    tb

      where
        boolOp :: Op1 Bool -> m (expr Bool) -> m (expr resT)
        boolOp :: Op1 Bool -> m (expr Bool) -> m (expr resT)
    boolOp Op1 Bool
    op m (expr Bool)
    e = case Type resT
    resT of
          Type resT
    Bool -> (Type resT -> Op1 resT -> expr resT -> expr resT
    forall t. Type t -> Op1 t -> expr t -> expr t
    mkOp Type resT
    resT Op1 resT
    Op1 Bool
    op) (expr resT -> expr resT) -> m (expr resT) -> m (expr resT)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m (expr resT)
    m (expr Bool)
    e
          Type resT
    _    -> String -> m (expr resT)
    forall a. String -> a
    Err.impossible String
    typeErrMsg

        numOp :: Op1 resT -> m (expr resT)
        numOp :: Op1 resT -> m (expr resT)
    numOp Op1 resT
    op = (Type resT -> Op1 resT -> expr resT -> expr resT
    forall t. Type t -> Op1 t -> expr t -> expr t
    mkOp Type resT
    resT Op1 resT
    op) (expr resT -> expr resT) -> m (expr resT) -> m (expr resT)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Type resT -> Expr _a -> m (expr resT)
    forall t t'. Type t -> Expr t' -> m (expr t)
    handleExpr Type resT
    resT Expr _a
    e)

        -- Casting from Integer (Only possible solution)
        castTo :: C.Type ctb -> m (expr resT)
        castTo :: forall ctb. Type ctb -> m (expr resT)
    castTo Type ctb
    tb = Type ctb -> (forall t'. Type t' -> m (expr resT)) -> m (expr resT)
    forall t a. Type t -> (forall t'. Type t' -> a) -> a
    casting Type ctb
    tb ((forall t'. Type t' -> m (expr resT)) -> m (expr resT))
    -> (forall t'. Type t' -> m (expr resT)) -> m (expr resT)
    forall a b. (a -> b) -> a -> b
    $ \Type t'
    tb' -> case (Type t'
    tb', Type resT
    resT) of
          (Type t'
    Integer, Type resT
    Integer) -> Type resT -> Expr _a -> m (expr resT)
    forall t t'. Type t -> Expr t' -> m (expr t)
    handleExpr Type resT
    Type Integer
    Integer Expr _a
    e
          (Type t'
    Real, Type resT
    Real)       -> Type resT -> Expr _a -> m (expr resT)
    forall t t'. Type t -> Expr t' -> m (expr t)
    handleExpr Type resT
    Type Double
    Real Expr _a
    e
          (Type t', Type resT)
    _                  -> String -> m (expr resT)
    forall a. String -> a
    Err.impossible String
    typeErrMsg

        notHandled ::
          C.Type a -> String -> m (expr resT)
        notHandled :: forall a. Type a -> String -> m (expr resT)
    notHandled Type a
    ta String
    s = Type a -> (forall t'. Type t' -> m (expr resT)) -> m (expr resT)
    forall t a. Type t -> (forall t'. Type t' -> a) -> a
    casting Type a
    ta ((forall t'. Type t' -> m (expr resT)) -> m (expr resT))
    -> (forall t'. Type t' -> m (expr resT)) -> m (expr resT)
    forall a b. (a -> b) -> a -> b
    $ \Type t'
    ta' ->
          UnhandledOp1 -> m (expr resT)
    notHandledF (UnhandledOp1 -> m (expr resT)) -> UnhandledOp1 -> m (expr resT)
    forall a b. (a -> b) -> a -> b
    $ String -> Type t' -> Type resT -> UnhandledOp1
    forall a b. String -> Type a -> Type b -> UnhandledOp1
    UnhandledOp1 String
    s Type t'
    ta' Type resT
    resT

    -- | Translate an Op2.
    --
    -- This function is parameterized so that it can be used to translate
    -- in different contexts and with different targets.
    --
    -- 'm' is the monad in which the computation is made
    --
    -- 'resT' is the desired return type of the expression being translated
    handleOp2 ::
      forall m expr _a _b _c resT . (Monad m)

      => Type resT
         -- ^ The desired return type

      -> (C.Op2 _a _b _c, C.Expr _a, C.Expr _b)
         -- ^ The binary operator encountered and its arguments

      -> (forall t t'. Type t -> C.Expr t' -> m (expr t))
         -- ^ The monadic function to translate an expression

      -> (UnhandledOp2 -> m (expr resT))
          -- ^ A function to deal with a operators not handled

      -> (forall t a . Type t -> Op2 a t -> expr a -> expr a -> expr t)
         -- ^ The Op2 constructor of the 'expr' type

      -> (expr Bool -> expr Bool)
         -- ^ The Op1 for boolean negation

      -> m (expr resT)

    handleOp2 :: forall (m :: * -> *) (expr :: * -> *) _a _b _c resT.
    Monad m =>
    Type resT
    -> (Op2 _a _b _c, Expr _a, Expr _b)
    -> (forall t t'. Type t -> Expr t' -> m (expr t))
    -> (UnhandledOp2 -> m (expr resT))
    -> (forall t a. Type t -> Op2 a t -> expr a -> expr a -> expr t)
    -> (expr Bool -> expr Bool)
    -> m (expr resT)
    handleOp2 Type resT
    resT (Op2 _a _b _c
    op, Expr _a
    e1, Expr _b
    e2) forall t t'. Type t -> Expr t' -> m (expr t)
    handleExpr UnhandledOp2 -> m (expr resT)
    notHandledF forall t a. Type t -> Op2 a t -> expr a -> expr a -> expr t
    mkOp expr Bool -> expr Bool
    notOp = case Op2 _a _b _c
    op of

      Op2 _a _b _c
    C.And        -> Op2 Bool Bool -> m (expr resT)
    boolConnector Op2 Bool Bool
    And
      Op2 _a _b _c
    C.Or         -> Op2 Bool Bool -> m (expr resT)
    boolConnector Op2 Bool Bool
    Or

      -- Numeric operators
      C.Add Type _a
    _      -> (forall num. Num num => Op2 num num) -> m (expr resT)
    numOp Op2 num num
    forall num. Num num => Op2 num num
    Add
      C.Sub Type _a
    _      -> (forall num. Num num => Op2 num num) -> m (expr resT)
    numOp Op2 num num
    forall num. Num num => Op2 num num
    Sub
      C.Mul Type _a
    _      -> (forall num. Num num => Op2 num num) -> m (expr resT)
    numOp Op2 num num
    forall num. Num num => Op2 num num
    Mul

      -- Integral operators.
      C.Mod Type _a
    _    -> (forall num. Num num => Op2 num num) -> m (expr resT)
    numOp Op2 num num
    forall num. Num num => Op2 num num
    Mod
      C.Div Type _a
    ta    -> Type _a -> String -> m (expr resT)
    forall a. Type a -> String -> m (expr resT)
    notHandled Type _a
    ta String
    "div"

      -- Fractional operators.
      C.Fdiv Type _a
    _    -> (forall num. Num num => Op2 num num) -> m (expr resT)
    numOp Op2 num num
    forall num. Num num => Op2 num num
    Fdiv

      -- Floating operators.
      C.Pow Type _a
    _     -> (forall num. Num num => Op2 num num) -> m (expr resT)
    numOp Op2 num num
    forall num. Num num => Op2 num num
    Pow
      C.Logb Type _a
    ta   -> Type _a -> String -> m (expr resT)
    forall a. Type a -> String -> m (expr resT)
    notHandled Type _a
    ta String
    "logb"

      -- Equality operators.
      C.Eq Type _a
    ta     -> Type _a -> m (expr resT)
    forall cta. Type cta -> m (expr resT)
    eqOp Type _a
    ta
      C.Ne Type _a
    ta     -> Type _a -> m (expr resT)
    forall cta. Type cta -> m (expr resT)
    neqOp Type _a
    ta

      -- Relational operators.
      C.Le Type _a
    ta     -> Type _a -> (forall num. Num num => Op2 num Bool) -> m (expr resT)
    forall cta.
    Type cta -> (forall num. Num num => Op2 num Bool) -> m (expr resT)
    numComp Type _a
    ta Op2 num Bool
    forall num. Num num => Op2 num Bool
    Le
      C.Ge Type _a
    ta     -> Type _a -> (forall num. Num num => Op2 num Bool) -> m (expr resT)
    forall cta.
    Type cta -> (forall num. Num num => Op2 num Bool) -> m (expr resT)
    numComp Type _a
    ta Op2 num Bool
    forall num. Num num => Op2 num Bool
    Ge
      C.Lt Type _a
    ta     -> Type _a -> (forall num. Num num => Op2 num Bool) -> m (expr resT)
    forall cta.
    Type cta -> (forall num. Num num => Op2 num Bool) -> m (expr resT)
    numComp Type _a
    ta Op2 num Bool
    forall num. Num num => Op2 num Bool
    Lt
      C.Gt Type _a
    ta     -> Type _a -> (forall num. Num num => Op2 num Bool) -> m (expr resT)
    forall cta.
    Type cta -> (forall num. Num num => Op2 num Bool) -> m (expr resT)
    numComp Type _a
    ta Op2 num Bool
    forall num. Num num => Op2 num Bool
    Gt

      -- Bitwise operators.
      C.BwAnd Type _a
    ta          -> Type _a -> String -> m (expr resT)
    forall a. Type a -> String -> m (expr resT)
    notHandled Type _a
    ta String
    "bwand"
      C.BwOr Type _a
    ta           -> Type _a -> String -> m (expr resT)
    forall a. Type a -> String -> m (expr resT)
    notHandled Type _a
    ta String
    "bwor"
      C.BwXor Type _a
    ta          -> Type _a -> String -> m (expr resT)
    forall a. Type a -> String -> m (expr resT)
    notHandled Type _a
    ta String
    "bwxor"

      -- In fact, '_tb' is ignored caused it can only
      -- be casted to 'Integer', like 'ta'
      C.BwShiftL Type _a
    ta Type _b
    _tb   -> Type _a -> String -> m (expr resT)
    forall a. Type a -> String -> m (expr resT)
    notHandled Type _a
    ta String
    "bwshiftl"
      C.BwShiftR Type _a
    ta Type _b
    _tb   -> Type _a -> String -> m (expr resT)
    forall a. Type a -> String -> m (expr resT)
    notHandled Type _a
    ta String
    "bwshiftr"

      where

        boolOp :: Op2 a Bool -> expr a -> expr a -> expr resT
        boolOp :: forall a. Op2 a Bool -> expr a -> expr a -> expr resT
    boolOp Op2 a Bool
    op expr a
    e1' expr a
    e2' = case Type resT
    resT of
          Type resT
    Bool -> Type resT -> Op2 a resT -> expr a -> expr a -> expr resT
    forall t a. Type t -> Op2 a t -> expr a -> expr a -> expr t
    mkOp Type resT
    resT Op2 a resT
    Op2 a Bool
    op expr a
    e1' expr a
    e2'
          Type resT
    _    -> String -> expr resT
    forall a. String -> a
    Err.impossible String
    typeErrMsg

        boolConnector :: Op2 Bool Bool -> m (expr resT)
        boolConnector :: Op2 Bool Bool -> m (expr resT)
    boolConnector Op2 Bool Bool
    op = do
         e1' <- Type Bool -> Expr _a -> m (expr Bool)
    forall t t'. Type t -> Expr t' -> m (expr t)
    handleExpr Type Bool
    Bool Expr _a
    e1
         e2' <- handleExpr Bool e2
         return $ boolOp op e1' e2'

        eqOp :: C.Type cta -> m (expr resT)
        eqOp :: forall cta. Type cta -> m (expr resT)
    eqOp Type cta
    ta = Type cta -> (forall t'. Type t' -> m (expr resT)) -> m (expr resT)
    forall t a. Type t -> (forall t'. Type t' -> a) -> a
    casting Type cta
    ta ((forall t'. Type t' -> m (expr resT)) -> m (expr resT))
    -> (forall t'. Type t' -> m (expr resT)) -> m (expr resT)
    forall a b. (a -> b) -> a -> b
    $ \Type t'
    ta' -> do
          e1' <-  Type t' -> Expr _a -> m (expr t')
    forall t t'. Type t -> Expr t' -> m (expr t)
    handleExpr Type t'
    ta' Expr _a
    e1
          e2' <-  handleExpr ta' e2
          return $ boolOp Eq e1' e2'

        neqOp ::  C.Type cta -> m (expr resT)
        neqOp :: forall cta. Type cta -> m (expr resT)
    neqOp Type cta
    ta = case Type resT
    resT of
          Type resT
    Bool -> do
            e <- Type cta -> m (expr resT)
    forall cta. Type cta -> m (expr resT)
    eqOp Type cta
    ta
            return $ notOp e
          Type resT
    _ -> String -> m (expr resT)
    forall a. String -> a
    Err.impossible String
    typeErrMsg

        numOp :: (forall num . (Num num) => Op2 num num) -> m (expr resT)
        numOp :: (forall num. Num num => Op2 num num) -> m (expr resT)
    numOp forall num. Num num => Op2 num num
    op = case Type resT
    resT of
          Type resT
    Integer -> do
            e1' <- Type Integer -> Expr _a -> m (expr Integer)
    forall t t'. Type t -> Expr t' -> m (expr t)
    handleExpr Type Integer
    Integer Expr _a
    e1
            e2' <- handleExpr Integer e2
            return $ mkOp resT op e1' e2'

          Type resT
    Real -> do
            e1' <- Type Double -> Expr _a -> m (expr Double)
    forall t t'. Type t -> Expr t' -> m (expr t)
    handleExpr Type Double
    Real Expr _a
    e1
            e2' <- handleExpr Real e2
            return $ mkOp resT op e1' e2'

          Type resT
    _ -> String -> m (expr resT)
    forall a. String -> a
    Err.impossible String
    typeErrMsg

        numComp ::
          C.Type cta ->
          (forall num . (Num num) => Op2 num Bool) -> m (expr resT)
        numComp :: forall cta.
    Type cta -> (forall num. Num num => Op2 num Bool) -> m (expr resT)
    numComp Type cta
    ta forall num. Num num => Op2 num Bool
    op = Type cta -> (forall t'. Type t' -> m (expr resT)) -> m (expr resT)
    forall t a. Type t -> (forall t'. Type t' -> a) -> a
    casting Type cta
    ta ((forall t'. Type t' -> m (expr resT)) -> m (expr resT))
    -> (forall t'. Type t' -> m (expr resT)) -> m (expr resT)
    forall a b. (a -> b) -> a -> b
    $ \case
          Type t'
    Integer -> do
            e1' <- Type Integer -> Expr _a -> m (expr Integer)
    forall t t'. Type t -> Expr t' -> m (expr t)
    handleExpr Type Integer
    Integer Expr _a
    e1
            e2' <- handleExpr Integer e2
            return $ boolOp op e1' e2'
          Type t'
    Real -> do
            e1' <- Type Double -> Expr _a -> m (expr Double)
    forall t t'. Type t -> Expr t' -> m (expr t)
    handleExpr Type Double
    Real Expr _a
    e1
            e2' <- handleExpr Real e2
            return $ boolOp op e1' e2'
          Type t'
    _       -> String -> m (expr resT)
    forall a. String -> a
    Err.impossible String
    typeErrMsg

        notHandled :: forall a . C.Type a -> String -> m (expr resT)
        notHandled :: forall a. Type a -> String -> m (expr resT)
    notHandled Type a
    ta String
    s = Type a -> (forall t'. Type t' -> m (expr resT)) -> m (expr resT)
    forall t a. Type t -> (forall t'. Type t' -> a) -> a
    casting Type a
    ta ((forall t'. Type t' -> m (expr resT)) -> m (expr resT))
    -> (forall t'. Type t' -> m (expr resT)) -> m (expr resT)
    forall a b. (a -> b) -> a -> b
    $ \Type t'
    ta' ->
          UnhandledOp2 -> m (expr resT)
    notHandledF (String -> Type t' -> Type t' -> Type t' -> UnhandledOp2
    forall a b c. String -> Type a -> Type b -> Type c -> UnhandledOp2
    UnhandledOp2 String
    s Type t'
    ta' Type t'
    ta' Type t'
    ta')

    -- | Error message for unexpected behavior / internal errors.
    typeErrMsg :: String
    typeErrMsg :: String
    typeErrMsg = String
    "Unexpected type error in 'Misc.CoreOperators'"