content: {-|
    Copyright  :  (C) 2012-2016, University of Twente,
                      2016-2017, Myrtle Software Ltd,
                      2017-2022, Google Inc.,
                      2021-2024, QBayLogic B.V.
    License    :  BSD2 (see the file LICENSE)
    Maintainer :  QBayLogic B.V. <devops@qbaylogic.com>
    Transformations on case-expressions
  -}
  
  {-# LANGUAGE BangPatterns #-}
  {-# LANGUAGE CPP #-}
  {-# LANGUAGE FlexibleContexts #-}
  {-# LANGUAGE LambdaCase #-}
  {-# LANGUAGE MagicHash #-}
  {-# LANGUAGE OverloadedStrings #-}
  {-# LANGUAGE TemplateHaskell #-}
  
  module Clash.Normalize.Transformations.Case
    ( caseCase
    , caseCon
    , caseElemNonReachable
    , caseFlat
    , caseLet
    , caseOneAlt
    , elimExistentials
    ) where
  
  import Control.Exception.Base (patError)
  #if MIN_VERSION_base(4,16,0)
  import GHC.Prim.Panic (absentError)
  #else
  import Control.Exception.Base (absentError)
  #endif
  import qualified Control.Lens as Lens
  import Control.Monad.State.Strict (evalState)
  import Data.Bifunctor (second)
  import Data.Coerce (coerce)
  import qualified Data.Either as Either
  import qualified Data.List as List
  import qualified Data.List.Extra as List
  import qualified Data.Maybe as Maybe
  import qualified Data.Primitive.ByteArray as BA
  import qualified Data.Text.Extra as Text (showt)
  import GHC.Stack (HasCallStack)
  
  #if MIN_VERSION_base(4,15,0)
  import GHC.Num.Integer (Integer(..))
  #else
  import GHC.Integer.GMP.Internals (BigNat(..), Integer(..))
  #endif
  
  import Clash.Sized.Internal.BitVector as BV (BitVector, eq#)
  import Clash.Sized.Internal.Index as I (Index, eq#)
  import Clash.Sized.Internal.Signed as S (Signed, eq#)
  import Clash.Sized.Internal.Unsigned as U (Unsigned, eq#)
  
  import Clash.Core.DataCon (DataCon(..))
  import Clash.Core.EqSolver
  import Clash.Core.FreeVars (freeLocalIds, localVarsDoNotOccurIn)
  import Clash.Core.HasType
  import Clash.Core.Literal (Literal(..))
  import Clash.Core.Name (nameOcc)
  import Clash.Core.Pretty (showPpr)
  import Clash.Core.Subst
  import Clash.Core.Term
    ( Alt, Pat(..), PrimInfo(..), Term(..), collectArgs, collectArgsTicks
    , collectTicks, mkApps, mkTicks, patIds, stripTicks, Bind(..))
  import Clash.Core.TyCon (TyConMap)
  import Clash.Core.Type (LitTy(..), Type(..), TypeView(..), coreView1, tyView)
  import Clash.Core.Util (listToLets, mkInternalVar)
  import Clash.Core.VarEnv
    ( InScopeSet, elemVarSet, extendInScopeSet, extendInScopeSetList, mkVarSet
    , unitVarSet, uniqAway)
  import Clash.Debug (traceIf)
  import Clash.Driver.Types (DebugOpts(dbg_invariants))
  import Clash.Netlist.Types (FilteredHWType(..), HWType(..))
  import Clash.Netlist.Util (coreTypeToHWType, representableType)
  import qualified Clash.Normalize.Primitives as NP (undefined, undefinedX)
  import Clash.Normalize.Types (NormRewrite, NormalizeSession)
  import Clash.Rewrite.Combinators ((>-!))
  import Clash.Rewrite.Types
    ( TransformContext(..), bindings, customReprs, debugOpts, tcCache
    , typeTranslator, workFreeBinders)
  import Clash.Rewrite.Util (changed, isFromInt, whnfRW)
  import Clash.Rewrite.WorkFree
  import Clash.Util (curLoc)
  
  import Clash.XException (errorX)
  
  -- | Move a Case-decomposition from the subject of a Case-decomposition to the
  -- alternatives
  caseCase :: HasCallStack => NormRewrite
  caseCase (TransformContext is0 _) e@(Case (stripTicks -> Case scrut alts1Ty alts1) alts2Ty alts2) = do
    ty1Rep <- representableType
      <$> Lens.view typeTranslator
      <*> Lens.view customReprs
      <*> pure False
      <*> Lens.view tcCache
      <*> pure alts1Ty
  
    -- This is only worth doing if the inner case-expression has a
    -- non-representable alternative type.
    if ty1Rep then return e else
      -- Deshadow to prevent accidental capture of free variables of inner
      -- case. Imagine:
      --
      --   case (case a of {x -> x}) of {_ -> x}
      --
      -- 'x' is introduced the inner 'case' and used (as a free variable) in
      -- the outer one. The goal of 'caseCase' is to rewrite cases such that
      -- their subjects aren't cases. This is achieved by 'pushing' the outer
      -- case to all the alternatives of the inner one. Naively doing so in
      -- this example would cause an accidental capture:
      --
      --   case a of {x -> case x of {_ -> x}}
      --
      -- Suddenly, the 'x' in the alternative of the inner case statement
      -- refers to the one introduced by the outer one, instead of being a
      -- free variable. To prevent this, we deshadow the alternatives of the
      -- original inner case. We now end up with:
      --
      --   case a of {x1 -> case x1 of {_ -> x}}
      --
      let newAlts = fmap (second (\altE -> Case altE alts2Ty alts2))
                        (fmap (deShadowAlt is0) alts1)
       in changed $ Case scrut alts2Ty newAlts
  
  caseCase _ e = return e
  {-# SCC caseCase #-}
  
  {-
  NOTE: caseOneAlt before caseCon'
  
  When you put a bang on a signal argument:
      f :: Signal d a -> _
      f !x = ...
  GHC generates a case like:
      case x of
        _ :- _ -> ...
  
  When this f is inlined in an:
      g = f (pure False)
  And clash does its Signal d a ~ a thing we get:
      g = case False of
        _ :- _ -> ...
  Because no pattern matches caseCon transforms this into
      g = undefined
  
  By trying caseOneAlt first clash can instead drop the case
  and use the body of the single alternative.
  -}
  caseCon :: HasCallStack => NormRewrite
  caseCon = const caseOneAlt >-! caseCon'
  
  -- | Specialize a Case-decomposition (replace by the RHS of an alternative) if
  -- the subject is (an application of) a DataCon; or if there is only a single
  -- alternative that doesn't reference variables bound by the pattern.
  --
  -- Note [CaseCon deshadow]
  --
  -- Imagine:
  --
  -- @
  -- case D (f a b) (g x y) of
  --   D a b -> h a
  -- @
  --
  -- rewriting this to:
  --
  -- @
  -- let a = f a b
  -- in  h a
  -- @
  --
  -- is very bad because the newly introduced let-binding now captures the free
  -- variable 'a' in 'f a b'.
  --
  -- instead me must rewrite to:
  --
  -- @
  -- let a1 = f a b
  -- in  h a1
  -- @
  caseCon' :: HasCallStack => NormRewrite
  caseCon' ctx@(TransformContext is0 _) e@(Case subj ty alts) = do
   tcm <- Lens.view tcCache
   case collectArgsTicks subj of
    -- The subject is an applied data constructor
    (Data dc, args, ticks) -> case List.find (equalCon . fst) alts of
      Just (DataPat _ tvs xs, altE) -> do
       let
        -- Create the substitution environment for all the existential
        -- type variables.
        exTysList = List.zipEqual tvs (drop (length (dcUnivTyVars dc)) (Either.rights args))
        exTySubst = extendTvSubstList (mkSubst is0) exTysList
        -- Apply the type-substitution in all the pattern variables, we need
        -- to do this because we might use them as let-bindings later on,
        -- and they should have the correct type.
        xs1 = fmap (substTyInVar exTySubst) xs
        -- Create an initial set of let-binders for all variables used in the
        -- RHS of the alternative. We might later decide to substitute instead
        -- of let-bind in case the RHS of the let-binder is work-free.
        fvs = Lens.foldMapOf freeLocalIds unitVarSet altE
        (binds,_) = List.partition ((`elemVarSet` fvs) . fst)
                  $ List.zipEqual xs1 (Either.lefts args)
        binds1 = fmap (second (`mkTicks` ticks)) binds
       altE1 <-
         case binds1 of
          [] ->
            -- Apply the type-substitution for the existential type variables
            pure (substTm "caseCon'" exTySubst altE)
          _  -> do
            -- See Note [CaseCon deshadow]
            let
              -- Only let-bind expression that perform work.
              is1 = extendInScopeSetList (extendInScopeSetList is0 tvs) xs1
            ((is3,substIds),binds2) <- List.mapAccumLM newBinder (is1,[]) binds1
            let
              -- Create a substitution for all the existential type variables
              -- and the work-free expressions
              subst = mkSubst is3
                        `extendTvSubstList` exTysList
                        `extendIdSubstList` substIds
              body  = substTm "caseCon'" subst altE
            case Maybe.catMaybes binds2 of
              []     -> pure body
              -- Use listToLets to create a series of non-recursive lets instead
              -- of a recursive group. We know these binders will not form a group.
              binds3 -> pure (listToLets binds3 body)
       changed altE1
      _ -> case alts of
             -- In Core, default patterns always come first, so we match against
             -- that if there is one, and we couldn't match with any of the data
             -- patterns.
             ((DefaultPat,altE):_) -> changed altE
             _ -> changed (TyApp (Prim NP.undefined) ty)
      where
        -- Check whether the pattern matches the data constructor
        equalCon (DataPat dcPat _ _) = dcTag dc == dcTag dcPat
        equalCon _ = False
  
        -- Decide whether the applied arguments of the data constructor should
        -- be let-bound, or substituted into the alternative. We decide this
        -- based on the fact on whether the argument has the potential to make
        -- the circuit larger than needed if we were to duplicate that argument.
        newBinder (isN0, substN) (x, arg) = do
          bndrs <- Lens.use bindings
          isWorkFree workFreeBinders bndrs arg >>= \case
            True -> pure ((isN0, (x, arg):substN), Nothing)
            False ->
              let
                x' = uniqAway isN0 x
                isN1 = extendInScopeSet isN0 x'
              in
                pure ((isN1, (x, Var x'):substN), Just (x', arg))
  
    -- The subject is a literal
    (Literal l,_,_) -> case List.find (equalLit . fst) alts of
      Just (LitPat _,altE) -> changed altE
      _ -> matchLiteralContructor e l alts
      where
        equalLit (LitPat l') = l == l'
        equalLit _ = False
  
    -- The subject is an applied primitive
    (Prim _,_,_) ->
      -- We try to reduce the applied primitive to WHNF
      whnfRW True ctx subj $ \ctx1 subj1 -> case collectArgsTicks subj1 of
        -- WHNF of subject is a literal, try `caseCon` with that
        (Literal l,_,_) -> caseCon ctx1 (Case (Literal l) ty alts)
        -- WHNF of subject is a data-constructor, try `caseCon` with that
        (Data _,_,_) -> caseCon ctx1 (Case subj1 ty alts)
        -- WHNF of subject is _|_, in the form of `error`: that means that the
        -- entire case-expression is evaluates to _|_
        (Prim pInfo,repTy:_:callStack:msg:_,ticks)
          | primName pInfo == Text.showt 'error ->
          let e1 = mkApps (mkTicks (Prim pInfo) ticks)
                          [repTy,Right ty,callStack,msg]
           in changed e1
        -- WHNF of subject is _|_, in the form of `absentError`: that means that
        -- the entire case-expression is evaluates to _|_
        (Prim pInfo,_:msgOrCallStack:_,ticks)
          | primName pInfo == Text.showt 'absentError ->
          let e1 = mkApps (mkTicks (Prim pInfo) ticks)
                          [Right ty,msgOrCallStack]
          in  changed e1
        -- WHNF of subject is _|_, in the form of  `patError`, `undefined`, or
        -- `errorWithoutStackTrace`: that means the entire case-expression is _|_
        (Prim pInfo,repTy:_:msgOrCallStack:_,ticks)
          | primName pInfo `elem` [ Text.showt 'patError
                                  , Text.showt 'undefined
                                  , Text.showt 'errorWithoutStackTrace] ->
          let e1 = mkApps (mkTicks (Prim pInfo) ticks)
                          [repTy,Right ty,msgOrCallStack]
          in  changed e1
        -- WHNF of subject is _|_, in the form of our internal _|_-values: that
        -- means the entire case-expression is _|_
        (Prim pInfo,[_],ticks)
          | primName pInfo `elem` [ Text.showt 'NP.undefined
                                  , Text.showt 'NP.undefinedX ] ->
          let e1 = mkApps (mkTicks (Prim pInfo) ticks) [Right ty]
          in changed e1
        -- WHNF of subject is _|_, in the form of `errorX`: that means that
        -- the entire case-expression is evaluates to _|_
        (Prim pInfo,_:callStack:msg:_,ticks)
          | primName pInfo == Text.showt 'errorX
          -> let e1 = mkApps (mkTicks (Prim pInfo) ticks) [Right ty,callStack,msg]
              in changed e1
        -- WHNF of subject is non of the above, so either a variable reference,
        -- or a primitive for which the evaluator doesn't have any evaluation
        -- rules.
        _ -> do
          let subjTy = inferCoreTypeOf tcm subj
          tran <- Lens.view typeTranslator
          reprs <- Lens.view customReprs
          case (`evalState` mempty) (coreTypeToHWType tran reprs tcm subjTy) of
            Right (FilteredHWType (Void (Just hty)) _areVoids)
              | hty `elem` [BitVector 0, Unsigned 0, Signed 0, Index 1]
              -- If we know that the type of the subject is zero-bits wide and
              -- one of the Clash number types. Then the only valid alternative is
              -- the one that can match on the literal "0", so try 'caseCon' with
              -- that.
              -> caseCon ctx1 (Case (Literal (IntegerLiteral 0)) ty alts)
            _ -> do
              opts <- Lens.view debugOpts
              -- When invariants are being checked, report missing evaluation
              -- rules for the primitive evaluator.
              traceIf (dbg_invariants opts && isConstant subj)
                ("Unmatchable constant as case subject: " ++ showPpr subj ++
                   "\nWHNF is: " ++ showPpr subj1)
                -- Otherwise check whether the entire case-expression has a
                -- single alternative, and pick that one.
                (caseOneAlt e)
  
    -- The subject is a variable
    (Var v, [], _) | isNum0 (coreTypeOf v) ->
      -- If we know that the type of the subject is zero-bits wide and
      -- one of the Clash number types. Then the only valid alternative is
      -- the one that can match on the literal "0", so try 'caseCon' with
      -- that.
      caseCon ctx (Case (Literal (IntegerLiteral 0)) ty alts)
     where
      isNum0 (tyView -> TyConApp (nameOcc -> tcNm) [arg])
        | tcNm `elem`
          [ Text.showt ''BitVector
          , Text.showt ''Signed
          , Text.showt ''Unsigned
          ]
        = isLitX 0 arg
        | tcNm == Text.showt ''Index
        = isLitX 1 arg
      isNum0 (coreView1 tcm -> Just t) = isNum0 t
      isNum0 _ = False
  
      isLitX n (LitTy (NumTy m)) = n == m
      isLitX n (coreView1 tcm -> Just t) = isLitX n t
      isLitX _ _ = False
  
    -- Otherwise check whether the entire case-expression has a single
    -- alternative, and pick that one.
    _ -> caseOneAlt e
  
  caseCon' _ e = return e
  {-# SCC caseCon' #-}
  
  {- [Note: Name re-creation]
  The names of heap bound variables are safely generate with mkUniqSystemId in Clash.Core.Evaluator.newLetBinding.
  But only their uniqs end up in the heap, not the complete names.
  So we use mkUnsafeSystemName to recreate the same Name.
  -}
  
  matchLiteralContructor
    :: Term
    -> Literal
    -> [Alt]
    -> NormalizeSession Term
  matchLiteralContructor c (IntegerLiteral l) alts = go (reverse alts)
   where
    go [(DefaultPat,e)] = changed e
    go ((DataPat dc [] [x],e):alts')
      | dcTag dc == 1
      , l >= ((-2)^(63::Int)) &&  l < 2^(63::Int)
      = let fvs = Lens.foldMapOf freeLocalIds unitVarSet e
            bind = NonRec x (Literal (IntLiteral l))
         in if x `elemVarSet` fvs
              then changed (Let bind e)
              else changed e
      | dcTag dc == 2
      , l >= 2^(63::Int)
  #if MIN_VERSION_base(4,15,0)
      = let !(IP ba) = l
  #else
      = let !(Jp# !(BN# ba)) = l
  #endif
            ba'       = BA.ByteArray ba
            fvs       = Lens.foldMapOf freeLocalIds unitVarSet e
            bind      = NonRec x (Literal (ByteArrayLiteral ba'))
         in if x `elemVarSet` fvs
              then changed (Let bind e)
              else changed e
      | dcTag dc == 3
      , l < ((-2)^(63::Int))
  #if MIN_VERSION_base(4,15,0)
      = let !(IN ba) = l
  #else
      = let !(Jn# !(BN# ba)) = l
  #endif
            ba'       = BA.ByteArray ba
            fvs       = Lens.foldMapOf freeLocalIds unitVarSet e
            bind      = NonRec x (Literal (ByteArrayLiteral ba'))
         in if x `elemVarSet` fvs
              then changed (Let bind e)
              else changed e
      | otherwise
      = go alts'
    go ((LitPat l', e):alts')
      | IntegerLiteral l == l'
      = changed e
      | otherwise
      = go alts'
    go _ = error $ $(curLoc) ++ "Report as bug: caseCon error: " ++ showPpr c
  
  matchLiteralContructor c (NaturalLiteral l) alts = go (reverse alts)
   where
    go [(DefaultPat,e)] = changed e
    go ((DataPat dc [] [x],e):alts')
      | dcTag dc == 1
      , l >= 0 && l < 2^(64::Int)
      = let fvs       = Lens.foldMapOf freeLocalIds unitVarSet e
            bind      = NonRec x (Literal (WordLiteral l))
         in if x `elemVarSet` fvs
              then changed (Let bind e)
              else changed e
      | dcTag dc == 2
      , l >= 2^(64::Int)
  #if MIN_VERSION_base(4,15,0)
      = let !(IP ba) = l
  #else
      = let !(Jp# !(BN# ba)) = l
  #endif
            ba'       = BA.ByteArray ba
            fvs       = Lens.foldMapOf freeLocalIds unitVarSet e
            bind      = NonRec x (Literal (ByteArrayLiteral ba'))
         in if x `elemVarSet` fvs
              then changed (Let bind e)
              else changed e
      | otherwise
      = go alts'
    go ((LitPat l', e):alts')
      | NaturalLiteral l == l'
      = changed e
      | otherwise
      = go alts'
    go _ = error $ $(curLoc) ++ "Report as bug: caseCon error: " ++ showPpr c
  
  matchLiteralContructor _ _ ((DefaultPat,e):_) = changed e
  matchLiteralContructor c _ _ =
    error $ $(curLoc) ++ "Report as bug: caseCon error: " ++ showPpr c
  {-# SCC matchLiteralContructor #-}
  
  -- | Remove non-reachable alternatives. For example, consider:
  --
  -- @
  -- data STy ty where
  --   SInt :: Int -> STy Int
  --   SBool :: Bool -> STy Bool
  --
  -- f :: STy ty -> ty
  -- f (SInt b) = b + 1
  -- f (SBool True) = False
  -- f (SBool False) = True
  -- {\-\# NOINLINE f \#-\}
  --
  -- g :: STy Int -> Int
  -- g = f
  -- @
  --
  -- @f@ is always specialized on @STy Int@. The SBool alternatives are therefore
  -- unreachable. Additional information can be found at:
  -- https://github.com/clash-lang/clash-compiler/pull/465
  caseElemNonReachable :: HasCallStack => NormRewrite
  caseElemNonReachable _ case0@(Case scrut altsTy alts0) = do
    tcm <- Lens.view tcCache
  
    let (altsAbsurd, altsOther) = List.partition (isAbsurdPat tcm . fst) alts0
    case altsAbsurd of
      [] -> return case0
      _  -> changed =<< caseOneAlt (Case scrut altsTy altsOther)
  
  caseElemNonReachable _ e = return e
  {-# SCC caseElemNonReachable #-}
  
  -- | Flatten ridiculous case-statements generated by GHC
  --
  -- For case-statements in haskell of the form:
  --
  -- @
  -- f :: Unsigned 4 -> Unsigned 4
  -- f x = case x of
  --   0 -> 3
  --   1 -> 2
  --   2 -> 1
  --   3 -> 0
  -- @
  --
  -- GHC generates Core that looks like:
  --
  -- @
  -- f = \\(x :: Unsigned 4) -> case x == fromInteger 3 of
  --                             False -> case x == fromInteger 2 of
  --                               False -> case x == fromInteger 1 of
  --                                 False -> case x == fromInteger 0 of
  --                                   False -> error "incomplete case"
  --                                   True  -> fromInteger 3
  --                                 True -> fromInteger 2
  --                               True -> fromInteger 1
  --                             True -> fromInteger 0
  -- @
  --
  -- Which would result in a priority decoder circuit where a normal decoder
  -- circuit was desired.
  --
  -- This transformation transforms the above Core to the saner:
  --
  -- @
  -- f = \\(x :: Unsigned 4) -> case x of
  --        _ -> error "incomplete case"
  --        0 -> fromInteger 3
  --        1 -> fromInteger 2
  --        2 -> fromInteger 1
  --        3 -> fromInteger 0
  -- @
  caseFlat :: HasCallStack => NormRewrite
  caseFlat (TransformContext is0 _) e@(Case (collectEqArgs -> Just (scrut',val)) ty _) =
    case collectFlat scrut' e of
      Just alts' -> case collectArgs val of
        -- When we're pattern matching on `Int`, extract the `Int#` first before
        -- we do the Literal matching branches.
        (Data dc,_)
          | nameOcc (dcName dc) == "GHC.Types.I#"
          , [argTy] <- dcArgTys dc
          -> do
            wild <- mkInternalVar is0 "wild" argTy
            changed (Case scrut' ty
                      [(DataPat dc [] [wild]
                       ,Case (Var wild) ty (last alts' : init alts'))])
        _ -> changed (Case scrut' ty (last alts' : init alts'))
      Nothing -> return e
  
  caseFlat _ e = return e
  {-# SCC caseFlat #-}
  
  collectFlat :: Term -> Term -> Maybe [Alt]
  collectFlat scrut (Case (collectEqArgs -> Just (scrut', val)) _ty [lAlt,rAlt])
    | scrut' == scrut
    = case collectArgs val of
        (Prim p,args') | isFromInt (primName p) ->
          go (last args')
        (Data dc,args') | nameOcc (dcName dc) == "GHC.Types.I#" ->
          go (last args')
        _ -> Nothing
    where
      go (Left (Literal i)) = case (lAlt,rAlt) of
                ((pl,el),(pr,er))
                  | isFalseDcPat pl || isTrueDcPat pr ->
                     case collectFlat scrut el of
                       Just alts' -> Just ((LitPat i, er) : alts')
                       Nothing    -> Just [(LitPat i, er)
                                          ,(DefaultPat, el)
                                          ]
                  | otherwise ->
                     case collectFlat scrut er of
                       Just alts' -> Just ((LitPat i, el) : alts')
                       Nothing    -> Just [(LitPat i, el)
                                          ,(DefaultPat, er)
                                          ]
      go _ = Nothing
  
      isFalseDcPat (DataPat p _ _)
        = ((== "GHC.Types.False") . nameOcc . dcName) p
      isFalseDcPat _ = False
  
      isTrueDcPat (DataPat p _ _)
        = ((== "GHC.Types.True") . nameOcc . dcName) p
      isTrueDcPat _ = False
  
  collectFlat _ _ = Nothing
  {-# SCC collectFlat #-}
  
  collectEqArgs :: Term -> Maybe (Term,Term)
  collectEqArgs f@(collectArgsTicks -> (Prim p, args, ticks))
    | nm == Text.showt 'BV.eq#
      = case args of
          [_,_,Left scrut,Left val] -> Just (mkTicks scrut ticks,val)
          _ -> error ("collectEqArgs: BV.eq expects 4 arguments, but got: " <> showPpr f)
    | nm == Text.showt 'I.eq#  ||
      nm == Text.showt 'S.eq# ||
      nm == Text.showt 'U.eq#
      = case args of
          [_,Left scrut,Left val] -> Just (mkTicks scrut ticks,val)
          _ -> error (show nm <> " expects 3 arguments, but got: " <> showPpr f)
    | nm == "GHC.Classes.eqInt"
      = case args of
          [Left scrut,Left val] -> Just (mkTicks scrut ticks,val)
          _ -> error ("eqInt expects 2 arguments, but got: " <> showPpr f)
   where
    nm = primName p
  
  collectEqArgs _ = Nothing
  
  -- | Lift the let-bindings out of the subject of a Case-decomposition
  caseLet :: HasCallStack => NormRewrite
  caseLet (TransformContext is0 _) (Case (collectTicks -> (Let xes e,ticks)) ty alts) = do
    -- Note [CaseLet deshadow]
    -- Imagine
    --
    -- @
    -- case (let x = u in e) of {p -> a}
    -- @
    --
    -- where `a` has a free variable named `x`.
    --
    -- Simply transforming the above to:
    --
    -- @
    -- let x = u in case e of {p -> a}
    -- @
    --
    -- would be very bad, because now the let-binding captures the free x variable
    -- in a.
    --
    -- We must therefor rename `x` so that it doesn't capture the free variables
    -- in the alternative:
    --
    -- @
    -- let x1 = u[x:=x1] in case e[x:=x1] of {p -> a}
    -- @
    --
    -- It is safe to over-approximate the free variables in `a` by simply taking
    -- the current InScopeSet.
    let (xes1,e1) = deshadowLetExpr is0 xes e
    changed (Let (fmap (`mkTicks` ticks) xes1)
                    (Case (mkTicks e1 ticks) ty alts))
  
  caseLet _ e = return e
  {-# SCC caseLet #-}
  
  caseOneAlt :: Term -> NormalizeSession Term
  caseOneAlt e@(Case _ _ [(pat,altE)]) =
    case pat of
      DefaultPat -> changed altE
      LitPat _ -> changed altE
      DataPat _ tvs xs
        | (coerce tvs ++ coerce xs) `localVarsDoNotOccurIn` altE
        -> changed altE
        | otherwise
        -> return e
  
  caseOneAlt (Case _ _ ((pat,alt):alts@(_:_)))
    | all ((== alt) . snd) alts
    , (tvs,xs) <- patIds pat
    , (coerce tvs ++ coerce xs) `localVarsDoNotOccurIn` alt
    = changed alt
  
  caseOneAlt e = return e
  {-# SCC caseOneAlt #-}
  
  -- | Tries to eliminate existentials by using heuristics to determine what the
  -- existential should be. For example, consider Vec:
  --
  --    data Vec :: Nat -> Type -> Type where
  --      Nil       :: Vec 0 a
  --      Cons x xs :: a -> Vec n a -> Vec (n + 1) a
  --
  -- Thus, 'null' (annotated with existentials) could look like:
  --
  --    null :: forall n . Vec n Bool -> Bool
  --    null v =
  --      case v of
  --        Nil  {n ~ 0}                                     -> True
  --        Cons {n1:Nat} {n~n1+1} (x :: a) (xs :: Vec n1 a) -> False
  --
  -- When it's applied to a vector of length 5, this becomes:
  --
  --    null :: Vec 5 Bool -> Bool
  --    null v =
  --      case v of
  --        Nil  {5 ~ 0}                                     -> True
  --        Cons {n1:Nat} {5~n1+1} (x :: a) (xs :: Vec n1 a) -> False
  --
  -- This function solves 'n1' and replaces every occurrence with its solution. A
  -- very limited number of solutions are currently recognized: only adds (such
  -- as in the example) will be solved.
  elimExistentials :: HasCallStack => NormRewrite
  elimExistentials (TransformContext is0 _) (Case scrut altsTy alts0) = do
    tcm <- Lens.view tcCache
    alts1 <- traverse (go is0 tcm) alts0
    caseOneAlt (Case scrut altsTy alts1)
   where
      -- Eliminate free type variables if possible
      go :: InScopeSet -> TyConMap -> Alt -> NormalizeSession Alt
      go is2 tcm alt@(pat@(DataPat dc exts0 xs0), term0) =
        case solveNonAbsurds tcm (mkVarSet exts0) (patEqs tcm pat) of
          -- No equations solved:
          [] -> return alt
          -- One or more equations solved:
          sols ->
            changed =<< go is2 tcm (DataPat dc exts1 xs1, term1)
            where
              -- Substitute solution in existentials and applied types
              is3 = extendInScopeSetList is2 exts0
              xs1 = fmap (substTyInVar (extendTvSubstList (mkSubst is3) sols)) xs0
              exts1 = substInExistentialsList is2 exts0 sols
  
              -- Substitute solution in term.
              is4 = extendInScopeSetList is3 xs1
              subst = extendTvSubstList (mkSubst is4) sols
              term1 = substTm "Replacing tyVar due to solved eq" subst term0
  
      go _ _ alt = return alt
  
  elimExistentials _ e = return e
  {-# SCC elimExistentials #-}
  