    {-# LANGUAGE NondecreasingIndentation #-}

    {-| Compile-time irrelevance.

    In type theory with compile-time irrelevance à la Pfenning (LiCS 2001),
    variables in the context are annotated with relevance attributes.
    @@
      Γ = r₁x₁:A₁, ..., rⱼxⱼ:Aⱼ
    @@
    To handle irrelevant projections, we also record the current relevance
    attribute in the judgement.  For instance, this attribute is equal to
    to 'Irrelevant' if we are in an irrelevant position, like an
    irrelevant argument.
    @@
      Γ ⊢r t : A
    @@
    Only relevant variables can be used:
    @@

      (Relevant x : A) ∈ Γ
      --------------------
      Γ  ⊢r  x  :  A
    @@
    Irrelevant global declarations can only be used if @r = Irrelevant@.

    When we enter a @r'@-relevant function argument, we compose the @r@ with @r'@
    and (left-)divide the attributes in the context by @r'@.
    @@
      Γ  ⊢r  t  :  (r' x : A) → B      r' \ Γ  ⊢(r'·r)  u  :  A
      ---------------------------------------------------------
      Γ  ⊢r  t u  :  B[u/x]
    @@
    No surprises for abstraction:
    @@

      Γ, (r' x : A)  ⊢r  :  B
      -----------------------------
      Γ  ⊢r  λxt  :  (r' x : A) → B
    @@

    This is different for runtime irrelevance (erasure) which is ``flat'',
    meaning that once one is in an irrelevant context, all new assumptions will
    be usable, since they are turned relevant once entering the context.
    See Conor McBride (WadlerFest 2016), for a type system in this spirit:

    We use such a rule for runtime-irrelevance:
    @@
      Γ, (q \ q') x : A  ⊢q  t  :  B
      ------------------------------
      Γ  ⊢q  λxt  :  (q' x : A) → B
    @@

    Conor's system is however set up differently, with a very different
    variable rule:

    @@

      (q x : A) ∈ Γ
      --------------
      Γ  ⊢q  x  :  A

      Γ, (q·p) x : A  ⊢q  t  :  B
      -----------------------------
      Γ  ⊢q  λxt  :  (p x : A) → B

      Γ  ⊢q  t  :  (p x : A) → B       Γ'  ⊢qp  u  :  A
      -------------------------------------------------
      Γ + Γ'  ⊢q  t u  :  B[u/x]
    @@

    -}

    module Agda.TypeChecking.Irrelevance where

    import Control.Arrow (second)

    import Control.Monad.Except

    import qualified Data.Map as Map

    import Agda.Interaction.Options

    import Agda.Syntax.Common
    import Agda.Syntax.Internal

    import Agda.TypeChecking.Monad
    import Agda.TypeChecking.Pretty
    import Agda.TypeChecking.Reduce
    import Agda.TypeChecking.Substitute.Class

    import Agda.Utils.Function
    import Agda.Utils.Lens
    import Agda.Utils.Maybe
    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
    nonStrictToIrr

    -- * 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
      Bool
    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
      VerboseKey -> VerboseLevel -> VerboseKey -> m a -> m a
    forall (m :: * -> *) a.
    MonadDebug m =>
    VerboseKey -> VerboseLevel -> VerboseKey -> m a -> m a
    verboseBracket VerboseKey
    "tc.irr" VerboseLevel
    60 VerboseKey
    "workOnTypes" (m a -> m a) -> m a -> m a
    forall a b. (a -> b) -> a -> b
    $ Bool -> m a -> m a
    forall (m :: * -> *) a. MonadTCEnv m => Bool -> m a -> m a
    workOnTypes' Bool
    allowed m a
    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
      = (if Bool
    experimental
         then (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 ((Relevance -> Relevance) -> Dom e -> Dom e
    forall a. LensRelevance a => (Relevance -> Relevance) -> a -> a
    mapRelevance Relevance -> Relevance
    irrToNonStrict)
         else m a -> m a
    forall a. a -> a
    id)
      (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
    applyQuantityToContext Quantity
    zeroQuantity
      (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 (m :: * -> *) a.
    MonadTCEnv m =>
    (TCEnv -> TCEnv) -> m a -> m a
    localTC (\ TCEnv
    e -> TCEnv
    e { envWorkingOnTypes :: Bool
    envWorkingOnTypes = Bool
    True })

    -- | (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 =
      case r -> Relevance
    forall a. LensRelevance a => a -> Relevance
    getRelevance r
    thing of
        Relevance
    Relevant -> tcm a -> tcm a
    forall a. a -> a
    id
        Relevance
    rel      -> 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

    -- | (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 (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' [ContextEntry] TCEnv -> LensMap [ContextEntry] TCEnv
    forall i o. Lens' i o -> LensMap i o
    over Lens' [ContextEntry] TCEnv
    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' (Map Name (Open (Term, Dom Type))) TCEnv
    -> LensMap (Map Name (Open (Term, Dom Type))) TCEnv
    forall i o. Lens' i o -> LensMap i o
    over Lens' (Map Name (Open (Term, Dom Type))) TCEnv
    eLetBindings ((Open (Term, Dom Type) -> Open (Term, Dom Type))
    -> Map Name (Open (Term, Dom Type))
    -> Map Name (Open (Term, Dom Type))
    forall a b k. (a -> b) -> Map k a -> Map k b
    Map.map ((Open (Term, Dom Type) -> Open (Term, Dom Type))
     -> Map Name (Open (Term, Dom Type))
     -> Map Name (Open (Term, Dom Type)))
    -> ((Dom Type -> Dom Type)
        -> Open (Term, Dom Type) -> Open (Term, Dom Type))
    -> (Dom Type -> Dom Type)
    -> Map Name (Open (Term, Dom Type))
    -> Map Name (Open (Term, Dom Type))
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ((Term, Dom Type) -> (Term, Dom Type))
    -> Open (Term, Dom Type) -> Open (Term, Dom Type)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (((Term, Dom Type) -> (Term, Dom Type))
     -> Open (Term, Dom Type) -> Open (Term, Dom Type))
    -> ((Dom Type -> Dom Type) -> (Term, Dom Type) -> (Term, Dom Type))
    -> (Dom Type -> Dom Type)
    -> Open (Term, Dom Type)
    -> Open (Term, Dom Type)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Dom Type -> Dom Type) -> (Term, Dom Type) -> (Term, Dom Type)
    forall (a :: * -> * -> *) b c d.
    Arrow a =>
    a b c -> a (d, b) (d, c)
    second ((Dom Type -> Dom Type)
     -> Map Name (Open (Term, Dom Type))
     -> Map Name (Open (Term, Dom Type)))
    -> (Dom Type -> Dom Type)
    -> Map Name (Open (Term, Dom Type))
    -> Map Name (Open (Term, Dom Type))
    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 (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' Relevance TCEnv -> LensMap Relevance TCEnv
    forall i o. Lens' i o -> LensMap i o
    over Lens' Relevance TCEnv
    eRelevance LensMap Relevance TCEnv
    -> (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
        Relevance
    Relevant -> tcm a
    cont
        Relevance
    rel -> tcm Bool -> (tcm a -> tcm a) -> tcm a -> tcm a
    forall (m :: * -> *) a.
    Monad m =>
    m Bool -> (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

    -- | Sets the current quantity (unless the given quantity is 1).
    applyQuantityToContext :: (MonadTCEnv tcm, LensQuantity q) => q -> tcm a -> tcm a
    applyQuantityToContext :: forall (tcm :: * -> *) q a.
    (MonadTCEnv tcm, LensQuantity q) =>
    q -> tcm a -> tcm a
    applyQuantityToContext q
    thing =
      case q -> Quantity
    forall a. LensQuantity a => a -> Quantity
    getQuantity q
    thing of
        Quantity1{} -> tcm a -> tcm a
    forall a. a -> a
    id
        Quantity
    q           -> Quantity -> tcm a -> tcm a
    forall (tcm :: * -> *) a.
    MonadTCEnv tcm =>
    Quantity -> tcm a -> tcm a
    applyQuantityToJudgementOnly Quantity
    q

    -- | Apply quantity @q@ the the quantity annotation of the (typing/equality)
    --   judgement.  This is part of the work done when going into a @q@-context.
    --
    --   Precondition: @Quantity /= Quantity1@
    applyQuantityToJudgementOnly :: (MonadTCEnv tcm) => Quantity -> tcm a -> tcm a
    applyQuantityToJudgementOnly :: forall (tcm :: * -> *) a.
    MonadTCEnv tcm =>
    Quantity -> tcm a -> tcm a
    applyQuantityToJudgementOnly = (TCEnv -> TCEnv) -> tcm a -> tcm a
    forall (m :: * -> *) a.
    MonadTCEnv m =>
    (TCEnv -> TCEnv) -> m a -> m a
    localTC ((TCEnv -> TCEnv) -> tcm a -> tcm a)
    -> (Quantity -> TCEnv -> TCEnv) -> Quantity -> tcm a -> tcm a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Lens' Quantity TCEnv -> LensMap Quantity TCEnv
    forall i o. Lens' i o -> LensMap i o
    over Lens' Quantity TCEnv
    eQuantity LensMap Quantity TCEnv
    -> (Quantity -> Quantity -> Quantity) -> Quantity -> TCEnv -> TCEnv
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Quantity -> Quantity -> Quantity
    composeQuantity

    -- | 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 (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' [ContextEntry] TCEnv -> LensMap [ContextEntry] TCEnv
    forall i o. Lens' i o -> LensMap i o
    over Lens' [ContextEntry] TCEnv
    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' (Map Name (Open (Term, Dom Type))) TCEnv
    -> LensMap (Map Name (Open (Term, Dom Type))) TCEnv
    forall i o. Lens' i o -> LensMap i o
    over Lens' (Map Name (Open (Term, Dom Type))) TCEnv
    eLetBindings ((Open (Term, Dom Type) -> Open (Term, Dom Type))
    -> Map Name (Open (Term, Dom Type))
    -> Map Name (Open (Term, Dom Type))
    forall a b k. (a -> b) -> Map k a -> Map k b
    Map.map ((Open (Term, Dom Type) -> Open (Term, Dom Type))
     -> Map Name (Open (Term, Dom Type))
     -> Map Name (Open (Term, Dom Type)))
    -> ((Dom Type -> Dom Type)
        -> Open (Term, Dom Type) -> Open (Term, Dom Type))
    -> (Dom Type -> Dom Type)
    -> Map Name (Open (Term, Dom Type))
    -> Map Name (Open (Term, Dom Type))
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ((Term, Dom Type) -> (Term, Dom Type))
    -> Open (Term, Dom Type) -> Open (Term, Dom Type)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (((Term, Dom Type) -> (Term, Dom Type))
     -> Open (Term, Dom Type) -> Open (Term, Dom Type))
    -> ((Dom Type -> Dom Type) -> (Term, Dom Type) -> (Term, Dom Type))
    -> (Dom Type -> Dom Type)
    -> Open (Term, Dom Type)
    -> Open (Term, Dom Type)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Dom Type -> Dom Type) -> (Term, Dom Type) -> (Term, Dom Type)
    forall (a :: * -> * -> *) b c d.
    Arrow a =>
    a b c -> a (d, b) (d, c)
    second ((Dom Type -> Dom Type)
     -> Map Name (Open (Term, Dom Type))
     -> Map Name (Open (Term, Dom Type)))
    -> (Dom Type -> Dom Type)
    -> Map Name (Open (Term, Dom Type))
    -> Map Name (Open (Term, Dom Type))
    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 (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 (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)

    -- | (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 (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' [ContextEntry] TCEnv -> LensMap [ContextEntry] TCEnv
    forall i o. Lens' i o -> LensMap i o
    over Lens' [ContextEntry] TCEnv
    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' (Map Name (Open (Term, Dom Type))) TCEnv
    -> LensMap (Map Name (Open (Term, Dom Type))) TCEnv
    forall i o. Lens' i o -> LensMap i o
    over Lens' (Map Name (Open (Term, Dom Type))) TCEnv
    eLetBindings
          ((Open (Term, Dom Type) -> Open (Term, Dom Type))
    -> Map Name (Open (Term, Dom Type))
    -> Map Name (Open (Term, Dom Type))
    forall a b k. (a -> b) -> Map k a -> Map k b
    Map.map ((Open (Term, Dom Type) -> Open (Term, Dom Type))
     -> Map Name (Open (Term, Dom Type))
     -> Map Name (Open (Term, Dom Type)))
    -> ((Dom Type -> Dom Type)
        -> Open (Term, Dom Type) -> Open (Term, Dom Type))
    -> (Dom Type -> Dom Type)
    -> Map Name (Open (Term, Dom Type))
    -> Map Name (Open (Term, Dom Type))
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ((Term, Dom Type) -> (Term, Dom Type))
    -> Open (Term, Dom Type) -> Open (Term, Dom Type)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (((Term, Dom Type) -> (Term, Dom Type))
     -> Open (Term, Dom Type) -> Open (Term, Dom Type))
    -> ((Dom Type -> Dom Type) -> (Term, Dom Type) -> (Term, Dom Type))
    -> (Dom Type -> Dom Type)
    -> Open (Term, Dom Type)
    -> Open (Term, Dom Type)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Dom Type -> Dom Type) -> (Term, Dom Type) -> (Term, Dom Type)
    forall (a :: * -> * -> *) b c d.
    Arrow a =>
    a b c -> a (d, b) (d, c)
    second ((Dom Type -> Dom Type)
     -> Map Name (Open (Term, Dom Type))
     -> Map Name (Open (Term, Dom Type)))
    -> (Dom Type -> Dom Type)
    -> Map Name (Open (Term, Dom Type))
    -> Map Name (Open (Term, Dom Type))
    forall a b. (a -> b) -> a -> b
    $ Modality -> Dom Type -> Dom Type
    forall a. LensModality a => Modality -> a -> a
    inverseApplyModalityButNotQuantity Modality
    m)

    -- | Apply modality @m@ the the modality annotation of the (typing/equality)
    --   judgement.  This is part of the work done when going into a @m@-context.
    --
    --   Precondition: @Modality /= Relevant@
    applyModalityToJudgementOnly :: (MonadTCEnv tcm) => Modality -> tcm a -> tcm a
    applyModalityToJudgementOnly :: forall (tcm :: * -> *) a.
    MonadTCEnv tcm =>
    Modality -> tcm a -> tcm a
    applyModalityToJudgementOnly = (TCEnv -> TCEnv) -> tcm a -> tcm a
    forall (m :: * -> *) a.
    MonadTCEnv m =>
    (TCEnv -> TCEnv) -> m a -> m a
    localTC ((TCEnv -> TCEnv) -> tcm a -> tcm a)
    -> (Modality -> TCEnv -> TCEnv) -> Modality -> tcm a -> tcm a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Lens' Modality TCEnv -> LensMap Modality TCEnv
    forall i o. Lens' i o -> LensMap i o
    over Lens' Modality TCEnv
    eModality LensMap Modality TCEnv
    -> (Modality -> Modality -> Modality) -> Modality -> TCEnv -> TCEnv
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Modality -> Modality -> Modality
    composeModality

    -- | 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
    $ Quantity -> tcm a -> tcm a
    forall (tcm :: * -> *) q a.
    (MonadTCEnv tcm, LensQuantity q) =>
    q -> tcm a -> tcm a
    applyQuantityToContext (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 :: * -> *) a.
    MonadTCEnv tcm =>
    Quantity -> tcm a -> tcm a
    applyQuantityToJudgementOnly Quantity
    zeroQuantity

    -- | Check whether something can be used in a position of the given relevance.
    --
    --   This is a substitute for double-checking that only makes sure
    --   relevances are correct.  See issue #2640.
    --
    --   Used in unifier (@ unifyStep Solution{}@).
    --
    --   At the moment, this implements McBride-style irrelevance,
    --   where Pfenning-style would be the most accurate thing.
    --   However, these two notions only differ how they handle
    --   bound variables in a term.  Here, we are only concerned
    --   in the free variables, used meta-variables, and used
    --   (irrelevant) definitions.
    --
    class UsableRelevance a where
      usableRel
        :: (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m, MonadDebug m)
        => Relevance -> a -> m Bool

    instance UsableRelevance Term where
      usableRel :: forall (m :: * -> *).
    (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m,
     MonadDebug m) =>
    Relevance -> Term -> m Bool
    usableRel Relevance
    rel = \case
        Var VerboseLevel
    i Elims
    vs -> do
          Relevance
    irel <- Dom Type -> Relevance
    forall a. LensRelevance a => a -> Relevance
    getRelevance (Dom Type -> Relevance) -> m (Dom Type) -> m Relevance
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> VerboseLevel -> m (Dom Type)
    forall (m :: * -> *).
    (Applicative m, MonadFail m, MonadTCEnv m) =>
    VerboseLevel -> m (Dom Type)
    domOfBV VerboseLevel
    i
          let ok :: Bool
    ok = Relevance
    irel Relevance -> Relevance -> Bool
    `moreRelevant` Relevance
    rel
          VerboseKey -> VerboseLevel -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> VerboseLevel -> TCMT IO Doc -> m ()
    reportSDoc VerboseKey
    "tc.irr" VerboseLevel
    50 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
    forall a b. (a -> b) -> a -> b
    $
            TCMT IO Doc
    "Variable" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM (VerboseLevel -> Term
    var VerboseLevel
    i) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+>
            VerboseKey -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => VerboseKey -> m Doc
    text (VerboseKey
    "has relevance " VerboseKey -> VerboseKey -> VerboseKey
    forall a. [a] -> [a] -> [a]
    ++ Relevance -> VerboseKey
    forall a. Show a => a -> VerboseKey
    show Relevance
    irel VerboseKey -> VerboseKey -> VerboseKey
    forall a. [a] -> [a] -> [a]
    ++ VerboseKey
    ", which is " VerboseKey -> VerboseKey -> VerboseKey
    forall a. [a] -> [a] -> [a]
    ++
                  (if Bool
    ok then VerboseKey
    "" else VerboseKey
    "NOT ") VerboseKey -> VerboseKey -> VerboseKey
    forall a. [a] -> [a] -> [a]
    ++ VerboseKey
    "more relevant than " VerboseKey -> VerboseKey -> VerboseKey
    forall a. [a] -> [a] -> [a]
    ++ Relevance -> VerboseKey
    forall a. Show a => a -> VerboseKey
    show Relevance
    rel)
          Bool -> m Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    ok m Bool -> m Bool -> m Bool
    forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
    `and2M` Relevance -> Elims -> m Bool
    forall a (m :: * -> *).
    (UsableRelevance a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
     MonadAddContext m, MonadDebug m) =>
    Relevance -> a -> m Bool
    usableRel Relevance
    rel Elims
    vs
        Def QName
    f Elims
    vs -> do
          Relevance
    frel <- QName -> m Relevance
    forall (m :: * -> *). HasConstInfo m => QName -> m Relevance
    relOfConst QName
    f
          Bool -> m Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Relevance
    frel Relevance -> Relevance -> Bool
    `moreRelevant` Relevance
    rel) m Bool -> m Bool -> m Bool
    forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
    `and2M` Relevance -> Elims -> m Bool
    forall a (m :: * -> *).
    (UsableRelevance a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
     MonadAddContext m, MonadDebug m) =>
    Relevance -> a -> m Bool
    usableRel Relevance
    rel Elims
    vs
        Con ConHead
    c ConInfo
    _ Elims
    vs -> Relevance -> Elims -> m Bool
    forall a (m :: * -> *).
    (UsableRelevance a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
     MonadAddContext m, MonadDebug m) =>
    Relevance -> a -> m Bool
    usableRel Relevance
    rel Elims
    vs
        Lit Literal
    l    -> Bool -> m Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    True
        Lam ArgInfo
    _ Abs Term
    v  -> Relevance -> Abs Term -> m Bool
    forall a (m :: * -> *).
    (UsableRelevance a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
     MonadAddContext m, MonadDebug m) =>
    Relevance -> a -> m Bool
    usableRel Relevance
    rel Abs Term
    v
        Pi Dom Type
    a Abs Type
    b   -> Relevance -> (Dom Type, Abs Type) -> m Bool
    forall a (m :: * -> *).
    (UsableRelevance a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
     MonadAddContext m, MonadDebug m) =>
    Relevance -> a -> m Bool
    usableRel Relevance
    rel (Dom Type
    a,Abs Type
    b)
        Sort Sort
    s   -> Relevance -> Sort -> m Bool
    forall a (m :: * -> *).
    (UsableRelevance a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
     MonadAddContext m, MonadDebug m) =>
    Relevance -> a -> m Bool
    usableRel Relevance
    rel Sort
    s
        Level Level
    l  -> Bool -> m Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    True
        MetaV MetaId
    m Elims
    vs -> do
          Relevance
    mrel <- MetaVariable -> Relevance
    getMetaRelevance (MetaVariable -> Relevance) -> m MetaVariable -> m Relevance
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> MetaId -> m MetaVariable
    forall (m :: * -> *).
    (MonadFail m, ReadTCState m) =>
    MetaId -> m MetaVariable
    lookupMeta MetaId
    m
          Bool -> m Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Relevance
    mrel Relevance -> Relevance -> Bool
    `moreRelevant` Relevance
    rel) m Bool -> m Bool -> m Bool
    forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
    `and2M` Relevance -> Elims -> m Bool
    forall a (m :: * -> *).
    (UsableRelevance a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
     MonadAddContext m, MonadDebug m) =>
    Relevance -> a -> m Bool
    usableRel Relevance
    rel Elims
    vs
        DontCare Term
    v -> Relevance -> Term -> m Bool
    forall a (m :: * -> *).
    (UsableRelevance a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
     MonadAddContext m, MonadDebug m) =>
    Relevance -> a -> m Bool
    usableRel Relevance
    rel Term
    v -- TODO: allow irrelevant things to be used in DontCare position?
        Dummy{}  -> Bool -> m Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    True

    instance UsableRelevance a => UsableRelevance (Type' a) where
      usableRel :: forall (m :: * -> *).
    (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m,
     MonadDebug m) =>
    Relevance -> Type' a -> m Bool
    usableRel Relevance
    rel (El Sort
    _ a
    t) = Relevance -> a -> m Bool
    forall a (m :: * -> *).
    (UsableRelevance a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
     MonadAddContext m, MonadDebug m) =>
    Relevance -> a -> m Bool
    usableRel Relevance
    rel a
    t

    instance UsableRelevance Sort where
      usableRel :: forall (m :: * -> *).
    (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m,
     MonadDebug m) =>
    Relevance -> Sort -> m Bool
    usableRel Relevance
    rel = \case
        Type Level
    l -> Relevance -> Level -> m Bool
    forall a (m :: * -> *).
    (UsableRelevance a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
     MonadAddContext m, MonadDebug m) =>
    Relevance -> a -> m Bool
    usableRel Relevance
    rel Level
    l
        Prop Level
    l -> Relevance -> Level -> m Bool
    forall a (m :: * -> *).
    (UsableRelevance a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
     MonadAddContext m, MonadDebug m) =>
    Relevance -> a -> m Bool
    usableRel Relevance
    rel Level
    l
        Inf IsFibrant
    f Integer
    n -> Bool -> m Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    True
        SSet Level
    l -> Relevance -> Level -> m Bool
    forall a (m :: * -> *).
    (UsableRelevance a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
     MonadAddContext m, MonadDebug m) =>
    Relevance -> a -> m Bool
    usableRel Relevance
    rel Level
    l
        Sort
    SizeUniv -> Bool -> m Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    True
        Sort
    LockUniv -> Bool -> m Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    True
        PiSort Dom' Term Term
    a Sort
    s1 Abs Sort
    s2 -> Relevance -> (Dom' Term Term, Sort, Abs Sort) -> m Bool
    forall a (m :: * -> *).
    (UsableRelevance a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
     MonadAddContext m, MonadDebug m) =>
    Relevance -> a -> m Bool
    usableRel Relevance
    rel (Dom' Term Term
    a,Sort
    s1,Abs Sort
    s2)
        FunSort Sort
    s1 Sort
    s2 -> Relevance -> (Sort, Sort) -> m Bool
    forall a (m :: * -> *).
    (UsableRelevance a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
     MonadAddContext m, MonadDebug m) =>
    Relevance -> a -> m Bool
    usableRel Relevance
    rel (Sort
    s1,Sort
    s2)
        UnivSort Sort
    s -> Relevance -> Sort -> m Bool
    forall a (m :: * -> *).
    (UsableRelevance a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
     MonadAddContext m, MonadDebug m) =>
    Relevance -> a -> m Bool
    usableRel Relevance
    rel Sort
    s
        MetaS MetaId
    x Elims
    es -> Relevance -> Elims -> m Bool
    forall a (m :: * -> *).
    (UsableRelevance a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
     MonadAddContext m, MonadDebug m) =>
    Relevance -> a -> m Bool
    usableRel Relevance
    rel Elims
    es
        DefS QName
    d Elims
    es  -> Relevance -> Term -> m Bool
    forall a (m :: * -> *).
    (UsableRelevance a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
     MonadAddContext m, MonadDebug m) =>
    Relevance -> a -> m Bool
    usableRel Relevance
    rel (Term -> m Bool) -> Term -> m Bool
    forall a b. (a -> b) -> a -> b
    $ QName -> Elims -> Term
    Def QName
    d Elims
    es
        DummyS{} -> Bool -> m Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    True

    instance UsableRelevance Level where
      usableRel :: forall (m :: * -> *).
    (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m,
     MonadDebug m) =>
    Relevance -> Level -> m Bool
    usableRel Relevance
    rel (Max Integer
    _ [PlusLevel' Term]
    ls) = Relevance -> [PlusLevel' Term] -> m Bool
    forall a (m :: * -> *).
    (UsableRelevance a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
     MonadAddContext m, MonadDebug m) =>
    Relevance -> a -> m Bool
    usableRel Relevance
    rel [PlusLevel' Term]
    ls

    instance UsableRelevance PlusLevel where
      usableRel :: forall (m :: * -> *).
    (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m,
     MonadDebug m) =>
    Relevance -> PlusLevel' Term -> m Bool
    usableRel Relevance
    rel (Plus Integer
    _ Term
    l) = Relevance -> Term -> m Bool
    forall a (m :: * -> *).
    (UsableRelevance a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
     MonadAddContext m, MonadDebug m) =>
    Relevance -> a -> m Bool
    usableRel Relevance
    rel Term
    l

    instance UsableRelevance a => UsableRelevance [a] where
      usableRel :: forall (m :: * -> *).
    (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m,
     MonadDebug m) =>
    Relevance -> [a] -> m Bool
    usableRel Relevance
    rel = [m Bool] -> m Bool
    forall (f :: * -> *) (m :: * -> *).
    (Foldable f, Monad m) =>
    f (m Bool) -> m Bool
    andM ([m Bool] -> m Bool) -> ([a] -> [m Bool]) -> [a] -> m Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (a -> m Bool) -> [a] -> [m Bool]
    forall a b. (a -> b) -> [a] -> [b]
    map (Relevance -> a -> m Bool
    forall a (m :: * -> *).
    (UsableRelevance a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
     MonadAddContext m, MonadDebug m) =>
    Relevance -> a -> m Bool
    usableRel Relevance
    rel)

    instance (UsableRelevance a, UsableRelevance b) => UsableRelevance (a,b) where
      usableRel :: forall (m :: * -> *).
    (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m,
     MonadDebug m) =>
    Relevance -> (a, b) -> m Bool
    usableRel Relevance
    rel (a
    a,b
    b) = Relevance -> a -> m Bool
    forall a (m :: * -> *).
    (UsableRelevance a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
     MonadAddContext m, MonadDebug m) =>
    Relevance -> a -> m Bool
    usableRel Relevance
    rel a
    a m Bool -> m Bool -> m Bool
    forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
    `and2M` Relevance -> b -> m Bool
    forall a (m :: * -> *).
    (UsableRelevance a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
     MonadAddContext m, MonadDebug m) =>
    Relevance -> a -> m Bool
    usableRel Relevance
    rel b
    b

    instance (UsableRelevance a, UsableRelevance b, UsableRelevance c) => UsableRelevance (a,b,c) where
      usableRel :: forall (m :: * -> *).
    (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m,
     MonadDebug m) =>
    Relevance -> (a, b, c) -> m Bool
    usableRel Relevance
    rel (a
    a,b
    b,c
    c) = Relevance -> a -> m Bool
    forall a (m :: * -> *).
    (UsableRelevance a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
     MonadAddContext m, MonadDebug m) =>
    Relevance -> a -> m Bool
    usableRel Relevance
    rel a
    a m Bool -> m Bool -> m Bool
    forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
    `and2M` Relevance -> b -> m Bool
    forall a (m :: * -> *).
    (UsableRelevance a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
     MonadAddContext m, MonadDebug m) =>
    Relevance -> a -> m Bool
    usableRel Relevance
    rel b
    b m Bool -> m Bool -> m Bool
    forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
    `and2M` Relevance -> c -> m Bool
    forall a (m :: * -> *).
    (UsableRelevance a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
     MonadAddContext m, MonadDebug m) =>
    Relevance -> a -> m Bool
    usableRel Relevance
    rel c
    c

    instance UsableRelevance a => UsableRelevance (Elim' a) where
      usableRel :: forall (m :: * -> *).
    (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m,
     MonadDebug m) =>
    Relevance -> Elim' a -> m Bool
    usableRel Relevance
    rel (Apply Arg a
    a) = Relevance -> Arg a -> m Bool
    forall a (m :: * -> *).
    (UsableRelevance a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
     MonadAddContext m, MonadDebug m) =>
    Relevance -> a -> m Bool
    usableRel Relevance
    rel Arg a
    a
      usableRel Relevance
    rel (Proj ProjOrigin
    _ QName
    p) = do
        Relevance
    prel <- QName -> m Relevance
    forall (m :: * -> *). HasConstInfo m => QName -> m Relevance
    relOfConst QName
    p
        Bool -> m Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Bool -> m Bool) -> Bool -> m Bool
    forall a b. (a -> b) -> a -> b
    $ Relevance
    prel Relevance -> Relevance -> Bool
    `moreRelevant` Relevance
    rel
      usableRel Relevance
    rel (IApply a
    x a
    y a
    v) = [a] -> (a -> m Bool) -> m Bool
    forall (f :: * -> *) (m :: * -> *) a.
    (Functor f, Foldable f, Monad m) =>
    f a -> (a -> m Bool) -> m Bool
    allM [a
    x,a
    y,a
    v] ((a -> m Bool) -> m Bool) -> (a -> m Bool) -> m Bool
    forall a b. (a -> b) -> a -> b
    $ Relevance -> a -> m Bool
    forall a (m :: * -> *).
    (UsableRelevance a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
     MonadAddContext m, MonadDebug m) =>
    Relevance -> a -> m Bool
    usableRel Relevance
    rel

    instance UsableRelevance a => UsableRelevance (Arg a) where
      usableRel :: forall (m :: * -> *).
    (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m,
     MonadDebug m) =>
    Relevance -> Arg a -> m Bool
    usableRel Relevance
    rel (Arg ArgInfo
    info a
    u) =
        let rel' :: Relevance
    rel' = ArgInfo -> Relevance
    forall a. LensRelevance a => a -> Relevance
    getRelevance ArgInfo
    info
        in  Relevance -> a -> m Bool
    forall a (m :: * -> *).
    (UsableRelevance a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
     MonadAddContext m, MonadDebug m) =>
    Relevance -> a -> m Bool
    usableRel (Relevance
    rel Relevance -> Relevance -> Relevance
    `composeRelevance` Relevance
    rel') a
    u

    instance UsableRelevance a => UsableRelevance (Dom a) where
      usableRel :: forall (m :: * -> *).
    (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m,
     MonadDebug m) =>
    Relevance -> Dom a -> m Bool
    usableRel Relevance
    rel Dom{unDom :: forall t e. Dom' t e -> e
    unDom = a
    u} = Relevance -> a -> m Bool
    forall a (m :: * -> *).
    (UsableRelevance a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
     MonadAddContext m, MonadDebug m) =>
    Relevance -> a -> m Bool
    usableRel Relevance
    rel a
    u

    instance (Subst a, UsableRelevance a) => UsableRelevance (Abs a) where
      usableRel :: forall (m :: * -> *).
    (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m,
     MonadDebug m) =>
    Relevance -> Abs a -> m Bool
    usableRel Relevance
    rel Abs a
    abs = Abs a -> (a -> m Bool) -> m Bool
    forall a (m :: * -> *) b.
    (Subst a, MonadAddContext m) =>
    Abs a -> (a -> m b) -> m b
    underAbstraction_ Abs a
    abs ((a -> m Bool) -> m Bool) -> (a -> m Bool) -> m Bool
    forall a b. (a -> b) -> a -> b
    $ \a
    u -> Relevance -> a -> m Bool
    forall a (m :: * -> *).
    (UsableRelevance a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
     MonadAddContext m, MonadDebug m) =>
    Relevance -> a -> m Bool
    usableRel Relevance
    rel a
    u

    -- | Check whether something can be used in a position of the given modality.
    --
    --   This is a substitute for double-checking that only makes sure
    --   modalities are correct.  See issue #2640.
    --
    --   Used in unifier (@ unifyStep Solution{}@).
    --
    --   This uses McBride-style modality checking.
    --   It does not differ from Pfenning-style if we
    --   are only interested in the modality of the
    --   free variables, used meta-variables, and used
    --   definitions.
    --
    class UsableModality a where
      usableMod
        :: (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m, MonadDebug m, MonadReduce m, MonadError Blocker m)
        => Modality -> a -> m Bool

    instance UsableModality Term where
      usableMod :: forall (m :: * -> *).
    (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m,
     MonadDebug m, MonadReduce m, MonadError Blocker m) =>
    Modality -> Term -> m Bool
    usableMod Modality
    mod Term
    u = do
       case Term
    u of
        Var VerboseLevel
    i Elims
    vs -> do
          Modality
    imod <- Dom Type -> Modality
    forall a. LensModality a => a -> Modality
    getModality (Dom Type -> Modality) -> m (Dom Type) -> m Modality
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> VerboseLevel -> m (Dom Type)
    forall (m :: * -> *).
    (Applicative m, MonadFail m, MonadTCEnv m) =>
    VerboseLevel -> m (Dom Type)
    domOfBV VerboseLevel
    i
          let ok :: Bool
    ok = Modality
    imod Modality -> Modality -> Bool
    `moreUsableModality` Modality
    mod
          VerboseKey -> VerboseLevel -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> VerboseLevel -> TCMT IO Doc -> m ()
    reportSDoc VerboseKey
    "tc.irr" VerboseLevel
    50 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
    forall a b. (a -> b) -> a -> b
    $
            TCMT IO Doc
    "Variable" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM (VerboseLevel -> Term
    var VerboseLevel
    i) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+>
            VerboseKey -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => VerboseKey -> m Doc
    text (VerboseKey
    "has modality " VerboseKey -> VerboseKey -> VerboseKey
    forall a. [a] -> [a] -> [a]
    ++ Modality -> VerboseKey
    forall a. Show a => a -> VerboseKey
    show Modality
    imod VerboseKey -> VerboseKey -> VerboseKey
    forall a. [a] -> [a] -> [a]
    ++ VerboseKey
    ", which is a " VerboseKey -> VerboseKey -> VerboseKey
    forall a. [a] -> [a] -> [a]
    ++
                  (if Bool
    ok then VerboseKey
    "" else VerboseKey
    "NOT ") VerboseKey -> VerboseKey -> VerboseKey
    forall a. [a] -> [a] -> [a]
    ++ VerboseKey
    "more usable modality than " VerboseKey -> VerboseKey -> VerboseKey
    forall a. [a] -> [a] -> [a]
    ++ Modality -> VerboseKey
    forall a. Show a => a -> VerboseKey
    show Modality
    mod)
          Bool -> m Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    ok m Bool -> m Bool -> m Bool
    forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
    `and2M` Modality -> Elims -> m Bool
    forall a (m :: * -> *).
    (UsableModality a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
     MonadAddContext m, MonadDebug m, MonadReduce m,
     MonadError Blocker m) =>
    Modality -> a -> m Bool
    usableMod Modality
    mod Elims
    vs
        Def QName
    f Elims
    vs -> do
          Modality
    fmod <- QName -> m Modality
    forall (m :: * -> *). HasConstInfo m => QName -> m Modality
    modalityOfConst QName
    f
          let ok :: Bool
    ok = Modality
    fmod Modality -> Modality -> Bool
    `moreUsableModality` Modality
    mod
          VerboseKey -> VerboseLevel -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> VerboseLevel -> TCMT IO Doc -> m ()
    reportSDoc VerboseKey
    "tc.irr" VerboseLevel
    50 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
    forall a b. (a -> b) -> a -> b
    $
            TCMT IO Doc
    "Definition" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM (QName -> Elims -> Term
    Def QName
    f []) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+>
            VerboseKey -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => VerboseKey -> m Doc
    text (VerboseKey
    "has modality " VerboseKey -> VerboseKey -> VerboseKey
    forall a. [a] -> [a] -> [a]
    ++ Modality -> VerboseKey
    forall a. Show a => a -> VerboseKey
    show Modality
    fmod VerboseKey -> VerboseKey -> VerboseKey
    forall a. [a] -> [a] -> [a]
    ++ VerboseKey
    ", which is a " VerboseKey -> VerboseKey -> VerboseKey
    forall a. [a] -> [a] -> [a]
    ++
                  (if Bool
    ok then VerboseKey
    "" else VerboseKey
    "NOT ") VerboseKey -> VerboseKey -> VerboseKey
    forall a. [a] -> [a] -> [a]
    ++ VerboseKey
    "more usable modality than " VerboseKey -> VerboseKey -> VerboseKey
    forall a. [a] -> [a] -> [a]
    ++ Modality -> VerboseKey
    forall a. Show a => a -> VerboseKey
    show Modality
    mod)
          Bool -> m Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    ok m Bool -> m Bool -> m Bool
    forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
    `and2M` Modality -> Elims -> m Bool
    forall a (m :: * -> *).
    (UsableModality a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
     MonadAddContext m, MonadDebug m, MonadReduce m,
     MonadError Blocker m) =>
    Modality -> a -> m Bool
    usableMod Modality
    mod Elims
    vs
        Con ConHead
    c ConInfo
    _ Elims
    vs -> Modality -> Elims -> m Bool
    forall a (m :: * -> *).
    (UsableModality a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
     MonadAddContext m, MonadDebug m, MonadReduce m,
     MonadError Blocker m) =>
    Modality -> a -> m Bool
    usableMod Modality
    mod Elims
    vs
        Lit Literal
    l    -> Bool -> m Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    True
        Lam ArgInfo
    info Abs Term
    v  -> ArgInfo -> Modality -> Abs Term -> m Bool
    forall a (m :: * -> *).
    (Subst a, MonadAddContext m, UsableModality a, ReadTCState m,
     HasConstInfo m, MonadReduce m, MonadError Blocker m) =>
    ArgInfo -> Modality -> Abs a -> m Bool
    usableModAbs ArgInfo
    info Modality
    mod Abs Term
    v
        -- Even if Pi contains Type, here we check it as a constructor for terms in the universe.
        Pi Dom Type
    a Abs Type
    b   -> Modality -> Term -> m Bool
    forall a (m :: * -> *).
    (UsableModality a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
     MonadAddContext m, MonadDebug m, MonadReduce m,
     MonadError Blocker m) =>
    Modality -> a -> m Bool
    usableMod Modality
    domMod (Type -> Term
    forall t a. Type'' t a -> a
    unEl (Type -> Term) -> Type -> Term
    forall a b. (a -> b) -> a -> b
    $ Dom Type -> Type
    forall t e. Dom' t e -> e
    unDom Dom Type
    a) m Bool -> m Bool -> m Bool
    forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
    `and2M` ArgInfo -> Modality -> Abs Term -> m Bool
    forall a (m :: * -> *).
    (Subst a, MonadAddContext m, UsableModality a, ReadTCState m,
     HasConstInfo m, MonadReduce m, MonadError Blocker m) =>
    ArgInfo -> Modality -> Abs a -> m Bool
    usableModAbs (Dom Type -> ArgInfo
    forall a. LensArgInfo a => a -> ArgInfo
    getArgInfo Dom Type
    a) Modality
    mod (Type -> Term
    forall t a. Type'' t a -> a
    unEl (Type -> Term) -> Abs Type -> Abs Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Abs Type
    b)
          where
            domMod :: Modality
    domMod = (Quantity -> Quantity) -> Modality -> Modality
    forall a. LensQuantity a => (Quantity -> Quantity) -> a -> a
    mapQuantity (Quantity -> Quantity -> Quantity
    composeQuantity (Quantity -> Quantity -> Quantity)
    -> Quantity -> Quantity -> Quantity
    forall a b. (a -> b) -> a -> b
    $ Dom Type -> Quantity
    forall a. LensQuantity a => a -> Quantity
    getQuantity Dom Type
    a) (Modality -> Modality) -> Modality -> Modality
    forall a b. (a -> b) -> a -> b
    $
                     (Cohesion -> Cohesion) -> Modality -> Modality
    forall a. LensCohesion a => (Cohesion -> Cohesion) -> a -> a
    mapCohesion (Cohesion -> Cohesion -> Cohesion
    composeCohesion (Cohesion -> Cohesion -> Cohesion)
    -> Cohesion -> Cohesion -> Cohesion
    forall a b. (a -> b) -> a -> b
    $ Dom Type -> Cohesion
    forall a. LensCohesion a => a -> Cohesion
    getCohesion Dom Type
    a) Modality
    mod
        -- Andrea 15/10/2020 not updating these cases yet, but they are quite suspicious,
        -- do we have special typing rules for Sort and Level?
        Sort Sort
    s   -> Modality -> Sort -> m Bool
    forall a (m :: * -> *).
    (UsableModality a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
     MonadAddContext m, MonadDebug m, MonadReduce m,
     MonadError Blocker m) =>
    Modality -> a -> m Bool
    usableMod Modality
    mod Sort
    s
        Level Level
    l  -> Bool -> m Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    True
        MetaV MetaId
    m Elims
    vs -> do
          Modality
    mmod <- MetaVariable -> Modality
    getMetaModality (MetaVariable -> Modality) -> m MetaVariable -> m Modality
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> MetaId -> m MetaVariable
    forall (m :: * -> *).
    (MonadFail m, ReadTCState m) =>
    MetaId -> m MetaVariable
    lookupMeta MetaId
    m
          let ok :: Bool
    ok = Modality
    mmod Modality -> Modality -> Bool
    `moreUsableModality` Modality
    mod
          VerboseKey -> VerboseLevel -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> VerboseLevel -> TCMT IO Doc -> m ()
    reportSDoc VerboseKey
    "tc.irr" VerboseLevel
    50 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
    forall a b. (a -> b) -> a -> b
    $
            TCMT IO Doc
    "Metavariable" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM (MetaId -> Elims -> Term
    MetaV MetaId
    m []) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+>
            VerboseKey -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => VerboseKey -> m Doc
    text (VerboseKey
    "has modality " VerboseKey -> VerboseKey -> VerboseKey
    forall a. [a] -> [a] -> [a]
    ++ Modality -> VerboseKey
    forall a. Show a => a -> VerboseKey
    show Modality
    mmod VerboseKey -> VerboseKey -> VerboseKey
    forall a. [a] -> [a] -> [a]
    ++ VerboseKey
    ", which is a " VerboseKey -> VerboseKey -> VerboseKey
    forall a. [a] -> [a] -> [a]
    ++
                  (if Bool
    ok then VerboseKey
    "" else VerboseKey
    "NOT ") VerboseKey -> VerboseKey -> VerboseKey
    forall a. [a] -> [a] -> [a]
    ++ VerboseKey
    "more usable modality than " VerboseKey -> VerboseKey -> VerboseKey
    forall a. [a] -> [a] -> [a]
    ++ Modality -> VerboseKey
    forall a. Show a => a -> VerboseKey
    show Modality
    mod)
          (Bool -> m Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    ok m Bool -> m Bool -> m Bool
    forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
    `and2M` Modality -> Elims -> m Bool
    forall a (m :: * -> *).
    (UsableModality a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
     MonadAddContext m, MonadDebug m, MonadReduce m,
     MonadError Blocker m) =>
    Modality -> a -> m Bool
    usableMod Modality
    mod Elims
    vs) m Bool -> m Bool -> m Bool
    forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
    `or2M` do
            Term
    u <- Term -> m Term
    forall a (m :: * -> *). (Instantiate a, MonadReduce m) => a -> m a
    instantiate Term
    u
            Maybe MetaId -> m Bool -> (MetaId -> m Bool) -> m Bool
    forall a b. Maybe a -> b -> (a -> b) -> b
    caseMaybe (Term -> Maybe MetaId
    forall a. IsMeta a => a -> Maybe MetaId
    isMeta Term
    u) (Modality -> Term -> m Bool
    forall a (m :: * -> *).
    (UsableModality a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
     MonadAddContext m, MonadDebug m, MonadReduce m,
     MonadError Blocker m) =>
    Modality -> a -> m Bool
    usableMod Modality
    mod Term
    u) ((MetaId -> m Bool) -> m Bool) -> (MetaId -> m Bool) -> m Bool
    forall a b. (a -> b) -> a -> b
    $ \ MetaId
    m -> Blocker -> m Bool
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError (MetaId -> Blocker
    UnblockOnMeta MetaId
    m)
        DontCare Term
    v -> Modality -> Term -> m Bool
    forall a (m :: * -> *).
    (UsableModality a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
     MonadAddContext m, MonadDebug m, MonadReduce m,
     MonadError Blocker m) =>
    Modality -> a -> m Bool
    usableMod Modality
    mod Term
    v
        Dummy{}  -> Bool -> m Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    True

    usableModAbs :: (Subst a, MonadAddContext m, UsableModality a,
                           ReadTCState m, HasConstInfo m, MonadReduce m, MonadError Blocker m) =>
                          ArgInfo -> Modality -> Abs a -> m Bool
    usableModAbs :: forall a (m :: * -> *).
    (Subst a, MonadAddContext m, UsableModality a, ReadTCState m,
     HasConstInfo m, MonadReduce m, MonadError Blocker m) =>
    ArgInfo -> Modality -> Abs a -> m Bool
    usableModAbs ArgInfo
    info Modality
    mod Abs a
    abs = Dom Type -> Abs a -> (a -> m Bool) -> m Bool
    forall a (m :: * -> *) b.
    (Subst a, MonadAddContext m) =>
    Dom Type -> Abs a -> (a -> m b) -> m b
    underAbstraction (ArgInfo -> Dom Type -> Dom Type
    forall a. LensArgInfo a => ArgInfo -> a -> a
    setArgInfo ArgInfo
    info (Dom Type -> Dom Type) -> Dom Type -> Dom Type
    forall a b. (a -> b) -> a -> b
    $ Dom Type
    HasCallStack => Dom Type
    __DUMMY_DOM__) Abs a
    abs ((a -> m Bool) -> m Bool) -> (a -> m Bool) -> m Bool
    forall a b. (a -> b) -> a -> b
    $ \ a
    u -> Modality -> a -> m Bool
    forall a (m :: * -> *).
    (UsableModality a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
     MonadAddContext m, MonadDebug m, MonadReduce m,
     MonadError Blocker m) =>
    Modality -> a -> m Bool
    usableMod Modality
    mod a
    u

    instance UsableRelevance a => UsableModality (Type' a) where
      usableMod :: forall (m :: * -> *).
    (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m,
     MonadDebug m, MonadReduce m, MonadError Blocker m) =>
    Modality -> Type' a -> m Bool
    usableMod Modality
    mod (El Sort
    _ a
    t) = Relevance -> a -> m Bool
    forall a (m :: * -> *).
    (UsableRelevance a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
     MonadAddContext m, MonadDebug m) =>
    Relevance -> a -> m Bool
    usableRel (Modality -> Relevance
    forall a. LensRelevance a => a -> Relevance
    getRelevance Modality
    mod) a
    t

    instance UsableModality Sort where
      usableMod :: forall (m :: * -> *).
    (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m,
     MonadDebug m, MonadReduce m, MonadError Blocker m) =>
    Modality -> Sort -> m Bool
    usableMod Modality
    mod Sort
    s = Relevance -> Sort -> m Bool
    forall a (m :: * -> *).
    (UsableRelevance a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
     MonadAddContext m, MonadDebug m) =>
    Relevance -> a -> m Bool
    usableRel (Modality -> Relevance
    forall a. LensRelevance a => a -> Relevance
    getRelevance Modality
    mod) Sort
    s
      -- usableMod mod s = case s of
      --   Type l -> usableMod mod l
      --   Prop l -> usableMod mod l
      --   Inf    -> return True
      --   SizeUniv -> return True
      --   PiSort a s -> usableMod mod (a,s)
      --   UnivSort s -> usableMod mod s
      --   MetaS x es -> usableMod mod es
      --   DummyS{} -> return True

    instance UsableModality Level where
      usableMod :: forall (m :: * -> *).
    (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m,
     MonadDebug m, MonadReduce m, MonadError Blocker m) =>
    Modality -> Level -> m Bool
    usableMod Modality
    mod (Max Integer
    _ [PlusLevel' Term]
    ls) = Relevance -> [PlusLevel' Term] -> m Bool
    forall a (m :: * -> *).
    (UsableRelevance a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
     MonadAddContext m, MonadDebug m) =>
    Relevance -> a -> m Bool
    usableRel (Modality -> Relevance
    forall a. LensRelevance a => a -> Relevance
    getRelevance Modality
    mod) [PlusLevel' Term]
    ls

    -- instance UsableModality PlusLevel where
    --   usableMod mod ClosedLevel{} = return True
    --   usableMod mod (Plus _ l)    = usableMod mod l

    instance UsableModality a => UsableModality [a] where
      usableMod :: forall (m :: * -> *).
    (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m,
     MonadDebug m, MonadReduce m, MonadError Blocker m) =>
    Modality -> [a] -> m Bool
    usableMod Modality
    mod = [m Bool] -> m Bool
    forall (f :: * -> *) (m :: * -> *).
    (Foldable f, Monad m) =>
    f (m Bool) -> m Bool
    andM ([m Bool] -> m Bool) -> ([a] -> [m Bool]) -> [a] -> m Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (a -> m Bool) -> [a] -> [m Bool]
    forall a b. (a -> b) -> [a] -> [b]
    map (Modality -> a -> m Bool
    forall a (m :: * -> *).
    (UsableModality a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
     MonadAddContext m, MonadDebug m, MonadReduce m,
     MonadError Blocker m) =>
    Modality -> a -> m Bool
    usableMod Modality
    mod)

    instance (UsableModality a, UsableModality b) => UsableModality (a,b) where
      usableMod :: forall (m :: * -> *).
    (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m,
     MonadDebug m, MonadReduce m, MonadError Blocker m) =>
    Modality -> (a, b) -> m Bool
    usableMod Modality
    mod (a
    a,b
    b) = Modality -> a -> m Bool
    forall a (m :: * -> *).
    (UsableModality a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
     MonadAddContext m, MonadDebug m, MonadReduce m,
     MonadError Blocker m) =>
    Modality -> a -> m Bool
    usableMod Modality
    mod a
    a m Bool -> m Bool -> m Bool
    forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
    `and2M` Modality -> b -> m Bool
    forall a (m :: * -> *).
    (UsableModality a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
     MonadAddContext m, MonadDebug m, MonadReduce m,
     MonadError Blocker m) =>
    Modality -> a -> m Bool
    usableMod Modality
    mod b
    b

    instance UsableModality a => UsableModality (Elim' a) where
      usableMod :: forall (m :: * -> *).
    (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m,
     MonadDebug m, MonadReduce m, MonadError Blocker m) =>
    Modality -> Elim' a -> m Bool
    usableMod Modality
    mod (Apply Arg a
    a) = Modality -> Arg a -> m Bool
    forall a (m :: * -> *).
    (UsableModality a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
     MonadAddContext m, MonadDebug m, MonadReduce m,
     MonadError Blocker m) =>
    Modality -> a -> m Bool
    usableMod Modality
    mod Arg a
    a
      usableMod Modality
    mod (Proj ProjOrigin
    _ QName
    p) = do
        Modality
    pmod <- QName -> m Modality
    forall (m :: * -> *). HasConstInfo m => QName -> m Modality
    modalityOfConst QName
    p
        Bool -> m Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Bool -> m Bool) -> Bool -> m Bool
    forall a b. (a -> b) -> a -> b
    $ Modality
    pmod Modality -> Modality -> Bool
    `moreUsableModality` Modality
    mod
      usableMod Modality
    mod (IApply a
    x a
    y a
    v) = [a] -> (a -> m Bool) -> m Bool
    forall (f :: * -> *) (m :: * -> *) a.
    (Functor f, Foldable f, Monad m) =>
    f a -> (a -> m Bool) -> m Bool
    allM [a
    x,a
    y,a
    v] ((a -> m Bool) -> m Bool) -> (a -> m Bool) -> m Bool
    forall a b. (a -> b) -> a -> b
    $ Modality -> a -> m Bool
    forall a (m :: * -> *).
    (UsableModality a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
     MonadAddContext m, MonadDebug m, MonadReduce m,
     MonadError Blocker m) =>
    Modality -> a -> m Bool
    usableMod Modality
    mod

    instance UsableModality a => UsableModality (Arg a) where
      usableMod :: forall (m :: * -> *).
    (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m,
     MonadDebug m, MonadReduce m, MonadError Blocker m) =>
    Modality -> Arg a -> m Bool
    usableMod Modality
    mod (Arg ArgInfo
    info a
    u) =
        let mod' :: Modality
    mod' = ArgInfo -> Modality
    forall a. LensModality a => a -> Modality
    getModality ArgInfo
    info
        in  Modality -> a -> m Bool
    forall a (m :: * -> *).
    (UsableModality a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
     MonadAddContext m, MonadDebug m, MonadReduce m,
     MonadError Blocker m) =>
    Modality -> a -> m Bool
    usableMod (Modality
    mod Modality -> Modality -> Modality
    `composeModality` Modality
    mod') a
    u

    instance UsableModality a => UsableModality (Dom a) where
      usableMod :: forall (m :: * -> *).
    (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m,
     MonadDebug m, MonadReduce m, MonadError Blocker m) =>
    Modality -> Dom a -> m Bool
    usableMod Modality
    mod Dom{unDom :: forall t e. Dom' t e -> e
    unDom = a
    u} = Modality -> a -> m Bool
    forall a (m :: * -> *).
    (UsableModality a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
     MonadAddContext m, MonadDebug m, MonadReduce m,
     MonadError Blocker m) =>
    Modality -> a -> m Bool
    usableMod Modality
    mod a
    u

    usableAtModality :: MonadConstraint TCM => Modality -> Term -> TCM ()
    usableAtModality :: MonadConstraint (TCMT IO) => Modality -> Term -> TCM ()
    usableAtModality Modality
    mod Term
    t = Constraint -> TCM () -> TCM ()
    forall (m :: * -> *).
    MonadConstraint m =>
    Constraint -> m () -> m ()
    catchConstraint (Modality -> Term -> Constraint
    UsableAtModality Modality
    mod Term
    t) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
      Either Blocker Bool
    res <- ExceptT Blocker (TCMT IO) Bool -> TCMT IO (Either Blocker Bool)
    forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
    runExceptT (ExceptT Blocker (TCMT IO) Bool -> TCMT IO (Either Blocker Bool))
    -> ExceptT Blocker (TCMT IO) Bool -> TCMT IO (Either Blocker Bool)
    forall a b. (a -> b) -> a -> b
    $ Modality -> Term -> ExceptT Blocker (TCMT IO) Bool
    forall a (m :: * -> *).
    (UsableModality a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
     MonadAddContext m, MonadDebug m, MonadReduce m,
     MonadError Blocker m) =>
    Modality -> a -> m Bool
    usableMod Modality
    mod Term
    t
      case Either Blocker Bool
    res of
        Right Bool
    b -> do
          Bool -> TCM () -> TCM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless Bool
    b (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
            TypeError -> TCM ()
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> TCM ()) -> (Doc -> TypeError) -> Doc -> TCM ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Doc -> TypeError
    GenericDocError (Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< (Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Term
    t TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> TCMT IO Doc
    "is not usable at the required modality" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Modality -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Modality
    mod)
        Left Blocker
    blocker -> Blocker -> TCM ()
    forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
    patternViolation Blocker
    blocker

    -- * Propositions

    -- | Is a type a proposition?  (Needs reduction.)

    isPropM
      :: (LensSort a, PrettyTCM a, PureTCM m, MonadBlock m)
      => a -> m Bool
    isPropM :: forall a (m :: * -> *).
    (LensSort a, PrettyTCM a, PureTCM m, MonadBlock m) =>
    a -> m Bool
    isPropM a
    a = do
      VerboseKey -> VerboseLevel -> TCMT IO Doc -> m Bool -> m Bool
    forall (m :: * -> *) a.
    MonadDebug m =>
    VerboseKey -> VerboseLevel -> TCMT IO Doc -> m a -> m a
    traceSDoc VerboseKey
    "tc.prop" VerboseLevel
    80 (TCMT IO Doc
    "Is " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> a -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM a
    a TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> TCMT IO Doc
    "of sort" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Sort -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM (a -> Sort
    forall a. LensSort a => a -> Sort
    getSort a
    a) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> TCMT IO Doc
    "in Prop?") (m Bool -> m Bool) -> m Bool -> m Bool
    forall a b. (a -> b) -> a -> b
    $ do
      Sort -> m Sort
    forall (m :: * -> *) t.
    (MonadReduce m, MonadBlock m, IsMeta t, Reduce t) =>
    t -> m t
    abortIfBlocked (a -> Sort
    forall a. LensSort a => a -> Sort
    getSort a
    a) m Sort -> (Sort -> Bool) -> m Bool
    forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
    <&> \case
        Prop{} -> Bool
    True
        Sort
    _      -> Bool
    False

    isIrrelevantOrPropM
      :: (LensRelevance a, LensSort a, PrettyTCM a, PureTCM m, MonadBlock m)
      => a -> m Bool
    isIrrelevantOrPropM :: forall a (m :: * -> *).
    (LensRelevance a, LensSort a, PrettyTCM a, PureTCM m,
     MonadBlock m) =>
    a -> m Bool
    isIrrelevantOrPropM a
    x = Bool -> m Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return (a -> Bool
    forall a. LensRelevance a => a -> Bool
    isIrrelevant a
    x) m Bool -> m Bool -> m Bool
    forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
    `or2M` a -> m Bool
    forall a (m :: * -> *).
    (LensSort a, PrettyTCM a, PureTCM m, MonadBlock m) =>
    a -> m Bool
    isPropM a
    x

    -- * Fibrant types

    -- | Is a type fibrant (i.e. Type, Prop)?

    isFibrant
      :: (LensSort a, PureTCM m, MonadBlock m)
      => a -> m Bool
    isFibrant :: forall a (m :: * -> *).
    (LensSort a, PureTCM m, MonadBlock m) =>
    a -> m Bool
    isFibrant a
    a = Sort -> m Sort
    forall (m :: * -> *) t.
    (MonadReduce m, MonadBlock m, IsMeta t, Reduce t) =>
    t -> m t
    abortIfBlocked (a -> Sort
    forall a. LensSort a => a -> Sort
    getSort a
    a) m Sort -> (Sort -> Bool) -> m Bool
    forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
    <&> \case
      Type{}     -> Bool
    True
      Prop{}     -> Bool
    True
      Inf IsFibrant
    f Integer
    _    -> IsFibrant
    f IsFibrant -> IsFibrant -> Bool
    forall a. Eq a => a -> a -> Bool
    == IsFibrant
    IsFibrant
      SSet{}     -> Bool
    False
      SizeUniv{} -> Bool
    False
      LockUniv{} -> Bool
    False
      PiSort{}   -> Bool
    False
      FunSort{}  -> Bool
    False
      UnivSort{} -> Bool
    False
      MetaS{}    -> Bool
    False
      DefS{}     -> Bool
    False
      DummyS{}   -> Bool
    False

    -- | Cofibrant types are those that could be the domain of a fibrant
    --   pi type. (Notion by C. Sattler).
    isCoFibrantSort :: (LensSort a, PureTCM m, MonadBlock m) => a -> m Bool
    isCoFibrantSort :: forall a (m :: * -> *).
    (LensSort a, PureTCM m, MonadBlock m) =>
    a -> m Bool
    isCoFibrantSort a
    a = Sort -> m Sort
    forall (m :: * -> *) t.
    (MonadReduce m, MonadBlock m, IsMeta t, Reduce t) =>
    t -> m t
    abortIfBlocked (a -> Sort
    forall a. LensSort a => a -> Sort
    getSort a
    a) m Sort -> (Sort -> Bool) -> m Bool
    forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
    <&> \case
      Type{}     -> Bool
    True
      Prop{}     -> Bool
    True
      Inf IsFibrant
    f Integer
    _    -> IsFibrant
    f IsFibrant -> IsFibrant -> Bool
    forall a. Eq a => a -> a -> Bool
    == IsFibrant
    IsFibrant
      SSet{}     -> Bool
    False
      SizeUniv{} -> Bool
    False
      LockUniv{} -> Bool
    True
      PiSort{}   -> Bool
    False
      FunSort{}  -> Bool
    False
      UnivSort{} -> Bool
    False
      MetaS{}    -> Bool
    False
      DefS{}     -> Bool
    False
      DummyS{}   -> Bool
    False