    module Agda.TypeChecking.Rules.LHS.Implicit where

    import Prelude hiding (null)

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

    import Agda.Syntax.Common
    import Agda.Syntax.Position
    import Agda.Syntax.Info
    import Agda.Syntax.Internal as I
    import qualified Agda.Syntax.Abstract as A

    import Agda.TypeChecking.Monad
    import Agda.TypeChecking.Implicit
    import Agda.TypeChecking.Substitute
    import Agda.TypeChecking.Pretty
    import Agda.TypeChecking.Reduce
    import Agda.TypeChecking.Telescope

    import Agda.Utils.Function
    import Agda.Utils.Functor
    import Agda.Utils.Maybe
    import Agda.Utils.Monad

    import Agda.Utils.Impossible

    implicitP :: ArgInfo -> NamedArg A.Pattern
    implicitP :: ArgInfo -> NamedArg Pattern
    implicitP ArgInfo
    info = ArgInfo -> Named NamedName Pattern -> NamedArg Pattern
    forall e. ArgInfo -> e -> Arg e
    Arg (Origin -> ArgInfo -> ArgInfo
    forall a. LensOrigin a => Origin -> a -> a
    setOrigin Origin
    Inserted ArgInfo
    info) (Named NamedName Pattern -> NamedArg Pattern)
    -> Named NamedName Pattern -> NamedArg Pattern
    forall a b. (a -> b) -> a -> b
    $ Pattern -> Named NamedName Pattern
    forall a name. a -> Named name a
    unnamed (Pattern -> Named NamedName Pattern)
    -> Pattern -> Named NamedName Pattern
    forall a b. (a -> b) -> a -> b
    $ PatInfo -> Pattern
    forall e. PatInfo -> Pattern' e
    A.WildP (PatInfo -> Pattern) -> PatInfo -> Pattern
    forall a b. (a -> b) -> a -> b
    $ Range -> PatInfo
    PatRange (Range -> PatInfo) -> Range -> PatInfo
    forall a b. (a -> b) -> a -> b
    $ Range
    forall a. Range' a
    noRange

    -- | Insert implicit patterns in a list of patterns.
    --   Even if 'DontExpandLast', trailing SIZELT patterns are inserted.
    insertImplicitPatterns
      :: (PureTCM m, MonadError TCErr m, MonadFresh NameId m, MonadTrace m)
      => ExpandHidden -> [NamedArg A.Pattern]
      -> Telescope -> m [NamedArg A.Pattern]
    insertImplicitPatterns :: forall (m :: * -> *).
    (PureTCM m, MonadError TCErr m, MonadFresh NameId m,
     MonadTrace m) =>
    ExpandHidden
    -> [NamedArg Pattern] -> Telescope -> m [NamedArg Pattern]
    insertImplicitPatterns ExpandHidden
    exh [NamedArg Pattern]
    ps Telescope
    tel =
      ExpandHidden -> [NamedArg Pattern] -> Type -> m [NamedArg Pattern]
    forall (m :: * -> *).
    (PureTCM m, MonadError TCErr m, MonadFresh NameId m,
     MonadTrace m) =>
    ExpandHidden -> [NamedArg Pattern] -> Type -> m [NamedArg Pattern]
    insertImplicitPatternsT ExpandHidden
    exh [NamedArg Pattern]
    ps (Telescope -> Type -> Type
    telePi Telescope
    tel Type
    HasCallStack => Type
    __DUMMY_TYPE__)

    -- | Insert trailing SizeLt patterns, if any.
    insertImplicitSizeLtPatterns :: PureTCM m => Type -> m [NamedArg A.Pattern]
    insertImplicitSizeLtPatterns :: forall (m :: * -> *). PureTCM m => Type -> m [NamedArg Pattern]
    insertImplicitSizeLtPatterns Type
    t = do
      -- Testing for SizeLt.  In case of blocked type, we return no.
      -- We assume that on the LHS, we know the type.  (TODO: Sufficient?)
      Term -> Maybe BoundedSize
    isSize <- m (Term -> Maybe BoundedSize)
    forall (m :: * -> *).
    (HasOptions m, HasBuiltins m) =>
    m (Term -> Maybe BoundedSize)
    isSizeTypeTest
      let isBounded :: BoundedSize -> Bool
    isBounded BoundedSize
    BoundedNo   = Bool
    False
          isBounded BoundedLt{} = Bool
    True
          isSizeLt :: Type -> m Bool
    isSizeLt Type
    t = Bool -> (BoundedSize -> Bool) -> Maybe BoundedSize -> Bool
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe Bool
    False BoundedSize -> Bool
    isBounded (Maybe BoundedSize -> Bool)
    -> (Type -> Maybe BoundedSize) -> Type -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Term -> Maybe BoundedSize
    isSize (Term -> Maybe BoundedSize)
    -> (Type -> Term) -> Type -> Maybe BoundedSize
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Type -> Term
    forall t a. Type'' t a -> a
    unEl (Type -> Bool) -> m Type -> m Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Type -> m Type
    forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
    reduce Type
    t

      -- Search for the last SizeLt type among the hidden arguments.
      TelV Telescope
    tel Type
    _ <- Type -> m (TelV Type)
    forall (m :: * -> *).
    (MonadReduce m, MonadAddContext m) =>
    Type -> m (TelV Type)
    telView Type
    t
      let ts :: [Dom (ArgName, Type)]
    ts = (Dom (ArgName, Type) -> Bool)
    -> [Dom (ArgName, Type)] -> [Dom (ArgName, Type)]
    forall a. (a -> Bool) -> [a] -> [a]
    takeWhile (Bool -> Bool
    not (Bool -> Bool)
    -> (Dom (ArgName, Type) -> Bool) -> Dom (ArgName, Type) -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Dom (ArgName, Type) -> Bool
    forall a. LensHiding a => a -> Bool
    visible) ([Dom (ArgName, Type)] -> [Dom (ArgName, Type)])
    -> [Dom (ArgName, Type)] -> [Dom (ArgName, Type)]
    forall a b. (a -> b) -> a -> b
    $ Telescope -> [Dom (ArgName, Type)]
    forall t. Tele (Dom t) -> [Dom (ArgName, t)]
    telToList Telescope
    tel
      [Dom (ArgName, Type)]
    keep <- (Dom (ArgName, Type) -> m Bool)
    -> [Dom (ArgName, Type)] -> m [Dom (ArgName, Type)]
    forall (m :: * -> *) a. Monad m => (a -> m Bool) -> [a] -> m [a]
    dropWhileEndM (Bool -> Bool
    not (Bool -> Bool)
    -> (Dom (ArgName, Type) -> m Bool) -> Dom (ArgName, Type) -> m Bool
    forall (m :: * -> *) b c a.
    Functor m =>
    (b -> c) -> (a -> m b) -> a -> m c
    <.> Type -> m Bool
    isSizeLt (Type -> m Bool)
    -> (Dom (ArgName, Type) -> Type) -> Dom (ArgName, Type) -> m Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (ArgName, Type) -> Type
    forall a b. (a, b) -> b
    snd ((ArgName, Type) -> Type)
    -> (Dom (ArgName, Type) -> (ArgName, Type))
    -> Dom (ArgName, Type)
    -> Type
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Dom (ArgName, Type) -> (ArgName, Type)
    forall t e. Dom' t e -> e
    unDom) [Dom (ArgName, Type)]
    ts
      -- Insert implicit patterns upto (including) the last SizeLt type.
      [NamedArg Pattern] -> m [NamedArg Pattern]
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([NamedArg Pattern] -> m [NamedArg Pattern])
    -> [NamedArg Pattern] -> m [NamedArg Pattern]
    forall a b. (a -> b) -> a -> b
    $ (Dom (ArgName, Type) -> NamedArg Pattern)
    -> [Dom (ArgName, Type)] -> [NamedArg Pattern]
    forall a b. (a -> b) -> [a] -> [b]
    map (ArgInfo -> NamedArg Pattern
    implicitP (ArgInfo -> NamedArg Pattern)
    -> (Dom (ArgName, Type) -> ArgInfo)
    -> Dom (ArgName, Type)
    -> NamedArg Pattern
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Dom (ArgName, Type) -> ArgInfo
    forall t e. Dom' t e -> ArgInfo
    domInfo) [Dom (ArgName, Type)]
    keep

    -- | Insert implicit patterns in a list of patterns.
    --   Even if 'DontExpandLast', trailing SIZELT patterns are inserted.
    insertImplicitPatternsT
      :: (PureTCM m, MonadError TCErr m, MonadFresh NameId m, MonadTrace m)
      => ExpandHidden -> [NamedArg A.Pattern] -> Type
      -> m [NamedArg A.Pattern]
    insertImplicitPatternsT :: forall (m :: * -> *).
    (PureTCM m, MonadError TCErr m, MonadFresh NameId m,
     MonadTrace m) =>
    ExpandHidden -> [NamedArg Pattern] -> Type -> m [NamedArg Pattern]
    insertImplicitPatternsT ExpandHidden
    DontExpandLast [] Type
    a = Type -> m [NamedArg Pattern]
    forall (m :: * -> *). PureTCM m => Type -> m [NamedArg Pattern]
    insertImplicitSizeLtPatterns Type
    a
    insertImplicitPatternsT ExpandHidden
    exh            [NamedArg Pattern]
    ps Type
    a = do
      TelV Telescope
    tel Type
    b <- 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.lhs.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
    "insertImplicitPatternsT"
             , 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
    "ps  = " 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 -> [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 ([TCMT IO Doc] -> [TCMT IO Doc]) -> [TCMT IO Doc] -> [TCMT IO Doc]
    forall a b. (a -> b) -> a -> b
    $ (NamedArg Pattern -> TCMT IO Doc)
    -> [NamedArg Pattern] -> [TCMT IO Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map NamedArg Pattern -> TCMT IO Doc
    forall a (m :: * -> *).
    (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
    a -> m Doc
    prettyA [NamedArg Pattern]
    ps
             , 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
    <+> Telescope -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Telescope
    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
    "b   = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Telescope -> TCMT IO Doc -> TCMT IO Doc
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext Telescope
    tel (Type -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Type
    b)
             ]
      ArgName -> Int -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> Int -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "tc.lhs.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
    "insertImplicitPatternsT"
             , 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
    "ps  = " 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)
    -> ([NamedArg Pattern] -> ArgName)
    -> [NamedArg Pattern]
    -> TCMT IO Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [NamedArg Pattern] -> ArgName
    forall a. Show a => a -> ArgName
    show) [NamedArg Pattern]
    ps
             , 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)
    -> (Telescope -> ArgName) -> Telescope -> TCMT IO Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Telescope -> ArgName
    forall a. Show a => a -> ArgName
    show) Telescope
    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
    "b   = " 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
    b
             ]
      case [NamedArg Pattern]
    ps of
        [] -> NamedArg (Pattern' Any) -> Telescope -> m [NamedArg Pattern]
    forall {m :: * -> *} {e} {t}.
    (MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
    NamedArg e -> Tele (Dom t) -> m [NamedArg Pattern]
    insImp NamedArg (Pattern' Any)
    forall {e}. NamedArg (Pattern' e)
    dummy Telescope
    tel
        NamedArg Pattern
    p : [NamedArg Pattern]
    _ -> NamedArg Pattern -> m [NamedArg Pattern] -> m [NamedArg Pattern]
    forall (m :: * -> *) x a.
    (MonadTrace m, HasRange x) =>
    x -> m a -> m a
    setCurrentRange NamedArg Pattern
    p (m [NamedArg Pattern] -> m [NamedArg Pattern])
    -> m [NamedArg Pattern] -> m [NamedArg Pattern]
    forall a b. (a -> b) -> a -> b
    $ do
          -- Andreas, 2015-05-11.
          -- If p is a projection pattern, make it visible for the purpose of
          -- calling insImp / insertImplicit, to get correct behavior.
          let p' :: NamedArg Pattern
    p' = Bool
    -> (NamedArg Pattern -> NamedArg Pattern)
    -> NamedArg Pattern
    -> NamedArg Pattern
    forall a. Bool -> (a -> a) -> a -> a
    applyWhen (Maybe (ProjOrigin, AmbiguousQName) -> Bool
    forall a. Maybe a -> Bool
    isJust (Maybe (ProjOrigin, AmbiguousQName) -> Bool)
    -> Maybe (ProjOrigin, AmbiguousQName) -> Bool
    forall a b. (a -> b) -> a -> b
    $ NamedArg Pattern -> Maybe (ProjOrigin, AmbiguousQName)
    forall a. IsProjP a => a -> Maybe (ProjOrigin, AmbiguousQName)
    A.isProjP NamedArg Pattern
    p) (Hiding -> NamedArg Pattern -> NamedArg Pattern
    forall a. LensHiding a => Hiding -> a -> a
    setHiding Hiding
    NotHidden) NamedArg Pattern
    p
          [NamedArg Pattern]
    hs <- NamedArg Pattern -> Telescope -> m [NamedArg Pattern]
    forall {m :: * -> *} {e} {t}.
    (MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
    NamedArg e -> Tele (Dom t) -> m [NamedArg Pattern]
    insImp NamedArg Pattern
    p' Telescope
    tel
          -- Continue with implicit patterns inserted before @p@.
          -- The list @hs ++ ps@ cannot be empty.
          let ps0 :: [NamedArg Pattern]
    ps0@(~(NamedArg Pattern
    p1 : [NamedArg Pattern]
    ps1)) = [NamedArg Pattern]
    hs [NamedArg Pattern] -> [NamedArg Pattern] -> [NamedArg Pattern]
    forall a. [a] -> [a] -> [a]
    ++ [NamedArg Pattern]
    ps
          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 [NamedArg Pattern])
    -> m [NamedArg Pattern]
    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 @p1@.
            Left (Dom Type
    _, Abs Type
    b) -> (NamedArg Pattern
    p1 NamedArg Pattern -> [NamedArg Pattern] -> [NamedArg Pattern]
    forall a. a -> [a] -> [a]
    :) ([NamedArg Pattern] -> [NamedArg Pattern])
    -> m [NamedArg Pattern] -> m [NamedArg Pattern]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ExpandHidden -> [NamedArg Pattern] -> Type -> m [NamedArg Pattern]
    forall (m :: * -> *).
    (PureTCM m, MonadError TCErr m, MonadFresh NameId m,
     MonadTrace m) =>
    ExpandHidden -> [NamedArg Pattern] -> Type -> m [NamedArg Pattern]
    insertImplicitPatternsT ExpandHidden
    exh [NamedArg Pattern]
    ps1 (Abs Type -> Type
    forall a. Subst a => Abs a -> a
    absBody Abs Type
    b)
            -- Otherwise, we are done.
            Right{}     -> [NamedArg Pattern] -> m [NamedArg Pattern]
    forall (m :: * -> *) a. Monad m => a -> m a
    return [NamedArg Pattern]
    ps0
      where
        dummy :: NamedArg (Pattern' e)
    dummy = Pattern' e -> NamedArg (Pattern' e)
    forall a. a -> NamedArg a
    defaultNamedArg (BindName -> Pattern' e
    forall e. BindName -> Pattern' e
    A.VarP BindName
    forall a. HasCallStack => a
    __IMPOSSIBLE__)

        insImp :: NamedArg e -> Tele (Dom t) -> m [NamedArg Pattern]
    insImp NamedArg e
    p Tele (Dom t)
    EmptyTel = [NamedArg Pattern] -> m [NamedArg Pattern]
    forall (m :: * -> *) a. Monad m => a -> m a
    return []
        insImp NamedArg e
    p Tele (Dom t)
    tel = case NamedArg e -> [Dom (ArgName, t)] -> ImplicitInsertion
    forall e a. NamedArg e -> [Dom a] -> ImplicitInsertion
    insertImplicit NamedArg e
    p ([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 Pattern]
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError TypeError
    WrongHidingInLHS
          NoSuchName ArgName
    x   -> TypeError -> m [NamedArg Pattern]
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError TypeError
    WrongHidingInLHS
          ImpInsert [Dom ()]
    n    -> [NamedArg Pattern] -> m [NamedArg Pattern]
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([NamedArg Pattern] -> m [NamedArg Pattern])
    -> [NamedArg Pattern] -> m [NamedArg Pattern]
    forall a b. (a -> b) -> a -> b
    $ (Dom () -> NamedArg Pattern) -> [Dom ()] -> [NamedArg Pattern]
    forall a b. (a -> b) -> [a] -> [b]
    map Dom () -> NamedArg Pattern
    forall {a}. LensArgInfo a => a -> NamedArg Pattern
    implicitArg [Dom ()]
    n

        implicitArg :: a -> NamedArg Pattern
    implicitArg a
    d = ArgInfo -> NamedArg Pattern
    implicitP (ArgInfo -> NamedArg Pattern) -> ArgInfo -> NamedArg Pattern
    forall a b. (a -> b) -> a -> b
    $ a -> ArgInfo
    forall a. LensArgInfo a => a -> ArgInfo
    getArgInfo a
    d