    {-# 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 (HasRange, beginningOf, getRange)
    import Agda.Syntax.Common
    import Agda.Syntax.Abstract (Binder, mkBinder_)
    import Agda.Syntax.Info ( MetaKind (InstanceMeta, UnificationMeta) )
    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.Function (applyWhen)
    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:

    -- | Split a given Pi 'Type' until you reach the given named argument,
    -- returning the number of arguments skipped to reach the right plicity
    -- and name.
    splitImplicitBinderT :: HasRange a => NamedArg a -> Type -> TCM (Telescope, Type)
    splitImplicitBinderT :: forall a. HasRange a => NamedArg a -> Type -> TCM (Telescope, Type)
    splitImplicitBinderT NamedArg a
    narg Type
    ty = do
      -- Split off any invisible arguments at the front (so if the first
      -- argument is visible, return tel = EmptyTel)
      TelV tel ty0 <- Int -> (Dom Type -> Bool) -> Type -> TCMT IO (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
    ty

      case tel of
        -- If we didn't lob off any arguments then we can use the original
        -- type and the empty telescope
        Telescope
    EmptyTel -> (Telescope, Type) -> TCM (Telescope, Type)
    forall a. a -> TCMT IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Telescope
    forall a. Tele a
    EmptyTel, Type
    ty)

        -- Otherwise we try inserting implicit arguments.
        Telescope
    _ -> NamedArg a -> TCM (Telescope, Type) -> TCM (Telescope, Type)
    forall (m :: * -> *) x a.
    (MonadTrace m, HasRange x) =>
    x -> m a -> m a
    setCurrentRange NamedArg a
    narg case NamedArg a -> [Dom (ArgName, Type)] -> ImplicitInsertion
    forall e a. NamedArg e -> [Dom a] -> ImplicitInsertion
    insertImplicit NamedArg a
    narg ([Dom (ArgName, Type)] -> ImplicitInsertion)
    -> [Dom (ArgName, Type)] -> ImplicitInsertion
    forall a b. (a -> b) -> a -> b
    $ Telescope -> [Dom (ArgName, Type)]
    forall t. Tele (Dom t) -> [Dom (ArgName, t)]
    telToList Telescope
    tel of
          ImplicitInsertion
    BadImplicits   -> TypeError -> TCM (Telescope, Type)
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError TypeError
    WrongHidingInLHS
          NoSuchName ArgName
    x   -> TypeError -> TCM (Telescope, Type)
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError TypeError
    WrongHidingInLHS
          ImpInsert [Dom ()]
    doms ->
            let (Telescope
    here, Telescope
    there) = Int -> Telescope -> (Telescope, Telescope)
    splitTelescopeAt ([Dom ()] -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [Dom ()]
    doms) Telescope
    tel
            in (Telescope, Type) -> TCM (Telescope, Type)
    forall a. a -> TCMT IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Telescope
    here, Telescope -> Type -> Type
    forall t. Abstract t => Telescope -> t -> t
    abstract Telescope
    there Type
    ty0)

    -- | @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 a b. (a -> b) -> Arg a -> Arg b
    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 a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([], Type
    t0)
    implicitNamedArgs Int
    n Hiding -> ArgName -> Bool
    expand Type
    t0 = do
        t0' <- Type -> m Type
    forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
    reduce Type
    t0
        reportSDoc "tc.term.args" 30 $ "implicitNamedArgs" <+> prettyTCM t0'
        reportSDoc "tc.term.args" 80 $ "implicitNamedArgs" <+> text (show t0')
        case unEl 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
              kind <- if ArgInfo -> Bool
    forall a. LensHiding a => a -> Bool
    hidden ArgInfo
    info then MetaKind -> m MetaKind
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return MetaKind
    UnificationMeta 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
    forall (m :: * -> *). MonadPretty m => Type -> 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)
                  ]

                MetaKind -> m MetaKind
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return MetaKind
    InstanceMeta
              (_, v) <- newMetaArg kind info x CmpLeq a
              whenJust tac $ \ Term
    tac -> TCM () -> m ()
    forall a. TCM a -> m a
    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 = 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)
              mapFst (narg :) <$> implicitNamedArgs (n-1) expand (absApp b v)
          Term
    _ -> ([Arg (Named NamedName Term)], Type)
    -> m ([Arg (Named NamedName Term)], Type)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([], Type
    t0')

    -- | Create a metavariable of 'MetaKind'.

    newMetaArg
      :: (PureTCM m, MonadMetaSolver m)
      => MetaKind   -- ^ Kind of meta.
      -> ArgInfo    -- ^ Rrelevance 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) =>
    MetaKind
    -> ArgInfo -> ArgName -> Comparison -> Type -> m (MetaId, Term)
    newMetaArg MetaKind
    kind ArgInfo
    info ArgName
    x Comparison
    cmp Type
    a = do
      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 =
            Bool
    -> (m (MetaId, Term) -> m (MetaId, Term))
    -> m (MetaId, Term)
    -> m (MetaId, Term)
    forall b a. IsBool b => b -> (a -> a) -> a -> a
    applyWhen (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) ((m (MetaId, Term) -> m (MetaId, Term))
     -> m (MetaId, Term) -> m (MetaId, Term))
    -> (m (MetaId, Term) -> m (MetaId, Term))
    -> m (MetaId, Term)
    -> m (MetaId, Term)
    forall a b. (a -> b) -> a -> b
    $ Relevance -> m (MetaId, Term) -> m (MetaId, Term)
    forall (tcm :: * -> *) r a.
    (MonadTCEnv tcm, LensRelevance r) =>
    r -> tcm a -> tcm a
    applyRelevanceToContext Relevance
    irrelevant
      applyModalityToContext info $ irrelevantIfProp $
        newMeta (argNameToString x) kind a
      where
        newMeta :: MonadMetaSolver m => String -> MetaKind -> Type -> m (MetaId, Term)
        newMeta :: forall (m :: * -> *).
    MonadMetaSolver m =>
    ArgName -> MetaKind -> Type -> m (MetaId, Term)
    newMeta ArgName
    n = \case
          MetaKind
    InstanceMeta    -> ArgName -> Type -> m (MetaId, Term)
    forall (m :: * -> *).
    MonadMetaSolver m =>
    ArgName -> Type -> m (MetaId, Term)
    newInstanceMeta ArgName
    n
          MetaKind
    UnificationMeta -> 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 (always 'UnificationMeta').

    newInteractionMetaArg
      :: ArgInfo    -- ^ 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
    $
        RunMetaOccursCheck
    -> ArgName -> Comparison -> Type -> TCM (MetaId, Term)
    forall (m :: * -> *).
    MonadMetaSolver m =>
    RunMetaOccursCheck
    -> ArgName -> Comparison -> Type -> m (MetaId, Term)
    newNamedValueMeta' RunMetaOccursCheck
    RunMetaOccursCheck (ArgName -> ArgName
    argNameToString ArgName
    x) Comparison
    cmp Type
    a

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

    -- | 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
    $cshowsPrec :: Int -> ImplicitInsertion -> ArgName -> ArgName
    showsPrec :: Int -> ImplicitInsertion -> ArgName -> ArgName
    $cshow :: ImplicitInsertion -> ArgName
    show :: ImplicitInsertion -> ArgName
    $cshowList :: [ImplicitInsertion] -> ArgName -> ArgName
    showList :: [ImplicitInsertion] -> ArgName -> ArgName
    Show)

    pattern NoInsertNeeded :: ImplicitInsertion
    pattern $mNoInsertNeeded :: forall {r}. ImplicitInsertion -> ((# #) -> r) -> ((# #) -> r) -> r
    $bNoInsertNeeded :: ImplicitInsertion
    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