{-# OPTIONS_GHC -Wunused-imports #-}

module Agda.TypeChecking.Monad.Env where

import qualified Data.List as List

import Data.Maybe (fromMaybe)

import Agda.Syntax.Common
import Agda.Syntax.Abstract.Name

import Agda.TypeChecking.Monad.Base

import qualified Agda.Utils.SmallSet as SmallSet

import Agda.Utils.Impossible

-- | Get the name of the current module, if any.
{-# SPECIALIZE currentModule :: TCM ModuleName #-}
{-# SPECIALIZE currentModule :: ReduceM ModuleName #-}
currentModule :: MonadTCEnv m => m ModuleName
currentModule :: forall (m :: * -> *). MonadTCEnv m => m ModuleName
currentModule = Lens' TCEnv ModuleName -> m ModuleName
forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
viewTC (ModuleName -> f ModuleName) -> TCEnv -> f TCEnv
Lens' TCEnv ModuleName
eCurrentModule

{-# INLINE withCurrentModule #-}
-- | Set the name of the current module.
withCurrentModule :: (MonadTCEnv m) => ModuleName -> m a -> m a
withCurrentModule :: forall (m :: * -> *) a. MonadTCEnv m => ModuleName -> m a -> m a
withCurrentModule ModuleName
m = (TCEnv -> TCEnv) -> m a -> m a
forall a. (TCEnv -> TCEnv) -> m a -> m a
forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC ((TCEnv -> TCEnv) -> m a -> m a) -> (TCEnv -> TCEnv) -> m a -> m a
forall a b. (a -> b) -> a -> b
$ ASetter TCEnv TCEnv ModuleName ModuleName
-> ModuleName -> TCEnv -> TCEnv
forall s t a b. ASetter s t a b -> b -> s -> t
set ASetter TCEnv TCEnv ModuleName ModuleName
Lens' TCEnv ModuleName
eCurrentModule ModuleName
m

-- | Get the path of the currently checked file
getCurrentPath :: (MonadTCEnv m, MonadFileId m) => m AbsolutePath
getCurrentPath :: forall (m :: * -> *).
(MonadTCEnv m, MonadFileId m) =>
m AbsolutePath
getCurrentPath = do
  i <- FileId -> Maybe FileId -> FileId
forall a. a -> Maybe a -> a
fromMaybe FileId
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe FileId -> FileId) -> m (Maybe FileId) -> m FileId
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Lens' TCEnv (Maybe FileId) -> m (Maybe FileId)
forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
viewTC (Maybe FileId -> f (Maybe FileId)) -> TCEnv -> f TCEnv
Lens' TCEnv (Maybe FileId)
eCurrentPath
  fileFromId i

-- | Get the number of variables bound by anonymous modules.
{-# SPECIALIZE getAnonymousVariables :: ModuleName -> TCM Nat #-}
{-# SPECIALIZE getAnonymousVariables :: ModuleName -> ReduceM Nat #-}
getAnonymousVariables :: MonadTCEnv m => ModuleName -> m Nat
getAnonymousVariables :: forall (m :: * -> *). MonadTCEnv m => ModuleName -> m Nat
getAnonymousVariables ModuleName
m = do
  ms <- Lens' TCEnv [(ModuleName, Nat)] -> m [(ModuleName, Nat)]
forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
viewTC ([(ModuleName, Nat)] -> f [(ModuleName, Nat)]) -> TCEnv -> f TCEnv
Lens' TCEnv [(ModuleName, Nat)]
eAnonymousModules
  return $ sum [ n | (m', n) <- ms, mnameToList m' `List.isPrefixOf` mnameToList m ]

{-# INLINE withAnonymousModule #-}
-- | Add variables bound by an anonymous module.
withAnonymousModule :: ModuleName -> Nat -> TCM a -> TCM a
withAnonymousModule :: forall a. ModuleName -> Nat -> TCM a -> TCM a
withAnonymousModule ModuleName
m Nat
n =
  (TCEnv -> TCEnv) -> TCMT IO a -> TCMT IO a
forall a. (TCEnv -> TCEnv) -> TCMT IO a -> TCMT IO a
forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC ((TCEnv -> TCEnv) -> TCMT IO a -> TCMT IO a)
-> (TCEnv -> TCEnv) -> TCMT IO a -> TCMT IO a
forall a b. (a -> b) -> a -> b
$ ASetter TCEnv TCEnv [(ModuleName, Nat)] [(ModuleName, Nat)]
-> ([(ModuleName, Nat)] -> [(ModuleName, Nat)]) -> TCEnv -> TCEnv
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
over ASetter TCEnv TCEnv [(ModuleName, Nat)] [(ModuleName, Nat)]
Lens' TCEnv [(ModuleName, Nat)]
eAnonymousModules \[(ModuleName, Nat)]
ms -> (ModuleName
m, Nat
n) (ModuleName, Nat) -> [(ModuleName, Nat)] -> [(ModuleName, Nat)]
forall a. a -> [a] -> [a]
: [(ModuleName, Nat)]
ms

{-# INLINE withEnv #-}
-- | Set the current environment to the given
withEnv :: MonadTCEnv m => TCEnv -> m a -> m a
withEnv :: forall (m :: * -> *) a. MonadTCEnv m => TCEnv -> m a -> m a
withEnv TCEnv
env = (TCEnv -> TCEnv) -> m a -> m a
forall a. (TCEnv -> TCEnv) -> m a -> m a
forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC \TCEnv
env0 ->
  -- Keep persistent settings
  TCEnv
env TCEnv -> (TCEnv -> TCEnv) -> TCEnv
forall a b. a -> (a -> b) -> b
& (Bool -> Identity Bool) -> TCEnv -> Identity TCEnv
Lens' TCEnv Bool
ePrintMetasBare ((Bool -> Identity Bool) -> TCEnv -> Identity TCEnv)
-> Bool -> TCEnv -> TCEnv
forall s t a b. ASetter s t a b -> b -> s -> t
.~ (TCEnv
env0 TCEnv -> Getting Bool TCEnv Bool -> Bool
forall s a. s -> Getting a s a -> a
^. Getting Bool TCEnv Bool
Lens' TCEnv Bool
ePrintMetasBare)

-- | Get the current environment
getEnv :: TCM TCEnv
getEnv :: TCM TCEnv
getEnv = TCM TCEnv
forall (m :: * -> *). MonadTCEnv m => m TCEnv
askTC

{-# INLINE withHighlightingLevel #-}
-- | Set highlighting level
withHighlightingLevel :: HighlightingLevel -> TCM a -> TCM a
withHighlightingLevel :: forall a. HighlightingLevel -> TCM a -> TCM a
withHighlightingLevel HighlightingLevel
h = (TCEnv -> TCEnv) -> TCMT IO a -> TCMT IO a
forall a. (TCEnv -> TCEnv) -> TCMT IO a -> TCMT IO a
forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC ((TCEnv -> TCEnv) -> TCMT IO a -> TCMT IO a)
-> (TCEnv -> TCEnv) -> TCMT IO a -> TCMT IO a
forall a b. (a -> b) -> a -> b
$ ASetter TCEnv TCEnv HighlightingLevel HighlightingLevel
-> HighlightingLevel -> TCEnv -> TCEnv
forall s t a b. ASetter s t a b -> b -> s -> t
set ASetter TCEnv TCEnv HighlightingLevel HighlightingLevel
Lens' TCEnv HighlightingLevel
eHighlightingLevel HighlightingLevel
h

{-# INLINE doExpandLast #-}
-- | Restore setting for 'ExpandLast' to default.
doExpandLast :: TCM a -> TCM a
doExpandLast :: forall a. TCM a -> TCM a
doExpandLast = (TCEnv -> TCEnv) -> TCMT IO a -> TCMT IO a
forall a. (TCEnv -> TCEnv) -> TCMT IO a -> TCMT IO a
forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC ((TCEnv -> TCEnv) -> TCMT IO a -> TCMT IO a)
-> (TCEnv -> TCEnv) -> TCMT IO a -> TCMT IO a
forall a b. (a -> b) -> a -> b
$ ASetter TCEnv TCEnv ExpandHidden ExpandHidden
-> (ExpandHidden -> ExpandHidden) -> TCEnv -> TCEnv
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
over ASetter TCEnv TCEnv ExpandHidden ExpandHidden
Lens' TCEnv ExpandHidden
eExpandLast ExpandHidden -> ExpandHidden
setExpand where
    setExpand :: ExpandHidden -> ExpandHidden
setExpand ExpandHidden
ReallyDontExpandLast = ExpandHidden
ReallyDontExpandLast
    setExpand ExpandHidden
_                    = ExpandHidden
ExpandLast

{-# INLINE dontExpandLast #-}
dontExpandLast :: TCM a -> TCM a
dontExpandLast :: forall a. TCM a -> TCM a
dontExpandLast = (TCEnv -> TCEnv) -> TCMT IO a -> TCMT IO a
forall a. (TCEnv -> TCEnv) -> TCMT IO a -> TCMT IO a
forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC ((TCEnv -> TCEnv) -> TCMT IO a -> TCMT IO a)
-> (TCEnv -> TCEnv) -> TCMT IO a -> TCMT IO a
forall a b. (a -> b) -> a -> b
$ ASetter TCEnv TCEnv ExpandHidden ExpandHidden
-> ExpandHidden -> TCEnv -> TCEnv
forall s t a b. ASetter s t a b -> b -> s -> t
set ASetter TCEnv TCEnv ExpandHidden ExpandHidden
Lens' TCEnv ExpandHidden
eExpandLast ExpandHidden
DontExpandLast

{-# INLINE reallyDontExpandLast #-}
reallyDontExpandLast :: TCM a -> TCM a
reallyDontExpandLast :: forall a. TCM a -> TCM a
reallyDontExpandLast = (TCEnv -> TCEnv) -> TCMT IO a -> TCMT IO a
forall a. (TCEnv -> TCEnv) -> TCMT IO a -> TCMT IO a
forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC ((TCEnv -> TCEnv) -> TCMT IO a -> TCMT IO a)
-> (TCEnv -> TCEnv) -> TCMT IO a -> TCMT IO a
forall a b. (a -> b) -> a -> b
$ ASetter TCEnv TCEnv ExpandHidden ExpandHidden
-> ExpandHidden -> TCEnv -> TCEnv
forall s t a b. ASetter s t a b -> b -> s -> t
set ASetter TCEnv TCEnv ExpandHidden ExpandHidden
Lens' TCEnv ExpandHidden
eExpandLast ExpandHidden
ReallyDontExpandLast

-- | If the reduced did a proper match (constructor or literal pattern),
--   then record this as simplification step.
{-# INLINE performedSimplification #-}
performedSimplification :: MonadTCEnv m => m a -> m a
performedSimplification :: forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
performedSimplification = (TCEnv -> TCEnv) -> m a -> m a
forall a. (TCEnv -> TCEnv) -> m a -> m a
forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC ((TCEnv -> TCEnv) -> m a -> m a) -> (TCEnv -> TCEnv) -> m a -> m a
forall a b. (a -> b) -> a -> b
$ ASetter TCEnv TCEnv Simplification Simplification
-> Simplification -> TCEnv -> TCEnv
forall s t a b. ASetter s t a b -> b -> s -> t
set ASetter TCEnv TCEnv Simplification Simplification
Lens' TCEnv Simplification
eSimplification Simplification
YesSimplification

{-# INLINE performedSimplification' #-}
performedSimplification' :: MonadTCEnv m => Simplification -> m a -> m a
performedSimplification' :: forall (m :: * -> *) a.
MonadTCEnv m =>
Simplification -> m a -> m a
performedSimplification' Simplification
simpl = (TCEnv -> TCEnv) -> m a -> m a
forall a. (TCEnv -> TCEnv) -> m a -> m a
forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC ((TCEnv -> TCEnv) -> m a -> m a) -> (TCEnv -> TCEnv) -> m a -> m a
forall a b. (a -> b) -> a -> b
$ ASetter TCEnv TCEnv Simplification Simplification
-> (Simplification -> Simplification) -> TCEnv -> TCEnv
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
over' ASetter TCEnv TCEnv Simplification Simplification
Lens' TCEnv Simplification
eSimplification (Simplification
simpl Simplification -> Simplification -> Simplification
forall a. Semigroup a => a -> a -> a
<>)

getSimplification :: MonadTCEnv m => m Simplification
getSimplification :: forall (m :: * -> *). MonadTCEnv m => m Simplification
getSimplification = Lens' TCEnv Simplification -> m Simplification
forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
viewTC (Simplification -> f Simplification) -> TCEnv -> f TCEnv
Lens' TCEnv Simplification
eSimplification

-- * Controlling reduction.

-- | Lens for 'AllowedReductions'.
updateAllowedReductions :: (AllowedReductions -> AllowedReductions) -> TCEnv -> TCEnv
updateAllowedReductions :: (AllowedReductions -> AllowedReductions) -> TCEnv -> TCEnv
updateAllowedReductions = ASetter TCEnv TCEnv AllowedReductions AllowedReductions
-> (AllowedReductions -> AllowedReductions) -> TCEnv -> TCEnv
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
over ASetter TCEnv TCEnv AllowedReductions AllowedReductions
Lens' TCEnv AllowedReductions
eAllowedReductions

{-# INLINE modifyAllowedReductions #-}
modifyAllowedReductions :: MonadTCEnv m => (AllowedReductions -> AllowedReductions) -> m a -> m a
modifyAllowedReductions :: forall (m :: * -> *) a.
MonadTCEnv m =>
(AllowedReductions -> AllowedReductions) -> m a -> m a
modifyAllowedReductions = (TCEnv -> TCEnv) -> m a -> m a
forall a. (TCEnv -> TCEnv) -> m a -> m a
forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC ((TCEnv -> TCEnv) -> m a -> m a)
-> ((AllowedReductions -> AllowedReductions) -> TCEnv -> TCEnv)
-> (AllowedReductions -> AllowedReductions)
-> m a
-> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (AllowedReductions -> AllowedReductions) -> TCEnv -> TCEnv
updateAllowedReductions

{-# INLINE putAllowedReductions #-}
putAllowedReductions :: MonadTCEnv m => AllowedReductions -> m a -> m a
putAllowedReductions :: forall (m :: * -> *) a.
MonadTCEnv m =>
AllowedReductions -> m a -> m a
putAllowedReductions = (AllowedReductions -> AllowedReductions) -> m a -> m a
forall (m :: * -> *) a.
MonadTCEnv m =>
(AllowedReductions -> AllowedReductions) -> m a -> m a
modifyAllowedReductions ((AllowedReductions -> AllowedReductions) -> m a -> m a)
-> (AllowedReductions -> AllowedReductions -> AllowedReductions)
-> AllowedReductions
-> m a
-> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AllowedReductions -> AllowedReductions -> AllowedReductions
forall a b. a -> b -> a
const

{-# INLINE onlyReduceProjections #-}
-- | Reduce @Def f vs@ only if @f@ is a projection.
onlyReduceProjections :: MonadTCEnv m => m a -> m a
onlyReduceProjections :: forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
onlyReduceProjections = (AllowedReductions -> AllowedReductions) -> m a -> m a
forall (m :: * -> *) a.
MonadTCEnv m =>
(AllowedReductions -> AllowedReductions) -> m a -> m a
modifyAllowedReductions ((AllowedReductions -> AllowedReductions) -> m a -> m a)
-> (AllowedReductions -> AllowedReductions) -> m a -> m a
forall a b. (a -> b) -> a -> b
$ AllowedReductions -> AllowedReductions -> AllowedReductions
forall a. SmallSet a -> SmallSet a -> SmallSet a
SmallSet.intersection (AllowedReductions -> AllowedReductions -> AllowedReductions)
-> AllowedReductions -> AllowedReductions -> AllowedReductions
forall a b. (a -> b) -> a -> b
$
  AllowedReduction -> AllowedReductions
forall a. SmallSetElement a => a -> SmallSet a
SmallSet.singleton AllowedReduction
ProjectionReductions

{-# INLINE allowAllReductions #-}
-- | Allow all reductions except for non-terminating functions (default).
allowAllReductions :: MonadTCEnv m => m a -> m a
allowAllReductions :: forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
allowAllReductions = AllowedReductions -> m a -> m a
forall (m :: * -> *) a.
MonadTCEnv m =>
AllowedReductions -> m a -> m a
putAllowedReductions AllowedReductions
allReductions

{-# INLINE allowNonTerminatingReductions #-}
-- | Allow all reductions including non-terminating functions.
allowNonTerminatingReductions :: MonadTCEnv m => m a -> m a
allowNonTerminatingReductions :: forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
allowNonTerminatingReductions = AllowedReductions -> m a -> m a
forall (m :: * -> *) a.
MonadTCEnv m =>
AllowedReductions -> m a -> m a
putAllowedReductions AllowedReductions
reallyAllReductions

{-# INLINE onlyReduceTypes #-}
-- | Allow all reductions when reducing types. Otherwise only allow
--   inlined functions to be unfolded.
onlyReduceTypes :: MonadTCEnv m => m a -> m a
onlyReduceTypes :: forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
onlyReduceTypes = (AllowedReductions -> AllowedReductions) -> m a -> m a
forall (m :: * -> *) a.
MonadTCEnv m =>
(AllowedReductions -> AllowedReductions) -> m a -> m a
modifyAllowedReductions ((AllowedReductions -> AllowedReductions) -> m a -> m a)
-> (AllowedReductions -> AllowedReductions) -> m a -> m a
forall a b. (a -> b) -> a -> b
$ AllowedReductions -> AllowedReductions -> AllowedReductions
forall a. SmallSet a -> SmallSet a -> SmallSet a
SmallSet.intersection (AllowedReductions -> AllowedReductions -> AllowedReductions)
-> AllowedReductions -> AllowedReductions -> AllowedReductions
forall a b. (a -> b) -> a -> b
$
  [AllowedReduction] -> AllowedReductions
forall a. SmallSetElement a => [a] -> SmallSet a
SmallSet.fromList [AllowedReduction
TypeLevelReductions, AllowedReduction
InlineReductions]

{-# INLINE typeLevelReductions #-}
-- | Update allowed reductions when working on types
typeLevelReductions :: MonadTCEnv m => m a -> m a
typeLevelReductions :: forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
typeLevelReductions = (AllowedReductions -> AllowedReductions) -> m a -> m a
forall (m :: * -> *) a.
MonadTCEnv m =>
(AllowedReductions -> AllowedReductions) -> m a -> m a
modifyAllowedReductions ((AllowedReductions -> AllowedReductions) -> m a -> m a)
-> (AllowedReductions -> AllowedReductions) -> m a -> m a
forall a b. (a -> b) -> a -> b
$ \AllowedReductions
reds -> if
  | AllowedReduction
TypeLevelReductions AllowedReduction -> AllowedReductions -> Bool
forall a. SmallSetElement a => a -> SmallSet a -> Bool
`SmallSet.member` AllowedReductions
reds ->
      if AllowedReduction
NonTerminatingReductions AllowedReduction -> AllowedReductions -> Bool
forall a. SmallSetElement a => a -> SmallSet a -> Bool
`SmallSet.member` AllowedReductions
reds
       then AllowedReductions
reallyAllReductions
       else AllowedReductions
allReductions
  | Bool
otherwise -> AllowedReductions
reds

-- * Concerning 'envInsideDotPattern'

{-# INLINE insideDotPattern #-}
insideDotPattern :: TCM a -> TCM a
insideDotPattern :: forall a. TCM a -> TCM a
insideDotPattern = (TCEnv -> TCEnv) -> TCMT IO a -> TCMT IO a
forall a. (TCEnv -> TCEnv) -> TCMT IO a -> TCMT IO a
forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC ((TCEnv -> TCEnv) -> TCMT IO a -> TCMT IO a)
-> (TCEnv -> TCEnv) -> TCMT IO a -> TCMT IO a
forall a b. (a -> b) -> a -> b
$ ((Bool -> Identity Bool) -> TCEnv -> Identity TCEnv)
-> Bool -> TCEnv -> TCEnv
forall s t a b. ASetter s t a b -> b -> s -> t
set (Bool -> Identity Bool) -> TCEnv -> Identity TCEnv
Lens' TCEnv Bool
eInsideDotPattern Bool
True

isInsideDotPattern :: TCM Bool
isInsideDotPattern :: TCM Bool
isInsideDotPattern = Lens' TCEnv Bool -> TCM Bool
forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
viewTC (Bool -> f Bool) -> TCEnv -> f TCEnv
Lens' TCEnv Bool
eInsideDotPattern

{-# INLINE callByName #-}
-- | Don't use call-by-need evaluation for the given computation.
callByName :: TCM a -> TCM a
callByName :: forall a. TCM a -> TCM a
callByName = (TCEnv -> TCEnv) -> TCMT IO a -> TCMT IO a
forall a. (TCEnv -> TCEnv) -> TCMT IO a -> TCMT IO a
forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC ((TCEnv -> TCEnv) -> TCMT IO a -> TCMT IO a)
-> (TCEnv -> TCEnv) -> TCMT IO a -> TCMT IO a
forall a b. (a -> b) -> a -> b
$ ((Bool -> Identity Bool) -> TCEnv -> Identity TCEnv)
-> Bool -> TCEnv -> TCEnv
forall s t a b. ASetter s t a b -> b -> s -> t
set (Bool -> Identity Bool) -> TCEnv -> Identity TCEnv
Lens' TCEnv Bool
eCallByNeed Bool
False

{-# INLINE dontFoldLetBindings #-}
-- | Don't fold let bindings when printing. This is a bit crude since it disables any folding of let
--   bindings at all. In many cases it's better to use `removeLetBinding` before printing to drop
--   the let bindings that should not be folded.
dontFoldLetBindings :: MonadTCEnv m => m a -> m a
dontFoldLetBindings :: forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
dontFoldLetBindings = (TCEnv -> TCEnv) -> m a -> m a
forall a. (TCEnv -> TCEnv) -> m a -> m a
forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC ((TCEnv -> TCEnv) -> m a -> m a) -> (TCEnv -> TCEnv) -> m a -> m a
forall a b. (a -> b) -> a -> b
$ ((Bool -> Identity Bool) -> TCEnv -> Identity TCEnv)
-> Bool -> TCEnv -> TCEnv
forall s t a b. ASetter s t a b -> b -> s -> t
set (Bool -> Identity Bool) -> TCEnv -> Identity TCEnv
Lens' TCEnv Bool
eFoldLetBindings Bool
False