{-# OPTIONS_GHC -Wunused-imports #-}

{-# LANGUAGE NondecreasingIndentation #-}

{-| Compile-time irrelevance.

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

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

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

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

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

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

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

@@

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

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

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


-}

module Agda.TypeChecking.Irrelevance where

import Control.Monad.Except

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

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

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

instance UsableRelevance Sort where
  usableRel :: forall (m :: * -> *).
(ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m,
 MonadDebug m) =>
Relevance -> Sort -> m Bool
usableRel Relevance
rel = \case
    Univ Univ
_ Level
l -> forall a (m :: * -> *).
(UsableRelevance a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
 MonadAddContext m, MonadDebug m) =>
Relevance -> a -> m Bool
usableRel Relevance
rel Level
l
    Inf Univ
_ Integer
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
    Sort
SizeUniv -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
    Sort
LockUniv -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
    Sort
LevelUniv -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
    Sort
IntervalUniv -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
    PiSort Dom' Term Term
a Sort
s1 Abs Sort
s2 -> forall a (m :: * -> *).
(UsableRelevance a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
 MonadAddContext m, MonadDebug m) =>
Relevance -> a -> m Bool
usableRel Relevance
rel (Dom' Term Term
a,Sort
s1,Abs Sort
s2)
    FunSort Sort
s1 Sort
s2 -> forall a (m :: * -> *).
(UsableRelevance a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
 MonadAddContext m, MonadDebug m) =>
Relevance -> a -> m Bool
usableRel Relevance
rel (Sort
s1,Sort
s2)
    UnivSort Sort
s -> forall a (m :: * -> *).
(UsableRelevance a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
 MonadAddContext m, MonadDebug m) =>
Relevance -> a -> m Bool
usableRel Relevance
rel Sort
s
    MetaS MetaId
x Elims
es -> forall a (m :: * -> *).
(UsableRelevance a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
 MonadAddContext m, MonadDebug m) =>
Relevance -> a -> m Bool
usableRel Relevance
rel Elims
es
    DefS QName
d Elims
es  -> forall a (m :: * -> *).
(UsableRelevance a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
 MonadAddContext m, MonadDebug m) =>
Relevance -> a -> m Bool
usableRel Relevance
rel forall a b. (a -> b) -> a -> b
$ QName -> Elims -> Term
Def QName
d Elims
es
    DummyS{} -> 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) = forall a (m :: * -> *).
(UsableRelevance a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
 MonadAddContext m, MonadDebug m) =>
Relevance -> a -> m Bool
usableRel Relevance
rel [PlusLevel' Term]
ls

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

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

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

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

instance UsableRelevance a => UsableRelevance (Elim' a) where
  usableRel :: forall (m :: * -> *).
(ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m,
 MonadDebug m) =>
Relevance -> Elim' a -> m Bool
usableRel Relevance
rel (Apply Arg a
a) = forall a (m :: * -> *).
(UsableRelevance a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
 MonadAddContext m, MonadDebug m) =>
Relevance -> a -> m Bool
usableRel Relevance
rel Arg a
a
  usableRel Relevance
rel (Proj ProjOrigin
_ QName
p) = do
    Relevance
prel <- forall (m :: * -> *). HasConstInfo m => QName -> m Relevance
relOfConst QName
p
    forall (m :: * -> *) a. Monad m => a -> m a
return 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) = forall a (m :: * -> *).
(UsableRelevance a, 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' = forall a. LensRelevance a => a -> Relevance
getRelevance ArgInfo
info
    in  forall a (m :: * -> *).
(UsableRelevance a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
 MonadAddContext m, MonadDebug m) =>
Relevance -> a -> m Bool
usableRel (Relevance
rel Relevance -> Relevance -> Relevance
`composeRelevance` Relevance
rel') a
u

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

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

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

instance UsableModality Term where
  usableMod :: forall (m :: * -> *).
(ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m,
 MonadDebug m, MonadReduce m, MonadError Blocker m) =>
Modality -> Term -> m Bool
usableMod Modality
mod Term
u = do
   case Term
u of
    Var Int
i Elims
vs -> do
      Modality
imod <- forall a. LensModality a => a -> Modality
getModality forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(Applicative m, MonadFail m, MonadTCEnv m) =>
Int -> m (Dom Type)
domOfBV Int
i
      let ok :: Bool
ok = Modality
imod Modality -> Modality -> Bool
`moreUsableModality` Modality
mod
      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.irr" Int
50 forall a b. (a -> b) -> a -> b
$
        TCMT IO Doc
"Variable" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (Int -> Term
var Int
i) forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>
        forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char]
"has modality " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Modality
imod forall a. [a] -> [a] -> [a]
++ [Char]
", which is a " forall a. [a] -> [a] -> [a]
++
              (if Bool
ok then [Char]
"" else [Char]
"NOT ") forall a. [a] -> [a] -> [a]
++ [Char]
"more usable modality than " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Modality
mod)
      forall (m :: * -> *) a. Monad m => a -> m a
return Bool
ok forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`and2M` forall a (m :: * -> *).
(UsableModality a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
 MonadAddContext m, MonadDebug m, MonadReduce m,
 MonadError Blocker m) =>
Modality -> a -> m Bool
usableMod Modality
mod Elims
vs
    Def QName
f Elims
vs -> do
      Modality
fmod <- forall (m :: * -> *). HasConstInfo m => QName -> m Modality
modalityOfConst QName
f
      -- Pure modalities don't matter here, only positional ones, hence remove
      -- them from the equation.
      let ok :: Bool
ok = forall a. LensCohesion a => Cohesion -> a -> a
setCohesion Cohesion
Flat Modality
fmod Modality -> Modality -> Bool
`moreUsableModality` Modality
mod
      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.irr" Int
50 forall a b. (a -> b) -> a -> b
$
        TCMT IO Doc
"Definition" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (QName -> Elims -> Term
Def QName
f []) forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>
        forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char]
"has modality " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Modality
fmod forall a. [a] -> [a] -> [a]
++ [Char]
", which is a " forall a. [a] -> [a] -> [a]
++
              (if Bool
ok then [Char]
"" else [Char]
"NOT ") forall a. [a] -> [a] -> [a]
++ [Char]
"more usable modality than " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Modality
mod)
      forall (m :: * -> *) a. Monad m => a -> m a
