{-# LANGUAGE UndecidableInstances #-}
{-# 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 qualified Data.Map as Map

import Agda.Interaction.Options

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

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

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

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

-- * Operations on 'Dom'.

-- | Prepare parts of a parameter telescope for abstraction in constructors
--   and projections.
hideAndRelParams :: Dom a -> Dom a
hideAndRelParams :: Dom a -> Dom a
hideAndRelParams = Dom a -> Dom a
forall a. LensHiding a => a -> a
hideOrKeepInstance (Dom a -> Dom a) -> (Dom a -> Dom a) -> Dom a -> Dom a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Relevance -> Relevance) -> Dom a -> Dom 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 :: m a -> m a
workOnTypes m a
cont = do
  Bool
allowed <- PragmaOptions -> Bool
optExperimentalIrrelevance (PragmaOptions -> Bool) -> m PragmaOptions -> m Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m PragmaOptions
forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions
  VerboseKey -> VerboseLevel -> VerboseKey -> m a -> m a
forall (m :: * -> *) a.
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m a -> m a
verboseBracket VerboseKey
"tc.irr" VerboseLevel
60 VerboseKey
"workOnTypes" (m a -> m a) -> m a -> m a
forall a b. (a -> b) -> a -> b
$ Bool -> m a -> m a
forall (m :: * -> *) a. MonadTCEnv m => Bool -> m a -> m a
workOnTypes' Bool
allowed m a
cont

-- | Internal workhorse, expects value of --experimental-irrelevance flag
--   as argument.
workOnTypes' :: (MonadTCEnv m) => Bool -> m a -> m a
workOnTypes' :: Bool -> m a -> m a
workOnTypes' Bool
experimental
  = (forall e. Dom e -> Dom e) -> m a -> m a
forall (tcm :: * -> *) a.
MonadTCEnv tcm =>
(forall e. Dom e -> Dom e) -> tcm a -> tcm a
modifyContextInfo ((Relevance -> Relevance) -> Dom e -> Dom e
forall a. LensRelevance a => (Relevance -> Relevance) -> a -> a
mapRelevance Relevance -> Relevance
f)
  (m a -> m a) -> (m a -> m a) -> m a -> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Quantity -> m a -> m a
forall (tcm :: * -> *) q a.
(MonadTCEnv tcm, LensQuantity q) =>
q -> tcm a -> tcm a
applyQuantityToContext Quantity
zeroQuantity
  (m a -> m a) -> (m a -> m a) -> m a -> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. m a -> m a
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
typeLevelReductions
  (m a -> m a) -> (m a -> m a) -> m a -> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TCEnv -> TCEnv) -> m a -> m a
forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC (\ TCEnv
e -> TCEnv
e { envWorkingOnTypes :: Bool
envWorkingOnTypes = Bool
True })
  where
    f :: Relevance -> Relevance
f | Bool
experimental = Relevance -> Relevance
irrToNonStrict
      | Bool
otherwise    = Relevance -> Relevance
forall a. a -> a
id

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

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

-- | Like 'applyRelevanceToContext', but only act on context if
--   @--irrelevant-projections@.
--   See issue #2170.
applyRelevanceToContextFunBody :: (MonadTCM tcm, LensRelevance r) => r -> tcm a -> tcm a
applyRelevanceToContextFunBody :: 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

