    {-|
      Copyright  :  (C) 2015-2016, University of Twente,
                        2021-2024, QBayLogic B.V.
                        2022,      LumiGuide Fietsdetectie B.V.
      License    :  BSD2 (see the file LICENSE)
      Maintainer :  QBayLogic B.V. <devops@qbaylogic.com>

      The 'disjointExpressionConsolidation' transformation lifts applications of
      global binders out of alternatives of case-statements.

      e.g. It converts:

      > case x of
      >   A -> f 3 y
      >   B -> f x x
      >   C -> h x

      into:

      > let f_arg0 = case x of {A -> 3; B -> x}
      >     f_arg1 = case x of {A -> y; B -> x}
      >     f_out  = f f_arg0 f_arg1
      > in  case x of
      >       A -> f_out
      >       B -> f_out
      >       C -> h x
    -}

    {-# LANGUAGE CPP #-}
    {-# LANGUAGE OverloadedStrings #-}
    {-# LANGUAGE RecursiveDo #-}
    {-# LANGUAGE ViewPatterns #-}
    {-# LANGUAGE TemplateHaskell #-}
    {-# LANGUAGE MagicHash #-}

    module Clash.Normalize.Transformations.DEC
      ( disjointExpressionConsolidation
      ) where

    #if !MIN_VERSION_base(4,18,0)
    import Control.Applicative (liftA2)
    #endif
    import Control.Lens ((^.), _1)
    import qualified Control.Lens as Lens
    import qualified Control.Monad as Monad
    import Data.Bifunctor (first, second)
    import Data.Bits ((.&.), complement)
    import Data.Coerce (coerce)
    import qualified Data.Either as Either
    import qualified Data.Foldable as Foldable
    import qualified Data.Graph as Graph
    import Data.IntMap.Strict (IntMap)
    import qualified Data.IntMap.Strict as IntMap
    import qualified Data.List as List
    import qualified Data.List.Extra as List
    import qualified Data.Map.Strict as Map
    import qualified Data.Maybe as Maybe
    import Data.Monoid (All(..))
    import qualified Data.Text as Text
    import Data.Text.Extra (showt)
    import GHC.Stack (HasCallStack)
    import qualified Language.Haskell.TH as TH

    #if MIN_VERSION_ghc(9,6,0)
    import GHC.Core.Make (chunkify, mkChunkified)
    #elif MIN_VERSION_ghc(8,10,0)
    import GHC.Hs.Utils (chunkify, mkChunkified)
    #else
    import HsUtils (chunkify, mkChunkified)
    #endif

    #if MIN_VERSION_ghc(9,0,0)
    import GHC.Settings.Constants (mAX_TUPLE_SIZE)
    #else
    import Constants (mAX_TUPLE_SIZE)
    #endif

    -- internal
    import Clash.Core.DataCon (DataCon)
    import Clash.Core.Evaluator.Types  (whnf')
    import Clash.Core.FreeVars
      (termFreeVars', typeFreeVars', localVarsDoNotOccurIn)
    import Clash.Core.HasType
    import Clash.Core.Literal (Literal(..))
    import Clash.Core.Name (OccName, nameOcc)
    import Clash.Core.Pretty (showPpr)
    import Clash.Core.Term
      ( Alt, LetBinding, Pat(..), PrimInfo(..), Term(..), TickInfo(..)
      , collectArgs, collectArgsTicks, mkApps, mkTicks, patIds, stripTicks)
    import Clash.Core.TyCon (TyConMap, TyConName, tyConDataCons)
    import Clash.Core.Type
      (Type, TypeView (..), isPolyFunTy, mkTyConApp, splitFunForallTy, tyView)
    import Clash.Core.Util (mkInternalVar, mkSelectorCase, sccLetBindings)
    import Clash.Core.Var (Id, isGlobalId, isLocalId, varName)
    import Clash.Core.VarEnv
      ( InScopeSet, elemInScopeSet, extendInScopeSet, extendInScopeSetList
      , notElemInScopeSet, unionInScope)
    import qualified Clash.Data.UniqMap as UniqMap
    import Clash.Normalize.Transformations.Letrec (deadCode)
    import Clash.Normalize.Types (NormRewrite, NormalizeSession)
    import Clash.Rewrite.Combinators (bottomupR)
    import Clash.Rewrite.Types
    import Clash.Rewrite.Util (changed, isFromInt, isUntranslatableType)
    import Clash.Rewrite.WorkFree (isConstant)
    import Clash.Util (MonadUnique, curLoc)
    import Clash.Util.Supply (splitSupply)

    -- primitives
    import qualified Clash.Sized.Internal.BitVector
    import qualified Clash.Sized.Internal.Index
    import qualified Clash.Sized.Internal.Signed
    import qualified Clash.Sized.Internal.Unsigned
    import qualified GHC.Base
    import qualified GHC.Classes
    #if MIN_VERSION_base(4,15,0)
    import qualified GHC.Num.Integer
    #else
    -- interger-gmp primitives are defined in the hidden module GHC.Integer.Type,
    -- but exported from GHC.Integer
    import qualified GHC.Integer as GHC.Integer.Type
    #endif
    import qualified GHC.Prim

    -- | This transformation lifts applications of global binders out of
    -- alternatives of case-statements.
    --
    -- e.g. It converts:
    --
    -- @
    -- case x of
    --   A -> f 3 y
    --   B -> f x x
    --   C -> h x
    -- @
    --
    -- into:
    --
    -- @
    -- let f_arg0 = case x of {A -> 3; B -> x}
    --     f_arg1 = case x of {A -> y; B -> x}
    --     f_out  = f f_arg0 f_arg1
    -- in  case x of
    --       A -> f_out
    --       B -> f_out
    --       C -> h x
    -- @
    --
    -- Though that's a lie. It actually converts it into:
    --
    -- @
    -- let f_tupIn = case x of {A -> (3,y); B -> (x,x)}
    --     f_arg0  = case f_tupIn of (l,_) -> l
    --     f_arg1  = case f_tupIn of (_,r) -> r
    --     f_out   = f f_arg0 f_arg1
    -- in  case x of
    --       A -> f_out
    --       B -> f_out
    --       C -> h x
    -- @
    --
    -- In order to share the expression that's in the subject of the case expression,
    -- and to share the /decoder/ circuit that logic synthesis will create to map the
    -- bits of the subject expression to the bits needed to make the selection in the
    -- multiplexer.
    disjointExpressionConsolidation :: HasCallStack => NormRewrite
    disjointExpressionConsolidation :: HasCallStack => NormRewrite
    disjointExpressionConsolidation ctx :: TransformContext
    ctx@(TransformContext InScopeSet
    isCtx Context
    _) e :: Term
    e@(Case Term
    _scrut Type
    _ty _alts :: [Alt]
    _alts@(Alt
    _:Alt
    _:[Alt]
    _)) = do
        -- Collect all (the applications of) global binders (and certain primitives)
        -- that would be interesting to share out of the case-alternatives.
        (_,isCollected,collected) <- InScopeSet
    -> [(Term, Term)]
    -> [Term]
    -> Term
    -> NormalizeSession
         (Term, InScopeSet, [(Term, ([Term], CaseTree [Either Term Type]))])
    collectGlobals InScopeSet
    isCtx [] [] Term
    e
        -- Filter those that are used at most once in every (nested) branch.
        let disJoint = ((Term, ([Term], CaseTree [Either Term Type])) -> Bool)
    -> [(Term, ([Term], CaseTree [Either Term Type]))]
    -> [(Term, ([Term], CaseTree [Either Term Type]))]
    forall a. (a -> Bool) -> [a] -> [a]
    filter (CaseTree [Either Term Type] -> Bool
    isDisjoint (CaseTree [Either Term Type] -> Bool)
    -> ((Term, ([Term], CaseTree [Either Term Type]))
        -> CaseTree [Either Term Type])
    -> (Term, ([Term], CaseTree [Either Term Type]))
    -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ([Term], CaseTree [Either Term Type])
    -> CaseTree [Either Term Type]
    forall a b. (a, b) -> b
    snd (([Term], CaseTree [Either Term Type])
     -> CaseTree [Either Term Type])
    -> ((Term, ([Term], CaseTree [Either Term Type]))
        -> ([Term], CaseTree [Either Term Type]))
    -> (Term, ([Term], CaseTree [Either Term Type]))
    -> CaseTree [Either Term Type]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Term, ([Term], CaseTree [Either Term Type]))
    -> ([Term], CaseTree [Either Term Type])
    forall a b. (a, b) -> b
    snd) [(Term, ([Term], CaseTree [Either Term Type]))]
    collected
        if null disJoint
           then return e
           else do
             -- For every to-lift expression create (the generalization of):
             --
             -- let f_tupIn = case x of {A -> (3,y); B -> (x,x)}
             --     f_arg0  = case f_tupIn of (l,_) -> l
             --     f_arg1  = case f_tupIn of (_,r) -> r
             -- in  f f_arg0 f_arg0
             --
             -- if an argument is non-representable, the case-expression is inlined,
             -- and no let-binding will be created for it.
             --
             -- NB: mkDisJointGroup needs the context InScopeSet, isCtx, to determine
             -- whether expressions reference variables from the context, or
             -- variables inside a let-expression inside one of the alternatives.
             lifted <- mapM (mkDisjointGroup isCtx) disJoint
             tcm    <- Lens.view tcCache
             -- Create let-binders for all of the lifted expressions
             --
             -- NB: Because we will be substituting under binders we use the collected
             -- inScopeSet, isCollected, which also contains all the binders
             -- created inside all of the alternatives. With this inScopeSet, we
             -- ensure that the let-bindings we create here won't be accidentally
             -- captured by binders inside the case-alternatives.
             (_,funOutIds) <- List.mapAccumLM (mkFunOut tcm)
                                              isCollected
                                              (zip disJoint lifted)
             -- Create "substitutions" of the form [f X Y := f_out]
             let substitution = [Term] -> [Term] -> [(Term, Term)]
    forall a b. [a] -> [b] -> [(a, b)]
    zip (((Term, ([Term], CaseTree [Either Term Type])) -> Term)
    -> [(Term, ([Term], CaseTree [Either Term Type]))] -> [Term]
    forall a b. (a -> b) -> [a] -> [b]
    map (Term, ([Term], CaseTree [Either Term Type])) -> Term
    forall a b. (a, b) -> a
    fst [(Term, ([Term], CaseTree [Either Term Type]))]
    disJoint) ((Id -> Term) -> [Id] -> [Term]
    forall a b. (a -> b) -> [a] -> [b]
    map Id -> Term
    Var [Id]
    funOutIds)
             -- For all of the lifted expression: substitute occurrences of the
             -- disjoint expressions (f X Y) by a variable reference to the lifted
             -- expression (f_out)
             let isCtx1 = InScopeSet -> [Id] -> InScopeSet
    forall a. InScopeSet -> [Var a] -> InScopeSet
    extendInScopeSetList InScopeSet
    isCtx [Id]
    funOutIds
             lifted1 <- substLifted isCtx1 substitution lifted
             -- Do the same for the actual case expression
             (e1,_,_) <- collectGlobals isCtx1 substitution [] e
             -- Let-bind all the lifted function
             let lb = [LetBinding] -> Term -> Term
    Letrec ([Id] -> [Term] -> [LetBinding]
    forall a b. [a] -> [b] -> [(a, b)]
    zip [Id]
    funOutIds [Term]
    lifted1) Term
    e1
             -- Do an initial dead-code elimination pass, as `mkDisJoint` doesn't
             -- clean-up unused let-binders.
             lb1 <- bottomupR deadCode ctx lb
             changed lb1
      where
        -- Make the let-binder for the lifted expressions
        mkFunOut :: TyConMap -> InScopeSet -> ((Term, b), (a, b)) -> m (InScopeSet, Id)
    mkFunOut TyConMap
    tcm InScopeSet
    isN ((Term
    fun,b
    _),(a
    eLifted,b
    _)) = do
          let ty :: Type
    ty  = TyConMap -> a -> Type
    forall a. InferType a => TyConMap -> a -> Type
    inferCoreTypeOf TyConMap
    tcm a
    eLifted
              nm :: Text
    nm  = Term -> Text
    decFunName Term
    fun
              nm1 :: Text
    nm1 = Text
    nm Text -> Text -> Text
    `Text.append` Text
    "_out"
          nm2 <- InScopeSet -> Text -> Type -> m Id
    forall (m :: Type -> Type).
    MonadUnique m =>
    InScopeSet -> Text -> Type -> m Id
    mkInternalVar InScopeSet
    isN Text
    nm1 Type
    ty
          return (extendInScopeSet isN nm2,nm2)

        -- Substitute inside the lifted expressions
        --
        -- In case you are wondering why this function isn't simply
        --
        -- > mapM (\s (eL,seen) -> collectGlobal isN s seen eL) substitution lifted
        --
        -- then that's because we have e.g. the list of "substitutions":
        --
        -- [foo _ _ := foo_out; bar _ _ := bar_out]
        --
        -- and if we were to apply that to a lifted expression, which is going
        -- to be of the form `foo (case ...) (case ...)` then we would end up
        -- with let-bindings that are simply:
        --
        -- > let foo_out = foo_out ; bar_out = bar_out
        --
        -- instead of the desired
        --
        -- > let foo_out = foo ((case ...)[foo _ _ := foo_out; bar _ _ := bar_out])
        -- >                   ((case ...)[foo _ _ := foo_out; bar _ _ := bar_out])
        -- >     bar_out = bar ((case ...)[foo _ _ := foo_out; bar _ _ := bar_out])
        -- >                   ((case ...)[foo _ _ := foo_out; bar _ _ := bar_out])
        --
        -- So what we do is that for every lifted-expression we make sure that the
        -- 'substitution' never contains the self-substitution, so we end up with:
        --
        -- > let foo_out = (foo (case ...) (case ...))[bar _ _ := bar_out]
        --       bar_out = (bar (case ...) (case ...))[foo _ _ := foo_out]
        --
        -- We used to have a different approach, see commit
        -- 73d237017c4a5fff0c49bb72c9c4d5f6c68faf69
        --
        -- But that lead to the generation of combinational loops. Now that we no
        -- longer traverse into recursive groups of let-bindings, the issue #1316
        -- that the above commit tried to solve, no longer shows up.
        substLifted :: InScopeSet
    -> [(Term, Term)]
    -> [(Term, [Term])]
    -> RewriteMonad NormalizeState [Term]
    substLifted InScopeSet
    isN [(Term, Term)]
    substitution [(Term, [Term])]
    lifted = do
          -- remove the self-substitutions for the respective lifted expressions
          let subsMatrix :: [[(Term, Term)]]
    subsMatrix = [(Term, Term)] -> [[(Term, Term)]]
    forall {a}. [a] -> [[a]]
    l2m [(Term, Term)]
    substitution
          lifted1 <- ([(Term, Term)]
     -> (Term, [Term])
     -> NormalizeSession
          (Term, InScopeSet,
           [(Term, ([Term], CaseTree [Either Term Type]))]))
    -> [[(Term, Term)]]
    -> [(Term, [Term])]
    -> RewriteMonad
         NormalizeState
         [(Term, InScopeSet,
           [(Term, ([Term], CaseTree [Either Term Type]))])]
    forall (m :: Type -> Type) a b c.
    Applicative m =>
    (a -> b -> m c) -> [a] -> [b] -> m [c]
    Monad.zipWithM (\[(Term, Term)]
    s (Term
    eL,[Term]
    seen) -> InScopeSet
    -> [(Term, Term)]
    -> [Term]
    -> Term
    -> NormalizeSession
         (Term, InScopeSet, [(Term, ([Term], CaseTree [Either Term Type]))])
    collectGlobals InScopeSet
    isN [(Term, Term)]
    s [Term]
    seen Term
    eL)
                                     [[(Term, Term)]]
    subsMatrix
                                     [(Term, [Term])]
    lifted
          return (map (^. _1) lifted1)

        l2m :: [a] -> [[a]]
    l2m = [a] -> [a] -> [[a]]
    forall {a}. [a] -> [a] -> [[a]]
    go []
         where
          go :: [a] -> [a] -> [[a]]
    go [a]
    _  []     = []
          go [a]
    xs (a
    y:[a]
    ys) = ([a]
    xs [a] -> [a] -> [a]
    forall a. [a] -> [a] -> [a]
    ++ [a]
    ys) [a] -> [[a]] -> [[a]]
    forall a. a -> [a] -> [a]
    : [a] -> [a] -> [[a]]
    go ([a]
    xs [a] -> [a] -> [a]
    forall a. [a] -> [a] -> [a]
    ++ [a
    y]) [a]
    ys

    disjointExpressionConsolidation TransformContext
    _ Term
    e = Term -> RewriteMonad NormalizeState Term
    forall a. a -> RewriteMonad NormalizeState a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return Term
    e
    {-# SCC disjointExpressionConsolidation #-}

    decFunName :: Term -> OccName
    decFunName :: Term -> Text
    decFunName Term
    fun = [Text] -> Text
    forall a. HasCallStack => [a] -> a
    last ([Text] -> Text) -> (Text -> [Text]) -> Text -> Text
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . HasCallStack => Text -> Text -> [Text]
    Text -> Text -> [Text]
    Text.splitOn Text
    "." (Text -> Text) -> Text -> Text
    forall a b. (a -> b) -> a -> b
    $ case Term -> (Term, [Either Term Type])
    collectArgs Term
    fun of
      (Var Id
    v, [Either Term Type]
    _) -> Name Term -> Text
    forall a. Name a -> Text
    nameOcc (Id -> Name Term
    forall a. Var a -> Name a
    varName Id
    v)
      (Prim PrimInfo
    p, [Either Term Type]
    _) -> PrimInfo -> Text
    primName PrimInfo
    p
      (Term, [Either Term Type])
    _ -> Text
    "complex_expression"

    data CaseTree a
      = Leaf a
      | LB [LetBinding] (CaseTree a)
      | Branch Term [(Pat,CaseTree a)]
      deriving (CaseTree a -> CaseTree a -> Bool
    (CaseTree a -> CaseTree a -> Bool)
    -> (CaseTree a -> CaseTree a -> Bool) -> Eq (CaseTree a)
    forall a. Eq a => CaseTree a -> CaseTree a -> Bool
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: forall a. Eq a => CaseTree a -> CaseTree a -> Bool
    == :: CaseTree a -> CaseTree a -> Bool
    $c/= :: forall a. Eq a => CaseTree a -> CaseTree a -> Bool
    /= :: CaseTree a -> CaseTree a -> Bool
    Eq,Int -> CaseTree a -> ShowS
    [CaseTree a] -> ShowS
    CaseTree a -> [Char]
    (Int -> CaseTree a -> ShowS)
    -> (CaseTree a -> [Char])
    -> ([CaseTree a] -> ShowS)
    -> Show (CaseTree a)
    forall a. Show a => Int -> CaseTree a -> ShowS
    forall a. Show a => [CaseTree a] -> ShowS
    forall a. Show a => CaseTree a -> [Char]
    forall a.
    (Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: forall a. Show a => Int -> CaseTree a -> ShowS
    showsPrec :: Int -> CaseTree a -> ShowS
    $cshow :: forall a. Show a => CaseTree a -> [Char]
    show :: CaseTree a -> [Char]
    $cshowList :: forall a. Show a => [CaseTree a] -> ShowS
    showList :: [CaseTree a] -> ShowS
    Show,(forall a b. (a -> b) -> CaseTree a -> CaseTree b)
    -> (forall a b. a -> CaseTree b -> CaseTree a) -> Functor CaseTree
    forall a b. a -> CaseTree b -> CaseTree a
    forall a b. (a -> b) -> CaseTree a -> CaseTree b
    forall (f :: Type -> Type).
    (forall a b. (a -> b) -> f a -> f b)
    -> (forall a b. a -> f b -> f a) -> Functor f
    $cfmap :: forall a b. (a -> b) -> CaseTree a -> CaseTree b
    fmap :: forall a b. (a -> b) -> CaseTree a -> CaseTree b
    $c<$ :: forall a b. a -> CaseTree b -> CaseTree a
    <$ :: forall a b. a -> CaseTree b -> CaseTree a
    Functor,(forall m. Monoid m => CaseTree m -> m)
    -> (forall m a. Monoid m => (a -> m) -> CaseTree a -> m)
    -> (forall m a. Monoid m => (a -> m) -> CaseTree a -> m)
    -> (forall a b. (a -> b -> b) -> b -> CaseTree a -> b)
    -> (forall a b. (a -> b -> b) -> b -> CaseTree a -> b)
    -> (forall b a. (b -> a -> b) -> b -> CaseTree a -> b)
    -> (forall b a. (b -> a -> b) -> b -> CaseTree a -> b)
    -> (forall a. (a -> a -> a) -> CaseTree a -> a)
    -> (forall a. (a -> a -> a) -> CaseTree a -> a)
    -> (forall a. CaseTree a -> [a])
    -> (forall a. CaseTree a -> Bool)
    -> (forall a. CaseTree a -> Int)
    -> (forall a. Eq a => a -> CaseTree a -> Bool)
    -> (forall a. Ord a => CaseTree a -> a)
    -> (forall a. Ord a => CaseTree a -> a)
    -> (forall a. Num a => CaseTree a -> a)
    -> (forall a. Num a => CaseTree a -> a)
    -> Foldable CaseTree
    forall a. Eq a => a -> CaseTree a -> Bool
    forall a. Num a => CaseTree a -> a
    forall a. Ord a => CaseTree a -> a
    forall m. Monoid m => CaseTree m -> m
    forall a. CaseTree a -> Bool
    forall a. CaseTree a -> Int
    forall a. CaseTree a -> [a]
    forall a. (a -> a -> a) -> CaseTree a -> a
    forall m a. Monoid m => (a -> m) -> CaseTree a -> m
    forall b a. (b -> a -> b) -> b -> CaseTree a -> b
    forall a b. (a -> b -> b) -> b -> CaseTree a -> b
    forall (t :: Type -> Type).
    (forall m. Monoid m => t m -> m)
    -> (forall m a. Monoid m => (a -> m) -> t a -> m)
    -> (forall m a. Monoid m => (a -> m) -> t a -> m)
    -> (forall a b. (a -> b -> b) -> b -> t a -> b)
    -> (forall a b. (a -> b -> b) -> b -> t a -> b)
    -> (forall b a. (b -> a -> b) -> b -> t a -> b)
    -> (forall b a. (b -> a -> b) -> b -> t a -> b)
    -> (forall a. (a -> a -> a) -> t a -> a)
    -> (forall a. (a -> a -> a) -> t a -> a)
    -> (forall a. t a -> [a])
    -> (forall a. t a -> Bool)
    -> (forall a. t a -> Int)
    -> (forall a. Eq a => a -> t a -> Bool)
    -> (forall a. Ord a => t a -> a)
    -> (forall a. Ord a => t a -> a)
    -> (forall a. Num a => t a -> a)
    -> (forall a. Num a => t a -> a)
    -> Foldable t
    $cfold :: forall m. Monoid m => CaseTree m -> m
    fold :: forall m. Monoid m => CaseTree m -> m
    $cfoldMap :: forall m a. Monoid m => (a -> m) -> CaseTree a -> m
    foldMap :: forall m a. Monoid m => (a -> m) -> CaseTree a -> m
    $cfoldMap' :: forall m a. Monoid m => (a -> m) -> CaseTree a -> m
    foldMap' :: forall m a. Monoid m => (a -> m) -> CaseTree a -> m
    $cfoldr :: forall a b. (a -> b -> b) -> b -> CaseTree a -> b
    foldr :: forall a b. (a -> b -> b) -> b -> CaseTree a -> b
    $cfoldr' :: forall a b. (a -> b -> b) -> b -> CaseTree a -> b
    foldr' :: forall a b. (a -> b -> b) -> b -> CaseTree a -> b
    $cfoldl :: forall b a. (b -> a -> b) -> b -> CaseTree a -> b
    foldl :: forall b a. (b -> a -> b) -> b -> CaseTree a -> b
    $cfoldl' :: forall b a. (b -> a -> b) -> b -> CaseTree a -> b
    foldl' :: forall b a. (b -> a -> b) -> b -> CaseTree a -> b
    $cfoldr1 :: forall a. (a -> a -> a) -> CaseTree a -> a
    foldr1 :: forall a. (a -> a -> a) -> CaseTree a -> a
    $cfoldl1 :: forall a. (a -> a -> a) -> CaseTree a -> a
    foldl1 :: forall a. (a -> a -> a) -> CaseTree a -> a
    $ctoList :: forall a. CaseTree a -> [a]
    toList :: forall a. CaseTree a -> [a]
    $cnull :: forall a. CaseTree a -> Bool
    null :: forall a. CaseTree a -> Bool
    $clength :: forall a. CaseTree a -> Int
    length :: forall a. CaseTree a -> Int
    $celem :: forall a. Eq a => a -> CaseTree a -> Bool
    elem :: forall a. Eq a => a -> CaseTree a -> Bool
    $cmaximum :: forall a. Ord a => CaseTree a -> a
    maximum :: forall a. Ord a => CaseTree a -> a
    $cminimum :: forall a. Ord a => CaseTree a -> a
    minimum :: forall a. Ord a => CaseTree a -> a
    $csum :: forall a. Num a => CaseTree a -> a
    sum :: forall a. Num a => CaseTree a -> a
    $cproduct :: forall a. Num a => CaseTree a -> a
    product :: forall a. Num a => CaseTree a -> a
    Foldable)

    instance Applicative CaseTree where
      pure :: forall a. a -> CaseTree a
    pure = a -> CaseTree a
    forall a. a -> CaseTree a
    Leaf
      liftA2 :: forall a b c.
    (a -> b -> c) -> CaseTree a -> CaseTree b -> CaseTree c
    liftA2 a -> b -> c
    f (Leaf a
    a) (Leaf b
    b) = c -> CaseTree c
    forall a. a -> CaseTree a
    Leaf (a -> b -> c
    f a
    a b
    b)
      liftA2 a -> b -> c
    f (LB [LetBinding]
    lb CaseTree a
    c1) (LB [LetBinding]
    _ CaseTree b
    c2) = [LetBinding] -> CaseTree c -> CaseTree c
    forall a. [LetBinding] -> CaseTree a -> CaseTree a
    LB [LetBinding]
    lb ((a -> b -> c) -> CaseTree a -> CaseTree b -> CaseTree c
    forall a b c.
    (a -> b -> c) -> CaseTree a -> CaseTree b -> CaseTree c
    forall (f :: Type -> Type) a b c.
    Applicative f =>
    (a -> b -> c) -> f a -> f b -> f c
    liftA2 a -> b -> c
    f CaseTree a
    c1 CaseTree b
    c2)
      liftA2 a -> b -> c
    f (Branch Term
    scrut [(Pat, CaseTree a)]
    alts1) (Branch Term
    _ [(Pat, CaseTree b)]
    alts2) =
        Term -> [(Pat, CaseTree c)] -> CaseTree c
    forall a. Term -> [(Pat, CaseTree a)] -> CaseTree a
    Branch Term
    scrut (((Pat, CaseTree a) -> (Pat, CaseTree b) -> (Pat, CaseTree c))
    -> [(Pat, CaseTree a)]
    -> [(Pat, CaseTree b)]
    -> [(Pat, CaseTree c)]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith (\(Pat
    p1,CaseTree a
    a1) (Pat
    _,CaseTree b
    a2) -> (Pat
    p1,(a -> b -> c) -> CaseTree a -> CaseTree b -> CaseTree c
    forall a b c.
    (a -> b -> c) -> CaseTree a -> CaseTree b -> CaseTree c
    forall (f :: Type -> Type) a b c.
    Applicative f =>
    (a -> b -> c) -> f a -> f b -> f c
    liftA2 a -> b -> c
    f CaseTree a
    a1 CaseTree b
    a2)) [(Pat, CaseTree a)]
    alts1 [(Pat, CaseTree b)]
    alts2)
      liftA2 a -> b -> c
    _ CaseTree a
    _ CaseTree b
    _ = [Char] -> CaseTree c
    forall a. HasCallStack => [Char] -> a
    error [Char]
    "CaseTree.liftA2: internal error, this should not happen."

    -- | Test if a 'CaseTree' collected from an expression indicates that
    -- application of a global binder is disjoint: occur in separate branches of a
    -- case-expression.
    isDisjoint :: CaseTree ([Either Term Type])
               -> Bool
    isDisjoint :: CaseTree [Either Term Type] -> Bool
    isDisjoint (Branch Term
    _ [(Pat, CaseTree [Either Term Type])
    _]) = Bool
    False
    isDisjoint CaseTree [Either Term Type]
    ct = CaseTree [Either Term Type] -> Bool
    forall {b} {a}. Eq b => CaseTree [Either a b] -> Bool
    go CaseTree [Either Term Type]
    ct
      where
        go :: CaseTree [Either a b] -> Bool
    go (Leaf [Either a b]
    _)             = Bool
    False
        go (LB [LetBinding]
    _ CaseTree [Either a b]
    ct')           = CaseTree [Either a b] -> Bool
    go CaseTree [Either a b]
    ct'
        go (Branch Term
    _ [])        = Bool
    False
        go (Branch Term
    _ [(Pat
    _,CaseTree [Either a b]
    x)])   = CaseTree [Either a b] -> Bool
    go CaseTree [Either a b]
    x
        go b :: CaseTree [Either a b]
    b@(Branch Term
    _ ((Pat, CaseTree [Either a b])
    _:(Pat, CaseTree [Either a b])
    _:[(Pat, CaseTree [Either a b])]
    _)) = [[b]] -> Bool
    forall a. Eq a => [a] -> Bool
    allEqual (([Either a b] -> [b]) -> [[Either a b]] -> [[b]]
    forall a b. (a -> b) -> [a] -> [b]
    map [Either a b] -> [b]
    forall a b. [Either a b] -> [b]
    Either.rights (CaseTree [Either a b] -> [[Either a b]]
    forall a. CaseTree a -> [a]
    forall (t :: Type -> Type) a. Foldable t => t a -> [a]
    Foldable.toList CaseTree [Either a b]
    b))

    -- | Test if all elements in a list are equal to each other.
    allEqual :: Eq a => [a] -> Bool
    allEqual :: forall a. Eq a => [a] -> Bool
    allEqual []     = Bool
    True
    allEqual (a
    x:[a]
    xs) = (a -> Bool) -> [a] -> Bool
    forall (t :: Type -> Type) a.
    Foldable t =>
    (a -> Bool) -> t a -> Bool
    all (a -> a -> Bool
    forall a. Eq a => a -> a -> Bool
    == a
    x) [a]
    xs

    -- | Collect 'CaseTree's for (potentially) disjoint applications of globals out
    -- of an expression. Also substitute truly disjoint applications of globals by a
    -- reference to a lifted out application.
    collectGlobals
      :: InScopeSet
      -> [(Term,Term)]
      -- ^ Substitution of (applications of) a global binder by a reference to a
      -- lifted term.
      -> [Term]
      -- ^ List of already seen global binders
      -> Term
      -- ^ The expression
      -> NormalizeSession (Term, InScopeSet, [(Term, ([Term], CaseTree [Either Term Type]))])
    collectGlobals :: InScopeSet
    -> [(Term, Term)]
    -> [Term]
    -> Term
    -> NormalizeSession
         (Term, InScopeSet, [(Term, ([Term], CaseTree [Either Term Type]))])
    collectGlobals InScopeSet
    is0 [(Term, Term)]
    substitution [Term]
    seen (Case Term
    scrut Type
    ty [Alt]
    alts) = do
      rec (alts1, isAlts, collectedAlts) <-
            collectGlobalsAlts is0 substitution seen scrut1 alts
          (scrut1, isScrut, collectedScrut) <-
            collectGlobals is0 substitution (map fst collectedAlts ++ seen) scrut
      return ( Case scrut1 ty alts1
             , unionInScope isAlts isScrut
             , collectedAlts ++ collectedScrut )

    collectGlobals InScopeSet
    is0 [(Term, Term)]
    substitution [Term]
    seen e :: Term
    e@(Term -> (Term, [Either Term Type], [TickInfo])
    collectArgsTicks -> (Term
    fun, args :: [Either Term Type]
    args@(Either Term Type
    _:[Either Term Type]
    _), [TickInfo]
    ticks))
      | Bool -> Bool
    not (Term -> Bool
    isConstant Term
    e) = do
        tcm <- Getting TyConMap RewriteEnv TyConMap
    -> RewriteMonad NormalizeState TyConMap
    forall s (m :: Type -> Type) a.
    MonadReader s m =>
    Getting a s a -> m a
    Lens.view Getting TyConMap RewriteEnv TyConMap
    Getter RewriteEnv TyConMap
    tcCache
        bndrs <- Lens.use bindings
        evaluate <- Lens.view evaluator
        ids <- Lens.use uniqSupply
        let (ids1,ids2) = splitSupply ids
        uniqSupply Lens..= ids2
        gh <- Lens.use globalHeap
        let eval = (Getting Term (PrimHeap, PureHeap, Term) Term
    -> (PrimHeap, PureHeap, Term) -> Term
    forall s (m :: Type -> Type) a.
    MonadReader s m =>
    Getting a s a -> m a
    Lens.view Getting Term (PrimHeap, PureHeap, Term) Term
    forall s t a b. Field3 s t a b => Lens s t a b
    Lens
      (PrimHeap, PureHeap, Term) (PrimHeap, PureHeap, Term) Term Term
    Lens._3) ((PrimHeap, PureHeap, Term) -> Term)
    -> (Term -> (PrimHeap, PureHeap, Term)) -> Term -> Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Evaluator
    -> BindingMap
    -> PureHeap
    -> TyConMap
    -> PrimHeap
    -> Supply
    -> InScopeSet
    -> Bool
    -> Term
    -> (PrimHeap, PureHeap, Term)
    whnf' Evaluator
    evaluate BindingMap
    bndrs PureHeap
    forall a. Monoid a => a
    mempty TyConMap
    tcm PrimHeap
    gh Supply
    ids1 InScopeSet
    is0 Bool
    False
        let eTy  = TyConMap -> Term -> Type
    forall a. InferType a => TyConMap -> a -> Type
    inferCoreTypeOf TyConMap
    tcm Term
    e
        untran <- isUntranslatableType False eTy
        case untran of
          -- Don't lift out non-representable values, because they cannot be let-bound
          -- in our desired normal form.
          Bool
    False -> do
            -- Look for, and substitute by, disjoint applications of globals in
            -- the arguments first before considering the current term in function
            -- position. Doing it in the other order (this term in function position
            -- first, followed by arguments) resulted in issue #1322
            (args1,isArgs,collectedArgs) <-
              InScopeSet
    -> [(Term, Term)]
    -> [Term]
    -> [Either Term Type]
    -> NormalizeSession
         ([Either Term Type], InScopeSet,
          [(Term, ([Term], CaseTree [Either Term Type]))])
    collectGlobalsArgs InScopeSet
    is0 [(Term, Term)]
    substitution [Term]
    seen [Either Term Type]
    args
            let seenInArgs = ((Term, ([Term], CaseTree [Either Term Type])) -> Term)
    -> [(Term, ([Term], CaseTree [Either Term Type]))] -> [Term]
    forall a b. (a -> b) -> [a] -> [b]
    map (Term, ([Term], CaseTree [Either Term Type])) -> Term
    forall a b. (a, b) -> a
    fst [(Term, ([Term], CaseTree [Either Term Type]))]
    collectedArgs [Term] -> [Term] -> [Term]
    forall a. [a] -> [a] -> [a]
    ++ [Term]
    seen
                isInteresting = InScopeSet
    -> (Term -> Term)
    -> Term
    -> [Either Term Type]
    -> [TickInfo]
    -> Maybe Term
    interestingToLift InScopeSet
    is0 Term -> Term
    eval Term
    fun [Either Term Type]
    args [TickInfo]
    ticks
            case isInteresting of
              Just Term
    fun1 | Term
    fun1 Term -> [Term] -> Bool
    forall (t :: Type -> Type) a.
    (Foldable t, Eq a) =>
    a -> t a -> Bool
    `notElem` [Term]
    seenInArgs -> do
                let e1 :: Term
    e1 = Term -> Maybe Term -> Term
    forall a. a -> Maybe a -> a
    Maybe.fromMaybe (Term -> [Either Term Type] -> Term
    mkApps (Term -> [TickInfo] -> Term
    mkTicks Term
    fun1 [TickInfo]
    ticks) [Either Term Type]
    args1) (Term -> [(Term, Term)] -> Maybe Term
    forall a b. Eq a => a -> [(a, b)] -> Maybe b
    List.lookup Term
    fun1 [(Term, Term)]
    substitution)
                -- This function is lifted out an environment with the currently 'seen'
                -- binders. When we later apply substitution, we need to start with this
                -- environment, otherwise we perform incorrect substitutions in the
                -- arguments.
                (Term, InScopeSet, [(Term, ([Term], CaseTree [Either Term Type]))])
    -> NormalizeSession
         (Term, InScopeSet, [(Term, ([Term], CaseTree [Either Term Type]))])
    forall a. a -> RewriteMonad NormalizeState a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return (Term
    e1,InScopeSet
    isArgs,(Term
    fun1,([Term]
    seen,[Either Term Type] -> CaseTree [Either Term Type]
    forall a. a -> CaseTree a
    Leaf [Either Term Type]
    args1))(Term, ([Term], CaseTree [Either Term Type]))
    -> [(Term, ([Term], CaseTree [Either Term Type]))]
    -> [(Term, ([Term], CaseTree [Either Term Type]))]
    forall a. a -> [a] -> [a]
    :[(Term, ([Term], CaseTree [Either Term Type]))]
    collectedArgs)
              Maybe Term
    _ -> (Term, InScopeSet, [(Term, ([Term], CaseTree [Either Term Type]))])
    -> NormalizeSession
         (Term, InScopeSet, [(Term, ([Term], CaseTree [Either Term Type]))])
    forall a. a -> RewriteMonad NormalizeState a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return (Term -> [Either Term Type] -> Term
    mkApps (Term -> [TickInfo] -> Term
    mkTicks Term
    fun [TickInfo]
    ticks) [Either Term Type]
    args1, InScopeSet
    isArgs, [(Term, ([Term], CaseTree [Either Term Type]))]
    collectedArgs)
          Bool
    _ -> (Term, InScopeSet, [(Term, ([Term], CaseTree [Either Term Type]))])
    -> NormalizeSession
         (Term, InScopeSet, [(Term, ([Term], CaseTree [Either Term Type]))])
    forall a. a -> RewriteMonad NormalizeState a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return (Term
    e,InScopeSet
    is0,[])

    -- FIXME: This duplicates A LOT of let-bindings, where I just pray that after
    -- the ANF, CSE, and DeadCodeRemoval pass all duplicates are removed.
    --
    -- I think we should be able to do better, but perhaps we cannot fix it here.
    collectGlobals InScopeSet
    is0 [(Term, Term)]
    substitution [Term]
    seen (Letrec [LetBinding]
    lbs Term
    body) = do
      let is1 :: InScopeSet
    is1 = InScopeSet -> [Id] -> InScopeSet
    forall a. InScopeSet -> [Var a] -> InScopeSet
    extendInScopeSetList InScopeSet
    is0 ((LetBinding -> Id) -> [LetBinding] -> [Id]
    forall a b. (a -> b) -> [a] -> [b]
    map LetBinding -> Id
    forall a b. (a, b) -> a
    fst [LetBinding]
    lbs)
      (body1,isBody,collectedBody) <-
        InScopeSet
    -> [(Term, Term)]
    -> [Term]
    -> Term
    -> NormalizeSession
         (Term, InScopeSet, [(Term, ([Term], CaseTree [Either Term Type]))])
    collectGlobals InScopeSet
    is1 [(Term, Term)]
    substitution [Term]
    seen Term
    body
      (lbs1,isBndrs,collectedBndrs) <-
        collectGlobalsLbs is1 substitution (map fst collectedBody ++ seen) lbs
      return ( Letrec lbs1 body1
             , unionInScope isBody isBndrs
             , map (second (second (LB lbs1))) (collectedBody ++ collectedBndrs)
             )

    collectGlobals InScopeSet
    is0 [(Term, Term)]
    substitution [Term]
    seen (Tick TickInfo
    t Term
    e) = do
      (e1,is1,collected) <- InScopeSet
    -> [(Term, Term)]
    -> [Term]
    -> Term
    -> NormalizeSession
         (Term, InScopeSet, [(Term, ([Term], CaseTree [Either Term Type]))])
    collectGlobals InScopeSet
    is0 [(Term, Term)]
    substitution [Term]
    seen Term
    e
      return (Tick t e1, is1, collected)

    collectGlobals InScopeSet
    is0 [(Term, Term)]
    _ [Term]
    _ Term
    e = (Term, InScopeSet, [(Term, ([Term], CaseTree [Either Term Type]))])
    -> NormalizeSession
         (Term, InScopeSet, [(Term, ([Term], CaseTree [Either Term Type]))])
    forall a. a -> RewriteMonad NormalizeState a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return (Term
    e,InScopeSet
    is0,[])

    -- | Collect 'CaseTree's for (potentially) disjoint applications of globals out
    -- of a list of application arguments. Also substitute truly disjoint
    -- applications of globals by a reference to a lifted out application.
    collectGlobalsArgs
      :: InScopeSet
      -> [(Term,Term)] -- ^ Substitution of (applications of) a global
                       -- binder by a reference to a lifted term.
      -> [Term] -- ^ List of already seen global binders
      -> [Either Term Type] -- ^ The list of arguments
      -> NormalizeSession
           ( [Either Term Type]
           , InScopeSet
           , [(Term, ([Term], CaseTree [(Either Term Type)]))]
           )
    collectGlobalsArgs :: InScopeSet
    -> [(Term, Term)]
    -> [Term]
    -> [Either Term Type]
    -> NormalizeSession
         ([Either Term Type], InScopeSet,
          [(Term, ([Term], CaseTree [Either Term Type]))])
    collectGlobalsArgs InScopeSet
    is0 [(Term, Term)]
    substitution [Term]
    seen [Either Term Type]
    args = do
        ((is1,_),(args',collected)) <- ([(Either Term Type,
       [(Term, ([Term], CaseTree [Either Term Type]))])]
     -> ([Either Term Type],
         [[(Term, ([Term], CaseTree [Either Term Type]))]]))
    -> ((InScopeSet, [Term]),
        [(Either Term Type,
          [(Term, ([Term], CaseTree [Either Term Type]))])])
    -> ((InScopeSet, [Term]),
        ([Either Term Type],
         [[(Term, ([Term], CaseTree [Either Term Type]))]]))
    forall b c a. (b -> c) -> (a, b) -> (a, c)
    forall (p :: Type -> Type -> Type) b c a.
    Bifunctor p =>
    (b -> c) -> p a b -> p a c
    second [(Either Term Type,
      [(Term, ([Term], CaseTree [Either Term Type]))])]
    -> ([Either Term Type],
        [[(Term, ([Term], CaseTree [Either Term Type]))]])
    forall a b. [(a, b)] -> ([a], [b])
    unzip (((InScopeSet, [Term]),
      [(Either Term Type,
        [(Term, ([Term], CaseTree [Either Term Type]))])])
     -> ((InScopeSet, [Term]),
         ([Either Term Type],
          [[(Term, ([Term], CaseTree [Either Term Type]))]])))
    -> RewriteMonad
         NormalizeState
         ((InScopeSet, [Term]),
          [(Either Term Type,
            [(Term, ([Term], CaseTree [Either Term Type]))])])
    -> RewriteMonad
         NormalizeState
         ((InScopeSet, [Term]),
          ([Either Term Type],
           [[(Term, ([Term], CaseTree [Either Term Type]))]]))
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> ((InScopeSet, [Term])
     -> Either Term Type
     -> RewriteMonad
          NormalizeState
          ((InScopeSet, [Term]),
           (Either Term Type,
            [(Term, ([Term], CaseTree [Either Term Type]))])))
    -> (InScopeSet, [Term])
    -> [Either Term Type]
    -> RewriteMonad
         NormalizeState
         ((InScopeSet, [Term]),
          [(Either Term Type,
            [(Term, ([Term], CaseTree [Either Term Type]))])])
    forall (m :: Type -> Type) acc x y.
    Monad m =>
    (acc -> x -> m (acc, y)) -> acc -> [x] -> m (acc, [y])
    List.mapAccumLM (InScopeSet, [Term])
    -> Either Term Type
    -> RewriteMonad
         NormalizeState
         ((InScopeSet, [Term]),
          (Either Term Type,
           [(Term, ([Term], CaseTree [Either Term Type]))]))
    forall {b}.
    (InScopeSet, [Term])
    -> Either Term b
    -> RewriteMonad
         NormalizeState
         ((InScopeSet, [Term]),
          (Either Term b, [(Term, ([Term], CaseTree [Either Term Type]))]))
    go (InScopeSet
    is0,[Term]
    seen) [Either Term Type]
    args
        return (args',is1,concat collected)
      where
        go :: (InScopeSet, [Term])
    -> Either Term b
    -> RewriteMonad
         NormalizeState
         ((InScopeSet, [Term]),
          (Either Term b, [(Term, ([Term], CaseTree [Either Term Type]))]))
    go (InScopeSet
    isN0,[Term]
    s) (Left Term
    tm) = do
          (tm',isN1,collected) <- InScopeSet
    -> [(Term, Term)]
    -> [Term]
    -> Term
    -> NormalizeSession
         (Term, InScopeSet, [(Term, ([Term], CaseTree [Either Term Type]))])
    collectGlobals InScopeSet
    isN0 [(Term, Term)]
    substitution [Term]
    s Term
    tm
          return ((isN1,map fst collected ++ s),(Left tm',collected))
        go (InScopeSet
    isN,[Term]
    s) (Right b
    ty) = ((InScopeSet, [Term]),
     (Either Term b, [(Term, ([Term], CaseTree [Either Term Type]))]))
    -> RewriteMonad
         NormalizeState
         ((InScopeSet, [Term]),
          (Either Term b, [(Term, ([Term], CaseTree [Either Term Type]))]))
    forall a. a -> RewriteMonad NormalizeState a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return ((InScopeSet
    isN,[Term]
    s),(b -> Either Term b
    forall a b. b -> Either a b
    Right b
    ty,[]))

    -- | Collect 'CaseTree's for (potentially) disjoint applications of globals out
    -- of a list of alternatives. Also substitute truly disjoint applications of
    -- globals by a reference to a lifted out application.
    collectGlobalsAlts ::
         InScopeSet
      -> [(Term,Term)] -- ^ Substitution of (applications of) a global
                       -- binder by a reference to a lifted term.
      -> [Term] -- ^ List of already seen global binders
      -> Term -- ^ The subject term
      -> [Alt] -- ^ The list of alternatives
      -> NormalizeSession
           ( [Alt]
           , InScopeSet
           , [(Term, ([Term], CaseTree [(Either Term Type)]))]
           )
    collectGlobalsAlts :: InScopeSet
    -> [(Term, Term)]
    -> [Term]
    -> Term
    -> [Alt]
    -> NormalizeSession
         ([Alt], InScopeSet,
          [(Term, ([Term], CaseTree [Either Term Type]))])
    collectGlobalsAlts InScopeSet
    is0 [(Term, Term)]
    substitution [Term]
    seen Term
    scrut [Alt]
    alts = do
        (is1,(alts',collected)) <- ([(Alt, [(Term, ([Term], (Pat, CaseTree [Either Term Type])))])]
     -> ([Alt],
         [[(Term, ([Term], (Pat, CaseTree [Either Term Type])))]]))
    -> (InScopeSet,
        [(Alt, [(Term, ([Term], (Pat, CaseTree [Either Term Type])))])])
    -> (InScopeSet,
        ([Alt], [[(Term, ([Term], (Pat, CaseTree [Either Term Type])))]]))
    forall b c a. (b -> c) -> (a, b) -> (a, c)
    forall (p :: Type -> Type -> Type) b c a.
    Bifunctor p =>
    (b -> c) -> p a b -> p a c
    second [(Alt, [(Term, ([Term], (Pat, CaseTree [Either Term Type])))])]
    -> ([Alt],
        [[(Term, ([Term], (Pat, CaseTree [Either Term Type])))]])
    forall a b. [(a, b)] -> ([a], [b])
    unzip ((InScopeSet,
      [(Alt, [(Term, ([Term], (Pat, CaseTree [Either Term Type])))])])
     -> (InScopeSet,
         ([Alt], [[(Term, ([Term], (Pat, CaseTree [Either Term Type])))]])))
    -> RewriteMonad
         NormalizeState
         (InScopeSet,
          [(Alt, [(Term, ([Term], (Pat, CaseTree [Either Term Type])))])])
    -> RewriteMonad
         NormalizeState
         (InScopeSet,
          ([Alt], [[(Term, ([Term], (Pat, CaseTree [Either Term Type])))]]))
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> (InScopeSet
     -> Alt
     -> RewriteMonad
          NormalizeState
          (InScopeSet,
           (Alt, [(Term, ([Term], (Pat, CaseTree [Either Term Type])))])))
    -> InScopeSet
    -> [Alt]
    -> RewriteMonad
         NormalizeState
         (InScopeSet,
          [(Alt, [(Term, ([Term], (Pat, CaseTree [Either Term Type])))])])
    forall (m :: Type -> Type) acc x y.
    Monad m =>
    (acc -> x -> m (acc, y)) -> acc -> [x] -> m (acc, [y])
    List.mapAccumLM InScopeSet
    -> Alt
    -> RewriteMonad
         NormalizeState
         (InScopeSet,
          (Alt, [(Term, ([Term], (Pat, CaseTree [Either Term Type])))]))
    go InScopeSet
    is0 [Alt]
    alts
        let collectedM  = ([(Term, ([Term], (Pat, CaseTree [Either Term Type])))]
     -> Map Term ([Term], [(Pat, CaseTree [Either Term Type])]))
    -> [[(Term, ([Term], (Pat, CaseTree [Either Term Type])))]]
    -> [Map Term ([Term], [(Pat, CaseTree [Either Term Type])])]
    forall a b. (a -> b) -> [a] -> [b]
    map ([(Term, ([Term], [(Pat, CaseTree [Either Term Type])]))]
    -> Map Term ([Term], [(Pat, CaseTree [Either Term Type])])
    forall k a. Ord k => [(k, a)] -> Map k a
    Map.fromList ([(Term, ([Term], [(Pat, CaseTree [Either Term Type])]))]
     -> Map Term ([Term], [(Pat, CaseTree [Either Term Type])]))
    -> ([(Term, ([Term], (Pat, CaseTree [Either Term Type])))]
        -> [(Term, ([Term], [(Pat, CaseTree [Either Term Type])]))])
    -> [(Term, ([Term], (Pat, CaseTree [Either Term Type])))]
    -> Map Term ([Term], [(Pat, CaseTree [Either Term Type])])
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ((Term, ([Term], (Pat, CaseTree [Either Term Type])))
     -> (Term, ([Term], [(Pat, CaseTree [Either Term Type])])))
    -> [(Term, ([Term], (Pat, CaseTree [Either Term Type])))]
    -> [(Term, ([Term], [(Pat, CaseTree [Either Term Type])]))]
    forall a b. (a -> b) -> [a] -> [b]
    map ((([Term], (Pat, CaseTree [Either Term Type]))
     -> ([Term], [(Pat, CaseTree [Either Term Type])]))
    -> (Term, ([Term], (Pat, CaseTree [Either Term Type])))
    -> (Term, ([Term], [(Pat, CaseTree [Either Term Type])]))
    forall b c a. (b -> c) -> (a, b) -> (a, c)
    forall (p :: Type -> Type -> Type) b c a.
    Bifunctor p =>
    (b -> c) -> p a b -> p a c
    second (((Pat, CaseTree [Either Term Type])
     -> [(Pat, CaseTree [Either Term Type])])
    -> ([Term], (Pat, CaseTree [Either Term Type]))
    -> ([Term], [(Pat, CaseTree [Either Term Type])])
    forall b c a. (b -> c) -> (a, b) -> (a, c)
    forall (p :: Type -> Type -> Type) b c a.
    Bifunctor p =>
    (b -> c) -> p a b -> p a c
    second ((Pat, CaseTree [Either Term Type])
    -> [(Pat, CaseTree [Either Term Type])]
    -> [(Pat, CaseTree [Either Term Type])]
    forall a. a -> [a] -> [a]
    :[])))) [[(Term, ([Term], (Pat, CaseTree [Either Term Type])))]]
    collected
            collectedUN = (([Term], [(Pat, CaseTree [Either Term Type])])
     -> ([Term], [(Pat, CaseTree [Either Term Type])])
     -> ([Term], [(Pat, CaseTree [Either Term Type])]))
    -> [Map Term ([Term], [(Pat, CaseTree [Either Term Type])])]
    -> Map Term ([Term], [(Pat, CaseTree [Either Term Type])])
    forall (f :: Type -> Type) k a.
    (Foldable f, Ord k) =>
    (a -> a -> a) -> f (Map k a) -> Map k a
    Map.unionsWith (\([Term]
    l1,[(Pat, CaseTree [Either Term Type])]
    r1) ([Term]
    l2,[(Pat, CaseTree [Either Term Type])]
    r2) -> ([Term] -> [Term]
    forall a. Eq a => [a] -> [a]
    List.nub ([Term]
    l1 [Term] -> [Term] -> [Term]
    forall a. [a] -> [a] -> [a]
    ++ [Term]
    l2),[(Pat, CaseTree [Either Term Type])]
    r1 [(Pat, CaseTree [Either Term Type])]
    -> [(Pat, CaseTree [Either Term Type])]
    -> [(Pat, CaseTree [Either Term Type])]
    forall a. [a] -> [a] -> [a]
    ++ [(Pat, CaseTree [Either Term Type])]
    r2)) [Map Term ([Term], [(Pat, CaseTree [Either Term Type])])]
    collectedM
            collected'  = ((Term, ([Term], [(Pat, CaseTree [Either Term Type])]))
     -> (Term, ([Term], CaseTree [Either Term Type])))
    -> [(Term, ([Term], [(Pat, CaseTree [Either Term Type])]))]
    -> [(Term, ([Term], CaseTree [Either Term Type]))]
    forall a b. (a -> b) -> [a] -> [b]
    map ((([Term], [(Pat, CaseTree [Either Term Type])])
     -> ([Term], CaseTree [Either Term Type]))
    -> (Term, ([Term], [(Pat, CaseTree [Either Term Type])]))
    -> (Term, ([Term], CaseTree [Either Term Type]))
    forall b c a. (b -> c) -> (a, b) -> (a, c)
    forall (p :: Type -> Type -> Type) b c a.
    Bifunctor p =>
    (b -> c) -> p a b -> p a c
    second (([(Pat, CaseTree [Either Term Type])]
     -> CaseTree [Either Term Type])
    -> ([Term], [(Pat, CaseTree [Either Term Type])])
    -> ([Term], CaseTree [Either Term Type])
    forall b c a. (b -> c) -> (a, b) -> (a, c)
    forall (p :: Type -> Type -> Type) b c a.
    Bifunctor p =>
    (b -> c) -> p a b -> p a c
    second (Term
    -> [(Pat, CaseTree [Either Term Type])]
    -> CaseTree [Either Term Type]
    forall a. Term -> [(Pat, CaseTree a)] -> CaseTree a
    Branch Term
    scrut))) (Map Term ([Term], [(Pat, CaseTree [Either Term Type])])
    -> [(Term, ([Term], [(Pat, CaseTree [Either Term Type])]))]
    forall k a. Map k a -> [(k, a)]
    Map.toList Map Term ([Term], [(Pat, CaseTree [Either Term Type])])
    collectedUN)
        return (alts',is1,collected')
      where
        go :: InScopeSet
    -> Alt
    -> RewriteMonad
         NormalizeState
         (InScopeSet,
          (Alt, [(Term, ([Term], (Pat, CaseTree [Either Term Type])))]))
    go InScopeSet
    isN0 (Pat
    p,Term
    e) = do
          let isN1 :: InScopeSet
    isN1 = InScopeSet -> [Id] -> InScopeSet
    forall a. InScopeSet -> [Var a] -> InScopeSet
    extendInScopeSetList InScopeSet
    isN0 (([TyVar], [Id]) -> [Id]
    forall a b. (a, b) -> b
    snd (Pat -> ([TyVar], [Id])
    patIds Pat
    p))
          (e',isN2,collected) <- InScopeSet
    -> [(Term, Term)]
    -> [Term]
    -> Term
    -> NormalizeSession
         (Term, InScopeSet, [(Term, ([Term], CaseTree [Either Term Type]))])
    collectGlobals InScopeSet
    isN1 [(Term, Term)]
    substitution [Term]
    seen Term
    e
          return (isN2,((p,e'),map (second (second (p,))) collected))

    -- | Collect 'CaseTree's for (potentially) disjoint applications of globals out
    -- of a list of let-bindings. Also substitute truly disjoint applications of
    -- globals by a reference to a lifted out application.
    collectGlobalsLbs ::
         InScopeSet
      -> [(Term,Term)] -- ^ Substitution of (applications of) a global
                       -- binder by a reference to a lifted term.
      -> [Term] -- ^ List of already seen global binders
      -> [LetBinding] -- ^ The list let-bindings
      -> NormalizeSession
           ( [LetBinding]
           , InScopeSet
           , [(Term, ([Term], CaseTree [(Either Term Type)]))]
           )
    collectGlobalsLbs :: InScopeSet
    -> [(Term, Term)]
    -> [Term]
    -> [LetBinding]
    -> NormalizeSession
         ([LetBinding], InScopeSet,
          [(Term, ([Term], CaseTree [Either Term Type]))])
    collectGlobalsLbs InScopeSet
    is0 [(Term, Term)]
    substitution [Term]
    seen [LetBinding]
    lbs = do
        let lbsSCCs :: [SCC LetBinding]
    lbsSCCs = HasCallStack => [LetBinding] -> [SCC LetBinding]
    [LetBinding] -> [SCC LetBinding]
    sccLetBindings [LetBinding]
    lbs
        ((is1,_),(lbsSCCs1,collected)) <-
          ([(SCC LetBinding,
       [(Term, ([Term], CaseTree [Either Term Type]))])]
     -> ([SCC LetBinding],
         [[(Term, ([Term], CaseTree [Either Term Type]))]]))
    -> ((InScopeSet, [Term]),
        [(SCC LetBinding,
          [(Term, ([Term], CaseTree [Either Term Type]))])])
    -> ((InScopeSet, [Term]),
        ([SCC LetBinding],
         [[(Term, ([Term], CaseTree [Either Term Type]))]]))
    forall b c a. (b -> c) -> (a, b) -> (a, c)
    forall (p :: Type -> Type -> Type) b c a.
    Bifunctor p =>
    (b -> c) -> p a b -> p a c
    second [(SCC LetBinding, [(Term, ([Term], CaseTree [Either Term Type]))])]
    -> ([SCC LetBinding],
        [[(Term, ([Term], CaseTree [Either Term Type]))]])
    forall a b. [(a, b)] -> ([a], [b])
    unzip (((InScopeSet, [Term]),
      [(SCC LetBinding,
        [(Term, ([Term], CaseTree [Either Term Type]))])])
     -> ((InScopeSet, [Term]),
         ([SCC LetBinding],
          [[(Term, ([Term], CaseTree [Either Term Type]))]])))
    -> RewriteMonad
         NormalizeState
         ((InScopeSet, [Term]),
          [(SCC LetBinding,
            [(Term, ([Term], CaseTree [Either Term Type]))])])
    -> RewriteMonad
         NormalizeState
         ((InScopeSet, [Term]),
          ([SCC LetBinding],
           [[(Term, ([Term], CaseTree [Either Term Type]))]]))
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> ((InScopeSet, [Term])
     -> SCC LetBinding
     -> RewriteMonad
          NormalizeState
          ((InScopeSet, [Term]),
           (SCC LetBinding, [(Term, ([Term], CaseTree [Either Term Type]))])))
    -> (InScopeSet, [Term])
    -> [SCC LetBinding]
    -> RewriteMonad
         NormalizeState
         ((InScopeSet, [Term]),
          [(SCC LetBinding,
            [(Term, ([Term], CaseTree [Either Term Type]))])])
    forall (m :: Type -> Type) acc x y.
    Monad m =>
    (acc -> x -> m (acc, y)) -> acc -> [x] -> m (acc, [y])
    List.mapAccumLM (InScopeSet, [Term])
    -> SCC LetBinding
    -> RewriteMonad
         NormalizeState
         ((InScopeSet, [Term]),
          (SCC LetBinding, [(Term, ([Term], CaseTree [Either Term Type]))]))
    go (InScopeSet
    is0,[Term]
    seen) [SCC LetBinding]
    lbsSCCs
        return (Graph.flattenSCCs lbsSCCs1,is1,concat collected)
      where
        go :: (InScopeSet,[Term]) -> Graph.SCC LetBinding
           -> NormalizeSession
                ( (InScopeSet, [Term])
                , ( Graph.SCC LetBinding
                  , [(Term, ([Term], CaseTree [(Either Term Type)]))]
                  )
                )
        go :: (InScopeSet, [Term])
    -> SCC LetBinding
    -> RewriteMonad
         NormalizeState
         ((InScopeSet, [Term]),
          (SCC LetBinding, [(Term, ([Term], CaseTree [Either Term Type]))]))
    go (InScopeSet
    isN0,[Term]
    s) (Graph.AcyclicSCC (Id
    id_, Term
    e)) = do
          (e',isN1,collected) <- InScopeSet
    -> [(Term, Term)]
    -> [Term]
    -> Term
    -> NormalizeSession
         (Term, InScopeSet, [(Term, ([Term], CaseTree [Either Term Type]))])
    collectGlobals InScopeSet
    isN0 [(Term, Term)]
    substitution [Term]
    s Term
    e
          return ((isN1,map fst collected ++ s),(Graph.AcyclicSCC (id_,e'),collected))
        -- TODO: This completely skips recursive let-bindings in the collection of
        -- potentially disjoint applications of globals; and skips substituting truly
        -- disjoint applications of globals by a reference to a lifted out application.
        --
        -- This is to prevent the creation of combinational loops that have occurred
        -- "in the wild", but for which we have not been able to a create small
        -- unit test that triggers this creation-of-combinational-loops bug.
        -- Completely skipping recursive let-bindings is taking the hammer to
        -- solving this bug, without knowing whether a scalpel even existed and what
        -- it might look like. We should at some point think hard how traversing
        -- recursive let-bindings can introduce combinational loops, and whether
        -- there exists a solution that can traverse recursive let-bindings,
        -- finding more opportunities for DEC, while not introducing combinational
        -- loops.
        go (InScopeSet, [Term])
    acc scc :: SCC LetBinding
    scc@(Graph.CyclicSCC {}) = ((InScopeSet, [Term]),
     (SCC LetBinding, [(Term, ([Term], CaseTree [Either Term Type]))]))
    -> RewriteMonad
         NormalizeState
         ((InScopeSet, [Term]),
          (SCC LetBinding, [(Term, ([Term], CaseTree [Either Term Type]))]))
    forall a. a -> RewriteMonad NormalizeState a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return ((InScopeSet, [Term])
    acc,(SCC LetBinding
    scc,[]))

    -- | Given a case-tree corresponding to a disjoint interesting \"term-in-a-
    -- function-position\", return a let-expression: where the let-binding holds
    -- a case-expression selecting between the distinct arguments of the case-tree,
    -- and the body is an application of the term applied to the shared arguments of
    -- the case tree, and variable references to the created let-bindings.
    --
    -- case-expressions whose type would be non-representable are not let-bound,
    -- but occur directly in the argument position of the application in the body
    -- of the let-expression.
    mkDisjointGroup
      :: InScopeSet
      -- ^ Variables in scope at the very top of the case-tree, i.e., the original
      -- expression
      -> (Term,([Term],CaseTree [Either Term Type]))
      -- ^ Case-tree of arguments belonging to the applied term.
      -> NormalizeSession (Term,[Term])
    mkDisjointGroup :: InScopeSet
    -> (Term, ([Term], CaseTree [Either Term Type]))
    -> RewriteMonad NormalizeState (Term, [Term])
    mkDisjointGroup InScopeSet
    inScope (Term
    fun,([Term]
    seen,CaseTree [Either Term Type]
    cs)) = do
        tcm <- Getting TyConMap RewriteEnv TyConMap
    -> RewriteMonad NormalizeState TyConMap
    forall s (m :: Type -> Type) a.
    MonadReader s m =>
    Getting a s a -> m a
    Lens.view Getting TyConMap RewriteEnv TyConMap
    Getter RewriteEnv TyConMap
    tcCache
        let funName = Term -> Text
    decFunName Term
    fun
            argLen = case CaseTree [Either Term Type] -> [[Either Term Type]]
    forall a. CaseTree a -> [a]
    forall (t :: Type -> Type) a. Foldable t => t a -> [a]
    Foldable.toList CaseTree [Either Term Type]
    cs of
                       [] -> [Char] -> Int
    forall a. HasCallStack => [Char] -> a
    error [Char]
    "mkDisjointGroup: no disjoint groups"
                       [Either Term Type]
    l:[[Either Term Type]]
    _ -> [Either Term Type] -> Int
    forall a. [a] -> Int
    forall (t :: Type -> Type) a. Foldable t => t a -> Int
    length [Either Term Type]
    l
            csT :: [CaseTree (Either Term Type)] -- "Transposed" 'CaseTree [Either Term Type]'
            csT = (Int -> CaseTree (Either Term Type))
    -> [Int] -> [CaseTree (Either Term Type)]
    forall a b. (a -> b) -> [a] -> [b]
    map (\Int
    i -> ([Either Term Type] -> Either Term Type)
    -> CaseTree [Either Term Type] -> CaseTree (Either Term Type)
    forall a b. (a -> b) -> CaseTree a -> CaseTree b
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    fmap ([Either Term Type] -> Int -> Either Term Type
    forall a. HasCallStack => [a] -> Int -> a
    !!Int
    i) CaseTree [Either Term Type]
    cs) [Int
    0..(Int
    argLenInt -> Int -> Int
    forall a. Num a => a -> a -> a
    -Int
    1)] -- sequenceA does the wrong thing
        (lbs,newArgs) <- List.mapAccumRM (\[(Id, (Type, CaseTree Term))]
    lbs (CaseTree (Either Term Type)
    c,Word
    pos) -> do
          let cL :: [Either Term Type]
    cL = CaseTree (Either Term Type) -> [Either Term Type]
    forall a. CaseTree a -> [a]
    forall (t :: Type -> Type) a. Foldable t => t a -> [a]
    Foldable.toList CaseTree (Either Term Type)
    c
          case ([Either Term Type]
    cL, TyConMap -> InScopeSet -> [Either Term Type] -> Bool
    areShared TyConMap
    tcm InScopeSet
    inScope ((Either Term Type -> Either Term Type)
    -> [Either Term Type] -> [Either Term Type]
    forall a b. (a -> b) -> [a] -> [b]
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((Term -> Term) -> Either Term Type -> Either Term Type
    forall a b c. (a -> b) -> Either a c -> Either b c
    forall (p :: Type -> Type -> Type) a b c.
    Bifunctor p =>
    (a -> b) -> p a c -> p b c
    first Term -> Term
    stripTicks) [Either Term Type]
    cL)) of
            (Right Type
    ty:[Either Term Type]
    _, Bool
    True) ->
              ([(Id, (Type, CaseTree Term))], Either Term Type)
    -> RewriteMonad
         NormalizeState ([(Id, (Type, CaseTree Term))], Either Term Type)
    forall a. a -> RewriteMonad NormalizeState a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return ([(Id, (Type, CaseTree Term))]
    lbs,Type -> Either Term Type
    forall a b. b -> Either a b
    Right Type
    ty)
            (Right Type
    _:[Either Term Type]
    _, Bool
    False) ->
              [Char]
    -> RewriteMonad
         NormalizeState ([(Id, (Type, CaseTree Term))], Either Term Type)
    forall a. HasCallStack => [Char] -> a
    error ([Char]
    "mkDisjointGroup: non-equal type arguments: " [Char] -> ShowS
    forall a. Semigroup a => a -> a -> a
    <>
                     [Type] -> [Char]
    forall p. PrettyPrec p => p -> [Char]
    showPpr ([Either Term Type] -> [Type]
    forall a b. [Either a b] -> [b]
    Either.rights [Either Term Type]
    cL))
            (Left Term
    tm:[Either Term Type]
    _, Bool
    True) ->
              ([(Id, (Type, CaseTree Term))], Either Term Type)
    -> RewriteMonad
         NormalizeState ([(Id, (Type, CaseTree Term))], Either Term Type)
    forall a. a -> RewriteMonad NormalizeState a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return ([(Id, (Type, CaseTree Term))]
    lbs,Term -> Either Term Type
    forall a b. a -> Either a b
    Left Term
    tm)
            (Left Term
    tm:[Either Term Type]
    _, Bool
    False) -> do
              let ty :: Type
    ty = TyConMap -> Term -> Type
    forall a. InferType a => TyConMap -> a -> Type
    inferCoreTypeOf TyConMap
    tcm Term
    tm
              let err :: a
    err = [Char] -> a
    forall a. HasCallStack => [Char] -> a
    error ([Char]
    "mkDisjointGroup: mixed type and term arguments: " [Char] -> ShowS
    forall a. Semigroup a => a -> a -> a
    <> [Either Term Type] -> [Char]
    forall a. Show a => a -> [Char]
    show [Either Term Type]
    cL)
              (lbM,arg) <- InScopeSet
    -> Type
    -> CaseTree Term
    -> Text
    -> Word
    -> NormalizeSession (Maybe (Id, (Type, CaseTree Term)), Term)
    disJointSelProj InScopeSet
    inScope Type
    ty (Term -> Either Term Type -> Term
    forall a b. a -> Either a b -> a
    Either.fromLeft Term
    forall {a}. a
    err (Either Term Type -> Term)
    -> CaseTree (Either Term Type) -> CaseTree Term
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> CaseTree (Either Term Type)
    c) Text
    funName Word
    pos
              case lbM of
                Just (Id, (Type, CaseTree Term))
    lb -> ([(Id, (Type, CaseTree Term))], Either Term Type)
    -> RewriteMonad
         NormalizeState ([(Id, (Type, CaseTree Term))], Either Term Type)
    forall a. a -> RewriteMonad NormalizeState a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return ((Id, (Type, CaseTree Term))
    lb(Id, (Type, CaseTree Term))
    -> [(Id, (Type, CaseTree Term))] -> [(Id, (Type, CaseTree Term))]
    forall a. a -> [a] -> [a]
    :[(Id, (Type, CaseTree Term))]
    lbs, Term -> Either Term Type
    forall a b. a -> Either a b
    Left Term
    arg)
                Maybe (Id, (Type, CaseTree Term))
    _ -> ([(Id, (Type, CaseTree Term))], Either Term Type)
    -> RewriteMonad
         NormalizeState ([(Id, (Type, CaseTree Term))], Either Term Type)
    forall a. a -> RewriteMonad NormalizeState a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return ([(Id, (Type, CaseTree Term))]
    lbs, Term -> Either Term Type
    forall a b. a -> Either a b
    Left Term
    arg)
            ([], Bool
    _) ->
              [Char]
    -> RewriteMonad
         NormalizeState ([(Id, (Type, CaseTree Term))], Either Term Type)
    forall a. HasCallStack => [Char] -> a
    error [Char]
    "mkDisjointGroup: no arguments"
          ) [] (zip csT [0..])
        let funApp = Term -> [Either Term Type] -> Term
    mkApps Term
    fun [Either Term Type]
    newArgs
        tupTcm <- Lens.view tupleTcCache
        case lbs of
          [] ->
            (Term, [Term]) -> RewriteMonad NormalizeState (Term, [Term])
    forall a. a -> RewriteMonad NormalizeState a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return (Term
    funApp, [Term]
    seen)
          [(Id
    v,(Type
    ty,CaseTree Term
    ct))] -> do
            let e :: Term
    e = TyConMap
    -> IntMap TyConName -> Type -> [Type] -> CaseTree [Term] -> Term
    genCase TyConMap
    tcm IntMap TyConName
    tupTcm Type
    ty [Type
    ty] ((Term -> [Term]) -> CaseTree Term -> CaseTree [Term]
    forall a b. (a -> b) -> CaseTree a -> CaseTree b
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    fmap (Term -> [Term] -> [Term]
    forall a. a -> [a] -> [a]
    :[]) CaseTree Term
    ct)
            (Term, [Term]) -> RewriteMonad NormalizeState (Term, [Term])
    forall a. a -> RewriteMonad NormalizeState a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return ([LetBinding] -> Term -> Term
    Letrec [(Id
    v,Term
    e)] Term
    funApp, [Term]
    seen)
          [(Id, (Type, CaseTree Term))]
    _ -> do
            let ([Id]
    vs,[(Type, CaseTree Term)]
    zs) = [(Id, (Type, CaseTree Term))] -> ([Id], [(Type, CaseTree Term)])
    forall a b. [(a, b)] -> ([a], [b])
    unzip [(Id, (Type, CaseTree Term))]
    lbs
                csL :: [CaseTree Term]
                ([Type]
    tys,[CaseTree Term]
    csL) = [(Type, CaseTree Term)] -> ([Type], [CaseTree Term])
    forall a b. [(a, b)] -> ([a], [b])
    unzip [(Type, CaseTree Term)]
    zs
                csLT :: CaseTree [Term]
                csLT :: CaseTree [Term]
    csLT = (([Term] -> [Term]) -> [Term])
    -> CaseTree ([Term] -> [Term]) -> CaseTree [Term]
    forall a b. (a -> b) -> CaseTree a -> CaseTree b
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    fmap (([Term] -> [Term]) -> [Term] -> [Term]
    forall a b. (a -> b) -> a -> b
    $ []) ((CaseTree ([Term] -> [Term])
     -> CaseTree ([Term] -> [Term]) -> CaseTree ([Term] -> [Term]))
    -> [CaseTree ([Term] -> [Term])] -> CaseTree ([Term] -> [Term])
    forall a. (a -> a -> a) -> [a] -> a
    forall (t :: Type -> Type) a.
    Foldable t =>
    (a -> a -> a) -> t a -> a
    foldr1 ((([Term] -> [Term]) -> ([Term] -> [Term]) -> [Term] -> [Term])
    -> CaseTree ([Term] -> [Term])
    -> CaseTree ([Term] -> [Term])
    -> CaseTree ([Term] -> [Term])
    forall a b c.
    (a -> b -> c) -> CaseTree a -> CaseTree b -> CaseTree c
    forall (f :: Type -> Type) a b c.
    Applicative f =>
    (a -> b -> c) -> f a -> f b -> f c
    liftA2 ([Term] -> [Term]) -> ([Term] -> [Term]) -> [Term] -> [Term]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    (.)) ((CaseTree Term -> CaseTree ([Term] -> [Term]))
    -> [CaseTree Term] -> [CaseTree ([Term] -> [Term])]
    forall a b. (a -> b) -> [a] -> [b]
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((Term -> [Term] -> [Term])
    -> CaseTree Term -> CaseTree ([Term] -> [Term])
    forall a b. (a -> b) -> CaseTree a -> CaseTree b
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    fmap (:)) [CaseTree Term]
    csL))
                bigTupTy :: Type
    bigTupTy = TyConMap -> IntMap TyConName -> [Type] -> Type
    mkBigTupTy TyConMap
    tcm IntMap TyConName
    tupTcm [Type]
    tys
                ct :: Term
    ct = TyConMap
    -> IntMap TyConName -> Type -> [Type] -> CaseTree [Term] -> Term
    genCase TyConMap
    tcm IntMap TyConName
    tupTcm Type
    bigTupTy [Type]
    tys CaseTree [Term]
    csLT
            tupIn <- InScopeSet -> Text -> Type -> RewriteMonad NormalizeState Id
    forall (m :: Type -> Type).
    MonadUnique m =>
    InScopeSet -> Text -> Type -> m Id
    mkInternalVar InScopeSet
    inScope (Text
    funName Text -> Text -> Text
    forall a. Semigroup a => a -> a -> a
    <> Text
    "_tupIn") Type
    bigTupTy
            projections <-
              Monad.zipWithM (\Id
    v Int
    n ->
                (Id
    v,) (Term -> LetBinding)
    -> RewriteMonad NormalizeState Term
    -> RewriteMonad NormalizeState LetBinding
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> InScopeSet
    -> TyConMap
    -> IntMap TyConName
    -> Term
    -> [Type]
    -> Int
    -> RewriteMonad NormalizeState Term
    forall (m :: Type -> Type).
    MonadUnique m =>
    InScopeSet
    -> TyConMap -> IntMap TyConName -> Term -> [Type] -> Int -> m Term
    mkBigTupSelector InScopeSet
    inScope TyConMap
    tcm IntMap TyConName
    tupTcm (Id -> Term
    Var Id
    tupIn) [Type]
    tys Int
    n)
                vs [0..]
            return (Letrec ((tupIn,ct):projections) funApp, seen)

    -- | Create a selector for the case-tree of the argument. If the argument is
    -- representable create a let-binding for the created selector, and return
    -- a variable reference to this let-binding. If the argument is not representable
    -- return the selector directly.
    disJointSelProj
      :: InScopeSet
      -> Type
      -- ^ Types of the argument
      -> CaseTree Term
      -- ^ The case-tree of argument
      -> OccName
      -- ^ Name of the lifted function
      -> Word
      -- ^ Position of the argument
      -> NormalizeSession (Maybe (Id, (Type, CaseTree Term)),Term)
    disJointSelProj :: InScopeSet
    -> Type
    -> CaseTree Term
    -> Text
    -> Word
    -> NormalizeSession (Maybe (Id, (Type, CaseTree Term)), Term)
    disJointSelProj InScopeSet
    inScope Type
    argTy CaseTree Term
    cs Text
    funName Word
    argN = do
        tcm <- Getting TyConMap RewriteEnv TyConMap
    -> RewriteMonad NormalizeState TyConMap
    forall s (m :: Type -> Type) a.
    MonadReader s m =>
    Getting a s a -> m a
    Lens.view Getting TyConMap RewriteEnv TyConMap
    Getter RewriteEnv TyConMap
    tcCache
        tupTcm <- Lens.view tupleTcCache
        let sel = TyConMap
    -> IntMap TyConName -> Type -> [Type] -> CaseTree [Term] -> Term
    genCase TyConMap
    tcm IntMap TyConName
    tupTcm Type
    argTy [Type
    argTy] ((Term -> [Term]) -> CaseTree Term -> CaseTree [Term]
    forall a b. (a -> b) -> CaseTree a -> CaseTree b
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    fmap (Term -> [Term] -> [Term]
    forall a. a -> [a] -> [a]
    :[]) CaseTree Term
    cs)
        untran <- isUntranslatableType False argTy
        case untran of
          Bool
    True -> (Maybe (Id, (Type, CaseTree Term)), Term)
    -> NormalizeSession (Maybe (Id, (Type, CaseTree Term)), Term)
    forall a. a -> RewriteMonad NormalizeState a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return (Maybe (Id, (Type, CaseTree Term))
    forall a. Maybe a
    Nothing, Term
    sel)
          Bool
    False -> do
            argId <- InScopeSet -> Text -> Type -> RewriteMonad NormalizeState Id
    forall (m :: Type -> Type).
    MonadUnique m =>
    InScopeSet -> Text -> Type -> m Id
    mkInternalVar InScopeSet
    inScope (Text
    funName Text -> Text -> Text
    forall a. Semigroup a => a -> a -> a
    <> Text
    "_arg" Text -> Text -> Text
    forall a. Semigroup a => a -> a -> a
    <> Word -> Text
    forall a. Show a => a -> Text
    showt Word
    argN) Type
    argTy
            return (Just (argId,(argTy,cs)), Var argId)

    -- | Arguments are shared between invocations if:
    --
    -- * They contain _no_ references to locally-bound variables
    -- * Are either:
    --     1. All equal
    --     2. A proof of an equality: we don't care about the shape of a proof.
    --
    --        Whether we have `Refl : True ~ True` or `SomeAxiom : (1 <=? 2) ~ True`
    --        it doesn't matter, since when we normalize both sides we always end
    --        up with a proof of `True ~ True`.
    --        Since DEC only fires for applications where all the type arguments
    --        are equal, we can deduce that all equality arguments witness the same
    --        equality, hence we don't have to care about the shape of the proof.
    areShared :: TyConMap -> InScopeSet -> [Either Term Type] -> Bool
    areShared :: TyConMap -> InScopeSet -> [Either Term Type] -> Bool
    areShared TyConMap
    _   InScopeSet
    _       []       = Bool
    True
    areShared TyConMap
    tcm InScopeSet
    inScope xs :: [Either Term Type]
    xs@(Either Term Type
    x:[Either Term Type]
    _) = Bool
    noFV1 Bool -> Bool -> Bool
    && (Either Term Type -> Bool
    forall {a} {b}. InferType a => Either a b -> Bool
    isProof Either Term Type
    x Bool -> Bool -> Bool
    || [Either Term Type] -> Bool
    forall a. Eq a => [a] -> Bool
    allEqual [Either Term Type]
    xs)
     where
      noFV1 :: Bool
    noFV1 = case Either Term Type
    x of
        Right Type
    ty -> All -> Bool
    getAll (Getting All Type (Var (ZonkAny 1))
    -> (Var (ZonkAny 1) -> All) -> Type -> All
    forall r s a. Getting r s a -> (a -> r) -> s -> r
    Lens.foldMapOf ((forall b. Var b -> Bool)
    -> Word64Set -> Getting All Type (Var (ZonkAny 1))
    forall (f :: Type -> Type) a.
    (Contravariant f, Applicative f) =>
    (forall b. Var b -> Bool)
    -> Word64Set -> (Var a -> f (Var a)) -> Type -> f Type
    typeFreeVars' Var b -> Bool
    forall b. Var b -> Bool
    isLocallyBound Word64Set
    forall a. Monoid a => a
    mempty)
                                           (All -> Var (ZonkAny 1) -> All
    forall a b. a -> b -> a
    const (Bool -> All
    All Bool
    False)) Type
    ty)
        Left Term
    tm  -> All -> Bool
    getAll (Getting All Term (Var (ZonkAny 2))
    -> (Var (ZonkAny 2) -> All) -> Term -> All
    forall r s a. Getting r s a -> (a -> r) -> s -> r
    Lens.foldMapOf ((forall b. Var b -> Bool) -> Getting All Term (Var (ZonkAny 2))
    forall (f :: Type -> Type) a.
    (Contravariant f, Applicative f) =>
    (forall b. Var b -> Bool) -> (Var a -> f (Var a)) -> Term -> f Term
    termFreeVars' Var b -> Bool
    forall b. Var b -> Bool
    isLocallyBound)
                                           (All -> Var (ZonkAny 2) -> All
    forall a b. a -> b -> a
    const (Bool -> All
    All Bool
    False)) Term
    tm)

      isLocallyBound :: Var a -> Bool
    isLocallyBound Var a
    v = Var a -> Bool
    forall b. Var b -> Bool
    isLocalId Var a
    v Bool -> Bool -> Bool
    && Var a
    v Var a -> InScopeSet -> Bool
    forall a. Var a -> InScopeSet -> Bool
    `notElemInScopeSet` InScopeSet
    inScope

      isProof :: Either a b -> Bool
    isProof (Left a
    co) = case Type -> TypeView
    tyView (TyConMap -> a -> Type
    forall a. InferType a => TyConMap -> a -> Type
    inferCoreTypeOf TyConMap
    tcm a
    co) of
        TyConApp (TyConName -> Text
    forall a. Name a -> Text
    nameOcc -> Text
    nm) [Type]
    _ ->  Text
    nm Text -> Text -> Bool
    forall a. Eq a => a -> a -> Bool
    == Name -> Text
    fromTHName ''(~)
        TypeView
    _ -> Bool
    False
      isProof Either a b
    _ = Bool
    False

    -- | Create a case-expression that selects between the distinct arguments given
    -- a case-tree
    genCase :: TyConMap
            -> IntMap TyConName
            -> Type -- ^ Type of the alternatives
            -> [Type] -- ^ Types of the arguments
            -> CaseTree [Term] -- ^ CaseTree of arguments
            -> Term
    genCase :: TyConMap
    -> IntMap TyConName -> Type -> [Type] -> CaseTree [Term] -> Term
    genCase TyConMap
    tcm IntMap TyConName
    tupTcm Type
    ty [Type]
    argTys = CaseTree [Term] -> Term
    go
      where
        go :: CaseTree [Term] -> Term
    go (Leaf [Term]
    tms) =
          TyConMap -> IntMap TyConName -> [(Type, Term)] -> Term
    mkBigTupTm TyConMap
    tcm IntMap TyConName
    tupTcm ([Type] -> [Term] -> [(Type, Term)]
    forall a b. [a] -> [b] -> [(a, b)]
    List.zipEqual [Type]
    argTys [Term]
    tms)

        go (LB [LetBinding]
    lb CaseTree [Term]
    ct) =
          [LetBinding] -> Term -> Term
    Letrec [LetBinding]
    lb (CaseTree [Term] -> Term
    go CaseTree [Term]
    ct)

        go (Branch Term
    scrut [(Pat
    p,CaseTree [Term]
    ct)]) =
          let ct' :: Term
    ct' = CaseTree [Term] -> Term
    go CaseTree [Term]
    ct
              ([TyVar]
    ptvs,[Id]
    pids) = Pat -> ([TyVar], [Id])
    patIds Pat
    p
          in  if ([TyVar] -> [Var (ZonkAny 0)]
    forall a b. Coercible a b => a -> b
    coerce [TyVar]
    ptvs [Var (ZonkAny 0)] -> [Var (ZonkAny 0)] -> [Var (ZonkAny 0)]
    forall a. [a] -> [a] -> [a]
    ++ [Id] -> [Var (ZonkAny 0)]
    forall a b. Coercible a b => a -> b
    coerce [Id]
    pids) [Var (ZonkAny 0)] -> Term -> Bool
    forall a. [Var a] -> Term -> Bool
    `localVarsDoNotOccurIn` Term
    ct'
                 then Term
    ct'
                 else Term -> Type -> [Alt] -> Term
    Case Term
    scrut Type
    ty [(Pat
    p,Term
    ct')]

        go (Branch Term
    scrut [(Pat, CaseTree [Term])]
    pats) =
          Term -> Type -> [Alt] -> Term
    Case Term
    scrut Type
    ty (((Pat, CaseTree [Term]) -> Alt)
    -> [(Pat, CaseTree [Term])] -> [Alt]
    forall a b. (a -> b) -> [a] -> [b]
    map ((CaseTree [Term] -> Term) -> (Pat, CaseTree [Term]) -> Alt
    forall b c a. (b -> c) -> (a, b) -> (a, c)
    forall (p :: Type -> Type -> Type) b c a.
    Bifunctor p =>
    (b -> c) -> p a b -> p a c
    second CaseTree [Term] -> Term
    go) [(Pat, CaseTree [Term])]
    pats)

    -- | Lookup the TyConName and DataCon for a tuple of size n
    findTup :: TyConMap -> IntMap TyConName -> Int -> (TyConName,DataCon)
    findTup :: TyConMap -> IntMap TyConName -> Int -> (TyConName, DataCon)
    findTup TyConMap
    tcm IntMap TyConName
    tupTcm Int
    n =
      (TyConName, DataCon)
    -> Maybe (TyConName, DataCon) -> (TyConName, DataCon)
    forall a. a -> Maybe a -> a
    Maybe.fromMaybe ([Char] -> (TyConName, DataCon)
    forall a. HasCallStack => [Char] -> a
    error ([Char]
    "Cannot build " [Char] -> ShowS
    forall a. Semigroup a => a -> a -> a
    <> Int -> [Char]
    forall a. Show a => a -> [Char]
    show Int
    n [Char] -> ShowS
    forall a. Semigroup a => a -> a -> a
    <> [Char]
    "-tuble")) (Maybe (TyConName, DataCon) -> (TyConName, DataCon))
    -> Maybe (TyConName, DataCon) -> (TyConName, DataCon)
    forall a b. (a -> b) -> a -> b
    $ do
        tupTcNm <- Int -> IntMap TyConName -> Maybe TyConName
    forall a. Int -> IntMap a -> Maybe a
    IntMap.lookup Int
    n IntMap TyConName
    tupTcm
        tupTc <- UniqMap.lookup tupTcNm tcm
        tupDc <- Maybe.listToMaybe (tyConDataCons tupTc)
        return (tupTcNm,tupDc)

    mkBigTupTm :: TyConMap -> IntMap TyConName -> [(Type,Term)] -> Term
    mkBigTupTm :: TyConMap -> IntMap TyConName -> [(Type, Term)] -> Term
    mkBigTupTm TyConMap
    tcm IntMap TyConName
    tupTcm [(Type, Term)]
    args = (Type, Term) -> Term
    forall a b. (a, b) -> b
    snd ((Type, Term) -> Term) -> (Type, Term) -> Term
    forall a b. (a -> b) -> a -> b
    $ TyConMap -> IntMap TyConName -> [(Type, Term)] -> (Type, Term)
    mkBigTup TyConMap
    tcm IntMap TyConName
    tupTcm [(Type, Term)]
    args

    mkSmallTup,mkBigTup :: TyConMap -> IntMap TyConName -> [(Type,Term)] -> (Type,Term)
    mkSmallTup :: TyConMap -> IntMap TyConName -> [(Type, Term)] -> (Type, Term)
    mkSmallTup TyConMap
    _ IntMap TyConName
    _ [] = [Char] -> (Type, Term)
    forall a. HasCallStack => [Char] -> a
    error ([Char] -> (Type, Term)) -> [Char] -> (Type, Term)
    forall a b. (a -> b) -> a -> b
    $ $[Char]
    curLoc [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    "mkSmallTup: Can't create 0-tuple"
    mkSmallTup TyConMap
    _ IntMap TyConName
    _ [(Type
    ty,Term
    tm)] = (Type
    ty,Term
    tm)
    mkSmallTup TyConMap
    tcm IntMap TyConName
    tupTcm [(Type, Term)]
    args = (Type
    ty,Term
    tm)
      where
        ([Type]
    argTys,[Term]
    tms) = [(Type, Term)] -> ([Type], [Term])
    forall a b. [(a, b)] -> ([a], [b])
    unzip [(Type, Term)]
    args
        (TyConName
    tupTcNm,DataCon
    tupDc) = TyConMap -> IntMap TyConName -> Int -> (TyConName, DataCon)
    findTup TyConMap
    tcm IntMap TyConName
    tupTcm ([(Type, Term)] -> Int
    forall a. [a] -> Int
    forall (t :: Type -> Type) a. Foldable t => t a -> Int
    length [(Type, Term)]
    args)
        tm :: Term
    tm = Term -> [Either Term Type] -> Term
    mkApps (DataCon -> Term
    Data DataCon
    tupDc) ((Type -> Either Term Type) -> [Type] -> [Either Term Type]
    forall a b. (a -> b) -> [a] -> [b]
    map Type -> Either Term Type
    forall a b. b -> Either a b
    Right [Type]
    argTys [Either Term Type] -> [Either Term Type] -> [Either Term Type]
    forall a. [a] -> [a] -> [a]
    ++ (Term -> Either Term Type) -> [Term] -> [Either Term Type]
    forall a b. (a -> b) -> [a] -> [b]
    map Term -> Either Term Type
    forall a b. a -> Either a b
    Left [Term]
    tms)
        ty :: Type
    ty = TyConName -> [Type] -> Type
    mkTyConApp TyConName
    tupTcNm [Type]
    argTys

    mkBigTup :: TyConMap -> IntMap TyConName -> [(Type, Term)] -> (Type, Term)
    mkBigTup TyConMap
    tcm IntMap TyConName
    tupTcm = ([(Type, Term)] -> (Type, Term)) -> [(Type, Term)] -> (Type, Term)
    forall a. ([a] -> a) -> [a] -> a
    mkChunkified (TyConMap -> IntMap TyConName -> [(Type, Term)] -> (Type, Term)
    mkSmallTup TyConMap
    tcm IntMap TyConName
    tupTcm)

    mkSmallTupTy,mkBigTupTy
      :: TyConMap
      -> IntMap TyConName
      -> [Type]
      -> Type
    mkSmallTupTy :: TyConMap -> IntMap TyConName -> [Type] -> Type
    mkSmallTupTy TyConMap
    _ IntMap TyConName
    _ [] = [Char] -> Type
    forall a. HasCallStack => [Char] -> a
    error ([Char] -> Type) -> [Char] -> Type
    forall a b. (a -> b) -> a -> b
    $ $[Char]
    curLoc [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    "mkSmallTupTy: Can't create 0-tuple"
    mkSmallTupTy TyConMap
    _ IntMap TyConName
    _ [Type
    ty] = Type
    ty
    mkSmallTupTy TyConMap
    tcm IntMap TyConName
    tupTcm [Type]
    tys = TyConName -> [Type] -> Type
    mkTyConApp TyConName
    tupTcNm [Type]
    tys
      where
        m :: Int
    m = [Type] -> Int
    forall a. [a] -> Int
    forall (t :: Type -> Type) a. Foldable t => t a -> Int
    length [Type]
    tys
        (TyConName
    tupTcNm,DataCon
    _) = TyConMap -> IntMap TyConName -> Int -> (TyConName, DataCon)
    findTup TyConMap
    tcm IntMap TyConName
    tupTcm Int
    m

    mkBigTupTy :: TyConMap -> IntMap TyConName -> [Type] -> Type
    mkBigTupTy TyConMap
    tcm IntMap TyConName
    tupTcm = ([Type] -> Type) -> [Type] -> Type
    forall a. ([a] -> a) -> [a] -> a
    mkChunkified (TyConMap -> IntMap TyConName -> [Type] -> Type
    mkSmallTupTy TyConMap
    tcm IntMap TyConName
    tupTcm)

    mkSmallTupSelector,mkBigTupSelector
      :: MonadUnique m
      => InScopeSet
      -> TyConMap
      -> IntMap TyConName
      -> Term
      -> [Type]
      -> Int
      -> m Term
    mkSmallTupSelector :: forall (m :: Type -> Type).
    MonadUnique m =>
    InScopeSet
    -> TyConMap -> IntMap TyConName -> Term -> [Type] -> Int -> m Term
    mkSmallTupSelector InScopeSet
    _ TyConMap
    _ IntMap TyConName
    _ Term
    scrut [Type
    _] Int
    0 = Term -> m Term
    forall a. a -> m a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return Term
    scrut
    mkSmallTupSelector InScopeSet
    _ TyConMap
    _ IntMap TyConName
    _ Term
    _     [Type
    _] Int
    n = [Char] -> m Term
    forall a. HasCallStack => [Char] -> a
    error ([Char] -> m Term) -> [Char] -> m Term
    forall a b. (a -> b) -> a -> b
    $ $[Char]
    curLoc [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    "mkSmallTupSelector called with one type, but to select " [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Int -> [Char]
    forall a. Show a => a -> [Char]
    show Int
    n
    mkSmallTupSelector InScopeSet
    inScope TyConMap
    tcm IntMap TyConName
    _ Term
    scrut [Type]
    _ Int
    n = [Char] -> InScopeSet -> TyConMap -> Term -> Int -> Int -> m Term
    forall (m :: Type -> Type).
    (HasCallStack, MonadUnique m) =>
    [Char] -> InScopeSet -> TyConMap -> Term -> Int -> Int -> m Term
    mkSelectorCase ($[Char]
    curLoc [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    "mkSmallTupSelector") InScopeSet
    inScope TyConMap
    tcm Term
    scrut Int
    1 Int
    n

    mkBigTupSelector :: forall (m :: Type -> Type).
    MonadUnique m =>
    InScopeSet
    -> TyConMap -> IntMap TyConName -> Term -> [Type] -> Int -> m Term
    mkBigTupSelector InScopeSet
    inScope TyConMap
    tcm IntMap TyConName
    tupTcm Term
    scrut [Type]
    tys Int
    n = [[Type]] -> m Term
    forall {m :: Type -> Type}. MonadUnique m => [[Type]] -> m Term
    go ([Type] -> [[Type]]
    forall {a}. [a] -> [[a]]
    chunkify [Type]
    tys)
      where
        go :: [[Type]] -> m Term
    go [[Type]
    _] = InScopeSet
    -> TyConMap -> IntMap TyConName -> Term -> [Type] -> Int -> m Term
    forall (m :: Type -> Type).
    MonadUnique m =>
    InScopeSet
    -> TyConMap -> IntMap TyConName -> Term -> [Type] -> Int -> m Term
    mkSmallTupSelector InScopeSet
    inScope TyConMap
    tcm IntMap TyConName
    tupTcm Term
    scrut [Type]
    tys Int
    n
        go [[Type]]
    tyss = do
          let (Int
    nOuter,Int
    nInner) = Int -> Int -> (Int, Int)
    forall a. Integral a => a -> a -> (a, a)
    divMod Int
    n Int
    mAX_TUPLE_SIZE
              tyss' :: [Type]
    tyss' = ([Type] -> Type) -> [[Type]] -> [Type]
    forall a b. (a -> b) -> [a] -> [b]
    map (TyConMap -> IntMap TyConName -> [Type] -> Type
    mkSmallTupTy TyConMap
    tcm IntMap TyConName
    tupTcm) [[Type]]
    tyss
          outer <- InScopeSet
    -> TyConMap -> IntMap TyConName -> Term -> [Type] -> Int -> m Term
    forall (m :: Type -> Type).
    MonadUnique m =>
    InScopeSet
    -> TyConMap -> IntMap TyConName -> Term -> [Type] -> Int -> m Term
    mkSmallTupSelector InScopeSet
    inScope TyConMap
    tcm IntMap TyConName
    tupTcm Term
    scrut [Type]
    tyss' Int
    nOuter
          inner <- mkSmallTupSelector inScope tcm tupTcm outer (tyss List.!! nOuter) nInner
          return inner

    -- | Determine if a term in a function position is interesting to lift out of
    -- of a case-expression.
    --
    -- This holds for all global functions, and certain primitives. Currently those
    -- primitives are:
    --
    -- * All non-cheap multiplications
    -- * All division-like operations with a non-cheap divisor
    --
    -- Multiplying/dividing by zero or powers of two are considered cheap and
    -- isn't lifted out.
    interestingToLift
      :: InScopeSet
      -- ^ in scope
      -> (Term -> Term)
      -- ^ Evaluator
      -> Term
      -- ^ Term in function position
      -> [Either Term Type]
      -- ^ Arguments
      -> [TickInfo]
      -- ^ Tick annoations
      -> Maybe Term
    interestingToLift :: InScopeSet
    -> (Term -> Term)
    -> Term
    -> [Either Term Type]
    -> [TickInfo]
    -> Maybe Term
    interestingToLift InScopeSet
    inScope Term -> Term
    _ e :: Term
    e@(Var Id
    v) [Either Term Type]
    _ [TickInfo]
    ticks =
      if TickInfo
    NoDeDup TickInfo -> [TickInfo] -> Bool
    forall (t :: Type -> Type) a.
    (Foldable t, Eq a) =>
    a -> t a -> Bool
    `notElem` [TickInfo]
    ticks Bool -> Bool -> Bool
    && (Id -> Bool
    forall b. Var b -> Bool
    isGlobalId Id
    v Bool -> Bool -> Bool
    ||  Id
    v Id -> InScopeSet -> Bool
    forall a. Var a -> InScopeSet -> Bool
    `elemInScopeSet` InScopeSet
    inScope)
         then (Term -> Maybe Term
    forall a. a -> Maybe a
    Just Term
    e)
         else Maybe Term
    forall a. Maybe a
    Nothing
    interestingToLift InScopeSet
    inScope Term -> Term
    eval e :: Term
    e@(Prim PrimInfo
    pInfo) [Either Term Type]
    args [TickInfo]
    ticks
      | TickInfo
    NoDeDup TickInfo -> [TickInfo] -> Bool
    forall (t :: Type -> Type) a.
    (Foldable t, Eq a) =>
    a -> t a -> Bool
    `notElem` [TickInfo]
    ticks = do
      let anyArgNotConstant :: Bool
    anyArgNotConstant = (Term -> Bool) -> [Term] -> Bool
    forall (t :: Type -> Type) a.
    Foldable t =>
    (a -> Bool) -> t a -> Bool
    any (Bool -> Bool
    not (Bool -> Bool) -> (Term -> Bool) -> Term -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Term -> Bool
    isConstant) [Term]
    lArgs
      case Text -> [(Text, Bool)] -> Maybe Bool
    forall a b. Eq a => a -> [(a, b)] -> Maybe b
    List.lookup (PrimInfo -> Text
    primName PrimInfo
    pInfo) [(Text, Bool)]
    interestingPrims of
        Just Bool
    t | Bool
    t Bool -> Bool -> Bool
    || Bool
    anyArgNotConstant -> (Term -> Maybe Term
    forall a. a -> Maybe a
    Just Term
    e)
        Maybe Bool
    _ | TickInfo
    DeDup TickInfo -> [TickInfo] -> Bool
    forall a. Eq a => a -> [a] -> Bool
    forall (t :: Type -> Type) a.
    (Foldable t, Eq a) =>
    a -> t a -> Bool
    `elem` [TickInfo]
    ticks -> (Term -> Maybe Term
    forall a. a -> Maybe a
    Just Term
    e)
        Maybe Bool
    _ ->
          if Type -> Bool
    isHOTy (PrimInfo -> Type
    forall a. HasType a => a -> Type
    coreTypeOf PrimInfo
    pInfo) then do
            let anyInteresting :: Bool
    anyInteresting = (Term -> Bool) -> [Term] -> Bool
    forall (t :: Type -> Type) a.
    Foldable t =>
    (a -> Bool) -> t a -> Bool
    List.any (Maybe Term -> Bool
    forall a. Maybe a -> Bool
    Maybe.isJust (Maybe Term -> Bool) -> (Term -> Maybe Term) -> Term -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Term -> Maybe Term
    isInteresting) [Term]
    lArgs
            if Bool
    anyInteresting then Term -> Maybe Term
    forall a. a -> Maybe a
    Just Term
    e else Maybe Term
    forall a. Maybe a
    Nothing
          else
            Maybe Term
    forall a. Maybe a
    Nothing

      where
        isInteresting :: Term -> Maybe Term
    isInteresting = (\(Term
    x, [Either Term Type]
    y, [TickInfo]
    z) -> InScopeSet
    -> (Term -> Term)
    -> Term
    -> [Either Term Type]
    -> [TickInfo]
    -> Maybe Term
    interestingToLift InScopeSet
    inScope Term -> Term
    eval Term
    x [Either Term Type]
    y [TickInfo]
    z) ((Term, [Either Term Type], [TickInfo]) -> Maybe Term)
    -> (Term -> (Term, [Either Term Type], [TickInfo]))
    -> Term
    -> Maybe Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Term -> (Term, [Either Term Type], [TickInfo])
    collectArgsTicks
        interestingPrims :: [(Text, Bool)]
    interestingPrims = ((Name, Bool) -> (Text, Bool)) -> [(Name, Bool)] -> [(Text, Bool)]
    forall a b. (a -> b) -> [a] -> [b]
    map ((Name -> Text) -> (Name, Bool) -> (Text, Bool)
    forall a b c. (a -> b) -> (a, c) -> (b, c)
    forall (p :: Type -> Type -> Type) a b c.
    Bifunctor p =>
    (a -> b) -> p a c -> p b c
    first Name -> Text
    fromTHName)
          [('(Clash.Sized.Internal.BitVector.*#),Bool
    bothNotPow2)
          ,('Clash.Sized.Internal.BitVector.times#,Bool
    bothNotPow2)
          ,('Clash.Sized.Internal.BitVector.quot#,Bool
    lastNotPow2)
          ,('Clash.Sized.Internal.BitVector.rem#,Bool
    lastNotPow2)
          ,('(Clash.Sized.Internal.Index.*#),Bool
    bothNotPow2)
          ,('Clash.Sized.Internal.Index.times#,Bool
    bothNotPow2)
          ,('Clash.Sized.Internal.Index.quot#,Bool
    lastNotPow2)
          ,('Clash.Sized.Internal.Index.rem#,Bool
    lastNotPow2)
          ,('(Clash.Sized.Internal.Signed.*#),Bool
    bothNotPow2)
          ,('Clash.Sized.Internal.Signed.times#,Bool
    bothNotPow2)
          ,('Clash.Sized.Internal.Signed.rem#,Bool
    lastNotPow2)
          ,('Clash.Sized.Internal.Signed.quot#,Bool
    lastNotPow2)
          ,('Clash.Sized.Internal.Signed.div#,Bool
    lastNotPow2)
          ,('Clash.Sized.Internal.Signed.mod#,Bool
    lastNotPow2)
          ,('(Clash.Sized.Internal.Unsigned.*#),Bool
    bothNotPow2)
          ,('Clash.Sized.Internal.Unsigned.times#,Bool
    bothNotPow2)
          ,('Clash.Sized.Internal.Unsigned.quot#,Bool
    lastNotPow2)
          ,('Clash.Sized.Internal.Unsigned.rem#,Bool
    lastNotPow2)
          ,('GHC.Base.quotInt,Bool
    lastNotPow2)
          ,('GHC.Base.remInt,Bool
    lastNotPow2)
          ,('GHC.Base.divInt,Bool
    lastNotPow2)
          ,('GHC.Base.modInt,Bool
    lastNotPow2)
          ,('GHC.Classes.divInt#,Bool
    lastNotPow2)
          ,('GHC.Classes.modInt#,Bool
    lastNotPow2)
    #if MIN_VERSION_base(4,15,0)
          ,('GHC.Num.Integer.integerMul,Bool
    bothNotPow2)
          ,('GHC.Num.Integer.integerDiv,Bool
    lastNotPow2)
          ,('GHC.Num.Integer.integerMod,Bool
    lastNotPow2)
          ,('GHC.Num.Integer.integerQuot,Bool
    lastNotPow2)
          ,('GHC.Num.Integer.integerRem,Bool
    lastNotPow2)
    #else
          ,('GHC.Integer.Type.timesInteger,bothNotPow2)
          ,('GHC.Integer.Type.divInteger,lastNotPow2)
          ,('GHC.Integer.Type.modInteger,lastNotPow2)
          ,('GHC.Integer.Type.quotInteger,lastNotPow2)
          ,('GHC.Integer.Type.remInteger,lastNotPow2)
    #endif
          ,('(GHC.Prim.*#),Bool
    bothNotPow2)
          ,('GHC.Prim.quotInt#,Bool
    lastNotPow2)
          ,('GHC.Prim.remInt#,Bool
    lastNotPow2)
          ]

        lArgs :: [Term]
    lArgs       = [Either Term Type] -> [Term]
    forall a b. [Either a b] -> [a]
    Either.lefts [Either Term Type]
    args

        lastNotPow2 :: Bool
    lastNotPow2 = case [Term]
    lArgs of
                        [] -> Bool
    True
                        [Term]
    _  -> Bool -> Bool
    not (Term -> Bool
    termIsPow2 ([Term] -> Term
    forall a. HasCallStack => [a] -> a
    last [Term]
    lArgs))
        -- | This only looks at the last two arguments, skipping over any constraints if they exist
        bothNotPow2 :: Bool
    bothNotPow2 = [Term] -> Bool
    go [Term]
    lArgs
         where
          go :: [Term] -> Bool
    go [Term]
    xs = case [Term]
    xs of
                    [] -> Bool
    True
                    [Term
    a] -> Bool -> Bool
    not (Term -> Bool
    termIsPow2 Term
    a)
                    [Term
    a,Term
    b] -> Bool -> Bool
    not (Term -> Bool
    termIsPow2 Term
    a) Bool -> Bool -> Bool
    && Bool -> Bool
    not (Term -> Bool
    termIsPow2 Term
    b)
                    (Term
    _:[Term]
    rest) -> [Term] -> Bool
    go [Term]
    rest

        termIsPow2 :: Term -> Bool
    termIsPow2 Term
    e' = case Term -> Term
    eval Term
    e' of
          Literal (IntegerLiteral Integer
    n) -> Integer -> Bool
    forall {a}. (Bits a, Num a) => a -> Bool
    isPow2 Integer
    n
          Term
    a -> case Term -> (Term, [Either Term Type])
    collectArgs Term
    a of
            (Prim PrimInfo
    p,[Right Type
    _,Left Term
    _,       Left (Literal (IntegerLiteral Integer
    n))])
              | Text -> Bool
    isFromInt (PrimInfo -> Text
    primName PrimInfo
    p) -> Integer -> Bool
    forall {a}. (Bits a, Num a) => a -> Bool
    isPow2 Integer
    n
            (Prim PrimInfo
    p,[Right Type
    _,Left Term
    _,Left Term
    _,Left (Literal (IntegerLiteral Integer
    n))])
              | PrimInfo -> Text
    primName PrimInfo
    p Text -> Text -> Bool
    forall a. Eq a => a -> a -> Bool
    == Name -> Text
    fromTHName 'Clash.Sized.Internal.BitVector.fromInteger#  -> Integer -> Bool
    forall {a}. (Bits a, Num a) => a -> Bool
    isPow2 Integer
    n
            (Term, [Either Term Type])
    _ -> Bool
    False

        -- This used to contain (x /= 0), but multiplying by zero is free
        isPow2 :: a -> Bool
    isPow2 a
    x = (a
    x a -> a -> a
    forall a. Bits a => a -> a -> a
    .&. (a -> a
    forall a. Bits a => a -> a
    complement a
    x a -> a -> a
    forall a. Num a => a -> a -> a
    + a
    1)) a -> a -> Bool
    forall a. Eq a => a -> a -> Bool
    == a
    x

        isHOTy :: Type -> Bool
    isHOTy Type
    t = case Type -> ([Either TyVar Type], Type)
    splitFunForallTy Type
    t of
          ([Either TyVar Type]
    args',Type
    _) -> (Type -> Bool) -> [Type] -> Bool
    forall (t :: Type -> Type) a.
    Foldable t =>
    (a -> Bool) -> t a -> Bool
    any Type -> Bool
    isPolyFunTy ([Either TyVar Type] -> [Type]
    forall a b. [Either a b] -> [b]
    Either.rights [Either TyVar Type]
    args')

    interestingToLift InScopeSet
    _ Term -> Term
    _ Term
    _ [Either Term Type]
    _ [TickInfo]
    _ = Maybe Term
    forall a. Maybe a
    Nothing

    fromTHName :: TH.Name -> Text.Text
    fromTHName :: Name -> Text
    fromTHName = [Char] -> Text
    Text.pack ([Char] -> Text) -> (Name -> [Char]) -> Name -> Text
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Name -> [Char]
    forall a. Show a => a -> [Char]
    show