return Bool
ok forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`and2M` forall a (m :: * -> *).
(UsableModality a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
 MonadAddContext m, MonadDebug m, MonadReduce m,
 MonadError Blocker m) =>
Modality -> a -> m Bool
usableMod Modality
mod Elims
vs
    Con ConHead
c ConInfo
o Elims
vs -> do
      Modality
cmod <- 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
      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.irr" Int
50 forall a b. (a -> b) -> a -> b
$
        TCMT IO Doc
"The constructor" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (ConHead -> ConInfo -> Elims -> Term
Con ConHead
c ConInfo
o []) forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>
        forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char]
"has the modality " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Modality
cmod forall a. [a] -> [a] -> [a]
++ [Char]
", which is " forall a. [a] -> [a] -> [a]
++
              (if Bool
ok then [Char]
"" else [Char]
"NOT ") forall a. [a] -> [a] -> [a]
++
              [Char]
"more usable than the modality " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Modality
mod forall a. [a] -> [a] -> [a]
++ [Char]
".")
      forall (m :: * -> *) a. Monad m => a -> m a
return Bool
ok forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`and2M` forall a (m :: * -> *).
(UsableModality a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
 MonadAddContext m, MonadDebug m, MonadReduce m,
 MonadError Blocker m) =>
Modality -> a -> m Bool
usableMod Modality
mod Elims
vs
    Lit Literal
l    -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
    Lam ArgInfo