-- | (Conditionally) wake up erased variables and make them unrestricted.
--   For instance,
--   in an erased function argument otherwise erased variables
--   may be used, so they are awoken before type checking the argument.
--
--   Also allow the use of erased definitions.
applyQuantityToContext :: (MonadTCEnv tcm, LensQuantity q) => q -> tcm a -> tcm a
applyQuantityToContext :: 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
applyQuantityToContextOnly   Quantity
q
               (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
q

-- | (Conditionally) wake up erased variables and make them unrestricted.
--   For instance,
--   in an erased function argument otherwise erased variables
--   may be used, so they are awoken before type checking the argument.
--
--   Precondition: @Quantity /= Quantity1@
applyQuantityToContextOnly :: (MonadTCEnv tcm) => Quantity -> tcm a -> tcm a
applyQuantityToContextOnly :: Quantity -> tcm a -> tcm a
applyQuantityToContextOnly Quantity
q = (TCEnv -> TCEnv) -> tcm a -> tcm a
forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC
  ((TCEnv -> TCEnv) -> tcm a -> tcm a)
-> (TCEnv -> TCEnv) -> tcm a -> tcm a
forall a b. (a -> b) -> a -> b
$ Lens' [ContextEntry] TCEnv -> LensMap [ContextEntry] TCEnv
forall i o. Lens' i o -> LensMap i o
over Lens' [ContextEntry] TCEnv
eContext     ((ContextEntry -> ContextEntry) -> [ContextEntry] -> [ContextEntry]
forall a b. (a -> b) -> [a] -> [b]
map ((ContextEntry -> ContextEntry)
 -> [ContextEntry] -> [ContextEntry])
-> (ContextEntry -> ContextEntry)
-> [ContextEntry]
-> [ContextEntry]
forall a b. (a -> b) -> a -> b
$ Quantity -> ContextEntry -> ContextEntry
forall a. LensQuantity a => Quantity -> a -> a
inverseApplyQuantity Quantity
q)
  (TCEnv -> TCEnv) -> (TCEnv -> TCEnv) -> TCEnv -> TCEnv
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Lens' (Map Name (Open (Term, Dom Type))) TCEnv
-> LensMap (Map Name (Open (Term, Dom Type))) TCEnv
forall i o. Lens' i o -> LensMap i o
over Lens' (Map Name (Open (Term, Dom Type))) TCEnv
eLetBindings ((Open (Term, Dom Type) -> Open (Term, Dom Type))
-> Map Name (Open (Term, Dom Type))
-> Map Name (Open (Term, Dom Type))
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map ((Open (Term, Dom Type) -> Open (Term, Dom Type))
 -> Map Name (Open (Term, Dom Type))
 -> Map Name (Open (Term, Dom Type)))
-> ((Dom Type -> Dom Type)
    -> Open (Term, Dom Type) -> Open (Term, Dom Type))
-> (Dom Type -> Dom Type)
-> Map Name (Open (Term, Dom Type))
-> Map Name (Open (Term, Dom Type))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Term, Dom Type) -> (Term, Dom Type))
-> Open (Term, Dom Type) -> Open (Term, Dom Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (((Term, Dom Type) -> (Term, Dom Type))
 -> Open (Term, Dom Type) -> Open (Term, Dom Type))
-> ((Dom Type -> Dom Type) -> (Term, Dom Type) -> (Term, Dom Type))
-> (Dom Type -> Dom Type)
-> Open (Term, Dom Type)
-> Open (Term, Dom Type)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Dom Type -> Dom Type) -> (Term, Dom Type) -> (Term, Dom Type)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second ((Dom Type -> Dom Type)
 -> Map Name (Open (Term, Dom Type))
 -> Map Name (Open (Term, Dom Type)))
-> (Dom Type -> Dom Type)
-> Map Name (Open (Term, Dom Type))
-> Map Name (Open (Term, Dom Type))
forall a b. (a -> b) -> a -> b
$ Quantity -> Dom Type -> Dom Type
forall a. LensQuantity a => Quantity -> a -> a
inverseApplyQuantity 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 :: Quantity -> tcm a -> tcm a
applyQuantityToJudgementOnly = (TCEnv -> TCEnv) -> tcm a -> tcm a
forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC ((TCEnv -> TCEnv) -> tcm a -> tcm a)
-> (Quantity -> TCEnv -> TCEnv) -> Quantity -> tcm a -> tcm a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Lens' Quantity TCEnv -> LensMap Quantity TCEnv
forall i o. Lens' i o -> LensMap i o
over Lens' Quantity TCEnv
eQuantity LensMap Quantity TCEnv
-> (Quantity -> Quantity -> Quantity) -> Quantity -> TCEnv -> TCEnv
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Quantity -> Quantity -> Quantity
composeQuantity

-- | Apply inverse composition with the given cohesion to the typing context.
applyCohesionToContext :: (MonadTCEnv tcm, LensCohesion m) => m -> tcm a -> tcm a
applyCohesionToContext :: 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
forall a. Monoid a => a
mempty -> 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 :: Cohesion -> tcm a -> tcm a
applyCohesionToContextOnly Cohesion
q = (TCEnv -> TCEnv) -> tcm a -> tcm a
forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC
  ((TCEnv -> TCEnv) -> tcm a -> tcm a)
