    {-# LANGUAGE PatternSynonyms #-}

    {-| Functions for inserting implicit arguments at the right places.
    -}
    module Agda.TypeChecking.Implicit where

    import Control.Monad
    import Control.Monad.Except
    import Control.Monad.IO.Class

    import Agda.Syntax.Position (beginningOf, getRange)
    import Agda.Syntax.Common
    import Agda.Syntax.Abstract (Binder, mkBinder_)
    import Agda.Syntax.Internal as I

    import Agda.TypeChecking.Irrelevance
    import {-# SOURCE #-} Agda.TypeChecking.MetaVars
    import {-# SOURCE #-} Agda.TypeChecking.Rules.Term (unquoteTactic)
    import Agda.TypeChecking.Monad
    import Agda.TypeChecking.Reduce
    import Agda.TypeChecking.Substitute
    import Agda.TypeChecking.Pretty
    import Agda.TypeChecking.Telescope

    import Agda.Utils.Functor
    import Agda.Utils.List1 (List1, pattern (:|))
    import qualified Agda.Utils.List1 as List1
    import Agda.Utils.Maybe
    import Agda.Utils.Tuple

    -- Cut and paste from insertImplicitPatternsT:

    -- | Insert implicit binders in a list of binders, but not at the end.
    insertImplicitBindersT
      :: (PureTCM m, MonadError TCErr m, MonadFresh NameId m, MonadTrace m)
      => [NamedArg Binder]     -- ^ Should be non-empty, otherwise nothing happens.
      -> Type                  -- ^ Function type eliminated by arguments given by binders.
      -> m [NamedArg Binder] -- ^ Padded binders.
    insertImplicitBindersT :: forall (m :: * -> *).
    (PureTCM m, MonadError TCErr m, MonadFresh NameId m,
     MonadTrace m) =>
    [NamedArg Binder] -> Type -> m [NamedArg Binder]
    insertImplicitBindersT = \case
      []     -> \ Type
    _ -> [NamedArg Binder] -> m [NamedArg Binder]
    forall (m :: * -> *) a. Monad m => a -> m a
    return []
      NamedArg Binder
    b : [NamedArg Binder]
    bs -> NonEmpty (NamedArg Binder) -> [NamedArg Binder]
    forall a. NonEmpty a -> [a]
    List1.toList (NonEmpty (NamedArg Binder) -> [NamedArg Binder])
    -> (Type -> m (NonEmpty (NamedArg Binder)))
    -> Type
    -> m [NamedArg Binder]
    forall (m :: * -> *) b c a.
    Functor m =>
    (b -> c) -> (a -> m b) -> a -> m c
    <.> NonEmpty (NamedArg Binder)
    -> Type -> m (NonEmpty (NamedArg Binder))
    forall (m :: * -> *).
    (PureTCM m, MonadError TCErr m, MonadFresh NameId m,
     MonadTrace m) =>
    NonEmpty (NamedArg Binder)
    -> Type -> m (NonEmpty (NamedArg Binder))
    insertImplicitBindersT1 (NamedArg Binder
    b NamedArg Binder -> [NamedArg Binder] -> NonEmpty (NamedArg Binder)
    forall a. a -> [a] -> NonEmpty a
    :| [NamedArg Binder]
    bs)

    -- | Insert implicit binders in a list of binders, but not at the end.
    insertImplicitBindersT1
      :: (PureTCM m, MonadError TCErr m, MonadFresh NameId m, MonadTrace m)
      => List1 (NamedArg Binder)        -- ^ Non-empty.
      -> Type                           -- ^ Function type eliminated by arguments given by binders.
      -> m (List1 (NamedArg Binder))  -- ^ Padded binders.
    insertImplicitBindersT1 :: forall (m :: * -> *).
    (PureTCM m, MonadError TCErr m, MonadFresh NameId m,
     MonadTrace m) =>
    NonEmpty (NamedArg Binder)
    -> Type -> m (NonEmpty (NamedArg Binder))
    insertImplicitBindersT1 bs :: NonEmpty (NamedArg Binder)
    bs@(NamedArg Binder
    b :| [NamedArg Binder]
    _) Type
    a = NamedArg Binder
    -> m (NonEmpty (NamedArg Binder)) -> m (NonEmpty (NamedArg Binder))
    forall (m :: * -> *) x a.
    (MonadTrace m, HasRange x) =>
    x -> m a -> m a
    setCurrentRange NamedArg Binder
    b (m (NonEmpty (NamedArg Binder)) -> m (NonEmpty (NamedArg Binder)))
    -> m (NonEmpty (NamedArg Binder)) -> m (NonEmpty (NamedArg Binder))
    forall a b. (a -> b) -> a -> b
    $ do
      TelV Tele (Dom Type)
    tel Type
    ty0 <- Int -> (Dom Type -> Bool) -> Type -> m (TelV Type)
    forall (m :: * -> *).
    (MonadReduce m, MonadAddContext m) =>
    Int -> (Dom Type -> Bool) -> Type -> m (TelV Type)
    telViewUpTo' (-Int
    1) (Bool -> Bool
    not (Bool -> Bool) -> (Dom Type -> Bool) -> Dom Type -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Dom Type -> Bool
    forall a. LensHiding a => a -> Bool
    visible) Type
    a
      ArgName -> Int -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> Int -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "tc.term.lambda.imp" Int
    20 (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
    "insertImplicitBindersT"
             , Int -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "bs  = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> do
                 TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => m Doc -> m Doc
    brackets (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    fsep ([TCMT IO Doc] -> TCMT IO Doc) -> [TCMT IO Doc] -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc -> NonEmpty (TCMT IO Doc) -> [TCMT IO Doc]
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Semigroup (m Doc), Foldable t) =>
    m Doc -> t (m Doc) -> [m Doc]
    punctuate TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc
    comma (NonEmpty (TCMT IO Doc) -> [TCMT IO Doc])
    -> NonEmpty (TCMT IO Doc) -> [TCMT IO Doc]
    forall a b. (a -> b) -> a -> b
    $ (NamedArg Binder -> TCMT IO Doc)
    -> NonEmpty (NamedArg Binder) -> NonEmpty (TCMT IO Doc)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap NamedArg Binder -> TCMT IO Doc
    forall a (m :: * -> *).
    (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
    a -> m Doc
    prettyA NonEmpty (NamedArg Binder)
    bs
             , Int -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "tel = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Tele (Dom Type) -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Tele (Dom Type)
    tel
             , Int -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "ty  = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Tele (Dom Type) -> TCMT IO Doc -> TCMT IO Doc
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext Tele (Dom Type)
    tel (Type -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Type
    ty0)
             ]
      ArgName -> Int -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> Int -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "tc.term.lambda.imp" Int
    70 (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
    "insertImplicitBindersT"
             , Int -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "bs  = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> (ArgName -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => ArgName -> m Doc
    text (ArgName -> TCMT IO Doc)
    -> (NonEmpty (NamedArg Binder) -> ArgName)
    -> NonEmpty (NamedArg Binder)
    -> TCMT IO Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [NamedArg Binder] -> ArgName
    forall a. Show a => a -> ArgName
    show ([NamedArg Binder] -> ArgName)
    -> (NonEmpty (NamedArg Binder) -> [NamedArg Binder])
    -> NonEmpty (NamedArg Binder)
    -> ArgName
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . NonEmpty (NamedArg Binder) -> [NamedArg Binder]
    forall a. NonEmpty a -> [a]
    List1.toList) NonEmpty (NamedArg Binder)
    bs
             , Int -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "tel = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> (ArgName -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => ArgName -> m Doc
    text (ArgName -> TCMT IO Doc)
    -> (Tele (Dom Type) -> ArgName) -> Tele (Dom Type) -> TCMT IO Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Tele (Dom Type) -> ArgName
    forall a. Show a => a -> ArgName
    show) Tele (Dom Type)
    tel
             , Int -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "ty  = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> (ArgName -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => ArgName -> m Doc
    text (ArgName -> TCMT IO Doc)
    -> (Type -> ArgName) -> Type -> TCMT IO Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Type -> ArgName
    forall a. Show a => a -> ArgName
    show) Type
    ty0
             ]
      [NamedArg Binder]
    hs <- NamedArg Binder -> Tele (Dom Type) -> m [NamedArg Binder]
    forall {m :: * -> *} {e} {t}.
    (MonadTCEnv m, ReadTCState m, MonadError TCErr m,
     MonadFresh NameId m, HasRange e) =>
    NamedArg e -> Tele (Dom t) -> m [NamedArg Binder]
    insImp NamedArg Binder
    b Tele (Dom Type)
    tel
      -- Continue with implicit binders inserted before @b@.
      let bs0 :: NonEmpty (NamedArg Binder)
    bs0@(NamedArg Binder
    b1 :| [NamedArg Binder]
    bs1) = [NamedArg Binder]
    -> NonEmpty (NamedArg Binder) -> NonEmpty (NamedArg Binder)
    forall a. [a] -> List1 a -> List1 a
    List1.prependList [NamedArg Binder]
    hs NonEmpty (NamedArg Binder)
    bs
      Type -> m Type
    forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
    reduce Type
    a m Type
    -> (Type -> m (Either (Dom Type, Abs Type) Type))
    -> m (Either (Dom Type, Abs Type) Type)
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= Type -> m (Either (Dom Type, Abs Type) Type)
    forall (m :: * -> *).
    HasBuiltins m =>
    Type -> m (Either (Dom Type, Abs Type) Type)
    piOrPath m (Either (Dom Type, Abs Type) Type)
    -> (Either (Dom Type, Abs Type) Type
        -> m (NonEmpty (NamedArg Binder)))
    -> m (NonEmpty (NamedArg Binder))
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
        -- If @a@ is a function (or path) type, continue inserting after @b1@.
        Left (Dom Type
    _, Abs Type
    ty) -> (NamedArg Binder
    b1 NamedArg Binder -> [NamedArg Binder] -> NonEmpty (NamedArg Binder)
    forall a. a -> [a] -> NonEmpty a
    :|) ([NamedArg Binder] -> NonEmpty (NamedArg Binder))
    -> m [NamedArg Binder] -> m (NonEmpty (NamedArg Binder))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [NamedArg Binder] -> Type -> m [NamedArg Binder]
    forall (m :: * -> *).
    (PureTCM m, MonadError TCErr m, MonadFresh NameId m,
     MonadTrace m) =>
    [NamedArg Binder] -> Type -> m [NamedArg Binder]
    insertImplicitBindersT [NamedArg Binder]
    bs1 (Abs Type -> Type
    forall a. Subst a => Abs a -> a
    absBody Abs Type
    ty)
        -- Otherwise, we are done.
        Right{}      -> NonEmpty (NamedArg Binder) -> m (NonEmpty (NamedArg Binder))
    forall (m :: * -> *) a. Monad m => a -> m a
    return NonEmpty (NamedArg Binder)
    bs0
      where
      insImp :: NamedArg e -> Tele (Dom t) -> m [NamedArg Binder]
    insImp NamedArg e
    b Tele (Dom t)
    EmptyTel = [NamedArg Binder] -> m [NamedArg Binder]
    forall (m :: * -> *) a. Monad m => a -> m a
    return []
      insImp NamedArg e
    b Tele (Dom t)
    tel = case NamedArg e -> [Dom (ArgName, t)] -> ImplicitInsertion
    forall e a. NamedArg e -> [Dom a] -> ImplicitInsertion
    insertImplicit NamedArg e
    b ([Dom (ArgName, t)] -> ImplicitInsertion)
    -> [Dom (ArgName, t)] -> ImplicitInsertion
    forall a b. (a -> b) -> a -> b
    $ Tele (Dom t) -> [Dom (ArgName, t)]
    forall t. Tele (Dom t) -> [Dom (ArgName, t)]
    telToList Tele (Dom t)
    tel of
        ImplicitInsertion
    BadImplicits   -> TypeError -> m [NamedArg Binder]
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError TypeError
    WrongHidingInLHS
        NoSuchName ArgName
    x   -> TypeError -> m [NamedArg Binder]
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError TypeError
    WrongHidingInLHS
        ImpInsert [Dom ()]
    doms -> (Dom () -> m (NamedArg Binder)) -> [Dom ()] -> m [NamedArg Binder]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM Dom () -> m (NamedArg Binder)
    implicitArg [Dom ()]
    doms
          where
          implicitArg :: Dom () -> m (NamedArg Binder)
    implicitArg Dom ()
    d = Origin -> NamedArg Binder -> NamedArg Binder
    forall a. LensOrigin a => Origin -> a -> a
    setOrigin Origin
    Inserted (NamedArg Binder -> NamedArg Binder)
    -> (Name -> NamedArg Binder) -> Name -> NamedArg Binder
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ArgInfo -> Binder -> NamedArg Binder
    forall a. ArgInfo -> a -> NamedArg a
    unnamedArg (Dom () -> ArgInfo
    forall t e. Dom' t e -> ArgInfo
    domInfo Dom ()
    d) (Binder -> NamedArg Binder)
    -> (Name -> Binder) -> Name -> NamedArg Binder
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Name -> Binder
    mkBinder_ (Name -> NamedArg Binder) -> m Name -> m (NamedArg Binder)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> do
            Range -> m Name
    forall (m :: * -> *). MonadFresh NameId m => Range -> m Name
    freshNoName (Range -> m Name) -> Range -> m Name
    forall a b. (a -> b) -> a -> b
    $ Range -> Range
    beginningOf (Range -> Range) -> Range -> Range
    forall a b. (a -> b) -> a -> b
    $ NamedArg e -> Range
    forall a. HasRange a => a -> Range
    getRange NamedArg e
    b

    -- | @implicitArgs n expand t@ generates up to @n@ implicit argument
    --   metas (unbounded if @n<0@), as long as @t@ is a function type
    --   and @expand@ holds on the hiding info of its domain.

    implicitArgs
      :: (PureTCM m, MonadMetaSolver m, MonadTCM m)
      => Int               -- ^ @n@, the maximum number of implicts to be inserted.
      -> (Hiding -> Bool)  -- ^ @expand@, the predicate to test whether we should keep inserting.
      -> Type              -- ^ The (function) type @t@ we are eliminating.
      -> m (Args, Type)  -- ^ The eliminating arguments and the remaining type.
    implicitArgs :: forall (m :: * -> *).
    (PureTCM m, MonadMetaSolver m, MonadTCM m) =>
    Int -> (Hiding -> Bool) -> Type -> m (Args, Type)
    implicitArgs Int
    n Hiding -> Bool
    expand Type
    t = ([Arg (Named NamedName Term)] -> Args)
    -> ([Arg (Named NamedName Term)], Type) -> (Args, Type)
    forall a c b. (a -> c) -> (a, b) -> (c, b)
    mapFst ((Arg (Named NamedName Term) -> Arg Term)
    -> [Arg (Named NamedName Term)] -> Args
    forall a b. (a -> b) -> [a] -> [b]
    map ((Named NamedName Term -> Term)
    -> Arg (Named NamedName Term) -> Arg Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Named NamedName Term -> Term
    forall name a. Named name a -> a
    namedThing)) (([Arg (Named NamedName Term)], Type) -> (Args, Type))
    -> m ([Arg (Named NamedName Term)], Type) -> m (Args, Type)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> do
      Int
    -> (Hiding -> ArgName -> Bool)
    -> Type
    -> m ([Arg (Named NamedName Term)], Type)
    forall (m :: * -> *).
    (PureTCM m, MonadMetaSolver m, MonadTCM m) =>
    Int
    -> (Hiding -> ArgName -> Bool)
    -> Type
    -> m ([Arg (Named NamedName Term)], Type)
    implicitNamedArgs Int
    n (\ Hiding
    h ArgName
    x -> Hiding -> Bool
    expand Hiding
    h) Type
    t

    -- | @implicitNamedArgs n expand t@ generates up to @n@ named implicit arguments
    --   metas (unbounded if @n<0@), as long as @t@ is a function type
    --   and @expand@ holds on the hiding and name info of its domain.

    implicitNamedArgs
      :: (PureTCM m, MonadMetaSolver m, MonadTCM m)
      => Int                          -- ^ @n@, the maximum number of implicts to be inserted.
      -> (Hiding -> ArgName -> Bool)  -- ^ @expand@, the predicate to test whether we should keep inserting.
      -> Type                         -- ^ The (function) type @t@ we are eliminating.
      -> m (NamedArgs, Type)        -- ^ The eliminating arguments and the remaining type.
    implicitNamedArgs :: forall (m :: * -> *).
    (PureTCM m, MonadMetaSolver m, MonadTCM m) =>
    Int
    -> (Hiding -> ArgName -> Bool)
    -> Type
    -> m ([Arg (Named NamedName Term)], Type)
    implicitNamedArgs Int
    0 Hiding -> ArgName -> Bool
    expand Type
    t0 = ([Arg (Named NamedName Term)], Type)
    -> m ([Arg (Named NamedName Term)], Type)
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([], Type
    t0)
    implicitNamedArgs Int
    n Hiding -> ArgName -> Bool
    expand Type
    t0 = do
        Type
    t0' <- Type -> m Type
    forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
    reduce Type
    t0
        ArgName -> Int -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> Int -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "tc.term.args" Int
    30 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "implicitNamedArgs" 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
    t0'
        ArgName -> Int -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> Int -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "tc.term.args" Int
    80 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "implicitNamedArgs" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> ArgName -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => ArgName -> m Doc
    text (Type -> ArgName
    forall a. Show a => a -> ArgName
    show Type
    t0')
        case Type -> Term
    forall t a. Type'' t a -> a
    unEl Type
    t0' of
          Pi dom :: Dom Type
    dom@Dom{domInfo :: forall t e. Dom' t e -> ArgInfo
    domInfo = ArgInfo
    info, domTactic :: forall t e. Dom' t e -> Maybe t
    domTactic = Maybe Term
    tac, unDom :: forall t e. Dom' t e -> e
    unDom = Type
    a} Abs Type
    b
            | let x :: ArgName
    x = ArgName -> Dom Type -> ArgName
    forall a.
    (LensNamed a, NameOf a ~ NamedName) =>
    ArgName -> a -> ArgName
    bareNameWithDefault ArgName
    "_" Dom Type
    dom, Hiding -> ArgName -> Bool
    expand (ArgInfo -> Hiding
    forall a. LensHiding a => a -> Hiding
    getHiding ArgInfo
    info) ArgName
    x -> do
              ArgInfo
    info' <- if ArgInfo -> Bool
    forall a. LensHiding a => a -> Bool
    hidden ArgInfo
    info then ArgInfo -> m ArgInfo
    forall (m :: * -> *) a. Monad m => a -> m a
    return ArgInfo
    info else do
                ArgName -> Int -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> Int -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "tc.term.args.ifs" Int
    15 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
    forall a b. (a -> b) -> a -> b
    $
                  TCMT IO Doc
    "inserting instance meta for 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
                ArgName -> Int -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> Int -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "tc.term.args.ifs" Int
    40 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
    forall a b. (a -> b) -> a -> b
    $ Int -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    2 (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
    "x      = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> ArgName -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => ArgName -> m Doc
    text (ArgName -> ArgName
    forall a. Show a => a -> ArgName
    show ArgName
    x)
                  , TCMT IO Doc
    "hiding = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> ArgName -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => ArgName -> m Doc
    text (Hiding -> ArgName
    forall a. Show a => a -> ArgName
    show (Hiding -> ArgName) -> Hiding -> ArgName
    forall a b. (a -> b) -> a -> b
    $ ArgInfo -> Hiding
    forall a. LensHiding a => a -> Hiding
    getHiding ArgInfo
    info)
                  ]

                ArgInfo -> m ArgInfo
    forall (m :: * -> *) a. Monad m => a -> m a
    return (ArgInfo -> m ArgInfo) -> ArgInfo -> m ArgInfo
    forall a b. (a -> b) -> a -> b
    $ ArgInfo -> ArgInfo
    forall a. LensHiding a => a -> a
    makeInstance ArgInfo
    info
              (MetaId
    _, Term
    v) <- ArgInfo -> ArgName -> Comparison -> Type -> m (MetaId, Term)
    forall (m :: * -> *).
    (PureTCM m, MonadMetaSolver m) =>
    ArgInfo -> ArgName -> Comparison -> Type -> m (MetaId, Term)
    newMetaArg ArgInfo
    info' ArgName
    x Comparison
    CmpLeq Type
    a
              Maybe Term -> (Term -> m ()) -> m ()
    forall (m :: * -> *) a. Monad m => Maybe a -> (a -> m ()) -> m ()
    whenJust Maybe Term
    tac ((Term -> m ()) -> m ()) -> (Term -> m ()) -> m ()
    forall a b. (a -> b) -> a -> b
    $ \ Term
    tac -> TCM () -> m ()
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCM () -> m ()) -> TCM () -> m ()
    forall a b. (a -> b) -> a -> b
    $
                ArgInfo -> TCM () -> TCM ()
    forall (tcm :: * -> *) m a.
    (MonadTCEnv tcm, LensModality m) =>
    m -> tcm a -> tcm a
    applyModalityToContext ArgInfo
    info (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Term -> Term -> Type -> TCM ()
    unquoteTactic Term
    tac Term
    v Type
    a
              let narg :: Arg (Named NamedName Term)
    narg = ArgInfo -> Named NamedName Term -> Arg (Named NamedName Term)
    forall e. ArgInfo -> e -> Arg e
    Arg ArgInfo
    info (Maybe NamedName -> Term -> Named NamedName Term
    forall name a. Maybe name -> a -> Named name a
    Named (NamedName -> Maybe NamedName
    forall a. a -> Maybe a
    Just (NamedName -> Maybe NamedName) -> NamedName -> Maybe NamedName
    forall a b. (a -> b) -> a -> b
    $ Origin -> Ranged ArgName -> NamedName
    forall a. Origin -> a -> WithOrigin a
    WithOrigin Origin
    Inserted (Ranged ArgName -> NamedName) -> Ranged ArgName -> NamedName
    forall a b. (a -> b) -> a -> b
    $ ArgName -> Ranged ArgName
    forall a. a -> Ranged a
    unranged ArgName
    x) Term
    v)
              ([Arg (Named NamedName Term)] -> [Arg (Named NamedName Term)])
    -> ([Arg (Named NamedName Term)], Type)
    -> ([Arg (Named NamedName Term)], Type)
    forall a c b. (a -> c) -> (a, b) -> (c, b)
    mapFst (Arg (Named NamedName Term)
    narg Arg (Named NamedName Term)
    -> [Arg (Named NamedName Term)] -> [Arg (Named NamedName Term)]
    forall a. a -> [a] -> [a]
    :) (([Arg (Named NamedName Term)], Type)
     -> ([Arg (Named NamedName Term)], Type))
    -> m ([Arg (Named NamedName Term)], Type)
    -> m ([Arg (Named NamedName Term)], Type)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Int
    -> (Hiding -> ArgName -> Bool)
    -> Type
    -> m ([Arg (Named NamedName Term)], Type)
    forall (m :: * -> *).
    (PureTCM m, MonadMetaSolver m, MonadTCM m) =>
    Int
    -> (Hiding -> ArgName -> Bool)
    -> Type
    -> m ([Arg (Named NamedName Term)], Type)
    implicitNamedArgs (Int
    nInt -> Int -> Int
    forall a. Num a => a -> a -> a
    -Int
    1) Hiding -> ArgName -> Bool
    expand (Abs Type -> SubstArg Type -> Type
    forall a. Subst a => Abs a -> SubstArg a -> a
    absApp Abs Type
    b Term
    SubstArg Type
    v)
          Term
    _ -> ([Arg (Named NamedName Term)], Type)
    -> m ([Arg (Named NamedName Term)], Type)
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([], Type
    t0')

    -- | Create a metavariable according to the 'Hiding' info.

    newMetaArg
      :: (PureTCM m, MonadMetaSolver m)
      => ArgInfo    -- ^ Kind/relevance of meta.
      -> ArgName    -- ^ Name suggestion for meta.
      -> Comparison -- ^ Check (@CmpLeq@) or infer (@CmpEq@) the type.
      -> Type       -- ^ Type of meta.
      -> m (MetaId, Term)  -- ^ The created meta as id and as term.
    newMetaArg :: forall (m :: * -> *).
    (PureTCM m, MonadMetaSolver m) =>
    ArgInfo -> ArgName -> Comparison -> Type -> m (MetaId, Term)
    newMetaArg ArgInfo
    info ArgName
    x Comparison
    cmp Type
    a = do
      Either Blocker Bool
    prp <- BlockT m Bool -> m (Either Blocker Bool)
    forall (m :: * -> *) a.
    Monad m =>
    BlockT m a -> m (Either Blocker a)
    runBlocked (BlockT m Bool -> m (Either Blocker Bool))
    -> BlockT m Bool -> m (Either Blocker Bool)
    forall a b. (a -> b) -> a -> b
    $ Type -> BlockT m Bool
    forall a (m :: * -> *).
    (LensSort a, PrettyTCM a, PureTCM m, MonadBlock m) =>
    a -> m Bool
    isPropM Type
    a
      let irrelevantIfProp :: m (MetaId, Term) -> m (MetaId, Term)
    irrelevantIfProp =
            if Either Blocker Bool
    prp Either Blocker Bool -> Either Blocker Bool -> Bool
    forall a. Eq a => a -> a -> Bool
    == Bool -> Either Blocker Bool
    forall a b. b -> Either a b
    Right Bool
    True
            then Relevance -> m (MetaId, Term) -> m (MetaId, Term)
    forall (tcm :: * -> *) r a.
    (MonadTCEnv tcm, LensRelevance r) =>
    r -> tcm a -> tcm a
    applyRelevanceToContext Relevance
    Irrelevant
            else m (MetaId, Term) -> m (MetaId, Term)
    forall a. a -> a
    id
      ArgInfo -> m (MetaId, Term) -> m (MetaId, Term)
    forall (tcm :: * -> *) m a.
    (MonadTCEnv tcm, LensModality m) =>
    m -> tcm a -> tcm a
    applyModalityToContext ArgInfo
    info (m (MetaId, Term) -> m (MetaId, Term))
    -> m (MetaId, Term) -> m (MetaId, Term)
    forall a b. (a -> b) -> a -> b
    $ m (MetaId, Term) -> m (MetaId, Term)
    irrelevantIfProp (m (MetaId, Term) -> m (MetaId, Term))
    -> m (MetaId, Term) -> m (MetaId, Term)
    forall a b. (a -> b) -> a -> b
    $
        Hiding -> ArgName -> Type -> m (MetaId, Term)
    forall (m :: * -> *).
    MonadMetaSolver m =>
    Hiding -> ArgName -> Type -> m (MetaId, Term)
    newMeta (ArgInfo -> Hiding
    forall a. LensHiding a => a -> Hiding
    getHiding ArgInfo
    info) (ArgName -> ArgName
    argNameToString ArgName
    x) Type
    a
      where
        newMeta :: MonadMetaSolver m => Hiding -> String -> Type -> m (MetaId, Term)
        newMeta :: forall (m :: * -> *).
    MonadMetaSolver m =>
    Hiding -> ArgName -> Type -> m (MetaId, Term)
    newMeta Instance{} ArgName
    n = ArgName -> Type -> m (MetaId, Term)
    forall (m :: * -> *).
    MonadMetaSolver m =>
    ArgName -> Type -> m (MetaId, Term)
    newInstanceMeta ArgName
    n
        newMeta Hiding
    Hidden     ArgName
    n = RunMetaOccursCheck
    -> ArgName -> Comparison -> Type -> m (MetaId, Term)
    forall (m :: * -> *).
    MonadMetaSolver m =>
    RunMetaOccursCheck
    -> ArgName -> Comparison -> Type -> m (MetaId, Term)
    newNamedValueMeta RunMetaOccursCheck
    RunMetaOccursCheck ArgName
    n Comparison
    cmp
        newMeta Hiding
    NotHidden  ArgName
    n = RunMetaOccursCheck
    -> ArgName -> Comparison -> Type -> m (MetaId, Term)
    forall (m :: * -> *).
    MonadMetaSolver m =>
    RunMetaOccursCheck
    -> ArgName -> Comparison -> Type -> m (MetaId, Term)
    newNamedValueMeta RunMetaOccursCheck
    RunMetaOccursCheck ArgName
    n Comparison
    cmp

    -- | Create a questionmark according to the 'Hiding' info.

    newInteractionMetaArg
      :: ArgInfo    -- ^ Kind/relevance of meta.
      -> ArgName    -- ^ Name suggestion for meta.
      -> Comparison -- ^ Check (@CmpLeq@) or infer (@CmpEq@) the type.
      -> Type       -- ^ Type of meta.
      -> TCM (MetaId, Term)  -- ^ The created meta as id and as term.
    newInteractionMetaArg :: ArgInfo -> ArgName -> Comparison -> Type -> TCM (MetaId, Term)
    newInteractionMetaArg ArgInfo
    info ArgName
    x Comparison
    cmp Type
    a = do
      ArgInfo -> TCM (MetaId, Term) -> TCM (MetaId, Term)
    forall (tcm :: * -> *) m a.
    (MonadTCEnv tcm, LensModality m) =>
    m -> tcm a -> tcm a
    applyModalityToContext ArgInfo
    info (TCM (MetaId, Term) -> TCM (MetaId, Term))
    -> TCM (MetaId, Term) -> TCM (MetaId, Term)
    forall a b. (a -> b) -> a -> b
    $
        Hiding -> ArgName -> Type -> TCM (MetaId, Term)
    newMeta (ArgInfo -> Hiding
    forall a. LensHiding a => a -> Hiding
    getHiding ArgInfo
    info) (ArgName -> ArgName
    argNameToString ArgName
    x) Type
    a
      where
        newMeta :: Hiding -> String -> Type -> TCM (MetaId, Term)
        newMeta :: Hiding -> ArgName -> Type -> TCM (MetaId, Term)
    newMeta Instance{} ArgName
    n = ArgName -> Type -> TCM (MetaId, Term)
    forall (m :: * -> *).
    MonadMetaSolver m =>
    ArgName -> Type -> m (MetaId, Term)
    newInstanceMeta ArgName
    n
        newMeta Hiding
    Hidden     ArgName
    n = RunMetaOccursCheck
    -> ArgName -> Comparison -> Type -> TCM (MetaId, Term)
    forall (m :: * -> *).
    MonadMetaSolver m =>
    RunMetaOccursCheck
    -> ArgName -> Comparison -> Type -> m (MetaId, Term)
    newNamedValueMeta' RunMetaOccursCheck
    RunMetaOccursCheck ArgName
    n Comparison
    cmp
        newMeta Hiding
    NotHidden  ArgName
    n = RunMetaOccursCheck
    -> ArgName -> Comparison -> Type -> TCM (MetaId, Term)
    forall (m :: * -> *).
    MonadMetaSolver m =>
    RunMetaOccursCheck
    -> ArgName -> Comparison -> Type -> m (MetaId, Term)
    newNamedValueMeta' RunMetaOccursCheck
    RunMetaOccursCheck ArgName
    n Comparison
    cmp

    ---------------------------------------------------------------------------

    -- | Possible results of 'insertImplicit'.
    data ImplicitInsertion
          = ImpInsert [Dom ()] -- ^ Success: this many implicits have to be inserted (list can be empty).
          | BadImplicits       -- ^ Error: hidden argument where there should have been a non-hidden argument.
          | NoSuchName ArgName -- ^ Error: bad named argument.
      deriving (Int -> ImplicitInsertion -> ArgName -> ArgName
    [ImplicitInsertion] -> ArgName -> ArgName
    ImplicitInsertion -> ArgName
    (Int -> ImplicitInsertion -> ArgName -> ArgName)
    -> (ImplicitInsertion -> ArgName)
    -> ([ImplicitInsertion] -> ArgName -> ArgName)
    -> Show ImplicitInsertion
    forall a.
    (Int -> a -> ArgName -> ArgName)
    -> (a -> ArgName) -> ([a] -> ArgName -> ArgName) -> Show a
    showList :: [ImplicitInsertion] -> ArgName -> ArgName
    $cshowList :: [ImplicitInsertion] -> ArgName -> ArgName
    show :: ImplicitInsertion -> ArgName
    $cshow :: ImplicitInsertion -> ArgName
    showsPrec :: Int -> ImplicitInsertion -> ArgName -> ArgName
    $cshowsPrec :: Int -> ImplicitInsertion -> ArgName -> ArgName
    Show)

    pattern NoInsertNeeded :: ImplicitInsertion
    pattern $bNoInsertNeeded :: ImplicitInsertion
    $mNoInsertNeeded :: forall {r}. ImplicitInsertion -> (Void# -> r) -> (Void# -> r) -> r
    NoInsertNeeded = ImpInsert []

    -- | If the next given argument is @a@ and the expected arguments are @ts@
    --   @insertImplicit' a ts@ returns the prefix of @ts@ that precedes @a@.
    --
    --   If @a@ is named but this name does not appear in @ts@, the 'NoSuchName' exception is thrown.
    --
    insertImplicit
      :: NamedArg e  -- ^ Next given argument @a@.
      -> [Dom a]     -- ^ Expected arguments @ts@.
      -> ImplicitInsertion
    insertImplicit :: forall e a. NamedArg e -> [Dom a] -> ImplicitInsertion
    insertImplicit NamedArg e
    a [Dom a]
    doms = NamedArg e -> [Dom ArgName] -> ImplicitInsertion
    forall e. NamedArg e -> [Dom ArgName] -> ImplicitInsertion
    insertImplicit' NamedArg e
    a ([Dom ArgName] -> ImplicitInsertion)
    -> [Dom ArgName] -> ImplicitInsertion
    forall a b. (a -> b) -> a -> b
    $
      [Dom a] -> (Dom a -> Dom ArgName) -> [Dom ArgName]
    forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
    for [Dom a]
    doms ((Dom a -> Dom ArgName) -> [Dom ArgName])
    -> (Dom a -> Dom ArgName) -> [Dom ArgName]
    forall a b. (a -> b) -> a -> b
    $ \ Dom a
    dom ->
        Dom a
    dom Dom a -> ArgName -> Dom ArgName
    forall (f :: * -> *) a b. Functor f => f a -> b -> f b
    $> ArgName -> Dom a -> ArgName
    forall a.
    (LensNamed a, NameOf a ~ NamedName) =>
    ArgName -> a -> ArgName
    bareNameWithDefault ArgName
    "_" Dom a
    dom

    -- | If the next given argument is @a@ and the expected arguments are @ts@
    --   @insertImplicit' a ts@ returns the prefix of @ts@ that precedes @a@.
    --
    --   If @a@ is named but this name does not appear in @ts@, the 'NoSuchName' exception is thrown.
    --
    insertImplicit'
      :: NamedArg e     -- ^ Next given argument @a@.
      -> [Dom ArgName]  -- ^ Expected arguments @ts@.
      -> ImplicitInsertion
    insertImplicit' :: forall e. NamedArg e -> [Dom ArgName] -> ImplicitInsertion
    insertImplicit' NamedArg e
    _ [] = ImplicitInsertion
    BadImplicits
    insertImplicit' NamedArg e
    a [Dom ArgName]
    ts

      -- If @a@ is visible, then take the non-visible prefix of @ts@.
      | NamedArg e -> Bool
    forall a. LensHiding a => a -> Bool
    visible NamedArg e
    a = [Dom ()] -> ImplicitInsertion
    ImpInsert ([Dom ()] -> ImplicitInsertion) -> [Dom ()] -> ImplicitInsertion
    forall a b. (a -> b) -> a -> b
    $ (Dom () -> Bool) -> [Dom ()] -> [Dom ()]
    forall a. (a -> Bool) -> [a] -> [a]
    takeWhile Dom () -> Bool
    forall a. LensHiding a => a -> Bool
    notVisible ([Dom ()] -> [Dom ()]) -> [Dom ()] -> [Dom ()]
    forall a b. (a -> b) -> a -> b
    $ (Dom ArgName -> Dom ()) -> [Dom ArgName] -> [Dom ()]
    forall a b. (a -> b) -> [a] -> [b]
    map Dom ArgName -> Dom ()
    forall (f :: * -> *) a. Functor f => f a -> f ()
    void [Dom ArgName]
    ts

      -- If @a@ is named, take prefix of @ts@ until the name of @a@ (with correct hiding).
      -- If the name is not found, throw exception 'NoSuchName'.
      | Just ArgName
    x <- NamedArg e -> Maybe ArgName
    forall a. (LensNamed a, NameOf a ~ NamedName) => a -> Maybe ArgName
    bareNameOf NamedArg e
    a = ImplicitInsertion
    -> ([Dom ()] -> ImplicitInsertion)
    -> Maybe [Dom ()]
    -> ImplicitInsertion
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe (ArgName -> ImplicitInsertion
    NoSuchName ArgName
    x) [Dom ()] -> ImplicitInsertion
    ImpInsert (Maybe [Dom ()] -> ImplicitInsertion)
    -> Maybe [Dom ()] -> ImplicitInsertion
    forall a b. (a -> b) -> a -> b
    $
          (Dom ArgName -> Bool) -> [Dom ArgName] -> Maybe [Dom ()]
    takeHiddenUntil (\ Dom ArgName
    t -> ArgName
    x ArgName -> ArgName -> Bool
    forall a. Eq a => a -> a -> Bool
    == Dom ArgName -> ArgName
    forall t e. Dom' t e -> e
    unDom Dom ArgName
    t Bool -> Bool -> Bool
    && NamedArg e -> Dom ArgName -> Bool
    forall a b. (LensHiding a, LensHiding b) => a -> b -> Bool
    sameHiding NamedArg e
    a Dom ArgName
    t) [Dom ArgName]
    ts

      -- If @a@ is neither visible nor named, take prefix of @ts@ with different hiding than @a@.
      | Bool
    otherwise = ImplicitInsertion
    -> ([Dom ()] -> ImplicitInsertion)
    -> Maybe [Dom ()]
    -> ImplicitInsertion
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe ImplicitInsertion
    BadImplicits [Dom ()] -> ImplicitInsertion
    ImpInsert (Maybe [Dom ()] -> ImplicitInsertion)
    -> Maybe [Dom ()] -> ImplicitInsertion
    forall a b. (a -> b) -> a -> b
    $
          (Dom ArgName -> Bool) -> [Dom ArgName] -> Maybe [Dom ()]
    takeHiddenUntil (NamedArg e -> Dom ArgName -> Bool
    forall a b. (LensHiding a, LensHiding b) => a -> b -> Bool
    sameHiding NamedArg e
    a) [Dom ArgName]
    ts

        where
        -- @takeHiddenUntil p ts@ returns the 'getHiding' of the prefix of @ts@
        -- until @p@ holds or a visible argument is encountered.
        -- If @p@ never holds, 'Nothing' is returned.
        --
        --   Precondition: @p@ should imply @not . visible@.
        takeHiddenUntil :: (Dom ArgName -> Bool) -> [Dom ArgName] -> Maybe [Dom ()]
        takeHiddenUntil :: (Dom ArgName -> Bool) -> [Dom ArgName] -> Maybe [Dom ()]
    takeHiddenUntil Dom ArgName -> Bool
    p [Dom ArgName]
    ts =
          case [Dom ArgName]
    ts2 of
            []      -> Maybe [Dom ()]
    forall a. Maybe a
    Nothing  -- Predicate was never true
            (Dom ArgName
    t : [Dom ArgName]
    _) -> if Dom ArgName -> Bool
    forall a. LensHiding a => a -> Bool
    visible Dom ArgName
    t then Maybe [Dom ()]
    forall a. Maybe a
    Nothing else [Dom ()] -> Maybe [Dom ()]
    forall a. a -> Maybe a
    Just ([Dom ()] -> Maybe [Dom ()]) -> [Dom ()] -> Maybe [Dom ()]
    forall a b. (a -> b) -> a -> b
    $ (Dom ArgName -> Dom ()) -> [Dom ArgName] -> [Dom ()]
    forall a b. (a -> b) -> [a] -> [b]
    map Dom ArgName -> Dom ()
    forall (f :: * -> *) a. Functor f => f a -> f ()
    void [Dom ArgName]
    ts1
          where
          ([Dom ArgName]
    ts1, [Dom ArgName]
    ts2) = (Dom ArgName -> Bool)
    -> [Dom ArgName] -> ([Dom ArgName], [Dom ArgName])
    forall a. (a -> Bool) -> [a] -> ([a], [a])
    break (\ Dom ArgName
    t -> Dom ArgName -> Bool
    p Dom ArgName
    t Bool -> Bool -> Bool
    || Dom ArgName -> Bool
    forall a. LensHiding a => a -> Bool
    visible Dom ArgName
    t) [Dom ArgName]
    ts