info Abs Term
v  -> 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   -> forall a (m :: * -> *).
(UsableModality a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
 MonadAddContext m, MonadDebug m, MonadReduce m,
 MonadError Blocker m) =>
Modality -> a -> m Bool
usableMod Modality
domMod (forall t a. Type'' t a -> a
unEl forall a b. (a -> b) -> a -> b
$ forall t e. Dom' t e -> e
unDom Dom Type
a) forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`and2M` 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 (forall a. LensArgInfo a => a -> ArgInfo
getArgInfo Dom Type
a) Modality
mod (forall t a. Type'' t a -> a
unEl forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Abs Type
b)
      where
        domMod :: Modality
domMod = forall a. LensQuantity a => (Quantity -> Quantity) -> a -> a
mapQuantity (Quantity -> Quantity -> Quantity
composeQuantity forall a b. (a -> b) -> a -> b
$ forall a. LensQuantity a => a -> Quantity
getQuantity Dom Type
a) forall a b. (a -> b) -> a -> b
$
                 forall a. LensCohesion a => (Cohesion -> Cohesion) -> a -> a
mapCohesion (Cohesion -> Cohesion -> Cohesion
composeCohesion forall a b. (a -> b) -> a -> b
$ 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   -> forall a (m :: * -> *).
(UsableModality a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
 MonadAddContext m, MonadDebug m, MonadReduce m,
 MonadError Blocker m) =>
Modality -> a -> m Bool
usableMod Modality
mod Sort
s
    Level Level
l  -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
    MetaV MetaId
m Elims
vs -> do
      Modality
mmod <- forall (m :: * -> *). ReadTCState m => MetaId -> m Modality
lookupMetaModality MetaId
m
      let ok :: Bool
ok = Modality
mmod Modality -> Modality -> Bool
`moreUsableModality` Modality
mod
      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.irr" Int
50 forall a b. (a -> b) -> a -> b
$
        TCMT IO Doc
"Metavariable" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (MetaId -> Elims -> Term
MetaV MetaId
m []) forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>
        forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char]
"has modality " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Modality
mmod forall a. [a] -> [a] -> [a]
++ [Char]
", which is a " forall a. [a] -> [a] -> [a]
++
              (if Bool
ok then [Char]
"" else [Char]
"NOT ") forall a. [a] -> [a] -> [a]
++ [Char]
"more usable modality than " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Modality
mod)
      (forall (m :: * -> *) a. Monad m => a -> m a
return Bool
ok forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`and2M` forall a (m :: * -> *).
(UsableModality a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
 MonadAddContext m, MonadDebug m, MonadReduce m,
 MonadError Blocker m) =>
Modality -> a -> m Bool
usableMod Modality
mod Elims
vs) forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`or2M` do
        Term
u <- forall a (m :: * -> *). (Instantiate a, MonadReduce m) => a -> m a
instantiate Term
u
        forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe (forall a. IsMeta a => a -> Maybe MetaId
isMeta Term
u) (forall a (m :: * -> *).
(UsableModality a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
 MonadAddContext m, MonadDebug m, MonadReduce m,
 MonadError Blocker m) =>
Modality -> a -> m Bool
usableMod Modality
mod Term
u) forall a b. (a -> b) -> a -> b
$ \ MetaId
m -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (MetaId -> Blocker
UnblockOnMeta MetaId
m)
    DontCare Term
v -> forall a (m :: * -> *).
(UsableModality a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
 MonadAddContext m, MonadDebug m, MonadReduce m,
 MonadError Blocker m) =>
Modality -> a -> m Bool
usableMod Modality
mod Term
v
    Dummy{}  -> 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 = forall a (m :: * -> *) b.