-> (TCEnv -> TCEnv) -> tcm a -> tcm a
forall a b. (a -> b) -> a -> b
$ Lens' [ContextEntry] TCEnv -> LensMap [ContextEntry] TCEnv
forall i o. Lens' i o -> LensMap i o
over Lens' [ContextEntry] TCEnv
eContext     ((ContextEntry -> ContextEntry) -> [ContextEntry] -> [ContextEntry]
forall a b. (a -> b) -> [a] -> [b]
map ((ContextEntry -> ContextEntry)
 -> [ContextEntry] -> [ContextEntry])
-> (ContextEntry -> ContextEntry)
-> [ContextEntry]
-> [ContextEntry]
forall a b. (a -> b) -> a -> b
$ Cohesion -> ContextEntry -> ContextEntry
forall a. LensCohesion a => Cohesion -> a -> a
inverseApplyCohesion Cohesion
q)
  (TCEnv -> TCEnv) -> (TCEnv -> TCEnv) -> TCEnv -> TCEnv
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Lens' (Map Name (Open (Term, Dom Type))) TCEnv
-> LensMap (Map Name (Open (Term, Dom Type))) TCEnv
forall i o. Lens' i o -> LensMap i o
over Lens' (Map Name (Open (Term, Dom Type))) TCEnv
eLetBindings ((Open (Term, Dom Type) -> Open (Term, Dom Type))
-> Map Name (Open (Term, Dom Type))
-> Map Name (Open (Term, Dom Type))
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map ((Open (Term, Dom Type) -> Open (Term, Dom Type))
 -> Map Name (Open (Term, Dom Type))
 -> Map Name (Open (Term, Dom Type)))
-> ((Dom Type -> Dom Type)
    -> Open (Term, Dom Type) -> Open (Term, Dom Type))
-> (Dom Type -> Dom Type)
-> Map Name (Open (Term, Dom Type))
-> Map Name (Open (Term, Dom Type))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Term, Dom Type) -> (Term, Dom Type))
-> Open (Term, Dom Type) -> Open (Term, Dom Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (((Term, Dom Type) -> (Term, Dom Type))
 -> Open (Term, Dom Type) -> Open (Term, Dom Type))
-> ((Dom Type -> Dom Type) -> (Term, Dom Type) -> (Term, Dom Type))
-> (Dom Type -> Dom Type)
-> Open (Term, Dom Type)
-> Open (Term, Dom Type)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Dom Type -> Dom Type) -> (Term, Dom Type) -> (Term, Dom Type)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second ((Dom Type -> Dom Type)
 -> Map Name (Open (Term, Dom Type))
 -> Map Name (Open (Term, Dom Type)))
-> (Dom Type -> Dom Type)
-> Map Name (Open (Term, Dom Type))
-> Map Name (Open (Term, Dom Type))
forall a b. (a -> b) -> a -> b
$ Cohesion -> Dom Type -> Dom Type
forall a. LensCohesion a => Cohesion -> a -> a
inverseApplyCohesion Cohesion
q)

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

-- | (Conditionally) wake up irrelevant variables and make them relevant.
--   For instance,
--   in an irrelevant function argument otherwise irrelevant variables
--   may be used, so they are awoken before type checking the argument.
--
--   Also allow the use of irrelevant definitions.
applyModalityToContext :: (MonadTCEnv tcm, LensModality m) => m -> tcm a -> tcm a
applyModalityToContext :: 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
forall a. Monoid a => a
mempty -> 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.
--
--   Precondition: @Modality /= Relevant@
applyModalityToContextOnly :: (MonadTCEnv tcm) => Modality -> tcm a -> tcm a
applyModalityToContextOnly :: Modality -> tcm a -> tcm a
applyModalityToContextOnly Modality
m = (TCEnv -> TCEnv) -> tcm a -> tcm a
forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC
  ((TCEnv -> TCEnv) -> tcm a -> tcm a)
