    {-|
      Copyright   :  (C) 2012-2016, University of Twente,
                              2017, Google Inc.
                              2021, QBayLogic B.V.
      License     :  BSD2 (see the file LICENSE)
      Maintainer  :  QBayLogic B.V. <devops@qbaylogic.com>

      Capture-free substitution function for CoreHW
    -}

    {-# LANGUAGE CPP #-}
    {-# LANGUAGE LambdaCase #-}
    {-# LANGUAGE OverloadedStrings #-}
    {-# LANGUAGE StandaloneDeriving #-}
    {-# LANGUAGE UndecidableInstances #-}

    {-# OPTIONS_GHC -fno-warn-orphans #-}

    #include "../../ClashDebug.h"

    module Clash.Core.Subst
      ( -- * Substitution into types
        -- ** Substitution environments
        TvSubst (..)
      , TvSubstEnv
      -- , mkTvSubst
      , extendTvSubst
      , extendTvSubstList
        -- ** Applying substitutions
      , substTy
      , substTyWith
      , substTyInVar
      , substGlobalsInExistentials
      , substInExistentials
      , substInExistentialsList
        -- * Substitution into terms
        -- ** Substitution environments
      , Subst (..)
      , mkSubst
      , mkTvSubst
      , extendInScopeId
      , extendInScopeIdList
      , extendIdSubst
      , extendIdSubstList
      , extendGblSubstList
        -- ** Applying substitutions
      , substTm
      , maybeSubstTm
      , substAlt
      , substId
        -- * Variable renaming
      , deShadowTerm
      , deShadowAlt
      , freshenTm
      , deshadowLetExpr
        -- * Alpha equivalence
      , aeqType
      , aeqTerm
        -- * Structural equivalence
      , eqTerm
      , eqType
      )
    where

    import           Data.Coerce               (coerce)

    #if MIN_VERSION_prettyprinter(1,7,0)
    import           Prettyprinter
    #else
    import           Data.Text.Prettyprint.Doc
    #endif

    import           Data.Hashable             (Hashable (hashWithSalt))
    import qualified Data.List                 as List
    import qualified Data.List.Extra           as List
    import           Data.Ord                  (comparing)
    import           GHC.Stack                 (HasCallStack)
    import           GHC.SrcLoc.Extra          ()
    import           GHC.TypeLits
      (TypeError, ErrorMessage (Text, (:<>:)))

    import           Clash.Core.HasFreeVars
    import           Clash.Core.Pretty         (ppr, fromPpr)
    import           Clash.Core.Term
      (Bind(..), Pat (..), Term (..), TickInfo (..), PrimInfo(primName))
    import           Clash.Core.Type           (Type (..))
    import           Clash.Core.VarEnv
    import           Clash.Core.Var            (Id, Var (..), TyVar, isGlobalId)
    import qualified Clash.Data.UniqMap as UniqMap
    import           Clash.Debug               (debugIsOn)
    import           Clash.Util
    import           Clash.Pretty

    -- * Subst

    -- | A substitution of 'Type's for 'TyVar's
    --
    -- Note [Extending the TvSubstEnv]
    -- See 'TvSubst' for the invariants that must hold
    --
    -- This invariant allows a short-cut when the subst env is empty: if the
    -- TvSubstEnv is empty, i.e. @nullVarEnv TvSubstEnv@ holds, then
    -- (substTy subst ty) does nothing.
    --
    -- For example, consider:
    --
    --    (/\a -> /\b(a ~ Int) -> ... b ...) Int
    --
    -- We substitute Int for 'a'. The Unique of 'b' does not change, but
    -- nevertheless we add 'b' to the 'TvSubstEnv' because b's kind does change
    --
    -- This invariant has several consequences:
    --
    --   * In 'substTyVarBndr', we extend TvSubstEnv if the unique has changed, or
    --     if the kind has changed
    --
    --   * In 'substTyVar', we do not need to consult the 'InScopeSet'; the
    --     TvSubstEnv is enough
    --
    --   * In 'substTy', we can short-circuit when TvSubstEnv is empty
    type TvSubstEnv = VarEnv Type

    -- | Type substitution
    --
    -- The following invariants must hold:
    --
    --   1. The 'InScopeSet' is needed only to guide the generation of fresh uniques
    --
    --   2. In particular, the kind of the type variables in the 'InScopeSet' is not
    --      relevant.
    --
    --   3. The substitution is only applied once
    --
    -- Note [Apply Once]
    --
    -- We might instantiate @forall a b. ty@ with the types @[a, b]@ or @[b, a]@.
    -- So the substitution might go like @[a -> b, b -> a]@. A similar situation
    -- arises in terms when we find a redex like @(/\a -> /\b -> e) b a@. Then we
    -- also end up with a substitution that permutes variables. Other variations
    -- happen to; for example @[a -> (a,b)]@.
    --
    -- SO A TvSubst MUST BE APPLIED PRECISELY ONCE, OR THINGS MIGHT LOOP
    --
    -- Note [The substitution invariant]
    --
    -- When calling (substTy subst ty) it should be the case that the 'InScopeSet'
    -- is a superset of both:
    --
    --   * The free variables of the range of the substitution
    --
    --   * The free variables of /ty/ minus the domain of the substitution
    data TvSubst
      = TvSubst InScopeSet -- Variable in scope /after/ substitution
                TvSubstEnv -- Substitution for types

    instance ClashPretty TvSubst where
      clashPretty :: TvSubst -> Doc ()
    clashPretty (TvSubst InScopeSet
    ins TvSubstEnv
    tenv) =
        Doc () -> Doc ()
    forall ann. Doc ann -> Doc ann
    brackets (Doc () -> Doc ()) -> Doc () -> Doc ()
    forall a b. (a -> b) -> a -> b
    $ [Doc ()] -> Doc ()
    forall ann. [Doc ann] -> Doc ann
    sep [ Doc ()
    "TvSubst"
                       , Int -> Doc () -> Doc ()
    forall ann. Int -> Doc ann -> Doc ann
    nest Int
    2 (Doc ()
    "In scope:" Doc () -> Doc () -> Doc ()
    forall ann. Doc ann -> Doc ann -> Doc ann
    <+> InScopeSet -> Doc ()
    forall a. ClashPretty a => a -> Doc ()
    clashPretty InScopeSet
    ins)
                       , Int -> Doc () -> Doc ()
    forall ann. Int -> Doc ann -> Doc ann
    nest Int
    2 (Doc ()
    "Type env:" Doc () -> Doc () -> Doc ()
    forall ann. Doc ann -> Doc ann -> Doc ann
    <+> TvSubstEnv -> Doc ()
    forall a. ClashPretty a => a -> Doc ()
    clashPretty TvSubstEnv
    tenv)]

    -- | A substitution  of 'Term's for 'Id's
    --
    -- Note [Extending the Subst]
    --
    -- For a term 'Subst', which binds 'Id's as well, we make a different choice for
    -- Ids than we do for TyVars.
    --
    -- For TyVars see 'TvSubstEnv's Note [Extending the TvSubstEnv]
    --
    -- For Ids, we have a different invariant:
    --
    --   The IdSubstEnv is extended only when the Unique on an Id changes.
    --   Otherwise, we just extend the InScopeSet
    --
    -- In consequence:
    --
    --   * If all subst envs are empty, substsTm would be a no-op
    --
    --     However, substTm still goes ahead and substitutes. Reason: we may want
    --     to replace existing Ids with new ones from the in-scope set, to avoid
    --     space leaks.
    --
    --   * In substIdBndr, we extend the 'IdSubstEnv' only when the unique changes
    --
    --   * If TvSubstEnv and IdSubstEnv are all empty, substExpr does nothing
    --     (Note that the above rule for 'substIdBndr' maintains this property.)
    --
    --   * In 'lookupIdSubst', we must look up the Id in the in-scope set, because
    --     it may contain non-trivial changes. Exmaple:
    --
    --     (/\a -> \x:a. ... x ...) Int
    --
    --     We extend the 'TvSubstEnv' with a @[a |-> Int]@; but x's unique does not
    --     change so we only extend the in-scope set. Then we must look up in the
    --     in-scope set when we find the occurrence of x.
    --
    --   * The requirement to look  up the Id in the in-scope set means that we
    --     must not take no-op short cut when the 'IdSubstEnv' is empty. We must
    --     still look up ever Id in the in-scope set.
    --
    --   * (However, we don't need to do so for the expression found in the
    --     IdSubstEnv, whose range is assumed to be correct wrt the in-scope set)
    type IdSubstEnv = VarEnv Term

    -- | A substitution environment containing containing both 'Id' and 'TyVar'
    -- substitutions.
    --
    -- Some invariants apply to how you use the substitution:
    --
    --   1. The 'InScopeSet' contains at least those 'Id's and 'TyVar's that will
    --      be in scope /after/ applying the substitution  to a term. Precisely,
    --      the in-scope set must be a superset of the free variables of the
    --      substitution range that might possibly clash with locally-bound
    --      variables in the thing being substituted in.
    --
    --   2. You may only apply the substitution once. See 'TvSubst'
    --
    -- There are various ways of setting up the in-scope set such that the first of
    -- of these invariants holds:
    --
    --   * Arrange that the in-scope set really is all the things in scope
    --
    --   * Arrange that it's the  free vars of the range of the substitution
    --
    --   * Make it empty, if you know that all the free variables of the
    --     substitution are fresh, and hence can´t possibly clash
    data Subst
      = Subst
      { Subst -> InScopeSet
    substInScope :: InScopeSet -- Variables in scope /after/ substitution
      , Subst -> IdSubstEnv
    substTmEnv   :: IdSubstEnv -- Substitution for terms
      , Subst -> TvSubstEnv
    substTyEnv   :: TvSubstEnv -- Substitution for types
      , Subst -> IdSubstEnv
    substGblEnv  :: IdSubstEnv -- Substitution of globals (in terms)
      }

    emptySubst
      :: Subst
    emptySubst :: Subst
    emptySubst = InScopeSet -> IdSubstEnv -> TvSubstEnv -> IdSubstEnv -> Subst
    Subst InScopeSet
    emptyInScopeSet IdSubstEnv
    forall a. VarEnv a
    emptyVarEnv TvSubstEnv
    forall a. VarEnv a
    emptyVarEnv IdSubstEnv
    forall a. VarEnv a
    emptyVarEnv

    -- | An empty substitution, starting the variables currently in scope
    mkSubst
      :: InScopeSet
      -> Subst
    mkSubst :: InScopeSet -> Subst
    mkSubst InScopeSet
    is = InScopeSet -> IdSubstEnv -> TvSubstEnv -> IdSubstEnv -> Subst
    Subst InScopeSet
    is IdSubstEnv
    forall a. VarEnv a
    emptyVarEnv TvSubstEnv
    forall a. VarEnv a
    emptyVarEnv IdSubstEnv
    forall a. VarEnv a
    emptyVarEnv

    -- | Create a type substitution
    mkTvSubst
      :: InScopeSet
      -> VarEnv Type
      -> Subst
    mkTvSubst :: InScopeSet -> TvSubstEnv -> Subst
    mkTvSubst InScopeSet
    is TvSubstEnv
    env = InScopeSet -> IdSubstEnv -> TvSubstEnv -> IdSubstEnv -> Subst
    Subst InScopeSet
    is IdSubstEnv
    forall a. VarEnv a
    emptyVarEnv TvSubstEnv
    env IdSubstEnv
    forall a. VarEnv a
    emptyVarEnv

    -- | Generates the in-scope set for the 'Subst' from the types in the incoming
    -- environment.
    --
    -- Should only be used the type we're substituting into has no free variables
    -- outside of the domain of substitution
    zipTvSubst
      :: [TyVar]
      -> [Type]
      -> Subst
    zipTvSubst :: [TyVar] -> [Type] -> Subst
    zipTvSubst [TyVar]
    tvs [Type]
    tys
      | Bool
    debugIsOn
      , Bool -> Bool
    not ([TyVar] -> [Type] -> Bool
    forall a b. [a] -> [b] -> Bool
    List.equalLength [TyVar]
    tvs [Type]
    tys)
      = String -> Doc ClashAnnotation -> Subst -> Subst
    forall ann a. String -> Doc ann -> a -> a
    pprTrace String
    "zipTvSubst" ([TyVar] -> Doc ClashAnnotation
    forall p. PrettyPrec p => p -> Doc ClashAnnotation
    ppr [TyVar]
    tvs Doc ClashAnnotation -> Doc ClashAnnotation -> Doc ClashAnnotation
    forall a. Semigroup a => a -> a -> a
    <> Doc ClashAnnotation
    forall ann. Doc ann
    line Doc ClashAnnotation -> Doc ClashAnnotation -> Doc ClashAnnotation
    forall a. Semigroup a => a -> a -> a
    <> [Type] -> Doc ClashAnnotation
    forall p. PrettyPrec p => p -> Doc ClashAnnotation
    ppr [Type]
    tys) Subst
    emptySubst
      | Bool
    otherwise
      = InScopeSet -> IdSubstEnv -> TvSubstEnv -> IdSubstEnv -> Subst
    Subst (VarSet -> InScopeSet
    mkInScopeSet ([Type] -> VarSet
    forall a. HasFreeVars a => a -> VarSet
    freeVarsOf [Type]
    tys)) IdSubstEnv
    forall a. VarEnv a
    emptyVarEnv TvSubstEnv
    tenv IdSubstEnv
    forall a. VarEnv a
    emptyVarEnv
     where
      tenv :: TvSubstEnv
    tenv = [TyVar] -> [Type] -> TvSubstEnv
    zipTyEnv [TyVar]
    tvs [Type]
    tys

    zipTyEnv
      :: [TyVar]
      -> [Type]
      -> VarEnv Type
    zipTyEnv :: [TyVar] -> [Type] -> TvSubstEnv
    zipTyEnv [TyVar]
    tvs [Type]
    tys = [(TyVar, Type)] -> TvSubstEnv
    forall a b. [(Var a, b)] -> VarEnv b
    mkVarEnv ([TyVar] -> [Type] -> [(TyVar, Type)]
    forall a b. [a] -> [b] -> [(a, b)]
    List.zipEqual [TyVar]
    tvs [Type]
    tys)

    -- | Extend the substitution environment with a new 'Id' substitution
    extendIdSubst
      :: Subst
      -> Id
      -> Term
      -> Subst
    extendIdSubst :: Subst -> Id -> Term -> Subst
    extendIdSubst (Subst InScopeSet
    is IdSubstEnv
    env TvSubstEnv
    tenv IdSubstEnv
    genv) Id
    i Term
    e =
      InScopeSet -> IdSubstEnv -> TvSubstEnv -> IdSubstEnv -> Subst
    Subst InScopeSet
    is (Id -> Term -> IdSubstEnv -> IdSubstEnv
    forall b a. Var b -> a -> VarEnv a -> VarEnv a
    extendVarEnv Id
    i Term
    e IdSubstEnv
    env) TvSubstEnv
    tenv IdSubstEnv
    genv

    -- | Extend the substitution environment with a list of 'Id' substitutions
    extendIdSubstList
      :: Subst
      -> [(Id,Term)]
      -> Subst
    extendIdSubstList :: Subst -> [(Id, Term)] -> Subst
    extendIdSubstList (Subst InScopeSet
    is IdSubstEnv
    env TvSubstEnv
    tenv IdSubstEnv
    genv) [(Id, Term)]
    es =
      InScopeSet -> IdSubstEnv -> TvSubstEnv -> IdSubstEnv -> Subst
    Subst InScopeSet
    is (IdSubstEnv -> [(Id, Term)] -> IdSubstEnv
    forall a b. VarEnv a -> [(Var b, a)] -> VarEnv a
    extendVarEnvList IdSubstEnv
    env [(Id, Term)]
    es) TvSubstEnv
    tenv IdSubstEnv
    genv

    -- | Extend the substitution environment with a list of global 'Id' substitutions
    extendGblSubstList
      :: Subst
      -> [(Id,Term)]
      -> Subst
    extendGblSubstList :: Subst -> [(Id, Term)] -> Subst
    extendGblSubstList (Subst InScopeSet
    is IdSubstEnv
    env TvSubstEnv
    tenv IdSubstEnv
    genv) [(Id, Term)]
    es =
      InScopeSet -> IdSubstEnv -> TvSubstEnv -> IdSubstEnv -> Subst
    Subst InScopeSet
    is IdSubstEnv
    env TvSubstEnv
    tenv (IdSubstEnv -> [(Id, Term)] -> IdSubstEnv
    forall a b. VarEnv a -> [(Var b, a)] -> VarEnv a
    extendVarEnvList IdSubstEnv
    genv [(Id, Term)]
    es)

    -- | Extend the substitution environment with a new 'TyVar' substitution
    extendTvSubst
      :: Subst
      -> TyVar
      -> Type
      -> Subst
    extendTvSubst :: Subst -> TyVar -> Type -> Subst
    extendTvSubst (Subst InScopeSet
    is IdSubstEnv
    env TvSubstEnv
    tenv IdSubstEnv
    genv) TyVar
    tv Type
    t =
      InScopeSet -> IdSubstEnv -> TvSubstEnv -> IdSubstEnv -> Subst
    Subst InScopeSet
    is IdSubstEnv
    env (TyVar -> Type -> TvSubstEnv -> TvSubstEnv
    forall b a. Var b -> a -> VarEnv a -> VarEnv a
    extendVarEnv TyVar
    tv Type
    t TvSubstEnv
    tenv) IdSubstEnv
    genv

    -- | Extend the substitution environment with a list of 'TyVar' substitutions
    extendTvSubstList
      :: Subst
      -> [(TyVar, Type)]
      -> Subst
    extendTvSubstList :: Subst -> [(TyVar, Type)] -> Subst
    extendTvSubstList (Subst InScopeSet
    is IdSubstEnv
    env TvSubstEnv
    tenv IdSubstEnv
    genv) [(TyVar, Type)]
    ts =
      InScopeSet -> IdSubstEnv -> TvSubstEnv -> IdSubstEnv -> Subst
    Subst InScopeSet
    is IdSubstEnv
    env (TvSubstEnv -> [(TyVar, Type)] -> TvSubstEnv
    forall a b. VarEnv a -> [(Var b, a)] -> VarEnv a
    extendVarEnvList TvSubstEnv
    tenv [(TyVar, Type)]
    ts) IdSubstEnv
    genv

    -- | Add an 'Id' to the in-scope set: as a side effect, remove any existing
    -- substitutions for it.
    extendInScopeId
      :: Subst
      -> Id
      -> Subst
    extendInScopeId :: Subst -> Id -> Subst
    extendInScopeId (Subst InScopeSet
    inScope IdSubstEnv
    env TvSubstEnv
    tenv IdSubstEnv
    genv) Id
    id' =
      InScopeSet -> IdSubstEnv -> TvSubstEnv -> IdSubstEnv -> Subst
    Subst InScopeSet
    inScope' IdSubstEnv
    env' TvSubstEnv
    tenv IdSubstEnv
    genv
     where
      inScope' :: InScopeSet
    inScope' = InScopeSet -> Id -> InScopeSet
    forall a. InScopeSet -> Var a -> InScopeSet
    extendInScopeSet InScopeSet
    inScope Id
    id'
      env' :: IdSubstEnv
    env'     = IdSubstEnv -> Id -> IdSubstEnv
    forall a b. VarEnv a -> Var b -> VarEnv a
    delVarEnv IdSubstEnv
    env Id
    id'

    -- | Add 'Id's to the in-scope set. See also 'extendInScopeId'
    extendInScopeIdList
      :: Subst
      -> [Id]
      -> Subst
    extendInScopeIdList :: Subst -> [Id] -> Subst
    extendInScopeIdList (Subst InScopeSet
    inScope IdSubstEnv
    env TvSubstEnv
    tenv IdSubstEnv
    genv) [Id]
    ids =
      InScopeSet -> IdSubstEnv -> TvSubstEnv -> IdSubstEnv -> Subst
    Subst InScopeSet
    inScope' IdSubstEnv
    env' TvSubstEnv
    tenv IdSubstEnv
    genv
     where
      inScope' :: InScopeSet
    inScope' = InScopeSet -> [Id] -> InScopeSet
    forall a. InScopeSet -> [Var a] -> InScopeSet
    extendInScopeSetList InScopeSet
    inScope [Id]
    ids
      env' :: IdSubstEnv
    env'     = IdSubstEnv -> [Id] -> IdSubstEnv
    forall a b. VarEnv a -> [Var b] -> VarEnv a
    delVarEnvList IdSubstEnv
    env [Id]
    ids

    -- | Substitute within a 'Type'
    --
    -- The substitution has to satisfy the invariant described in
    -- 'TvSubst's Note [The substitution environment]
    substTy
      :: HasCallStack
      => Subst
      -> Type
      -> Type
    substTy :: HasCallStack => Subst -> Type -> Type
    substTy (Subst InScopeSet
    inScope IdSubstEnv
    _ TvSubstEnv
    tvS IdSubstEnv
    _) Type
    ty
      | TvSubstEnv -> Bool
    forall a. VarEnv a -> Bool
    nullVarEnv TvSubstEnv
    tvS
      = Type
    ty
      | Bool
    otherwise
      = TvSubst -> [Type] -> Type -> Type
    forall a. HasCallStack => TvSubst -> [Type] -> a -> a
    checkValidSubst TvSubst
    s' [Type
    ty] (HasCallStack => TvSubst -> Type -> Type
    TvSubst -> Type -> Type
    substTy' TvSubst
    s' Type
    ty)
     where
      s' :: TvSubst
    s' = InScopeSet -> TvSubstEnv -> TvSubst
    TvSubst InScopeSet
    inScope TvSubstEnv
    tvS

    -- | Substitute within a 'TyVar'. See 'substTy'.
    substTyInVar
      :: HasCallStack
      => Subst
      -> Var a
      -> Var a
    substTyInVar :: forall a. HasCallStack => Subst -> Var a -> Var a
    substTyInVar Subst
    subst Var a
    tyVar =
      Var a
    tyVar { varType = (substTy subst (varType tyVar)) }

    -- | Like 'substTy', but skips the checks for the invariants described in
    -- 'TvSubts' Note [The substitution environment]. Should be used inside this
    -- module only.
    substTyUnchecked
      :: HasCallStack
      => TvSubst
      -> Type
      -> Type
    substTyUnchecked :: HasCallStack => TvSubst -> Type -> Type
    substTyUnchecked subst :: TvSubst
    subst@(TvSubst InScopeSet
    _ TvSubstEnv
    tvS) Type
    ty
      | TvSubstEnv -> Bool
    forall a. VarEnv a -> Bool
    nullVarEnv TvSubstEnv
    tvS
      = Type
    ty
      | Bool
    otherwise
      = HasCallStack => TvSubst -> Type -> Type
    TvSubst -> Type -> Type
    substTy' TvSubst
    subst Type
    ty

    -- Safely substitute global type variables in a list of potentially
    -- shadowing type variables.
    substGlobalsInExistentials
      :: HasCallStack
      => InScopeSet
      -- ^ Variables in scope
      -> [TyVar]
      -- ^ List of existentials to apply the substitution for
      -> [(TyVar, Type)]
      -- ^ Substitutions
      -> [TyVar]
    substGlobalsInExistentials :: HasCallStack => InScopeSet -> [TyVar] -> [(TyVar, Type)] -> [TyVar]
    substGlobalsInExistentials InScopeSet
    is [TyVar]
    exts [(TyVar, Type)]
    substs0 = [TyVar]
    result
      -- TODO: Is is actually possible that existentials shadow each other? If they
      -- TODO: can't, we can remove this function
      where
        iss :: [InScopeSet]
    iss     = (InScopeSet -> TyVar -> InScopeSet)
    -> InScopeSet -> [TyVar] -> [InScopeSet]
    forall b a. (b -> a -> b) -> b -> [a] -> [b]
    scanl InScopeSet -> TyVar -> InScopeSet
    forall a. InScopeSet -> Var a -> InScopeSet
    extendInScopeSet InScopeSet
    is [TyVar]
    exts
        substs1 :: [Subst]
    substs1 = (InScopeSet -> Subst) -> [InScopeSet] -> [Subst]
    forall a b. (a -> b) -> [a] -> [b]
    map (\InScopeSet
    is_ -> Subst -> [(TyVar, Type)] -> Subst
    extendTvSubstList (InScopeSet -> Subst
    mkSubst InScopeSet
    is_) [(TyVar, Type)]
    substs0) [InScopeSet]
    iss
        result :: [TyVar]
    result  = (Subst -> TyVar -> TyVar) -> [Subst] -> [TyVar] -> [TyVar]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith Subst -> TyVar -> TyVar
    forall a. HasCallStack => Subst -> Var a -> Var a
    substTyInVar [Subst]
    substs1 [TyVar]
    exts

    -- | Safely substitute type variables in a list of existentials. This function
    -- will account for cases where existentials shadow each other.
    substInExistentialsList
      :: HasCallStack
      => InScopeSet
      -- ^ Variables in scope
      -> [TyVar]
      -- ^ List of existentials to apply the substitution for
      -> [(TyVar, Type)]
      -- ^ Substitutions
      -> [TyVar]
    substInExistentialsList :: HasCallStack => InScopeSet -> [TyVar] -> [(TyVar, Type)] -> [TyVar]
    substInExistentialsList InScopeSet
    is [TyVar]
    exts [(TyVar, Type)]
    substs =
      ([TyVar] -> (TyVar, Type) -> [TyVar])
    -> [TyVar] -> [(TyVar, Type)] -> [TyVar]
    forall b a. (b -> a -> b) -> b -> [a] -> b
    forall (t :: Type -> Type) b a.
    Foldable t =>
    (b -> a -> b) -> b -> t a -> b
    foldl (HasCallStack => InScopeSet -> [TyVar] -> (TyVar, Type) -> [TyVar]
    InScopeSet -> [TyVar] -> (TyVar, Type) -> [TyVar]
    substInExistentials InScopeSet
    is) [TyVar]
    exts [(TyVar, Type)]
    substs

    -- | Safely substitute a type variable in a list of existentials. This function
    -- will account for cases where existentials shadow each other.
    substInExistentials
      :: HasCallStack
      => InScopeSet
      -- ^ Variables in scope
      -> [TyVar]
      -- ^ List of existentials to apply the substitution for
      -> (TyVar, Type)
      -- ^ Substitution
      -> [TyVar]
    substInExistentials :: HasCallStack => InScopeSet -> [TyVar] -> (TyVar, Type) -> [TyVar]
    substInExistentials InScopeSet
    is [TyVar]
    exts subst :: (TyVar, Type)
    subst@(TyVar
    typeVar, Type
    _type) =
      -- TODO: Is is actually possible that existentials shadow each other? If they
      -- TODO: can't, we can remove this function
      case TyVar -> [TyVar] -> [Int]
    forall a. Eq a => a -> [a] -> [Int]
    List.elemIndices TyVar
    typeVar [TyVar]
    exts of
        [] ->
          -- We're not replacing any of the existentials, but a global variable
          HasCallStack => InScopeSet -> [TyVar] -> [(TyVar, Type)] -> [TyVar]
    InScopeSet -> [TyVar] -> [(TyVar, Type)] -> [TyVar]
    substGlobalsInExistentials InScopeSet
    is [TyVar]
    exts [(TyVar, Type)
    subst]
        ([Int] -> Int
    forall a. HasCallStack => [a] -> a
    last -> Int
    i) ->
          -- We're replacing an existential. That means we're not touching any
          -- variables that were introduced before it. For all variables after it,
          -- it is as we would replace global variables in them.
          Int -> [TyVar] -> [TyVar]
    forall a. Int -> [a] -> [a]
    take (Int
    iInt -> Int -> Int
    forall a. Num a => a -> a -> a
    +Int
    1) [TyVar]
    exts [TyVar] -> [TyVar] -> [TyVar]
    forall a. [a] -> [a] -> [a]
    ++ HasCallStack => InScopeSet -> [TyVar] -> [(TyVar, Type)] -> [TyVar]
    InScopeSet -> [TyVar] -> [(TyVar, Type)] -> [TyVar]
    substGlobalsInExistentials InScopeSet
    is (Int -> [TyVar] -> [TyVar]
    forall a. Int -> [a] -> [a]
    drop (Int
    iInt -> Int -> Int
    forall a. Num a => a -> a -> a
    +Int
    1) [TyVar]
    exts) [(TyVar, Type)
    subst]

    -- | This checks if the substitution satisfies the invariant from 'TvSubst's
    -- Note [The substitution invariant].
    checkValidSubst
      :: HasCallStack
      => TvSubst
      -> [Type]
      -> a
      -> a
    checkValidSubst :: forall a. HasCallStack => TvSubst -> [Type] -> a -> a
    checkValidSubst subst :: TvSubst
    subst@(TvSubst InScopeSet
    inScope TvSubstEnv
    tenv) [Type]
    tys a
    a =
      WARN( not (isValidSubst subst),
            "inScope" <+> clashPretty inScope <> line <>
            "tenv" <+> clashPretty tenv <> line <>
            "tenvFVs" <+> clashPretty (freeVarsOf tenv) <> line <>
            "tys" <+> fromPpr tys)
      WARN( not tysFVsInSope,
           "inScope" <+> clashPretty inScope <> line <>
           "tenv" <+> clashPretty tenv <> line <>
           "tys" <+> fromPpr tys <> line <>
           "needsInScope" <+> clashPretty needsInScope)
      a
    a
     where
      needsInScope :: VarSet
    needsInScope = (Unique -> Type -> VarSet -> VarSet)
    -> VarSet -> TvSubstEnv -> VarSet
    forall a b. (Unique -> a -> b -> b) -> b -> UniqMap a -> b
    UniqMap.foldrWithUnique (\Unique
    k Type
    _ VarSet
    s -> Unique -> VarSet -> VarSet
    delVarSetByKey Unique
    k VarSet
    s)
                       ([Type] -> VarSet
    forall a. HasFreeVars a => a -> VarSet
    freeVarsOf [Type]
    tys)
                       TvSubstEnv
    tenv
      tysFVsInSope :: Bool
    tysFVsInSope = VarSet
    needsInScope VarSet -> InScopeSet -> Bool
    `varSetInScope` InScopeSet
    inScope

    -- | When calling 'substTy' it should be the case that the in-scope set in the
    -- substitution is a superset of the free variables of the range of the
    -- substitution.
    --
    -- See also 'TvSubst's Note [The substitution invariant].
    isValidSubst
      :: TvSubst
      -> Bool
    isValidSubst :: TvSubst -> Bool
    isValidSubst (TvSubst InScopeSet
    inScope TvSubstEnv
    tenv) = VarSet
    tenvFVs VarSet -> InScopeSet -> Bool
    `varSetInScope` InScopeSet
    inScope
     where
      tenvFVs :: VarSet
    tenvFVs = TvSubstEnv -> VarSet
    forall a. HasFreeVars a => a -> VarSet
    freeVarsOf TvSubstEnv
    tenv

    -- | The work-horse of 'substTy'
    substTy'
      :: HasCallStack
      => TvSubst
      -> Type
      -> Type
    substTy' :: HasCallStack => TvSubst -> Type -> Type
    substTy' TvSubst
    subst = Type -> Type
    go where
      go :: Type -> Type
    go = \case
        VarTy TyVar
    tv -> TvSubst -> TyVar -> Type
    substTyVar TvSubst
    subst TyVar
    tv
        ForAllTy TyVar
    tv Type
    ty -> case TvSubst -> TyVar -> (TvSubst, TyVar)
    substTyVarBndr TvSubst
    subst TyVar
    tv of
          (TvSubst
    subst', TyVar
    tv') -> TyVar -> Type -> Type
    ForAllTy TyVar
    tv' (HasCallStack => TvSubst -> Type -> Type
    TvSubst -> Type -> Type
    substTy' TvSubst
    subst' Type
    ty)
        AppTy Type
    fun Type
    arg -> Type -> Type -> Type
    AppTy (Type -> Type
    go Type
    fun) (Type -> Type
    go Type
    arg)
        Type
    ty -> Type
    ty

    -- | Substitute a variable with a type if it's within the substitution's domain.
    --
    -- Does not substitute within the kind of free variables.
    substTyVar
      :: TvSubst
      -> TyVar
      -> Type
    substTyVar :: TvSubst -> TyVar -> Type
    substTyVar (TvSubst InScopeSet
    _ TvSubstEnv
    tenv) TyVar
    tv = case TyVar -> TvSubstEnv -> Maybe Type
    forall b a. Var b -> VarEnv a -> Maybe a
    lookupVarEnv TyVar
    tv TvSubstEnv
    tenv of
      Just Type
    ty -> Type
    ty
      Maybe Type
    _       -> TyVar -> Type
    VarTy TyVar
    tv

    -- | Substitute a type variable in a binding position, returning an extended
    -- substitution environment and a new type variable.
    --
    -- Substitutes within the kind of the type variable
    substTyVarBndr
      :: TvSubst
      -> TyVar
      -> (TvSubst, TyVar)
    substTyVarBndr :: TvSubst -> TyVar -> (TvSubst, TyVar)
    substTyVarBndr subst :: TvSubst
    subst@(TvSubst InScopeSet
    inScope TvSubstEnv
    tenv) TyVar
    oldVar =
      ASSERT2( no_capture, clashPretty oldVar <> line
                        <> clashPretty newVar <> line
                        <> clashPretty subst )
      (InScopeSet -> TvSubstEnv -> TvSubst
    TvSubst (InScopeSet
    inScope InScopeSet -> TyVar -> InScopeSet
    forall a. InScopeSet -> Var a -> InScopeSet
    `extendInScopeSet` TyVar
    newVar) TvSubstEnv
    newEnv, TyVar
    newVar)
     where
      newEnv :: TvSubstEnv
    newEnv | Bool
    noChange  = TvSubstEnv -> TyVar -> TvSubstEnv
    forall a b. VarEnv a -> Var b -> VarEnv a
    delVarEnv TvSubstEnv
    tenv TyVar
    oldVar
             | Bool
    otherwise = TyVar -> Type -> TvSubstEnv -> TvSubstEnv
    forall b a. Var b -> a -> VarEnv a -> VarEnv a
    extendVarEnv TyVar
    oldVar (TyVar -> Type
    VarTy TyVar
    newVar) TvSubstEnv
    tenv

      -- Assertion that we're not capturing something in the substitution
      no_capture :: Bool
    no_capture = Bool -> Bool
    not (TyVar
    newVar TyVar -> VarSet -> Bool
    forall a. Var a -> VarSet -> Bool
    `elemVarSet` TvSubstEnv -> VarSet
    forall a. HasFreeVars a => a -> VarSet
    freeVarsOf TvSubstEnv
    tenv)

      oldKi :: Type
    oldKi        = TyVar -> Type
    forall a. Var a -> Type
    varType TyVar
    oldVar
      -- verify that the kind is closed
      noKindChange :: Bool
    noKindChange = Type -> Bool
    forall a. HasFreeVars a => a -> Bool
    isClosed Type
    oldKi
      -- noChange means that the new type variable is identical in all respects to
      -- the old type variable (same unique, same kind)
      -- See 'TvSubstEnv's Note [Extending the TvSubstEnv]
      --
      -- In that case we don't need to extend the substitution to map old to new.
      -- But instead we must zap any current substitution for the variable. For
      -- example
      --
      --   (\x.e) with subst = [x | -> e']
      --
      -- Here we must simply zap the substitution for x
      noChange :: Bool
    noChange     = Bool
    noKindChange Bool -> Bool -> Bool
    && (TyVar
    newVar TyVar -> TyVar -> Bool
    forall a. Eq a => a -> a -> Bool
    == TyVar
    oldVar)

      -- uniqAway ensures that the new variable is not already in scope
      newVar :: TyVar
    newVar | Bool
    noKindChange = InScopeSet -> TyVar -> TyVar
    forall a. (Uniquable a, ClashPretty a) => InScopeSet -> a -> a
    uniqAway InScopeSet
    inScope TyVar
    oldVar
             | Bool
    otherwise    = InScopeSet -> TyVar -> TyVar
    forall a. (Uniquable a, ClashPretty a) => InScopeSet -> a -> a
    uniqAway InScopeSet
    inScope
                                (TyVar
    oldVar {varType = substTyUnchecked subst oldKi})

    -- | Substitute within a 'Term'. Just return original term if given
    -- substitution is "Nothing".
    maybeSubstTm
      :: HasCallStack
      => Doc ()
      -> Maybe Subst
      -> Term
      -> Term
    maybeSubstTm :: HasCallStack => Doc () -> Maybe Subst -> Term -> Term
    maybeSubstTm Doc ()
    _doc Maybe Subst
    Nothing = Term -> Term
    forall a. a -> a
    id
    maybeSubstTm Doc ()
    doc (Just Subst
    s) = HasCallStack => Doc () -> Subst -> Term -> Term
    Doc () -> Subst -> Term -> Term
    substTm Doc ()
    doc Subst
    s

    -- | Substitute within a 'Term'
    substTm
      :: HasCallStack
      => Doc ()
      -> Subst
      -> Term
      -> Term
    substTm :: HasCallStack => Doc () -> Subst -> Term -> Term
    substTm Doc ()
    doc Subst
    subst = Term -> Term
    go where
      go :: Term -> Term
    go = \case
        Var Id
    v -> HasCallStack => Doc () -> Subst -> Id -> Term
    Doc () -> Subst -> Id -> Term
    lookupIdSubst (Doc ()
    doc Doc () -> Doc () -> Doc ()
    forall a. Semigroup a => a -> a -> a
    <> Doc ()
    forall ann. Doc ann
    line Doc () -> Doc () -> Doc ()
    forall a. Semigroup a => a -> a -> a
    <> Doc ()
    "subsTm") Subst
    subst Id
    v
        Lam Id
    v Term
    e -> case HasCallStack => Subst -> Id -> (Subst, Id)
    Subst -> Id -> (Subst, Id)
    substIdBndr Subst
    subst Id
    v of
          (Subst
    subst',Id
    v') -> Id -> Term -> Term
    Lam Id
    v' (HasCallStack => Doc () -> Subst -> Term -> Term
    Doc () -> Subst -> Term -> Term
    substTm Doc ()
    doc Subst
    subst' Term
    e)
        TyLam TyVar
    v Term
    e -> case HasCallStack => Subst -> TyVar -> (Subst, TyVar)
    Subst -> TyVar -> (Subst, TyVar)
    substTyVarBndr' Subst
    subst TyVar
    v of
          (Subst
    subst',TyVar
    v') -> TyVar -> Term -> Term
    TyLam TyVar
    v' (HasCallStack => Doc () -> Subst -> Term -> Term
    Doc () -> Subst -> Term -> Term
    substTm Doc ()
    doc Subst
    subst' Term
    e)
        App Term
    l Term
    r -> Term -> Term -> Term
    App (Term -> Term
    go Term
    l) (Term -> Term
    go Term
    r)
        TyApp Term
    l Type
    r -> Term -> Type -> Term
    TyApp (Term -> Term
    go Term
    l) (HasCallStack => Subst -> Type -> Type
    Subst -> Type -> Type
    substTy Subst
    subst Type
    r)
        Let Bind Term
    bs Term
    e -> case HasCallStack => Doc () -> Subst -> Bind Term -> (Subst, Bind Term)
    Doc () -> Subst -> Bind Term -> (Subst, Bind Term)
    substBind Doc ()
    doc Subst
    subst Bind Term
    bs of
          (Subst
    subst',Bind Term
    bs') -> Bind Term -> Term -> Term
    Let Bind Term
    bs' (HasCallStack => Doc () -> Subst -> Term -> Term
    Doc () -> Subst -> Term -> Term
    substTm Doc ()
    doc Subst
    subst' Term
    e)
        Case Term
    subj Type
    ty [Alt]
    alts -> Term -> Type -> [Alt] -> Term
    Case (Term -> Term
    go Term
    subj) (HasCallStack => Subst -> Type -> Type
    Subst -> Type -> Type
    substTy Subst
    subst Type
    ty) ((Alt -> Alt) -> [Alt] -> [Alt]
    forall a b. (a -> b) -> [a] -> [b]
    map Alt -> Alt
    goAlt [Alt]
    alts)
        Cast Term
    e Type
    t1 Type
    t2 -> Term -> Type -> Type -> Term
    Cast (Term -> Term
    go Term
    e) (HasCallStack => Subst -> Type -> Type
    Subst -> Type -> Type
    substTy Subst
    subst Type
    t1) (HasCallStack => Subst -> Type -> Type
    Subst -> Type -> Type
    substTy Subst
    subst Type
    t2)
        Tick TickInfo
    tick Term
    e -> TickInfo -> Term -> Term
    Tick (TickInfo -> TickInfo
    goTick TickInfo
    tick) (Term -> Term
    go Term
    e)
        Term
    tm -> Term
    tm

      goAlt :: Alt -> Alt
    goAlt (Pat
    pat,Term
    alt) = case Pat
    pat of
        DataPat DataCon
    dc [TyVar]
    tvs [Id]
    ids -> case (Subst -> TyVar -> (Subst, TyVar))
    -> Subst -> [TyVar] -> (Subst, [TyVar])
    forall (t :: Type -> Type) s a b.
    Traversable t =>
    (s -> a -> (s, b)) -> s -> t a -> (s, t b)
    List.mapAccumL HasCallStack => Subst -> TyVar -> (Subst, TyVar)
    Subst -> TyVar -> (Subst, TyVar)
    substTyVarBndr' Subst
    subst [TyVar]
    tvs of
          (Subst
    subst1,[TyVar]
    tvs') -> case (Subst -> Id -> (Subst, Id)) -> Subst -> [Id] -> (Subst, [Id])
    forall (t :: Type -> Type) s a b.
    Traversable t =>
    (s -> a -> (s, b)) -> s -> t a -> (s, t b)
    List.mapAccumL HasCallStack => Subst -> Id -> (Subst, Id)
    Subst -> Id -> (Subst, Id)
    substIdBndr Subst
    subst1 [Id]
    ids of
            (Subst
    subst2,[Id]
    ids') -> (DataCon -> [TyVar] -> [Id] -> Pat
    DataPat DataCon
    dc [TyVar]
    tvs' [Id]
    ids',HasCallStack => Doc () -> Subst -> Term -> Term
    Doc () -> Subst -> Term -> Term
    substTm Doc ()
    doc Subst
    subst2 Term
    alt)
        Pat
    _ -> (Pat
    pat,Term -> Term
    go Term
    alt)

      goTick :: TickInfo -> TickInfo
    goTick t :: TickInfo
    t@(SrcSpan SrcSpan
    _)  = TickInfo
    t
      goTick (NameMod NameMod
    m Type
    ty) = NameMod -> Type -> TickInfo
    NameMod NameMod
    m (HasCallStack => Subst -> Type -> Type
    Subst -> Type -> Type
    substTy Subst
    subst Type
    ty)
      goTick t :: TickInfo
    t@TickInfo
    DeDup        = TickInfo
    t
      goTick t :: TickInfo
    t@TickInfo
    NoDeDup      = TickInfo
    t

    -- | Substitute within a case-alternative
    substAlt
      :: HasCallStack
      => Doc ()
      -> Subst
      -- ^ The substitution
      -> (Pat, Term)
      -- ^ The alternative in which to apply the substitution
      -> (Pat, Term)
    substAlt :: HasCallStack => Doc () -> Subst -> Alt -> Alt
    substAlt Doc ()
    doc Subst
    subst (Pat
    pat,Term
    alt) = case Pat
    pat of
      DataPat DataCon
    dc [TyVar]
    tvs [Id]
    ids -> case (Subst -> TyVar -> (Subst, TyVar))
    -> Subst -> [TyVar] -> (Subst, [TyVar])
    forall (t :: Type -> Type) s a b.
    Traversable t =>
    (s -> a -> (s, b)) -> s -> t a -> (s, t b)
    List.mapAccumL HasCallStack => Subst -> TyVar -> (Subst, TyVar)
    Subst -> TyVar -> (Subst, TyVar)
    substTyVarBndr' Subst
    subst [TyVar]
    tvs of
        (Subst
    subst1,[TyVar]
    tvs1) -> case (Subst -> Id -> (Subst, Id)) -> Subst -> [Id] -> (Subst, [Id])
    forall (t :: Type -> Type) s a b.
    Traversable t =>
    (s -> a -> (s, b)) -> s -> t a -> (s, t b)
    List.mapAccumL HasCallStack => Subst -> Id -> (Subst, Id)
    Subst -> Id -> (Subst, Id)
    substIdBndr Subst
    subst1 [Id]
    ids of
          (Subst
    subst2,[Id]
    ids1) -> (DataCon -> [TyVar] -> [Id] -> Pat
    DataPat DataCon
    dc [TyVar]
    tvs1 [Id]
    ids1,HasCallStack => Doc () -> Subst -> Term -> Term
    Doc () -> Subst -> Term -> Term
    substTm Doc ()
    doc Subst
    subst2 Term
    alt)
      Pat
    _ -> (Pat
    pat, HasCallStack => Doc () -> Subst -> Term -> Term
    Doc () -> Subst -> Term -> Term
    substTm Doc ()
    doc Subst
    subst Term
    alt)

    substId
      :: HasCallStack
      => Subst
      -> Id
      -> Id
    substId :: HasCallStack => Subst -> Id -> Id
    substId Subst
    subst Id
    oldId = (Subst, Id) -> Id
    forall a b. (a, b) -> b
    snd ((Subst, Id) -> Id) -> (Subst, Id) -> Id
    forall a b. (a -> b) -> a -> b
    $ HasCallStack => Subst -> Id -> (Subst, Id)
    Subst -> Id -> (Subst, Id)
    substIdBndr Subst
    subst Id
    oldId

    -- | Find the substitution for an 'Id' in the 'Subst'
    lookupIdSubst
      :: HasCallStack
      => Doc ()
      -> Subst
      -> Id
      -> Term
    lookupIdSubst :: HasCallStack => Doc () -> Subst -> Id -> Term
    lookupIdSubst Doc ()
    doc (Subst InScopeSet
    inScope IdSubstEnv
    tmS TvSubstEnv
    _ IdSubstEnv
    genv) Id
    v
      | Id -> Bool
    forall a. Var a -> Bool
    isGlobalId Id
    v = case Id -> IdSubstEnv -> Maybe Term
    forall b a. Var b -> VarEnv a -> Maybe a
    lookupVarEnv Id
    v IdSubstEnv
    genv of
                         Just Term
    e -> Term
    e
                         Maybe Term
    _      -> Id -> Term
    Var Id
    v
      | Just Term
    e <- Id -> IdSubstEnv -> Maybe Term
    forall b a. Var b -> VarEnv a -> Maybe a
    lookupVarEnv Id
    v IdSubstEnv
    tmS = Term
    e
      -- Vital! See 'IdSubstEnv' Note [Extending the Subst]
      --
      -- TODO: We match on Id here to workaround an issue where type variables
      -- TODO: "shadow" term variables. Omitting the check would make 'lookupIdSubst'
      -- TODO: potentially replace an "Id" with a TyVar. For more information:
      -- TODO:
      -- TODO:   https://github.com/clash-lang/clash-compiler/issues/1046
      -- TODO:
      | Just v' :: Var Any
    v'@(Id {}) <- InScopeSet -> Id -> Maybe (Var Any)
    forall a. InScopeSet -> Var a -> Maybe (Var Any)
    lookupInScope InScopeSet
    inScope Id
    v = Id -> Term
    Var (Var Any -> Id
    forall a b. Coercible a b => a -> b
    coerce Var Any
    v')
      | Bool
    otherwise = WARN(True, "Subst.lookupIdSubst" <+> doc <+> fromPpr v)
                    Id -> Term
    Var Id
    v

    -- | Substitute an 'Id' for another one according to the 'Subst' given,
    -- returning the result and an update 'Subst' that should be used in subsequent
    -- substitutions.
    substIdBndr
      :: HasCallStack
      => Subst
      -> Id
      -> (Subst,Id)
    substIdBndr :: HasCallStack => Subst -> Id -> (Subst, Id)
    substIdBndr subst :: Subst
    subst@(Subst InScopeSet
    inScope IdSubstEnv
    env TvSubstEnv
    tenv IdSubstEnv
    genv) Id
    oldId =
      (InScopeSet -> IdSubstEnv -> TvSubstEnv -> IdSubstEnv -> Subst
    Subst (InScopeSet
    inScope InScopeSet -> Id -> InScopeSet
    forall a. InScopeSet -> Var a -> InScopeSet
    `extendInScopeSet` Id
    newId) IdSubstEnv
    newEnv TvSubstEnv
    tenv IdSubstEnv
    genv, Id
    newId)
     where
      id1 :: Id
    id1 = InScopeSet -> Id -> Id
    forall a. (Uniquable a, ClashPretty a) => InScopeSet -> a -> a
    uniqAway InScopeSet
    inScope Id
    oldId
      newId :: Id
    newId | Bool
    noTypeChange = Id
    id1
            | Bool
    otherwise    = Id
    id1 {varType = substTy subst (varType id1)}

      oldTy :: Type
    oldTy = Id -> Type
    forall a. Var a -> Type
    varType Id
    oldId
      noTypeChange :: Bool
    noTypeChange = TvSubstEnv -> Bool
    forall a. VarEnv a -> Bool
    nullVarEnv TvSubstEnv
    tenv Bool -> Bool -> Bool
    || Type -> Bool
    forall a. HasFreeVars a => a -> Bool
    isClosed Type
    oldTy

      -- Extend the substitution if the unique has changed.
      --
      -- In case it hasn't changed we don't need to extend the substitution to map
      -- old to new. But instead we must zap any current substitution for the
      -- variable. For example
      --
      --   (\x.e) with subst = [x | -> e']
      --
      -- Here we must simply zap the substitution for x
      newEnv :: IdSubstEnv
    newEnv | Bool
    noChange  = IdSubstEnv -> Id -> IdSubstEnv
    forall a b. VarEnv a -> Var b -> VarEnv a
    delVarEnv IdSubstEnv
    env Id
    oldId
             | Bool
    otherwise = Id -> Term -> IdSubstEnv -> IdSubstEnv
    forall b a. Var b -> a -> VarEnv a -> VarEnv a
    extendVarEnv Id
    oldId (Id -> Term
    Var Id
    newId) IdSubstEnv
    env

      -- See Note [Extending the Subst] why it's not necessary to check noTypeChange
      noChange :: Bool
    noChange = Id
    id1 Id -> Id -> Bool
    forall a. Eq a => a -> a -> Bool
    == Id
    oldId

    -- | Like 'substTyVarBndr' but takes a 'Subst' instead of a 'TvSubst'
    substTyVarBndr'
      :: HasCallStack
      => Subst
      -> TyVar
      -> (Subst,TyVar)
    substTyVarBndr' :: HasCallStack => Subst -> TyVar -> (Subst, TyVar)
    substTyVarBndr' (Subst InScopeSet
    inScope IdSubstEnv
    tmS TvSubstEnv
    tyS IdSubstEnv
    tgS) TyVar
    tv =
      case TvSubst -> TyVar -> (TvSubst, TyVar)
    substTyVarBndr (InScopeSet -> TvSubstEnv -> TvSubst
    TvSubst InScopeSet
    inScope TvSubstEnv
    tyS) TyVar
    tv of
        (TvSubst InScopeSet
    inScope' TvSubstEnv
    tyS',TyVar
    tv') -> (InScopeSet -> IdSubstEnv -> TvSubstEnv -> IdSubstEnv -> Subst
    Subst InScopeSet
    inScope' IdSubstEnv
    tmS TvSubstEnv
    tyS' IdSubstEnv
    tgS, TyVar
    tv')

    -- | Apply a substitution to an entire set of let-bindings, additionally
    -- returning an updated 'Subst' that should be used by subsequent substitutions.
    substBind
      :: HasCallStack
      => Doc ()
      -> Subst
      -> Bind Term
      -> (Subst, Bind Term)
    substBind :: HasCallStack => Doc () -> Subst -> Bind Term -> (Subst, Bind Term)
    substBind Doc ()
    doc Subst
    subst (NonRec Id
    i Term
    x) =
      (Subst
    subst', Id -> Term -> Bind Term
    forall a. Id -> a -> Bind a
    NonRec Id
    i' Term
    x')
     where
      (Subst
    subst', Id
    i') = HasCallStack => Subst -> Id -> (Subst, Id)
    Subst -> Id -> (Subst, Id)
    substIdBndr Subst
    subst Id
    i
      x' :: Term
    x' = HasCallStack => Doc () -> Subst -> Term -> Term
    Doc () -> Subst -> Term -> Term
    substTm (Doc ()
    "substBind" Doc () -> Doc () -> Doc ()
    forall ann. Doc ann -> Doc ann -> Doc ann
    <+> Doc ()
    doc) Subst
    subst Term
    x

    substBind Doc ()
    doc Subst
    subst (Rec [(Id, Term)]
    xs) =
      (Subst
    subst', [(Id, Term)] -> Bind Term
    forall a. [(Id, a)] -> Bind a
    Rec ([Id] -> [Term] -> [(Id, Term)]
    forall a b. [a] -> [b] -> [(a, b)]
    zip [Id]
    bndrs' [Term]
    rhss'))
     where
      ([Id]
    bndrs,[Term]
    rhss)    = [(Id, Term)] -> ([Id], [Term])
    forall a b. [(a, b)] -> ([a], [b])
    unzip [(Id, Term)]
    xs
      (Subst
    subst',[Id]
    bndrs') = (Subst -> Id -> (Subst, Id)) -> Subst -> [Id] -> (Subst, [Id])
    forall (t :: Type -> Type) s a b.
    Traversable t =>
    (s -> a -> (s, b)) -> s -> t a -> (s, t b)
    List.mapAccumL HasCallStack => Subst -> Id -> (Subst, Id)
    Subst -> Id -> (Subst, Id)
    substIdBndr Subst
    subst [Id]
    bndrs
      rhss' :: [Term]
    rhss'           = (Term -> Term) -> [Term] -> [Term]
    forall a b. (a -> b) -> [a] -> [b]
    map (HasCallStack => Doc () -> Subst -> Term -> Term
    Doc () -> Subst -> Term -> Term
    substTm (Doc ()
    "substBind" Doc () -> Doc () -> Doc ()
    forall ann. Doc ann -> Doc ann -> Doc ann
    <+> Doc ()
    doc) Subst
    subst') [Term]
    rhss

    -- | Type substitution, see 'zipTvSubst'
    --
    -- Works only if the domain of the substitution is superset of the type being
    -- substituted into
    substTyWith
      :: HasCallStack
      => [TyVar]
      -> [Type]
      -> Type
      -> Type
    substTyWith :: HasCallStack => [TyVar] -> [Type] -> Type -> Type
    substTyWith [TyVar]
    tvs [Type]
    tys =
      ASSERT( List.equalLength tvs tys )
      HasCallStack => Subst -> Type -> Type
    Subst -> Type -> Type
    substTy ([TyVar] -> [Type] -> Subst
    zipTvSubst [TyVar]
    tvs [Type]
    tys)

    -- | Ensure that non of the binders in an expression shadow each-other, nor
    -- conflict with he in-scope set
    deShadowTerm
      :: HasCallStack
      => InScopeSet
      -> Term
      -> Term
    deShadowTerm :: HasCallStack => InScopeSet -> Term -> Term
    deShadowTerm InScopeSet
    is Term
    e = HasCallStack => Doc () -> Subst -> Term -> Term
    Doc () -> Subst -> Term -> Term
    substTm Doc ()
    "deShadowTerm" (InScopeSet -> Subst
    mkSubst InScopeSet
    is) Term
    e

    -- | Ensure that non of the binders in an alternative shadow each-other, nor
    -- conflict with the in-scope set
    deShadowAlt ::
      HasCallStack =>
      InScopeSet ->
      (Pat, Term) ->
      (Pat, Term)
    deShadowAlt :: HasCallStack => InScopeSet -> Alt -> Alt
    deShadowAlt InScopeSet
    is = HasCallStack => Doc () -> Subst -> Alt -> Alt
    Doc () -> Subst -> Alt -> Alt
    substAlt Doc ()
    "deShadowAlt" (InScopeSet -> Subst
    mkSubst InScopeSet
    is)

    -- | Ensure that non of the let-bindings of a let-expression shadow w.r.t the
    -- in-scope set
    deshadowLetExpr
      :: HasCallStack
      => InScopeSet
      -- ^ Current InScopeSet
      -> Bind Term
      -- ^ Bindings of the let-expression
      -> Term
      -- ^ The body of the let-expression
      -> (Bind Term, Term)
      -- ^ Deshadowed let-bindings, where let-bound expressions and the let-body
      -- properly reference the renamed variables
    deshadowLetExpr :: HasCallStack =>
    InScopeSet -> Bind Term -> Term -> (Bind Term, Term)
    deshadowLetExpr InScopeSet
    is Bind Term
    bs Term
    e =
      case HasCallStack => Doc () -> Subst -> Bind Term -> (Subst, Bind Term)
    Doc () -> Subst -> Bind Term -> (Subst, Bind Term)
    substBind Doc ()
    "deshadowLetBindings" (InScopeSet -> Subst
    mkSubst InScopeSet
    is) Bind Term
    bs of
        (Subst
    s1,Bind Term
    bs1) -> (Bind Term
    bs1, HasCallStack => Doc () -> Subst -> Term -> Term
    Doc () -> Subst -> Term -> Term
    substTm Doc ()
    "deShadowLetBody" Subst
    s1 Term
    e)

    -- | A much stronger variant of `deShadowTerm` that ensures that all bound
    -- variables are unique.
    --
    -- Also returns an extended 'InScopeSet' additionally containing the (renamed)
    -- unique bound variables of the term.
    freshenTm
      :: InScopeSet
      -- ^ Current set of variables in scope
      -> Term
      -> (InScopeSet, Term)
    freshenTm :: InScopeSet -> Term -> (InScopeSet, Term)
    freshenTm InScopeSet
    is0 = Subst -> Term -> (InScopeSet, Term)
    go (InScopeSet -> Subst
    mkSubst InScopeSet
    is0) where
      go :: Subst -> Term -> (InScopeSet, Term)
    go Subst
    subst0 = \case
        Var Id
    v -> (Subst -> InScopeSet
    substInScope Subst
    subst0, HasCallStack => Doc () -> Subst -> Id -> Term
    Doc () -> Subst -> Id -> Term
    lookupIdSubst Doc ()
    "freshenTm" Subst
    subst0 Id
    v)
        Lam Id
    v Term
    e -> case HasCallStack => Subst -> Id -> (Subst, Id)
    Subst -> Id -> (Subst, Id)
    substIdBndr Subst
    subst0 Id
    v of
          (Subst
    subst1,Id
    v') -> case Subst -> Term -> (InScopeSet, Term)
    go Subst
    subst1 Term
    e of
            (InScopeSet
    is2,Term
    e') -> (InScopeSet
    is2, Id -> Term -> Term
    Lam Id
    v' Term
    e')
        TyLam TyVar
    v Term
    e -> case HasCallStack => Subst -> TyVar -> (Subst, TyVar)
    Subst -> TyVar -> (Subst, TyVar)
    substTyVarBndr' Subst
    subst0 TyVar
    v of
          (Subst
    subst1,TyVar
    v') -> case Subst -> Term -> (InScopeSet, Term)
    go Subst
    subst1 Term
    e of
            (InScopeSet
    is2,Term
    e') -> (InScopeSet
    is2,TyVar -> Term -> Term
    TyLam TyVar
    v' Term
    e')
        App Term
    l Term
    r -> case Subst -> Term -> (InScopeSet, Term)
    go Subst
    subst0 Term
    l of
          (InScopeSet
    is1,Term
    l') -> case Subst -> Term -> (InScopeSet, Term)
    go Subst
    subst0 {substInScope = is1} Term
    r of
            (InScopeSet
    is2,Term
    r') -> (InScopeSet
    is2, Term -> Term -> Term
    App Term
    l' Term
    r')
        TyApp Term
    l Type
    r -> case Subst -> Term -> (InScopeSet, Term)
    go Subst
    subst0 Term
    l of
          (InScopeSet
    is1,Term
    l') -> (InScopeSet
    is1, Term -> Type -> Term
    TyApp Term
    l' (HasCallStack => Subst -> Type -> Type
    Subst -> Type -> Type
    substTy Subst
    subst0 Type
    r))
        Let Bind Term
    bs Term
    e -> case Subst -> Bind Term -> (Subst, Bind Term)
    goBind Subst
    subst0 Bind Term
    bs of
          (Subst
    subst1,Bind Term
    bs') -> case Subst -> Term -> (InScopeSet, Term)
    go Subst
    subst1 Term
    e of
            (InScopeSet
    is2,Term
    e') -> (InScopeSet
    is2,Bind Term -> Term -> Term
    Let Bind Term
    bs' Term
    e')
        Case Term
    subj Type
    ty [Alt]
    alts -> case Subst -> Term -> (InScopeSet, Term)
    go Subst
    subst0 Term
    subj of
          (InScopeSet
    is1,Term
    subj') -> case (InScopeSet -> Alt -> (InScopeSet, Alt))
    -> InScopeSet -> [Alt] -> (InScopeSet, [Alt])
    forall (t :: Type -> Type) s a b.
    Traversable t =>
    (s -> a -> (s, b)) -> s -> t a -> (s, t b)
    List.mapAccumL (\InScopeSet
    isN -> Subst -> Alt -> (InScopeSet, Alt)
    goAlt Subst
    subst0 {substInScope = isN}) InScopeSet
    is1 [Alt]
    alts of
            (InScopeSet
    is2,[Alt]
    alts') -> (InScopeSet
    is2, Term -> Type -> [Alt] -> Term
    Case Term
    subj' (HasCallStack => Subst -> Type -> Type
    Subst -> Type -> Type
    substTy Subst
    subst0 Type
    ty) [Alt]
    alts')
        Cast Term
    e Type
    t1 Type
    t2 -> case Subst -> Term -> (InScopeSet, Term)
    go Subst
    subst0 Term
    e of
          (InScopeSet
    is1, Term
    e') -> (InScopeSet
    is1, Term -> Type -> Type -> Term
    Cast Term
    e' (HasCallStack => Subst -> Type -> Type
    Subst -> Type -> Type
    substTy Subst
    subst0 Type
    t1) (HasCallStack => Subst -> Type -> Type
    Subst -> Type -> Type
    substTy Subst
    subst0 Type
    t2))
        Tick TickInfo
    tick Term
    e -> case Subst -> Term -> (InScopeSet, Term)
    go Subst
    subst0 Term
    e of
           (InScopeSet
    is1, Term
    e') -> (InScopeSet
    is1, TickInfo -> Term -> Term
    Tick (Subst -> TickInfo -> TickInfo
    goTick Subst
    subst0 TickInfo
    tick) Term
    e')
        Term
    tm -> (Subst -> InScopeSet
    substInScope Subst
    subst0, Term
    tm)

      goBind :: Subst -> Bind Term -> (Subst, Bind Term)
    goBind Subst
    subst0 (NonRec Id
    i Term
    x) =
        let (Subst
    subst1, Id
    i') = HasCallStack => Subst -> Id -> (Subst, Id)
    Subst -> Id -> (Subst, Id)
    substIdBndr Subst
    subst0 Id
    i
            (InScopeSet
    is2, Term
    x') = Subst -> Term -> (InScopeSet, Term)
    go Subst
    subst0 Term
    x
         in (Subst
    subst1 { substInScope = extendInScopeSet is2 i' }, Id -> Term -> Bind Term
    forall a. Id -> a -> Bind a
    NonRec Id
    i' Term
    x')

      goBind Subst
    subst0 (Rec [(Id, Term)]
    xs) =
        let ([Id]
    bndrs,[Term]
    rhss)    = [(Id, Term)] -> ([Id], [Term])
    forall a b. [(a, b)] -> ([a], [b])
    unzip [(Id, Term)]
    xs
            (Subst
    subst1,[Id]
    bndrs') = (Subst -> Id -> (Subst, Id)) -> Subst -> [Id] -> (Subst, [Id])
    forall (t :: Type -> Type) s a b.
    Traversable t =>
    (s -> a -> (s, b)) -> s -> t a -> (s, t b)
    List.mapAccumL HasCallStack => Subst -> Id -> (Subst, Id)
    Subst -> Id -> (Subst, Id)
    substIdBndr Subst
    subst0 [Id]
    bndrs
            (InScopeSet
    is2,[Term]
    rhss')     = (InScopeSet -> Term -> (InScopeSet, Term))
    -> InScopeSet -> [Term] -> (InScopeSet, [Term])
    forall (t :: Type -> Type) s a b.
    Traversable t =>
    (s -> a -> (s, b)) -> s -> t a -> (s, t b)
    List.mapAccumL (\InScopeSet
    isN -> Subst -> Term -> (InScopeSet, Term)
    go Subst
    subst1 {substInScope = isN})
                                             (Subst -> InScopeSet
    substInScope Subst
    subst1)
                                             [Term]
    rhss
        in  (Subst
    subst1 {substInScope = is2}, [(Id, Term)] -> Bind Term
    forall a. [(Id, a)] -> Bind a
    Rec ([(Id, Term)] -> Bind Term) -> [(Id, Term)] -> Bind Term
    forall a b. (a -> b) -> a -> b
    $ [Id] -> [Term] -> [(Id, Term)]
    forall a b. [a] -> [b] -> [(a, b)]
    zip [Id]
    bndrs' [Term]
    rhss')

      goAlt :: Subst -> Alt -> (InScopeSet, Alt)
    goAlt Subst
    subst0 (Pat
    pat,Term
    alt) = case Pat
    pat of
        DataPat DataCon
    dc [TyVar]
    tvs [Id]
    ids -> case (Subst -> TyVar -> (Subst, TyVar))
    -> Subst -> [TyVar] -> (Subst, [TyVar])
    forall (t :: Type -> Type) s a b.
    Traversable t =>
    (s -> a -> (s, b)) -> s -> t a -> (s, t b)
    List.mapAccumL HasCallStack => Subst -> TyVar -> (Subst, TyVar)
    Subst -> TyVar -> (Subst, TyVar)
    substTyVarBndr' Subst
    subst0 [TyVar]
    tvs of
          (Subst
    subst1,[TyVar]
    tvs') -> case (Subst -> Id -> (Subst, Id)) -> Subst -> [Id] -> (Subst, [Id])
    forall (t :: Type -> Type) s a b.
    Traversable t =>
    (s -> a -> (s, b)) -> s -> t a -> (s, t b)
    List.mapAccumL HasCallStack => Subst -> Id -> (Subst, Id)
    Subst -> Id -> (Subst, Id)
    substIdBndr Subst
    subst1 [Id]
    ids of
            (Subst
    subst2,[Id]
    ids') -> case Subst -> Term -> (InScopeSet, Term)
    go Subst
    subst2 Term
    alt of
              (InScopeSet
    is3,Term
    alt') -> (InScopeSet
    is3,(DataCon -> [TyVar] -> [Id] -> Pat
    DataPat DataCon
    dc [TyVar]
    tvs' [Id]
    ids',Term
    alt'))
        Pat
    _ -> case Subst -> Term -> (InScopeSet, Term)
    go Subst
    subst0 Term
    alt of
          (InScopeSet
    is1,Term
    alt') -> (InScopeSet
    is1,(Pat
    pat,Term
    alt'))

      goTick :: Subst -> TickInfo -> TickInfo
    goTick Subst
    subst0 (NameMod NameMod
    m Type
    ty) = NameMod -> Type -> TickInfo
    NameMod NameMod
    m (HasCallStack => Subst -> Type -> Type
    Subst -> Type -> Type
    substTy Subst
    subst0 Type
    ty)
      goTick Subst
    _      TickInfo
    tick           = TickInfo
    tick

    -- * AEQ

    -- | Alpha equality for types
    aeqType
      :: Type
      -> Type
      -> Bool
    aeqType :: Type -> Type -> Bool
    aeqType Type
    t1 Type
    t2 = RnEnv -> Type -> Type -> Ordering
    acmpType' RnEnv
    rnEnv Type
    t1 Type
    t2 Ordering -> Ordering -> Bool
    forall a. Eq a => a -> a -> Bool
    == Ordering
    EQ
     where
      rnEnv :: RnEnv
    rnEnv = InScopeSet -> RnEnv
    mkRnEnv (VarSet -> InScopeSet
    mkInScopeSet ([Type] -> VarSet
    forall a. HasFreeVars a => a -> VarSet
    freeVarsOf [Type
    t1,Type
    t2]))

    -- | Alpha comparison for types
    acmpType
      :: Type
      -> Type
      -> Ordering
    acmpType :: Type -> Type -> Ordering
    acmpType Type
    t1 Type
    t2 = RnEnv -> Type -> Type -> Ordering
    acmpType' (InScopeSet -> RnEnv
    mkRnEnv InScopeSet
    inScope) Type
    t1 Type
    t2
     where
      inScope :: InScopeSet
    inScope = VarSet -> InScopeSet
    mkInScopeSet ([Type] -> VarSet
    forall a. HasFreeVars a => a -> VarSet
    freeVarsOf [Type
    t1,Type
    t2])

    -- | Alpha comparison for types. Faster than 'acmpType' as it doesn't need to
    -- calculate the free variables to create the 'InScopeSet'
    acmpType'
      :: RnEnv
      -> Type
      -> Type
      -> Ordering
    acmpType' :: RnEnv -> Type -> Type -> Ordering
    acmpType' = RnEnv -> Type -> Type -> Ordering
    go
     where
      go :: RnEnv -> Type -> Type -> Ordering
    go RnEnv
    env (VarTy TyVar
    tv1) (VarTy TyVar
    tv2) = TyVar -> TyVar -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare (RnEnv -> TyVar -> TyVar
    rnOccLTy RnEnv
    env TyVar
    tv1) (RnEnv -> TyVar -> TyVar
    rnOccRTy RnEnv
    env TyVar
    tv2)
      go RnEnv
    _   (ConstTy ConstTy
    c1) (ConstTy ConstTy
    c2) = ConstTy -> ConstTy -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare ConstTy
    c1 ConstTy
    c2
      go RnEnv
    env (ForAllTy TyVar
    tv1 Type
    t1) (ForAllTy TyVar
    tv2 Type
    t2) =
        RnEnv -> Type -> Type -> Ordering
    go RnEnv
    env (TyVar -> Type
    forall a. Var a -> Type
    varType TyVar
    tv1) (TyVar -> Type
    forall a. Var a -> Type
    varType TyVar
    tv2) Ordering -> Ordering -> Ordering
    `thenCompare` RnEnv -> Type -> Type -> Ordering
    go (RnEnv -> TyVar -> TyVar -> RnEnv
    rnTyBndr RnEnv
    env TyVar
    tv1 TyVar
    tv2) Type
    t1 Type
    t2
      go RnEnv
    env (AppTy Type
    s1 Type
    t1) (AppTy Type
    s2 Type
    t2) =
        RnEnv -> Type -> Type -> Ordering
    go RnEnv
    env Type
    s1 Type
    s2 Ordering -> Ordering -> Ordering
    `thenCompare` RnEnv -> Type -> Type -> Ordering
    go RnEnv
    env Type
    t1 Type
    t2
      go RnEnv
    _ (LitTy LitTy
    l1) (LitTy LitTy
    l2) = LitTy -> LitTy -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare LitTy
    l1 LitTy
    l2
      go RnEnv
    env (AnnType [Attr Text]
    a1 Type
    t1) (AnnType [Attr Text]
    a2 Type
    t2) =
        [Attr Text] -> [Attr Text] -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare [Attr Text]
    a1 [Attr Text]
    a2 Ordering -> Ordering -> Ordering
    `thenCompare` RnEnv -> Type -> Type -> Ordering
    go RnEnv
    env Type
    t1 Type
    t2
      go RnEnv
    _ Type
    t1 Type
    t2 = Word -> Word -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare (Type -> Word
    getRank Type
    t1) (Type -> Word
    getRank Type
    t2)

      getRank :: Type -> Word
      getRank :: Type -> Word
    getRank (VarTy {})    = Word
    0
      getRank (LitTy {})    = Word
    1
      getRank (ConstTy {})  = Word
    2
      getRank (AnnType {})  = Word
    3
      getRank (AppTy {})    = Word
    4
      getRank (ForAllTy {}) = Word
    5

    -- | Structural equality on 'Type'
    eqType
      :: Type
      -> Type
      -> Bool
    eqType :: Type -> Type -> Bool
    eqType = Type -> Type -> Bool
    go
     where
      go :: Type -> Type -> Bool
    go (VarTy TyVar
    tv1) (VarTy TyVar
    tv2) = TyVar
    tv1 TyVar -> TyVar -> Bool
    forall a. Eq a => a -> a -> Bool
    == TyVar
    tv2
      go (ConstTy ConstTy
    c1) (ConstTy ConstTy
    c2) = ConstTy
    c1 ConstTy -> ConstTy -> Bool
    forall a. Eq a => a -> a -> Bool
    == ConstTy
    c2
      go (ForAllTy TyVar
    tv1 Type
    t1) (ForAllTy TyVar
    tv2 Type
    t2) =
        TyVar
    tv1 TyVar -> TyVar -> Bool
    forall a. Eq a => a -> a -> Bool
    == TyVar
    tv2 Bool -> Bool -> Bool
    && Type -> Type -> Bool
    go (TyVar -> Type
    forall a. Var a -> Type
    varType TyVar
    tv1) (TyVar -> Type
    forall a. Var a -> Type
    varType TyVar
    tv2) Bool -> Bool -> Bool
    && Type -> Type -> Bool
    go Type
    t1 Type
    t2
      go (AppTy Type
    s1 Type
    t1) (AppTy Type
    s2 Type
    t2) = Type -> Type -> Bool
    go Type
    s1 Type
    s2 Bool -> Bool -> Bool
    && Type -> Type -> Bool
    go Type
    t1 Type
    t2
      go (LitTy LitTy
    l1) (LitTy LitTy
    l2) = LitTy
    l1 LitTy -> LitTy -> Bool
    forall a. Eq a => a -> a -> Bool
    == LitTy
    l2
      go (AnnType [Attr Text]
    a1 Type
    t1) (AnnType [Attr Text]
    a2 Type
    t2) = [Attr Text]
    a1 [Attr Text] -> [Attr Text] -> Bool
    forall a. Eq a => a -> a -> Bool
    == [Attr Text]
    a2 Bool -> Bool -> Bool
    && Type -> Type -> Bool
    go Type
    t1 Type
    t2
      go Type
    _ Type
    _ = Bool
    False

    -- | Alpha equality for terms
    aeqTerm
      :: Term
      -> Term
      -> Bool
    aeqTerm :: Term -> Term -> Bool
    aeqTerm Term
    t1 Term
    t2 = InScopeSet -> Term -> Term -> Bool
    aeqTerm' InScopeSet
    inScope Term
    t1 Term
    t2
     where
      inScope :: InScopeSet
    inScope = VarSet -> InScopeSet
    mkInScopeSet ([Term] -> VarSet
    forall a. HasFreeVars a => a -> VarSet
    freeVarsOf [Term
    t1,Term
    t2])

    -- | Alpha equality for terms. Faster than 'aeqTerm' as it doesn't need to
    -- calculate the free variables to create the 'InScopeSet'
    aeqTerm'
      :: InScopeSet
      -- ^ Superset of variables in scope of the left and right term
      -> Term
      -> Term
      -> Bool
    aeqTerm' :: InScopeSet -> Term -> Term -> Bool
    aeqTerm' InScopeSet
    inScope Term
    t1 Term
    t2 = InScopeSet -> Term -> Term -> Ordering
    acmpTerm' InScopeSet
    inScope Term
    t1 Term
    t2 Ordering -> Ordering -> Bool
    forall a. Eq a => a -> a -> Bool
    == Ordering
    EQ

    -- | Alpha comparison for types
    acmpTerm
      :: Term
      -> Term
      -> Ordering
    acmpTerm :: Term -> Term -> Ordering
    acmpTerm Term
    t1 Term
    t2 = InScopeSet -> Term -> Term -> Ordering
    acmpTerm' InScopeSet
    inScope Term
    t1 Term
    t2
     where
      inScope :: InScopeSet
    inScope = VarSet -> InScopeSet
    mkInScopeSet ([Term] -> VarSet
    forall a. HasFreeVars a => a -> VarSet
    freeVarsOf [Term
    t1,Term
    t2])

    -- | Alpha comparison for types. Faster than 'acmpTerm' as it doesn't need to
    -- calculate the free variables to create the 'InScopeSet'
    acmpTerm'
      :: InScopeSet
      -- ^ Superset of variables in scope of the left and right term
      -> Term
      -> Term
      -> Ordering
    acmpTerm' :: InScopeSet -> Term -> Term -> Ordering
    acmpTerm' InScopeSet
    inScope = RnEnv -> Term -> Term -> Ordering
    go (InScopeSet -> RnEnv
    mkRnEnv InScopeSet
    inScope)
     where
      thenCmpTm :: Ordering -> Ordering -> Ordering
    thenCmpTm Ordering
    EQ  Ordering
    rel = Ordering
    rel
      thenCmpTm Ordering
    rel Ordering
    _   = Ordering
    rel

      go :: RnEnv -> Term -> Term -> Ordering
    go RnEnv
    env (Var Id
    id1) (Var Id
    id2)   = Id -> Id -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare (RnEnv -> Id -> Id
    rnOccLId RnEnv
    env Id
    id1) (RnEnv -> Id -> Id
    rnOccRId RnEnv
    env Id
    id2)
      go RnEnv
    _   (Data DataCon
    dc1) (Data DataCon
    dc2) = DataCon -> DataCon -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare DataCon
    dc1 DataCon
    dc2
      go RnEnv
    _   (Literal Literal
    l1) (Literal Literal
    l2) = Literal -> Literal -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare Literal
    l1 Literal
    l2
      go RnEnv
    _   (Prim PrimInfo
    p1) (Prim PrimInfo
    p2) = (PrimInfo -> Text) -> PrimInfo -> PrimInfo -> Ordering
    forall a b. Ord a => (b -> a) -> b -> b -> Ordering
    comparing PrimInfo -> Text
    primName PrimInfo
    p1 PrimInfo
    p2
      go RnEnv
    env (Lam Id
    b1 Term
    e1) (Lam Id
    b2 Term
    e2) =
        RnEnv -> Type -> Type -> Ordering
    acmpType' RnEnv
    env (Id -> Type
    forall a. Var a -> Type
    varType Id
    b1) (Id -> Type
    forall a. Var a -> Type
    varType Id
    b2) Ordering -> Ordering -> Ordering
    `thenCompare`
        RnEnv -> Term -> Term -> Ordering
    go (RnEnv -> Id -> Id -> RnEnv
    rnTmBndr RnEnv
    env Id
    b1 Id
    b2) Term
    e1 Term
    e2
      go RnEnv
    env (TyLam TyVar
    b1 Term
    e1) (TyLam TyVar
    b2 Term
    e2) =
        RnEnv -> Type -> Type -> Ordering
    acmpType' RnEnv
    env (TyVar -> Type
    forall a. Var a -> Type
    varType TyVar
    b1) (TyVar -> Type
    forall a. Var a -> Type
    varType TyVar
    b2) Ordering -> Ordering -> Ordering
    `thenCompare`
        RnEnv -> Term -> Term -> Ordering
    go (RnEnv -> TyVar -> TyVar -> RnEnv
    rnTyBndr RnEnv
    env TyVar
    b1 TyVar
    b2) Term
    e1 Term
    e2
      go RnEnv
    env (App Term
    l1 Term
    r1) (App Term
    l2 Term
    r2) =
        RnEnv -> Term -> Term -> Ordering
    go RnEnv
    env Term
    l1 Term
    l2 Ordering -> Ordering -> Ordering
    `thenCompare` RnEnv -> Term -> Term -> Ordering
    go RnEnv
    env Term
    r1 Term
    r2
      go RnEnv
    env (TyApp Term
    l1 Type
    r1) (TyApp Term
    l2 Type
    r2) =
        RnEnv -> Term -> Term -> Ordering
    go RnEnv
    env Term
    l1 Term
    l2 Ordering -> Ordering -> Ordering
    `thenCompare` RnEnv -> Type -> Type -> Ordering
    acmpType' RnEnv
    env Type
    r1 Type
    r2
      go RnEnv
    env (Let (NonRec Id
    i1 Term
    x1) Term
    e1) (Let (NonRec Id
    i2 Term
    x2) Term
    e2) =
        RnEnv -> Term -> Term -> Ordering
    go RnEnv
    env Term
    x1 Term
    x2 Ordering -> Ordering -> Ordering
    `thenCompare` RnEnv -> Term -> Term -> Ordering
    go (RnEnv -> Id -> Id -> RnEnv
    rnTmBndr RnEnv
    env Id
    i1 Id
    i2) Term
    e1 Term
    e2
      go RnEnv
    env (Let (Rec [(Id, Term)]
    bs1) Term
    e1) (Let (Rec [(Id, Term)]
    bs2) Term
    e2) =
        Int -> Int -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare ([(Id, Term)] -> Int
    forall a. [a] -> Int
    forall (t :: Type -> Type) a. Foldable t => t a -> Int
    length [(Id, Term)]
    bs1) ([(Id, Term)] -> Int
    forall a. [a] -> Int
    forall (t :: Type -> Type) a. Foldable t => t a -> Int
    length [(Id, Term)]
    bs2) Ordering -> Ordering -> Ordering
    `thenCompare`
        (Ordering -> Ordering -> Ordering)
    -> Ordering -> [Ordering] -> Ordering
    forall a b. (a -> b -> b) -> b -> [a] -> b
    forall (t :: Type -> Type) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr Ordering -> Ordering -> Ordering
    thenCmpTm Ordering
    EQ ((Term -> Term -> Ordering) -> [Term] -> [Term] -> [Ordering]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith (RnEnv -> Term -> Term -> Ordering
    go RnEnv
    env') [Term]
    rhs1 [Term]
    rhs2) Ordering -> Ordering -> Ordering
    `thenCompare`
        RnEnv -> Term -> Term -> Ordering
    go RnEnv
    env' Term
    e1 Term
    e2
       where
        ([Id]
    ids1,[Term]
    rhs1) = [(Id, Term)] -> ([Id], [Term])
    forall a b. [(a, b)] -> ([a], [b])
    unzip [(Id, Term)]
    bs1
        ([Id]
    ids2,[Term]
    rhs2) = [(Id, Term)] -> ([Id], [Term])
    forall a b. [(a, b)] -> ([a], [b])
    unzip [(Id, Term)]
    bs2
        env' :: RnEnv
    env' = RnEnv -> [Id] -> [Id] -> RnEnv
    rnTmBndrs RnEnv
    env [Id]
    ids1 [Id]
    ids2
      go RnEnv
    env (Case Term
    e1 Type
    _ [Alt]
    a1) (Case Term
    e2 Type
    _ [Alt]
    a2) =
        Int -> Int -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare ([Alt] -> Int
    forall a. [a] -> Int
    forall (t :: Type -> Type) a. Foldable t => t a -> Int
    length [Alt]
    a1) ([Alt] -> Int
    forall a. [a] -> Int
    forall (t :: Type -> Type) a. Foldable t => t a -> Int
    length [Alt]
    a2) Ordering -> Ordering -> Ordering
    `thenCompare`
        RnEnv -> Term -> Term -> Ordering
    go RnEnv
    env Term
    e1 Term
    e2 Ordering -> Ordering -> Ordering
    `thenCompare`
        (Ordering -> Ordering -> Ordering)
    -> Ordering -> [Ordering] -> Ordering
    forall a b. (a -> b -> b) -> b -> [a] -> b
    forall (t :: Type -> Type) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr Ordering -> Ordering -> Ordering
    thenCmpTm Ordering
    EQ ((Alt -> Alt -> Ordering) -> [Alt] -> [Alt] -> [Ordering]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith (RnEnv -> Alt -> Alt -> Ordering
    goAlt RnEnv
    env) [Alt]
    a1 [Alt]
    a2)
      go RnEnv
    env (Cast Term
    e1 Type
    l1 Type
    r1) (Cast Term
    e2 Type
    l2 Type
    r2) =
        RnEnv -> Term -> Term -> Ordering
    go RnEnv
    env Term
    e1 Term
    e2 Ordering -> Ordering -> Ordering
    `thenCompare`
        RnEnv -> Type -> Type -> Ordering
    acmpType' RnEnv
    env Type
    l1 Type
    l2 Ordering -> Ordering -> Ordering
    `thenCompare`
        RnEnv -> Type -> Type -> Ordering
    acmpType' RnEnv
    env Type
    r1 Type
    r2
      go RnEnv
    env (Tick TickInfo
    t1 Term
    e1) (Tick TickInfo
    t2 Term
    e2) =
        TickInfo -> TickInfo -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare TickInfo
    t1 TickInfo
    t2 Ordering -> Ordering -> Ordering
    `thenCompare` RnEnv -> Term -> Term -> Ordering
    go RnEnv
    env Term
    e1 Term
    e2
      go RnEnv
    _ Term
    e1 Term
    e2 = Word -> Word -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare (Term -> Word
    getRank Term
    e1) (Term -> Word
    getRank Term
    e2)

      goAlt :: RnEnv -> Alt -> Alt -> Ordering
    goAlt RnEnv
    env (DataPat DataCon
    c1 [TyVar]
    tvs1 [Id]
    ids1,Term
    e1) (DataPat DataCon
    c2 [TyVar]
    tvs2 [Id]
    ids2,Term
    e2) =
        DataCon -> DataCon -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare DataCon
    c1 DataCon
    c2 Ordering -> Ordering -> Ordering
    `thenCompare` RnEnv -> Term -> Term -> Ordering
    go RnEnv
    env' Term
    e1 Term
    e2
       where
        env' :: RnEnv
    env' = RnEnv -> [Id] -> [Id] -> RnEnv
    rnTmBndrs (RnEnv -> [TyVar] -> [TyVar] -> RnEnv
    rnTyBndrs RnEnv
    env [TyVar]
    tvs1 [TyVar]
    tvs2) [Id]
    ids1 [Id]
    ids2
      goAlt RnEnv
    env (Pat
    c1,Term
    e1) (Pat
    c2,Term
    e2) =
        Pat -> Pat -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare Pat
    c1 Pat
    c2 Ordering -> Ordering -> Ordering
    `thenCompare` RnEnv -> Term -> Term -> Ordering
    go RnEnv
    env Term
    e1 Term
    e2

      getRank :: Term -> Word
      getRank :: Term -> Word
    getRank = \case
        Var {}     -> Word
    0
        Data {}    -> Word
    1
        Literal {} -> Word
    2
        Prim {}    -> Word
    3
        Cast {}    -> Word
    4
        App {}     -> Word
    5
        TyApp {}   -> Word
    6
        Lam {}     -> Word
    7
        TyLam {}   -> Word
    8
        Let NonRec{} Term
    _ -> Word
    9
        Let Rec{} Term
    _ -> Word
    10
        Case {}    -> Word
    11
        Tick {}    -> Word
    12

    -- | Structural equality on 'Term'
    eqTerm :: Term -> Term -> Bool
    eqTerm :: Term -> Term -> Bool
    eqTerm = Term -> Term -> Bool
    go
     where
      go :: Term -> Term -> Bool
    go (Var Id
    id1) (Var Id
    id2) = Id
    id1 Id -> Id -> Bool
    forall a. Eq a => a -> a -> Bool
    == Id
    id2
      go (Data DataCon
    dc1) (Data DataCon
    dc2) = DataCon
    dc1 DataCon -> DataCon -> Bool
    forall a. Eq a => a -> a -> Bool
    == DataCon
    dc2
      go (Literal Literal
    l1) (Literal Literal
    l2) = Literal
    l1 Literal -> Literal -> Bool
    forall a. Eq a => a -> a -> Bool
    == Literal
    l2
      go (Prim PrimInfo
    p1) (Prim PrimInfo
    p2) = PrimInfo -> Text
    primName PrimInfo
    p1 Text -> Text -> Bool
    forall a. Eq a => a -> a -> Bool
    == PrimInfo -> Text
    primName PrimInfo
    p2
      go (Lam Id
    b1 Term
    e1) (Lam Id
    b2 Term
    e2) =
        Id
    b1 Id -> Id -> Bool
    forall a. Eq a => a -> a -> Bool
    == Id
    b2 Bool -> Bool -> Bool
    && Type -> Type -> Bool
    eqType (Id -> Type
    forall a. Var a -> Type
    varType Id
    b1) (Id -> Type
    forall a. Var a -> Type
    varType Id
    b2) Bool -> Bool -> Bool
    && Term -> Term -> Bool
    go Term
    e1 Term
    e2
      go (TyLam TyVar
    b1 Term
    e1) (TyLam TyVar
    b2 Term
    e2) =
        TyVar
    b1 TyVar -> TyVar -> Bool
    forall a. Eq a => a -> a -> Bool
    == TyVar
    b2 Bool -> Bool -> Bool
    && Type -> Type -> Bool
    eqType (TyVar -> Type
    forall a. Var a -> Type
    varType TyVar
    b1) (TyVar -> Type
    forall a. Var a -> Type
    varType TyVar
    b2) Bool -> Bool -> Bool
    && Term -> Term -> Bool
    go Term
    e1 Term
    e2
      go (App Term
    l1 Term
    r1) (App Term
    l2 Term
    r2) = Term -> Term -> Bool
    go Term
    l1 Term
    l2 Bool -> Bool -> Bool
    && Term -> Term -> Bool
    go Term
    r1 Term
    r2
      go (TyApp Term
    l1 Type
    r1) (TyApp Term
    l2 Type
    r2) = Term -> Term -> Bool
    go Term
    l1 Term
    l2 Bool -> Bool -> Bool
    && Type -> Type -> Bool
    eqType Type
    r1 Type
    r2
      go (Let Bind Term
    bs1 Term
    e1) (Let Bind Term
    bs2 Term
    e2) =
        Term -> Term -> Bool
    go Term
    e1 Term
    e2 Bool -> Bool -> Bool
    &&
        Bind Term -> Bind Term -> Bool
    goBind Bind Term
    bs1 Bind Term
    bs2
       where
        goBind :: Bind Term -> Bind Term -> Bool
    goBind (NonRec Id
    b1 Term
    r1) (NonRec Id
    b2 Term
    r2) =
          -- No need to check types of NonRec bindings, when the RHSs match the
          -- types must be the same.
          Id
    b1 Id -> Id -> Bool
    forall a. Eq a => a -> a -> Bool
    == Id
    b2 Bool -> Bool -> Bool
    && Term -> Term -> Bool
    go Term
    r1 Term
    r2
        goBind (Rec [(Id, Term)]
    brs1) (Rec [(Id, Term)]
    brs2) =
          ((Id, Term) -> (Id, Term) -> Bool)
    -> [(Id, Term)] -> [(Id, Term)] -> Bool
    forall a b. (a -> b -> Bool) -> [a] -> [b] -> Bool
    List.all2
            (\(Id
    b1,Term
    r1) (Id
    b2,Term
    r2) ->
              Id
    b1 Id -> Id -> Bool
    forall a. Eq a => a -> a -> Bool
    == Id
    b2 Bool -> Bool -> Bool
    &&
              -- We need to check the types of Rec bindings, because:
              --
              -- letrec (x : Bool) = x in X
              --
              -- is not structurally equivalent to
              --
              -- letrec (x : Int) = x in x
              Type -> Type -> Bool
    eqType (Id -> Type
    forall a. Var a -> Type
    varType Id
    b1) (Id -> Type
    forall a. Var a -> Type
    varType Id
    b2) Bool -> Bool -> Bool
    &&
              Term -> Term -> Bool
    go Term
    r1 Term
    r2)
            [(Id, Term)]
    brs1 [(Id, Term)]
    brs2
        goBind Bind Term
    _ Bind Term
    _ = Bool
    False
      go (Case Term
    e1 Type
    _ [Alt]
    a1) (Case Term
    e2 Type
    _ [Alt]
    a2) =
        Term -> Term -> Bool
    go Term
    e1 Term
    e2 Bool -> Bool -> Bool
    &&
        (Alt -> Alt -> Bool) -> [Alt] -> [Alt] -> Bool
    forall a b. (a -> b -> Bool) -> [a] -> [b] -> Bool
    List.all2 Alt -> Alt -> Bool
    forall {a}. Eq a => (a, Term) -> (a, Term) -> Bool
    goAlt [Alt]
    a1 [Alt]
    a2
       where
        goAlt :: (a, Term) -> (a, Term) -> Bool
    goAlt (a
    p1,Term
    r1) (a
    p2,Term
    r2) = a
    p1 a -> a -> Bool
    forall a. Eq a => a -> a -> Bool
    == a
    p2 Bool -> Bool -> Bool
    && Term -> Term -> Bool
    go Term
    r1 Term
    r2
      go (Cast Term
    e1 Type
    l1 Type
    r1) (Cast Term
    e2 Type
    l2 Type
    r2) =
        Term -> Term -> Bool
    go Term
    e1 Term
    e2 Bool -> Bool -> Bool
    &&
        Type -> Type -> Bool
    eqType Type
    l1 Type
    l2 Bool -> Bool -> Bool
    &&
        Type -> Type -> Bool
    eqType Type
    r1 Type
    r2
      go (Tick TickInfo
    t1 Term
    e1) (Tick TickInfo
    t2 Term
    e2) = TickInfo
    t1 TickInfo -> TickInfo -> Bool
    forall a. Eq a => a -> a -> Bool
    == TickInfo
    t2 Bool -> Bool -> Bool
    && Term -> Term -> Bool
    go Term
    e1 Term
    e2
      go Term
    _ Term
    _ = Bool
    False

    instance Eq Type where
      == :: Type -> Type -> Bool
    (==) = Type -> Type -> Bool
    aeqType

    instance Ord Type where
      compare :: Type -> Type -> Ordering
    compare = Type -> Type -> Ordering
    acmpType

    instance Eq Term where
      == :: Term -> Term -> Bool
    (==) = Term -> Term -> Bool
    aeqTerm

    instance TypeError (
            'Text "A broken implementation of Hashable Term has been "
      ':<>: 'Text "removed in Clash 1.4.7. If this is an issue for you, please submit "
      ':<>: 'Text "an issue report at https://github.com/clash-lang/clash-compiler/issues."
      ) => Hashable Term where
        hashWithSalt :: Int -> Term -> Int
    hashWithSalt = String -> Int -> Term -> Int
    forall a. HasCallStack => String -> a
    error String
    "Term.hashWithSalt: unreachable"

    instance Ord Term where
      compare :: Term -> Term -> Ordering
    compare = Term -> Term -> Ordering
    acmpTerm