(Subst a, MonadAddContext m) =>
Dom Type -> Abs a -> (a -> m b) -> m b
underAbstraction (forall a. LensArgInfo a => ArgInfo -> a -> a
setArgInfo ArgInfo
info forall a b. (a -> b) -> a -> b
$ HasCallStack => Dom Type
__DUMMY_DOM__) Abs a
abs forall a b. (a -> b) -> a -> b
$ \ a
u -> forall a (m :: * -> *).
(UsableModality a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
 MonadAddContext m, MonadDebug m, MonadReduce m,
 MonadError Blocker m) =>
Modality -> a -> m Bool
usableMod Modality
mod a
u

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

instance UsableModality Level where
  usableMod :: forall (m :: * -> *).
(ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m,
 MonadDebug m, MonadReduce m, MonadError Blocker m) =>
Modality -> Level -> m Bool
usableMod Modality
mod (Max Integer
_ [PlusLevel' Term]
ls) = forall a (m :: * -> *).
(UsableRelevance a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
 MonadAddContext m, MonadDebug m) =>
Relevance -> a -> m Bool
usableRel (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 = forall (f :: * -> *) (m :: * -> *).
(Foldable f, Monad m) =>
f (m Bool) -> m Bool
andM forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map (forall a (m :: * -> *).
(UsableModality a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
 MonadAddContext m, MonadDebug m, MonadReduce m,
 MonadError Blocker m) =>
Modality -> a -> m Bool
usableMod Modality
mod)

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

instance UsableModality a => UsableModality (Elim' a) where
  usableMod :: forall (m :: * -> *).
(ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m,
 MonadDebug m, MonadReduce m, MonadError Blocker m) =>
Modality -> Elim' a -> m Bool
usableMod Modality
mod (Apply Arg a
a) = forall a (m :: * -> *).
(UsableModality a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
 MonadAddContext m, MonadDebug m, MonadReduce m,
 MonadError Blocker m) =>
Modality -> a -> m Bool
usableMod Modality
mod Arg a
a
  usableMod Modality
mod (Proj ProjOrigin
_ QName
p) = do
    Modality
pmod <- forall (m :: * -> *). HasConstInfo m => QName -> m Modality
modalityOfConst QName
p
    forall (m :: * -> *) a. Monad m => a -> m a
return 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) = forall a (m :: * -> *).
(UsableModality a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
 MonadAddContext m, MonadDebug m, MonadReduce m,
 MonadError Blocker m) =>
Modality -> a -> m Bool
usableMod Modality
mod a
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' = forall a. LensModality a => a -> Modality
getModality ArgInfo
info
    in  forall a (m :: * -> *).
(UsableModality a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
 MonadAddContext m, MonadDebug m, MonadReduce m,
 MonadError Blocker m) =>
Modality -> a -> m Bool
usableMod (Modality
mod Modality -> Modality -> Modality
`composeModality` Modality
mod') a
u

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

usableAtModality'
  :: MonadConstraint TCM
  -- 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 =
  forall (m :: * -> *).
MonadConstraint m =>
Constraint -> m () -> m ()
catchConstraint (WhyCheckModality -> Maybe Sort -> Modality -> Term -> Constraint
UsableAtModality WhyCheckModality
why Maybe Sort
ms Modality
mod Term
t) forall a b. (a -> b) -> a -> b
$ do
    forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM (forall b a. b -> (a -> b) -> Maybe a -> b
maybe (forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True) forall a (m :: * -> *).
(LensSort a, PureTCM m, MonadBlock m) =>
a -> m Bool
isFibrant Maybe Sort
ms) forall a b. (a -> b) -> a -> b
$ do
      Either Blocker Bool
res <- forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *).
(UsableModality a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
 MonadAddContext m, MonadDebug m, MonadReduce m,
 MonadError Blocker m) =>
Modality -> a -> m Bool
usableMod Modality
mod Term
t
      case Either Blocker Bool
res of
        Right Bool
b -> forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
b forall a b. (a -> b) -> a -> b
$
          forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
GenericDocError forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCMT IO Doc
formatWhy
        Left Blocker
blocker -> forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation Blocker
blocker
  where
    formatWhy :: TCMT IO Doc
formatWhy = do
      Bool
compatible <- PragmaOptions -> Bool
optCubicalCompatible forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions
      Bool
cubical <- forall a. Maybe a -> Bool
isJust forall b c a. (b -> c) -> (a -> b) -> a -> c
. PragmaOptions -> Maybe Cubical
optCubical forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions
      let
        context :: [Char]
context
          | Bool
cubical    = [Char]
"in Cubical Agda,"
          | Bool
compatible = [Char]
"to maintain compatibility with Cubical Agda,"
          | Bool
otherwise  = [Char]
"when --without-K is enabled,"

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

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

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

        -- Note: if a generated clause is modality-incorrect, that's a
        -- bug in the LHS modality check
        WhyCheckModality
GeneratedClause ->
          forall (m :: * -> *) a.
(HasCallStack, MonadDebug m) =>
[Char] -> m a
__IMPOSSIBLE_VERBOSE__ forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> [Char]
show forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<
                   forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
t
              forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"is not usable at the required modality"
              forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (f :: * -> *) a. Applicative f => a -> f a
pure (Modality -> Doc
attributesForModality Modality
mod)
        WhyCheckModality
_ -> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
t forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"is not usable at the required modality"
         forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> 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 = MonadConstraint (TCMT IO) =>
Maybe Sort -> WhyCheckModality -> Modality -> Term -> TCM ()
usableAtModality' 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
  forall (m :: * -> *) a.
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m a -> m a
traceSDoc [Char]
"tc.prop" Int
80 (TCMT IO Doc
"Is " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM a
a forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"of sort" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (forall a. LensSort a => a -> Sort
getSort a
a) forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"in Prop?") forall a b. (a -> b) -> a -> b
$ do
  forall (m :: * -> *) t.
(MonadReduce m, MonadBlock m, IsMeta t, Reduce t) =>
t -> m t
abortIfBlocked (forall a. LensSort a => a -> Sort
getSort a
a) 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 = forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. LensRelevance a => a -> Bool
isIrrelevant a
x) forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`or2M` 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 = forall (m :: * -> *) t.
(MonadReduce m, MonadBlock m, IsMeta t, Reduce t) =>
t -> m t
abortIfBlocked (forall a. LensSort a => a -> Sort
getSort a
a) forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> \case
  Univ Univ
u Level
_   -> Univ -> IsFibrant
univFibrancy Univ
u forall a. Eq a => a -> a -> Bool
== IsFibrant
IsFibrant
  Inf Univ
u Integer
_    -> Univ -> IsFibrant
univFibrancy Univ
u forall a. Eq a => a -> a -> Bool
== IsFibrant
IsFibrant
  SizeUniv{} -> Bool
False
  LockUniv{} -> Bool
False
  LevelUniv{}  -> 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 = forall (m :: * -> *) t.
(MonadReduce m, MonadBlock m, IsMeta t, Reduce t) =>
t -> m t
abortIfBlocked (forall a. LensSort a => a -> Sort
getSort a
a) forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> \case
  Univ Univ
u Level
_   -> Univ -> IsFibrant
univFibrancy Univ
u forall a. Eq a => a -> a -> Bool
== IsFibrant
IsFibrant
  Inf Univ
u Integer
_    -> Univ -> IsFibrant
univFibrancy Univ
u forall a. Eq a => a -> a -> Bool
== IsFibrant
IsFibrant
  SizeUniv{} -> Bool
False
  LockUniv{} -> Bool
True
  LevelUniv{}  -> Bool
False
  IntervalUniv{} -> Bool
True
  PiSort{}   -> Bool
False
  FunSort{}  -> Bool
False
  UnivSort{} -> Bool
False
  MetaS{}    -> Bool
False
  DefS{}     -> Bool
False
  DummyS{}   -> Bool
False