    {-# OPTIONS_GHC -Wunused-imports #-}

    {- | Modality.

    Agda has support for several modalities, namely:

     * 'Cohesion'
     * 'Quantity'
     * 'Relevance'

    In order to type check such modalities, we must store the current modality in
    the typing context. This module provides functions to update the context based
    on a given modality.

    See "Agda.TypeChecking.Irrelevance".
    -}

    module Agda.TypeChecking.Monad.Modality where

    import qualified Data.Map as Map

    import Agda.Interaction.Options

    import Agda.Syntax.Common

    import Agda.TypeChecking.Monad.Base
    import Agda.TypeChecking.Monad.Context
    import Agda.TypeChecking.Monad.Debug
    import Agda.TypeChecking.Monad.Env

    import Agda.Utils.Function
    import Agda.Utils.Lens
    import Agda.Utils.Monad

    -- | data 'Relevance'
    --   see "Agda.Syntax.Common".

    -- * Operations on 'Dom'.

    -- | Prepare parts of a parameter telescope for abstraction in constructors
    --   and projections.
    hideAndRelParams :: (LensHiding a, LensRelevance a) => a -> a
    hideAndRelParams :: forall a. (LensHiding a, LensRelevance a) => a -> a
    hideAndRelParams = a -> a
    forall a. LensHiding a => a -> a
    hideOrKeepInstance (a -> a) -> (a -> a) -> a -> a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Relevance -> Relevance) -> a -> a
    forall a. LensRelevance a => (Relevance -> Relevance) -> a -> a
    mapRelevance Relevance -> Relevance
    shapeIrrelevantToIrrelevant

    -- * Operations on 'Context'.

    -- | Modify the context whenever going from the l.h.s. (term side)
    --   of the typing judgement to the r.h.s. (type side).
    workOnTypes :: (MonadTCEnv m, HasOptions m, MonadDebug m)
                => m a -> m a
    workOnTypes :: forall (m :: * -> *) a.
    (MonadTCEnv m, HasOptions m, MonadDebug m) =>
    m a -> m a
    workOnTypes m a
    cont = do
      allowed <- PragmaOptions -> Bool
    optExperimentalIrrelevance (PragmaOptions -> Bool) -> m PragmaOptions -> m Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m PragmaOptions
    forall (m :: * -> *). HasOptions m => m PragmaOptions
    pragmaOptions
      verboseBracket "tc.irr" 60 "workOnTypes" $ workOnTypes' allowed cont

    -- | Internal workhorse, expects value of --experimental-irrelevance flag
    --   as argument.
    workOnTypes' :: (MonadTCEnv m) => Bool -> m a -> m a
    workOnTypes' :: forall (m :: * -> *) a. MonadTCEnv m => Bool -> m a -> m a
    workOnTypes' Bool
    experimental
      = Bool -> (m a -> m a) -> m a -> m a
    forall b a. IsBool b => b -> (a -> a) -> a -> a
    applyWhen Bool
    experimental ((forall e. Dom e -> Dom e) -> m a -> m a
    forall (tcm :: * -> *) a.
    MonadTCEnv tcm =>
    (forall e. Dom e -> Dom e) -> tcm a -> tcm a
    modifyContextInfo ((forall e. Dom e -> Dom e) -> m a -> m a)
    -> (forall e. Dom e -> Dom e) -> m a -> m a
    forall a b. (a -> b) -> a -> b
    $ (Relevance -> Relevance) -> Dom e -> Dom e
    forall a. LensRelevance a => (Relevance -> Relevance) -> a -> a
    mapRelevance Relevance -> Relevance
    irrelevantToShapeIrrelevant)
      (m a -> m a) -> (m a -> m a) -> m a -> m a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Quantity -> m a -> m a
    forall (tcm :: * -> *) q a.
    (MonadTCEnv tcm, LensQuantity q) =>
    q -> tcm a -> tcm a
    applyQuantityToJudgement Quantity
    zeroQuantity
      (m a -> m a) -> (m a -> m a) -> m a -> m a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PolarityModality -> m a -> m a
    forall (tcm :: * -> *) p a.
    (MonadTCEnv tcm, LensModalPolarity p) =>
    p -> tcm a -> tcm a
    applyPolarityToContext (ModalPolarity -> PolarityModality
    withStandardLock ModalPolarity
    UnusedPolarity)
      (m a -> m a) -> (m a -> m a) -> m a -> m a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . m a -> m a
    forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
    typeLevelReductions
      (m a -> m a) -> (m a -> m a) -> m a -> m a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (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
    e -> TCEnv
    e { envWorkingOnTypes = True })

    applyPolarityToContext :: (MonadTCEnv tcm, LensModalPolarity p) => p -> tcm a -> tcm a
    applyPolarityToContext :: forall (tcm :: * -> *) p a.
    (MonadTCEnv tcm, LensModalPolarity p) =>
    p -> tcm a -> tcm a
    applyPolarityToContext p
    p = (TCEnv -> TCEnv) -> tcm a -> tcm a
    forall a. (TCEnv -> TCEnv) -> tcm a -> tcm a
    forall (m :: * -> *) a.
    MonadTCEnv m =>
    (TCEnv -> TCEnv) -> m a -> m a
    localTC
      ((TCEnv -> TCEnv) -> tcm a -> tcm a)
    -> (TCEnv -> TCEnv) -> tcm a -> tcm a
    forall a b. (a -> b) -> a -> b
    $ Lens' TCEnv [ContextEntry] -> LensMap TCEnv [ContextEntry]
    forall o i. Lens' o i -> LensMap o i
    over ([ContextEntry] -> f [ContextEntry]) -> TCEnv -> f TCEnv
    Lens' TCEnv [ContextEntry]
    eContext     ((ContextEntry -> ContextEntry) -> [ContextEntry] -> [ContextEntry]
    forall a b. (a -> b) -> [a] -> [b]
    map ((ContextEntry -> ContextEntry)
     -> [ContextEntry] -> [ContextEntry])
    -> (ContextEntry -> ContextEntry)
    -> [ContextEntry]
    -> [ContextEntry]
    forall a b. (a -> b) -> a -> b
    $ PolarityModality -> ContextEntry -> ContextEntry
    forall a. LensModalPolarity a => PolarityModality -> a -> a
    inverseApplyPolarity PolarityModality
    pol)
      (TCEnv -> TCEnv) -> (TCEnv -> TCEnv) -> TCEnv -> TCEnv
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Lens' TCEnv (Map Name (Open LetBinding))
    -> LensMap TCEnv (Map Name (Open LetBinding))
    forall o i. Lens' o i -> LensMap o i
    over (Map Name (Open LetBinding) -> f (Map Name (Open LetBinding)))
    -> TCEnv -> f TCEnv
    Lens' TCEnv (Map Name (Open LetBinding))
    eLetBindings ((Open LetBinding -> Open LetBinding)
    -> Map Name (Open LetBinding) -> Map Name (Open LetBinding)
    forall a b k. (a -> b) -> Map k a -> Map k b
    Map.map ((Open LetBinding -> Open LetBinding)
     -> Map Name (Open LetBinding) -> Map Name (Open LetBinding))
    -> ((Dom Type -> Dom Type) -> Open LetBinding -> Open LetBinding)
    -> (Dom Type -> Dom Type)
    -> Map Name (Open LetBinding)
    -> Map Name (Open LetBinding)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (LetBinding -> LetBinding) -> Open LetBinding -> Open LetBinding
    forall a b. (a -> b) -> Open a -> Open b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((LetBinding -> LetBinding) -> Open LetBinding -> Open LetBinding)
    -> ((Dom Type -> Dom Type) -> LetBinding -> LetBinding)
    -> (Dom Type -> Dom Type)
    -> Open LetBinding
    -> Open LetBinding
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Dom Type -> Dom Type) -> LetBinding -> LetBinding
    onLetBindingType
                           ((Dom Type -> Dom Type)
     -> Map Name (Open LetBinding) -> Map Name (Open LetBinding))
    -> (Dom Type -> Dom Type)
    -> Map Name (Open LetBinding)
    -> Map Name (Open LetBinding)
    forall a b. (a -> b) -> a -> b
    $ PolarityModality -> Dom Type -> Dom Type
    forall a. LensModalPolarity a => PolarityModality -> a -> a
    inverseApplyPolarity PolarityModality
    pol)
      where
        pol :: PolarityModality
    pol = p -> PolarityModality
    forall a. LensModalPolarity a => a -> PolarityModality
    getModalPolarity p
    p

    -- | (Conditionally) wake up irrelevant variables and make them relevant.
    --   For instance,
    --   in an irrelevant function argument otherwise irrelevant variables
    --   may be used, so they are awoken before type checking the argument.
    --
    --   Also allow the use of irrelevant definitions.
    applyRelevanceToContext :: (MonadTCEnv tcm, LensRelevance r) => r -> tcm a -> tcm a
    applyRelevanceToContext :: forall (tcm :: * -> *) r a.
    (MonadTCEnv tcm, LensRelevance r) =>
    r -> tcm a -> tcm a
    applyRelevanceToContext r
    thing =
      Bool -> (tcm a -> tcm a) -> tcm a -> tcm a
    forall b a. IsBool b => b -> (a -> a) -> a -> a
    applyUnless (Relevance -> Bool
    forall a. LensRelevance a => a -> Bool
    isRelevant Relevance
    rel)
       ((tcm a -> tcm a) -> tcm a -> tcm a)
    -> (tcm a -> tcm a) -> tcm a -> tcm a
    forall a b. (a -> b) -> a -> b
    $ Relevance -> tcm a -> tcm a
    forall (tcm :: * -> *) a.
    MonadTCEnv tcm =>
    Relevance -> tcm a -> tcm a
    applyRelevanceToContextOnly   Relevance
    rel
       (tcm a -> tcm a) -> (tcm a -> tcm a) -> tcm a -> tcm a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Relevance -> tcm a -> tcm a
    forall (tcm :: * -> *) a.
    MonadTCEnv tcm =>
    Relevance -> tcm a -> tcm a
    applyRelevanceToJudgementOnly Relevance
    rel
      where rel :: Relevance
    rel = r -> Relevance
    forall a. LensRelevance a => a -> Relevance
    getRelevance r
    thing

    -- | (Conditionally) wake up irrelevant variables and make them relevant.
    --   For instance,
    --   in an irrelevant function argument otherwise irrelevant variables
    --   may be used, so they are awoken before type checking the argument.
    --
    --   Precondition: @Relevance /= Relevant@
    applyRelevanceToContextOnly :: (MonadTCEnv tcm) => Relevance -> tcm a -> tcm a
    applyRelevanceToContextOnly :: forall (tcm :: * -> *) a.
    MonadTCEnv tcm =>
    Relevance -> tcm a -> tcm a
    applyRelevanceToContextOnly Relevance
    rel = (TCEnv -> TCEnv) -> tcm a -> tcm a
    forall a. (TCEnv -> TCEnv) -> tcm a -> tcm a
    forall (m :: * -> *) a.
    MonadTCEnv m =>
    (TCEnv -> TCEnv) -> m a -> m a
    localTC
      ((TCEnv -> TCEnv) -> tcm a -> tcm a)
    -> (TCEnv -> TCEnv) -> tcm a -> tcm a
    forall a b. (a -> b) -> a -> b
    $ Lens' TCEnv [ContextEntry] -> LensMap TCEnv [ContextEntry]
    forall o i. Lens' o i -> LensMap o i
    over ([ContextEntry] -> f [ContextEntry]) -> TCEnv -> f TCEnv
    Lens' TCEnv [ContextEntry]
    eContext     ((ContextEntry -> ContextEntry) -> [ContextEntry] -> [ContextEntry]
    forall a b. (a -> b) -> [a] -> [b]
    map ((ContextEntry -> ContextEntry)
     -> [ContextEntry] -> [ContextEntry])
    -> (ContextEntry -> ContextEntry)
    -> [ContextEntry]
    -> [ContextEntry]
    forall a b. (a -> b) -> a -> b
    $ Relevance -> ContextEntry -> ContextEntry
    forall a. LensRelevance a => Relevance -> a -> a
    inverseApplyRelevance Relevance
    rel)
      (TCEnv -> TCEnv) -> (TCEnv -> TCEnv) -> TCEnv -> TCEnv
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Lens' TCEnv (Map Name (Open LetBinding))
    -> LensMap TCEnv (Map Name (Open LetBinding))
    forall o i. Lens' o i -> LensMap o i
    over (Map Name (Open LetBinding) -> f (Map Name (Open LetBinding)))
    -> TCEnv -> f TCEnv
    Lens' TCEnv (Map Name (Open LetBinding))
    eLetBindings ((Open LetBinding -> Open LetBinding)
    -> Map Name (Open LetBinding) -> Map Name (Open LetBinding)
    forall a b k. (a -> b) -> Map k a -> Map k b
    Map.map ((Open LetBinding -> Open LetBinding)
     -> Map Name (Open LetBinding) -> Map Name (Open LetBinding))
    -> ((Dom Type -> Dom Type) -> Open LetBinding -> Open LetBinding)
    -> (Dom Type -> Dom Type)
    -> Map Name (Open LetBinding)
    -> Map Name (Open LetBinding)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (LetBinding -> LetBinding) -> Open LetBinding -> Open LetBinding
    forall a b. (a -> b) -> Open a -> Open b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((LetBinding -> LetBinding) -> Open LetBinding -> Open LetBinding)
    -> ((Dom Type -> Dom Type) -> LetBinding -> LetBinding)
    -> (Dom Type -> Dom Type)
    -> Open LetBinding
    -> Open LetBinding
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Dom Type -> Dom Type) -> LetBinding -> LetBinding
    onLetBindingType ((Dom Type -> Dom Type)
     -> Map Name (Open LetBinding) -> Map Name (Open LetBinding))
    -> (Dom Type -> Dom Type)
    -> Map Name (Open LetBinding)
    -> Map Name (Open LetBinding)
    forall a b. (a -> b) -> a -> b
    $ Relevance -> Dom Type -> Dom Type
    forall a. LensRelevance a => Relevance -> a -> a
    inverseApplyRelevance Relevance
    rel)

    -- | Apply relevance @rel@ the the relevance annotation of the (typing/equality)
    --   judgement.  This is part of the work done when going into a @rel@-context.
    --
    --   Precondition: @Relevance /= Relevant@
    applyRelevanceToJudgementOnly :: (MonadTCEnv tcm) => Relevance -> tcm a -> tcm a
    applyRelevanceToJudgementOnly :: forall (tcm :: * -> *) a.
    MonadTCEnv tcm =>
    Relevance -> tcm a -> tcm a
    applyRelevanceToJudgementOnly = (TCEnv -> TCEnv) -> tcm a -> tcm a
    forall a. (TCEnv -> TCEnv) -> tcm a -> tcm a
    forall (m :: * -> *) a.
    MonadTCEnv m =>
    (TCEnv -> TCEnv) -> m a -> m a
    localTC ((TCEnv -> TCEnv) -> tcm a -> tcm a)
    -> (Relevance -> TCEnv -> TCEnv) -> Relevance -> tcm a -> tcm a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Lens' TCEnv Relevance -> LensMap TCEnv Relevance
    forall o i. Lens' o i -> LensMap o i
    over (Relevance -> f Relevance) -> TCEnv -> f TCEnv
    Lens' TCEnv Relevance
    eRelevance LensMap TCEnv Relevance
    -> (Relevance -> Relevance -> Relevance)
    -> Relevance
    -> TCEnv
    -> TCEnv
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Relevance -> Relevance -> Relevance
    composeRelevance

    -- | Like 'applyRelevanceToContext', but only act on context if
    --   @--irrelevant-projections@.
    --   See issue #2170.
    applyRelevanceToContextFunBody :: (MonadTCM tcm, LensRelevance r) => r -> tcm a -> tcm a
    applyRelevanceToContextFunBody :: forall (tcm :: * -> *) r a.
    (MonadTCM tcm, LensRelevance r) =>
    r -> tcm a -> tcm a
    applyRelevanceToContextFunBody r
    thing tcm a
    cont =
      case r -> Relevance
    forall a. LensRelevance a => a -> Relevance
    getRelevance r
    thing of
        Relevant{} -> tcm a
    cont
        Relevance
    rel -> tcm Bool -> (tcm a -> tcm a) -> tcm a -> tcm a
    forall b (m :: * -> *) a.
    (IsBool b, Monad m) =>
    m b -> (m a -> m a) -> m a -> m a
    applyWhenM (PragmaOptions -> Bool
    optIrrelevantProjections (PragmaOptions -> Bool) -> tcm PragmaOptions -> tcm Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> tcm PragmaOptions
    forall (m :: * -> *). HasOptions m => m PragmaOptions
    pragmaOptions)
          (Relevance -> tcm a -> tcm a
    forall (tcm :: * -> *) a.
    MonadTCEnv tcm =>
    Relevance -> tcm a -> tcm a
    applyRelevanceToContextOnly Relevance
    rel) (tcm a -> tcm a) -> tcm a -> tcm a
    forall a b. (a -> b) -> a -> b
    $    -- enable local irr. defs only when option
          Relevance -> tcm a -> tcm a
    forall (tcm :: * -> *) a.
    MonadTCEnv tcm =>
    Relevance -> tcm a -> tcm a
    applyRelevanceToJudgementOnly Relevance
    rel tcm a
    cont -- enable global irr. defs alway

    -- | Apply the quantity to the quantity annotation of the
    -- (typing/equality) judgement.
    --
    -- Precondition: The quantity must not be @'Quantity1' something@.
    applyQuantityToJudgement ::
      (MonadTCEnv tcm, LensQuantity q) => q -> tcm a -> tcm a
    applyQuantityToJudgement :: forall (tcm :: * -> *) q a.
    (MonadTCEnv tcm, LensQuantity q) =>
    q -> tcm a -> tcm a
    applyQuantityToJudgement =
      (TCEnv -> TCEnv) -> tcm a -> tcm a
    forall a. (TCEnv -> TCEnv) -> tcm a -> tcm a
    forall (m :: * -> *) a.
    MonadTCEnv m =>
    (TCEnv -> TCEnv) -> m a -> m a
    localTC ((TCEnv -> TCEnv) -> tcm a -> tcm a)
    -> (q -> TCEnv -> TCEnv) -> q -> tcm a -> tcm a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Lens' TCEnv Quantity -> LensMap TCEnv Quantity
    forall o i. Lens' o i -> LensMap o i
    over (Quantity -> f Quantity) -> TCEnv -> f TCEnv
    Lens' TCEnv Quantity
    eQuantity LensMap TCEnv Quantity
    -> (q -> Quantity -> Quantity) -> q -> TCEnv -> TCEnv
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Quantity -> Quantity -> Quantity
    composeQuantity (Quantity -> Quantity -> Quantity)
    -> (q -> Quantity) -> q -> Quantity -> Quantity
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . q -> Quantity
    forall a. LensQuantity a => a -> Quantity
    getQuantity

    -- | Apply inverse composition with the given cohesion to the typing context.
    applyCohesionToContext :: (MonadTCEnv tcm, LensCohesion m) => m -> tcm a -> tcm a
    applyCohesionToContext :: forall (tcm :: * -> *) m a.
    (MonadTCEnv tcm, LensCohesion m) =>
    m -> tcm a -> tcm a
    applyCohesionToContext m
    thing =
      case m -> Cohesion
    forall a. LensCohesion a => a -> Cohesion
    getCohesion m
    thing of
        Cohesion
    m | Cohesion
    m Cohesion -> Cohesion -> Bool
    forall a. Eq a => a -> a -> Bool
    == Cohesion
    unitCohesion -> tcm a -> tcm a
    forall a. a -> a
    id
          | Bool
    otherwise         -> Cohesion -> tcm a -> tcm a
    forall (tcm :: * -> *) a.
    MonadTCEnv tcm =>
    Cohesion -> tcm a -> tcm a
    applyCohesionToContextOnly   Cohesion
    m
                                 -- Cohesion does not apply to the judgment.

    applyCohesionToContextOnly :: (MonadTCEnv tcm) => Cohesion -> tcm a -> tcm a
    applyCohesionToContextOnly :: forall (tcm :: * -> *) a.
    MonadTCEnv tcm =>
    Cohesion -> tcm a -> tcm a
    applyCohesionToContextOnly Cohesion
    q = (TCEnv -> TCEnv) -> tcm a -> tcm a
    forall a. (TCEnv -> TCEnv) -> tcm a -> tcm a
    forall (m :: * -> *) a.
    MonadTCEnv m =>
    (TCEnv -> TCEnv) -> m a -> m a
    localTC
      ((TCEnv -> TCEnv) -> tcm a -> tcm a)
    -> (TCEnv -> TCEnv) -> tcm a -> tcm a
    forall a b. (a -> b) -> a -> b
    $ Lens' TCEnv [ContextEntry] -> LensMap TCEnv [ContextEntry]
    forall o i. Lens' o i -> LensMap o i
    over ([ContextEntry] -> f [ContextEntry]) -> TCEnv -> f TCEnv
    Lens' TCEnv [ContextEntry]
    eContext     ((ContextEntry -> ContextEntry) -> [ContextEntry] -> [ContextEntry]
    forall a b. (a -> b) -> [a] -> [b]
    map ((ContextEntry -> ContextEntry)
     -> [ContextEntry] -> [ContextEntry])
    -> (ContextEntry -> ContextEntry)
    -> [ContextEntry]
    -> [ContextEntry]
    forall a b. (a -> b) -> a -> b
    $ Cohesion -> ContextEntry -> ContextEntry
    forall a. LensCohesion a => Cohesion -> a -> a
    inverseApplyCohesion Cohesion
    q)
      (TCEnv -> TCEnv) -> (TCEnv -> TCEnv) -> TCEnv -> TCEnv
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Lens' TCEnv (Map Name (Open LetBinding))
    -> LensMap TCEnv (Map Name (Open LetBinding))
    forall o i. Lens' o i -> LensMap o i
    over (Map Name (Open LetBinding) -> f (Map Name (Open LetBinding)))
    -> TCEnv -> f TCEnv
    Lens' TCEnv (Map Name (Open LetBinding))
    eLetBindings ((Open LetBinding -> Open LetBinding)
    -> Map Name (Open LetBinding) -> Map Name (Open LetBinding)
    forall a b k. (a -> b) -> Map k a -> Map k b
    Map.map ((Open LetBinding -> Open LetBinding)
     -> Map Name (Open LetBinding) -> Map Name (Open LetBinding))
    -> ((Dom Type -> Dom Type) -> Open LetBinding -> Open LetBinding)
    -> (Dom Type -> Dom Type)
    -> Map Name (Open LetBinding)
    -> Map Name (Open LetBinding)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (LetBinding -> LetBinding) -> Open LetBinding -> Open LetBinding
    forall a b. (a -> b) -> Open a -> Open b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((LetBinding -> LetBinding) -> Open LetBinding -> Open LetBinding)
    -> ((Dom Type -> Dom Type) -> LetBinding -> LetBinding)
    -> (Dom Type -> Dom Type)
    -> Open LetBinding
    -> Open LetBinding
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Dom Type -> Dom Type) -> LetBinding -> LetBinding
    onLetBindingType ((Dom Type -> Dom Type)
     -> Map Name (Open LetBinding) -> Map Name (Open LetBinding))
    -> (Dom Type -> Dom Type)
    -> Map Name (Open LetBinding)
    -> Map Name (Open LetBinding)
    forall a b. (a -> b) -> a -> b
    $ Cohesion -> Dom Type -> Dom Type
    forall a. LensCohesion a => Cohesion -> a -> a
    inverseApplyCohesion Cohesion
    q)

    -- | Can we split on arguments of the given cohesion?
    splittableCohesion :: (HasOptions m, LensCohesion a) => a -> m Bool
    splittableCohesion :: forall (m :: * -> *) a.
    (HasOptions m, LensCohesion a) =>
    a -> m Bool
    splittableCohesion a
    a = do
      let c :: Cohesion
    c = a -> Cohesion
    forall a. LensCohesion a => a -> Cohesion
    getCohesion a
    a
      Bool -> m Bool
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Cohesion -> Bool
    forall a. LensCohesion a => a -> Bool
    usableCohesion Cohesion
    c) m Bool -> m Bool -> m Bool
    forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
    `and2M` (Bool -> m Bool
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Cohesion
    c Cohesion -> Cohesion -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Cohesion
    Flat) m Bool -> m Bool -> m Bool
    forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
    `or2M` do PragmaOptions -> Bool
    optFlatSplit (PragmaOptions -> Bool) -> m PragmaOptions -> m Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m PragmaOptions
    forall (m :: * -> *). HasOptions m => m PragmaOptions
    pragmaOptions)

    {-# SPECIALIZE applyModalityToContext :: Modality -> TCM a -> TCM a #-}
    -- | (Conditionally) wake up irrelevant variables and make them relevant.
    --   For instance,
    --   in an irrelevant function argument otherwise irrelevant variables
    --   may be used, so they are awoken before type checking the argument.
    --
    --   Also allow the use of irrelevant definitions.
    --
    --   This function might also do something for other modalities.
    applyModalityToContext :: (MonadTCEnv tcm, LensModality m) => m -> tcm a -> tcm a
    applyModalityToContext :: forall (tcm :: * -> *) m a.
    (MonadTCEnv tcm, LensModality m) =>
    m -> tcm a -> tcm a
    applyModalityToContext m
    thing =
      case m -> Modality
    forall a. LensModality a => a -> Modality
    getModality m
    thing of
        Modality
    m | Modality
    m Modality -> Modality -> Bool
    forall a. Eq a => a -> a -> Bool
    == Modality
    unitModality -> tcm a -> tcm a
    forall a. a -> a
    id
          | Bool
    otherwise         -> Modality -> tcm a -> tcm a
    forall (tcm :: * -> *) a.
    MonadTCEnv tcm =>
    Modality -> tcm a -> tcm a
    applyModalityToContextOnly   Modality
    m
                               (tcm a -> tcm a) -> (tcm a -> tcm a) -> tcm a -> tcm a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Modality -> tcm a -> tcm a
    forall (tcm :: * -> *) a.
    MonadTCEnv tcm =>
    Modality -> tcm a -> tcm a
    applyModalityToJudgementOnly Modality
    m

    -- | (Conditionally) wake up irrelevant variables and make them relevant.
    --   For instance,
    --   in an irrelevant function argument otherwise irrelevant variables
    --   may be used, so they are awoken before type checking the
    --   argument.
    --
    --   This function might also do something for other modalities, but
    --   not for quantities.
    --
    --   Precondition: @Modality /= Relevant@
    applyModalityToContextOnly :: (MonadTCEnv tcm) => Modality -> tcm a -> tcm a
    applyModalityToContextOnly :: forall (tcm :: * -> *) a.
    MonadTCEnv tcm =>
    Modality -> tcm a -> tcm a
    applyModalityToContextOnly Modality
    m = (TCEnv -> TCEnv) -> tcm a -> tcm a
    forall a. (TCEnv -> TCEnv) -> tcm a -> tcm a
    forall (m :: * -> *) a.
    MonadTCEnv m =>
    (TCEnv -> TCEnv) -> m a -> m a
    localTC
      ((TCEnv -> TCEnv) -> tcm a -> tcm a)
    -> (TCEnv -> TCEnv) -> tcm a -> tcm a
    forall a b. (a -> b) -> a -> b
    $ Lens' TCEnv [ContextEntry] -> LensMap TCEnv [ContextEntry]
    forall o i. Lens' o i -> LensMap o i
    over ([ContextEntry] -> f [ContextEntry]) -> TCEnv -> f TCEnv
    Lens' TCEnv [ContextEntry]
    eContext ((ContextEntry -> ContextEntry) -> [ContextEntry] -> [ContextEntry]
    forall a b. (a -> b) -> [a] -> [b]
    map ((ContextEntry -> ContextEntry)
     -> [ContextEntry] -> [ContextEntry])
    -> (ContextEntry -> ContextEntry)
    -> [ContextEntry]
    -> [ContextEntry]
    forall a b. (a -> b) -> a -> b
    $ Modality -> ContextEntry -> ContextEntry
    forall a. LensModality a => Modality -> a -> a
    inverseApplyModalityButNotQuantity Modality
    m)
      (TCEnv -> TCEnv) -> (TCEnv -> TCEnv) -> TCEnv -> TCEnv
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Lens' TCEnv (Map Name (Open LetBinding))
    -> LensMap TCEnv (Map Name (Open LetBinding))
    forall o i. Lens' o i -> LensMap o i
    over (Map Name (Open LetBinding) -> f (Map Name (Open LetBinding)))
    -> TCEnv -> f TCEnv
    Lens' TCEnv (Map Name (Open LetBinding))
    eLetBindings
          ((Open LetBinding -> Open LetBinding)
    -> Map Name (Open LetBinding) -> Map Name (Open LetBinding)
    forall a b k. (a -> b) -> Map k a -> Map k b
    Map.map ((Open LetBinding -> Open LetBinding)
     -> Map Name (Open LetBinding) -> Map Name (Open LetBinding))
    -> ((Dom Type -> Dom Type) -> Open LetBinding -> Open LetBinding)
    -> (Dom Type -> Dom Type)
    -> Map Name (Open LetBinding)
    -> Map Name (Open LetBinding)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (LetBinding -> LetBinding) -> Open LetBinding -> Open LetBinding
    forall a b. (a -> b) -> Open a -> Open b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((LetBinding -> LetBinding) -> Open LetBinding -> Open LetBinding)
    -> ((Dom Type -> Dom Type) -> LetBinding -> LetBinding)
    -> (Dom Type -> Dom Type)
    -> Open LetBinding
    -> Open LetBinding
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Dom Type -> Dom Type) -> LetBinding -> LetBinding
    onLetBindingType ((Dom Type -> Dom Type)
     -> Map Name (Open LetBinding) -> Map Name (Open LetBinding))
    -> (Dom Type -> Dom Type)
    -> Map Name (Open LetBinding)
    -> Map Name (Open LetBinding)
    forall a b. (a -> b) -> a -> b
    $ Modality -> Dom Type -> Dom Type
    forall a. LensModality a => Modality -> a -> a
    inverseApplyModalityButNotQuantity Modality
    m)

    -- | Apply the relevance and quantity components of the modality to
    -- the modality annotation of the (typing/equality) judgement.
    --
    -- Precondition: The relevance component must not be 'Relevant'.
    applyModalityToJudgementOnly :: (MonadTCEnv tcm) => Modality -> tcm a -> tcm a
    applyModalityToJudgementOnly :: forall (tcm :: * -> *) a.
    MonadTCEnv tcm =>
    Modality -> tcm a -> tcm a
    applyModalityToJudgementOnly Modality
    m =
      (TCEnv -> TCEnv) -> tcm a -> tcm a
    forall a. (TCEnv -> TCEnv) -> tcm a -> tcm a
    forall (m :: * -> *) a.
    MonadTCEnv m =>
    (TCEnv -> TCEnv) -> m a -> m a
    localTC ((TCEnv -> TCEnv) -> tcm a -> tcm a)
    -> (TCEnv -> TCEnv) -> tcm a -> tcm a
    forall a b. (a -> b) -> a -> b
    $ Lens' TCEnv Relevance -> LensMap TCEnv Relevance
    forall o i. Lens' o i -> LensMap o i
    over (Relevance -> f Relevance) -> TCEnv -> f TCEnv
    Lens' TCEnv Relevance
    eRelevance (Relevance -> Relevance -> Relevance
    composeRelevance (Modality -> Relevance
    forall a. LensRelevance a => a -> Relevance
    getRelevance Modality
    m)) (TCEnv -> TCEnv) -> (TCEnv -> TCEnv) -> TCEnv -> TCEnv
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    .
                Lens' TCEnv Quantity -> LensMap TCEnv Quantity
    forall o i. Lens' o i -> LensMap o i
    over (Quantity -> f Quantity) -> TCEnv -> f TCEnv
    Lens' TCEnv Quantity
    eQuantity  (Quantity -> Quantity -> Quantity
    composeQuantity  (Modality -> Quantity
    forall a. LensQuantity a => a -> Quantity
    getQuantity Modality
    m))

    -- | Like 'applyModalityToContext', but only act on context (for Relevance) if
    --   @--irrelevant-projections@.
    --   See issue #2170.
    applyModalityToContextFunBody :: (MonadTCM tcm, LensModality r) => r -> tcm a -> tcm a
    applyModalityToContextFunBody :: forall (tcm :: * -> *) r a.
    (MonadTCM tcm, LensModality r) =>
    r -> tcm a -> tcm a
    applyModalityToContextFunBody r
    thing tcm a
    cont = do
        tcm Bool -> tcm a -> tcm a -> tcm a
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
    ifM (PragmaOptions -> Bool
    optIrrelevantProjections (PragmaOptions -> Bool) -> tcm PragmaOptions -> tcm Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> tcm PragmaOptions
    forall (m :: * -> *). HasOptions m => m PragmaOptions
    pragmaOptions)
          {-then-} (Modality -> tcm a -> tcm a
    forall (tcm :: * -> *) m a.
    (MonadTCEnv tcm, LensModality m) =>
    m -> tcm a -> tcm a
    applyModalityToContext Modality
    m tcm a
    cont)                -- enable global irr. defs always
          {-else-} (Relevance -> tcm a -> tcm a
    forall (tcm :: * -> *) r a.
    (MonadTCM tcm, LensRelevance r) =>
    r -> tcm a -> tcm a
    applyRelevanceToContextFunBody (Modality -> Relevance
    forall a. LensRelevance a => a -> Relevance
    getRelevance Modality
    m)
                   (tcm a -> tcm a) -> tcm a -> tcm a
    forall a b. (a -> b) -> a -> b
    $ Cohesion -> tcm a -> tcm a
    forall (tcm :: * -> *) m a.
    (MonadTCEnv tcm, LensCohesion m) =>
    m -> tcm a -> tcm a
    applyCohesionToContext (Modality -> Cohesion
    forall a. LensCohesion a => a -> Cohesion
    getCohesion Modality
    m)
                   (tcm a -> tcm a) -> tcm a -> tcm a
    forall a b. (a -> b) -> a -> b
    $ PolarityModality -> tcm a -> tcm a
    forall (tcm :: * -> *) p a.
    (MonadTCEnv tcm, LensModalPolarity p) =>
    p -> tcm a -> tcm a
    applyPolarityToContext (Modality -> PolarityModality
    forall a. LensModalPolarity a => a -> PolarityModality
    getModalPolarity Modality
    m)
                   (tcm a -> tcm a) -> tcm a -> tcm a
    forall a b. (a -> b) -> a -> b
    $ Quantity -> tcm a -> tcm a
    forall (tcm :: * -> *) q a.
    (MonadTCEnv tcm, LensQuantity q) =>
    q -> tcm a -> tcm a
    applyQuantityToJudgement (Modality -> Quantity
    forall a. LensQuantity a => a -> Quantity
    getQuantity Modality
    m) tcm a
    cont) -- enable local irr. defs only when option
      where
        m :: Modality
    m = r -> Modality
    forall a. LensModality a => a -> Modality
    getModality r
    thing

    -- | Wake up irrelevant variables and make them relevant. This is used
    --   when type checking terms in a hole, in which case you want to be able to
    --   (for instance) infer the type of an irrelevant variable. In the course
    --   of type checking an irrelevant function argument 'applyRelevanceToContext'
    --   is used instead, which also sets the context relevance to 'Irrelevant'.
    --   This is not the right thing to do when type checking interactively in a
    --   hole since it also marks all metas created during type checking as
    --   irrelevant (issue #2568).
    --
    --   Also set the current quantity to 0.
    wakeIrrelevantVars :: (MonadTCEnv tcm) => tcm a -> tcm a
    wakeIrrelevantVars :: forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
    wakeIrrelevantVars
      = Relevance -> tcm a -> tcm a
    forall (tcm :: * -> *) a.
    MonadTCEnv tcm =>
    Relevance -> tcm a -> tcm a
    applyRelevanceToContextOnly Relevance
    irrelevant
      (tcm a -> tcm a) -> (tcm a -> tcm a) -> tcm a -> tcm a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Quantity -> tcm a -> tcm a
    forall (tcm :: * -> *) q a.
    (MonadTCEnv tcm, LensQuantity q) =>
    q -> tcm a -> tcm a
    applyQuantityToJudgement Quantity
    zeroQuantity