    {-# OPTIONS_GHC -Wunused-imports #-}

    module Agda.TypeChecking.Modalities
      ( checkModality'
      , checkModality
      , checkModalityArgs
      ) where

    import Control.Applicative ((<|>))

    import Agda.Interaction.Options

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

    import Agda.TypeChecking.Conversion
    import Agda.TypeChecking.Free
    import Agda.TypeChecking.Free.Lazy
    import Agda.TypeChecking.Monad
    import Agda.TypeChecking.Pretty
    import Agda.TypeChecking.Substitute

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

    -- | The second argument is the definition of the first.
    --   Returns 'Nothing' if ok, otherwise the error message.
    checkRelevance' :: (MonadConversion m) => QName -> Definition -> m (Maybe TypeError)
    checkRelevance' :: forall (m :: * -> *).
    MonadConversion m =>
    QName -> Definition -> m (Maybe TypeError)
    checkRelevance' QName
    x Definition
    def = do
      case Definition -> Relevance
    forall a. LensRelevance a => a -> Relevance
    getRelevance Definition
    def of
        Relevant{} -> Maybe TypeError -> m (Maybe TypeError)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe TypeError
    forall a. Maybe a
    Nothing -- relevance functions can be used in any context.
        Relevance
    drel -> do
          -- Andreas,, 2018-06-09, issue #2170
          -- irrelevant projections are only allowed if --irrelevant-projections
          let isProj :: Bool
    isProj = Definition -> Defn
    theDef Definition
    def Defn -> Lens' Defn Bool -> Bool
    forall o i. o -> Lens' o i -> i
    ^. (Bool -> f Bool) -> Defn -> f Defn
    Lens' Defn Bool
    funProj
          m Bool
    -> m (Maybe TypeError)
    -> m (Maybe TypeError)
    -> m (Maybe TypeError)
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
    ifM (Bool -> m Bool
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Bool
    isProj m Bool -> m Bool -> m Bool
    forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
    `and2M`
               (Bool -> Bool
    not (Bool -> Bool) -> (PragmaOptions -> Bool) -> PragmaOptions -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PragmaOptions -> Bool
    optIrrelevantProjections (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)) {-then-} m (Maybe TypeError)
    needIrrProj {-else-} (m (Maybe TypeError) -> m (Maybe TypeError))
    -> m (Maybe TypeError) -> m (Maybe TypeError)
    forall a b. (a -> b) -> a -> b
    $ do
            rel <- Lens' TCEnv Relevance -> m Relevance
    forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
    viewTC (Relevance -> f Relevance) -> TCEnv -> f TCEnv
    Lens' TCEnv Relevance
    eRelevance
            reportSDoc "tc.irr" 50 $ vcat
              [ "declaration relevance =" <+> text (show drel)
              , "context     relevance =" <+> text (show rel)
              , prettyTCM x <+> "is" <+> applyUnless isProj ("not" <+>) "a projection"
              ]
            return $ boolToMaybe (not $ drel `moreRelevant` rel) $ DefinitionIsIrrelevant x
      where
      needIrrProj :: m (Maybe TypeError)
    needIrrProj = Maybe TypeError -> m (Maybe TypeError)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe TypeError -> m (Maybe TypeError))
    -> Maybe TypeError -> m (Maybe TypeError)
    forall a b. (a -> b) -> a -> b
    $ TypeError -> Maybe TypeError
    forall a. a -> Maybe a
    Just (TypeError -> Maybe TypeError) -> TypeError -> Maybe TypeError
    forall a b. (a -> b) -> a -> b
    $ QName -> TypeError
    ProjectionIsIrrelevant QName
    x

    -- | The second argument is the definition of the first.
    --   Returns 'Nothing' if ok, otherwise the error message.
    checkQuantity' :: (MonadConversion m) => QName -> Definition -> m (Maybe TypeError)
    checkQuantity' :: forall (m :: * -> *).
    MonadConversion m =>
    QName -> Definition -> m (Maybe TypeError)
    checkQuantity' QName
    x Definition
    def = do
      case Definition -> Quantity
    forall a. LensQuantity a => a -> Quantity
    getQuantity Definition
    def of
        dq :: Quantity
    dq@Quantityω{} -> do
          VerboseKey -> VerboseLevel -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> VerboseLevel -> TCMT IO Doc -> m ()
    reportSDoc VerboseKey
    "tc.irr" VerboseLevel
    50 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
    forall a b. (a -> b) -> a -> b
    $ [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat
            [ TCMT IO Doc
    "declaration quantity =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> VerboseKey -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => VerboseKey -> m Doc
    text (Quantity -> VerboseKey
    forall a. Show a => a -> VerboseKey
    show Quantity
    dq)
            -- , "context     quantity =" <+> text (show q)
            ]
          Maybe TypeError -> m (Maybe TypeError)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe TypeError
    forall a. Maybe a
    Nothing -- Abundant definitions can be used in any context.
        Quantity
    dq -> do
          q <- Lens' TCEnv Quantity -> m Quantity
    forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
    viewTC (Quantity -> f Quantity) -> TCEnv -> f TCEnv
    Lens' TCEnv Quantity
    eQuantity
          reportSDoc "tc.irr" 50 $ vcat
            [ "declaration quantity =" <+> text (show dq)
            , "context     quantity =" <+> text (show q)
            ]
          return $ boolToMaybe (not $ dq `moreQuantity` q) $ DefinitionIsErased x

    -- | The second argument is the definition of the first.
    checkModality' :: (MonadConversion m) => QName -> Definition -> m (Maybe TypeError)
    checkModality' :: forall (m :: * -> *).
    MonadConversion m =>
    QName -> Definition -> m (Maybe TypeError)
    checkModality' QName
    x Definition
    def = do
      relOk <- QName -> Definition -> m (Maybe TypeError)
    forall (m :: * -> *).
    MonadConversion m =>
    QName -> Definition -> m (Maybe TypeError)
    checkRelevance' QName
    x Definition
    def
      qtyOk <- checkQuantity' x def
      return $ relOk <|> qtyOk

    -- | The second argument is the definition of the first.
    checkModality :: (MonadConversion m) => QName -> Definition -> m ()
    checkModality :: forall (m :: * -> *).
    MonadConversion m =>
    QName -> Definition -> m ()
    checkModality QName
    x Definition
    def = QName -> Definition -> m (Maybe TypeError)
    forall (m :: * -> *).
    MonadConversion m =>
    QName -> Definition -> m (Maybe TypeError)
    checkModality' QName
    x Definition
    def m (Maybe TypeError) -> (Maybe TypeError -> m ()) -> m ()
    forall a b. m a -> (a -> m b) -> m b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= (TypeError -> m (ZonkAny 0)) -> Maybe TypeError -> m ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ TypeError -> m (ZonkAny 0)
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError

    -- | Checks that the given implicitely inserted arguments, are used in a modally
    --   correct way.
    checkModalityArgs :: (MonadConversion m) => Definition -> Args -> m ()
    checkModalityArgs :: forall (m :: * -> *).
    MonadConversion m =>
    Definition -> Args -> m ()
    checkModalityArgs Definition
    d Args
    vs = do
      let
        vmap :: VarMap
        vmap :: VarMap
    vmap = Args -> VarMap
    forall a c t.
    (IsVarSet a c, Singleton VerboseLevel c, Free t) =>
    t -> c
    freeVars Args
    vs

      -- we iterate over all vars in the context and their ArgInfo,
      -- checking for each that "vs" uses them as allowed.
      as <- m Args
    forall (m :: * -> *). MonadTCEnv m => m Args
    getContextArgs
      forM_ as $ \ (Arg ArgInfo
    avail Term
    t) -> do
        let m :: Maybe Modality
    m = do
              v <- Term -> Maybe VerboseLevel
    forall a. DeBruijn a => a -> Maybe VerboseLevel
    deBruijnView Term
    t
              varModality <$> lookupVarMap v vmap
        Maybe Modality -> (Modality -> m ()) -> m ()
    forall (m :: * -> *) a. Monad m => Maybe a -> (a -> m ()) -> m ()
    whenJust Maybe Modality
    m ((Modality -> m ()) -> m ()) -> (Modality -> m ()) -> m ()
    forall a b. (a -> b) -> a -> b
    $ \ Modality
    used -> do
          let availPosMod :: Modality
    availPosMod = Modality -> Modality
    positionalModalityComponent (ArgInfo -> Modality
    forall a. LensModality a => a -> Modality
    getModality ArgInfo
    avail)
              usedPosMod :: Modality
    usedPosMod = Modality -> Modality
    positionalModalityComponent (Modality -> Modality
    forall a. LensModality a => a -> Modality
    getModality Modality
    used)
          Bool -> m () -> m ()
    forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
    unless (Modality
    availPosMod Modality -> Modality -> Bool
    `moreUsableModality` Modality
    usedPosMod) (m () -> m ()) -> m () -> m ()
    forall a b. (a -> b) -> a -> b
    $
             TypeError -> m ()
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> m ()) -> TypeError -> m ()
    forall a b. (a -> b) -> a -> b
    $ Term -> Modality -> Modality -> Definition -> TypeError
    InvalidModalTelescopeUse Term
    t Modality
    usedPosMod Modality
    availPosMod Definition
    d