    {-# LANGUAGE PatternSynonyms #-}

    -- | The treeless syntax is intended to be used as input for the compiler backends.
    -- It is more low-level than Internal syntax and is not used for type checking.
    --
    -- Some of the features of treeless syntax are:
    -- - case expressions instead of case trees
    -- - no instantiated datatypes / constructors
    module Agda.Syntax.Treeless
        ( module Agda.Syntax.Abstract.Name
        , module Agda.Syntax.Treeless
        ) where

    import Control.Arrow (first, second)
    import Control.DeepSeq

    import Data.Data (Data)
    import Data.Word

    import GHC.Generics (Generic)

    import Agda.Syntax.Position
    import Agda.Syntax.Literal
    import Agda.Syntax.Common
    import Agda.Syntax.Abstract.Name

    data Compiled = Compiled
      { Compiled -> TTerm
    cTreeless :: TTerm
      , Compiled -> Maybe [ArgUsage]
    cArgUsage :: Maybe [ArgUsage]
          -- ^ 'Nothing' if treeless usage analysis has not run yet.
      }
      deriving (Typeable Compiled
    Typeable Compiled
    -> (forall (c :: * -> *).
        (forall d b. Data d => c (d -> b) -> d -> c b)
        -> (forall g. g -> c g) -> Compiled -> c Compiled)
    -> (forall (c :: * -> *).
        (forall b r. Data b => c (b -> r) -> c r)
        -> (forall r. r -> c r) -> Constr -> c Compiled)
    -> (Compiled -> Constr)
    -> (Compiled -> DataType)
    -> (forall (t :: * -> *) (c :: * -> *).
        Typeable t =>
        (forall d. Data d => c (t d)) -> Maybe (c Compiled))
    -> (forall (t :: * -> * -> *) (c :: * -> *).
        Typeable t =>
        (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Compiled))
    -> ((forall b. Data b => b -> b) -> Compiled -> Compiled)
    -> (forall r r'.
        (r -> r' -> r)
        -> r -> (forall d. Data d => d -> r') -> Compiled -> r)
    -> (forall r r'.
        (r' -> r -> r)
        -> r -> (forall d. Data d => d -> r') -> Compiled -> r)
    -> (forall u. (forall d. Data d => d -> u) -> Compiled -> [u])
    -> (forall u. Int -> (forall d. Data d => d -> u) -> Compiled -> u)
    -> (forall (m :: * -> *).
        Monad m =>
        (forall d. Data d => d -> m d) -> Compiled -> m Compiled)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> Compiled -> m Compiled)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> Compiled -> m Compiled)
    -> Data Compiled
    Compiled -> DataType
    Compiled -> Constr
    (forall b. Data b => b -> b) -> Compiled -> Compiled
    forall a.
    Typeable a
    -> (forall (c :: * -> *).
        (forall d b. Data d => c (d -> b) -> d -> c b)
        -> (forall g. g -> c g) -> a -> c a)
    -> (forall (c :: * -> *).
        (forall b r. Data b => c (b -> r) -> c r)
        -> (forall r. r -> c r) -> Constr -> c a)
    -> (a -> Constr)
    -> (a -> DataType)
    -> (forall (t :: * -> *) (c :: * -> *).
        Typeable t =>
        (forall d. Data d => c (t d)) -> Maybe (c a))
    -> (forall (t :: * -> * -> *) (c :: * -> *).
        Typeable t =>
        (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
    -> ((forall b. Data b => b -> b) -> a -> a)
    -> (forall r r'.
        (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
    -> (forall r r'.
        (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
    -> (forall u. (forall d. Data d => d -> u) -> a -> [u])
    -> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
    -> (forall (m :: * -> *).
        Monad m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> Data a
    forall u. Int -> (forall d. Data d => d -> u) -> Compiled -> u
    forall u. (forall d. Data d => d -> u) -> Compiled -> [u]
    forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> Compiled -> r
    forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> Compiled -> r
    forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Compiled -> m Compiled
    forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Compiled -> m Compiled
    forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Compiled
    forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Compiled -> c Compiled
    forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Compiled)
    forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Compiled)
    gmapMo :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Compiled -> m Compiled
    $cgmapMo :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Compiled -> m Compiled
    gmapMp :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Compiled -> m Compiled
    $cgmapMp :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Compiled -> m Compiled
    gmapM :: forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Compiled -> m Compiled
    $cgmapM :: forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Compiled -> m Compiled
    gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Compiled -> u
    $cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Compiled -> u
    gmapQ :: forall u. (forall d. Data d => d -> u) -> Compiled -> [u]
    $cgmapQ :: forall u. (forall d. Data d => d -> u) -> Compiled -> [u]
    gmapQr :: forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> Compiled -> r
    $cgmapQr :: forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> Compiled -> r
    gmapQl :: forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> Compiled -> r
    $cgmapQl :: forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> Compiled -> r
    gmapT :: (forall b. Data b => b -> b) -> Compiled -> Compiled
    $cgmapT :: (forall b. Data b => b -> b) -> Compiled -> Compiled
    dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Compiled)
    $cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Compiled)
    dataCast1 :: forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Compiled)
    $cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Compiled)
    dataTypeOf :: Compiled -> DataType
    $cdataTypeOf :: Compiled -> DataType
    toConstr :: Compiled -> Constr
    $ctoConstr :: Compiled -> Constr
    gunfold :: forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Compiled
    $cgunfold :: forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Compiled
    gfoldl :: forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Compiled -> c Compiled
    $cgfoldl :: forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Compiled -> c Compiled
    Data, Int -> Compiled -> ShowS
    [Compiled] -> ShowS
    Compiled -> String
    (Int -> Compiled -> ShowS)
    -> (Compiled -> String) -> ([Compiled] -> ShowS) -> Show Compiled
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    showList :: [Compiled] -> ShowS
    $cshowList :: [Compiled] -> ShowS
    show :: Compiled -> String
    $cshow :: Compiled -> String
    showsPrec :: Int -> Compiled -> ShowS
    $cshowsPrec :: Int -> Compiled -> ShowS
    Show, Compiled -> Compiled -> Bool
    (Compiled -> Compiled -> Bool)
    -> (Compiled -> Compiled -> Bool) -> Eq Compiled
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    /= :: Compiled -> Compiled -> Bool
    $c/= :: Compiled -> Compiled -> Bool
    == :: Compiled -> Compiled -> Bool
    $c== :: Compiled -> Compiled -> Bool
    Eq, Eq Compiled
    Eq Compiled
    -> (Compiled -> Compiled -> Ordering)
    -> (Compiled -> Compiled -> Bool)
    -> (Compiled -> Compiled -> Bool)
    -> (Compiled -> Compiled -> Bool)
    -> (Compiled -> Compiled -> Bool)
    -> (Compiled -> Compiled -> Compiled)
    -> (Compiled -> Compiled -> Compiled)
    -> Ord Compiled
    Compiled -> Compiled -> Bool
    Compiled -> Compiled -> Ordering
    Compiled -> Compiled -> Compiled
    forall a.
    Eq a
    -> (a -> a -> Ordering)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> Ord a
    min :: Compiled -> Compiled -> Compiled
    $cmin :: Compiled -> Compiled -> Compiled
    max :: Compiled -> Compiled -> Compiled
    $cmax :: Compiled -> Compiled -> Compiled
    >= :: Compiled -> Compiled -> Bool
    $c>= :: Compiled -> Compiled -> Bool
    > :: Compiled -> Compiled -> Bool
    $c> :: Compiled -> Compiled -> Bool
    <= :: Compiled -> Compiled -> Bool
    $c<= :: Compiled -> Compiled -> Bool
    < :: Compiled -> Compiled -> Bool
    $c< :: Compiled -> Compiled -> Bool
    compare :: Compiled -> Compiled -> Ordering
    $ccompare :: Compiled -> Compiled -> Ordering
    Ord, (forall x. Compiled -> Rep Compiled x)
    -> (forall x. Rep Compiled x -> Compiled) -> Generic Compiled
    forall x. Rep Compiled x -> Compiled
    forall x. Compiled -> Rep Compiled x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cto :: forall x. Rep Compiled x -> Compiled
    $cfrom :: forall x. Compiled -> Rep Compiled x
    Generic)

    -- | Usage status of function arguments in treeless code.
    data ArgUsage
      = ArgUsed
      | ArgUnused
      deriving (Typeable ArgUsage
    Typeable ArgUsage
    -> (forall (c :: * -> *).
        (forall d b. Data d => c (d -> b) -> d -> c b)
        -> (forall g. g -> c g) -> ArgUsage -> c ArgUsage)
    -> (forall (c :: * -> *).
        (forall b r. Data b => c (b -> r) -> c r)
        -> (forall r. r -> c r) -> Constr -> c ArgUsage)
    -> (ArgUsage -> Constr)
    -> (ArgUsage -> DataType)
    -> (forall (t :: * -> *) (c :: * -> *).
        Typeable t =>
        (forall d. Data d => c (t d)) -> Maybe (c ArgUsage))
    -> (forall (t :: * -> * -> *) (c :: * -> *).
        Typeable t =>
        (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ArgUsage))
    -> ((forall b. Data b => b -> b) -> ArgUsage -> ArgUsage)
    -> (forall r r'.
        (r -> r' -> r)
        -> r -> (forall d. Data d => d -> r') -> ArgUsage -> r)
    -> (forall r r'.
        (r' -> r -> r)
        -> r -> (forall d. Data d => d -> r') -> ArgUsage -> r)
    -> (forall u. (forall d. Data d => d -> u) -> ArgUsage -> [u])
    -> (forall u. Int -> (forall d. Data d => d -> u) -> ArgUsage -> u)
    -> (forall (m :: * -> *).
        Monad m =>
        (forall d. Data d => d -> m d) -> ArgUsage -> m ArgUsage)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> ArgUsage -> m ArgUsage)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> ArgUsage -> m ArgUsage)
    -> Data ArgUsage
    ArgUsage -> DataType
    ArgUsage -> Constr
    (forall b. Data b => b -> b) -> ArgUsage -> ArgUsage
    forall a.
    Typeable a
    -> (forall (c :: * -> *).
        (forall d b. Data d => c (d -> b) -> d -> c b)
        -> (forall g. g -> c g) -> a -> c a)
    -> (forall (c :: * -> *).
        (forall b r. Data b => c (b -> r) -> c r)
        -> (forall r. r -> c r) -> Constr -> c a)
    -> (a -> Constr)
    -> (a -> DataType)
    -> (forall (t :: * -> *) (c :: * -> *).
        Typeable t =>
        (forall d. Data d => c (t d)) -> Maybe (c a))
    -> (forall (t :: * -> * -> *) (c :: * -> *).
        Typeable t =>
        (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
    -> ((forall b. Data b => b -> b) -> a -> a)
    -> (forall r r'.
        (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
    -> (forall r r'.
        (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
    -> (forall u. (forall d. Data d => d -> u) -> a -> [u])
    -> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
    -> (forall (m :: * -> *).
        Monad m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> Data a
    forall u. Int -> (forall d. Data d => d -> u) -> ArgUsage -> u
    forall u. (forall d. Data d => d -> u) -> ArgUsage -> [u]
    forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> ArgUsage -> r
    forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> ArgUsage -> r
    forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> ArgUsage -> m ArgUsage
    forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> ArgUsage -> m ArgUsage
    forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c ArgUsage
    forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> ArgUsage -> c ArgUsage
    forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c ArgUsage)
    forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ArgUsage)
    gmapMo :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> ArgUsage -> m ArgUsage
    $cgmapMo :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> ArgUsage -> m ArgUsage
    gmapMp :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> ArgUsage -> m ArgUsage
    $cgmapMp :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> ArgUsage -> m ArgUsage
    gmapM :: forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> ArgUsage -> m ArgUsage
    $cgmapM :: forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> ArgUsage -> m ArgUsage
    gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> ArgUsage -> u
    $cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> ArgUsage -> u
    gmapQ :: forall u. (forall d. Data d => d -> u) -> ArgUsage -> [u]
    $cgmapQ :: forall u. (forall d. Data d => d -> u) -> ArgUsage -> [u]
    gmapQr :: forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> ArgUsage -> r
    $cgmapQr :: forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> ArgUsage -> r
    gmapQl :: forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> ArgUsage -> r
    $cgmapQl :: forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> ArgUsage -> r
    gmapT :: (forall b. Data b => b -> b) -> ArgUsage -> ArgUsage
    $cgmapT :: (forall b. Data b => b -> b) -> ArgUsage -> ArgUsage
    dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ArgUsage)
    $cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ArgUsage)
    dataCast1 :: forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c ArgUsage)
    $cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c ArgUsage)
    dataTypeOf :: ArgUsage -> DataType
    $cdataTypeOf :: ArgUsage -> DataType
    toConstr :: ArgUsage -> Constr
    $ctoConstr :: ArgUsage -> Constr
    gunfold :: forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c ArgUsage
    $cgunfold :: forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c ArgUsage
    gfoldl :: forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> ArgUsage -> c ArgUsage
    $cgfoldl :: forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> ArgUsage -> c ArgUsage
    Data, Int -> ArgUsage -> ShowS
    [ArgUsage] -> ShowS
    ArgUsage -> String
    (Int -> ArgUsage -> ShowS)
    -> (ArgUsage -> String) -> ([ArgUsage] -> ShowS) -> Show ArgUsage
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    showList :: [ArgUsage] -> ShowS
    $cshowList :: [ArgUsage] -> ShowS
    show :: ArgUsage -> String
    $cshow :: ArgUsage -> String
    showsPrec :: Int -> ArgUsage -> ShowS
    $cshowsPrec :: Int -> ArgUsage -> ShowS
    Show, ArgUsage -> ArgUsage -> Bool
    (ArgUsage -> ArgUsage -> Bool)
    -> (ArgUsage -> ArgUsage -> Bool) -> Eq ArgUsage
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    /= :: ArgUsage -> ArgUsage -> Bool
    $c/= :: ArgUsage -> ArgUsage -> Bool
    == :: ArgUsage -> ArgUsage -> Bool
    $c== :: ArgUsage -> ArgUsage -> Bool
    Eq, Eq ArgUsage
    Eq ArgUsage
    -> (ArgUsage -> ArgUsage -> Ordering)
    -> (ArgUsage -> ArgUsage -> Bool)
    -> (ArgUsage -> ArgUsage -> Bool)
    -> (ArgUsage -> ArgUsage -> Bool)
    -> (ArgUsage -> ArgUsage -> Bool)
    -> (ArgUsage -> ArgUsage -> ArgUsage)
    -> (ArgUsage -> ArgUsage -> ArgUsage)
    -> Ord ArgUsage
    ArgUsage -> ArgUsage -> Bool
    ArgUsage -> ArgUsage -> Ordering
    ArgUsage -> ArgUsage -> ArgUsage
    forall a.
    Eq a
    -> (a -> a -> Ordering)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> Ord a
    min :: ArgUsage -> ArgUsage -> ArgUsage
    $cmin :: ArgUsage -> ArgUsage -> ArgUsage
    max :: ArgUsage -> ArgUsage -> ArgUsage
    $cmax :: ArgUsage -> ArgUsage -> ArgUsage
    >= :: ArgUsage -> ArgUsage -> Bool
    $c>= :: ArgUsage -> ArgUsage -> Bool
    > :: ArgUsage -> ArgUsage -> Bool
    $c> :: ArgUsage -> ArgUsage -> Bool
    <= :: ArgUsage -> ArgUsage -> Bool
    $c<= :: ArgUsage -> ArgUsage -> Bool
    < :: ArgUsage -> ArgUsage -> Bool
    $c< :: ArgUsage -> ArgUsage -> Bool
    compare :: ArgUsage -> ArgUsage -> Ordering
    $ccompare :: ArgUsage -> ArgUsage -> Ordering
    Ord, (forall x. ArgUsage -> Rep ArgUsage x)
    -> (forall x. Rep ArgUsage x -> ArgUsage) -> Generic ArgUsage
    forall x. Rep ArgUsage x -> ArgUsage
    forall x. ArgUsage -> Rep ArgUsage x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cto :: forall x. Rep ArgUsage x -> ArgUsage
    $cfrom :: forall x. ArgUsage -> Rep ArgUsage x
    Generic)

    -- | The treeless compiler can behave differently depending on the target
    --   language evaluation strategy. For instance, more aggressive erasure for
    --   lazy targets.
    data EvaluationStrategy = LazyEvaluation | EagerEvaluation
      deriving (EvaluationStrategy -> EvaluationStrategy -> Bool
    (EvaluationStrategy -> EvaluationStrategy -> Bool)
    -> (EvaluationStrategy -> EvaluationStrategy -> Bool)
    -> Eq EvaluationStrategy
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    /= :: EvaluationStrategy -> EvaluationStrategy -> Bool
    $c/= :: EvaluationStrategy -> EvaluationStrategy -> Bool
    == :: EvaluationStrategy -> EvaluationStrategy -> Bool
    $c== :: EvaluationStrategy -> EvaluationStrategy -> Bool
    Eq, Int -> EvaluationStrategy -> ShowS
    [EvaluationStrategy] -> ShowS
    EvaluationStrategy -> String
    (Int -> EvaluationStrategy -> ShowS)
    -> (EvaluationStrategy -> String)
    -> ([EvaluationStrategy] -> ShowS)
    -> Show EvaluationStrategy
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    showList :: [EvaluationStrategy] -> ShowS
    $cshowList :: [EvaluationStrategy] -> ShowS
    show :: EvaluationStrategy -> String
    $cshow :: EvaluationStrategy -> String
    showsPrec :: Int -> EvaluationStrategy -> ShowS
    $cshowsPrec :: Int -> EvaluationStrategy -> ShowS
    Show)

    type Args = [TTerm]

    -- this currently assumes that TApp is translated in a lazy/cbn fashion.
    -- The AST should also support strict translation.
    --
    -- All local variables are using de Bruijn indices.
    data TTerm = TVar Int
               | TPrim TPrim
               | TDef QName
               | TApp TTerm Args
               | TLam TTerm
               | TLit Literal
               | TCon QName
               | TLet TTerm TTerm
               -- ^ introduces a new local binding. The bound term
               -- MUST only be evaluated if it is used inside the body.
               -- Sharing may happen, but is optional.
               -- It is also perfectly valid to just inline the bound term in the body.
               | TCase Int CaseInfo TTerm [TAlt]
               -- ^ Case scrutinee (always variable), case type, default value, alternatives
               -- First, all TACon alternatives are tried; then all TAGuard alternatives
               -- in top to bottom order.
               -- TACon alternatives must not overlap.
               | TUnit -- used for levels right now
               | TSort
               | TErased
               | TCoerce TTerm  -- ^ Used by the GHC backend
               | TError TError
               -- ^ A runtime error, something bad has happened.
      deriving (Typeable TTerm
    Typeable TTerm
    -> (forall (c :: * -> *).
        (forall d b. Data d => c (d -> b) -> d -> c b)
        -> (forall g. g -> c g) -> TTerm -> c TTerm)
    -> (forall (c :: * -> *).
        (forall b r. Data b => c (b -> r) -> c r)
        -> (forall r. r -> c r) -> Constr -> c TTerm)
    -> (TTerm -> Constr)
    -> (TTerm -> DataType)
    -> (forall (t :: * -> *) (c :: * -> *).
        Typeable t =>
        (forall d. Data d => c (t d)) -> Maybe (c TTerm))
    -> (forall (t :: * -> * -> *) (c :: * -> *).
        Typeable t =>
        (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TTerm))
    -> ((forall b. Data b => b -> b) -> TTerm -> TTerm)
    -> (forall r r'.
        (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TTerm -> r)
    -> (forall r r'.
        (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TTerm -> r)
    -> (forall u. (forall d. Data d => d -> u) -> TTerm -> [u])
    -> (forall u. Int -> (forall d. Data d => d -> u) -> TTerm -> u)
    -> (forall (m :: * -> *).
        Monad m =>
        (forall d. Data d => d -> m d) -> TTerm -> m TTerm)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> TTerm -> m TTerm)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> TTerm -> m TTerm)
    -> Data TTerm
    TTerm -> DataType
    TTerm -> Constr
    (forall b. Data b => b -> b) -> TTerm -> TTerm
    forall a.
    Typeable a
    -> (forall (c :: * -> *).
        (forall d b. Data d => c (d -> b) -> d -> c b)
        -> (forall g. g -> c g) -> a -> c a)
    -> (forall (c :: * -> *).
        (forall b r. Data b => c (b -> r) -> c r)
        -> (forall r. r -> c r) -> Constr -> c a)
    -> (a -> Constr)
    -> (a -> DataType)
    -> (forall (t :: * -> *) (c :: * -> *).
        Typeable t =>
        (forall d. Data d => c (t d)) -> Maybe (c a))
    -> (forall (t :: * -> * -> *) (c :: * -> *).
        Typeable t =>
        (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
    -> ((forall b. Data b => b -> b) -> a -> a)
    -> (forall r r'.
        (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
    -> (forall r r'.
        (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
    -> (forall u. (forall d. Data d => d -> u) -> a -> [u])
    -> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
    -> (forall (m :: * -> *).
        Monad m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> Data a
    forall u. Int -> (forall d. Data d => d -> u) -> TTerm -> u
    forall u. (forall d. Data d => d -> u) -> TTerm -> [u]
    forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TTerm -> r
    forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TTerm -> r
    forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> TTerm -> m TTerm
    forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> TTerm -> m TTerm
    forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c TTerm
    forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> TTerm -> c TTerm
    forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c TTerm)
    forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TTerm)
    gmapMo :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> TTerm -> m TTerm
    $cgmapMo :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> TTerm -> m TTerm
    gmapMp :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> TTerm -> m TTerm
    $cgmapMp :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> TTerm -> m TTerm
    gmapM :: forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> TTerm -> m TTerm
    $cgmapM :: forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> TTerm -> m TTerm
    gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> TTerm -> u
    $cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> TTerm -> u
    gmapQ :: forall u. (forall d. Data d => d -> u) -> TTerm -> [u]
    $cgmapQ :: forall u. (forall d. Data d => d -> u) -> TTerm -> [u]
    gmapQr :: forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TTerm -> r
    $cgmapQr :: forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TTerm -> r
    gmapQl :: forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TTerm -> r
    $cgmapQl :: forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TTerm -> r
    gmapT :: (forall b. Data b => b -> b) -> TTerm -> TTerm
    $cgmapT :: (forall b. Data b => b -> b) -> TTerm -> TTerm
    dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TTerm)
    $cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TTerm)
    dataCast1 :: forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c TTerm)
    $cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c TTerm)
    dataTypeOf :: TTerm -> DataType
    $cdataTypeOf :: TTerm -> DataType
    toConstr :: TTerm -> Constr
    $ctoConstr :: TTerm -> Constr
    gunfold :: forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c TTerm
    $cgunfold :: forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c TTerm
    gfoldl :: forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> TTerm -> c TTerm
    $cgfoldl :: forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> TTerm -> c TTerm
    Data, Int -> TTerm -> ShowS
    Args -> ShowS
    TTerm -> String
    (Int -> TTerm -> ShowS)
    -> (TTerm -> String) -> (Args -> ShowS) -> Show TTerm
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    showList :: Args -> ShowS
    $cshowList :: Args -> ShowS
    show :: TTerm -> String
    $cshow :: TTerm -> String
    showsPrec :: Int -> TTerm -> ShowS
    $cshowsPrec :: Int -> TTerm -> ShowS
    Show, TTerm -> TTerm -> Bool
    (TTerm -> TTerm -> Bool) -> (TTerm -> TTerm -> Bool) -> Eq TTerm
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    /= :: TTerm -> TTerm -> Bool
    $c/= :: TTerm -> TTerm -> Bool
    == :: TTerm -> TTerm -> Bool
    $c== :: TTerm -> TTerm -> Bool
    Eq, Eq TTerm
    Eq TTerm
    -> (TTerm -> TTerm -> Ordering)
    -> (TTerm -> TTerm -> Bool)
    -> (TTerm -> TTerm -> Bool)
    -> (TTerm -> TTerm -> Bool)
    -> (TTerm -> TTerm -> Bool)
    -> (TTerm -> TTerm -> TTerm)
    -> (TTerm -> TTerm -> TTerm)
    -> Ord TTerm
    TTerm -> TTerm -> Bool
    TTerm -> TTerm -> Ordering
    TTerm -> TTerm -> TTerm
    forall a.
    Eq a
    -> (a -> a -> Ordering)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> Ord a
    min :: TTerm -> TTerm -> TTerm
    $cmin :: TTerm -> TTerm -> TTerm
    max :: TTerm -> TTerm -> TTerm
    $cmax :: TTerm -> TTerm -> TTerm
    >= :: TTerm -> TTerm -> Bool
    $c>= :: TTerm -> TTerm -> Bool
    > :: TTerm -> TTerm -> Bool
    $c> :: TTerm -> TTerm -> Bool
    <= :: TTerm -> TTerm -> Bool
    $c<= :: TTerm -> TTerm -> Bool
    < :: TTerm -> TTerm -> Bool
    $c< :: TTerm -> TTerm -> Bool
    compare :: TTerm -> TTerm -> Ordering
    $ccompare :: TTerm -> TTerm -> Ordering
    Ord, (forall x. TTerm -> Rep TTerm x)
    -> (forall x. Rep TTerm x -> TTerm) -> Generic TTerm
    forall x. Rep TTerm x -> TTerm
    forall x. TTerm -> Rep TTerm x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cto :: forall x. Rep TTerm x -> TTerm
    $cfrom :: forall x. TTerm -> Rep TTerm x
    Generic)

    -- | Compiler-related primitives. This are NOT the same thing as primitives
    -- in Agda's surface or internal syntax!
    -- Some of the primitives have a suffix indicating which type of arguments they take,
    -- using the following naming convention:
    -- Char | Type
    -- C    | Character
    -- F    | Float
    -- I    | Integer
    -- Q    | QName
    -- S    | String
    data TPrim
      = PAdd | PAdd64
      | PSub | PSub64
      | PMul | PMul64
      | PQuot | PQuot64
      | PRem  | PRem64
      | PGeq
      | PLt   | PLt64
      | PEqI  | PEq64
      | PEqF
      | PEqS
      | PEqC
      | PEqQ
      | PIf
      | PSeq
      | PITo64 | P64ToI
      deriving (Typeable TPrim
    Typeable TPrim
    -> (forall (c :: * -> *).
        (forall d b. Data d => c (d -> b) -> d -> c b)
        -> (forall g. g -> c g) -> TPrim -> c TPrim)
    -> (forall (c :: * -> *).
        (forall b r. Data b => c (b -> r) -> c r)
        -> (forall r. r -> c r) -> Constr -> c TPrim)
    -> (TPrim -> Constr)
    -> (TPrim -> DataType)
    -> (forall (t :: * -> *) (c :: * -> *).
        Typeable t =>
        (forall d. Data d => c (t d)) -> Maybe (c TPrim))
    -> (forall (t :: * -> * -> *) (c :: * -> *).
        Typeable t =>
        (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TPrim))
    -> ((forall b. Data b => b -> b) -> TPrim -> TPrim)
    -> (forall r r'.
        (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TPrim -> r)
    -> (forall r r'.
        (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TPrim -> r)
    -> (forall u. (forall d. Data d => d -> u) -> TPrim -> [u])
    -> (forall u. Int -> (forall d. Data d => d -> u) -> TPrim -> u)
    -> (forall (m :: * -> *).
        Monad m =>
        (forall d. Data d => d -> m d) -> TPrim -> m TPrim)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> TPrim -> m TPrim)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> TPrim -> m TPrim)
    -> Data TPrim
    TPrim -> DataType
    TPrim -> Constr
    (forall b. Data b => b -> b) -> TPrim -> TPrim
    forall a.
    Typeable a
    -> (forall (c :: * -> *).
        (forall d b. Data d => c (d -> b) -> d -> c b)
        -> (forall g. g -> c g) -> a -> c a)
    -> (forall (c :: * -> *).
        (forall b r. Data b => c (b -> r) -> c r)
        -> (forall r. r -> c r) -> Constr -> c a)
    -> (a -> Constr)
    -> (a -> DataType)
    -> (forall (t :: * -> *) (c :: * -> *).
        Typeable t =>
        (forall d. Data d => c (t d)) -> Maybe (c a))
    -> (forall (t :: * -> * -> *) (c :: * -> *).
        Typeable t =>
        (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
    -> ((forall b. Data b => b -> b) -> a -> a)
    -> (forall r r'.
        (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
    -> (forall r r'.
        (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
    -> (forall u. (forall d. Data d => d -> u) -> a -> [u])
    -> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
    -> (forall (m :: * -> *).
        Monad m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> Data a
    forall u. Int -> (forall d. Data d => d -> u) -> TPrim -> u
    forall u. (forall d. Data d => d -> u) -> TPrim -> [u]
    forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TPrim -> r
    forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TPrim -> r
    forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> TPrim -> m TPrim
    forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> TPrim -> m TPrim
    forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c TPrim
    forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> TPrim -> c TPrim
    forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c TPrim)
    forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TPrim)
    gmapMo :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> TPrim -> m TPrim
    $cgmapMo :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> TPrim -> m TPrim
    gmapMp :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> TPrim -> m TPrim
    $cgmapMp :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> TPrim -> m TPrim
    gmapM :: forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> TPrim -> m TPrim
    $cgmapM :: forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> TPrim -> m TPrim
    gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> TPrim -> u
    $cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> TPrim -> u
    gmapQ :: forall u. (forall d. Data d => d -> u) -> TPrim -> [u]
    $cgmapQ :: forall u. (forall d. Data d => d -> u) -> TPrim -> [u]
    gmapQr :: forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TPrim -> r
    $cgmapQr :: forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TPrim -> r
    gmapQl :: forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TPrim -> r
    $cgmapQl :: forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TPrim -> r
    gmapT :: (forall b. Data b => b -> b) -> TPrim -> TPrim
    $cgmapT :: (forall b. Data b => b -> b) -> TPrim -> TPrim
    dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TPrim)
    $cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TPrim)
    dataCast1 :: forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c TPrim)
    $cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c TPrim)
    dataTypeOf :: TPrim -> DataType
    $cdataTypeOf :: TPrim -> DataType
    toConstr :: TPrim -> Constr
    $ctoConstr :: TPrim -> Constr
    gunfold :: forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c TPrim
    $cgunfold :: forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c TPrim
    gfoldl :: forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> TPrim -> c TPrim
    $cgfoldl :: forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> TPrim -> c TPrim
    Data, Int -> TPrim -> ShowS
    [TPrim] -> ShowS
    TPrim -> String
    (Int -> TPrim -> ShowS)
    -> (TPrim -> String) -> ([TPrim] -> ShowS) -> Show TPrim
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    showList :: [TPrim] -> ShowS
    $cshowList :: [TPrim] -> ShowS
    show :: TPrim -> String
    $cshow :: TPrim -> String
    showsPrec :: Int -> TPrim -> ShowS
    $cshowsPrec :: Int -> TPrim -> ShowS
    Show, TPrim -> TPrim -> Bool
    (TPrim -> TPrim -> Bool) -> (TPrim -> TPrim -> Bool) -> Eq TPrim
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    /= :: TPrim -> TPrim -> Bool
    $c/= :: TPrim -> TPrim -> Bool
    == :: TPrim -> TPrim -> Bool
    $c== :: TPrim -> TPrim -> Bool
    Eq, Eq TPrim
    Eq TPrim
    -> (TPrim -> TPrim -> Ordering)
    -> (TPrim -> TPrim -> Bool)
    -> (TPrim -> TPrim -> Bool)
    -> (TPrim -> TPrim -> Bool)
    -> (TPrim -> TPrim -> Bool)
    -> (TPrim -> TPrim -> TPrim)
    -> (TPrim -> TPrim -> TPrim)
    -> Ord TPrim
    TPrim -> TPrim -> Bool
    TPrim -> TPrim -> Ordering
    TPrim -> TPrim -> TPrim
    forall a.
    Eq a
    -> (a -> a -> Ordering)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> Ord a
    min :: TPrim -> TPrim -> TPrim
    $cmin :: TPrim -> TPrim -> TPrim
    max :: TPrim -> TPrim -> TPrim
    $cmax :: TPrim -> TPrim -> TPrim
    >= :: TPrim -> TPrim -> Bool
    $c>= :: TPrim -> TPrim -> Bool
    > :: TPrim -> TPrim -> Bool
    $c> :: TPrim -> TPrim -> Bool
    <= :: TPrim -> TPrim -> Bool
    $c<= :: TPrim -> TPrim -> Bool
    < :: TPrim -> TPrim -> Bool
    $c< :: TPrim -> TPrim -> Bool
    compare :: TPrim -> TPrim -> Ordering
    $ccompare :: TPrim -> TPrim -> Ordering
    Ord, (forall x. TPrim -> Rep TPrim x)
    -> (forall x. Rep TPrim x -> TPrim) -> Generic TPrim
    forall x. Rep TPrim x -> TPrim
    forall x. TPrim -> Rep TPrim x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cto :: forall x. Rep TPrim x -> TPrim
    $cfrom :: forall x. TPrim -> Rep TPrim x
    Generic)

    isPrimEq :: TPrim -> Bool
    isPrimEq :: TPrim -> Bool
    isPrimEq TPrim
    p = TPrim
    p TPrim -> [TPrim] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` [TPrim
    PEqI, TPrim
    PEqF, TPrim
    PEqS, TPrim
    PEqC, TPrim
    PEqQ, TPrim
    PEq64]

    -- | Strip leading coercions and indicate whether there were some.
    coerceView :: TTerm -> (Bool, TTerm)
    coerceView :: TTerm -> (Bool, TTerm)
    coerceView = \case
      TCoerce TTerm
    t -> (Bool
    True,) (TTerm -> (Bool, TTerm)) -> TTerm -> (Bool, TTerm)
    forall a b. (a -> b) -> a -> b
    $ (Bool, TTerm) -> TTerm
    forall a b. (a, b) -> b
    snd ((Bool, TTerm) -> TTerm) -> (Bool, TTerm) -> TTerm
    forall a b. (a -> b) -> a -> b
    $ TTerm -> (Bool, TTerm)
    coerceView TTerm
    t
      TTerm
    t         -> (Bool
    False, TTerm
    t)

    mkTApp :: TTerm -> Args -> TTerm
    mkTApp :: TTerm -> Args -> TTerm
    mkTApp TTerm
    x           [] = TTerm
    x
    mkTApp (TApp TTerm
    x Args
    as) Args
    bs = TTerm -> Args -> TTerm
    TApp TTerm
    x (Args
    as Args -> Args -> Args
    forall a. [a] -> [a] -> [a]
    ++ Args
    bs)
    mkTApp TTerm
    x           Args
    as = TTerm -> Args -> TTerm
    TApp TTerm
    x Args
    as

    tAppView :: TTerm -> (TTerm, [TTerm])
    tAppView :: TTerm -> (TTerm, Args)
    tAppView = \case
      TApp TTerm
    a Args
    bs -> (Args -> Args) -> (TTerm, Args) -> (TTerm, Args)
    forall (a :: * -> * -> *) b c d.
    Arrow a =>
    a b c -> a (d, b) (d, c)
    second (Args -> Args -> Args
    forall a. [a] -> [a] -> [a]
    ++ Args
    bs) ((TTerm, Args) -> (TTerm, Args)) -> (TTerm, Args) -> (TTerm, Args)
    forall a b. (a -> b) -> a -> b
    $ TTerm -> (TTerm, Args)
    tAppView TTerm
    a
      TTerm
    t         -> (TTerm
    t, [])

    -- | Expose the format @coerce f args@.
    --
    --   We fuse coercions, even if interleaving with applications.
    --   We assume that coercion is powerful enough to satisfy
    --   @
    --      coerce (coerce f a) b = coerce f a b
    --   @
    coerceAppView :: TTerm -> ((Bool, TTerm), [TTerm])
    coerceAppView :: TTerm -> ((Bool, TTerm), Args)
    coerceAppView = \case
      TCoerce TTerm
    t -> ((Bool, TTerm) -> (Bool, TTerm))
    -> ((Bool, TTerm), Args) -> ((Bool, TTerm), Args)
    forall (a :: * -> * -> *) b c d.
    Arrow a =>
    a b c -> a (b, d) (c, d)
    first ((Bool
    True,) (TTerm -> (Bool, TTerm))
    -> ((Bool, TTerm) -> TTerm) -> (Bool, TTerm) -> (Bool, TTerm)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Bool, TTerm) -> TTerm
    forall a b. (a, b) -> b
    snd) (((Bool, TTerm), Args) -> ((Bool, TTerm), Args))
    -> ((Bool, TTerm), Args) -> ((Bool, TTerm), Args)
    forall a b. (a -> b) -> a -> b
    $ TTerm -> ((Bool, TTerm), Args)
    coerceAppView TTerm
    t
      TApp TTerm
    a Args
    bs -> (Args -> Args) -> ((Bool, TTerm), Args) -> ((Bool, TTerm), Args)
    forall (a :: * -> * -> *) b c d.
    Arrow a =>
    a b c -> a (d, b) (d, c)
    second (Args -> Args -> Args
    forall a. [a] -> [a] -> [a]
    ++ Args
    bs) (((Bool, TTerm), Args) -> ((Bool, TTerm), Args))
    -> ((Bool, TTerm), Args) -> ((Bool, TTerm), Args)
    forall a b. (a -> b) -> a -> b
    $ TTerm -> ((Bool, TTerm), Args)
    coerceAppView TTerm
    a
      TTerm
    t         -> ((Bool
    False, TTerm
    t), [])

    tLetView :: TTerm -> ([TTerm], TTerm)
    tLetView :: TTerm -> (Args, TTerm)
    tLetView (TLet TTerm
    e TTerm
    b) = (Args -> Args) -> (Args, TTerm) -> (Args, TTerm)
    forall (a :: * -> * -> *) b c d.
    Arrow a =>
    a b c -> a (b, d) (c, d)
    first (TTerm
    e TTerm -> Args -> Args
    forall a. a -> [a] -> [a]
    :) ((Args, TTerm) -> (Args, TTerm)) -> (Args, TTerm) -> (Args, TTerm)
    forall a b. (a -> b) -> a -> b
    $ TTerm -> (Args, TTerm)
    tLetView TTerm
    b
    tLetView TTerm
    e          = ([], TTerm
    e)

    tLamView :: TTerm -> (Int, TTerm)
    tLamView :: TTerm -> (Int, TTerm)
    tLamView = Int -> TTerm -> (Int, TTerm)
    forall {a}. Num a => a -> TTerm -> (a, TTerm)
    go Int
    0
      where go :: a -> TTerm -> (a, TTerm)
    go a
    n (TLam TTerm
    b) = a -> TTerm -> (a, TTerm)
    go (a
    n a -> a -> a
    forall a. Num a => a -> a -> a
    + a
    1) TTerm
    b
            go a
    n TTerm
    t        = (a
    n, TTerm
    t)

    mkTLam :: Int -> TTerm -> TTerm
    mkTLam :: Int -> TTerm -> TTerm
    mkTLam Int
    n TTerm
    b = ((TTerm -> TTerm) -> TTerm -> TTerm)
    -> TTerm -> [TTerm -> TTerm] -> TTerm
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr (TTerm -> TTerm) -> TTerm -> TTerm
    forall a b. (a -> b) -> a -> b
    ($) TTerm
    b ([TTerm -> TTerm] -> TTerm) -> [TTerm -> TTerm] -> TTerm
    forall a b. (a -> b) -> a -> b
    $ Int -> (TTerm -> TTerm) -> [TTerm -> TTerm]
    forall a. Int -> a -> [a]
    replicate Int
    n TTerm -> TTerm
    TLam

    -- | Introduces a new binding
    mkLet :: TTerm -> TTerm -> TTerm
    mkLet :: TTerm -> TTerm -> TTerm
    mkLet TTerm
    x TTerm
    body = TTerm -> TTerm -> TTerm
    TLet TTerm
    x TTerm
    body

    tInt :: Integer -> TTerm
    tInt :: Integer -> TTerm
    tInt = Literal -> TTerm
    TLit (Literal -> TTerm) -> (Integer -> Literal) -> Integer -> TTerm
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Integer -> Literal
    LitNat

    intView :: TTerm -> Maybe Integer
    intView :: TTerm -> Maybe Integer
    intView (TLit (LitNat Integer
    x)) = Integer -> Maybe Integer
    forall a. a -> Maybe a
    Just Integer
    x
    intView TTerm
    _ = Maybe Integer
    forall a. Maybe a
    Nothing

    word64View :: TTerm -> Maybe Word64
    word64View :: TTerm -> Maybe Word64
    word64View (TLit (LitWord64 Word64
    x)) = Word64 -> Maybe Word64
    forall a. a -> Maybe a
    Just Word64
    x
    word64View TTerm
    _ = Maybe Word64
    forall a. Maybe a
    Nothing

    tPlusK :: Integer -> TTerm -> TTerm
    tPlusK :: Integer -> TTerm -> TTerm
    tPlusK Integer
    0 TTerm
    n = TTerm
    n
    tPlusK Integer
    k TTerm
    n | Integer
    k Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    < Integer
    0 = TPrim -> TTerm -> TTerm -> TTerm
    tOp TPrim
    PSub TTerm
    n (Integer -> TTerm
    tInt (-Integer
    k))
    tPlusK Integer
    k TTerm
    n = TPrim -> TTerm -> TTerm -> TTerm
    tOp TPrim
    PAdd (Integer -> TTerm
    tInt Integer
    k) TTerm
    n

    -- -(k + n)
    tNegPlusK :: Integer -> TTerm -> TTerm
    tNegPlusK :: Integer -> TTerm -> TTerm
    tNegPlusK Integer
    k TTerm
    n = TPrim -> TTerm -> TTerm -> TTerm
    tOp TPrim
    PSub (Integer -> TTerm
    tInt (-Integer
    k)) TTerm
    n

    plusKView :: TTerm -> Maybe (Integer, TTerm)
    plusKView :: TTerm -> Maybe (Integer, TTerm)
    plusKView (TApp (TPrim TPrim
    PAdd) [TTerm
    k, TTerm
    n]) | Just Integer
    k <- TTerm -> Maybe Integer
    intView TTerm
    k = (Integer, TTerm) -> Maybe (Integer, TTerm)
    forall a. a -> Maybe a
    Just (Integer
    k, TTerm
    n)
    plusKView (TApp (TPrim TPrim
    PSub) [TTerm
    n, TTerm
    k]) | Just Integer
    k <- TTerm -> Maybe Integer
    intView TTerm
    k = (Integer, TTerm) -> Maybe (Integer, TTerm)
    forall a. a -> Maybe a
    Just (-Integer
    k, TTerm
    n)
    plusKView TTerm
    _ = Maybe (Integer, TTerm)
    forall a. Maybe a
    Nothing

    negPlusKView :: TTerm -> Maybe (Integer, TTerm)
    negPlusKView :: TTerm -> Maybe (Integer, TTerm)
    negPlusKView (TApp (TPrim TPrim
    PSub) [TTerm
    k, TTerm
    n]) | Just Integer
    k <- TTerm -> Maybe Integer
    intView TTerm
    k = (Integer, TTerm) -> Maybe (Integer, TTerm)
    forall a. a -> Maybe a
    Just (-Integer
    k, TTerm
    n)
    negPlusKView TTerm
    _ = Maybe (Integer, TTerm)
    forall a. Maybe a
    Nothing

    tOp :: TPrim -> TTerm -> TTerm -> TTerm
    tOp :: TPrim -> TTerm -> TTerm -> TTerm
    tOp TPrim
    op TTerm
    a TTerm
    b = TPrim -> TTerm -> TTerm -> TTerm
    TPOp TPrim
    op TTerm
    a TTerm
    b

    pattern TPOp :: TPrim -> TTerm -> TTerm -> TTerm
    pattern $bTPOp :: TPrim -> TTerm -> TTerm -> TTerm
    $mTPOp :: forall {r}.
    TTerm -> (TPrim -> TTerm -> TTerm -> r) -> (Void# -> r) -> r
    TPOp op a b = TApp (TPrim op) [a, b]

    pattern TPFn :: TPrim -> TTerm -> TTerm
    pattern $bTPFn :: TPrim -> TTerm -> TTerm
    $mTPFn :: forall {r}. TTerm -> (TPrim -> TTerm -> r) -> (Void# -> r) -> r
    TPFn op a = TApp (TPrim op) [a]

    tUnreachable :: TTerm
    tUnreachable :: TTerm
    tUnreachable = TError -> TTerm
    TError TError
    TUnreachable

    tIfThenElse :: TTerm -> TTerm -> TTerm -> TTerm
    tIfThenElse :: TTerm -> TTerm -> TTerm -> TTerm
    tIfThenElse TTerm
    c TTerm
    i TTerm
    e = TTerm -> Args -> TTerm
    TApp (TPrim -> TTerm
    TPrim TPrim
    PIf) [TTerm
    c, TTerm
    i, TTerm
    e]

    data CaseType
      = CTData Quantity QName
        -- Case on datatype. The 'Quantity' is zero for matches on erased
        -- arguments.
      | CTNat
      | CTInt
      | CTChar
      | CTString
      | CTFloat
      | CTQName
      deriving (Typeable CaseType
    Typeable CaseType
    -> (forall (c :: * -> *).
        (forall d b. Data d => c (d -> b) -> d -> c b)
        -> (forall g. g -> c g) -> CaseType -> c CaseType)
    -> (forall (c :: * -> *).
        (forall b r. Data b => c (b -> r) -> c r)
        -> (forall r. r -> c r) -> Constr -> c CaseType)
    -> (CaseType -> Constr)
    -> (CaseType -> DataType)
    -> (forall (t :: * -> *) (c :: * -> *).
        Typeable t =>
        (forall d. Data d => c (t d)) -> Maybe (c CaseType))
    -> (forall (t :: * -> * -> *) (c :: * -> *).
        Typeable t =>
        (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c CaseType))
    -> ((forall b. Data b => b -> b) -> CaseType -> CaseType)
    -> (forall r r'.
        (r -> r' -> r)
        -> r -> (forall d. Data d => d -> r') -> CaseType -> r)
    -> (forall r r'.
        (r' -> r -> r)
        -> r -> (forall d. Data d => d -> r') -> CaseType -> r)
    -> (forall u. (forall d. Data d => d -> u) -> CaseType -> [u])
    -> (forall u. Int -> (forall d. Data d => d -> u) -> CaseType -> u)
    -> (forall (m :: * -> *).
        Monad m =>
        (forall d. Data d => d -> m d) -> CaseType -> m CaseType)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> CaseType -> m CaseType)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> CaseType -> m CaseType)
    -> Data CaseType
    CaseType -> DataType
    CaseType -> Constr
    (forall b. Data b => b -> b) -> CaseType -> CaseType
    forall a.
    Typeable a
    -> (forall (c :: * -> *).
        (forall d b. Data d => c (d -> b) -> d -> c b)
        -> (forall g. g -> c g) -> a -> c a)
    -> (forall (c :: * -> *).
        (forall b r. Data b => c (b -> r) -> c r)
        -> (forall r. r -> c r) -> Constr -> c a)
    -> (a -> Constr)
    -> (a -> DataType)
    -> (forall (t :: * -> *) (c :: * -> *).
        Typeable t =>
        (forall d. Data d => c (t d)) -> Maybe (c a))
    -> (forall (t :: * -> * -> *) (c :: * -> *).
        Typeable t =>
        (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
    -> ((forall b. Data b => b -> b) -> a -> a)
    -> (forall r r'.
        (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
    -> (forall r r'.
        (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
    -> (forall u. (forall d. Data d => d -> u) -> a -> [u])
    -> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
    -> (forall (m :: * -> *).
        Monad m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> Data a
    forall u. Int -> (forall d. Data d => d -> u) -> CaseType -> u
    forall u. (forall d. Data d => d -> u) -> CaseType -> [u]
    forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> CaseType -> r
    forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> CaseType -> r
    forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> CaseType -> m CaseType
    forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> CaseType -> m CaseType
    forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c CaseType
    forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> CaseType -> c CaseType
    forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c CaseType)
    forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c CaseType)
    gmapMo :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> CaseType -> m CaseType
    $cgmapMo :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> CaseType -> m CaseType
    gmapMp :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> CaseType -> m CaseType
    $cgmapMp :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> CaseType -> m CaseType
    gmapM :: forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> CaseType -> m CaseType
    $cgmapM :: forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> CaseType -> m CaseType
    gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> CaseType -> u
    $cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> CaseType -> u
    gmapQ :: forall u. (forall d. Data d => d -> u) -> CaseType -> [u]
    $cgmapQ :: forall u. (forall d. Data d => d -> u) -> CaseType -> [u]
    gmapQr :: forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> CaseType -> r
    $cgmapQr :: forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> CaseType -> r
    gmapQl :: forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> CaseType -> r
    $cgmapQl :: forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> CaseType -> r
    gmapT :: (forall b. Data b => b -> b) -> CaseType -> CaseType
    $cgmapT :: (forall b. Data b => b -> b) -> CaseType -> CaseType
    dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c CaseType)
    $cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c CaseType)
    dataCast1 :: forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c CaseType)
    $cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c CaseType)
    dataTypeOf :: CaseType -> DataType
    $cdataTypeOf :: CaseType -> DataType
    toConstr :: CaseType -> Constr
    $ctoConstr :: CaseType -> Constr
    gunfold :: forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c CaseType
    $cgunfold :: forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c CaseType
    gfoldl :: forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> CaseType -> c CaseType
    $cgfoldl :: forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> CaseType -> c CaseType
    Data, Int -> CaseType -> ShowS
    [CaseType] -> ShowS
    CaseType -> String
    (Int -> CaseType -> ShowS)
    -> (CaseType -> String) -> ([CaseType] -> ShowS) -> Show CaseType
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    showList :: [CaseType] -> ShowS
    $cshowList :: [CaseType] -> ShowS
    show :: CaseType -> String
    $cshow :: CaseType -> String
    showsPrec :: Int -> CaseType -> ShowS
    $cshowsPrec :: Int -> CaseType -> ShowS
    Show, CaseType -> CaseType -> Bool
    (CaseType -> CaseType -> Bool)
    -> (CaseType -> CaseType -> Bool) -> Eq CaseType
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    /= :: CaseType -> CaseType -> Bool
    $c/= :: CaseType -> CaseType -> Bool
    == :: CaseType -> CaseType -> Bool
    $c== :: CaseType -> CaseType -> Bool
    Eq, Eq CaseType
    Eq CaseType
    -> (CaseType -> CaseType -> Ordering)
    -> (CaseType -> CaseType -> Bool)
    -> (CaseType -> CaseType -> Bool)
    -> (CaseType -> CaseType -> Bool)
    -> (CaseType -> CaseType -> Bool)
    -> (CaseType -> CaseType -> CaseType)
    -> (CaseType -> CaseType -> CaseType)
    -> Ord CaseType
    CaseType -> CaseType -> Bool
    CaseType -> CaseType -> Ordering
    CaseType -> CaseType -> CaseType
    forall a.
    Eq a
    -> (a -> a -> Ordering)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> Ord a
    min :: CaseType -> CaseType -> CaseType
    $cmin :: CaseType -> CaseType -> CaseType
    max :: CaseType -> CaseType -> CaseType
    $cmax :: CaseType -> CaseType -> CaseType
    >= :: CaseType -> CaseType -> Bool
    $c>= :: CaseType -> CaseType -> Bool
    > :: CaseType -> CaseType -> Bool
    $c> :: CaseType -> CaseType -> Bool
    <= :: CaseType -> CaseType -> Bool
    $c<= :: CaseType -> CaseType -> Bool
    < :: CaseType -> CaseType -> Bool
    $c< :: CaseType -> CaseType -> Bool
    compare :: CaseType -> CaseType -> Ordering
    $ccompare :: CaseType -> CaseType -> Ordering
    Ord, (forall x. CaseType -> Rep CaseType x)
    -> (forall x. Rep CaseType x -> CaseType) -> Generic CaseType
    forall x. Rep CaseType x -> CaseType
    forall x. CaseType -> Rep CaseType x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cto :: forall x. Rep CaseType x -> CaseType
    $cfrom :: forall x. CaseType -> Rep CaseType x
    Generic)

    data CaseInfo = CaseInfo
      { CaseInfo -> Bool
    caseLazy :: Bool
      , CaseInfo -> CaseType
    caseType :: CaseType }
      deriving (Typeable CaseInfo
    Typeable CaseInfo
    -> (forall (c :: * -> *).
        (forall d b. Data d => c (d -> b) -> d -> c b)
        -> (forall g. g -> c g) -> CaseInfo -> c CaseInfo)
    -> (forall (c :: * -> *).
        (forall b r. Data b => c (b -> r) -> c r)
        -> (forall r. r -> c r) -> Constr -> c CaseInfo)
    -> (CaseInfo -> Constr)
    -> (CaseInfo -> DataType)
    -> (forall (t :: * -> *) (c :: * -> *).
        Typeable t =>
        (forall d. Data d => c (t d)) -> Maybe (c CaseInfo))
    -> (forall (t :: * -> * -> *) (c :: * -> *).
        Typeable t =>
        (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c CaseInfo))
    -> ((forall b. Data b => b -> b) -> CaseInfo -> CaseInfo)
    -> (forall r r'.
        (r -> r' -> r)
        -> r -> (forall d. Data d => d -> r') -> CaseInfo -> r)
    -> (forall r r'.
        (r' -> r -> r)
        -> r -> (forall d. Data d => d -> r') -> CaseInfo -> r)
    -> (forall u. (forall d. Data d => d -> u) -> CaseInfo -> [u])
    -> (forall u. Int -> (forall d. Data d => d -> u) -> CaseInfo -> u)
    -> (forall (m :: * -> *).
        Monad m =>
        (forall d. Data d => d -> m d) -> CaseInfo -> m CaseInfo)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> CaseInfo -> m CaseInfo)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> CaseInfo -> m CaseInfo)
    -> Data CaseInfo
    CaseInfo -> DataType
    CaseInfo -> Constr
    (forall b. Data b => b -> b) -> CaseInfo -> CaseInfo
    forall a.
    Typeable a
    -> (forall (c :: * -> *).
        (forall d b. Data d => c (d -> b) -> d -> c b)
        -> (forall g. g -> c g) -> a -> c a)
    -> (forall (c :: * -> *).
        (forall b r. Data b => c (b -> r) -> c r)
        -> (forall r. r -> c r) -> Constr -> c a)
    -> (a -> Constr)
    -> (a -> DataType)
    -> (forall (t :: * -> *) (c :: * -> *).
        Typeable t =>
        (forall d. Data d => c (t d)) -> Maybe (c a))
    -> (forall (t :: * -> * -> *) (c :: * -> *).
        Typeable t =>
        (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
    -> ((forall b. Data b => b -> b) -> a -> a)
    -> (forall r r'.
        (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
    -> (forall r r'.
        (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
    -> (forall u. (forall d. Data d => d -> u) -> a -> [u])
    -> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
    -> (forall (m :: * -> *).
        Monad m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> Data a
    forall u. Int -> (forall d. Data d => d -> u) -> CaseInfo -> u
    forall u. (forall d. Data d => d -> u) -> CaseInfo -> [u]
    forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> CaseInfo -> r
    forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> CaseInfo -> r
    forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> CaseInfo -> m CaseInfo
    forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> CaseInfo -> m CaseInfo
    forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c CaseInfo
    forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> CaseInfo -> c CaseInfo
    forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c CaseInfo)
    forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c CaseInfo)
    gmapMo :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> CaseInfo -> m CaseInfo
    $cgmapMo :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> CaseInfo -> m CaseInfo
    gmapMp :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> CaseInfo -> m CaseInfo
    $cgmapMp :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> CaseInfo -> m CaseInfo
    gmapM :: forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> CaseInfo -> m CaseInfo
    $cgmapM :: forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> CaseInfo -> m CaseInfo
    gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> CaseInfo -> u
    $cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> CaseInfo -> u
    gmapQ :: forall u. (forall d. Data d => d -> u) -> CaseInfo -> [u]
    $cgmapQ :: forall u. (forall d. Data d => d -> u) -> CaseInfo -> [u]
    gmapQr :: forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> CaseInfo -> r
    $cgmapQr :: forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> CaseInfo -> r
    gmapQl :: forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> CaseInfo -> r
    $cgmapQl :: forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> CaseInfo -> r
    gmapT :: (forall b. Data b => b -> b) -> CaseInfo -> CaseInfo
    $cgmapT :: (forall b. Data b => b -> b) -> CaseInfo -> CaseInfo
    dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c CaseInfo)
    $cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c CaseInfo)
    dataCast1 :: forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c CaseInfo)
    $cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c CaseInfo)
    dataTypeOf :: CaseInfo -> DataType
    $cdataTypeOf :: CaseInfo -> DataType
    toConstr :: CaseInfo -> Constr
    $ctoConstr :: CaseInfo -> Constr
    gunfold :: forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c CaseInfo
    $cgunfold :: forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c CaseInfo
    gfoldl :: forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> CaseInfo -> c CaseInfo
    $cgfoldl :: forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> CaseInfo -> c CaseInfo
    Data, Int -> CaseInfo -> ShowS
    [CaseInfo] -> ShowS
    CaseInfo -> String
    (Int -> CaseInfo -> ShowS)
    -> (CaseInfo -> String) -> ([CaseInfo] -> ShowS) -> Show CaseInfo
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    showList :: [CaseInfo] -> ShowS
    $cshowList :: [CaseInfo] -> ShowS
    show :: CaseInfo -> String
    $cshow :: CaseInfo -> String
    showsPrec :: Int -> CaseInfo -> ShowS
    $cshowsPrec :: Int -> CaseInfo -> ShowS
    Show, CaseInfo -> CaseInfo -> Bool
    (CaseInfo -> CaseInfo -> Bool)
    -> (CaseInfo -> CaseInfo -> Bool) -> Eq CaseInfo
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    /= :: CaseInfo -> CaseInfo -> Bool
    $c/= :: CaseInfo -> CaseInfo -> Bool
    == :: CaseInfo -> CaseInfo -> Bool
    $c== :: CaseInfo -> CaseInfo -> Bool
    Eq, Eq CaseInfo
    Eq CaseInfo
    -> (CaseInfo -> CaseInfo -> Ordering)
    -> (CaseInfo -> CaseInfo -> Bool)
    -> (CaseInfo -> CaseInfo -> Bool)
    -> (CaseInfo -> CaseInfo -> Bool)
    -> (CaseInfo -> CaseInfo -> Bool)
    -> (CaseInfo -> CaseInfo -> CaseInfo)
    -> (CaseInfo -> CaseInfo -> CaseInfo)
    -> Ord CaseInfo
    CaseInfo -> CaseInfo -> Bool
    CaseInfo -> CaseInfo -> Ordering
    CaseInfo -> CaseInfo -> CaseInfo
    forall a.
    Eq a
    -> (a -> a -> Ordering)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> Ord a
    min :: CaseInfo -> CaseInfo -> CaseInfo
    $cmin :: CaseInfo -> CaseInfo -> CaseInfo
    max :: CaseInfo -> CaseInfo -> CaseInfo
    $cmax :: CaseInfo -> CaseInfo -> CaseInfo
    >= :: CaseInfo -> CaseInfo -> Bool
    $c>= :: CaseInfo -> CaseInfo -> Bool
    > :: CaseInfo -> CaseInfo -> Bool
    $c> :: CaseInfo -> CaseInfo -> Bool
    <= :: CaseInfo -> CaseInfo -> Bool
    $c<= :: CaseInfo -> CaseInfo -> Bool
    < :: CaseInfo -> CaseInfo -> Bool
    $c< :: CaseInfo -> CaseInfo -> Bool
    compare :: CaseInfo -> CaseInfo -> Ordering
    $ccompare :: CaseInfo -> CaseInfo -> Ordering
    Ord, (forall x. CaseInfo -> Rep CaseInfo x)
    -> (forall x. Rep CaseInfo x -> CaseInfo) -> Generic CaseInfo
    forall x. Rep CaseInfo x -> CaseInfo
    forall x. CaseInfo -> Rep CaseInfo x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cto :: forall x. Rep CaseInfo x -> CaseInfo
    $cfrom :: forall x. CaseInfo -> Rep CaseInfo x
    Generic)

    data TAlt
      = TACon    { TAlt -> QName
    aCon  :: QName, TAlt -> Int
    aArity :: Int, TAlt -> TTerm
    aBody :: TTerm }
      -- ^ Matches on the given constructor. If the match succeeds,
      -- the pattern variables are prepended to the current environment
      -- (pushes all existing variables aArity steps further away)
      | TAGuard  { TAlt -> TTerm
    aGuard :: TTerm, aBody :: TTerm }
      -- ^ Binds no variables
      | TALit    { TAlt -> Literal
    aLit :: Literal,   aBody:: TTerm }
      deriving (Typeable TAlt
    Typeable TAlt
    -> (forall (c :: * -> *).
        (forall d b. Data d => c (d -> b) -> d -> c b)
        -> (forall g. g -> c g) -> TAlt -> c TAlt)
    -> (forall (c :: * -> *).
        (forall b r. Data b => c (b -> r) -> c r)
        -> (forall r. r -> c r) -> Constr -> c TAlt)
    -> (TAlt -> Constr)
    -> (TAlt -> DataType)
    -> (forall (t :: * -> *) (c :: * -> *).
        Typeable t =>
        (forall d. Data d => c (t d)) -> Maybe (c TAlt))
    -> (forall (t :: * -> * -> *) (c :: * -> *).
        Typeable t =>
        (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TAlt))
    -> ((forall b. Data b => b -> b) -> TAlt -> TAlt)
    -> (forall r r'.
        (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TAlt -> r)
    -> (forall r r'.
        (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TAlt -> r)
    -> (forall u. (forall d. Data d => d -> u) -> TAlt -> [u])
    -> (forall u. Int -> (forall d. Data d => d -> u) -> TAlt -> u)
    -> (forall (m :: * -> *).
        Monad m =>
        (forall d. Data d => d -> m d) -> TAlt -> m TAlt)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> TAlt -> m TAlt)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> TAlt -> m TAlt)
    -> Data TAlt
    TAlt -> DataType
    TAlt -> Constr
    (forall b. Data b => b -> b) -> TAlt -> TAlt
    forall a.
    Typeable a
    -> (forall (c :: * -> *).
        (forall d b. Data d => c (d -> b) -> d -> c b)
        -> (forall g. g -> c g) -> a -> c a)
    -> (forall (c :: * -> *).
        (forall b r. Data b => c (b -> r) -> c r)
        -> (forall r. r -> c r) -> Constr -> c a)
    -> (a -> Constr)
    -> (a -> DataType)
    -> (forall (t :: * -> *) (c :: * -> *).
        Typeable t =>
        (forall d. Data d => c (t d)) -> Maybe (c a))
    -> (forall (t :: * -> * -> *) (c :: * -> *).
        Typeable t =>
        (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
    -> ((forall b. Data b => b -> b) -> a -> a)
    -> (forall r r'.
        (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
    -> (forall r r'.
        (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
    -> (forall u. (forall d. Data d => d -> u) -> a -> [u])
    -> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
    -> (forall (m :: * -> *).
        Monad m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> Data a
    forall u. Int -> (forall d. Data d => d -> u) -> TAlt -> u
    forall u. (forall d. Data d => d -> u) -> TAlt -> [u]
    forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TAlt -> r
    forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TAlt -> r
    forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> TAlt -> m TAlt
    forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> TAlt -> m TAlt
    forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c TAlt
    forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> TAlt -> c TAlt
    forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c TAlt)
    forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TAlt)
    gmapMo :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> TAlt -> m TAlt
    $cgmapMo :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> TAlt -> m TAlt
    gmapMp :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> TAlt -> m TAlt
    $cgmapMp :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> TAlt -> m TAlt
    gmapM :: forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> TAlt -> m TAlt
    $cgmapM :: forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> TAlt -> m TAlt
    gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> TAlt -> u
    $cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> TAlt -> u
    gmapQ :: forall u. (forall d. Data d => d -> u) -> TAlt -> [u]
    $cgmapQ :: forall u. (forall d. Data d => d -> u) -> TAlt -> [u]
    gmapQr :: forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TAlt -> r
    $cgmapQr :: forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TAlt -> r
    gmapQl :: forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TAlt -> r
    $cgmapQl :: forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TAlt -> r
    gmapT :: (forall b. Data b => b -> b) -> TAlt -> TAlt
    $cgmapT :: (forall b. Data b => b -> b) -> TAlt -> TAlt
    dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TAlt)
    $cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TAlt)
    dataCast1 :: forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c TAlt)
    $cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c TAlt)
    dataTypeOf :: TAlt -> DataType
    $cdataTypeOf :: TAlt -> DataType
    toConstr :: TAlt -> Constr
    $ctoConstr :: TAlt -> Constr
    gunfold :: forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c TAlt
    $cgunfold :: forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c TAlt
    gfoldl :: forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> TAlt -> c TAlt
    $cgfoldl :: forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> TAlt -> c TAlt
    Data, Int -> TAlt -> ShowS
    [TAlt] -> ShowS
    TAlt -> String
    (Int -> TAlt -> ShowS)
    -> (TAlt -> String) -> ([TAlt] -> ShowS) -> Show TAlt
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    showList :: [TAlt] -> ShowS
    $cshowList :: [TAlt] -> ShowS
    show :: TAlt -> String
    $cshow :: TAlt -> String
    showsPrec :: Int -> TAlt -> ShowS
    $cshowsPrec :: Int -> TAlt -> ShowS
    Show, TAlt -> TAlt -> Bool
    (TAlt -> TAlt -> Bool) -> (TAlt -> TAlt -> Bool) -> Eq TAlt
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    /= :: TAlt -> TAlt -> Bool
    $c/= :: TAlt -> TAlt -> Bool
    == :: TAlt -> TAlt -> Bool
    $c== :: TAlt -> TAlt -> Bool
    Eq, Eq TAlt
    Eq TAlt
    -> (TAlt -> TAlt -> Ordering)
    -> (TAlt -> TAlt -> Bool)
    -> (TAlt -> TAlt -> Bool)
    -> (TAlt -> TAlt -> Bool)
    -> (TAlt -> TAlt -> Bool)
    -> (TAlt -> TAlt -> TAlt)
    -> (TAlt -> TAlt -> TAlt)
    -> Ord TAlt
    TAlt -> TAlt -> Bool
    TAlt -> TAlt -> Ordering
    TAlt -> TAlt -> TAlt
    forall a.
    Eq a
    -> (a -> a -> Ordering)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> Ord a
    min :: TAlt -> TAlt -> TAlt
    $cmin :: TAlt -> TAlt -> TAlt
    max :: TAlt -> TAlt -> TAlt
    $cmax :: TAlt -> TAlt -> TAlt
    >= :: TAlt -> TAlt -> Bool
    $c>= :: TAlt -> TAlt -> Bool
    > :: TAlt -> TAlt -> Bool
    $c> :: TAlt -> TAlt -> Bool
    <= :: TAlt -> TAlt -> Bool
    $c<= :: TAlt -> TAlt -> Bool
    < :: TAlt -> TAlt -> Bool
    $c< :: TAlt -> TAlt -> Bool
    compare :: TAlt -> TAlt -> Ordering
    $ccompare :: TAlt -> TAlt -> Ordering
    Ord, (forall x. TAlt -> Rep TAlt x)
    -> (forall x. Rep TAlt x -> TAlt) -> Generic TAlt
    forall x. Rep TAlt x -> TAlt
    forall x. TAlt -> Rep TAlt x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cto :: forall x. Rep TAlt x -> TAlt
    $cfrom :: forall x. TAlt -> Rep TAlt x
    Generic)

    data TError
      = TUnreachable
      -- ^ Code which is unreachable. E.g. absurd branches or missing case defaults.
      -- Runtime behaviour of unreachable code is undefined, but preferably
      -- the program will exit with an error message. The compiler is free
      -- to assume that this code is unreachable and to remove it.
      | TMeta String
      -- ^ Code which could not be obtained because of a hole in the program.
      -- This should throw a runtime error.
      -- The string gives some information about the meta variable that got compiled.
      deriving (Typeable TError
    Typeable TError
    -> (forall (c :: * -> *).
        (forall d b. Data d => c (d -> b) -> d -> c b)
        -> (forall g. g -> c g) -> TError -> c TError)
    -> (forall (c :: * -> *).
        (forall b r. Data b => c (b -> r) -> c r)
        -> (forall r. r -> c r) -> Constr -> c TError)
    -> (TError -> Constr)
    -> (TError -> DataType)
    -> (forall (t :: * -> *) (c :: * -> *).
        Typeable t =>
        (forall d. Data d => c (t d)) -> Maybe (c TError))
    -> (forall (t :: * -> * -> *) (c :: * -> *).
        Typeable t =>
        (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TError))
    -> ((forall b. Data b => b -> b) -> TError -> TError)
    -> (forall r r'.
        (r -> r' -> r)
        -> r -> (forall d. Data d => d -> r') -> TError -> r)
    -> (forall r r'.
        (r' -> r -> r)
        -> r -> (forall d. Data d => d -> r') -> TError -> r)
    -> (forall u. (forall d. Data d => d -> u) -> TError -> [u])
    -> (forall u. Int -> (forall d. Data d => d -> u) -> TError -> u)
    -> (forall (m :: * -> *).
        Monad m =>
        (forall d. Data d => d -> m d) -> TError -> m TError)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> TError -> m TError)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> TError -> m TError)
    -> Data TError
    TError -> DataType
    TError -> Constr
    (forall b. Data b => b -> b) -> TError -> TError
    forall a.
    Typeable a
    -> (forall (c :: * -> *).
        (forall d b. Data d => c (d -> b) -> d -> c b)
        -> (forall g. g -> c g) -> a -> c a)
    -> (forall (c :: * -> *).
        (forall b r. Data b => c (b -> r) -> c r)
        -> (forall r. r -> c r) -> Constr -> c a)
    -> (a -> Constr)
    -> (a -> DataType)
    -> (forall (t :: * -> *) (c :: * -> *).
        Typeable t =>
        (forall d. Data d => c (t d)) -> Maybe (c a))
    -> (forall (t :: * -> * -> *) (c :: * -> *).
        Typeable t =>
        (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
    -> ((forall b. Data b => b -> b) -> a -> a)
    -> (forall r r'.
        (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
    -> (forall r r'.
        (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
    -> (forall u. (forall d. Data d => d -> u) -> a -> [u])
    -> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
    -> (forall (m :: * -> *).
        Monad m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> Data a
    forall u. Int -> (forall d. Data d => d -> u) -> TError -> u
    forall u. (forall d. Data d => d -> u) -> TError -> [u]
    forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TError -> r
    forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TError -> r
    forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> TError -> m TError
    forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> TError -> m TError
    forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c TError
    forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> TError -> c TError
    forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c TError)
    forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TError)
    gmapMo :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> TError -> m TError
    $cgmapMo :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> TError -> m TError
    gmapMp :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> TError -> m TError
    $cgmapMp :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> TError -> m TError
    gmapM :: forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> TError -> m TError
    $cgmapM :: forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> TError -> m TError
    gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> TError -> u
    $cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> TError -> u
    gmapQ :: forall u. (forall d. Data d => d -> u) -> TError -> [u]
    $cgmapQ :: forall u. (forall d. Data d => d -> u) -> TError -> [u]
    gmapQr :: forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TError -> r
    $cgmapQr :: forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TError -> r
    gmapQl :: forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TError -> r
    $cgmapQl :: forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TError -> r
    gmapT :: (forall b. Data b => b -> b) -> TError -> TError
    $cgmapT :: (forall b. Data b => b -> b) -> TError -> TError
    dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TError)
    $cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TError)
    dataCast1 :: forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c TError)
    $cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c TError)
    dataTypeOf :: TError -> DataType
    $cdataTypeOf :: TError -> DataType
    toConstr :: TError -> Constr
    $ctoConstr :: TError -> Constr
    gunfold :: forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c TError
    $cgunfold :: forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c TError
    gfoldl :: forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> TError -> c TError
    $cgfoldl :: forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> TError -> c TError
    Data, Int -> TError -> ShowS
    [TError] -> ShowS
    TError -> String
    (Int -> TError -> ShowS)
    -> (TError -> String) -> ([TError] -> ShowS) -> Show TError
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    showList :: [TError] -> ShowS
    $cshowList :: [TError] -> ShowS
    show :: TError -> String
    $cshow :: TError -> String
    showsPrec :: Int -> TError -> ShowS
    $cshowsPrec :: Int -> TError -> ShowS
    Show, TError -> TError -> Bool
    (TError -> TError -> Bool)
    -> (TError -> TError -> Bool) -> Eq TError
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    /= :: TError -> TError -> Bool
    $c/= :: TError -> TError -> Bool
    == :: TError -> TError -> Bool
    $c== :: TError -> TError -> Bool
    Eq, Eq TError
    Eq TError
    -> (TError -> TError -> Ordering)
    -> (TError -> TError -> Bool)
    -> (TError -> TError -> Bool)
    -> (TError -> TError -> Bool)
    -> (TError -> TError -> Bool)
    -> (TError -> TError -> TError)
    -> (TError -> TError -> TError)
    -> Ord TError
    TError -> TError -> Bool
    TError -> TError -> Ordering
    TError -> TError -> TError
    forall a.
    Eq a
    -> (a -> a -> Ordering)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> Ord a
    min :: TError -> TError -> TError
    $cmin :: TError -> TError -> TError
    max :: TError -> TError -> TError
    $cmax :: TError -> TError -> TError
    >= :: TError -> TError -> Bool
    $c>= :: TError -> TError -> Bool
    > :: TError -> TError -> Bool
    $c> :: TError -> TError -> Bool
    <= :: TError -> TError -> Bool
    $c<= :: TError -> TError -> Bool
    < :: TError -> TError -> Bool
    $c< :: TError -> TError -> Bool
    compare :: TError -> TError -> Ordering
    $ccompare :: TError -> TError -> Ordering
    Ord, (forall x. TError -> Rep TError x)
    -> (forall x. Rep TError x -> TError) -> Generic TError
    forall x. Rep TError x -> TError
    forall x. TError -> Rep TError x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cto :: forall x. Rep TError x -> TError
    $cfrom :: forall x. TError -> Rep TError x
    Generic)

    class Unreachable a where
      -- | Checks if the given expression is unreachable or not.
      isUnreachable :: a -> Bool

    instance Unreachable TAlt where
      isUnreachable :: TAlt -> Bool
    isUnreachable = TTerm -> Bool
    forall a. Unreachable a => a -> Bool
    isUnreachable (TTerm -> Bool) -> (TAlt -> TTerm) -> TAlt -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . TAlt -> TTerm
    aBody

    instance Unreachable TTerm where
      isUnreachable :: TTerm -> Bool
    isUnreachable (TError TUnreachable{}) = Bool
    True
      isUnreachable (TLet TTerm
    _ TTerm
    b) = TTerm -> Bool
    forall a. Unreachable a => a -> Bool
    isUnreachable TTerm
    b
      isUnreachable TTerm
    _ = Bool
    False

    instance KillRange Compiled where
      killRange :: Compiled -> Compiled
    killRange Compiled
    c = Compiled
    c -- bogus, but not used anyway

    -- * Utilities for ArgUsage
    ---------------------------------------------------------------------------

    -- | @filterUsed used args@ drops those @args@ which are labelled
    -- @ArgUnused@ in list @used@.
    --
    -- Specification:
    --
    -- @
    --   filterUsed used args = [ a | (a, ArgUsed) <- zip args $ used ++ repeat ArgUsed ]
    -- @
    --
    -- Examples:
    --
    -- @
    --   filterUsed []                 == id
    --   filterUsed (repeat ArgUsed)   == id
    --   filterUsed (repeat ArgUnused) == const []
    -- @
    filterUsed :: [ArgUsage] -> [a] -> [a]
    filterUsed :: forall a. [ArgUsage] -> [a] -> [a]
    filterUsed = (([ArgUsage], [a]) -> [a]) -> [ArgUsage] -> [a] -> [a]
    forall a b c. ((a, b) -> c) -> a -> b -> c
    curry ((([ArgUsage], [a]) -> [a]) -> [ArgUsage] -> [a] -> [a])
    -> (([ArgUsage], [a]) -> [a]) -> [ArgUsage] -> [a] -> [a]
    forall a b. (a -> b) -> a -> b
    $ \case
      ([], [a]
    args) -> [a]
    args
      ([ArgUsage]
    _ , [])   -> []
      (ArgUsage
    ArgUsed   : [ArgUsage]
    used, a
    a : [a]
    args) -> a
    a a -> [a] -> [a]
    forall a. a -> [a] -> [a]
    : [ArgUsage] -> [a] -> [a]
    forall a. [ArgUsage] -> [a] -> [a]
    filterUsed [ArgUsage]
    used [a]
    args
      (ArgUsage
    ArgUnused : [ArgUsage]
    used, a
    a : [a]
    args) ->     [ArgUsage] -> [a] -> [a]
    forall a. [ArgUsage] -> [a] -> [a]
    filterUsed [ArgUsage]
    used [a]
    args

    -- NFData instances
    ---------------------------------------------------------------------------

    instance NFData Compiled
    instance NFData ArgUsage
    instance NFData TTerm
    instance NFData TPrim
    instance NFData CaseType
    instance NFData CaseInfo
    instance NFData TAlt
    instance NFData TError