    {-# OPTIONS_GHC -Wunused-imports #-}

    {-# 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.Monad.Except ( MonadError(..), runExceptT )

    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.TypeChecking.Telescope

    import Agda.Utils.Either (fromRightM)
    import Agda.Utils.Maybe
    import Agda.Utils.Monad

    import Agda.Utils.Impossible

    -- | 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 Int
    i Elims
    vs -> do
          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
    <$> Int -> m (Dom Type)
    forall (m :: * -> *).
    (MonadDebug m, MonadTCEnv m) =>
    Int -> m (Dom Type)
    domOfBV Int
    i
          let ok = Relevance
    irel Relevance -> Relevance -> Bool
    `moreRelevant` Relevance
    rel
          reportSDoc "tc.irr" 50 $
            "Variable" <+> prettyTCM (var i) <+>
            text ("has relevance " ++ show irel ++ ", which is " ++
                  (if ok then "" else "NOT ") ++ "more relevant than " ++ show rel)
          return ok `and2M` usableRel rel vs
        Def QName
    f Elims
    vs -> do
          frel <- QName -> m Relevance
    forall (m :: * -> *). HasConstInfo m => QName -> m Relevance
    relOfConst QName
    f
          return (frel `moreRelevant` rel) `and2M` usableRel rel 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
    forall (m :: * -> *).
    (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m,
     MonadDebug m) =>
    Relevance -> Elims -> m Bool
    usableRel Relevance
    rel Elims
    vs
        Lit Literal
    l    -> Bool -> m Bool
    forall a. a -> m a
    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
    forall (m :: * -> *).
    (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m,
     MonadDebug m) =>
    Relevance -> Abs Term -> 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
    forall (m :: * -> *).
    (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m,
     MonadDebug m) =>
    Relevance -> (Dom Type, Abs Type) -> 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
    forall (m :: * -> *).
    (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m,
     MonadDebug m) =>
    Relevance -> Sort -> m Bool
    usableRel Relevance
    rel Sort
    s
        Level Level
    l  -> Bool -> m Bool
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    True
        MetaV MetaId
    m Elims
    vs -> do
          mrel <- Modality -> Relevance
    forall a. LensRelevance a => a -> Relevance
    getRelevance (Modality -> Relevance) -> m Modality -> m Relevance
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> MetaId -> m Modality
    forall (m :: * -> *). ReadTCState m => MetaId -> m Modality
    lookupMetaModality MetaId
    m
          return (mrel `moreRelevant` rel) `and2M` usableRel rel 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
    forall (m :: * -> *).
    (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m,
     MonadDebug m) =>
    Relevance -> Term -> m Bool
    usableRel Relevance
    rel Term
    v -- TODO: allow irrelevant things to be used in DontCare position?
        Dummy{}  -> Bool -> m Bool
    forall a. a -> m a
    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
    forall (m :: * -> *).
    (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
        Univ Univ
    _ 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
    forall (m :: * -> *).
    (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m,
     MonadDebug m) =>
    Relevance -> Level -> m Bool
    usableRel Relevance
    rel Level
    l
        Inf Univ
    _ Integer
    _ -> Bool -> m Bool
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    True
        Sort
    SizeUniv -> Bool -> m Bool
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    True
        Sort
    LockUniv -> Bool -> m Bool
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    True
        Sort
    LevelUniv -> Bool -> m Bool
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    True
        Sort
    IntervalUniv -> Bool -> m Bool
    forall a. a -> m a
    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
    forall (m :: * -> *).
    (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m,
     MonadDebug m) =>
    Relevance -> (Dom' Term Term, Sort, Abs Sort) -> 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
    forall (m :: * -> *).
    (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m,
     MonadDebug m) =>
    Relevance -> (Sort, Sort) -> 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
    forall (m :: * -> *).
    (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m,
     MonadDebug m) =>
    Relevance -> Sort -> 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
    forall (m :: * -> *).
    (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m,
     MonadDebug m) =>
    Relevance -> Elims -> 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
    forall (m :: * -> *).
    (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m,
     MonadDebug m) =>
    Relevance -> Term -> 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 a. a -> m a
    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
    forall (m :: * -> *).
    (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m,
     MonadDebug m) =>
    Relevance -> [PlusLevel' Term] -> 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
    forall (m :: * -> *).
    (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m,
     MonadDebug m) =>
    Relevance -> Term -> 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
    forall (m :: * -> *).
    (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
    forall (m :: * -> *).
    (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
    forall (m :: * -> *).
    (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m,
     MonadDebug m) =>
    Relevance -> b -> 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
    forall (m :: * -> *).
    (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
    forall (m :: * -> *).
    (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m,
     MonadDebug m) =>
    Relevance -> b -> 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
    forall (m :: * -> *).
    (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m,
     MonadDebug m) =>
    Relevance -> c -> 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
    forall (m :: * -> *).
    (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m,
     MonadDebug m) =>
    Relevance -> Arg a -> m Bool
    usableRel Relevance
    rel Arg a
    a
      usableRel Relevance
    rel (Proj ProjOrigin
    _ QName
    p) = do
        prel <- QName -> m Relevance
    forall (m :: * -> *). HasConstInfo m => QName -> m Relevance
    relOfConst QName
    p
        return $ prel `moreRelevant` rel
      usableRel Relevance
    rel (IApply a
    x a
    y a
    v) = Relevance -> a -> m Bool
    forall a (m :: * -> *).
    (UsableRelevance a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
     MonadAddContext m, MonadDebug m) =>
    Relevance -> a -> m Bool
    forall (m :: * -> *).
    (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m,
     MonadDebug m) =>
    Relevance -> a -> m Bool
    usableRel Relevance
    rel a
    v

    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
    forall (m :: * -> *).
    (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
    forall (m :: * -> *).
    (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
    forall (m :: * -> *).
    (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 Int
    i Elims
    vs -> do
          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
    <$> Int -> m (Dom Type)
    forall (m :: * -> *).
    (MonadDebug m, MonadTCEnv m) =>
    Int -> m (Dom Type)
    domOfBV Int
    i
          let ok = Modality
    imod Modality -> Modality -> Bool
    `moreUsableModality` Modality
    mod
          reportSDoc "tc.irr" 50 $
            "Variable" <+> prettyTCM (var i) <+>
            text ("has modality " ++ show imod ++ ", which is a " ++
                  (if ok then "" else "NOT ") ++ "more usable modality than " ++ show mod)
          return ok `and2M` usableMod mod vs
        Def QName
    f Elims
    vs -> do
          fmod <- QName -> m Modality
    forall (m :: * -> *). HasConstInfo m => QName -> m Modality
    modalityOfConst QName
    f
          -- Pure modalities don't matter here, only positional ones, hence remove
          -- them from the equation.
          let ok = PolarityModality -> Modality -> Modality
    forall a. LensModalPolarity a => PolarityModality -> a -> a
    setModalPolarity (ModalPolarity -> PolarityModality
    withStandardLock ModalPolarity
    MixedPolarity) (Cohesion -> Modality -> Modality
    forall a. LensCohesion a => Cohesion -> a -> a
    setCohesion Cohesion
    Flat Modality
    fmod) Modality -> Modality -> Bool
    `moreUsableModality` Modality
    mod
          reportSDoc "tc.irr" 50 $
            "Definition" <+> prettyTCM (Def f []) <+>
            text ("has modality " ++ show fmod ++ ", which is a " ++
                  (if ok then "" else "NOT ") ++ "more usable modality than " ++ show mod)
          return ok `and2M` usableMod mod vs
        Con ConHead
    c ConInfo
    o Elims
    vs -> do
          cmod <- QName -> m Modality
    forall (m :: * -> *). HasConstInfo m => QName -> m Modality
    modalityOfConst (ConHead -> QName
    conName ConHead
    c)
          let ok = Modality
    cmod Modality -> Modality -> Bool
    `moreUsableModality` Modality
    mod
          reportSDoc "tc.irr" 50 $
            "The constructor" <+> prettyTCM (Con c o []) <+>
            text ("has the modality " ++ show cmod ++ ", which is " ++
                  (if ok then "" else "NOT ") ++
                  "more usable than the modality " ++ show mod ++ ".")
          return ok `and2M` usableMod mod vs
        Lit Literal
    l    -> Bool -> m Bool
    forall a. a -> m a
    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
    forall (m :: * -> *).
    (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m,
     MonadDebug m, MonadReduce m, MonadError Blocker m) =>
    Modality -> Term -> 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 -> Modality) -> Modality -> Modality
    forall a b. (a -> b) -> a -> b
    $
                     (PolarityModality -> PolarityModality) -> Modality -> Modality
    forall a.
    LensModalPolarity a =>
    (PolarityModality -> PolarityModality) -> a -> a
    mapModalPolarity (PolarityModality -> PolarityModality -> PolarityModality
    composePolarity (PolarityModality -> PolarityModality -> PolarityModality)
    -> PolarityModality -> PolarityModality -> PolarityModality
    forall a b. (a -> b) -> a -> b
    $ Dom Type -> PolarityModality
    forall a. LensModalPolarity a => a -> PolarityModality
    getModalPolarity 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
    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
        Level Level
    l  -> Bool -> m Bool
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    True
        MetaV MetaId
    m Elims
    vs -> do
          mmod <- MetaId -> m Modality
    forall (m :: * -> *). ReadTCState m => MetaId -> m Modality
    lookupMetaModality MetaId
    m
          let ok = Modality
    mmod Modality -> Modality -> Bool
    `moreUsableModality` Modality
    mod
          reportSDoc "tc.irr" 50 $
            "Metavariable" <+> prettyTCM (MetaV m []) <+>
            text ("has modality " ++ show mmod ++ ", which is a " ++
                  (if ok then "" else "NOT ") ++ "more usable modality than " ++ show mod)
          (return ok `and2M` usableMod mod vs) `or2M` do
            u <- instantiate u
            caseMaybe (isMeta u) (usableMod mod u) $ \ MetaId
    m -> Blocker -> m Bool
    forall a. Blocker -> m a
    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
    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
    v
        Dummy{}  -> Bool -> m Bool
    forall a. a -> m a
    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
    forall (m :: * -> *).
    (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
    forall (m :: * -> *).
    (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
    forall (m :: * -> *).
    (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m,
     MonadDebug m) =>
    Relevance -> Sort -> m Bool
    usableRel (Modality -> Relevance
    forall a. LensRelevance a => a -> Relevance
    getRelevance Modality
    mod) Sort
    s

    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
    forall (m :: * -> *).
    (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m,
     MonadDebug m) =>
    Relevance -> [PlusLevel' Term] -> 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
    forall (m :: * -> *).
    (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
    forall (m :: * -> *).
    (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
    forall (m :: * -> *).
    (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m,
     MonadDebug m, MonadReduce m, MonadError Blocker m) =>
    Modality -> b -> 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
    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 a
    a
      usableMod Modality
    mod (Proj ProjOrigin
    _ QName
    p) = do
        pmod <- QName -> m Modality
    forall (m :: * -> *). HasConstInfo m => QName -> m Modality
    modalityOfConst QName
    p
        return $ pmod `moreUsableModality` mod
      usableMod Modality
    mod (IApply a
    x a
    y a
    v) = 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
    forall (m :: * -> *).
    (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m,
     MonadDebug m, MonadReduce m, MonadError Blocker m) =>
    Modality -> a -> m Bool
    usableMod Modality
    mod a
    v

    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
    forall (m :: * -> *).
    (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
    forall (m :: * -> *).
    (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
      -- Note: This weird-looking constraint is to trick GHC into accepting
      -- that an instance of MonadConstraint TCM will exist, even if we
      -- can't import the module in which it is defined.
      => Maybe Sort -> WhyCheckModality -> Modality -> Term -> TCM ()
    usableAtModality' :: MonadConstraint (TCMT IO) =>
    Maybe Sort -> WhyCheckModality -> Modality -> Term -> TCM ()
    usableAtModality' Maybe Sort
    ms WhyCheckModality
    why Modality
    mod Term
    t =
      Constraint -> TCM () -> TCM ()
    forall (m :: * -> *).
    MonadConstraint m =>
    Constraint -> m () -> m ()
    catchConstraint (WhyCheckModality -> Maybe Sort -> Modality -> Term -> Constraint
    UsableAtModality WhyCheckModality
    why Maybe Sort
    ms Modality
    mod Term
    t) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
        TCMT IO Bool -> TCM () -> TCM ()
    forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
    whenM (TCMT IO Bool
    -> (Sort -> TCMT IO Bool) -> Maybe Sort -> TCMT IO Bool
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe (Bool -> TCMT IO Bool
    forall a. a -> TCMT IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Bool
    True) Sort -> TCMT IO Bool
    forall a (m :: * -> *).
    (LensSort a, PureTCM m, MonadBlock m) =>
    a -> m Bool
    isFibrant Maybe Sort
    ms) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
          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
    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
    t
          case res of
            Right Bool
    b -> Bool -> TCM () -> TCM ()
    forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
    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 ()) -> TypeError -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ WhyCheckModality -> Modality -> Term -> TypeError
    UnusableAtModality WhyCheckModality
    why Modality
    mod Term
    t
            Left Blocker
    blocker -> Blocker -> TCM ()
    forall a. Blocker -> TCMT IO a
    forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
    patternViolation Blocker
    blocker

    usableAtModality :: MonadConstraint TCM => WhyCheckModality -> Modality -> Term -> TCM ()
    usableAtModality :: MonadConstraint (TCMT IO) =>
    WhyCheckModality -> Modality -> Term -> TCM ()
    usableAtModality = Maybe Sort -> WhyCheckModality -> Modality -> Term -> TCM ()
    MonadConstraint (TCMT IO) =>
    Maybe Sort -> WhyCheckModality -> Modality -> Term -> TCM ()
    usableAtModality' Maybe Sort
    forall a. Maybe a
    Nothing

    -- * Propositions

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

    {-# SPECIALIZE isPropM :: Dom Type -> TCM Bool #-}
    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
      let s :: Sort
    s = a -> Sort
    forall a. LensSort a => a -> Sort
    getSort a
    a
      [Char] -> Int -> TCMT IO Doc -> m Bool -> m Bool
    forall (m :: * -> *) a.
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m a -> m a
    traceSDoc [Char]
    "tc.prop" Int
    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
    forall (m :: * -> *). 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
    forall (m :: * -> *). MonadPretty m => Sort -> m Doc
    prettyTCM Sort
    s TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> TCMT IO Doc
    "in Prop?") do
      Sort -> Bool
    forall t. Sort' t -> Bool
    isProp (Sort -> Bool) -> m Sort -> m Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Sort -> m Sort
    forall (m :: * -> *) t.
    (MonadReduce m, MonadBlock m, IsMeta t, Reduce t) =>
    t -> m t
    abortIfBlocked Sort
    s

    {-# SPECIALIZE isIrrelevantOrPropM :: Dom Type -> TCM Bool #-}
    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 a. a -> m a
    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

    allIrrelevantOrPropTel
      :: (PureTCM m, MonadBlock m)
      => Telescope -> m Bool
    allIrrelevantOrPropTel :: forall (m :: * -> *).
    (PureTCM m, MonadBlock m) =>
    Telescope -> m Bool
    allIrrelevantOrPropTel =
      (Dom ([Char], Type) -> m Bool -> m Bool)
    -> m Bool -> Telescope -> m Bool
    forall (m :: * -> *) b.
    MonadAddContext m =>
    (Dom ([Char], Type) -> m b -> m b) -> m b -> Telescope -> m b
    foldrTelescopeM (m Bool -> m Bool -> m Bool
    forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
    and2M (m Bool -> m Bool -> m Bool)
    -> (Dom ([Char], Type) -> m Bool)
    -> Dom ([Char], Type)
    -> m Bool
    -> m Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Dom Type -> m Bool
    forall a (m :: * -> *).
    (LensRelevance a, LensSort a, PrettyTCM a, PureTCM m,
     MonadBlock m) =>
    a -> m Bool
    isIrrelevantOrPropM (Dom Type -> m Bool)
    -> (Dom ([Char], Type) -> Dom Type) -> Dom ([Char], Type) -> m Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (([Char], Type) -> Type) -> Dom ([Char], Type) -> Dom Type
    forall a b. (a -> b) -> Dom' Term a -> Dom' Term b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ([Char], Type) -> Type
    forall a b. (a, b) -> b
    snd) (Bool -> m Bool
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    True)

    -- * 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 = (Blocker -> m Bool) -> m (Either Blocker Bool) -> m Bool
    forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> m (Either a b) -> m b
    fromRightM Blocker -> m Bool
    forall a. Blocker -> m a
    forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
    patternViolation (m (Either Blocker Bool) -> m Bool)
    -> (a -> m (Either Blocker Bool)) -> a -> m Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . a -> m (Either Blocker Bool)
    forall a (m :: * -> *).
    (LensSort a, PureTCM m) =>
    a -> m (Either Blocker Bool)
    isFibrant'

    isFibrant' :: (LensSort a, PureTCM m) => a -> m (Either Blocker Bool)
    isFibrant' :: forall a (m :: * -> *).
    (LensSort a, PureTCM m) =>
    a -> m (Either Blocker Bool)
    isFibrant' a
    s =
      Sort
    -> (Blocker -> Sort -> m (Either Blocker Bool))
    -> (NotBlocked -> Sort -> m (Either Blocker Bool))
    -> m (Either Blocker Bool)
    forall t (m :: * -> *) a.
    (Reduce t, IsMeta t, MonadReduce m) =>
    t -> (Blocker -> t -> m a) -> (NotBlocked -> t -> m a) -> m a
    ifBlocked (a -> Sort
    forall a. LensSort a => a -> Sort
    getSort a
    s) (\ Blocker
    blocker Sort
    _ -> Either Blocker Bool -> m (Either Blocker Bool)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Either Blocker Bool -> m (Either Blocker Bool))
    -> Either Blocker Bool -> m (Either Blocker Bool)
    forall a b. (a -> b) -> a -> b
    $ Blocker -> Either Blocker Bool
    forall a b. a -> Either a b
    Left Blocker
    blocker) \ NotBlocked
    _ ->
        Either Blocker Bool -> m (Either Blocker Bool)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Either Blocker Bool -> m (Either Blocker Bool))
    -> (Sort -> Either Blocker Bool) -> Sort -> m (Either Blocker Bool)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Bool -> Either Blocker Bool
    forall a b. b -> Either a b
    Right (Bool -> Either Blocker Bool)
    -> (Sort -> Bool) -> Sort -> Either Blocker Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . \case
          Univ Univ
    u Level
    _       -> Univ -> IsFibrant
    univFibrancy Univ
    u IsFibrant -> IsFibrant -> Bool
    forall a. Eq a => a -> a -> Bool
    == IsFibrant
    IsFibrant
          Inf Univ
    u Integer
    _        -> Univ -> IsFibrant
    univFibrancy Univ
    u IsFibrant -> IsFibrant -> Bool
    forall a. Eq a => a -> a -> Bool
    == IsFibrant
    IsFibrant
          SizeUniv{}     -> Bool
    False
          LockUniv{}     -> Bool
    False
          LevelUniv{}    -> Bool
    False
          IntervalUniv{} -> Bool
    False
          PiSort{}       -> Bool
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          FunSort{}      -> Bool
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          UnivSort{}     -> Bool
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          MetaS{}        -> Bool
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          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) => a -> m (Either Blocker Bool)
    isCoFibrantSort :: forall a (m :: * -> *).
    (LensSort a, PureTCM m) =>
    a -> m (Either Blocker Bool)
    isCoFibrantSort a
    s =
      Sort
    -> (Blocker -> Sort -> m (Either Blocker Bool))
    -> (NotBlocked -> Sort -> m (Either Blocker Bool))
    -> m (Either Blocker Bool)
    forall t (m :: * -> *) a.
    (Reduce t, IsMeta t, MonadReduce m) =>
    t -> (Blocker -> t -> m a) -> (NotBlocked -> t -> m a) -> m a
    ifBlocked (a -> Sort
    forall a. LensSort a => a -> Sort
    getSort a
    s) (\ Blocker
    blocker Sort
    _ -> Either Blocker Bool -> m (Either Blocker Bool)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Either Blocker Bool -> m (Either Blocker Bool))
    -> Either Blocker Bool -> m (Either Blocker Bool)
    forall a b. (a -> b) -> a -> b
    $ Blocker -> Either Blocker Bool
    forall a b. a -> Either a b
    Left Blocker
    blocker) \ NotBlocked
    _ ->
        Either Blocker Bool -> m (Either Blocker Bool)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Either Blocker Bool -> m (Either Blocker Bool))
    -> (Sort -> Either Blocker Bool) -> Sort -> m (Either Blocker Bool)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Bool -> Either Blocker Bool
    forall a b. b -> Either a b
    Right (Bool -> Either Blocker Bool)
    -> (Sort -> Bool) -> Sort -> Either Blocker Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . \case
          Univ Univ
    u Level
    _       -> Univ -> IsFibrant
    univFibrancy Univ
    u IsFibrant -> IsFibrant -> Bool
    forall a. Eq a => a -> a -> Bool
    == IsFibrant
    IsFibrant
          Inf Univ
    u Integer
    _        -> Univ -> IsFibrant
    univFibrancy Univ
    u IsFibrant -> IsFibrant -> Bool
    forall a. Eq a => a -> a -> Bool
    == IsFibrant
    IsFibrant
          SizeUniv{}     -> Bool
    False
          LockUniv{}     -> Bool
    True
          LevelUniv{}    -> Bool
    False
          IntervalUniv{} -> Bool
    True
          PiSort{}       -> Bool
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          FunSort{}      -> Bool
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          UnivSort{}     -> Bool
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          MetaS{}        -> Bool
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          DefS{}         -> Bool
    False
          DummyS{}       -> Bool
    False