-> (TCEnv -> TCEnv) -> tcm a -> tcm a
forall a b. (a -> b) -> a -> b
$ Lens' [ContextEntry] TCEnv -> LensMap [ContextEntry] TCEnv
forall i o. Lens' i o -> LensMap i o
over Lens' [ContextEntry] TCEnv
eContext     ((ContextEntry -> ContextEntry) -> [ContextEntry] -> [ContextEntry]
forall a b. (a -> b) -> [a] -> [b]
map ((ContextEntry -> ContextEntry)
 -> [ContextEntry] -> [ContextEntry])
-> (ContextEntry -> ContextEntry)
-> [ContextEntry]
-> [ContextEntry]
forall a b. (a -> b) -> a -> b
$ Modality -> ContextEntry -> ContextEntry
forall a. LensModality a => Modality -> a -> a
inverseApplyModality Modality
m)
  (TCEnv -> TCEnv) -> (TCEnv -> TCEnv) -> TCEnv -> TCEnv
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Lens' (Map Name (Open (Term, Dom Type))) TCEnv
-> LensMap (Map Name (Open (Term, Dom Type))) TCEnv
forall i o. Lens' i o -> LensMap i o
over Lens' (Map Name (Open (Term, Dom Type))) TCEnv
eLetBindings ((Open (Term, Dom Type) -> Open (Term, Dom Type))
-> Map Name (Open (Term, Dom Type))
-> Map Name (Open (Term, Dom Type))
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map ((Open (Term, Dom Type) -> Open (Term, Dom Type))
 -> Map Name (Open (Term, Dom Type))
 -> Map Name (Open (Term, Dom Type)))
-> ((Dom Type -> Dom Type)
    -> Open (Term, Dom Type) -> Open (Term, Dom Type))
-> (Dom Type -> Dom Type)
-> Map Name (Open (Term, Dom Type))
-> Map Name (Open (Term, Dom Type))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Term, Dom Type) -> (Term, Dom Type))
-> Open (Term, Dom Type) -> Open (Term, Dom Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (((Term, Dom Type) -> (Term, Dom Type))
 -> Open (Term, Dom Type) -> Open (Term, Dom Type))
-> ((Dom Type -> Dom Type) -> (Term, Dom Type) -> (Term, Dom Type))
-> (Dom Type -> Dom Type)
-> Open (Term, Dom Type)
-> Open (Term, Dom Type)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Dom Type -> Dom Type) -> (Term, Dom Type) -> (Term, Dom Type)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second ((Dom Type -> Dom Type)
 -> Map Name (Open (Term, Dom Type))
 -> Map Name (Open (Term, Dom Type)))
-> (Dom Type -> Dom Type)
-> Map Name (Open (Term, Dom Type))
-> Map Name (Open (Term, Dom Type))
forall a b. (a -> b) -> a -> b
$ Modality -> Dom Type -> Dom Type
forall a. LensModality a => Modality -> a -> a
inverseApplyModality 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 :: Modality -> tcm a -> tcm a
applyModalityToJudgementOnly = (TCEnv -> TCEnv) -> tcm a -> tcm a
forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC ((TCEnv -> TCEnv) -> tcm a -> tcm a)
-> (Modality -> TCEnv -> TCEnv) -> Modality -> tcm a -> tcm a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Lens' Modality TCEnv -> LensMap Modality TCEnv
forall i o. Lens' i o -> LensMap i o
over Lens' Modality TCEnv
eModality LensMap Modality TCEnv
-> (Modality -> Modality -> Modality) -> Modality -> TCEnv -> TCEnv
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Modality -> Modality -> Modality
composeModality

-- | Like 'applyModalityToContext', but only act on context (for Relevance) if
--   @--irrelevant-projections@.
--   See issue #2170.
applyModalityToContextFunBody :: (MonadTCM tcm, LensModality r) => r -> tcm a -> tcm a
applyModalityToContextFunBody :: 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).
wakeIrrelevantVars :: (MonadTCEnv tcm) => tcm a -> tcm a
wakeIrrelevantVars :: tcm a -> tcm 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
applyQuantityToContextOnly  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 :: Relevance -> a -> TCM Bool

instance UsableRelevance Term where
  usableRel :: Relevance -> Term -> TCM Bool
usableRel Relevance
rel Term
u = case Term
u of
    Var VerboseLevel
i Elims
vs -> do
      Relevance
