{-# 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.Syntax.Concrete.Pretty

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
import Agda.Utils.WithDefault
import qualified Agda.Utils.Null as Null
import Agda.Utils.WithDefault (collapseDefault)

-- | 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 a. 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 a. (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 a. (TCEnv -> TCEnv) -> tcm a -> tcm a
forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC
  ((TCEnv -> TCEnv) -> tcm a -> tcm a)
-> (TCEnv -> TCEnv) -> tcm a -> tcm a
forall a b. (a -> b) -> a -> b
$ Lens' [ContextEntry] TCEnv -> LensMap [ContextEntry] TCEnv
forall i o. Lens' i o -> LensMap i o
over ([ContextEntry] -> f [ContextEntry]) -> TCEnv -> f TCEnv
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 (Map Name (Open (Term, Dom Type))
 -> f (Map Name (Open (Term, Dom Type))))
-> TCEnv -> f TCEnv
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 a b. (a -> b) -> Open a -> Open b
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 b c d. (b -> c) -> (d, b) -> (d, c)
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 a. (TCEnv -> TCEnv) -> tcm a -> tcm a
forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC ((TCEnv -> TCEnv) -> tcm a -> tcm a)
-> (Relevance -> TCEnv -> TCEnv) -> Relevance -> tcm a -> tcm a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Lens' Relevance TCEnv -> LensMap Relevance TCEnv
forall i o. Lens' i o -> LensMap i o
over (Relevance -> f Relevance) -> TCEnv -> f TCEnv
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 a. (TCEnv -> TCEnv) -> tcm a -> tcm a
forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC ((TCEnv -> TCEnv) -> tcm a -> tcm a)
-> (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 (Quantity -> f Quantity) -> TCEnv -> f TCEnv
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 a. (TCEnv -> TCEnv) -> tcm a -> tcm a
forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC
  ((TCEnv -> TCEnv) -> tcm a -> tcm a)
-> (TCEnv -> TCEnv) -> tcm a -> tcm a
forall a b. (a -> b) -> a -> b
$ Lens' [ContextEntry] TCEnv -> LensMap [ContextEntry] TCEnv
forall i o. Lens' i o -> LensMap i o
over ([ContextEntry] -> f [ContextEntry]) -> TCEnv -> f TCEnv
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 (Map Name (Open (Term, Dom Type))
 -> f (Map Name (Open (Term, Dom Type))))
-> TCEnv -> f TCEnv
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 a b. (a -> b) -> Open a -> Open b
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 b c d. (b -> c) -> (d, b) -> (d, c)
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 a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Cohesion -> Bool
forall a. LensCohesion a => a -> Bool
usableCohesion Cohesion
c) m Bool -> m Bool -> m Bool
forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`and2M` (Bool -> m Bool
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Cohesion
c Cohesion -> Cohesion -> Bool
forall a. Eq a => a -> a -> Bool
/= Cohesion
Flat) m Bool -> m Bool -> m Bool
forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`or2M` do WithDefault 'False -> Bool
forall (b :: Bool). KnownBool b => WithDefault b -> Bool
collapseDefault (WithDefault 'False -> Bool)
-> (PragmaOptions -> WithDefault 'False) -> PragmaOptions -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PragmaOptions -> WithDefault 'False
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 a. (TCEnv -> TCEnv) -> tcm a -> tcm a
forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC
  ((TCEnv -> TCEnv) -> tcm a -> tcm a)
-> (TCEnv -> TCEnv) -> tcm a -> tcm a
forall a b. (a -> b) -> a -> b
$ Lens' [ContextEntry] TCEnv -> LensMap [ContextEntry] TCEnv
forall i o. Lens' i o -> LensMap i o
over ([ContextEntry] -> f [ContextEntry]) -> TCEnv -> f TCEnv
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 (Map Name (Open (Term, Dom Type))
 -> f (Map Name (Open (Term, Dom Type))))
-> TCEnv -> f TCEnv
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 a b. (a -> b) -> Open a -> Open b
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 b c d. (b -> c) -> (d, b) -> (d, c)
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 a. (TCEnv -> TCEnv) -> tcm a -> tcm a
forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC ((TCEnv -> TCEnv) -> tcm a -> tcm a)
-> (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 (Modality -> f Modality) -> TCEnv -> f TCEnv
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
forall (m :: * -> *). MonadPretty m => Term -> 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 a. a -> m a
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
forall (m :: * -> *).
(ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m,
 MonadDebug m) =>
Relevance -> Elims -> 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 a. a -> m a
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
forall (m :: * -> *).
(ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m,
 MonadDebug m) =>
Relevance -> Elims -> 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
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
      Relevance
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
      Bool -> m Bool
forall a. a -> m a
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
forall (m :: * -> *).
(ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m,
 MonadDebug m) =>
Relevance -> Elims -> 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
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
    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
forall (m :: * -> *).
(ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m,
 MonadDebug m) =>
Relevance -> Level -> 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
forall (m :: * -> *).
(ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m,
 MonadDebug m) =>
Relevance -> Level -> m Bool
usableRel Relevance
rel Level
l
    Inf IsFibrant
f Integer
n -> Bool -> m Bool
forall a. a -> m a
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
forall (m :: * -> *).
(ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m,
 MonadDebug m) =>
Relevance -> Level -> m Bool
usableRel Relevance
rel Level
l
    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
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
    Relevance
prel <- QName -> m Relevance
forall (m :: * -> *). HasConstInfo m => QName -> m Relevance
relOfConst QName
p
    Bool -> m Bool
forall a. a -> m a
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) = 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 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
forall (m :: * -> *). MonadPretty m => Term -> 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 a. a -> m a
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
forall (m :: * -> *).
(ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m,
 MonadDebug m, MonadReduce m, MonadError Blocker m) =>
Modality -> Elims -> 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
forall (m :: * -> *). MonadPretty m => Term -> 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 a. a -> m a
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
forall (m :: * -> *).
(ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m,
 MonadDebug m, MonadReduce m, MonadError Blocker m) =>
Modality -> Elims -> m Bool
usableMod Modality
mod Elims
vs
    Con ConHead
c ConInfo
o Elims
vs -> do
      Modality
cmod <- QName -> m Modality
forall (m :: * -> *). HasConstInfo m => QName -> m Modality
modalityOfConst (ConHead -> QName
conName ConHead
c)
      let ok :: Bool
ok = Modality
cmod 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
"The constructor" 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
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM (ConHead -> ConInfo -> Elims -> Term
Con ConHead
c ConInfo
o []) 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 the modality " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ Modality -> VerboseKey
forall a. Show a => a -> VerboseKey
show Modality
cmod 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 usable than the modality " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ Modality -> VerboseKey
forall a. Show a => a -> VerboseKey
show Modality
mod VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ VerboseKey
".")
      Bool -> m Bool
forall a. a -> m a
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
forall (m :: * -> *).
(ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m,
 MonadDebug m, MonadReduce m, MonadError Blocker m) =>
Modality -> Elims -> m Bool
usableMod Modality
mod 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
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
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
      Modality
mmod <- MetaId -> m Modality
forall (m :: * -> *). ReadTCState m => MetaId -> m Modality
lookupMetaModality 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
forall (m :: * -> *). MonadPretty m => Term -> 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 a. a -> m a
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
forall (m :: * -> *).
(ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m,
 MonadDebug m, MonadReduce m, MonadError Blocker m) =>
Modality -> Elims -> 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
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) ((MetaId -> m Bool) -> m Bool) -> (MetaId -> m Bool) -> m Bool
forall a b. (a -> b) -> a -> b
$ \ 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
  -- 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
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
    Modality
pmod <- QName -> m Modality
forall (m :: * -> *). HasConstInfo m => QName -> m Modality
modalityOfConst QName
p
    Bool -> m Bool
forall a. a -> m a
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) = 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
      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
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 Either Blocker Bool
res of
        Right Bool
b -> 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
=<< TCMT IO Doc
formatWhy
        Left Blocker
blocker -> Blocker -> TCM ()
forall a. Blocker -> TCMT IO a
forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation Blocker
blocker
  where
    formatWhy :: TCMT IO Doc
formatWhy = do
      Bool
compatible <- WithDefault 'False -> Bool
forall (b :: Bool). KnownBool b => WithDefault b -> Bool
collapseDefault (WithDefault 'False -> Bool)
-> (PragmaOptions -> WithDefault 'False) -> PragmaOptions -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PragmaOptions -> WithDefault 'False
optCubicalCompatible (PragmaOptions -> Bool) -> TCMT IO PragmaOptions -> TCMT IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO PragmaOptions
forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions
      Bool
cubical <- Maybe Cubical -> Bool
forall a. Maybe a -> Bool
isJust (Maybe Cubical -> Bool)
-> (PragmaOptions -> Maybe Cubical) -> PragmaOptions -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PragmaOptions -> Maybe Cubical
optCubical (PragmaOptions -> Bool) -> TCMT IO PragmaOptions -> TCMT IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO PragmaOptions
forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions
      let
        context :: VerboseKey
context
          | Bool
cubical    = VerboseKey
"in Cubical Agda,"
          | Bool
compatible = VerboseKey
"to maintain compatibility with Cubical Agda,"
          | Bool
otherwise  = VerboseKey
"when --without-K is enabled,"

        explanation :: VerboseKey -> [TCMT IO Doc]
explanation VerboseKey
what
          | Bool
cubical Bool -> Bool -> Bool
|| Bool
compatible =
            [ TCMT IO Doc
""
            , [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ( TCMT IO Doc
"Note:"TCMT IO Doc -> [TCMT IO Doc] -> [TCMT IO Doc]
forall a. a -> [a] -> [a]
:VerboseKey -> [TCMT IO Doc]
forall (m :: * -> *). Applicative m => VerboseKey -> [m Doc]
pwords VerboseKey
context
                  [TCMT IO Doc] -> [TCMT IO Doc] -> [TCMT IO Doc]
forall a. [a] -> [a] -> [a]
++ VerboseKey -> [TCMT IO Doc]
forall (m :: * -> *). Applicative m => VerboseKey -> [m Doc]
pwords VerboseKey
what [TCMT IO Doc] -> [TCMT IO Doc] -> [TCMT IO Doc]
forall a. [a] -> [a] -> [a]
++ VerboseKey -> [TCMT IO Doc]
forall (m :: * -> *). Applicative m => VerboseKey -> [m Doc]
pwords VerboseKey
"must be usable at the modality"
                  [TCMT IO Doc] -> [TCMT IO Doc] -> [TCMT IO Doc]
forall a. [a] -> [a] -> [a]
++ VerboseKey -> [TCMT IO Doc]
forall (m :: * -> *). Applicative m => VerboseKey -> [m Doc]
pwords VerboseKey
"in which the function was defined, since it will be"
                  [TCMT IO Doc] -> [TCMT IO Doc] -> [TCMT IO Doc]
forall a. [a] -> [a] -> [a]
++ VerboseKey -> [TCMT IO Doc]
forall (m :: * -> *). Applicative m => VerboseKey -> [m Doc]
pwords VerboseKey
"used for computing transports"
                  )
            , TCMT IO Doc
""
            ]
          | Bool
otherwise = []

      case WhyCheckModality
why of
        WhyCheckModality
IndexedClause ->
          [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat ([TCMT IO Doc] -> TCMT IO Doc) -> [TCMT IO Doc] -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$
            ( [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ( VerboseKey -> [TCMT IO Doc]
forall (m :: * -> *). Applicative m => VerboseKey -> [m Doc]
pwords VerboseKey
"This clause has target type"
                  [TCMT IO Doc] -> [TCMT IO Doc] -> [TCMT IO Doc]
forall a. [a] -> [a] -> [a]
++ [Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
t]
                  [TCMT IO Doc] -> [TCMT IO Doc] -> [TCMT IO Doc]
forall a. [a] -> [a] -> [a]
++ VerboseKey -> [TCMT IO Doc]
forall (m :: * -> *). Applicative m => VerboseKey -> [m Doc]
pwords VerboseKey
"which is not usable at the required modality"
                  [TCMT IO Doc] -> [TCMT IO Doc] -> [TCMT IO Doc]
forall a. [a] -> [a] -> [a]
++ [Doc -> TCMT IO Doc
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Modality -> Doc
attributesForModality Modality
mod) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall a. Semigroup a => a -> a -> a
<> TCMT IO Doc
"."]
                   )
            TCMT IO Doc -> [TCMT IO Doc] -> [TCMT IO Doc]
forall a. a -> [a] -> [a]
: VerboseKey -> [TCMT IO Doc]
explanation VerboseKey
"the target type")

        -- Arguments sometimes need to be transported too:
        IndexedClauseArg Name
forced Name
the_arg ->
          [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat ([TCMT IO Doc] -> TCMT IO Doc) -> [TCMT IO Doc] -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$
            ( [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep (VerboseKey -> [TCMT IO Doc]
forall (m :: * -> *). Applicative m => VerboseKey -> [m Doc]
pwords VerboseKey
"The argument" [TCMT IO Doc] -> [TCMT IO Doc] -> [TCMT IO Doc]
forall a. [a] -> [a] -> [a]
++ [Name -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Name -> m Doc
prettyTCM Name
the_arg] [TCMT IO Doc] -> [TCMT IO Doc] -> [TCMT IO Doc]
forall a. [a] -> [a] -> [a]
++ VerboseKey -> [TCMT IO Doc]
forall (m :: * -> *). Applicative m => VerboseKey -> [m Doc]
pwords VerboseKey
"has type")
            TCMT IO Doc -> [TCMT IO Doc] -> [TCMT IO Doc]
forall a. a -> [a] -> [a]
: VerboseLevel -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
t)
            TCMT IO Doc -> [TCMT IO Doc] -> [TCMT IO Doc]
forall a. a -> [a] -> [a]
: [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ( VerboseKey -> [TCMT IO Doc]
forall (m :: * -> *). Applicative m => VerboseKey -> [m Doc]
pwords VerboseKey
"which is not usable at the required modality"
                  [TCMT IO Doc] -> [TCMT IO Doc] -> [TCMT IO Doc]
forall a. [a] -> [a] -> [a]
++ [Doc -> TCMT IO Doc
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Modality -> Doc
attributesForModality Modality
mod) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall a. Semigroup a => a -> a -> a
<> TCMT IO Doc
"."] )
            TCMT IO Doc -> [TCMT IO Doc] -> [TCMT IO Doc]
forall a. a -> [a] -> [a]
: VerboseKey -> [TCMT IO Doc]
explanation VerboseKey
"this argument's type")

        -- Note: if a generated clause is modality-incorrect, that's a
        -- bug in the LHS modality check
        WhyCheckModality
GeneratedClause ->
          VerboseKey -> TCMT IO Doc
forall (m :: * -> *) a.
(HasCallStack, MonadDebug m) =>
VerboseKey -> m a
__IMPOSSIBLE_VERBOSE__ (VerboseKey -> TCMT IO Doc)
-> (Doc -> VerboseKey) -> Doc -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> VerboseKey
forall a. Show a => a -> VerboseKey
show (Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
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
forall (m :: * -> *). MonadPretty m => Term -> 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
<+> Doc -> TCMT IO Doc
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Modality -> Doc
attributesForModality Modality
mod)
        WhyCheckModality
_ -> Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> 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
<+> Doc -> TCMT IO Doc
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Modality -> Doc
attributesForModality Modality
mod)


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.)

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
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 (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 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

-- * 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
  IntervalUniv{} -> 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
  IntervalUniv{} -> Bool
True
  PiSort{}   -> Bool
False
  FunSort{}  -> Bool
False
  UnivSort{} -> Bool
False
  MetaS{}    -> Bool
False
  DefS{}     -> Bool
False
  DummyS{}   -> Bool
False