    -- | Computing the polarity (variance) of function arguments,
    --   for the sake of subtyping.

    module Agda.TypeChecking.Polarity
      ( -- * Polarity computation
        computePolarity
        -- * Auxiliary functions
      , composePol
      , nextPolarity
      , purgeNonvariant
      , polFromOcc
      ) where

    import Control.Monad  ( forM_, zipWithM )

    import Data.Maybe
    import Data.Semigroup ( Semigroup(..) )

    import Agda.Syntax.Abstract.Name
    import Agda.Syntax.Common
    import Agda.Syntax.Internal

    import Agda.TypeChecking.Monad
    import Agda.TypeChecking.Datatypes (getNumberOfParameters)
    import Agda.TypeChecking.Pretty
    import Agda.TypeChecking.SizedTypes
    import Agda.TypeChecking.Substitute
    import Agda.TypeChecking.Telescope
    import Agda.TypeChecking.Reduce
    import Agda.TypeChecking.Free
    import Agda.TypeChecking.Positivity.Occurrence

    import Agda.Utils.List
    import Agda.Utils.Maybe ( whenNothingM )
    import Agda.Utils.Monad
    import Agda.Utils.Pretty ( prettyShow )
    import Agda.Utils.Singleton
    import Agda.Utils.Size

    import Agda.Utils.Impossible

    ------------------------------------------------------------------------
    -- * Polarity lattice.
    ------------------------------------------------------------------------

    -- | Infimum on the information lattice.
    --   'Invariant' is bottom (dominant for inf),
    --   'Nonvariant' is top (neutral for inf).
    (/\) :: Polarity -> Polarity -> Polarity
    Polarity
    Nonvariant /\ :: Polarity -> Polarity -> Polarity
    /\ Polarity
    b = Polarity
    b
    Polarity
    a /\ Polarity
    Nonvariant = Polarity
    a
    Polarity
    a /\ Polarity
    b | Polarity
    a Polarity -> Polarity -> Bool
    forall a. Eq a => a -> a -> Bool
    == Polarity
    b    = Polarity
    a
           | Bool
    otherwise = Polarity
    Invariant

    -- | 'Polarity' negation, swapping monotone and antitone.
    neg :: Polarity -> Polarity
    neg :: Polarity -> Polarity
    neg Polarity
    Covariant     = Polarity
    Contravariant
    neg Polarity
    Contravariant = Polarity
    Covariant
    neg Polarity
    Invariant     = Polarity
    Invariant
    neg Polarity
    Nonvariant    = Polarity
    Nonvariant

    -- | What is the polarity of a function composition?
    composePol :: Polarity -> Polarity -> Polarity
    composePol :: Polarity -> Polarity -> Polarity
    composePol Polarity
    Nonvariant Polarity
    _    = Polarity
    Nonvariant
    composePol Polarity
    _ Polarity
    Nonvariant    = Polarity
    Nonvariant
    composePol Polarity
    Invariant Polarity
    _     = Polarity
    Invariant
    composePol Polarity
    Covariant Polarity
    x     = Polarity
    x
    composePol Polarity
    Contravariant Polarity
    x = Polarity -> Polarity
    neg Polarity
    x

    polFromOcc :: Occurrence -> Polarity
    polFromOcc :: Occurrence -> Polarity
    polFromOcc = \case
      Occurrence
    GuardPos  -> Polarity
    Covariant
      Occurrence
    StrictPos -> Polarity
    Covariant
      Occurrence
    JustPos   -> Polarity
    Covariant
      Occurrence
    JustNeg   -> Polarity
    Contravariant
      Occurrence
    Mixed     -> Polarity
    Invariant
      Occurrence
    Unused    -> Polarity
    Nonvariant

    ------------------------------------------------------------------------
    -- * Auxiliary functions
    ------------------------------------------------------------------------

    -- | Get the next polarity from a list, 'Invariant' if empty.
    nextPolarity :: [Polarity] -> (Polarity, [Polarity])
    nextPolarity :: [Polarity] -> (Polarity, [Polarity])
    nextPolarity []       = (Polarity
    Invariant, [])
    nextPolarity (Polarity
    p : [Polarity]
    ps) = (Polarity
    p, [Polarity]
    ps)

    -- | Replace 'Nonvariant' by 'Covariant'.
    --   (Arbitrary bias, but better than 'Invariant', see issue 1596).
    purgeNonvariant :: [Polarity] -> [Polarity]
    purgeNonvariant :: [Polarity] -> [Polarity]
    purgeNonvariant = (Polarity -> Polarity) -> [Polarity] -> [Polarity]
    forall a b. (a -> b) -> [a] -> [b]
    map (\ Polarity
    p -> if Polarity
    p Polarity -> Polarity -> Bool
    forall a. Eq a => a -> a -> Bool
    == Polarity
    Nonvariant then Polarity
    Covariant else Polarity
    p)

    -- | A quick transliterations of occurrences to polarities.
    polarityFromPositivity
      :: (HasConstInfo m, MonadTCEnv m, MonadTCState m, MonadDebug m)
      => QName -> m ()
    polarityFromPositivity :: forall (m :: * -> *).
    (HasConstInfo m, MonadTCEnv m, MonadTCState m, MonadDebug m) =>
    QName -> m ()
    polarityFromPositivity QName
    x = QName -> (Definition -> m ()) -> m ()
    forall (m :: * -> *) a.
    (MonadTCEnv m, HasConstInfo m) =>
    QName -> (Definition -> m a) -> m a
    inConcreteOrAbstractMode QName
    x ((Definition -> m ()) -> m ()) -> (Definition -> m ()) -> m ()
    forall a b. (a -> b) -> a -> b
    $ \ Definition
    def -> do

      -- Get basic polarity from positivity analysis.
      let npars :: Int
    npars = Definition -> Int
    droppedPars Definition
    def
      let pol0 :: [Polarity]
    pol0 = Int -> Polarity -> [Polarity]
    forall a. Int -> a -> [a]
    replicate Int
    npars Polarity
    Nonvariant [Polarity] -> [Polarity] -> [Polarity]
    forall a. [a] -> [a] -> [a]
    ++ (Occurrence -> Polarity) -> [Occurrence] -> [Polarity]
    forall a b. (a -> b) -> [a] -> [b]
    map Occurrence -> Polarity
    polFromOcc (Definition -> [Occurrence]
    defArgOccurrences Definition
    def)
      [Char] -> Int -> [Char] -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "tc.polarity.set" Int
    15 ([Char] -> m ()) -> [Char] -> m ()
    forall a b. (a -> b) -> a -> b
    $
        [Char]
    "Polarity of " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ QName -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow QName
    x [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    " from positivity: " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Polarity] -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow [Polarity]
    pol0

      -- set the polarity in the signature (not the final polarity, though)
      QName -> [Polarity] -> m ()
    forall (m :: * -> *).
    (MonadTCState m, MonadDebug m) =>
    QName -> [Polarity] -> m ()
    setPolarity QName
    x ([Polarity] -> m ()) -> [Polarity] -> m ()
    forall a b. (a -> b) -> a -> b
    $ Int -> [Polarity] -> [Polarity]
    forall a. Int -> [a] -> [a]
    drop Int
    npars [Polarity]
    pol0

    ------------------------------------------------------------------------
    -- * Computing the polarity of a symbol.
    ------------------------------------------------------------------------

    -- | Main function of this module.
    computePolarity
      :: ( HasOptions m, HasConstInfo m, HasBuiltins m
         , MonadTCEnv m, MonadTCState m, MonadReduce m, MonadAddContext m, MonadTCError m
         , MonadDebug m, MonadPretty m )
      => [QName] -> m ()
    computePolarity :: forall (m :: * -> *).
    (HasOptions m, HasConstInfo m, HasBuiltins m, MonadTCEnv m,
     MonadTCState m, MonadReduce m, MonadAddContext m, MonadTCError m,
     MonadDebug m, MonadPretty m) =>
    [QName] -> m ()
    computePolarity [QName]
    xs = do

     -- Andreas, 2017-04-26, issue #2554
     -- First, for mutual definitions, obtain a crude polarity from positivity.
     Bool -> m () -> m ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when ([QName] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [QName]
    xs Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    >= Int
    2) (m () -> m ()) -> m () -> m ()
    forall a b. (a -> b) -> a -> b
    $ (QName -> m ()) -> [QName] -> m ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ QName -> m ()
    forall (m :: * -> *).
    (HasConstInfo m, MonadTCEnv m, MonadTCState m, MonadDebug m) =>
    QName -> m ()
    polarityFromPositivity [QName]
    xs

     -- Then, refine it.
     [QName] -> (QName -> m ()) -> m ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    t a -> (a -> m b) -> m ()
    forM_ [QName]
    xs ((QName -> m ()) -> m ()) -> (QName -> m ()) -> m ()
    forall a b. (a -> b) -> a -> b
    $ \ QName
    x -> QName -> (Definition -> m ()) -> m ()
    forall (m :: * -> *) a.
    (MonadTCEnv m, HasConstInfo m) =>
    QName -> (Definition -> m a) -> m a
    inConcreteOrAbstractMode QName
    x ((Definition -> m ()) -> m ()) -> (Definition -> m ()) -> m ()
    forall a b. (a -> b) -> a -> b
    $ \ Definition
    def -> do
      [Char] -> Int -> [Char] -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "tc.polarity.set" Int
    25 ([Char] -> m ()) -> [Char] -> m ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "Refining polarity of " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ QName -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow QName
    x

      -- Again: get basic polarity from positivity analysis.
      let npars :: Int
    npars = Definition -> Int
    droppedPars Definition
    def
      let pol0 :: [Polarity]
    pol0 = Int -> Polarity -> [Polarity]
    forall a. Int -> a -> [a]
    replicate Int
    npars Polarity
    Nonvariant [Polarity] -> [Polarity] -> [Polarity]
    forall a. [a] -> [a] -> [a]
    ++ (Occurrence -> Polarity) -> [Occurrence] -> [Polarity]
    forall a b. (a -> b) -> [a] -> [b]
    map Occurrence -> Polarity
    polFromOcc (Definition -> [Occurrence]
    defArgOccurrences Definition
    def)
      [Char] -> Int -> [Char] -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "tc.polarity.set" Int
    15 ([Char] -> m ()) -> [Char] -> m ()
    forall a b. (a -> b) -> a -> b
    $
        [Char]
    "Polarity of " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ QName -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow QName
    x [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    " from positivity: " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Polarity] -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow [Polarity]
    pol0

    {-
      -- get basic polarity from shape of def (arguments matched on or not?)
      def      <- getConstInfo x
      let usagePol = usagePolarity $ theDef def
      reportSLn "tc.polarity.set" 15 $ "Polarity of " ++ prettyShow x ++ " from definition form: " ++ prettyShow usagePol
      let n = genericLength usagePol  -- n <- getArity x
      reportSLn "tc.polarity.set" 20 $ "  arity = " ++ show n

      -- refine polarity by positivity information
      pol0 <- zipWith (/\) usagePol <$> mapM getPol [0..n - 1]
      reportSLn "tc.polarity.set" 15 $ "Polarity of " ++ prettyShow x ++ " from positivity: " ++ prettyShow pol0
    -}

      -- compute polarity of sized types
      [Polarity]
    pol1 <- QName -> [Polarity] -> m [Polarity]
    forall (m :: * -> *).
    (HasOptions m, HasConstInfo m, HasBuiltins m, ReadTCState m,
     MonadTCEnv m, MonadTCState m, MonadReduce m, MonadAddContext m,
     MonadTCError m, MonadDebug m, MonadPretty m) =>
    QName -> [Polarity] -> m [Polarity]
    sizePolarity QName
    x [Polarity]
    pol0

      -- refine polarity again by using type information
      let t :: Type
    t = Definition -> Type
    defType Definition
    def
      -- Instantiation takes place in Rules.Decl.instantiateDefinitionType
      -- t <- instantiateFull t -- Andreas, 2014-04-11 Issue 1099: needed for
      --                        -- variable occurrence test in  dependentPolarity.
      [Char] -> Int -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.polarity.set" Int
    15 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
    forall a b. (a -> b) -> a -> b
    $
        TCMT IO Doc
    "Refining polarity with type " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Type -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Type
    t
      [Char] -> Int -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.polarity.set" Int
    60 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
    forall a b. (a -> b) -> a -> b
    $
        TCMT IO Doc
    "Refining polarity with type (raw): " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> ([Char] -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    text ([Char] -> TCMT IO Doc) -> (Type -> [Char]) -> Type -> TCMT IO Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    .Type -> [Char]
    forall a. Show a => a -> [Char]
    show) Type
    t

      [Polarity]
    pol <- Type -> [Polarity] -> [Polarity] -> m [Polarity]
    forall (m :: * -> *).
    (HasOptions m, HasBuiltins m, MonadReduce m, MonadAddContext m,
     MonadDebug m) =>
    Type -> [Polarity] -> [Polarity] -> m [Polarity]
    dependentPolarity Type
    t (Defn -> [Polarity] -> [Polarity]
    enablePhantomTypes (Definition -> Defn
    theDef Definition
    def) [Polarity]
    pol1) [Polarity]
    pol1
      [Char] -> Int -> [Char] -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "tc.polarity.set" Int
    10 ([Char] -> m ()) -> [Char] -> m ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "Polarity of " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ QName -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow QName
    x [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    ": " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Polarity] -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow [Polarity]
    pol

      -- set the polarity in the signature
      QName -> [Polarity] -> m ()
    forall (m :: * -> *).
    (MonadTCState m, MonadDebug m) =>
    QName -> [Polarity] -> m ()
    setPolarity QName
    x ([Polarity] -> m ()) -> [Polarity] -> m ()
    forall a b. (a -> b) -> a -> b
    $ Int -> [Polarity] -> [Polarity]
    forall a. Int -> [a] -> [a]
    drop Int
    npars [Polarity]
    pol -- purgeNonvariant pol -- temporarily disable non-variance

    -- | Data and record parameters are used as phantom arguments all over
    --   the test suite (and possibly in user developments).
    --   @enablePhantomTypes@ turns 'Nonvariant' parameters to 'Covariant'
    --   to enable phantoms.
    enablePhantomTypes :: Defn -> [Polarity] -> [Polarity]
    enablePhantomTypes :: Defn -> [Polarity] -> [Polarity]
    enablePhantomTypes Defn
    def [Polarity]
    pol = case Defn
    def of
      Datatype{ dataPars :: Defn -> Int
    dataPars = Int
    np } -> Int -> [Polarity]
    enable Int
    np
      Record  { recPars :: Defn -> Int
    recPars  = Int
    np } -> Int -> [Polarity]
    enable Int
    np
      Defn
    _                         -> [Polarity]
    pol
      where enable :: Int -> [Polarity]
    enable Int
    np = let ([Polarity]
    pars, [Polarity]
    rest) = Int -> [Polarity] -> ([Polarity], [Polarity])
    forall a. Int -> [a] -> ([a], [a])
    splitAt Int
    np [Polarity]
    pol
                        in  [Polarity] -> [Polarity]
    purgeNonvariant [Polarity]
    pars [Polarity] -> [Polarity] -> [Polarity]
    forall a. [a] -> [a] -> [a]
    ++ [Polarity]
    rest

    {- UNUSED
    -- | Extract a basic approximate polarity info from the shape of definition.
    --   Arguments that are matched against get 'Invariant', others 'Nonvariant'.
    --   For data types, parameters get 'Nonvariant', indices 'Invariant'.
    usagePolarity :: Defn -> [Polarity]
    usagePolarity def = case def of
        Axiom{}                                 -> []
        Function{ funClauses = [] }             -> []
        Function{ funClauses = cs }             -> usage $ map namedClausePats cs
        Datatype{ dataPars = np, dataIxs = ni } -> genericReplicate np Nonvariant
        Record{ recPars = n }                   -> genericReplicate n Nonvariant
        Constructor{}                           -> []
        Primitive{}                             -> []
      where
        usage = foldr1 (zipWith (/\)) . map (map (usagePat . namedArg))
        usagePat VarP{} = Nonvariant
        usagePat DotP{} = Nonvariant
        usagePat ConP{} = Invariant
        usagePat LitP{} = Invariant
    -}

    -- | Make arguments 'Invariant' if the type of a not-'Nonvariant'
    --   later argument depends on it.
    --   Also, enable phantom types by turning 'Nonvariant' into something
    --   else if it is a data/record parameter but not a size argument. [See issue 1596]
    --
    --   Precondition: the "phantom" polarity list has the same length as the polarity list.
    dependentPolarity
      :: (HasOptions m, HasBuiltins m, MonadReduce m, MonadAddContext m, MonadDebug m)
      => Type -> [Polarity] -> [Polarity] -> m [Polarity]
    dependentPolarity :: forall (m :: * -> *).
    (HasOptions m, HasBuiltins m, MonadReduce m, MonadAddContext m,
     MonadDebug m) =>
    Type -> [Polarity] -> [Polarity] -> m [Polarity]
    dependentPolarity Type
    t [Polarity]
    _      []          = [Polarity] -> m [Polarity]
    forall (m :: * -> *) a. Monad m => a -> m a
    return []  -- all remaining are 'Invariant'
    dependentPolarity Type
    t []     (Polarity
    _ : [Polarity]
    _)     = m [Polarity]
    forall a. HasCallStack => a
    __IMPOSSIBLE__
    dependentPolarity Type
    t (Polarity
    q:[Polarity]
    qs) pols :: [Polarity]
    pols@(Polarity
    p:[Polarity]
    ps) = do
      Term
    t <- Term -> m Term
    forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
    reduce (Term -> m Term) -> Term -> m Term
    forall a b. (a -> b) -> a -> b
    $ Type -> Term
    forall t a. Type'' t a -> a
    unEl Type
    t
      [Char] -> Int -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.polarity.dep" Int
    20 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "dependentPolarity t = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Term
    t
      [Char] -> Int -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.polarity.dep" Int
    70 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "dependentPolarity t = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> ([Char] -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    text ([Char] -> TCMT IO Doc) -> (Term -> [Char]) -> Term -> TCMT IO Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Term -> [Char]
    forall a. Show a => a -> [Char]
    show) Term
    t
      case Term
    t of
        Pi Dom Type
    dom Abs Type
    b -> do
          [Polarity]
    ps <- Dom Type -> Abs Type -> (Type -> m [Polarity]) -> m [Polarity]
    forall a (m :: * -> *) b.
    (Subst a, MonadAddContext m) =>
    Dom Type -> Abs a -> (a -> m b) -> m b
    underAbstraction Dom Type
    dom Abs Type
    b ((Type -> m [Polarity]) -> m [Polarity])
    -> (Type -> m [Polarity]) -> m [Polarity]
    forall a b. (a -> b) -> a -> b
    $ \ Type
    c -> Type -> [Polarity] -> [Polarity] -> m [Polarity]
    forall (m :: * -> *).
    (HasOptions m, HasBuiltins m, MonadReduce m, MonadAddContext m,
     MonadDebug m) =>
    Type -> [Polarity] -> [Polarity] -> m [Polarity]
    dependentPolarity Type
    c [Polarity]
    qs [Polarity]
    ps
          let fallback :: m Polarity
    fallback = m Bool -> m Polarity -> m Polarity -> m Polarity
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
    ifM (Maybe BoundedSize -> Bool
    forall a. Maybe a -> Bool
    isJust (Maybe BoundedSize -> Bool) -> m (Maybe BoundedSize) -> m Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Type -> m (Maybe BoundedSize)
    forall a (m :: * -> *).
    (IsSizeType a, HasOptions m, HasBuiltins m) =>
    a -> m (Maybe BoundedSize)
    isSizeType (Dom Type -> Type
    forall t e. Dom' t e -> e
    unDom Dom Type
    dom)) (Polarity -> m Polarity
    forall (m :: * -> *) a. Monad m => a -> m a
    return Polarity
    p) (Polarity -> m Polarity
    forall (m :: * -> *) a. Monad m => a -> m a
    return Polarity
    q)
          Polarity
    p <- case Abs Type
    b of
            Abs{} | Polarity
    p Polarity -> Polarity -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Polarity
    Invariant  ->
              -- Andreas, 2014-04-11 see Issue 1099
              -- Free variable analysis is not in the monad,
              -- hence metas must have been instantiated before!
              m Bool -> m Polarity -> m Polarity -> m Polarity
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
    ifM (Int -> Type -> [Polarity] -> m Bool
    forall (m :: * -> *).
    MonadReduce m =>
    Int -> Type -> [Polarity] -> m Bool
    relevantInIgnoringNonvariant Int
    0 (Abs Type -> Type
    forall a. Subst a => Abs a -> a
    absBody Abs Type
    b) [Polarity]
    ps)
                {- then -} (Polarity -> m Polarity
    forall (m :: * -> *) a. Monad m => a -> m a
    return Polarity
    Invariant)
                {- else -} m Polarity
    fallback
            Abs Type
    _ -> m Polarity
    fallback
          [Polarity] -> m [Polarity]
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([Polarity] -> m [Polarity]) -> [Polarity] -> m [Polarity]
    forall a b. (a -> b) -> a -> b
    $ Polarity
    p Polarity -> [Polarity] -> [Polarity]
    forall a. a -> [a] -> [a]
    : [Polarity]
    ps
        Term
    _ -> [Polarity] -> m [Polarity]
    forall (m :: * -> *) a. Monad m => a -> m a
    return [Polarity]
    pols

    -- | Check whether a variable is relevant in a type expression,
    --   ignoring domains of non-variant arguments.
    relevantInIgnoringNonvariant :: MonadReduce m => Nat -> Type -> [Polarity] -> m Bool
    relevantInIgnoringNonvariant :: forall (m :: * -> *).
    MonadReduce m =>
    Int -> Type -> [Polarity] -> m Bool
    relevantInIgnoringNonvariant Int
    i Type
    t []     = Bool -> m Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Bool -> m Bool) -> Bool -> m Bool
    forall a b. (a -> b) -> a -> b
    $ Int
    i Int -> Type -> Bool
    forall t. Free t => Int -> t -> Bool
    `relevantInIgnoringSortAnn` Type
    t
    relevantInIgnoringNonvariant Int
    i Type
    t (Polarity
    p:[Polarity]
    ps) =
      Type
    -> (Type -> m Bool) -> (Dom Type -> Abs Type -> m Bool) -> m Bool
    forall (m :: * -> *) a.
    MonadReduce m =>
    Type -> (Type -> m a) -> (Dom Type -> Abs Type -> m a) -> m a
    ifNotPiType Type
    t
        {-then-} (\ Type
    t -> Bool -> m Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Bool -> m Bool) -> Bool -> m Bool
    forall a b. (a -> b) -> a -> b
    $ Int
    i Int -> Type -> Bool
    forall t. Free t => Int -> t -> Bool
    `relevantInIgnoringSortAnn` Type
    t) ((Dom Type -> Abs Type -> m Bool) -> m Bool)
    -> (Dom Type -> Abs Type -> m Bool) -> m Bool
    forall a b. (a -> b) -> a -> b
    $
        {-else-} \ Dom Type
    a Abs Type
    b ->
          if Polarity
    p Polarity -> Polarity -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Polarity
    Nonvariant Bool -> Bool -> Bool
    && Int
    i Int -> Dom Type -> Bool
    forall t. Free t => Int -> t -> Bool
    `relevantInIgnoringSortAnn` Dom Type
    a
            then Bool -> m Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    True
            else Int -> Type -> [Polarity] -> m Bool
    forall (m :: * -> *).
    MonadReduce m =>
    Int -> Type -> [Polarity] -> m Bool
    relevantInIgnoringNonvariant (Int
    i Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    1) (Abs Type -> Type
    forall a. Subst a => Abs a -> a
    absBody Abs Type
    b) [Polarity]
    ps

    ------------------------------------------------------------------------
    -- * Sized types
    ------------------------------------------------------------------------

    -- | Hack for polarity of size indices.
    --   As a side effect, this sets the positivity of the size index.
    --   See test/succeed/PolaritySizeSucData.agda for a case where this is needed.
    sizePolarity
      :: forall m .
         ( HasOptions m, HasConstInfo m, HasBuiltins m, ReadTCState m
         , MonadTCEnv m, MonadTCState m, MonadReduce m, MonadAddContext m, MonadTCError m
         , MonadDebug m, MonadPretty m )
      => QName -> [Polarity] -> m [Polarity]
    sizePolarity :: forall (m :: * -> *).
    (HasOptions m, HasConstInfo m, HasBuiltins m, ReadTCState m,
     MonadTCEnv m, MonadTCState m, MonadReduce m, MonadAddContext m,
     MonadTCError m, MonadDebug m, MonadPretty m) =>
    QName -> [Polarity] -> m [Polarity]
    sizePolarity QName
    d [Polarity]
    pol0 = do
      let exit :: m [Polarity]
    exit = [Polarity] -> m [Polarity]
    forall (m :: * -> *) a. Monad m => a -> m a
    return [Polarity]
    pol0
      m Bool -> m [Polarity] -> m [Polarity] -> m [Polarity]
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
    ifNotM m Bool
    forall (m :: * -> *). HasOptions m => m Bool
    sizedTypesOption m [Polarity]
    exit (m [Polarity] -> m [Polarity]) -> m [Polarity] -> m [Polarity]
    forall a b. (a -> b) -> a -> b
    $ {- else -} do
        Definition
    def <- QName -> m Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    d
        case Definition -> Defn
    theDef Definition
    def of
          Datatype{ dataPars :: Defn -> Int
    dataPars = Int
    np, dataCons :: Defn -> [QName]
    dataCons = [QName]
    cons } -> do
            let TelV Tele (Dom Type)
    tel Type
    _      = Type -> TelV Type
    telView' (Type -> TelV Type) -> Type -> TelV Type
    forall a b. (a -> b) -> a -> b
    $ Definition -> Type
    defType Definition
    def
                ([Dom ([Char], Type)]
    parTel, [Dom ([Char], Type)]
    ixTel) = Int
    -> [Dom ([Char], Type)]
    -> ([Dom ([Char], Type)], [Dom ([Char], Type)])
    forall a. Int -> [a] -> ([a], [a])
    splitAt Int
    np ([Dom ([Char], Type)]
     -> ([Dom ([Char], Type)], [Dom ([Char], Type)]))
    -> [Dom ([Char], Type)]
    -> ([Dom ([Char], Type)], [Dom ([Char], Type)])
    forall a b. (a -> b) -> a -> b
    $ Tele (Dom Type) -> [Dom ([Char], Type)]
    forall t. Tele (Dom t) -> [Dom ([Char], t)]
    telToList Tele (Dom Type)
    tel
            case [Dom ([Char], Type)]
    ixTel of
              []                 -> m [Polarity]
    exit  -- No size index
              Dom{unDom :: forall t e. Dom' t e -> e
    unDom = ([Char]
    _,Type
    a)} : [Dom ([Char], Type)]
    _ -> m Bool -> m [Polarity] -> m [Polarity] -> m [Polarity]
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
    ifM ((Maybe BoundedSize -> Maybe BoundedSize -> Bool
    forall a. Eq a => a -> a -> Bool
    /= BoundedSize -> Maybe BoundedSize
    forall a. a -> Maybe a
    Just BoundedSize
    BoundedNo) (Maybe BoundedSize -> Bool) -> m (Maybe BoundedSize) -> m Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Type -> m (Maybe BoundedSize)
    forall a (m :: * -> *).
    (IsSizeType a, HasOptions m, HasBuiltins m) =>
    a -> m (Maybe BoundedSize)
    isSizeType Type
    a) m [Polarity]
    exit (m [Polarity] -> m [Polarity]) -> m [Polarity] -> m [Polarity]
    forall a b. (a -> b) -> a -> b
    $ do
                -- we assume the size index to be 'Covariant' ...
                let pol :: [Polarity]
    pol   = Int -> [Polarity] -> [Polarity]
    forall a. Int -> [a] -> [a]
    take Int
    np [Polarity]
    pol0
                    polCo :: [Polarity]
    polCo = [Polarity]
    pol [Polarity] -> [Polarity] -> [Polarity]
    forall a. [a] -> [a] -> [a]
    ++ [Polarity
    Covariant]
                    polIn :: [Polarity]
    polIn = [Polarity]
    pol [Polarity] -> [Polarity] -> [Polarity]
    forall a. [a] -> [a] -> [a]
    ++ [Polarity
    Invariant]
                QName -> [Polarity] -> m ()
    forall (m :: * -> *).
    (MonadTCState m, MonadDebug m) =>
    QName -> [Polarity] -> m ()
    setPolarity QName
    d ([Polarity] -> m ()) -> [Polarity] -> m ()
    forall a b. (a -> b) -> a -> b
    $ [Polarity]
    polCo
                -- and seek confirm it by looking at the constructor types
                let check :: QName -> m Bool
                    check :: QName -> m Bool
    check QName
    c = do
                      Type
    t <- Definition -> Type
    defType (Definition -> Type) -> m Definition -> m Type
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> m Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    c
                      Tele (Dom Type) -> m Bool -> m Bool
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext ([Dom ([Char], Type)] -> Tele (Dom Type)
    telFromList [Dom ([Char], Type)]
    parTel) (m Bool -> m Bool) -> m Bool -> m Bool
    forall a b. (a -> b) -> a -> b
    $ do
                        let pars :: [Arg Term]
    pars = (Int -> Arg Term) -> [Int] -> [Arg Term]
    forall a b. (a -> b) -> [a] -> [b]
    map (Term -> Arg Term
    forall a. a -> Arg a
    defaultArg (Term -> Arg Term) -> (Int -> Term) -> Int -> Arg Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Int -> Term
    var) ([Int] -> [Arg Term]) -> [Int] -> [Arg Term]
    forall a b. (a -> b) -> a -> b
    $ Int -> [Int]
    forall a. Integral a => a -> [a]
    downFrom Int
    np
                        TelV Tele (Dom Type)
    conTel Type
    target <- Type -> m (TelV Type)
    forall (m :: * -> *).
    (MonadReduce m, MonadAddContext m) =>
    Type -> m (TelV Type)
    telView (Type -> m (TelV Type)) -> m Type -> m (TelV Type)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< (Type
    t Type -> [Arg Term] -> m Type
    forall a (m :: * -> *).
    (PiApplyM a, MonadReduce m, HasBuiltins m) =>
    Type -> a -> m Type
    `piApplyM` [Arg Term]
    pars)
                        Type -> Tele (Dom Type) -> m Bool
    loop Type
    target Tele (Dom Type)
    conTel
                      where
                      loop :: Type -> Telescope -> m Bool
                      -- no suitable size argument
                      loop :: Type -> Tele (Dom Type) -> m Bool
    loop Type
    _ Tele (Dom Type)
    EmptyTel = do
                        [Char] -> Int -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.polarity.size" Int
    15 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
    forall a b. (a -> b) -> a -> b
    $
                          TCMT IO Doc
    "constructor" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> QName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM QName
    c TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> TCMT IO Doc
    "fails size polarity check"
                        Bool -> m Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False

                      -- try argument @dom@
                      loop Type
    target (ExtendTel Dom Type
    dom Abs (Tele (Dom Type))
    tel) = do
                        Maybe BoundedSize
    isSz <- Dom Type -> m (Maybe BoundedSize)
    forall a (m :: * -> *).
    (IsSizeType a, HasOptions m, HasBuiltins m) =>
    a -> m (Maybe BoundedSize)
    isSizeType Dom Type
    dom
                        Dom Type
    -> Abs (Tele (Dom Type)) -> (Tele (Dom Type) -> m Bool) -> m Bool
    forall a (m :: * -> *) b.
    (Subst a, MonadAddContext m) =>
    Dom Type -> Abs a -> (a -> m b) -> m b
    underAbstraction Dom Type
    dom Abs (Tele (Dom Type))
    tel ((Tele (Dom Type) -> m Bool) -> m Bool)
    -> (Tele (Dom Type) -> m Bool) -> m Bool
    forall a b. (a -> b) -> a -> b
    $ \ Tele (Dom Type)
    tel -> do
                          let continue :: m Bool
    continue = Type -> Tele (Dom Type) -> m Bool
    loop Type
    target Tele (Dom Type)
    tel

                          -- check that dom == Size
                          if Maybe BoundedSize
    isSz Maybe BoundedSize -> Maybe BoundedSize -> Bool
    forall a. Eq a => a -> a -> Bool
    /= BoundedSize -> Maybe BoundedSize
    forall a. a -> Maybe a
    Just BoundedSize
    BoundedNo then m Bool
    continue else do

                            -- check that the size argument appears in the
                            -- right spot in the target type
                            let sizeArg :: Int
    sizeArg = Tele (Dom Type) -> Int
    forall a. Sized a => a -> Int
    size Tele (Dom Type)
    tel
                            Bool
    isLin <- Tele (Dom Type) -> m Bool -> m Bool
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext Tele (Dom Type)
    tel (m Bool -> m Bool) -> m Bool -> m Bool
    forall a b. (a -> b) -> a -> b
    $ QName -> Int -> Type -> m Bool
    forall (m :: * -> *).
    (HasConstInfo m, ReadTCState m, MonadDebug m, MonadPretty m,
     MonadTCError m) =>
    QName -> Int -> Type -> m Bool
    checkSizeIndex QName
    d Int
    sizeArg Type
    target
                            if Bool -> Bool
    not Bool
    isLin then m Bool
    continue else do

                              -- check that only positive occurences in tel
                              [Polarity]
    pols <- (Int -> Type -> m Polarity) -> [Int] -> [Type] -> m [Polarity]
    forall (m :: * -> *) a b c.
    Applicative m =>
    (a -> b -> m c) -> [a] -> [b] -> m [c]
    zipWithM Int -> Type -> m Polarity
    forall a (m :: * -> *).
    (HasPolarity a, HasConstInfo m, MonadReduce m) =>
    Int -> a -> m Polarity
    polarity [Int
    0..] ([Type] -> m [Polarity]) -> [Type] -> m [Polarity]
    forall a b. (a -> b) -> a -> b
    $ (Dom ([Char], Type) -> Type) -> [Dom ([Char], Type)] -> [Type]
    forall a b. (a -> b) -> [a] -> [b]
    map (([Char], Type) -> Type
    forall a b. (a, b) -> b
    snd (([Char], Type) -> Type)
    -> (Dom ([Char], Type) -> ([Char], Type))
    -> Dom ([Char], Type)
    -> Type
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Dom ([Char], Type) -> ([Char], Type)
    forall t e. Dom' t e -> e
    unDom) ([Dom ([Char], Type)] -> [Type]) -> [Dom ([Char], Type)] -> [Type]
    forall a b. (a -> b) -> a -> b
    $ Tele (Dom Type) -> [Dom ([Char], Type)]
    forall t. Tele (Dom t) -> [Dom ([Char], t)]
    telToList Tele (Dom Type)
    tel
                              [Char] -> Int -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.polarity.size" Int
    25 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
    forall a b. (a -> b) -> a -> b
    $
                                [Char] -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    text ([Char] -> TCMT IO Doc) -> [Char] -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "to pass size polarity check, the following polarities need all to be covariant: " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Polarity] -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow [Polarity]
    pols
                              if (Polarity -> Bool) -> [Polarity] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    any (Polarity -> [Polarity] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `notElem` [Polarity
    Nonvariant, Polarity
    Covariant]) [Polarity]
    pols then m Bool
    continue else do
                                [Char] -> Int -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.polarity.size" Int
    15 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
    forall a b. (a -> b) -> a -> b
    $
                                  TCMT IO Doc
    "constructor" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> QName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM QName
    c TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> TCMT IO Doc
    "passes size polarity check"
                                Bool -> m Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    True

                m Bool -> m [Polarity] -> m [Polarity] -> m [Polarity]
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
    ifNotM ([m Bool] -> m Bool
    forall (f :: * -> *) (m :: * -> *).
    (Foldable f, Monad m) =>
    f (m Bool) -> m Bool
    andM ([m Bool] -> m Bool) -> [m Bool] -> m Bool
    forall a b. (a -> b) -> a -> b
    $ (QName -> m Bool) -> [QName] -> [m Bool]
    forall a b. (a -> b) -> [a] -> [b]
    map QName -> m Bool
    check [QName]
    cons)
                    ([Polarity] -> m [Polarity]
    forall (m :: * -> *) a. Monad m => a -> m a
    return [Polarity]
    polIn) -- no, does not conform to the rules of sized types
                  (m [Polarity] -> m [Polarity]) -> m [Polarity] -> m [Polarity]
    forall a b. (a -> b) -> a -> b
    $ do  -- yes, we have a sized type here
                    -- Andreas, 2015-07-01
                    -- As a side effect, mark the size also covariant for subsequent
                    -- positivity checking (which feeds back into polarity analysis).
                    QName -> ([Occurrence] -> [Occurrence]) -> m ()
    forall (m :: * -> *).
    MonadTCState m =>
    QName -> ([Occurrence] -> [Occurrence]) -> m ()
    modifyArgOccurrences QName
    d (([Occurrence] -> [Occurrence]) -> m ())
    -> ([Occurrence] -> [Occurrence]) -> m ()
    forall a b. (a -> b) -> a -> b
    $ \ [Occurrence]
    occ -> Int -> [Occurrence] -> [Occurrence]
    forall a. Int -> [a] -> [a]
    take Int
    np [Occurrence]
    occ [Occurrence] -> [Occurrence] -> [Occurrence]
    forall a. [a] -> [a] -> [a]
    ++ [Occurrence
    JustPos]
                    [Polarity] -> m [Polarity]
    forall (m :: * -> *) a. Monad m => a -> m a
    return [Polarity]
    polCo
          Defn
    _ -> m [Polarity]
    exit

    -- | @checkSizeIndex d i a@ checks that constructor target type @a@
    --   has form @d ps (↑ⁿ i) idxs@ where @|ps| = np(d)@.
    --
    --   Precondition: @a@ is reduced and of form @d ps idxs0@.
    checkSizeIndex
      :: (HasConstInfo m, ReadTCState m, MonadDebug m, MonadPretty m, MonadTCError m)
      => QName -> Nat -> Type -> m Bool
    checkSizeIndex :: forall (m :: * -> *).
    (HasConstInfo m, ReadTCState m, MonadDebug m, MonadPretty m,
     MonadTCError m) =>
    QName -> Int -> Type -> m Bool
    checkSizeIndex QName
    d Int
    i Type
    a = do
      [Char] -> Int -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.polarity.size" Int
    15 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *) a. ReadTCState m => m a -> m a
    withShowAllArguments (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat
        [ TCMT IO Doc
    "checking that constructor target type " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Type -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Type
    a
        , TCMT IO Doc
    "  is data type " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> QName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM QName
    d
        , TCMT IO Doc
    "  and has size index (successor(s) of) " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM (Int -> Term
    var Int
    i)
        ]
      case Type -> Term
    forall t a. Type'' t a -> a
    unEl Type
    a of
        Def QName
    d0 [Elim]
    es -> do
          m (Maybe QName) -> m () -> m ()
    forall (m :: * -> *) a. Monad m => m (Maybe a) -> m () -> m ()
    whenNothingM (QName -> QName -> m (Maybe QName)
    forall (m :: * -> *).
    HasConstInfo m =>
    QName -> QName -> m (Maybe QName)
    sameDef QName
    d QName
    d0) m ()
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          Int
    np <- Int -> Maybe Int -> Int
    forall a. a -> Maybe a -> a
    fromMaybe Int
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe Int -> Int) -> m (Maybe Int) -> m Int
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> m (Maybe Int)
    forall (m :: * -> *). HasConstInfo m => QName -> m (Maybe Int)
    getNumberOfParameters QName
    d0
          let ([Elim]
    pars, Apply Arg Term
    ix : [Elim]
    ixs) = Int -> [Elim] -> ([Elim], [Elim])
    forall a. Int -> [a] -> ([a], [a])
    splitAt Int
    np [Elim]
    es
          DeepSizeView
    s <- Term -> m DeepSizeView
    forall (m :: * -> *).
    (PureTCM m, MonadTCError m) =>
    Term -> m DeepSizeView
    deepSizeView (Term -> m DeepSizeView) -> Term -> m DeepSizeView
    forall a b. (a -> b) -> a -> b
    $ Arg Term -> Term
    forall e. Arg e -> e
    unArg Arg Term
    ix
          case DeepSizeView
    s of
            DSizeVar (ProjectedVar Int
    j []) Int
    _ | Int
    i Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    j
              -> Bool -> m Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Bool -> m Bool) -> Bool -> m Bool
    forall a b. (a -> b) -> a -> b
    $ Bool -> Bool
    not (Bool -> Bool) -> Bool -> Bool
    forall a b. (a -> b) -> a -> b
    $ Int -> [Elim] -> Bool
    forall t. Free t => Int -> t -> Bool
    freeIn Int
    i ([Elim]
    pars [Elim] -> [Elim] -> [Elim]
    forall a. [a] -> [a] -> [a]
    ++ [Elim]
    ixs)
            DeepSizeView
    _ -> Bool -> m Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False
        Term
    _ -> m Bool
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    -- | @polarity i a@ computes the least polarity of de Bruijn index @i@
    --   in syntactic entity @a@.
    polarity
      :: (HasPolarity a, HasConstInfo m, MonadReduce m)
      => Nat -> a -> m Polarity
    polarity :: forall a (m :: * -> *).
    (HasPolarity a, HasConstInfo m, MonadReduce m) =>
    Int -> a -> m Polarity
    polarity Int
    i a
    x = LeastPolarity m -> m Polarity
    forall (m :: * -> *). LeastPolarity m -> m Polarity
    getLeastPolarity (LeastPolarity m -> m Polarity) -> LeastPolarity m -> m Polarity
    forall a b. (a -> b) -> a -> b
    $ Int -> Polarity -> a -> LeastPolarity m
    forall a (m :: * -> *).
    (HasPolarity a, HasConstInfo m, MonadReduce m) =>
    Int -> Polarity -> a -> LeastPolarity m
    polarity' Int
    i Polarity
    Covariant a
    x

    -- | A monoid for lazily computing the infimum of the polarities of a variable in some object.
    -- Allows short-cutting.

    newtype LeastPolarity m = LeastPolarity { forall (m :: * -> *). LeastPolarity m -> m Polarity
    getLeastPolarity :: m Polarity}

    instance Monad m => Singleton Polarity (LeastPolarity m) where
      singleton :: Polarity -> LeastPolarity m
    singleton = m Polarity -> LeastPolarity m
    forall (m :: * -> *). m Polarity -> LeastPolarity m
    LeastPolarity (m Polarity -> LeastPolarity m)
    -> (Polarity -> m Polarity) -> Polarity -> LeastPolarity m
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Polarity -> m Polarity
    forall (m :: * -> *) a. Monad m => a -> m a
    return

    instance Monad m => Semigroup (LeastPolarity m) where
      LeastPolarity m Polarity
    mp <> :: LeastPolarity m -> LeastPolarity m -> LeastPolarity m
    <> LeastPolarity m Polarity
    mq = m Polarity -> LeastPolarity m
    forall (m :: * -> *). m Polarity -> LeastPolarity m
    LeastPolarity (m Polarity -> LeastPolarity m) -> m Polarity -> LeastPolarity m
    forall a b. (a -> b) -> a -> b
    $ do
        m Polarity
    mp m Polarity -> (Polarity -> m Polarity) -> m Polarity
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
          Polarity
    Invariant  -> Polarity -> m Polarity
    forall (m :: * -> *) a. Monad m => a -> m a
    return Polarity
    Invariant  -- Shortcut for the absorbing element.
          Polarity
    Nonvariant -> m Polarity
    mq                -- The neutral element.
          Polarity
    p          -> (Polarity
    p Polarity -> Polarity -> Polarity
    /\) (Polarity -> Polarity) -> m Polarity -> m Polarity
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m Polarity
    mq

    instance Monad m => Monoid (LeastPolarity m) where
      mempty :: LeastPolarity m
    mempty  = Polarity -> LeastPolarity m
    forall el coll. Singleton el coll => el -> coll
    singleton Polarity
    Nonvariant
      mappend :: LeastPolarity m -> LeastPolarity m -> LeastPolarity m
    mappend = LeastPolarity m -> LeastPolarity m -> LeastPolarity m
    forall a. Semigroup a => a -> a -> a
    (<>)

    -- | Bind for 'LeastPolarity'.
    (>>==) :: Monad m => m a -> (a -> LeastPolarity m) -> LeastPolarity m
    m a
    m >>== :: forall (m :: * -> *) a.
    Monad m =>
    m a -> (a -> LeastPolarity m) -> LeastPolarity m
    >>== a -> LeastPolarity m
    k = m Polarity -> LeastPolarity m
    forall (m :: * -> *). m Polarity -> LeastPolarity m
    LeastPolarity (m Polarity -> LeastPolarity m) -> m Polarity -> LeastPolarity m
    forall a b. (a -> b) -> a -> b
    $ m a
    m m a -> (a -> m Polarity) -> m Polarity
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= LeastPolarity m -> m Polarity
    forall (m :: * -> *). LeastPolarity m -> m Polarity
    getLeastPolarity (LeastPolarity m -> m Polarity)
    -> (a -> LeastPolarity m) -> a -> m Polarity
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . a -> LeastPolarity m
    k

    -- | @polarity' i p a@ computes the least polarity of de Bruijn index @i@
    --   in syntactic entity @a@, where root occurrences count as @p@.
    --
    --   Ignores occurrences in sorts.
    class HasPolarity a where
      polarity'
        :: (HasConstInfo m, MonadReduce m)
        => Nat -> Polarity -> a -> LeastPolarity m

      default polarity'
        :: (HasConstInfo m, MonadReduce m, HasPolarity b, Foldable t, t b ~ a)
        => Nat -> Polarity -> a -> LeastPolarity m
      polarity' Int
    i = (b -> LeastPolarity m) -> t b -> LeastPolarity m
    forall (t :: * -> *) m a.
    (Foldable t, Monoid m) =>
    (a -> m) -> t a -> m
    foldMap ((b -> LeastPolarity m) -> t b -> LeastPolarity m)
    -> (Polarity -> b -> LeastPolarity m)
    -> Polarity
    -> t b
    -> LeastPolarity m
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Int -> Polarity -> b -> LeastPolarity m
    forall a (m :: * -> *).
    (HasPolarity a, HasConstInfo m, MonadReduce m) =>
    Int -> Polarity -> a -> LeastPolarity m
    polarity' Int
    i

    instance HasPolarity a => HasPolarity [a]
    instance HasPolarity a => HasPolarity (Arg a)
    instance HasPolarity a => HasPolarity (Dom a)
    instance HasPolarity a => HasPolarity (Elim' a)
    instance HasPolarity a => HasPolarity (Level' a)
    instance HasPolarity a => HasPolarity (PlusLevel' a)

    -- | Does not look into sort.
    instance HasPolarity a => HasPolarity (Type'' t a)

    instance (HasPolarity a, HasPolarity b) => HasPolarity (a, b) where
      polarity' :: forall (m :: * -> *).
    (HasConstInfo m, MonadReduce m) =>
    Int -> Polarity -> (a, b) -> LeastPolarity m
    polarity' Int
    i Polarity
    p (a
    x, b
    y) = Int -> Polarity -> a -> LeastPolarity m
    forall a (m :: * -> *).
    (HasPolarity a, HasConstInfo m, MonadReduce m) =>
    Int -> Polarity -> a -> LeastPolarity m
    polarity' Int
    i Polarity
    p a
    x LeastPolarity m -> LeastPolarity m -> LeastPolarity m
    forall a. Semigroup a => a -> a -> a
    <> Int -> Polarity -> b -> LeastPolarity m
    forall a (m :: * -> *).
    (HasPolarity a, HasConstInfo m, MonadReduce m) =>
    Int -> Polarity -> a -> LeastPolarity m
    polarity' Int
    i Polarity
    p b
    y

    instance HasPolarity a => HasPolarity (Abs a) where
      polarity' :: forall (m :: * -> *).
    (HasConstInfo m, MonadReduce m) =>
    Int -> Polarity -> Abs a -> LeastPolarity m
    polarity' Int
    i Polarity
    p (Abs   [Char]
    _ a
    b) = Int -> Polarity -> a -> LeastPolarity m
    forall a (m :: * -> *).
    (HasPolarity a, HasConstInfo m, MonadReduce m) =>
    Int -> Polarity -> a -> LeastPolarity m
    polarity' (Int
    i Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    1) Polarity
    p a
    b
      polarity' Int
    i Polarity
    p (NoAbs [Char]
    _ a
    v) = Int -> Polarity -> a -> LeastPolarity m
    forall a (m :: * -> *).
    (HasPolarity a, HasConstInfo m, MonadReduce m) =>
    Int -> Polarity -> a -> LeastPolarity m
    polarity' Int
    i Polarity
    p a
    v

    instance HasPolarity Term where
      polarity' :: forall (m :: * -> *).
    (HasConstInfo m, MonadReduce m) =>
    Int -> Polarity -> Term -> LeastPolarity m
    polarity' Int
    i Polarity
    p Term
    v = Term -> m Term
    forall a (m :: * -> *). (Instantiate a, MonadReduce m) => a -> m a
    instantiate Term
    v m Term -> (Term -> LeastPolarity m) -> LeastPolarity m
    forall (m :: * -> *) a.
    Monad m =>
    m a -> (a -> LeastPolarity m) -> LeastPolarity m
    >>== \case
        -- Andreas, 2012-09-06: taking the polarity' of the arguments
        -- without taking the variance of the function into account seems wrong.
        Var Int
    n [Elim]
    ts
          | Int
    n Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    i    -> Polarity -> LeastPolarity m
    forall el coll. Singleton el coll => el -> coll
    singleton Polarity
    p LeastPolarity m -> LeastPolarity m -> LeastPolarity m
    forall a. Semigroup a => a -> a -> a
    <> Int -> Polarity -> [Elim] -> LeastPolarity m
    forall a (m :: * -> *).
    (HasPolarity a, HasConstInfo m, MonadReduce m) =>
    Int -> Polarity -> a -> LeastPolarity m
    polarity' Int
    i Polarity
    Invariant [Elim]
    ts
          | Bool
    otherwise -> Int -> Polarity -> [Elim] -> LeastPolarity m
    forall a (m :: * -> *).
    (HasPolarity a, HasConstInfo m, MonadReduce m) =>
    Int -> Polarity -> a -> LeastPolarity m
    polarity' Int
    i Polarity
    Invariant [Elim]
    ts
        Lam ArgInfo
    _ Abs Term
    t       -> Int -> Polarity -> Abs Term -> LeastPolarity m
    forall a (m :: * -> *).
    (HasPolarity a, HasConstInfo m, MonadReduce m) =>
    Int -> Polarity -> a -> LeastPolarity m
    polarity' Int
    i Polarity
    p Abs Term
    t
        Lit Literal
    _         -> LeastPolarity m
    forall a. Monoid a => a
    mempty
        Level Level
    l       -> Int -> Polarity -> Level -> LeastPolarity m
    forall a (m :: * -> *).
    (HasPolarity a, HasConstInfo m, MonadReduce m) =>
    Int -> Polarity -> a -> LeastPolarity m
    polarity' Int
    i Polarity
    p Level
    l
        Def QName
    x [Elim]
    ts      -> QName -> m [Polarity]
    forall (m :: * -> *). HasConstInfo m => QName -> m [Polarity]
    getPolarity QName
    x m [Polarity] -> ([Polarity] -> LeastPolarity m) -> LeastPolarity m
    forall (m :: * -> *) a.
    Monad m =>
    m a -> (a -> LeastPolarity m) -> LeastPolarity m
    >>== \ [Polarity]
    pols ->
                           let ps :: [Polarity]
    ps = (Polarity -> Polarity) -> [Polarity] -> [Polarity]
    forall a b. (a -> b) -> [a] -> [b]
    map (Polarity -> Polarity -> Polarity
    composePol Polarity
    p) [Polarity]
    pols [Polarity] -> [Polarity] -> [Polarity]
    forall a. [a] -> [a] -> [a]
    ++ Polarity -> [Polarity]
    forall a. a -> [a]
    repeat Polarity
    Invariant
                           in  [LeastPolarity m] -> LeastPolarity m
    forall a. Monoid a => [a] -> a
    mconcat ([LeastPolarity m] -> LeastPolarity m)
    -> [LeastPolarity m] -> LeastPolarity m
    forall a b. (a -> b) -> a -> b
    $ (Polarity -> Elim -> LeastPolarity m)
    -> [Polarity] -> [Elim] -> [LeastPolarity m]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith (Int -> Polarity -> Elim -> LeastPolarity m
    forall a (m :: * -> *).
    (HasPolarity a, HasConstInfo m, MonadReduce m) =>
    Int -> Polarity -> a -> LeastPolarity m
    polarity' Int
    i) [Polarity]
    ps [Elim]
    ts
        Con ConHead
    _ ConInfo
    _ [Elim]
    ts    -> Int -> Polarity -> [Elim] -> LeastPolarity m
    forall a (m :: * -> *).
    (HasPolarity a, HasConstInfo m, MonadReduce m) =>
    Int -> Polarity -> a -> LeastPolarity m
    polarity' Int
    i Polarity
    p [Elim]
    ts   -- Constructors can be seen as monotone in all args.
        Pi Dom Type
    a Abs Type
    b        -> Int -> Polarity -> Dom Type -> LeastPolarity m
    forall a (m :: * -> *).
    (HasPolarity a, HasConstInfo m, MonadReduce m) =>
    Int -> Polarity -> a -> LeastPolarity m
    polarity' Int
    i (Polarity -> Polarity
    neg Polarity
    p) Dom Type
    a LeastPolarity m -> LeastPolarity m -> LeastPolarity m
    forall a. Semigroup a => a -> a -> a
    <> Int -> Polarity -> Abs Type -> LeastPolarity m
    forall a (m :: * -> *).
    (HasPolarity a, HasConstInfo m, MonadReduce m) =>
    Int -> Polarity -> a -> LeastPolarity m
    polarity' Int
    i Polarity
    p Abs Type
    b
        Sort Sort
    s        -> LeastPolarity m
    forall a. Monoid a => a
    mempty -- polarity' i p s -- mempty
        MetaV MetaId
    _ [Elim]
    ts    -> Int -> Polarity -> [Elim] -> LeastPolarity m
    forall a (m :: * -> *).
    (HasPolarity a, HasConstInfo m, MonadReduce m) =>
    Int -> Polarity -> a -> LeastPolarity m
    polarity' Int
    i Polarity
    Invariant [Elim]
    ts
        DontCare Term
    t    -> Int -> Polarity -> Term -> LeastPolarity m
    forall a (m :: * -> *).
    (HasPolarity a, HasConstInfo m, MonadReduce m) =>
    Int -> Polarity -> a -> LeastPolarity m
    polarity' Int
    i Polarity
    p Term
    t -- mempty
        Dummy{}       -> LeastPolarity m
    forall a. Monoid a => a
    mempty