irel <- Dom Type -> Relevance
forall a. LensRelevance a => a -> Relevance
getRelevance (Dom Type -> Relevance) -> TCMT IO (Dom Type) -> TCMT IO Relevance
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> VerboseLevel -> TCMT IO (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 -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.irr" VerboseLevel
50 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$
        TCM Doc
"Variable" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (VerboseLevel -> Term
var VerboseLevel
i) TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>
        VerboseKey -> TCM Doc
forall (m :: * -> *). Monad 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 -> TCM Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
ok TCM Bool -> TCM Bool -> TCM Bool
forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`and2M` Relevance -> Elims -> TCM Bool
forall a. UsableRelevance a => Relevance -> a -> TCM Bool
usableRel Relevance
rel Elims
vs
    Def QName
f Elims
vs -> do
      Relevance
frel <- QName -> TCMT IO Relevance
forall (m :: * -> *). HasConstInfo m => QName -> m Relevance
relOfConst QName
f
      Bool -> TCM Bool
forall (m :: * -> *) a. Monad m => a -> m a
return (Relevance
frel Relevance -> Relevance -> Bool
`moreRelevant` Relevance
rel) TCM Bool -> TCM Bool -> TCM Bool
forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`and2M` Relevance -> Elims -> TCM Bool
forall a. UsableRelevance a => Relevance -> a -> TCM Bool
usableRel Relevance
rel Elims
vs
    Con ConHead
c ConInfo
_ Elims
vs -> Relevance -> Elims -> TCM Bool
forall a. UsableRelevance a => Relevance -> a -> TCM Bool
usableRel Relevance
rel Elims
vs
    Lit Literal
l    -> Bool -> TCM Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
    Lam ArgInfo
_ Abs Term
v  -> Relevance -> Abs Term -> TCM Bool
forall a. UsableRelevance a => Relevance -> a -> TCM Bool
usableRel Relevance
rel Abs Term
v
    Pi Dom Type
a Abs Type
b   -> Relevance -> (Dom Type, Abs Type) -> TCM Bool
forall a. UsableRelevance a => Relevance -> a -> TCM Bool
usableRel Relevance
rel (Dom Type
a,Abs Type
b)
    Sort Sort
s   -> Relevance -> Sort -> TCM Bool
forall a. UsableRelevance a => Relevance -> a -> TCM Bool
usableRel Relevance
rel Sort
s
    Level Level
l  -> Bool -> TCM Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
    MetaV MetaId
m Elims
vs -> do
      Relevance
mrel <- MetaVariable -> Relevance
getMetaRelevance (MetaVariable -> Relevance)
-> TCMT IO MetaVariable -> TCMT IO Relevance
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MetaId -> TCMT IO MetaVariable
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupMeta MetaId
m
      Bool -> TCM Bool
forall (m :: * -> *) a. Monad m => a -> m a
return (Relevance
mrel Relevance -> Relevance -> Bool
`moreRelevant` Relevance
rel) TCM Bool -> TCM Bool -> TCM Bool
forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`and2M` Relevance -> Elims -> TCM Bool
forall a. UsableRelevance a => Relevance -> a -> TCM Bool
usableRel Relevance
rel Elims
vs
    DontCare Term
v -> Relevance -> Term -> TCM Bool
forall a. UsableRelevance a => Relevance -> a -> TCM Bool
usableRel Relevance
rel Term
v -- TODO: allow irrelevant things to be used in DontCare position?
    Dummy{}  -> Bool -> TCM Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True

instance UsableRelevance a => UsableRelevance (Type' a) where
  usableRel :: Relevance -> Type' a -> TCM Bool
usableRel Relevance
rel (El Sort
_ a
t) = Relevance -> a -> TCM Bool
forall a. UsableRelevance a => Relevance -> a -> TCM Bool
usableRel Relevance
rel a
t

instance UsableRelevance Sort where
  usableRel :: Relevance -> Sort -> TCM Bool
usableRel Relevance
rel Sort
s = case Sort
s of
    Type Level
l -> Relevance -> Level -> TCM Bool
forall a. UsableRelevance a => Relevance -> a -> TCM Bool
usableRel Relevance
rel Level
l
    Prop Level
l -> Relevance -> Level -> TCM Bool
forall a. UsableRelevance a => Relevance -> a -> TCM Bool
usableRel Relevance
rel Level
l
    Sort
Inf    -> Bool -> TCM Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
    Sort
SizeUniv -> Bool -> TCM Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
    PiSort Dom Type
a Abs Sort
s -> Relevance -> (Dom Type, Abs Sort) -> TCM Bool
forall a. UsableRelevance a => Relevance -> a -> TCM Bool
usableRel Relevance
rel (Dom Type
a,Abs Sort
s)
    FunSort Sort
s1 Sort
s2 -> Relevance -> (Sort, Sort) -> TCM Bool
forall a. UsableRelevance a => Relevance -> a -> TCM Bool
usableRel Relevance
rel (Sort
s1,Sort
s2)
    UnivSort Sort
s -> Relevance -> Sort -> TCM Bool
forall a. UsableRelevance a => Relevance -> a -> TCM Bool
usableRel Relevance
rel Sort
s
    MetaS MetaId
x Elims
es -> Relevance -> Elims -> TCM Bool
forall a. UsableRelevance a => Relevance -> a -> TCM Bool
usableRel Relevance
rel Elims
es
    DefS QName
d Elims
es  -> Relevance -> Term -> TCM Bool
forall a. UsableRelevance a => Relevance -> a -> TCM Bool
usableRel Relevance
rel (Term -> TCM Bool) -> Term -> TCM Bool
forall a b. (a -> b) -> a -> b
$ QName -> Elims -> Term
Def QName
d Elims
es
    DummyS{} -> Bool -> TCM Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True

instance UsableRelevance Level where
  usableRel :: Relevance -> Level -> TCM Bool
usableRel Relevance
rel (Max Integer
_ [PlusLevel' Term]
ls) = Relevance -> [PlusLevel' Term] -> TCM Bool
forall a. UsableRelevance a => Relevance -> a -> TCM Bool
usableRel Relevance
rel [PlusLevel' Term]
ls

instance UsableRelevance PlusLevel where
  usableRel :: Relevance -> PlusLevel' Term -> TCM Bool
usableRel Relevance
rel (Plus Integer
_ LevelAtom' Term
l) = Relevance -> LevelAtom' Term -> TCM Bool
forall a. UsableRelevance a => Relevance -> a -> TCM Bool
usableRel Relevance
rel LevelAtom' Term
l

instance UsableRelevance LevelAtom where
  usableRel :: Relevance -> LevelAtom' Term -> TCM Bool
usableRel Relevance
rel LevelAtom' Term
l = case LevelAtom' Term
l of
    MetaLevel MetaId
m Elims
vs -> do
      Relevance
mrel <- MetaVariable -> Relevance
getMetaRelevance (MetaVariable -> Relevance)
-> TCMT IO MetaVariable -> TCMT IO Relevance
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MetaId -> TCMT IO MetaVariable
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupMeta MetaId
m
      Bool -> TCM Bool
forall (m :: * -> *) a. Monad m => a -> m a
return (Relevance
mrel Relevance -> Relevance -> Bool
`moreRelevant` Relevance
rel) TCM Bool -> TCM Bool -> TCM Bool
forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`and2M` Relevance -> Elims -> TCM Bool
forall a. UsableRelevance a => Relevance -> a -> TCM Bool
usableRel Relevance
rel Elims
vs
    NeutralLevel NotBlocked
_ Term
v -> Relevance -> Term -> TCM Bool
forall a. UsableRelevance a => Relevance -> a -> TCM Bool
usableRel Relevance
rel Term
v
    BlockedLevel MetaId
_ Term
v -> Relevance -> Term -> TCM Bool
forall a. UsableRelevance a => Relevance -> a -> TCM Bool
usableRel Relevance
rel Term
v
    UnreducedLevel Term
v -> Relevance -> Term -> TCM Bool
forall a. UsableRelevance a => Relevance -> a -> TCM Bool
usableRel Relevance
rel Term
v

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

instance (UsableRelevance a, UsableRelevance b) => UsableRelevance (a,b) where
  usableRel :: Relevance -> (a, b) -> TCM Bool
usableRel Relevance
rel (a
a,b
b) = Relevance -> a -> TCM Bool
forall a. UsableRelevance a => Relevance -> a -> TCM Bool
usableRel Relevance
rel a
a TCM Bool -> TCM Bool -> TCM Bool
forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`and2M` Relevance -> b -> TCM Bool
forall a. UsableRelevance a => Relevance -> a -> TCM Bool
usableRel Relevance
rel b
b

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

instance UsableRelevance a => UsableRelevance (Arg a) where
  usableRel :: Relevance -> Arg a -> TCM 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 -> TCM Bool
forall a. UsableRelevance a => Relevance -> a -> TCM Bool
usableRel (Relevance
rel Relevance -> Relevance -> Relevance
`composeRelevance` Relevance
rel') a
u

instance UsableRelevance a => UsableRelevance (Dom a) where
  usableRel :: Relevance -> Dom a -> TCM Bool
usableRel Relevance
rel Dom{unDom :: forall t e. Dom' t e -> e
unDom = a
u} = Relevance -> a -> TCM Bool
forall a. UsableRelevance a => Relevance -> a -> TCM Bool
usableRel Relevance
rel a
u

instance (Subst t a, UsableRelevance a) => UsableRelevance (Abs a) where
  usableRel :: Relevance -> Abs a -> TCM Bool
usableRel Relevance
rel Abs a
abs = Abs a -> (a -> TCM Bool) -> TCM Bool
forall t a (m :: * -> *) b.
(Subst t a, MonadAddContext m) =>
Abs a -> (a -> m b) -> m b
underAbstraction_ Abs a
abs ((a -> TCM Bool) -> TCM Bool) -> (a -> TCM Bool) -> TCM Bool
forall a b. (a -> b) -> a -> b
$ \a
u -> Relevance -> a -> TCM Bool
forall a. UsableRelevance a => Relevance -> a -> TCM 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 :: Modality -> a -> TCM Bool

instance UsableModality Term where
  usableMod :: Modality -> Term -> TCM Bool
usableMod Modality
mod Term
u = 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) -> TCMT IO (Dom Type) -> TCMT IO Modality
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> VerboseLevel -> TCMT IO (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 -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.irr" VerboseLevel
50 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$
        TCM Doc
"Variable" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (VerboseLevel -> Term
var VerboseLevel
i) TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>
        VerboseKey -> TCM Doc
forall (m :: * -> *). Monad 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 -> TCM Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
ok TCM Bool -> TCM Bool -> TCM Bool
forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`and2M` Modality -> Elims -> TCM Bool
forall a. UsableModality a => Modality -> a -> TCM Bool
usableMod Modality
mod Elims
vs
    Def QName
f Elims
vs -> do
      Modality
fmod <- QName -> TCMT IO 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 -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.irr" VerboseLevel
50 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$
        TCM Doc
"Definition" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (QName -> Elims -> Term
Def QName
f []) TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>
        VerboseKey -> TCM Doc
forall (m :: * -> *). Monad 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 -> TCM Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
ok TCM Bool -> TCM Bool -> TCM Bool
forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`and2M` Modality -> Elims -> TCM Bool
forall a. UsableModality a => Modality -> a -> TCM Bool
usableMod Modality
mod Elims
vs
    Con ConHead
c ConInfo
_ Elims
vs -> Modality -> Elims -> TCM Bool
forall a. UsableModality a => Modality -> a -> TCM Bool
usableMod Modality
mod Elims
vs
    Lit Literal
l    -> Bool -> TCM Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
    Lam ArgInfo
_ Abs Term
v  -> Modality -> Abs Term -> TCM Bool
forall a. UsableModality a => Modality -> a -> TCM Bool
usableMod Modality
mod Abs Term
v
    Pi Dom Type
a Abs Type
b   -> Modality -> (Dom Type, Abs Type) -> TCM Bool
forall a. UsableModality a => Modality -> a -> TCM Bool
usableMod Modality
mod (Dom Type
a,Abs Type
b)
    Sort Sort
s   -> Modality -> Sort -> TCM Bool
forall a. UsableModality a => Modality -> a -> TCM Bool
usableMod Modality
mod Sort
s
    Level Level
l  -> Bool -> TCM Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
    MetaV MetaId
m Elims
vs -> do
      Modality
mmod <- MetaVariable -> Modality
getMetaModality (MetaVariable -> Modality)
-> TCMT IO MetaVariable -> TCMT IO Modality
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MetaId -> TCMT IO MetaVariable
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupMeta MetaId
m
      let ok :: Bool
ok = Modality
mmod Modality -> Modality -> Bool
`moreUsableModality` Modality
mod
      VerboseKey -> VerboseLevel -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.irr" VerboseLevel
50 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$
        TCM Doc
"Metavariable" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (MetaId -> Elims -> Term
MetaV MetaId
m []) TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>
        VerboseKey -> TCM Doc
forall (m :: * -> *). Monad 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 -> TCM Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
ok TCM Bool -> TCM Bool -> TCM Bool
forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`and2M` Modality -> Elims -> TCM Bool
forall a. UsableModality a => Modality -> a -> TCM Bool
usableMod Modality
mod Elims
vs
    DontCare Term
v -> Modality -> Term -> TCM Bool
forall a. UsableModality a => Modality -> a -> TCM Bool
usableMod Modality
mod Term
v
    Dummy{}  -> Bool -> TCM Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True

instance UsableRelevance a => UsableModality (Type' a) where
  usableMod :: Modality -> Type' a -> TCM Bool
usableMod Modality
mod (El Sort
_ a
t) = Relevance -> a -> TCM Bool
forall a. UsableRelevance a => Relevance -> a -> TCM Bool
usableRel (Modality -> Relevance
forall a. LensRelevance a => a -> Relevance
getRelevance Modality
mod) a
t

instance UsableModality Sort where
  usableMod :: Modality -> Sort -> TCM Bool
usableMod Modality
mod Sort
s = Relevance -> Sort -> TCM Bool
forall a. UsableRelevance a => Relevance -> a -> TCM 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 :: Modality -> Level -> TCM Bool
usableMod Modality
mod (Max Integer
_ [PlusLevel' Term]
ls) = Relevance -> [PlusLevel' Term] -> TCM Bool
forall a. UsableRelevance a => Relevance -> a -> TCM 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 LevelAtom where
--   usableMod mod l = case l of
--     MetaLevel m vs -> do
--       mmod <- getMetaModality <$> lookupMeta m
--       return (mmod `moreUsableModality` mod) `and2M` usableMod mod vs
--     NeutralLevel _ v -> usableMod mod v
--     BlockedLevel _ v -> usableMod mod v
--     UnreducedLevel v -> usableMod mod v

instance UsableModality a => UsableModality [a] where
  usableMod :: Modality -> [a] -> TCM Bool
usableMod Modality
mod = [TCM Bool] -> TCM Bool
forall (f :: * -> *) (m :: * -> *).
(Foldable f, Monad m) =>
f (m Bool) -> m Bool
andM ([TCM Bool] -> TCM Bool) -> ([a] -> [TCM Bool]) -> [a] -> TCM Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> TCM Bool) -> [a] -> [TCM Bool]
forall a b. (a -> b) -> [a] -> [b]
map (Modality -> a -> TCM Bool
forall a. UsableModality a => Modality -> a -> TCM Bool
usableMod Modality
mod)

instance (UsableModality a, UsableModality b) => UsableModality (a,b) where
  usableMod :: Modality -> (a, b) -> TCM Bool
usableMod Modality
mod (a
a,b
b) = Modality -> a -> TCM Bool
forall a. UsableModality a => Modality -> a -> TCM Bool
usableMod Modality
mod a
a TCM Bool -> TCM Bool -> TCM Bool
forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`and2M` Modality -> b -> TCM Bool
forall a. UsableModality a => Modality -> a -> TCM Bool
usableMod Modality
mod b
b

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

instance UsableModality a => UsableModality (Arg a) where
  usableMod :: Modality -> Arg a -> TCM 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 -> TCM Bool
forall a. UsableModality a => Modality -> a -> TCM Bool
usableMod (Modality
mod Modality -> Modality -> Modality
`composeModality` Modality
mod') a
u

instance UsableModality a => UsableModality (Dom a) where
  usableMod :: Modality -> Dom a -> TCM Bool
usableMod Modality
mod Dom{unDom :: forall t e. Dom' t e -> e
unDom = a
u} = Modality -> a -> TCM Bool
forall a. UsableModality a => Modality -> a -> TCM Bool
usableMod Modality
mod a
u

instance (Subst t a, UsableModality a) => UsableModality (Abs a) where
  usableMod :: Modality -> Abs a -> TCM Bool
usableMod Modality
mod Abs a
abs = Abs a -> (a -> TCM Bool) -> TCM Bool
forall t a (m :: * -> *) b.
(Subst t a, MonadAddContext m) =>
Abs a -> (a -> m b) -> m b
underAbstraction_ Abs a
abs ((a -> TCM Bool) -> TCM Bool) -> (a -> TCM Bool) -> TCM Bool
forall a b. (a -> b) -> a -> b
$ \a
u -> Modality -> a -> TCM Bool
forall a. UsableModality a => Modality -> a -> TCM Bool
usableMod Modality
mod a
u


-- * Propositions

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

isPropM :: (LensSort a, PrettyTCM a, MonadReduce m, MonadDebug m) => a -> m Bool
isPropM :: a -> m Bool
isPropM a
a = do
  VerboseKey -> VerboseLevel -> TCM Doc -> m Bool -> m Bool
forall (m :: * -> *) a.
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m a -> m a
traceSDoc VerboseKey
"tc.prop" VerboseLevel
80 (TCM Doc
"Is " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> a -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM a
a TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCM Doc
"of sort" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Sort -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (a -> Sort
forall a. LensSort a => a -> Sort
getSort a
a) TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCM Doc
"in Prop?") (m Bool -> m Bool) -> m Bool -> m Bool
forall a b. (a -> b) -> a -> b
$ do
  Sort -> m Sort
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce (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, MonadReduce m, MonadDebug m) => a -> m Bool
isIrrelevantOrPropM :: a -> m Bool
isIrrelevantOrPropM a
x = Bool -> m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return (a -> Bool
forall a. LensRelevance a => a -> Bool
isIrrelevant a
x) m Bool -> m Bool -> m Bool
forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`or2M` a -> m Bool
forall a (m :: * -> *).
(LensSort a, PrettyTCM a, MonadReduce m, MonadDebug m) =>
a -> m Bool
isPropM a
x