    {-# LANGUAGE NondecreasingIndentation   #-}

    {-|
        Translating from internal syntax to abstract syntax. Enables nice
        pretty printing of internal syntax.

        TODO

            - numbers on metas
            - fake dependent functions to independent functions
            - meta parameters
            - shadowing
    -}
    module Agda.Syntax.Translation.InternalToAbstract
      ( Reify(..)
      , MonadReify
      , NamedClause(..)
      , reifyPatterns
      , reifyUnblocked
      , blankNotInScope
      , reifyDisplayFormP
      ) where

    import Prelude hiding (null)

    import Control.Applicative ( liftA2 )
    import Control.Arrow       ( (&&&) )
    import Control.Monad       ( filterM, forM )

    import qualified Data.List as List
    import qualified Data.Map as Map
    import Data.Maybe
    import Data.Semigroup ( Semigroup, (<>) )
    import Data.Set (Set)
    import qualified Data.Set as Set
    import qualified Data.Text as T
    import Data.Traversable (mapM)

    import Agda.Syntax.Literal
    import Agda.Syntax.Position
    import Agda.Syntax.Common
    import qualified Agda.Syntax.Concrete.Name as C
    import Agda.Syntax.Concrete (FieldAssignment'(..), TacticAttribute'(..))
    import Agda.Syntax.Info as Info
    import Agda.Syntax.Abstract as A hiding (Binder)
    import qualified Agda.Syntax.Abstract as A
    import Agda.Syntax.Abstract.Pattern
    import Agda.Syntax.Abstract.Pretty
    import Agda.Syntax.Abstract.UsedNames
    import Agda.Syntax.Internal as I
    import Agda.Syntax.Internal.Pattern as I
    import Agda.Syntax.Scope.Base (inverseScopeLookupName)

    import Agda.TypeChecking.Monad
    import Agda.TypeChecking.Reduce
    import {-# SOURCE #-} Agda.TypeChecking.Records
    import Agda.TypeChecking.CompiledClause (CompiledClauses'(Fail))
    import Agda.TypeChecking.DisplayForm
    import Agda.TypeChecking.Level
    import {-# SOURCE #-} Agda.TypeChecking.Datatypes
    import Agda.TypeChecking.Free
    import Agda.TypeChecking.Substitute
    import Agda.TypeChecking.SyntacticEquality
    import Agda.TypeChecking.Telescope

    import Agda.Interaction.Options

    import Agda.Utils.Either
    import Agda.Utils.Functor
    import Agda.Utils.Lens
    import Agda.Utils.List
    import Agda.Utils.List1 (List1, pattern (:|))
    import qualified Agda.Utils.List1 as List1
    import qualified Agda.Utils.Maybe.Strict as Strict
    import Agda.Utils.Maybe
    import Agda.Utils.Monad
    import Agda.Utils.Null
    import Agda.Utils.Permutation
    import Agda.Syntax.Common.Pretty
    import Agda.Utils.Singleton
    import Agda.Utils.Size
    import Agda.Utils.Tuple

    import Agda.Utils.Impossible

    -- | Like @reify@ but instantiates blocking metas, useful for reporting.
    reifyUnblocked :: Reify i => i -> TCM (ReifiesTo i)
    reifyUnblocked :: forall i. Reify i => i -> TCM (ReifiesTo i)
    reifyUnblocked i
    t = Lens' TCState Bool
    -> (Bool -> Bool) -> TCMT IO (ReifiesTo i) -> TCMT IO (ReifiesTo i)
    forall a b. Lens' TCState a -> (a -> a) -> TCMT IO b -> TCMT IO b
    forall (m :: * -> *) a b.
    ReadTCState m =>
    Lens' TCState a -> (a -> a) -> m b -> m b
    locallyTCState (Bool -> f Bool) -> TCState -> f TCState
    Lens' TCState Bool
    stInstantiateBlocking (Bool -> Bool -> Bool
    forall a b. a -> b -> a
    const Bool
    True) (TCMT IO (ReifiesTo i) -> TCMT IO (ReifiesTo i))
    -> TCMT IO (ReifiesTo i) -> TCMT IO (ReifiesTo i)
    forall a b. (a -> b) -> a -> b
    $ i -> TCMT IO (ReifiesTo i)
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    forall (m :: * -> *). MonadReify m => i -> m (ReifiesTo i)
    reify i
    t

    -- Composition of reified applications ------------------------------------
    --UNUSED Liang-Ting 2019-07-16
    ---- | Drops hidden arguments unless --show-implicit.
    --napps :: Expr -> [NamedArg Expr] -> TCM Expr
    --napps e = nelims e . map I.Apply

    {-# SPECIALIZE apps :: Expr -> [Arg Expr] -> TCM Expr #-}
    -- | Drops hidden arguments unless --show-implicit.
    apps :: MonadReify m => Expr -> [Arg Expr] -> m Expr
    apps :: forall (m :: * -> *). MonadReify m => Expr -> [Arg Expr] -> m Expr
    apps Expr
    e = Expr -> [Elim' Expr] -> m Expr
    forall (m :: * -> *).
    MonadReify m =>
    Expr -> [Elim' Expr] -> m Expr
    elims Expr
    e ([Elim' Expr] -> m Expr)
    -> ([Arg Expr] -> [Elim' Expr]) -> [Arg Expr] -> m Expr
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Arg Expr -> Elim' Expr) -> [Arg Expr] -> [Elim' Expr]
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Expr -> Elim' Expr
    forall a. Arg a -> Elim' a
    I.Apply

    -- Composition of reified eliminations ------------------------------------

    {-# SPECIALIZE nelims :: Expr -> [I.Elim' (Named_ Expr)] -> TCM Expr #-}
    -- | Drops hidden arguments unless --show-implicit.
    nelims :: MonadReify m => Expr -> [I.Elim' (Named_ Expr)] -> m Expr
    nelims :: forall (m :: * -> *).
    MonadReify m =>
    Expr -> [Elim' (Named_ Expr)] -> m Expr
    nelims Expr
    e [] = Expr -> m Expr
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Expr
    e
    nelims Expr
    e (I.IApply Named_ Expr
    x Named_ Expr
    y Named_ Expr
    r : [Elim' (Named_ Expr)]
    es) =
      Expr -> [Elim' (Named_ Expr)] -> m Expr
    forall (m :: * -> *).
    MonadReify m =>
    Expr -> [Elim' (Named_ Expr)] -> m Expr
    nelims (AppInfo -> Expr -> Arg (Named_ Expr) -> Expr
    A.App AppInfo
    defaultAppInfo_ Expr
    e (Arg (Named_ Expr) -> Expr) -> Arg (Named_ Expr) -> Expr
    forall a b. (a -> b) -> a -> b
    $ Named_ Expr -> Arg (Named_ Expr)
    forall a. a -> Arg a
    defaultArg Named_ Expr
    r) [Elim' (Named_ Expr)]
    es
    nelims Expr
    e (I.Apply Arg (Named_ Expr)
    arg : [Elim' (Named_ Expr)]
    es) = do
      arg <- Arg (Named_ Expr) -> m (ReifiesTo (Arg (Named_ Expr)))
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    forall (m :: * -> *).
    MonadReify m =>
    Arg (Named_ Expr) -> m (ReifiesTo (Arg (Named_ Expr)))
    reify Arg (Named_ Expr)
    arg  -- This replaces the arg by _ if irrelevant
      dontShowImp <- not <$> showImplicitArguments
      let hd | Arg (Named_ Expr) -> Bool
    forall a. LensHiding a => a -> Bool
    notVisible Arg (Named_ Expr)
    arg Bool -> Bool -> Bool
    && Bool
    dontShowImp = Expr
    e
             | Bool
    otherwise                     = AppInfo -> Expr -> Arg (Named_ Expr) -> Expr
    A.App AppInfo
    defaultAppInfo_ Expr
    e Arg (Named_ Expr)
    arg
      nelims hd es
    nelims Expr
    e (I.Proj ProjOrigin
    ProjPrefix QName
    d : [Elim' (Named_ Expr)]
    es)             = Expr -> QName -> [Elim' (Named_ Expr)] -> m Expr
    forall (m :: * -> *).
    MonadReify m =>
    Expr -> QName -> [Elim' (Named_ Expr)] -> m Expr
    nelimsProjPrefix Expr
    e QName
    d [Elim' (Named_ Expr)]
    es
    nelims Expr
    e (I.Proj ProjOrigin
    o          QName
    d : [Elim' (Named_ Expr)]
    es) | Expr -> Bool
    isSelf Expr
    e  = Expr -> [Elim' (Named_ Expr)] -> m Expr
    forall (m :: * -> *).
    MonadReify m =>
    Expr -> [Elim' (Named_ Expr)] -> m Expr
    nelims (ProjOrigin -> AmbiguousQName -> Expr
    A.Proj ProjOrigin
    ProjPrefix (AmbiguousQName -> Expr) -> AmbiguousQName -> Expr
    forall a b. (a -> b) -> a -> b
    $ QName -> AmbiguousQName
    unambiguous QName
    d) [Elim' (Named_ Expr)]
    es
                                        | Bool
    otherwise =
      Expr -> [Elim' (Named_ Expr)] -> m Expr
    forall (m :: * -> *).
    MonadReify m =>
    Expr -> [Elim' (Named_ Expr)] -> m Expr
    nelims (AppInfo -> Expr -> Arg (Named_ Expr) -> Expr
    A.App AppInfo
    defaultAppInfo_ Expr
    e (Expr -> Arg (Named_ Expr)
    forall a. a -> NamedArg a
    defaultNamedArg (Expr -> Arg (Named_ Expr)) -> Expr -> Arg (Named_ Expr)
    forall a b. (a -> b) -> a -> b
    $ ProjOrigin -> AmbiguousQName -> Expr
    A.Proj ProjOrigin
    o (AmbiguousQName -> Expr) -> AmbiguousQName -> Expr
    forall a b. (a -> b) -> a -> b
    $ QName -> AmbiguousQName
    unambiguous QName
    d)) [Elim' (Named_ Expr)]
    es

    {-# SPECIALIZE nelimsProjPrefix :: Expr -> QName -> [I.Elim' (Named_ Expr)] -> TCM Expr #-}
    nelimsProjPrefix :: MonadReify m => Expr -> QName -> [I.Elim' (Named_ Expr)] -> m Expr
    nelimsProjPrefix :: forall (m :: * -> *).
    MonadReify m =>
    Expr -> QName -> [Elim' (Named_ Expr)] -> m Expr
    nelimsProjPrefix Expr
    e QName
    d [Elim' (Named_ Expr)]
    es =
      Expr -> [Elim' (Named_ Expr)] -> m Expr
    forall (m :: * -> *).
    MonadReify m =>
    Expr -> [Elim' (Named_ Expr)] -> m Expr
    nelims (AppInfo -> Expr -> Arg (Named_ Expr) -> Expr
    A.App AppInfo
    defaultAppInfo_ (ProjOrigin -> AmbiguousQName -> Expr
    A.Proj ProjOrigin
    ProjPrefix (AmbiguousQName -> Expr) -> AmbiguousQName -> Expr
    forall a b. (a -> b) -> a -> b
    $ QName -> AmbiguousQName
    unambiguous QName
    d) (Arg (Named_ Expr) -> Expr) -> Arg (Named_ Expr) -> Expr
    forall a b. (a -> b) -> a -> b
    $ Expr -> Arg (Named_ Expr)
    forall a. a -> NamedArg a
    defaultNamedArg Expr
    e) [Elim' (Named_ Expr)]
    es

    -- | If we are referencing the record from inside the record definition, we don't insert an
    -- | A.App
    isSelf :: Expr -> Bool
    isSelf :: Expr -> Bool
    isSelf = \case
      A.Var Name
    n -> Name -> Bool
    nameIsRecordName Name
    n
      Expr
    _ -> Bool
    False

    {-# SPECIALIZE elims :: Expr -> [I.Elim' Expr] -> TCM Expr #-}
    -- | Drops hidden arguments unless --show-implicit.
    elims :: MonadReify m => Expr -> [I.Elim' Expr] -> m Expr
    elims :: forall (m :: * -> *).
    MonadReify m =>
    Expr -> [Elim' Expr] -> m Expr
    elims Expr
    e = Expr -> [Elim' (Named_ Expr)] -> m Expr
    forall (m :: * -> *).
    MonadReify m =>
    Expr -> [Elim' (Named_ Expr)] -> m Expr
    nelims Expr
    e ([Elim' (Named_ Expr)] -> m Expr)
    -> ([Elim' Expr] -> [Elim' (Named_ Expr)])
    -> [Elim' Expr]
    -> m Expr
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Elim' Expr -> Elim' (Named_ Expr))
    -> [Elim' Expr] -> [Elim' (Named_ Expr)]
    forall a b. (a -> b) -> [a] -> [b]
    map ((Expr -> Named_ Expr) -> Elim' Expr -> Elim' (Named_ Expr)
    forall a b. (a -> b) -> Elim' a -> Elim' b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Expr -> Named_ Expr
    forall a name. a -> Named name a
    unnamed)

    -- Omitting information ---------------------------------------------------

    noExprInfo :: ExprInfo
    noExprInfo :: ExprInfo
    noExprInfo = Range -> ExprInfo
    ExprRange Range
    forall a. Range' a
    noRange

    -- Conditional reification to omit terms that are not shown --------------

    {-# INLINE reifyWhenE #-}
    reifyWhenE :: (Reify i, MonadReify m, Underscore (ReifiesTo i)) => Bool -> i -> m (ReifiesTo i)
    reifyWhenE :: forall i (m :: * -> *).
    (Reify i, MonadReify m, Underscore (ReifiesTo i)) =>
    Bool -> i -> m (ReifiesTo i)
    reifyWhenE Bool
    True  i
    i = i -> m (ReifiesTo i)
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    forall (m :: * -> *). MonadReify m => i -> m (ReifiesTo i)
    reify i
    i
    reifyWhenE Bool
    False i
    t = ReifiesTo i -> m (ReifiesTo i)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ReifiesTo i
    forall a. Underscore a => a
    underscore

    -- Reification ------------------------------------------------------------

    type MonadReify m =
      ( PureTCM m
      , MonadInteractionPoints m
      , MonadFresh NameId m
      )

    class Reify i where
        type ReifiesTo i

        reify :: MonadReify m => i -> m (ReifiesTo i)

        --   @reifyWhen False@ should produce an 'underscore'.
        --   This function serves to reify hidden/irrelevant things.
        reifyWhen :: MonadReify m => Bool -> i -> m (ReifiesTo i)
        reifyWhen Bool
    _ = i -> m (ReifiesTo i)
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    forall (m :: * -> *). MonadReify m => i -> m (ReifiesTo i)
    reify

    instance Reify Bool where
        type ReifiesTo Bool = Bool
        reify :: forall (m :: * -> *). MonadReify m => Bool -> m (ReifiesTo Bool)
    reify = Bool -> m Bool
    Bool -> m (ReifiesTo Bool)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return

    instance Reify Char where
        type ReifiesTo Char = Char
        reify :: forall (m :: * -> *). MonadReify m => Char -> m (ReifiesTo Char)
    reify = Char -> m Char
    Char -> m (ReifiesTo Char)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return

    instance Reify Name where
        type ReifiesTo Name = Name
        reify :: forall (m :: * -> *). MonadReify m => Name -> m (ReifiesTo Name)
    reify = Name -> m Name
    Name -> m (ReifiesTo Name)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return

    instance Reify Expr where
        type ReifiesTo Expr = Expr

        reifyWhen :: forall (m :: * -> *).
    MonadReify m =>
    Bool -> Expr -> m (ReifiesTo Expr)
    reifyWhen = Bool -> Expr -> m (ReifiesTo Expr)
    forall i (m :: * -> *).
    (Reify i, MonadReify m, Underscore (ReifiesTo i)) =>
    Bool -> i -> m (ReifiesTo i)
    reifyWhenE
        reify :: forall (m :: * -> *). MonadReify m => Expr -> m (ReifiesTo Expr)
    reify = Expr -> m Expr
    Expr -> m (ReifiesTo Expr)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return

    instance Reify MetaId where
        type ReifiesTo MetaId = Expr

        reifyWhen :: forall (m :: * -> *).
    MonadReify m =>
    Bool -> MetaId -> m (ReifiesTo MetaId)
    reifyWhen = Bool -> MetaId -> m (ReifiesTo MetaId)
    forall i (m :: * -> *).
    (Reify i, MonadReify m, Underscore (ReifiesTo i)) =>
    Bool -> i -> m (ReifiesTo i)
    reifyWhenE
        reify :: forall (m :: * -> *).
    MonadReify m =>
    MetaId -> m (ReifiesTo MetaId)
    reify MetaId
    x = do
          b <- (TCEnv -> Bool) -> m Bool
    forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
    asksTC TCEnv -> Bool
    envPrintMetasBare
          mvar <- lookupLocalMeta x
          let mi  = MetaVariable -> MetaInfo
    mvInfo MetaVariable
    mvar
          let mi' = Info.MetaInfo
                     { metaRange :: Range
    metaRange          = Closure Range -> Range
    forall a. HasRange a => a -> Range
    getRange (Closure Range -> Range) -> Closure Range -> Range
    forall a b. (a -> b) -> a -> b
    $ MetaInfo -> Closure Range
    miClosRange MetaInfo
    mi
                     , metaScope :: ScopeInfo
    metaScope          = Closure Range -> ScopeInfo
    forall a. Closure a -> ScopeInfo
    clScope (Closure Range -> ScopeInfo) -> Closure Range -> ScopeInfo
    forall a b. (a -> b) -> a -> b
    $ MetaInfo -> Closure Range
    miClosRange MetaInfo
    mi
                     , metaNumber :: Maybe MetaId
    metaNumber         = if Bool
    b then Maybe MetaId
    forall a. Maybe a
    Nothing else MetaId -> Maybe MetaId
    forall a. a -> Maybe a
    Just MetaId
    x
                     , metaNameSuggestion :: MetaNameSuggestion
    metaNameSuggestion = if Bool
    b then MetaNameSuggestion
    "" else MetaInfo -> MetaNameSuggestion
    miNameSuggestion MetaInfo
    mi
                     , metaKind :: MetaKind
    metaKind           =  MetaInstantiation -> MetaKind
    metaInstantiationToMetaKind (MetaVariable -> MetaInstantiation
    mvInstantiation MetaVariable
    mvar)
                     }
              underscore = Expr -> m Expr
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Expr -> m Expr) -> Expr -> m Expr
    forall a b. (a -> b) -> a -> b
    $ MetaInfo -> Expr
    A.Underscore MetaInfo
    mi'
          -- If we are printing a term that will be pasted into the user
          -- source, we turn all unsolved (non-interaction) metas into
          -- interaction points
          isInteractionMeta x >>= \case
            Maybe InteractionId
    Nothing | Bool
    b -> do
              ii <- Bool -> Range -> Maybe Nat -> m InteractionId
    forall (m :: * -> *).
    MonadInteractionPoints m =>
    Bool -> Range -> Maybe Nat -> m InteractionId
    registerInteractionPoint Bool
    False Range
    forall a. Range' a
    noRange Maybe Nat
    forall a. Maybe a
    Nothing
              connectInteractionPoint ii x
              return $ A.QuestionMark mi' ii
            Just InteractionId
    ii | Bool
    b -> m Expr
    underscore
            Maybe InteractionId
    Nothing     -> m Expr
    underscore
            Just InteractionId
    ii     -> Expr -> m Expr
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Expr -> m Expr) -> Expr -> m Expr
    forall a b. (a -> b) -> a -> b
    $ MetaInfo -> InteractionId -> Expr
    A.QuestionMark MetaInfo
    mi' InteractionId
    ii
    {-# SPECIALIZE reify :: MetaId -> TCM (ReifiesTo MetaId) #-}

    instance Reify DisplayTerm where
      type ReifiesTo DisplayTerm = Expr

      reifyWhen :: forall (m :: * -> *).
    MonadReify m =>
    Bool -> DisplayTerm -> m (ReifiesTo DisplayTerm)
    reifyWhen = Bool -> DisplayTerm -> m (ReifiesTo DisplayTerm)
    forall i (m :: * -> *).
    (Reify i, MonadReify m, Underscore (ReifiesTo i)) =>
    Bool -> i -> m (ReifiesTo i)
    reifyWhenE
      reify :: forall (m :: * -> *).
    MonadReify m =>
    DisplayTerm -> m (ReifiesTo DisplayTerm)
    reify = \case
        DTerm' Term
    v Elims
    es       -> Expr -> [Elim' Expr] -> m Expr
    forall (m :: * -> *).
    MonadReify m =>
    Expr -> [Elim' Expr] -> m Expr
    elims (Expr -> [Elim' Expr] -> m Expr)
    -> (m Expr, m [Elim' Expr]) -> m Expr
    forall (m :: * -> *) a b c.
    Monad m =>
    (a -> b -> m c) -> (m a, m b) -> m c
    ==<< (Bool -> Term -> m Expr
    forall (m :: * -> *). MonadReify m => Bool -> Term -> m Expr
    reifyTerm Bool
    False Term
    v, Elims -> m (ReifiesTo Elims)
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    forall (m :: * -> *). MonadReify m => Elims -> m (ReifiesTo Elims)
    reify Elims
    es)
        DDot'  Term
    v Elims
    es       -> Expr -> [Elim' Expr] -> m Expr
    forall (m :: * -> *).
    MonadReify m =>
    Expr -> [Elim' Expr] -> m Expr
    elims (Expr -> [Elim' Expr] -> m Expr)
    -> (m Expr, m [Elim' Expr]) -> m Expr
    forall (m :: * -> *) a b c.
    Monad m =>
    (a -> b -> m c) -> (m a, m b) -> m c
    ==<< (Term -> m (ReifiesTo Term)
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    forall (m :: * -> *). MonadReify m => Term -> m (ReifiesTo Term)
    reify Term
    v, Elims -> m (ReifiesTo Elims)
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    forall (m :: * -> *). MonadReify m => Elims -> m (ReifiesTo Elims)
    reify Elims
    es)
        DCon ConHead
    c ConInfo
    ci [Arg DisplayTerm]
    vs      -> QName -> ConInfo -> [Arg Expr] -> m Expr
    forall (m :: * -> *).
    MonadReify m =>
    QName -> ConInfo -> [Arg Expr] -> m Expr
    recOrCon (ConHead -> QName
    conName ConHead
    c) ConInfo
    ci ([Arg Expr] -> m Expr) -> m [Arg Expr] -> m Expr
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< [Arg DisplayTerm] -> m (ReifiesTo [Arg DisplayTerm])
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    forall (m :: * -> *).
    MonadReify m =>
    [Arg DisplayTerm] -> m (ReifiesTo [Arg DisplayTerm])
    reify [Arg DisplayTerm]
    vs
        DDef QName
    f [Elim' DisplayTerm]
    es         -> Expr -> [Elim' Expr] -> m Expr
    forall (m :: * -> *).
    MonadReify m =>
    Expr -> [Elim' Expr] -> m Expr
    elims (QName -> Expr
    A.Def QName
    f) ([Elim' Expr] -> m Expr) -> m [Elim' Expr] -> m Expr
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< [Elim' DisplayTerm] -> m (ReifiesTo [Elim' DisplayTerm])
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    forall (m :: * -> *).
    MonadReify m =>
    [Elim' DisplayTerm] -> m (ReifiesTo [Elim' DisplayTerm])
    reify [Elim' DisplayTerm]
    es
        DWithApp DisplayTerm
    u List1 DisplayTerm
    us Elims
    es0 -> do
          (e, es) <- (DisplayTerm, List1 DisplayTerm)
    -> m (ReifiesTo (DisplayTerm, List1 DisplayTerm))
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    forall (m :: * -> *).
    MonadReify m =>
    (DisplayTerm, List1 DisplayTerm)
    -> m (ReifiesTo (DisplayTerm, List1 DisplayTerm))
    reify (DisplayTerm
    u, List1 DisplayTerm
    us)
          elims (A.WithApp noExprInfo e es) =<< reify es0
    {-# SPECIALIZE reify :: DisplayTerm -> TCM (ReifiesTo DisplayTerm) #-}

    {-# SPECIALIZE reifyDisplayForm :: QName -> I.Elims -> TCM A.Expr -> TCM A.Expr #-}
    -- | @reifyDisplayForm f vs fallback@
    --   tries to rewrite @f vs@ with a display form for @f@.
    --   If successful, reifies the resulting display term,
    --   otherwise, does @fallback@.
    reifyDisplayForm :: MonadReify m => QName -> I.Elims -> m A.Expr -> m A.Expr
    reifyDisplayForm :: forall (m :: * -> *).
    MonadReify m =>
    QName -> Elims -> m Expr -> m Expr
    reifyDisplayForm QName
    f Elims
    es m Expr
    fallback =
      m Bool -> m Expr -> m Expr -> m Expr
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
    ifNotM m Bool
    forall (m :: * -> *). MonadTCEnv m => m Bool
    displayFormsEnabled m Expr
    fallback (m Expr -> m Expr) -> m Expr -> m Expr
    forall a b. (a -> b) -> a -> b
    $ {- else -}
        m (Maybe DisplayTerm)
    -> m Expr -> (DisplayTerm -> m Expr) -> m Expr
    forall (m :: * -> *) a b.
    Monad m =>
    m (Maybe a) -> m b -> (a -> m b) -> m b
    caseMaybeM (QName -> Elims -> m (Maybe DisplayTerm)
    forall (m :: * -> *).
    MonadDisplayForm m =>
    QName -> Elims -> m (Maybe DisplayTerm)
    displayForm QName
    f Elims
    es) m Expr
    fallback DisplayTerm -> m Expr
    DisplayTerm -> m (ReifiesTo DisplayTerm)
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    forall (m :: * -> *).
    MonadReify m =>
    DisplayTerm -> m (ReifiesTo DisplayTerm)
    reify

    {-# SPECIALIZE reifyDisplayFormP :: QName -> A.Patterns -> A.Patterns -> TCM (QName, A.Patterns) #-}
    -- | @reifyDisplayFormP@ tries to recursively
    --   rewrite a lhs with a display form.
    --
    --   Note: we are not necessarily in the empty context upon entry!
    reifyDisplayFormP ::
         forall m.
         MonadReify m
      => QName         -- ^ LHS head symbol
      -> A.Patterns    -- ^ Patterns to be taken into account to find display form.
      -> A.Patterns    -- ^ Remaining trailing patterns ("with patterns").
      -> m (QName, A.Patterns) -- ^ New head symbol and new patterns.
    reifyDisplayFormP :: forall (m :: * -> *).
    MonadReify m =>
    QName -> Patterns -> Patterns -> m (QName, Patterns)
    reifyDisplayFormP QName
    f Patterns
    ps Patterns
    wps = do
      let fallback :: m (QName, Patterns)
    fallback = (QName, Patterns) -> m (QName, Patterns)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (QName
    f, Patterns
    ps Patterns -> Patterns -> Patterns
    forall a. [a] -> [a] -> [a]
    ++ Patterns
    wps)
      m Bool
    -> m (QName, Patterns)
    -> m (QName, Patterns)
    -> m (QName, Patterns)
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
    ifNotM m Bool
    forall (m :: * -> *). MonadTCEnv m => m Bool
    displayFormsEnabled m (QName, Patterns)
    fallback (m (QName, Patterns) -> m (QName, Patterns))
    -> m (QName, Patterns) -> m (QName, Patterns)
    forall a b. (a -> b) -> a -> b
    $ {- else -} do
        -- Try to rewrite @f 0 1 2 ... |ps|-1@ to a dt.
        -- Andreas, 2014-06-11  Issue 1177:
        -- I thought we need to add the placeholders for ps to the context,
        -- because otherwise displayForm will not raise the display term
        -- and we will have variable clashes.
        -- But apparently, it has no influence...
        -- Ulf, can you add an explanation?
        md <- -- addContext (replicate (length ps) "x") $
          QName -> Elims -> m (Maybe DisplayTerm)
    forall (m :: * -> *).
    MonadDisplayForm m =>
    QName -> Elims -> m (Maybe DisplayTerm)
    displayForm QName
    f (Elims -> m (Maybe DisplayTerm)) -> Elims -> m (Maybe DisplayTerm)
    forall a b. (a -> b) -> a -> b
    $ (Arg (Named_ Pattern) -> Nat -> Elim' Term)
    -> Patterns -> [Nat] -> Elims
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith (\ Arg (Named_ Pattern)
    p Nat
    i -> Arg Term -> Elim' Term
    forall a. Arg a -> Elim' a
    I.Apply (Arg Term -> Elim' Term) -> Arg Term -> Elim' Term
    forall a b. (a -> b) -> a -> b
    $ Arg (Named_ Pattern)
    p Arg (Named_ Pattern) -> Term -> Arg Term
    forall (f :: * -> *) a b. Functor f => f a -> b -> f b
    $> Nat -> Term
    I.var Nat
    i) Patterns
    ps [Nat
    0..]
        reportSLn "reify.display" 60 $
          "display form of " ++ prettyShow f ++ " " ++ show ps ++ " " ++ show wps ++ ":\n  " ++ show md
        case md of
          Just DisplayTerm
    d  | DisplayTerm -> Bool
    okDisplayForm DisplayTerm
    d -> do
            -- In the display term @d@, @var i@ should be a placeholder
            -- for the @i@th pattern of @ps@.
            -- Andreas, 2014-06-11:
            -- Are we sure that @d@ did not use @var i@ otherwise?
            (f', ps', wps') <- Patterns -> DisplayTerm -> m (QName, Patterns, Patterns)
    MonadReify m =>
    Patterns -> DisplayTerm -> m (QName, Patterns, Patterns)
    displayLHS Patterns
    ps DisplayTerm
    d
            reportSDoc "reify.display" 70 $ do
              doc <- prettyA $ SpineLHS empty f' (ps' ++ wps' ++ wps)
              return $ vcat
                [ "rewritten lhs to"
                , "  lhs' = " <+> doc
                ]
            reifyDisplayFormP f' ps' (wps' ++ wps)
          Maybe DisplayTerm
    _ -> do
            MetaNameSuggestion -> Nat -> MetaNameSuggestion -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    MetaNameSuggestion -> Nat -> MetaNameSuggestion -> m ()
    reportSLn MetaNameSuggestion
    "reify.display" Nat
    70 (MetaNameSuggestion -> m ()) -> MetaNameSuggestion -> m ()
    forall a b. (a -> b) -> a -> b
    $ MetaNameSuggestion
    "display form absent or not valid as lhs"
            m (QName, Patterns)
    fallback
      where
        -- Andreas, 2015-05-03: Ulf, please comment on what
        -- is the idea behind okDisplayForm.
        -- Ulf, 2016-04-15: okDisplayForm should return True if the display form
        -- can serve as a valid left-hand side. That means checking that it is a
        -- defined name applied to valid lhs eliminators (projections or
        -- applications to constructor patterns).
        okDisplayForm :: DisplayTerm -> Bool
        okDisplayForm :: DisplayTerm -> Bool
    okDisplayForm = \case
          DWithApp DisplayTerm
    d List1 DisplayTerm
    ds Elims
    es ->
            DisplayTerm -> Bool
    okDisplayForm DisplayTerm
    d Bool -> Bool -> Bool
    && (DisplayTerm -> Bool) -> List1 DisplayTerm -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all DisplayTerm -> Bool
    okDisplayTerm List1 DisplayTerm
    ds  Bool -> Bool -> Bool
    && (Elim' Term -> Bool) -> Elims -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all Elim' Term -> Bool
    okToDropE Elims
    es
            -- Andreas, 2016-05-03, issue #1950.
            -- We might drop trailing hidden trivial (=variable) patterns.
          DTerm' (I.Def QName
    f Elims
    es') Elims
    es -> (Elim' Term -> Bool) -> Elims -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all Elim' Term -> Bool
    okElim Elims
    es' Bool -> Bool -> Bool
    && (Elim' Term -> Bool) -> Elims -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all Elim' Term -> Bool
    okElim Elims
    es
          DDef QName
    f [Elim' DisplayTerm]
    es               -> (Elim' DisplayTerm -> Bool) -> [Elim' DisplayTerm] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all Elim' DisplayTerm -> Bool
    okDElim [Elim' DisplayTerm]
    es
          DDot'{}                 -> Bool
    False
          DCon{}                  -> Bool
    False
          DTerm'{}                -> Bool
    False

        okDisplayTerm :: DisplayTerm -> Bool
        okDisplayTerm :: DisplayTerm -> Bool
    okDisplayTerm = \case
          DTerm' Term
    v Elims
    es -> Elims -> Bool
    forall a. Null a => a -> Bool
    null Elims
    es Bool -> Bool -> Bool
    && Term -> Bool
    okTerm Term
    v
          DDot'{}     -> Bool
    True
          DCon{}      -> Bool
    True
          DDef{}      -> Bool
    False
          DWithApp{}  -> Bool
    False

        okDElim :: Elim' DisplayTerm -> Bool
        okDElim :: Elim' DisplayTerm -> Bool
    okDElim (I.IApply DisplayTerm
    x DisplayTerm
    y DisplayTerm
    r) = DisplayTerm -> Bool
    okDisplayTerm DisplayTerm
    r
        okDElim (I.Apply Arg DisplayTerm
    v) = DisplayTerm -> Bool
    okDisplayTerm (DisplayTerm -> Bool) -> DisplayTerm -> Bool
    forall a b. (a -> b) -> a -> b
    $ Arg DisplayTerm -> DisplayTerm
    forall e. Arg e -> e
    unArg Arg DisplayTerm
    v
        okDElim I.Proj{}    = Bool
    True

        okToDropE :: Elim' Term -> Bool
        okToDropE :: Elim' Term -> Bool
    okToDropE (I.Apply Arg Term
    v) = Arg Term -> Bool
    okToDrop Arg Term
    v
        okToDropE I.Proj{}    = Bool
    False
        okToDropE (I.IApply Term
    x Term
    y Term
    r) = Bool
    False

        okToDrop :: Arg I.Term -> Bool
        okToDrop :: Arg Term -> Bool
    okToDrop Arg Term
    arg = Arg Term -> Bool
    forall a. LensHiding a => a -> Bool
    notVisible Arg Term
    arg Bool -> Bool -> Bool
    && case Arg Term -> Term
    forall e. Arg e -> e
    unArg Arg Term
    arg of
          I.Var Nat
    _ []   -> Bool
    True
          I.DontCare{} -> Bool
    True  -- no matching on irrelevant things.  __IMPOSSIBLE__ anyway?
          I.Level{}    -> Bool
    True  -- no matching on levels. __IMPOSSIBLE__ anyway?
          Term
    _ -> Bool
    False

        okArg :: Arg I.Term -> Bool
        okArg :: Arg Term -> Bool
    okArg = Term -> Bool
    okTerm (Term -> Bool) -> (Arg Term -> Term) -> Arg Term -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Arg Term -> Term
    forall e. Arg e -> e
    unArg

        okElim :: Elim' I.Term -> Bool
        okElim :: Elim' Term -> Bool
    okElim (I.IApply Term
    x Term
    y Term
    r) = Term -> Bool
    okTerm Term
    r
        okElim (I.Apply Arg Term
    a) = Arg Term -> Bool
    okArg Arg Term
    a
        okElim I.Proj{}  = Bool
    True

        okTerm :: I.Term -> Bool
        okTerm :: Term -> Bool
    okTerm (I.Var Nat
    _ []) = Bool
    True
        okTerm (I.Con ConHead
    c ConInfo
    ci Elims
    vs) = (Elim' Term -> Bool) -> Elims -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all Elim' Term -> Bool
    okElim Elims
    vs
        okTerm (I.Def QName
    x []) = QName -> Bool
    forall a. IsNoName a => a -> Bool
    isNoName (QName -> Bool) -> QName -> Bool
    forall a b. (a -> b) -> a -> b
    $ QName -> QName
    qnameToConcrete QName
    x -- Handling wildcards in display forms
        okTerm Term
    _            = Bool
    False

        -- Flatten a dt into (parentName, parentElims, withArgs).
        flattenWith :: DisplayTerm -> (QName, [I.Elim' DisplayTerm], [I.Elim' DisplayTerm])
        flattenWith :: DisplayTerm -> (QName, [Elim' DisplayTerm], [Elim' DisplayTerm])
    flattenWith (DWithApp DisplayTerm
    d List1 DisplayTerm
    ds1 Elims
    es2) =
          let (QName
    f, [Elim' DisplayTerm]
    es, [Elim' DisplayTerm]
    ds0) = DisplayTerm -> (QName, [Elim' DisplayTerm], [Elim' DisplayTerm])
    flattenWith DisplayTerm
    d
          in  (QName
    f, [Elim' DisplayTerm]
    es, [Elim' DisplayTerm]
    ds0 [Elim' DisplayTerm] -> [Elim' DisplayTerm] -> [Elim' DisplayTerm]
    forall a. [a] -> [a] -> [a]
    ++ (DisplayTerm -> Elim' DisplayTerm)
    -> [DisplayTerm] -> [Elim' DisplayTerm]
    forall a b. (a -> b) -> [a] -> [b]
    map (Arg DisplayTerm -> Elim' DisplayTerm
    forall a. Arg a -> Elim' a
    I.Apply (Arg DisplayTerm -> Elim' DisplayTerm)
    -> (DisplayTerm -> Arg DisplayTerm)
    -> DisplayTerm
    -> Elim' DisplayTerm
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . DisplayTerm -> Arg DisplayTerm
    forall a. a -> Arg a
    defaultArg) (List1 DisplayTerm -> [Item (List1 DisplayTerm)]
    forall l. IsList l => l -> [Item l]
    List1.toList List1 DisplayTerm
    ds1) [Elim' DisplayTerm] -> [Elim' DisplayTerm] -> [Elim' DisplayTerm]
    forall a. [a] -> [a] -> [a]
    ++ (Elim' Term -> Elim' DisplayTerm) -> Elims -> [Elim' DisplayTerm]
    forall a b. (a -> b) -> [a] -> [b]
    map ((Term -> DisplayTerm) -> Elim' Term -> Elim' DisplayTerm
    forall a b. (a -> b) -> Elim' a -> Elim' b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Term -> DisplayTerm
    DTerm) Elims
    es2)
        flattenWith (DDef QName
    f [Elim' DisplayTerm]
    es) = (QName
    f, [Elim' DisplayTerm]
    es, [])     -- .^ hacky, but we should only hit this when printing debug info
        flattenWith (DTerm' (I.Def QName
    f Elims
    es') Elims
    es) = (QName
    f, (Elim' Term -> Elim' DisplayTerm) -> Elims -> [Elim' DisplayTerm]
    forall a b. (a -> b) -> [a] -> [b]
    map ((Term -> DisplayTerm) -> Elim' Term -> Elim' DisplayTerm
    forall a b. (a -> b) -> Elim' a -> Elim' b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Term -> DisplayTerm
    DTerm) (Elims -> [Elim' DisplayTerm]) -> Elims -> [Elim' DisplayTerm]
    forall a b. (a -> b) -> a -> b
    $ Elims
    es' Elims -> Elims -> Elims
    forall a. [a] -> [a] -> [a]
    ++ Elims
    es, [])
        flattenWith DisplayTerm
    _ = (QName, [Elim' DisplayTerm], [Elim' DisplayTerm])
    forall a. HasCallStack => a
    __IMPOSSIBLE__

        displayLHS
          :: MonadReify m
          => A.Patterns   -- Patterns to substituted into display term.
          -> DisplayTerm  -- Display term.
          -> m (QName, A.Patterns, A.Patterns)  -- New head, patterns, with-patterns.
        displayLHS :: MonadReify m =>
    Patterns -> DisplayTerm -> m (QName, Patterns, Patterns)
    displayLHS Patterns
    ps DisplayTerm
    d = do
            let (QName
    f, [Elim' DisplayTerm]
    vs, [Elim' DisplayTerm]
    es) = DisplayTerm -> (QName, [Elim' DisplayTerm], [Elim' DisplayTerm])
    flattenWith DisplayTerm
    d
            ps  <- (Elim' DisplayTerm -> m (Arg (Named_ Pattern)))
    -> [Elim' DisplayTerm] -> m Patterns
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM MonadReify m => Elim' DisplayTerm -> m (Arg (Named_ Pattern))
    Elim' DisplayTerm -> m (Arg (Named_ Pattern))
    elimToPat [Elim' DisplayTerm]
    vs
            wps <- mapM (updateNamedArg (A.WithP empty) <.> elimToPat) es
            return (f, ps, wps)
          where
            argToPat :: MonadReify m => Arg DisplayTerm -> m (NamedArg A.Pattern)
            argToPat :: MonadReify m => Arg DisplayTerm -> m (Arg (Named_ Pattern))
    argToPat Arg DisplayTerm
    arg = (DisplayTerm -> m (Named_ Pattern))
    -> Arg DisplayTerm -> m (Arg (Named_ Pattern))
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Arg a -> f (Arg b)
    traverse MonadReify m => DisplayTerm -> m (Named_ Pattern)
    DisplayTerm -> m (Named_ Pattern)
    termToPat Arg DisplayTerm
    arg

            elimToPat :: MonadReify m => I.Elim' DisplayTerm -> m (NamedArg A.Pattern)
            elimToPat :: MonadReify m => Elim' DisplayTerm -> m (Arg (Named_ Pattern))
    elimToPat (I.IApply DisplayTerm
    _ DisplayTerm
    _ DisplayTerm
    r) = MonadReify m => Arg DisplayTerm -> m (Arg (Named_ Pattern))
    Arg DisplayTerm -> m (Arg (Named_ Pattern))
    argToPat (ArgInfo -> DisplayTerm -> Arg DisplayTerm
    forall e. ArgInfo -> e -> Arg e
    Arg ArgInfo
    defaultArgInfo DisplayTerm
    r)
            elimToPat (I.Apply Arg DisplayTerm
    arg) = MonadReify m => Arg DisplayTerm -> m (Arg (Named_ Pattern))
    Arg DisplayTerm -> m (Arg (Named_ Pattern))
    argToPat Arg DisplayTerm
    arg
            elimToPat (I.Proj ProjOrigin
    o QName
    d)  = Arg (Named_ Pattern) -> m (Arg (Named_ Pattern))
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Arg (Named_ Pattern) -> m (Arg (Named_ Pattern)))
    -> Arg (Named_ Pattern) -> m (Arg (Named_ Pattern))
    forall a b. (a -> b) -> a -> b
    $ Pattern -> Arg (Named_ Pattern)
    forall a. a -> NamedArg a
    defaultNamedArg (Pattern -> Arg (Named_ Pattern))
    -> Pattern -> Arg (Named_ Pattern)
    forall a b. (a -> b) -> a -> b
    $ PatInfo -> ProjOrigin -> AmbiguousQName -> Pattern
    forall e. PatInfo -> ProjOrigin -> AmbiguousQName -> Pattern' e
    A.ProjP PatInfo
    patNoRange ProjOrigin
    o (AmbiguousQName -> Pattern) -> AmbiguousQName -> Pattern
    forall a b. (a -> b) -> a -> b
    $ QName -> AmbiguousQName
    unambiguous QName
    d

            -- Substitute variables in display term by patterns.
            termToPat :: MonadReify m => DisplayTerm -> m (Named_ A.Pattern)

            -- Main action HERE:
            termToPat :: MonadReify m => DisplayTerm -> m (Named_ Pattern)
    termToPat (DTerm (I.Var Nat
    n [])) =
              Named_ Pattern -> m (Named_ Pattern)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Named_ Pattern -> m (Named_ Pattern))
    -> Named_ Pattern -> m (Named_ Pattern)
    forall a b. (a -> b) -> a -> b
    $ Arg (Named_ Pattern) -> Named_ Pattern
    forall e. Arg e -> e
    unArg (Arg (Named_ Pattern) -> Named_ Pattern)
    -> Arg (Named_ Pattern) -> Named_ Pattern
    forall a b. (a -> b) -> a -> b
    $ Arg (Named_ Pattern)
    -> Maybe (Arg (Named_ Pattern)) -> Arg (Named_ Pattern)
    forall a. a -> Maybe a -> a
    fromMaybe Arg (Named_ Pattern)
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe (Arg (Named_ Pattern)) -> Arg (Named_ Pattern))
    -> Maybe (Arg (Named_ Pattern)) -> Arg (Named_ Pattern)
    forall a b. (a -> b) -> a -> b
    $ Patterns
    ps Patterns -> Nat -> Maybe (Arg (Named_ Pattern))
    forall a. [a] -> Nat -> Maybe a
    !!! Nat
    n

            termToPat (DCon ConHead
    c ConInfo
    ci [Arg DisplayTerm]
    vs)          = (Pattern -> Named_ Pattern) -> m Pattern -> m (Named_ Pattern)
    forall a b. (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Pattern -> Named_ Pattern
    forall a name. a -> Named name a
    unnamed (m Pattern -> m (Named_ Pattern))
    -> (Pattern -> m Pattern) -> Pattern -> m (Named_ Pattern)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Pattern -> m Pattern
    forall (m :: * -> *). MonadReify m => Pattern -> m Pattern
    tryRecPFromConP (Pattern -> m (Named_ Pattern)) -> m Pattern -> m (Named_ Pattern)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< do
               ConPatInfo -> AmbiguousQName -> Patterns -> Pattern
    forall e. ConPatInfo -> AmbiguousQName -> NAPs e -> Pattern' e
    A.ConP (ConInfo -> PatInfo -> ConPatLazy -> ConPatInfo
    ConPatInfo ConInfo
    ci PatInfo
    patNoRange ConPatLazy
    ConPatEager) (QName -> AmbiguousQName
    unambiguous (ConHead -> QName
    conName ConHead
    c)) (Patterns -> Pattern) -> m Patterns -> m Pattern
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Arg DisplayTerm -> m (Arg (Named_ Pattern)))
    -> [Arg DisplayTerm] -> m Patterns
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM MonadReify m => Arg DisplayTerm -> m (Arg (Named_ Pattern))
    Arg DisplayTerm -> m (Arg (Named_ Pattern))
    argToPat [Arg DisplayTerm]
    vs

            termToPat (DTerm' (I.Con ConHead
    c ConInfo
    ci Elims
    vs) Elims
    es) = (Pattern -> Named_ Pattern) -> m Pattern -> m (Named_ Pattern)
    forall a b. (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Pattern -> Named_ Pattern
    forall a name. a -> Named name a
    unnamed (m Pattern -> m (Named_ Pattern))
    -> (Pattern -> m Pattern) -> Pattern -> m (Named_ Pattern)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Pattern -> m Pattern
    forall (m :: * -> *). MonadReify m => Pattern -> m Pattern
    tryRecPFromConP (Pattern -> m (Named_ Pattern)) -> m Pattern -> m (Named_ Pattern)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< do
               ConPatInfo -> AmbiguousQName -> Patterns -> Pattern
    forall e. ConPatInfo -> AmbiguousQName -> NAPs e -> Pattern' e
    A.ConP (ConInfo -> PatInfo -> ConPatLazy -> ConPatInfo
    ConPatInfo ConInfo
    ci PatInfo
    patNoRange ConPatLazy
    ConPatEager) (QName -> AmbiguousQName
    unambiguous (ConHead -> QName
    conName ConHead
    c)) (Patterns -> Pattern) -> m Patterns -> m Pattern
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$>
                 (Elim' Term -> m (Arg (Named_ Pattern))) -> Elims -> m Patterns
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM (MonadReify m => Elim' DisplayTerm -> m (Arg (Named_ Pattern))
    Elim' DisplayTerm -> m (Arg (Named_ Pattern))
    elimToPat (Elim' DisplayTerm -> m (Arg (Named_ Pattern)))
    -> (Elim' Term -> Elim' DisplayTerm)
    -> Elim' Term
    -> m (Arg (Named_ Pattern))
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Term -> DisplayTerm) -> Elim' Term -> Elim' DisplayTerm
    forall a b. (a -> b) -> Elim' a -> Elim' b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Term -> DisplayTerm
    DTerm) (Elims
    vs Elims -> Elims -> Elims
    forall a. [a] -> [a] -> [a]
    ++ Elims
    es)

            termToPat (DTerm (I.Def QName
    _ [])) = Named_ Pattern -> m (Named_ Pattern)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Named_ Pattern -> m (Named_ Pattern))
    -> Named_ Pattern -> m (Named_ Pattern)
    forall a b. (a -> b) -> a -> b
    $ Pattern -> Named_ Pattern
    forall a name. a -> Named name a
    unnamed (Pattern -> Named_ Pattern) -> Pattern -> Named_ Pattern
    forall a b. (a -> b) -> a -> b
    $ PatInfo -> Pattern
    forall e. PatInfo -> Pattern' e
    A.WildP PatInfo
    patNoRange
            termToPat (DDef QName
    _ [])          = Named_ Pattern -> m (Named_ Pattern)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Named_ Pattern -> m (Named_ Pattern))
    -> Named_ Pattern -> m (Named_ Pattern)
    forall a b. (a -> b) -> a -> b
    $ Pattern -> Named_ Pattern
    forall a name. a -> Named name a
    unnamed (Pattern -> Named_ Pattern) -> Pattern -> Named_ Pattern
    forall a b. (a -> b) -> a -> b
    $ PatInfo -> Pattern
    forall e. PatInfo -> Pattern' e
    A.WildP PatInfo
    patNoRange

            termToPat (DTerm (I.Lit Literal
    l))    = Named_ Pattern -> m (Named_ Pattern)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Named_ Pattern -> m (Named_ Pattern))
    -> Named_ Pattern -> m (Named_ Pattern)
    forall a b. (a -> b) -> a -> b
    $ Pattern -> Named_ Pattern
    forall a name. a -> Named name a
    unnamed (Pattern -> Named_ Pattern) -> Pattern -> Named_ Pattern
    forall a b. (a -> b) -> a -> b
    $ PatInfo -> Literal -> Pattern
    forall e. PatInfo -> Literal -> Pattern' e
    A.LitP PatInfo
    patNoRange Literal
    l

            termToPat (DDot' Term
    v Elims
    es) =
              Pattern -> Named_ Pattern
    forall a name. a -> Named name a
    unnamed (Pattern -> Named_ Pattern)
    -> (Expr -> Pattern) -> Expr -> Named_ Pattern
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PatInfo -> Expr -> Pattern
    forall e. PatInfo -> e -> Pattern' e
    A.DotP PatInfo
    patNoRange (Expr -> Named_ Pattern) -> m Expr -> m (Named_ Pattern)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> do Expr -> [Elim' Expr] -> m Expr
    forall (m :: * -> *).
    MonadReify m =>
    Expr -> [Elim' Expr] -> m Expr
    elims (Expr -> [Elim' Expr] -> m Expr)
    -> (m Expr, m [Elim' Expr]) -> m Expr
    forall (m :: * -> *) a b c.
    Monad m =>
    (a -> b -> m c) -> (m a, m b) -> m c
    ==<< (MonadReify m => Term -> m Expr
    Term -> m Expr
    termToExpr Term
    v, Elims -> m (ReifiesTo Elims)
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    forall (m :: * -> *). MonadReify m => Elims -> m (ReifiesTo Elims)
    reify Elims
    es)

            termToPat DisplayTerm
    v =
              Pattern -> Named_ Pattern
    forall a name. a -> Named name a
    unnamed (Pattern -> Named_ Pattern)
    -> (Expr -> Pattern) -> Expr -> Named_ Pattern
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PatInfo -> Expr -> Pattern
    forall e. PatInfo -> e -> Pattern' e
    A.DotP PatInfo
    patNoRange (Expr -> Named_ Pattern) -> m Expr -> m (Named_ Pattern)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> DisplayTerm -> m (ReifiesTo DisplayTerm)
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    forall (m :: * -> *).
    MonadReify m =>
    DisplayTerm -> m (ReifiesTo DisplayTerm)
    reify DisplayTerm
    v

            len :: Nat
    len = Patterns -> Nat
    forall a. [a] -> Nat
    forall (t :: * -> *) a. Foldable t => t a -> Nat
    length Patterns
    ps

            argsToExpr :: MonadReify m => I.Args -> m [Arg A.Expr]
            argsToExpr :: MonadReify m => Args -> m [Arg Expr]
    argsToExpr = (Arg Term -> m (Arg Expr)) -> Args -> m [Arg Expr]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM ((Term -> m Expr) -> Arg Term -> m (Arg Expr)
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Arg a -> f (Arg b)
    traverse MonadReify m => Term -> m Expr
    Term -> m Expr
    termToExpr)

            -- TODO: restructure this to avoid having to repeat the code for reify
            termToExpr :: MonadReify m => Term -> m A.Expr
            termToExpr :: MonadReify m => Term -> m Expr
    termToExpr Term
    v = do
              MetaNameSuggestion -> Nat -> MetaNameSuggestion -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    MetaNameSuggestion -> Nat -> MetaNameSuggestion -> m ()
    reportSLn MetaNameSuggestion
    "reify.display" Nat
    60 (MetaNameSuggestion -> m ()) -> MetaNameSuggestion -> m ()
    forall a b. (a -> b) -> a -> b
    $ MetaNameSuggestion
    "termToExpr " MetaNameSuggestion -> MetaNameSuggestion -> MetaNameSuggestion
    forall a. [a] -> [a] -> [a]
    ++ Term -> MetaNameSuggestion
    forall a. Show a => a -> MetaNameSuggestion
    show Term
    v
              -- After unSpine, a Proj elimination is __IMPOSSIBLE__!
              case Term -> Term
    unSpine Term
    v of
                I.Con ConHead
    c ConInfo
    ci Elims
    es -> do
                  let vs :: Args
    vs = Args -> Maybe Args -> Args
    forall a. a -> Maybe a -> a
    fromMaybe Args
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe Args -> Args) -> Maybe Args -> Args
    forall a b. (a -> b) -> a -> b
    $ (Elim' Term -> Maybe (Arg Term)) -> Elims -> Maybe Args
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM Elim' Term -> Maybe (Arg Term)
    forall a. Elim' a -> Maybe (Arg a)
    isApplyElim Elims
    es
                  Expr -> [Arg Expr] -> m Expr
    forall (m :: * -> *). MonadReify m => Expr -> [Arg Expr] -> m Expr
    apps (AmbiguousQName -> Expr
    A.Con (QName -> AmbiguousQName
    unambiguous (ConHead -> QName
    conName ConHead
    c))) ([Arg Expr] -> m Expr) -> m [Arg Expr] -> m Expr
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Args -> m [Arg Expr]
    MonadReify m => Args -> m [Arg Expr]
    argsToExpr Args
    vs
                I.Def QName
    f Elims
    es -> do
                  let vs :: Args
    vs = Args -> Maybe Args -> Args
    forall a. a -> Maybe a -> a
    fromMaybe Args
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe Args -> Args) -> Maybe Args -> Args
    forall a b. (a -> b) -> a -> b
    $ (Elim' Term -> Maybe (Arg Term)) -> Elims -> Maybe Args
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM Elim' Term -> Maybe (Arg Term)
    forall a. Elim' a -> Maybe (Arg a)
    isApplyElim Elims
    es
                  Expr -> [Arg Expr] -> m Expr
    forall (m :: * -> *). MonadReify m => Expr -> [Arg Expr] -> m Expr
    apps (QName -> Expr
    A.Def QName
    f) ([Arg Expr] -> m Expr) -> m [Arg Expr] -> m Expr
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Args -> m [Arg Expr]
    MonadReify m => Args -> m [Arg Expr]
    argsToExpr Args
    vs
                I.Var Nat
    n Elims
    es -> do
                  let vs :: Args
    vs = Args -> Maybe Args -> Args
    forall a. a -> Maybe a -> a
    fromMaybe Args
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe Args -> Args) -> Maybe Args -> Args
    forall a b. (a -> b) -> a -> b
    $ (Elim' Term -> Maybe (Arg Term)) -> Elims -> Maybe Args
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM Elim' Term -> Maybe (Arg Term)
    forall a. Elim' a -> Maybe (Arg a)
    isApplyElim Elims
    es
                  -- Andreas, 2014-06-11  Issue 1177
                  -- due to β-normalization in substitution,
                  -- even the pattern variables @n < len@ can be
                  -- applied to some args @vs@.
                  e <- if Nat
    n Nat -> Nat -> Bool
    forall a. Ord a => a -> a -> Bool
    < Nat
    len
                       then Expr -> m Expr
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Expr -> m Expr) -> Expr -> m Expr
    forall a b. (a -> b) -> a -> b
    $ Pattern -> Expr
    patternToExpr (Pattern -> Expr) -> Pattern -> Expr
    forall a b. (a -> b) -> a -> b
    $ Arg (Named_ Pattern) -> Pattern
    forall a. NamedArg a -> a
    namedArg (Arg (Named_ Pattern) -> Pattern)
    -> Arg (Named_ Pattern) -> Pattern
    forall a b. (a -> b) -> a -> b
    $ Arg (Named_ Pattern) -> Patterns -> Nat -> Arg (Named_ Pattern)
    forall a. a -> [a] -> Nat -> a
    indexWithDefault Arg (Named_ Pattern)
    forall a. HasCallStack => a
    __IMPOSSIBLE__ Patterns
    ps Nat
    n
                       else Term -> m (ReifiesTo Term)
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    forall (m :: * -> *). MonadReify m => Term -> m (ReifiesTo Term)
    reify (Nat -> Term
    I.var (Nat
    n Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    - Nat
    len))
                  apps e =<< argsToExpr vs
                Term
    _ -> Expr -> m Expr
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Expr
    forall a. Underscore a => a
    underscore

    instance Reify Literal where
      type ReifiesTo Literal = Expr

      reifyWhen :: forall (m :: * -> *).
    MonadReify m =>
    Bool -> Literal -> m (ReifiesTo Literal)
    reifyWhen = Bool -> Literal -> m (ReifiesTo Literal)
    forall i (m :: * -> *).
    (Reify i, MonadReify m, Underscore (ReifiesTo i)) =>
    Bool -> i -> m (ReifiesTo i)
    reifyWhenE
      reify :: forall (m :: * -> *).
    MonadReify m =>
    Literal -> m (ReifiesTo Literal)
    reify Literal
    l = Expr -> m Expr
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Expr -> m Expr) -> Expr -> m Expr
    forall a b. (a -> b) -> a -> b
    $ ExprInfo -> Literal -> Expr
    A.Lit ExprInfo
    forall a. Null a => a
    empty Literal
    l; {-# INLINE reify #-}

    instance Reify Term where
      type ReifiesTo Term = Expr

      reifyWhen :: forall (m :: * -> *).
    MonadReify m =>
    Bool -> Term -> m (ReifiesTo Term)
    reifyWhen = Bool -> Term -> m (ReifiesTo Term)
    forall i (m :: * -> *).
    (Reify i, MonadReify m, Underscore (ReifiesTo i)) =>
    Bool -> i -> m (ReifiesTo i)
    reifyWhenE
      reify :: forall (m :: * -> *). MonadReify m => Term -> m (ReifiesTo Term)
    reify Term
    v = Bool -> Term -> m Expr
    forall (m :: * -> *). MonadReify m => Bool -> Term -> m Expr
    reifyTerm Bool
    True Term
    v; {-# INLINE reify #-}

    {-# SPECIALIZE reifyPathPConstAsPath :: QName -> Elims -> TCM (QName, Elims) #-}
    reifyPathPConstAsPath :: MonadReify m => QName -> Elims -> m (QName, Elims)
    reifyPathPConstAsPath :: forall (m :: * -> *).
    MonadReify m =>
    QName -> Elims -> m (QName, Elims)
    reifyPathPConstAsPath QName
    x es :: Elims
    es@[I.Apply Arg Term
    l, I.Apply Arg Term
    t, I.Apply Arg Term
    lhs, I.Apply Arg Term
    rhs] = do
       MetaNameSuggestion -> Nat -> MetaNameSuggestion -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    MetaNameSuggestion -> Nat -> MetaNameSuggestion -> m ()
    reportSLn MetaNameSuggestion
    "reify.def" Nat
    100 (MetaNameSuggestion -> m ()) -> MetaNameSuggestion -> m ()
    forall a b. (a -> b) -> a -> b
    $ MetaNameSuggestion
    "reifying def path " MetaNameSuggestion -> MetaNameSuggestion -> MetaNameSuggestion
    forall a. [a] -> [a] -> [a]
    ++ (QName, Elims) -> MetaNameSuggestion
    forall a. Show a => a -> MetaNameSuggestion
    show (QName
    x,Elims
    es)
       mpath  <- BuiltinId -> m (Maybe QName)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe QName)
    getBuiltinName' BuiltinId
    builtinPath
       mpathp <- getBuiltinName' builtinPathP
       let fallback = (QName, Elims) -> m (QName, Elims)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (QName
    x,Elims
    es)
       case (,) <$> mpath <*> mpathp of
         Just (QName
    path,QName
    pathp) | QName
    x QName -> QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == QName
    pathp -> do
           let a :: Maybe Term
    a = case Arg Term -> Term
    forall e. Arg e -> e
    unArg Arg Term
    t of
                    I.Lam ArgInfo
    _ (NoAbs MetaNameSuggestion
    _ Term
    b)    -> Term -> Maybe Term
    forall a. a -> Maybe a
    Just Term
    b
                    I.Lam ArgInfo
    _ (Abs   MetaNameSuggestion
    _ Term
    b)
                      | Bool -> Bool
    not (Bool -> Bool) -> Bool -> Bool
    forall a b. (a -> b) -> a -> b
    $ Nat
    0 Nat -> Term -> Bool
    forall a. Free a => Nat -> a -> Bool
    `freeIn` Term
    b -> Term -> Maybe Term
    forall a. a -> Maybe a
    Just (Impossible -> Term -> Term
    forall a. Subst a => Impossible -> a -> a
    strengthen Impossible
    HasCallStack => Impossible
    impossible Term
    b)
                    Term
    _                      -> Maybe Term
    forall a. Maybe a
    Nothing
           case Maybe Term
    a of
             Just Term
    a -> (QName, Elims) -> m (QName, Elims)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (QName
    path, [Arg Term -> Elim' Term
    forall a. Arg a -> Elim' a
    I.Apply Arg Term
    l, Arg Term -> Elim' Term
    forall a. Arg a -> Elim' a
    I.Apply (Hiding -> Arg Term -> Arg Term
    forall a. LensHiding a => Hiding -> a -> a
    setHiding Hiding
    Hidden (Arg Term -> Arg Term) -> Arg Term -> Arg Term
    forall a b. (a -> b) -> a -> b
    $ Term -> Arg Term
    forall a. a -> Arg a
    defaultArg Term
    a), Arg Term -> Elim' Term
    forall a. Arg a -> Elim' a
    I.Apply Arg Term
    lhs, Arg Term -> Elim' Term
    forall a. Arg a -> Elim' a
    I.Apply Arg Term
    rhs])
             Maybe Term
    Nothing -> m (QName, Elims)
    fallback
         Maybe (QName, QName)
    _ -> m (QName, Elims)
    fallback
    reifyPathPConstAsPath QName
    x Elims
    es = (QName, Elims) -> m (QName, Elims)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (QName
    x,Elims
    es)

    {-# SPECIALIZE tryReifyAsLetBinding :: Term -> TCM Expr -> TCM Expr #-}
    -- | Check if the term matches an existing let-binding, in that case use the corresponding variable,
    --   otherwise reify using the continuation.
    tryReifyAsLetBinding :: MonadReify m => Term -> m Expr -> m Expr
    tryReifyAsLetBinding :: forall (m :: * -> *). MonadReify m => Term -> m Expr -> m Expr
    tryReifyAsLetBinding Term
    v m Expr
    fallback = m Bool -> m Expr -> m Expr -> m Expr
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
    ifM ((TCEnv -> Bool) -> m Bool
    forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
    asksTC ((TCEnv -> Bool) -> m Bool) -> (TCEnv -> Bool) -> m Bool
    forall a b. (a -> b) -> a -> b
    $ Bool -> Bool
    not (Bool -> Bool) -> (TCEnv -> Bool) -> TCEnv -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . TCEnv -> Bool
    envFoldLetBindings) m Expr
    fallback (m Expr -> m Expr) -> m Expr -> m Expr
    forall a b. (a -> b) -> a -> b
    $ do
      letBindings <- do
        binds  <- (TCEnv -> [(Name, Open LetBinding)]) -> m [(Name, Open LetBinding)]
    forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
    asksTC (Map Name (Open LetBinding) -> [(Name, Open LetBinding)]
    forall k a. Map k a -> [(k, a)]
    Map.toAscList (Map Name (Open LetBinding) -> [(Name, Open LetBinding)])
    -> (TCEnv -> Map Name (Open LetBinding))
    -> TCEnv
    -> [(Name, Open LetBinding)]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . TCEnv -> Map Name (Open LetBinding)
    envLetBindings)
        opened <- forM binds $ \ (Name
    name, Open LetBinding
    open) -> (,Name
    name) (LetBinding -> (LetBinding, Name))
    -> m LetBinding -> m (LetBinding, Name)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Open LetBinding -> m LetBinding
    forall a (m :: * -> *).
    (TermSubst a, MonadTCEnv m) =>
    Open a -> m a
    getOpen Open LetBinding
    open
        return [ (body, name) | (LetBinding UserWritten body _, name) <- opened, not $ isNoName name ]  -- Only fold user-written lets
      matchingBindings <- filterM (\(Term, Name)
    t -> Term
    -> Term
    -> (Term -> Term -> m Bool)
    -> (Term -> Term -> m Bool)
    -> m Bool
    forall a (m :: * -> *) b.
    (Instantiate a, SynEq a, MonadReduce m) =>
    a -> a -> (a -> a -> m b) -> (a -> a -> m b) -> m b
    checkSyntacticEquality Term
    v ((Term, Name) -> Term
    forall a b. (a, b) -> a
    fst (Term, Name)
    t) (\Term
    _ Term
    _ -> Bool -> m Bool
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    True) (\Term
    _ Term
    _ -> Bool -> m Bool
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False)) letBindings
      case matchingBindings of
        (Term
    _, Name
    name) : [(Term, Name)]
    _ -> Expr -> m Expr
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Expr -> m Expr) -> Expr -> m Expr
    forall a b. (a -> b) -> a -> b
    $ Name -> Expr
    A.Var Name
    name
        []            -> m Expr
    fallback

    {-# SPECIALIZE reifyTerm :: Bool -> Term -> TCM Expr #-}
    reifyTerm ::
          MonadReify m
       => Bool           -- ^ Try to expand away anonymous definitions?
       -> Term
       -> m Expr
    reifyTerm :: forall (m :: * -> *). MonadReify m => Bool -> Term -> m Expr
    reifyTerm Bool
    expandAnonDefs0 Term
    v0 = Term -> m Expr -> m Expr
    forall (m :: * -> *). MonadReify m => Term -> m Expr -> m Expr
    tryReifyAsLetBinding Term
    v0 (m Expr -> m Expr) -> m Expr -> m Expr
    forall a b. (a -> b) -> a -> b
    $ do
      -- Jesper 2018-11-02: If 'PrintMetasBare', drop all meta eliminations.
      metasBare <- (TCEnv -> Bool) -> m Bool
    forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
    asksTC TCEnv -> Bool
    envPrintMetasBare
      reportSDoc "reify.term" 80 $ pure $ "reifyTerm v0 = " <+> pretty v0
      v <- instantiate v0 >>= \case
        I.MetaV MetaId
    x Elims
    _ | Bool
    metasBare -> Term -> m Term
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Term -> m Term) -> Term -> m Term
    forall a b. (a -> b) -> a -> b
    $ MetaId -> Elims -> Term
    I.MetaV MetaId
    x []
        Term
    v -> Term -> m Term
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Term
    v
      reportSDoc "reify.term" 80 $ pure $ "reifyTerm v = " <+> pretty v
      -- Ulf 2014-07-10: Don't expand anonymous when display forms are disabled
      -- (i.e. when we don't care about nice printing)
      expandAnonDefs <- return expandAnonDefs0 `and2M` displayFormsEnabled

      -- Andreas, 2016-07-21 if --postfix-projections
      -- then we print system-generated projections as postfix, else prefix.
      havePfp <- optPostfixProjections <$> pragmaOptions

      -- Amy, 2024-01-07: postfix and system projections should still be
      -- turned into head symbols *if* they have display forms attached.
      hasDisplay <- liftReduce $ unKleisli hasDisplayForms
      let
        prefixize :: ProjOrigin -> QName -> Bool
        prefixize ProjOrigin
    orig QName
    name = [Bool] -> Bool
    forall (t :: * -> *). Foldable t => t Bool -> Bool
    or
          [ if Bool
    havePfp then ProjOrigin
    orig ProjOrigin -> ProjOrigin -> Bool
    forall a. Eq a => a -> a -> Bool
    == ProjOrigin
    ProjPrefix else ProjOrigin
    orig ProjOrigin -> ProjOrigin -> Bool
    forall a. Eq a => a -> a -> Bool
    /= ProjOrigin
    ProjPostfix
          , QName -> Bool
    isOperator QName
    name
              -- Andreas, 2024-06-13, issue #7318:
              -- print e.g. G .|_| as | G |
          , QName -> Bool
    hasDisplay QName
    name
          ]
      reportSDoc "reify.term" 80 $ pure $ "reifyTerm (unSpine v) = " <+> pretty (unSpine' prefixize v)

      case unSpine' prefixize v of
        -- Hack to print generalized field projections with nicer names. Should
        -- only show up in errors. Check the spined form!
        Term
    _ | I.Var Nat
    n (I.Proj ProjOrigin
    _ QName
    p : Elims
    es) <- Term
    v,
            Just MetaNameSuggestion
    name <- QName -> Maybe MetaNameSuggestion
    getGeneralizedFieldName QName
    p -> do
          let fakeName :: Name
    fakeName = (QName -> Name
    qnameName QName
    p) {nameConcrete = C.simpleName name} -- TODO: infix names!?
          Expr -> [Elim' Expr] -> m Expr
    forall (m :: * -> *).
    MonadReify m =>
    Expr -> [Elim' Expr] -> m Expr
    elims (Name -> Expr
    A.Var Name
    fakeName) ([Elim' Expr] -> m Expr) -> m [Elim' Expr] -> m Expr
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Elims -> m (ReifiesTo Elims)
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    forall (m :: * -> *). MonadReify m => Elims -> m (ReifiesTo Elims)
    reify Elims
    es
        I.Var Nat
    n Elims
    es -> do
          x <- m Name -> m (Maybe Name) -> m Name
    forall (m :: * -> *) a. Monad m => m a -> m (Maybe a) -> m a
    fromMaybeM (MetaNameSuggestion -> m Name
    forall a (m :: * -> *).
    (FreshName a, MonadFresh NameId m) =>
    a -> m Name
    forall (m :: * -> *).
    MonadFresh NameId m =>
    MetaNameSuggestion -> m Name
    freshName_ (MetaNameSuggestion -> m Name) -> MetaNameSuggestion -> m Name
    forall a b. (a -> b) -> a -> b
    $ MetaNameSuggestion
    "@" MetaNameSuggestion -> MetaNameSuggestion -> MetaNameSuggestion
    forall a. [a] -> [a] -> [a]
    ++ Nat -> MetaNameSuggestion
    forall a. Show a => a -> MetaNameSuggestion
    show Nat
    n) (m (Maybe Name) -> m Name) -> m (Maybe Name) -> m Name
    forall a b. (a -> b) -> a -> b
    $ Nat -> m (Maybe Name)
    forall (m :: * -> *). MonadTCEnv m => Nat -> m (Maybe Name)
    nameOfBV' Nat
    n
          elims (A.Var x) =<< reify es
        I.Def QName
    x Elims
    es -> do
          MetaNameSuggestion -> Nat -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    MetaNameSuggestion -> Nat -> TCMT IO Doc -> m ()
    reportSDoc MetaNameSuggestion
    "reify.def" Nat
    80 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
    forall a b. (a -> b) -> a -> b
    $ Doc -> TCMT IO Doc
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Doc -> TCMT IO Doc) -> Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ Doc
    "reifying def" Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> QName -> Doc
    forall a. Pretty a => a -> Doc
    pretty QName
    x
          (x, es) <- QName -> Elims -> m (QName, Elims)
    forall (m :: * -> *).
    MonadReify m =>
    QName -> Elims -> m (QName, Elims)
    reifyPathPConstAsPath QName
    x Elims
    es
          reifyDisplayForm x es $ reifyDef expandAnonDefs x es

        I.Con ConHead
    c ConInfo
    ci Elims
    es -> do

          -- If the origin is a record expression, print a record expression.
          if ConInfo
    ci ConInfo -> ConInfo -> Bool
    forall a. Eq a => a -> a -> Bool
    == ConInfo
    ConORec then Maybe (QName, RecordData) -> m Expr
    recordExpression Maybe (QName, RecordData)
    forall a. Maybe a
    Nothing else do
            QName -> m (Maybe (QName, RecordData))
    forall (m :: * -> *).
    HasConstInfo m =>
    QName -> m (Maybe (QName, RecordData))
    isRecordConstructor QName
    x m (Maybe (QName, RecordData))
    -> (Maybe (QName, RecordData) -> m Expr) -> m Expr
    forall a b. m a -> (a -> m b) -> m b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case

              -- If it is a generated constructor, print a record expression.
              Just (QName
    r, RecordData
    def) | Bool -> Bool
    not (RecordData -> Bool
    _recNamedCon RecordData
    def) -> Maybe (QName, RecordData) -> m Expr
    recordExpression (Maybe (QName, RecordData) -> m Expr)
    -> Maybe (QName, RecordData) -> m Expr
    forall a b. (a -> b) -> a -> b
    $ (QName, RecordData) -> Maybe (QName, RecordData)
    forall a. a -> Maybe a
    Just (QName
    r, RecordData
    def)

              -- Otherwise, print a constructor application.
              Maybe (QName, RecordData)
    _ -> m Expr
    constructorApplication
          where
            x :: QName
    x = ConHead -> QName
    conName ConHead
    c

            recordExpression :: Maybe (QName, RecordData) -> m Expr
    recordExpression Maybe (QName, RecordData)
    mrdef = do
              (r, def) <- m (QName, RecordData)
    -> ((QName, RecordData) -> m (QName, RecordData))
    -> Maybe (QName, RecordData)
    -> m (QName, RecordData)
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe ((QName, RecordData)
    -> Maybe (QName, RecordData) -> (QName, RecordData)
    forall a. a -> Maybe a -> a
    fromMaybe (QName, RecordData)
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe (QName, RecordData) -> (QName, RecordData))
    -> m (Maybe (QName, RecordData)) -> m (QName, RecordData)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> m (Maybe (QName, RecordData))
    forall (m :: * -> *).
    HasConstInfo m =>
    QName -> m (Maybe (QName, RecordData))
    isRecordConstructor QName
    x) (QName, RecordData) -> m (QName, RecordData)
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Maybe (QName, RecordData)
    mrdef
              showImp <- showImplicitArguments
              let keep (Dom' Term Name
    a, Expr
    v) = Bool
    showImp Bool -> Bool -> Bool
    || Dom' Term Name -> Bool
    forall a. LensHiding a => a -> Bool
    visible Dom' Term Name
    a
              A.Rec empty noExprInfo
                . map (Left . uncurry FieldAssignment . mapFst unDom)
                . filter keep
                . zip (recordFieldNames def)
                . map unArg
                <$> reify (fromMaybe __IMPOSSIBLE__ $ allApplyElims es)

            constructorApplication :: m Expr
    constructorApplication = QName -> Elims -> m Expr -> m Expr
    forall (m :: * -> *).
    MonadReify m =>
    QName -> Elims -> m Expr -> m Expr
    reifyDisplayForm QName
    x Elims
    es (m Expr -> m Expr) -> m Expr -> m Expr
    forall a b. (a -> b) -> a -> b
    $ do
              def <- QName -> m Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    x
              let Constructor {conPars = np} = theDef def
              -- if we are the the module that defines constructor x
              -- then we have to drop at least the n module parameters
              n <- getDefFreeVars x
              -- the number of parameters is greater (if the data decl has
              -- extra parameters) or equal (if not) to n
              when (n > np) __IMPOSSIBLE__
              let h = AmbiguousQName -> Expr
    A.Con (QName -> AmbiguousQName
    unambiguous QName
    x)
              if null es
                then return h
                else do
                  es <- reify $ fromMaybe __IMPOSSIBLE__ $ allApplyElims es
                  -- Andreas, 2012-04-20: do not reify parameter arguments of constructor
                  -- if the first regular constructor argument is hidden
                  -- we turn it into a named argument, in order to avoid confusion
                  -- with the parameter arguments which can be supplied in abstract syntax
                  --
                  -- Andreas, 2012-09-17: this does not remove all sources of confusion,
                  -- since parameters could have the same name as regular arguments
                  -- (see for example the parameter {i} to Data.Star.Star, which is also
                  -- the first argument to the cons).
                  -- @data Star {i}{I : Set i} ... where cons : {i :  I} ...@
                  if np == 0
                    then apps h es
                    else do
                      -- Get name of first argument from type of constructor.
                      -- Here, we need the reducing version of @telView@
                      -- because target of constructor could be a definition
                      -- expanding into a function type.  See test/succeed/NameFirstIfHidden.agda.
                      TelV tel _ <- telView (defType def)
                      let (pars, rest) = splitAt np $ telToList tel
                      case rest of
                        -- Andreas, 2012-09-18
                        -- If the first regular constructor argument is hidden,
                        -- we keep the parameters to avoid confusion.
                        (Dom {domInfo :: forall t e. Dom' t e -> ArgInfo
    domInfo = ArgInfo
    info} : [Dom (MetaNameSuggestion, Type)]
    _) | ArgInfo -> Bool
    forall a. LensHiding a => a -> Bool
    notVisible ArgInfo
    info -> do
                          let us :: [Arg Expr]
    us = [Dom (MetaNameSuggestion, Type)]
    -> (Dom (MetaNameSuggestion, Type) -> Arg Expr) -> [Arg Expr]
    forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
    for (Nat
    -> [Dom (MetaNameSuggestion, Type)]
    -> [Dom (MetaNameSuggestion, Type)]
    forall a. Nat -> [a] -> [a]
    drop Nat
    n [Dom (MetaNameSuggestion, Type)]
    pars) ((Dom (MetaNameSuggestion, Type) -> Arg Expr) -> [Arg Expr])
    -> (Dom (MetaNameSuggestion, Type) -> Arg Expr) -> [Arg Expr]
    forall a b. (a -> b) -> a -> b
    $ \(Dom {domInfo :: forall t e. Dom' t e -> ArgInfo
    domInfo = ArgInfo
    ai}) ->
                                -- setRelevance Relevant $
                                Arg Expr -> Arg Expr
    forall a. LensHiding a => a -> a
    hideOrKeepInstance (Arg Expr -> Arg Expr) -> Arg Expr -> Arg Expr
    forall a b. (a -> b) -> a -> b
    $ ArgInfo -> Expr -> Arg Expr
    forall e. ArgInfo -> e -> Arg e
    Arg ArgInfo
    ai Expr
    forall a. Underscore a => a
    underscore
                          Expr -> [Arg Expr] -> m Expr
    forall (m :: * -> *). MonadReify m => Expr -> [Arg Expr] -> m Expr
    apps Expr
    h ([Arg Expr] -> m Expr) -> [Arg Expr] -> m Expr
    forall a b. (a -> b) -> a -> b
    $ [Arg Expr]
    us [Arg Expr] -> [Arg Expr] -> [Arg Expr]
    forall a. [a] -> [a] -> [a]
    ++ [Arg Expr]
    es -- Note: unless --show-implicit, @apps@ will drop @us@.
                        -- otherwise, we drop all parameters
                        [Dom (MetaNameSuggestion, Type)]
    _ -> Expr -> [Arg Expr] -> m Expr
    forall (m :: * -> *). MonadReify m => Expr -> [Arg Expr] -> m Expr
    apps Expr
    h [Arg Expr]
    es

    --    I.Lam info b | isAbsurdBody b -> return $ A. AbsurdLam noExprInfo $ getHiding info
        I.Lam ArgInfo
    info Abs Term
    b    -> do
          (x,e) <- Abs Term -> m (ReifiesTo (Abs Term))
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    forall (m :: * -> *).
    MonadReify m =>
    Abs Term -> m (ReifiesTo (Abs Term))
    reify Abs Term
    b
          -- #4160: Hacky solution: if --show-implicit, treat all lambdas as user-written. This will
          -- prevent them from being dropped by AbstractToConcrete (where we don't have easy access to
          -- the --show-implicit flag.
          info <- ifM showImplicitArguments (return $ setOrigin UserWritten info) (return info)
          return $ A.Lam exprNoRange (mkDomainFree $ unnamedArg info $ mkBinder_ x) e
          -- Andreas, 2011-04-07 we do not need relevance information at internal Lambda
        I.Lit Literal
    l        -> Literal -> m (ReifiesTo Literal)
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    forall (m :: * -> *).
    MonadReify m =>
    Literal -> m (ReifiesTo Literal)
    reify Literal
    l
        I.Level Level
    l      -> Level -> m (ReifiesTo Level)
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    forall (m :: * -> *). MonadReify m => Level -> m (ReifiesTo Level)
    reify Level
    l
        I.Pi Dom Type
    a Abs Type
    b       -> case Abs Type
    b of
            NoAbs MetaNameSuggestion
    _ Type
    b'
              | Dom Type -> Bool
    forall a. LensHiding a => a -> Bool
    visible Dom Type
    a, Bool -> Bool
    not (Dom Type -> Bool
    forall t e. Dom' t e -> Bool
    domIsFinite Dom Type
    a) -> (Arg Expr -> Expr -> Expr) -> (Arg Expr, Expr) -> Expr
    forall a b c. (a -> b -> c) -> (a, b) -> c
    uncurry (ExprInfo -> Arg Expr -> Expr -> Expr
    A.Fun (ExprInfo -> Arg Expr -> Expr -> Expr)
    -> ExprInfo -> Arg Expr -> Expr -> Expr
    forall a b. (a -> b) -> a -> b
    $ ExprInfo
    noExprInfo) ((Arg Expr, Expr) -> Expr) -> m (Arg Expr, Expr) -> m Expr
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Dom Type, Type) -> m (ReifiesTo (Dom Type, Type))
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    forall (m :: * -> *).
    MonadReify m =>
    (Dom Type, Type) -> m (ReifiesTo (Dom Type, Type))
    reify (Dom Type
    a, Type
    b')
                -- Andreas, 2013-11-11 Hidden/Instance I.Pi must be A.Pi
                -- since (a) the syntax {A} -> B or {{A}} -> B is not legal
                -- and (b) the name of the binder might matter.
                -- See issue 951 (a) and 952 (b).
                --
                -- Amy, 2022-09-05: Can't be finite either, since otherwise
                -- we say ".(IsOne φ) → A ≠ .(IsOne φ) → A" with no
                -- indication of which is finite and which isn't
              | Bool
    otherwise   -> Abs Type -> Arg Expr -> m Expr
    mkPi Abs Type
    b (Arg Expr -> m Expr) -> m (Arg Expr) -> m Expr
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Dom Type -> m (ReifiesTo (Dom Type))
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    forall (m :: * -> *).
    MonadReify m =>
    Dom Type -> m (ReifiesTo (Dom Type))
    reify Dom Type
    a
            Abs Type
    b               -> Abs Type -> Arg Expr -> m Expr
    mkPi Abs Type
    b (Arg Expr -> m Expr) -> m (Arg Expr) -> m Expr
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< do
              m Bool -> m (Arg Expr) -> m (Arg Expr) -> m (Arg Expr)
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
    ifM (Dom Type -> Type -> m Bool
    forall {m :: * -> *} {a} {t}.
    (MonadTCEnv m, Free a, Free t) =>
    t -> a -> m Bool
    domainFree Dom Type
    a (Abs Type -> Type
    forall a. Subst a => Abs a -> a
    absBody Abs Type
    b))
                {- then -} (Arg Expr -> m (Arg Expr)
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Arg Expr -> m (Arg Expr)) -> Arg Expr -> m (Arg Expr)
    forall a b. (a -> b) -> a -> b
    $ ArgInfo -> Expr -> Arg Expr
    forall e. ArgInfo -> e -> Arg e
    Arg (Dom Type -> ArgInfo
    forall t e. Dom' t e -> ArgInfo
    domInfo Dom Type
    a) Expr
    forall a. Underscore a => a
    underscore)
                {- else -} (Dom Type -> m (ReifiesTo (Dom Type))
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    forall (m :: * -> *).
    MonadReify m =>
    Dom Type -> m (ReifiesTo (Dom Type))
    reify Dom Type
    a)
          where
            mkPi :: Abs Type -> Arg Expr -> m Expr
    mkPi Abs Type
    b (Arg ArgInfo
    info Expr
    a') = m Bool -> m Expr -> m Expr -> m Expr
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
    ifM (ArgInfo -> m Bool
    forall (m :: * -> *). MonadReify m => ArgInfo -> m Bool
    skipGeneralizedParameter ArgInfo
    info) ((Name, Expr) -> Expr
    forall a b. (a, b) -> b
    snd ((Name, Expr) -> Expr) -> m (Name, Expr) -> m Expr
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Abs Type -> m (ReifiesTo (Abs Type))
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    forall (m :: * -> *).
    MonadReify m =>
    Abs Type -> m (ReifiesTo (Abs Type))
    reify Abs Type
    b) (m Expr -> m Expr) -> m Expr -> m Expr
    forall a b. (a -> b) -> a -> b
    $ do
              tac <- Maybe (Ranged Expr) -> TacticAttribute' Expr
    forall a. Maybe (Ranged a) -> TacticAttribute' a
    TacticAttribute (Maybe (Ranged Expr) -> TacticAttribute' Expr)
    -> m (Maybe (Ranged Expr)) -> m (TacticAttribute' Expr)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> do (Term -> m (Ranged Expr)) -> Maybe Term -> m (Maybe (Ranged Expr))
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Maybe a -> f (Maybe b)
    traverse (Range -> Expr -> Ranged Expr
    forall a. Range -> a -> Ranged a
    Ranged Range
    forall a. Range' a
    noRange (Expr -> Ranged Expr)
    -> (Term -> m Expr) -> Term -> m (Ranged Expr)
    forall (m :: * -> *) b c a.
    Functor m =>
    (b -> c) -> (a -> m b) -> a -> m c
    <.> Term -> m Expr
    Term -> m (ReifiesTo Term)
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    forall (m :: * -> *). MonadReify m => Term -> m (ReifiesTo Term)
    reify) (Maybe Term -> m (Maybe (Ranged Expr)))
    -> Maybe Term -> m (Maybe (Ranged Expr))
    forall a b. (a -> b) -> a -> b
    $ Dom Type -> Maybe Term
    forall t e. Dom' t e -> Maybe t
    domTactic Dom Type
    a
              (x, b) <- reify b
              let xs = Arg (Named (WithOrigin (Ranged MetaNameSuggestion)) Binder)
    -> List1
         (Arg (Named (WithOrigin (Ranged MetaNameSuggestion)) Binder))
    forall el coll. Singleton el coll => el -> coll
    singleton (Arg (Named (WithOrigin (Ranged MetaNameSuggestion)) Binder)
     -> List1
          (Arg (Named (WithOrigin (Ranged MetaNameSuggestion)) Binder)))
    -> Arg (Named (WithOrigin (Ranged MetaNameSuggestion)) Binder)
    -> List1
         (Arg (Named (WithOrigin (Ranged MetaNameSuggestion)) Binder))
    forall a b. (a -> b) -> a -> b
    $ ArgInfo
    -> Named (WithOrigin (Ranged MetaNameSuggestion)) Binder
    -> Arg (Named (WithOrigin (Ranged MetaNameSuggestion)) Binder)
    forall e. ArgInfo -> e -> Arg e
    Arg ArgInfo
    info (Named (WithOrigin (Ranged MetaNameSuggestion)) Binder
     -> Arg (Named (WithOrigin (Ranged MetaNameSuggestion)) Binder))
    -> Named (WithOrigin (Ranged MetaNameSuggestion)) Binder
    -> Arg (Named (WithOrigin (Ranged MetaNameSuggestion)) Binder)
    forall a b. (a -> b) -> a -> b
    $ Maybe (WithOrigin (Ranged MetaNameSuggestion))
    -> Binder -> Named (WithOrigin (Ranged MetaNameSuggestion)) Binder
    forall name a. Maybe name -> a -> Named name a
    Named (Dom Type -> Maybe (WithOrigin (Ranged MetaNameSuggestion))
    forall t e.
    Dom' t e -> Maybe (WithOrigin (Ranged MetaNameSuggestion))
    domName Dom Type
    a) (Binder -> Named (WithOrigin (Ranged MetaNameSuggestion)) Binder)
    -> Binder -> Named (WithOrigin (Ranged MetaNameSuggestion)) Binder
    forall a b. (a -> b) -> a -> b
    $ Name -> Binder
    mkBinder_ Name
    x
              return $ A.Pi noExprInfo
                (singleton $ TBind noRange (TypedBindingInfo tac (domIsFinite a)) xs a')
                b
            -- We can omit the domain type if it doesn't have any free variables
            -- and it's mentioned in the target type.
            domainFree :: t -> a -> m Bool
    domainFree t
    a a
    b = do
              df <- (TCEnv -> Bool) -> m Bool
    forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
    asksTC TCEnv -> Bool
    envPrintDomainFreePi
              return $ df && freeIn 0 b && closed a

            skipGeneralizedParameter :: MonadReify m => ArgInfo -> m Bool
            skipGeneralizedParameter :: forall (m :: * -> *). MonadReify m => ArgInfo -> m Bool
    skipGeneralizedParameter ArgInfo
    info = (Bool -> Bool
    not (Bool -> Bool) -> m Bool -> m Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m Bool
    forall (m :: * -> *). HasOptions m => m Bool
    showGeneralizedArguments) m Bool -> (Bool -> Bool) -> m Bool
    forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
    <&> (Bool -> Bool -> Bool
    && (ArgInfo -> Origin
    argInfoOrigin ArgInfo
    info Origin -> Origin -> Bool
    forall a. Eq a => a -> a -> Bool
    == Origin
    Generalization))

        I.Sort Sort
    s     -> Sort -> m (ReifiesTo Sort)
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    forall (m :: * -> *). MonadReify m => Sort -> m (ReifiesTo Sort)
    reify Sort
    s
        I.MetaV MetaId
    x Elims
    es -> do
              x' <- MetaId -> m (ReifiesTo MetaId)
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    forall (m :: * -> *).
    MonadReify m =>
    MetaId -> m (ReifiesTo MetaId)
    reify MetaId
    x

              es' <- reify es

              mv <- lookupLocalMeta x
              (msub1,meta_tel,msub2) <- do
                local_chkpt <- viewTC eCurrentCheckpoint
                (chkpt, tel, msub2) <- enterClosure mv $ \ Range
    _ ->
                                   (,,) (CheckpointId
     -> Tele (Dom Type)
     -> Maybe (Substitution' Term)
     -> (CheckpointId, Tele (Dom Type), Maybe (Substitution' Term)))
    -> m CheckpointId
    -> m (Tele (Dom Type)
          -> Maybe (Substitution' Term)
          -> (CheckpointId, Tele (Dom Type), Maybe (Substitution' Term)))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Lens' TCEnv CheckpointId -> m CheckpointId
    forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
    viewTC (CheckpointId -> f CheckpointId) -> TCEnv -> f TCEnv
    Lens' TCEnv CheckpointId
    eCurrentCheckpoint
                                        m (Tele (Dom Type)
       -> Maybe (Substitution' Term)
       -> (CheckpointId, Tele (Dom Type), Maybe (Substitution' Term)))
    -> m (Tele (Dom Type))
    -> m (Maybe (Substitution' Term)
          -> (CheckpointId, Tele (Dom Type), Maybe (Substitution' Term)))
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> m (Tele (Dom Type))
    forall (m :: * -> *). MonadTCEnv m => m (Tele (Dom Type))
    getContextTelescope
                                        m (Maybe (Substitution' Term)
       -> (CheckpointId, Tele (Dom Type), Maybe (Substitution' Term)))
    -> m (Maybe (Substitution' Term))
    -> m (CheckpointId, Tele (Dom Type), Maybe (Substitution' Term))
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Lens' TCEnv (Maybe (Substitution' Term))
    -> m (Maybe (Substitution' Term))
    forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
    viewTC ((Map CheckpointId (Substitution' Term)
     -> f (Map CheckpointId (Substitution' Term)))
    -> TCEnv -> f TCEnv
    Lens' TCEnv (Map CheckpointId (Substitution' Term))
    eCheckpoints ((Map CheckpointId (Substitution' Term)
      -> f (Map CheckpointId (Substitution' Term)))
     -> TCEnv -> f TCEnv)
    -> ((Maybe (Substitution' Term) -> f (Maybe (Substitution' Term)))
        -> Map CheckpointId (Substitution' Term)
        -> f (Map CheckpointId (Substitution' Term)))
    -> (Maybe (Substitution' Term) -> f (Maybe (Substitution' Term)))
    -> TCEnv
    -> f TCEnv
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . CheckpointId
    -> Lens'
         (Map CheckpointId (Substitution' Term))
         (Maybe (Substitution' Term))
    forall k v. Ord k => k -> Lens' (Map k v) (Maybe v)
    key CheckpointId
    local_chkpt)
                (,,) <$> viewTC (eCheckpoints . key chkpt) <*> pure tel <*> pure msub2

              opt_show_ids <- showIdentitySubstitutions
              let
                  addNames []    [Elim' a]
    es = (Elim' a -> Elim' (Named name a))
    -> [Elim' a] -> [Elim' (Named name a)]
    forall a b. (a -> b) -> [a] -> [b]
    map ((a -> Named name a) -> Elim' a -> Elim' (Named name a)
    forall a b. (a -> b) -> Elim' a -> Elim' b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap a -> Named name a
    forall a name. a -> Named name a
    unnamed) [Elim' a]
    es
                  addNames [name]
    _     [] = []
                  addNames [name]
    xs     (I.Proj{} : [Elim' a]
    _) = [Elim' (Named name a)]
    forall a. HasCallStack => a
    __IMPOSSIBLE__
                  addNames [name]
    xs     (I.IApply a
    x a
    y a
    r : [Elim' a]
    es) =
                    -- Needs to be I.Apply so it can have an Origin field.
                    [name] -> [Elim' a] -> [Elim' (Named name a)]
    addNames [name]
    xs (Arg a -> Elim' a
    forall a. Arg a -> Elim' a
    I.Apply (a -> Arg a
    forall a. a -> Arg a
    defaultArg a
    r) Elim' a -> [Elim' a] -> [Elim' a]
    forall a. a -> [a] -> [a]
    : [Elim' a]
    es)
                  addNames (name
    x:[name]
    xs) (I.Apply Arg a
    arg : [Elim' a]
    es) =
                    Arg (Named name a) -> Elim' (Named name a)
    forall a. Arg a -> Elim' a
    I.Apply (Maybe name -> a -> Named name a
    forall name a. Maybe name -> a -> Named name a
    Named (name -> Maybe name
    forall a. a -> Maybe a
    Just name
    x) (a -> Named name a) -> Arg a -> Arg (Named name a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Origin -> Arg a -> Arg a
    forall a. LensOrigin a => Origin -> a -> a
    setOrigin Origin
    Substitution Arg a
    arg)) Elim' (Named name a)
    -> [Elim' (Named name a)] -> [Elim' (Named name a)]
    forall a. a -> [a] -> [a]
    : [name] -> [Elim' a] -> [Elim' (Named name a)]
    addNames [name]
    xs [Elim' a]
    es

                  p = MetaVariable -> Permutation
    mvPermutation MetaVariable
    mv
                  applyPerm Permutation
    p [a]
    vs = Permutation -> [a] -> [a]
    forall a. Permutation -> [a] -> [a]
    permute (Nat -> Permutation -> Permutation
    takeP ([a] -> Nat
    forall a. Sized a => a -> Nat
    size [a]
    vs) Permutation
    p) [a]
    vs

                  names = (MetaNameSuggestion -> WithOrigin (Ranged MetaNameSuggestion))
    -> [MetaNameSuggestion] -> [WithOrigin (Ranged MetaNameSuggestion)]
    forall a b. (a -> b) -> [a] -> [b]
    map (Origin
    -> Ranged MetaNameSuggestion
    -> WithOrigin (Ranged MetaNameSuggestion)
    forall a. Origin -> a -> WithOrigin a
    WithOrigin Origin
    Inserted (Ranged MetaNameSuggestion
     -> WithOrigin (Ranged MetaNameSuggestion))
    -> (MetaNameSuggestion -> Ranged MetaNameSuggestion)
    -> MetaNameSuggestion
    -> WithOrigin (Ranged MetaNameSuggestion)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . MetaNameSuggestion -> Ranged MetaNameSuggestion
    forall a. a -> Ranged a
    unranged) ([MetaNameSuggestion] -> [WithOrigin (Ranged MetaNameSuggestion)])
    -> [MetaNameSuggestion] -> [WithOrigin (Ranged MetaNameSuggestion)]
    forall a b. (a -> b) -> a -> b
    $ Permutation
    p Permutation -> [MetaNameSuggestion] -> [MetaNameSuggestion]
    forall a. Permutation -> [a] -> [a]
    `applyPerm` Tele (Dom Type) -> [MetaNameSuggestion]
    teleNames Tele (Dom Type)
    meta_tel
                  named_es' = [WithOrigin (Ranged MetaNameSuggestion)]
    -> [Elim' Expr] -> [Elim' (Named_ Expr)]
    forall {name} {a}. [name] -> [Elim' a] -> [Elim' (Named name a)]
    addNames [WithOrigin (Ranged MetaNameSuggestion)]
    names [Elim' Expr]
    es'

                  dropIdentitySubs Substitution' Term
    sub_local2G Substitution' Term
    sub_tel2G =
                     let
                         args_G :: Args
    args_G = Substitution' (SubstArg Args) -> Args -> Args
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' Term
    Substitution' (SubstArg Args)
    sub_tel2G (Args -> Args) -> Args -> Args
    forall a b. (a -> b) -> a -> b
    $ Permutation
    p Permutation -> Args -> Args
    forall a. Permutation -> [a] -> [a]
    `applyPerm` (Tele (Dom Type) -> Args
    forall a t. DeBruijn a => Tele (Dom t) -> [Arg a]
    teleArgs Tele (Dom Type)
    meta_tel :: [Arg Term])
                         es_G :: Elims
    es_G = Substitution' Term
    Substitution' (SubstArg Elims)
    sub_local2G Substitution' (SubstArg Elims) -> Elims -> Elims
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    `applySubst` Elims
    es
                         sameVar :: Arg a -> Elim' a -> Bool
    sameVar Arg a
    x (I.Apply Arg a
    y) = Maybe Nat -> Bool
    forall a. Maybe a -> Bool
    isJust Maybe Nat
    xv Bool -> Bool -> Bool
    && Maybe Nat
    xv Maybe Nat -> Maybe Nat -> Bool
    forall a. Eq a => a -> a -> Bool
    == a -> Maybe Nat
    forall a. DeBruijn a => a -> Maybe Nat
    deBruijnView (Arg a -> a
    forall e. Arg e -> e
    unArg Arg a
    y)
                          where
                           xv :: Maybe Nat
    xv = a -> Maybe Nat
    forall a. DeBruijn a => a -> Maybe Nat
    deBruijnView (a -> Maybe Nat) -> a -> Maybe Nat
    forall a b. (a -> b) -> a -> b
    $ Arg a -> a
    forall e. Arg e -> e
    unArg Arg a
    x
                         sameVar Arg a
    _ Elim' a
    _ = Bool
    False
                         dropArg :: [Bool]
    dropArg = Nat -> [Bool] -> [Bool]
    forall a. Nat -> [a] -> [a]
    take ([WithOrigin (Ranged MetaNameSuggestion)] -> Nat
    forall a. Sized a => a -> Nat
    size [WithOrigin (Ranged MetaNameSuggestion)]
    names) ([Bool] -> [Bool]) -> [Bool] -> [Bool]
    forall a b. (a -> b) -> a -> b
    $ (Arg Term -> Elim' Term -> Bool) -> Args -> Elims -> [Bool]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith Arg Term -> Elim' Term -> Bool
    forall {a} {a}.
    (DeBruijn a, DeBruijn a) =>
    Arg a -> Elim' a -> Bool
    sameVar Args
    args_G Elims
    es_G
                         doDrop :: [Bool] -> [a] -> [a]
    doDrop (Bool
    b : [Bool]
    xs)  (a
    e : [a]
    es) = (if Bool
    b then [a] -> [a]
    forall a. a -> a
    id else (a
    e a -> [a] -> [a]
    forall a. a -> [a] -> [a]
    :)) ([a] -> [a]) -> [a] -> [a]
    forall a b. (a -> b) -> a -> b
    $ [Bool] -> [a] -> [a]
    doDrop [Bool]
    xs [a]
    es
                         doDrop []        [a]
    es = [a]
    es
                         doDrop [Bool]
    _         [] = []
                     in [Bool] -> [Elim' (Named_ Expr)] -> [Elim' (Named_ Expr)]
    forall {a}. [Bool] -> [a] -> [a]
    doDrop [Bool]
    dropArg ([Elim' (Named_ Expr)] -> [Elim' (Named_ Expr)])
    -> [Elim' (Named_ Expr)] -> [Elim' (Named_ Expr)]
    forall a b. (a -> b) -> a -> b
    $ [Elim' (Named_ Expr)]
    named_es'

                  simpl_named_es' | Bool
    opt_show_ids                 = [Elim' (Named_ Expr)]
    named_es'
                                  | Just Substitution' Term
    sub_mtel2local <- Maybe (Substitution' Term)
    msub1 = Substitution' Term -> Substitution' Term -> [Elim' (Named_ Expr)]
    dropIdentitySubs Substitution' Term
    forall a. Substitution' a
    IdS           Substitution' Term
    sub_mtel2local
                                  | Just Substitution' Term
    sub_local2mtel <- Maybe (Substitution' Term)
    msub2 = Substitution' Term -> Substitution' Term -> [Elim' (Named_ Expr)]
    dropIdentitySubs Substitution' Term
    sub_local2mtel Substitution' Term
    forall a. Substitution' a
    IdS
                                  | Bool
    otherwise                    = [Elim' (Named_ Expr)]
    named_es'

              nelims x' simpl_named_es'

        I.DontCare Term
    v -> do
          showIrr <- PragmaOptions -> Bool
    optShowIrrelevant (PragmaOptions -> Bool) -> m PragmaOptions -> m Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m PragmaOptions
    forall (m :: * -> *). HasOptions m => m PragmaOptions
    pragmaOptions
          if | showIrr   -> reifyTerm expandAnonDefs v
             | otherwise -> return underscore
        I.Dummy MetaNameSuggestion
    s [] -> Expr -> m Expr
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Expr -> m Expr) -> Expr -> m Expr
    forall a b. (a -> b) -> a -> b
    $ ExprInfo -> Literal -> Expr
    A.Lit ExprInfo
    forall a. Null a => a
    empty (Literal -> Expr) -> Literal -> Expr
    forall a b. (a -> b) -> a -> b
    $ Text -> Literal
    LitString (MetaNameSuggestion -> Text
    T.pack MetaNameSuggestion
    s)
        I.Dummy MetaNameSuggestion
    "applyE" Elims
    es | I.Apply (Arg ArgInfo
    _ Term
    h) : Elims
    es' <- Elims
    es -> do
                                h <- Term -> m (ReifiesTo Term)
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    forall (m :: * -> *). MonadReify m => Term -> m (ReifiesTo Term)
    reify Term
    h
                                es' <- reify es'
                                elims h es'
                            | Bool
    otherwise -> m Expr
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        I.Dummy MetaNameSuggestion
    s Elims
    es -> do
          s <- Term -> m (ReifiesTo Term)
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    forall (m :: * -> *). MonadReify m => Term -> m (ReifiesTo Term)
    reify (MetaNameSuggestion -> Elims -> Term
    I.Dummy MetaNameSuggestion
    s [])
          es <- reify es
          elims s es
      where
        -- Andreas, 2012-10-20  expand a copy if not in scope
        -- to improve error messages.
        -- Don't do this if we have just expanded into a display form,
        -- otherwise we loop!
        reifyDef :: MonadReify m => Bool -> QName -> I.Elims -> m Expr
        reifyDef :: forall (m :: * -> *).
    MonadReify m =>
    Bool -> QName -> Elims -> m Expr
    reifyDef Bool
    True QName
    x Elims
    es =
          m Bool -> m Expr -> m Expr -> m Expr
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
    ifM (Bool -> Bool
    not (Bool -> Bool) -> (ScopeInfo -> Bool) -> ScopeInfo -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [QName] -> Bool
    forall a. Null a => a -> Bool
    null ([QName] -> Bool) -> (ScopeInfo -> [QName]) -> ScopeInfo -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . QName -> ScopeInfo -> [QName]
    inverseScopeLookupName QName
    x (ScopeInfo -> Bool) -> m ScopeInfo -> m Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m ScopeInfo
    forall (m :: * -> *). ReadTCState m => m ScopeInfo
    getScope) (QName -> Elims -> m Expr
    forall (m :: * -> *). MonadReify m => QName -> Elims -> m Expr
    reifyDef' QName
    x Elims
    es) (m Expr -> m Expr) -> m Expr -> m Expr
    forall a b. (a -> b) -> a -> b
    $ do
          r <- QName -> Elims -> m (Reduced () Term)
    forall (m :: * -> *).
    PureTCM m =>
    QName -> Elims -> m (Reduced () Term)
    reduceDefCopy QName
    x Elims
    es
          case r of
            YesReduction Simplification
    _ Term
    v -> do
              MetaNameSuggestion -> Nat -> [MetaNameSuggestion] -> m ()
    forall a (m :: * -> *).
    (ReportS a, MonadDebug m) =>
    MetaNameSuggestion -> Nat -> a -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    MetaNameSuggestion -> Nat -> [MetaNameSuggestion] -> m ()
    reportS MetaNameSuggestion
    "reify.anon" Nat
    60
                [ MetaNameSuggestion
    "reduction on defined ident. in anonymous module"
                , MetaNameSuggestion
    "x = " MetaNameSuggestion -> MetaNameSuggestion -> MetaNameSuggestion
    forall a. [a] -> [a] -> [a]
    ++ QName -> MetaNameSuggestion
    forall a. Pretty a => a -> MetaNameSuggestion
    prettyShow QName
    x
                , MetaNameSuggestion
    "v = " MetaNameSuggestion -> MetaNameSuggestion -> MetaNameSuggestion
    forall a. [a] -> [a] -> [a]
    ++ Term -> MetaNameSuggestion
    forall a. Show a => a -> MetaNameSuggestion
    show Term
    v
                ]
              Term -> m (ReifiesTo Term)
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    forall (m :: * -> *). MonadReify m => Term -> m (ReifiesTo Term)
    reify Term
    v
            NoReduction () -> do
              MetaNameSuggestion -> Nat -> [MetaNameSuggestion] -> m ()
    forall a (m :: * -> *).
    (ReportS a, MonadDebug m) =>
    MetaNameSuggestion -> Nat -> a -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    MetaNameSuggestion -> Nat -> [MetaNameSuggestion] -> m ()
    reportS MetaNameSuggestion
    "reify.anon" Nat
    60
                [ MetaNameSuggestion
    "no reduction on defined ident. in anonymous module"
                , MetaNameSuggestion
    "x  = " MetaNameSuggestion -> MetaNameSuggestion -> MetaNameSuggestion
    forall a. [a] -> [a] -> [a]
    ++ QName -> MetaNameSuggestion
    forall a. Pretty a => a -> MetaNameSuggestion
    prettyShow QName
    x
                , MetaNameSuggestion
    "es = " MetaNameSuggestion -> MetaNameSuggestion -> MetaNameSuggestion
    forall a. [a] -> [a] -> [a]
    ++ Elims -> MetaNameSuggestion
    forall a. Show a => a -> MetaNameSuggestion
    show Elims
    es
                ]
              QName -> Elims -> m Expr
    forall (m :: * -> *). MonadReify m => QName -> Elims -> m Expr
    reifyDef' QName
    x Elims
    es
        reifyDef Bool
    _ QName
    x Elims
    es = QName -> Elims -> m Expr
    forall (m :: * -> *). MonadReify m => QName -> Elims -> m Expr
    reifyDef' QName
    x Elims
    es

        reifyDef' :: MonadReify m => QName -> I.Elims -> m Expr
        reifyDef' :: forall (m :: * -> *). MonadReify m => QName -> Elims -> m Expr
    reifyDef' QName
    x Elims
    es = do
          MetaNameSuggestion -> Nat -> MetaNameSuggestion -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    MetaNameSuggestion -> Nat -> MetaNameSuggestion -> m ()
    reportSLn MetaNameSuggestion
    "reify.def" Nat
    60 (MetaNameSuggestion -> m ()) -> MetaNameSuggestion -> m ()
    forall a b. (a -> b) -> a -> b
    $ MetaNameSuggestion
    "reifying call to " MetaNameSuggestion -> MetaNameSuggestion -> MetaNameSuggestion
    forall a. [a] -> [a] -> [a]
    ++ QName -> MetaNameSuggestion
    forall a. Pretty a => a -> MetaNameSuggestion
    prettyShow QName
    x
          -- We should drop this many arguments from the local context.
          n <- QName -> m Nat
    forall (m :: * -> *).
    (Functor m, Applicative m, ReadTCState m, MonadTCEnv m) =>
    QName -> m Nat
    getDefFreeVars QName
    x
          reportSLn "reify.def" 70 $ "freeVars for " ++ prettyShow x ++ " = " ++ show n
          -- If the definition is not (yet) in the signature,
          -- we just do the obvious.
          let fallback SigError
    _ = Expr -> [Elim' Expr] -> m Expr
    forall (m :: * -> *).
    MonadReify m =>
    Expr -> [Elim' Expr] -> m Expr
    elims (QName -> Expr
    A.Def QName
    x) ([Elim' Expr] -> m Expr) -> m [Elim' Expr] -> m Expr
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Elims -> m (ReifiesTo Elims)
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    forall (m :: * -> *). MonadReify m => Elims -> m (ReifiesTo Elims)
    reify (Nat -> Elims -> Elims
    forall a. Nat -> [a] -> [a]
    drop Nat
    n Elims
    es)
          caseEitherM (getConstInfo' x) fallback $ \ Definition
    defn -> do
          let def :: Defn
    def = Definition -> Defn
    theDef Definition
    defn

          -- Check if we have an absurd lambda.
          case Defn
    def of
           Function{ funCompiled :: Defn -> Maybe CompiledClauses
    funCompiled = Just Fail{}, funClauses :: Defn -> [Clause]
    funClauses = [Clause
    cl] }
              | QName -> Bool
    isAbsurdLambdaName QName
    x -> do
                      -- get hiding info from last pattern, which should be ()
                      let ([NamedArg DeBruijnPattern]
    ps, NamedArg DeBruijnPattern
    p) = ([NamedArg DeBruijnPattern], NamedArg DeBruijnPattern)
    -> Maybe ([NamedArg DeBruijnPattern], NamedArg DeBruijnPattern)
    -> ([NamedArg DeBruijnPattern], NamedArg DeBruijnPattern)
    forall a. a -> Maybe a -> a
    fromMaybe ([NamedArg DeBruijnPattern], NamedArg DeBruijnPattern)
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe ([NamedArg DeBruijnPattern], NamedArg DeBruijnPattern)
     -> ([NamedArg DeBruijnPattern], NamedArg DeBruijnPattern))
    -> Maybe ([NamedArg DeBruijnPattern], NamedArg DeBruijnPattern)
    -> ([NamedArg DeBruijnPattern], NamedArg DeBruijnPattern)
    forall a b. (a -> b) -> a -> b
    $ [NamedArg DeBruijnPattern]
    -> Maybe ([NamedArg DeBruijnPattern], NamedArg DeBruijnPattern)
    forall a. [a] -> Maybe ([a], a)
    initLast ([NamedArg DeBruijnPattern]
     -> Maybe ([NamedArg DeBruijnPattern], NamedArg DeBruijnPattern))
    -> [NamedArg DeBruijnPattern]
    -> Maybe ([NamedArg DeBruijnPattern], NamedArg DeBruijnPattern)
    forall a b. (a -> b) -> a -> b
    $ Clause -> [NamedArg DeBruijnPattern]
    namedClausePats Clause
    cl
                      let h :: Hiding
    h = NamedArg DeBruijnPattern -> Hiding
    forall a. LensHiding a => a -> Hiding
    getHiding NamedArg DeBruijnPattern
    p
                          n :: Nat
    n = [NamedArg DeBruijnPattern] -> Nat
    forall a. [a] -> Nat
    forall (t :: * -> *) a. Foldable t => t a -> Nat
    length [NamedArg DeBruijnPattern]
    ps  -- drop all args before the absurd one
                          absLam :: Expr
    absLam = ExprInfo -> Hiding -> Expr
    A.AbsurdLam ExprInfo
    exprNoRange Hiding
    h
                      if | Nat
    n Nat -> Nat -> Bool
    forall a. Ord a => a -> a -> Bool
    > Elims -> Nat
    forall a. [a] -> Nat
    forall (t :: * -> *) a. Foldable t => t a -> Nat
    length Elims
    es -> do -- We don't have all arguments before the absurd one!
                            let name :: DeBruijnPattern -> MetaNameSuggestion
    name (I.VarP PatternInfo
    _ DBPatVar
    x) = MetaNameSuggestion -> MetaNameSuggestion
    patVarNameToString (MetaNameSuggestion -> MetaNameSuggestion)
    -> MetaNameSuggestion -> MetaNameSuggestion
    forall a b. (a -> b) -> a -> b
    $ DBPatVar -> MetaNameSuggestion
    dbPatVarName DBPatVar
    x
                                name DeBruijnPattern
    _            = MetaNameSuggestion
    forall a. HasCallStack => a
    __IMPOSSIBLE__  -- only variables before absurd pattern
                                vars :: [(ArgInfo, MetaNameSuggestion)]
    vars = (NamedArg DeBruijnPattern -> (ArgInfo, MetaNameSuggestion))
    -> [NamedArg DeBruijnPattern] -> [(ArgInfo, MetaNameSuggestion)]
    forall a b. (a -> b) -> [a] -> [b]
    map (NamedArg DeBruijnPattern -> ArgInfo
    forall a. LensArgInfo a => a -> ArgInfo
    getArgInfo (NamedArg DeBruijnPattern -> ArgInfo)
    -> (NamedArg DeBruijnPattern -> MetaNameSuggestion)
    -> NamedArg DeBruijnPattern
    -> (ArgInfo, MetaNameSuggestion)
    forall b c c'. (b -> c) -> (b -> c') -> b -> (c, c')
    forall (a :: * -> * -> *) b c c'.
    Arrow a =>
    a b c -> a b c' -> a b (c, c')
    &&& DeBruijnPattern -> MetaNameSuggestion
    name (DeBruijnPattern -> MetaNameSuggestion)
    -> (NamedArg DeBruijnPattern -> DeBruijnPattern)
    -> NamedArg DeBruijnPattern
    -> MetaNameSuggestion
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . NamedArg DeBruijnPattern -> DeBruijnPattern
    forall a. NamedArg a -> a
    namedArg) ([NamedArg DeBruijnPattern] -> [(ArgInfo, MetaNameSuggestion)])
    -> [NamedArg DeBruijnPattern] -> [(ArgInfo, MetaNameSuggestion)]
    forall a b. (a -> b) -> a -> b
    $ Nat -> [NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern]
    forall a. Nat -> [a] -> [a]
    drop (Elims -> Nat
    forall a. [a] -> Nat
    forall (t :: * -> *) a. Foldable t => t a -> Nat
    length Elims
    es) [NamedArg DeBruijnPattern]
    ps
                                lam :: (ArgInfo, a) -> m (Expr -> Expr)
    lam (ArgInfo
    i, a
    s) = do
                                  x <- a -> m Name
    forall a (m :: * -> *).
    (FreshName a, MonadFresh NameId m) =>
    a -> m Name
    forall (m :: * -> *). MonadFresh NameId m => a -> m Name
    freshName_ a
    s
                                  return $ A.Lam exprNoRange (A.mkDomainFree $ unnamedArg i $ A.mkBinder_ x)
                            ((Expr -> Expr) -> Expr -> Expr) -> Expr -> [Expr -> Expr] -> Expr
    forall a b. (a -> b -> b) -> b -> [a] -> b
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr (Expr -> Expr) -> Expr -> Expr
    forall a b. (a -> b) -> a -> b
    ($) Expr
    absLam ([Expr -> Expr] -> Expr) -> m [Expr -> Expr] -> m Expr
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ((ArgInfo, MetaNameSuggestion) -> m (Expr -> Expr))
    -> [(ArgInfo, MetaNameSuggestion)] -> m [Expr -> Expr]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM (ArgInfo, MetaNameSuggestion) -> m (Expr -> Expr)
    forall {m :: * -> *} {a}.
    (FreshName a, MonadFresh NameId m) =>
    (ArgInfo, a) -> m (Expr -> Expr)
    lam [(ArgInfo, MetaNameSuggestion)]
    vars
                          | Bool
    otherwise -> Expr -> [Elim' Expr] -> m Expr
    forall (m :: * -> *).
    MonadReify m =>
    Expr -> [Elim' Expr] -> m Expr
    elims Expr
    absLam ([Elim' Expr] -> m Expr) -> m [Elim' Expr] -> m Expr
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Elims -> m (ReifiesTo Elims)
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    forall (m :: * -> *). MonadReify m => Elims -> m (ReifiesTo Elims)
    reify (Nat -> Elims -> Elims
    forall a. Nat -> [a] -> [a]
    drop Nat
    n Elims
    es)

          -- Otherwise (no absurd lambda):
           Defn
    _ -> do

            -- Andrea(s), 2016-07-06
            -- Extended lambdas are not considered to be projection like,
            -- as they are mutually recursive with their parent.
            -- Thus we do not have to consider padding them.

            -- Check whether we have an extended lambda and display forms are on.
            df <- m Bool
    forall (m :: * -> *). MonadTCEnv m => m Bool
    displayFormsEnabled

            -- #3004: give up if we have to print a pattern lambda inside its own body!
            alreadyPrinting <- viewTC ePrintingPatternLambdas

            extLam <- case def of
              Function{ funExtLam :: Defn -> Maybe ExtLamInfo
    funExtLam = Just{}, funProjection :: Defn -> Either ProjectionLikenessMissing Projection
    funProjection = Right{} } -> m (Maybe (Nat, Maybe System))
    forall a. HasCallStack => a
    __IMPOSSIBLE__
              Function{ funExtLam :: Defn -> Maybe ExtLamInfo
    funExtLam = Just (ExtLamInfo ModuleName
    m Bool
    b Maybe System
    sys) } ->
                (Nat, Maybe System) -> Maybe (Nat, Maybe System)
    forall a. a -> Maybe a
    Just ((Nat, Maybe System) -> Maybe (Nat, Maybe System))
    -> (Tele (Dom Type) -> (Nat, Maybe System))
    -> Tele (Dom Type)
    -> Maybe (Nat, Maybe System)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (,Maybe System -> Maybe System
    forall lazy strict. Strict lazy strict => strict -> lazy
    Strict.toLazy Maybe System
    sys) (Nat -> (Nat, Maybe System))
    -> (Tele (Dom Type) -> Nat)
    -> Tele (Dom Type)
    -> (Nat, Maybe System)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Tele (Dom Type) -> Nat
    forall a. Sized a => a -> Nat
    size (Tele (Dom Type) -> Maybe (Nat, Maybe System))
    -> m (Tele (Dom Type)) -> m (Maybe (Nat, Maybe System))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ModuleName -> m (Tele (Dom Type))
    forall (m :: * -> *).
    (Functor m, ReadTCState m) =>
    ModuleName -> m (Tele (Dom Type))
    lookupSection ModuleName
    m
              Defn
    _ -> Maybe (Nat, Maybe System) -> m (Maybe (Nat, Maybe System))
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe (Nat, Maybe System)
    forall a. Maybe a
    Nothing

            -- Amy, 2023-04-12: Don't reify clauses generated by the cubical
            -- coverage checker when printing an extended lambda. We can
            -- identify these clauses by looking for patterns headed by DefP
            -- (either transpX or hcomp associated with a data type).
            --
            -- Since these are always automatically derived, printing them
            -- is noise, and shows up even in non-cubical modules, as long
            -- as an imported extended lambda is defined cubical-compatibly.
            let insClause = [NamedArg DeBruijnPattern] -> Bool
    hasDefP ([NamedArg DeBruijnPattern] -> Bool)
    -> (Clause -> [NamedArg DeBruijnPattern]) -> Clause -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Clause -> [NamedArg DeBruijnPattern]
    namedClausePats
            case extLam of
              Just (Nat
    pars, Maybe System
    sys) | Bool
    df, QName
    x QName -> [QName] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `notElem` [QName]
    alreadyPrinting ->
                Lens' TCEnv [QName] -> ([QName] -> [QName]) -> m Expr -> m Expr
    forall (m :: * -> *) a b.
    MonadTCEnv m =>
    Lens' TCEnv a -> (a -> a) -> m b -> m b
    locallyTC ([QName] -> f [QName]) -> TCEnv -> f TCEnv
    Lens' TCEnv [QName]
    ePrintingPatternLambdas (QName
    x QName -> [QName] -> [QName]
    forall a. a -> [a] -> [a]
    :) (m Expr -> m Expr) -> m Expr -> m Expr
    forall a b. (a -> b) -> a -> b
    $
                QName
    -> ArgInfo -> Nat -> Maybe System -> [Clause] -> Elims -> m Expr
    forall (m :: * -> *).
    MonadReify m =>
    QName
    -> ArgInfo -> Nat -> Maybe System -> [Clause] -> Elims -> m Expr
    reifyExtLam QName
    x (Definition -> ArgInfo
    defArgInfo Definition
    defn) Nat
    pars Maybe System
    sys
                  ((Clause -> Bool) -> [Clause] -> [Clause]
    forall a. (a -> Bool) -> [a] -> [a]
    filter (Bool -> Bool
    not (Bool -> Bool) -> (Clause -> Bool) -> Clause -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Clause -> Bool
    insClause) (Definition -> [Clause]
    defClauses Definition
    defn)) Elims
    es

            -- Otherwise (ordinary function call):
              Maybe (Nat, Maybe System)
    _ -> do
               (pad, nes :: [Elim' (Named_ Term)]) <- case Defn
    def of

                Function{ funProjection :: Defn -> Either ProjectionLikenessMissing Projection
    funProjection = Right Projection{ projIndex :: Projection -> Nat
    projIndex = Nat
    np } } | Nat
    np Nat -> Nat -> Bool
    forall a. Ord a => a -> a -> Bool
    > Nat
    0 -> do
                  MetaNameSuggestion -> Nat -> MetaNameSuggestion -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    MetaNameSuggestion -> Nat -> MetaNameSuggestion -> m ()
    reportSLn MetaNameSuggestion
    "reify.def" Nat
    70 (MetaNameSuggestion -> m ()) -> MetaNameSuggestion -> m ()
    forall a b. (a -> b) -> a -> b
    $ MetaNameSuggestion
    "  def. is a projection with projIndex = " MetaNameSuggestion -> MetaNameSuggestion -> MetaNameSuggestion
    forall a. [a] -> [a] -> [a]
    ++ Nat -> MetaNameSuggestion
    forall a. Show a => a -> MetaNameSuggestion
    show Nat
    np

                  -- This is tricky:
                  --  * getDefFreeVars x tells us how many arguments
                  --    are part of the local context
                  --  * some of those arguments might have been dropped
                  --    due to projection likeness
                  --  * when showImplicits is on we'd like to see the dropped
                  --    projection arguments

                  TelV tel _ <- Nat -> Type -> m (TelV Type)
    forall (m :: * -> *).
    (MonadReduce m, MonadAddContext m) =>
    Nat -> Type -> m (TelV Type)
    telViewUpTo Nat
    np (Definition -> Type
    defType Definition
    defn)
                  let (as, rest) = splitAt (np - 1) $ telToList tel
                      dom = Dom (MetaNameSuggestion, Type)
    -> [Dom (MetaNameSuggestion, Type)]
    -> Dom (MetaNameSuggestion, Type)
    forall a. a -> [a] -> a
    headWithDefault Dom (MetaNameSuggestion, Type)
    forall a. HasCallStack => a
    __IMPOSSIBLE__ [Dom (MetaNameSuggestion, Type)]
    rest

                  -- These are the dropped projection arguments
                  scope <- getScope
                  let underscore = MetaInfo -> Expr
    A.Underscore (MetaInfo -> Expr) -> MetaInfo -> Expr
    forall a b. (a -> b) -> a -> b
    $ MetaInfo
    Info.emptyMetaInfo { metaScope = scope }
                  let pad :: [NamedArg Expr]
                      pad = [Dom (MetaNameSuggestion, Type)]
    -> (Dom (MetaNameSuggestion, Type) -> Arg (Named_ Expr))
    -> [Arg (Named_ Expr)]
    forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
    for [Dom (MetaNameSuggestion, Type)]
    as ((Dom (MetaNameSuggestion, Type) -> Arg (Named_ Expr))
     -> [Arg (Named_ Expr)])
    -> (Dom (MetaNameSuggestion, Type) -> Arg (Named_ Expr))
    -> [Arg (Named_ Expr)]
    forall a b. (a -> b) -> a -> b
    $ \ (Dom{domInfo :: forall t e. Dom' t e -> ArgInfo
    domInfo = ArgInfo
    ai, unDom :: forall t e. Dom' t e -> e
    unDom = (MetaNameSuggestion
    x, Type
    _)}) ->
                        ArgInfo -> Named_ Expr -> Arg (Named_ Expr)
    forall e. ArgInfo -> e -> Arg e
    Arg ArgInfo
    ai (Named_ Expr -> Arg (Named_ Expr))
    -> Named_ Expr -> Arg (Named_ Expr)
    forall a b. (a -> b) -> a -> b
    $ Maybe (WithOrigin (Ranged MetaNameSuggestion))
    -> Expr -> Named_ Expr
    forall name a. Maybe name -> a -> Named name a
    Named (WithOrigin (Ranged MetaNameSuggestion)
    -> Maybe (WithOrigin (Ranged MetaNameSuggestion))
    forall a. a -> Maybe a
    Just (WithOrigin (Ranged MetaNameSuggestion)
     -> Maybe (WithOrigin (Ranged MetaNameSuggestion)))
    -> WithOrigin (Ranged MetaNameSuggestion)
    -> Maybe (WithOrigin (Ranged MetaNameSuggestion))
    forall a b. (a -> b) -> a -> b
    $ Origin
    -> Ranged MetaNameSuggestion
    -> WithOrigin (Ranged MetaNameSuggestion)
    forall a. Origin -> a -> WithOrigin a
    WithOrigin Origin
    Inserted (Ranged MetaNameSuggestion
     -> WithOrigin (Ranged MetaNameSuggestion))
    -> Ranged MetaNameSuggestion
    -> WithOrigin (Ranged MetaNameSuggestion)
    forall a b. (a -> b) -> a -> b
    $ MetaNameSuggestion -> Ranged MetaNameSuggestion
    forall a. a -> Ranged a
    unranged MetaNameSuggestion
    x) Expr
    underscore
                          -- TODO #3353 Origin from Dom?

                  -- Now pad' ++ es' = drop n (pad ++ es)
                  let pad' = Nat -> [Arg (Named_ Expr)] -> [Arg (Named_ Expr)]
    forall a. Nat -> [a] -> [a]
    drop Nat
    n [Arg (Named_ Expr)]
    pad
                      es'  = Nat -> Elims -> Elims
    forall a. Nat -> [a] -> [a]
    drop (Nat -> Nat -> Nat
    forall a. Ord a => a -> a -> a
    max Nat
    0 (Nat
    n Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    - [Arg (Named_ Expr)] -> Nat
    forall a. Sized a => a -> Nat
    size [Arg (Named_ Expr)]
    pad)) Elims
    es
                  -- Andreas, 2012-04-21: get rid of hidden underscores {_} and {{_}}
                  -- Keep non-hidden arguments of the padding.
                  --
                  -- Andreas, 2016-12-20, issue #2348:
                  -- Let @padTail@ be the list of arguments of the padding
                  -- (*) after the last visible argument of the padding, and
                  -- (*) with the same visibility as the first regular argument.
                  -- If @padTail@ is not empty, we need to
                  -- print the first regular argument with name.
                  -- We further have to print all elements of @padTail@
                  -- which have the same name and visibility of the
                  -- first regular argument.
                  showImp <- showImplicitArguments

                  -- Get the visible arguments of the padding and the rest
                  -- after the last visible argument.
                  let (padVisNamed, padRest) = filterAndRest visible pad'

                  -- Remove the names from the visible arguments.
                  let padVis  = (Arg (Named_ Expr) -> Arg (Named_ Expr))
    -> [Arg (Named_ Expr)] -> [Arg (Named_ Expr)]
    forall a b. (a -> b) -> [a] -> [b]
    map ((Named_ Expr -> Named_ Expr)
    -> Arg (Named_ Expr) -> Arg (Named_ Expr)
    forall a b. (a -> b) -> Arg a -> Arg b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((Named_ Expr -> Named_ Expr)
     -> Arg (Named_ Expr) -> Arg (Named_ Expr))
    -> (Named_ Expr -> Named_ Expr)
    -> Arg (Named_ Expr)
    -> Arg (Named_ Expr)
    forall a b. (a -> b) -> a -> b
    $ Expr -> Named_ Expr
    forall a name. a -> Named name a
    unnamed (Expr -> Named_ Expr)
    -> (Named_ Expr -> Expr) -> Named_ Expr -> Named_ Expr
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Named_ Expr -> Expr
    forall name a. Named name a -> a
    namedThing) [Arg (Named_ Expr)]
    padVisNamed

                  -- Keep only the rest with the same visibility of @dom@...
                  let padTail = (Arg (Named_ Expr) -> Bool)
    -> [Arg (Named_ Expr)] -> [Arg (Named_ Expr)]
    forall a. (a -> Bool) -> [a] -> [a]
    filter (Dom (MetaNameSuggestion, Type) -> Arg (Named_ Expr) -> Bool
    forall a b. (LensHiding a, LensHiding b) => a -> b -> Bool
    sameHiding Dom (MetaNameSuggestion, Type)
    dom) [Arg (Named_ Expr)]
    padRest

                  -- ... and even the same name.
                  let padSame = (Arg (Named_ Expr) -> Bool)
    -> [Arg (Named_ Expr)] -> [Arg (Named_ Expr)]
    forall a. (a -> Bool) -> [a] -> [a]
    filter ((MetaNameSuggestion -> Maybe MetaNameSuggestion
    forall a. a -> Maybe a
    Just ((MetaNameSuggestion, Type) -> MetaNameSuggestion
    forall a b. (a, b) -> a
    fst ((MetaNameSuggestion, Type) -> MetaNameSuggestion)
    -> (MetaNameSuggestion, Type) -> MetaNameSuggestion
    forall a b. (a -> b) -> a -> b
    $ Dom (MetaNameSuggestion, Type) -> (MetaNameSuggestion, Type)
    forall t e. Dom' t e -> e
    unDom Dom (MetaNameSuggestion, Type)
    dom) Maybe MetaNameSuggestion -> Maybe MetaNameSuggestion -> Bool
    forall a. Eq a => a -> a -> Bool
    ==) (Maybe MetaNameSuggestion -> Bool)
    -> (Arg (Named_ Expr) -> Maybe MetaNameSuggestion)
    -> Arg (Named_ Expr)
    -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Arg (Named_ Expr) -> Maybe MetaNameSuggestion
    forall a.
    (LensNamed a, NameOf a ~ WithOrigin (Ranged MetaNameSuggestion)) =>
    a -> Maybe MetaNameSuggestion
    bareNameOf) [Arg (Named_ Expr)]
    padTail

                  return $ if null padTail || not showImp
                    then (padVis           , map (fmap unnamed) es')
                    else (padVis ++ padSame, nameFirstIfHidden dom es')

                -- If it is not a projection(-like) function, we need no padding.
                Defn
    _ -> ([Arg (Named_ Expr)], [Elim' (Named_ Term)])
    -> m ([Arg (Named_ Expr)], [Elim' (Named_ Term)])
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([], (Elim' Term -> Elim' (Named_ Term))
    -> Elims -> [Elim' (Named_ Term)]
    forall a b. (a -> b) -> [a] -> [b]
    map ((Term -> Named_ Term) -> Elim' Term -> Elim' (Named_ Term)
    forall a b. (a -> b) -> Elim' a -> Elim' b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Term -> Named_ Term
    forall a name. a -> Named name a
    unnamed) (Elims -> [Elim' (Named_ Term)]) -> Elims -> [Elim' (Named_ Term)]
    forall a b. (a -> b) -> a -> b
    $ Nat -> Elims -> Elims
    forall a. Nat -> [a] -> [a]
    drop Nat
    n Elims
    es)

               reportSDoc "reify.def" 100 $ return $ vcat
                 [ "  pad =" <+> pshow pad
                 , "  nes =" <+> pshow nes
                 ]
               let hd0 | Defn -> Bool
    isProperProjection Defn
    def = ProjOrigin -> AmbiguousQName -> Expr
    A.Proj ProjOrigin
    ProjPrefix (AmbiguousQName -> Expr) -> AmbiguousQName -> Expr
    forall a b. (a -> b) -> a -> b
    $ List1 QName -> AmbiguousQName
    AmbQ (List1 QName -> AmbiguousQName) -> List1 QName -> AmbiguousQName
    forall a b. (a -> b) -> a -> b
    $ QName -> List1 QName
    forall el coll. Singleton el coll => el -> coll
    singleton QName
    x
                       | Bool
    otherwise = QName -> Expr
    A.Def QName
    x
               let hd = (Expr -> Arg (Named_ Expr) -> Expr)
    -> Expr -> [Arg (Named_ Expr)] -> Expr
    forall b a. (b -> a -> b) -> b -> [a] -> b
    forall (t :: * -> *) b a.
    Foldable t =>
    (b -> a -> b) -> b -> t a -> b
    List.foldl' (AppInfo -> Expr -> Arg (Named_ Expr) -> Expr
    A.App AppInfo
    defaultAppInfo_) Expr
    hd0 [Arg (Named_ Expr)]
    pad
               nelims hd =<< reify nes

        -- Andreas, 2016-07-06 Issue #2047

        -- With parameter refinement, the "parameter" patterns of an extended
        -- lambda can now be different from variable patterns.  If we just drop
        -- them (plus the associated arguments to the extended lambda), we produce
        -- something

        -- i) that violates internal invariants.  In particular, the permutation
        -- dbPatPerm from the patterns to the telescope can no longer be
        -- computed.  (And in fact, dropping from the start of the telescope is
        -- just plainly unsound then.)

        -- ii) prints the wrong thing (old fix for #2047)

        -- What we do now, is more sound, although not entirely satisfying:
        -- When the "parameter" patterns of an external lambdas are not variable
        -- patterns, we fall back to printing the internal function created for the
        -- extended lambda, instead trying to construct the nice syntax.

        reifyExtLam
          :: MonadReify m
          => QName -> ArgInfo -> Int -> Maybe System -> [I.Clause]
          -> I.Elims -> m Expr
        reifyExtLam :: forall (m :: * -> *).
    MonadReify m =>
    QName
    -> ArgInfo -> Nat -> Maybe System -> [Clause] -> Elims -> m Expr
    reifyExtLam QName
    x ArgInfo
    ai Nat
    npars Maybe System
    msys [Clause]
    cls Elims
    es = do
          MetaNameSuggestion -> Nat -> MetaNameSuggestion -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    MetaNameSuggestion -> Nat -> MetaNameSuggestion -> m ()
    reportSLn MetaNameSuggestion
    "reify.def" Nat
    10 (MetaNameSuggestion -> m ()) -> MetaNameSuggestion -> m ()
    forall a b. (a -> b) -> a -> b
    $ MetaNameSuggestion
    "reifying extended lambda " MetaNameSuggestion -> MetaNameSuggestion -> MetaNameSuggestion
    forall a. [a] -> [a] -> [a]
    ++ QName -> MetaNameSuggestion
    forall a. Pretty a => a -> MetaNameSuggestion
    prettyShow QName
    x
          MetaNameSuggestion -> Nat -> MetaNameSuggestion -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    MetaNameSuggestion -> Nat -> MetaNameSuggestion -> m ()
    reportSLn MetaNameSuggestion
    "reify.def" Nat
    50 (MetaNameSuggestion -> m ()) -> MetaNameSuggestion -> m ()
    forall a b. (a -> b) -> a -> b
    $ Doc -> MetaNameSuggestion
    forall a. Doc a -> MetaNameSuggestion
    render (Doc -> MetaNameSuggestion) -> Doc -> MetaNameSuggestion
    forall a b. (a -> b) -> a -> b
    $ Nat -> Doc -> Doc
    forall a. Nat -> Doc a -> Doc a
    nest Nat
    2 (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    vcat
            [ Doc
    "npars =" Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> Nat -> Doc
    forall a. Pretty a => a -> Doc
    pretty Nat
    npars
            , Doc
    "es    =" Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    fsep ((Elim' Term -> Doc) -> Elims -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map (Nat -> Elim' Term -> Doc
    forall a. Pretty a => Nat -> a -> Doc
    prettyPrec Nat
    10) Elims
    es)
            , Doc
    "def   =" Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    vcat ((Clause -> Doc) -> [Clause] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map Clause -> Doc
    forall a. Pretty a => a -> Doc
    pretty [Clause]
    cls) ]
          -- As extended lambda clauses live in the top level, we add the whole
          -- section telescope to the number of parameters.
          let (Elims
    pares, Elims
    rest) = Nat -> Elims -> (Elims, Elims)
    forall a. Nat -> [a] -> ([a], [a])
    splitAt Nat
    npars Elims
    es
          let pars :: Args
    pars = Args -> Maybe Args -> Args
    forall a. a -> Maybe a -> a
    fromMaybe Args
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe Args -> Args) -> Maybe Args -> Args
    forall a b. (a -> b) -> a -> b
    $ Elims -> Maybe Args
    forall a. [Elim' a] -> Maybe [Arg a]
    allApplyElims Elims
    pares

          -- Since we applying the clauses to the parameters,
          -- we do not need to drop their initial "parameter" patterns
          -- (this is taken care of by @apply@).
          cls <- Maybe System -> m [Clause] -> (System -> m [Clause]) -> m [Clause]
    forall a b. Maybe a -> b -> (a -> b) -> b
    caseMaybe Maybe System
    msys
                   ((Clause -> m Clause) -> [Clause] -> m [Clause]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM (NamedClause -> m Clause
    NamedClause -> m (ReifiesTo NamedClause)
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    forall (m :: * -> *).
    MonadReify m =>
    NamedClause -> m (ReifiesTo NamedClause)
    reify (NamedClause -> m Clause)
    -> (Clause -> NamedClause) -> Clause -> m Clause
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . QName -> Bool -> Clause -> NamedClause
    NamedClause QName
    x Bool
    False (Clause -> NamedClause)
    -> (Clause -> Clause) -> Clause -> NamedClause
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Clause -> Args -> Clause
    forall t. Apply t => t -> Args -> t
    `apply` Args
    pars)) [Clause]
    cls)
                   (QNamed System -> m [Clause]
    QNamed System -> m (ReifiesTo (QNamed System))
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    forall (m :: * -> *).
    MonadReify m =>
    QNamed System -> m (ReifiesTo (QNamed System))
    reify (QNamed System -> m [Clause])
    -> (System -> QNamed System) -> System -> m [Clause]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . QName -> System -> QNamed System
    forall a. QName -> a -> QNamed a
    QNamed QName
    x (System -> QNamed System)
    -> (System -> System) -> System -> QNamed System
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (System -> Args -> System
    forall t. Apply t => t -> Args -> t
    `apply` Args
    pars))
          let cx     = Name -> Name
    nameConcrete (Name -> Name) -> Name -> Name
    forall a b. (a -> b) -> a -> b
    $ QName -> Name
    qnameName QName
    x
              dInfo  = Name -> Fixity' -> Access -> IsAbstract -> Range -> DefInfo' Expr
    forall t.
    Name -> Fixity' -> Access -> IsAbstract -> Range -> DefInfo' t
    mkDefInfo Name
    cx Fixity'
    noFixity' Access
    PublicAccess IsAbstract
    ConcreteDef
                         (QName -> Range
    forall a. HasRange a => a -> Range
    getRange QName
    x)
              erased = case ArgInfo -> Quantity
    forall a. LensQuantity a => a -> Quantity
    getQuantity ArgInfo
    ai of
                Quantity0 Q0Origin
    o -> Q0Origin -> Erased
    Erased Q0Origin
    o
                Quantityω QωOrigin
    o -> QωOrigin -> Erased
    NotErased QωOrigin
    o
                Quantity1 Q1Origin
    o -> Erased
    forall a. HasCallStack => a
    __IMPOSSIBLE__
              lam = case [Clause]
    cls of
                []       -> ExprInfo -> Hiding -> Expr
    A.AbsurdLam ExprInfo
    exprNoRange Hiding
    NotHidden
                (Clause
    cl:[Clause]
    cls) -> ExprInfo
    -> DefInfo' Expr -> Erased -> QName -> List1 Clause -> Expr
    A.ExtendedLam ExprInfo
    exprNoRange DefInfo' Expr
    dInfo Erased
    erased QName
    x (Clause
    cl Clause -> [Clause] -> List1 Clause
    forall a. a -> [a] -> NonEmpty a
    :| [Clause]
    cls)
          elims lam =<< reify rest

    -- | @nameFirstIfHidden (x:a) ({e} es) = {x = e} es@
    nameFirstIfHidden :: Dom (ArgName, t) -> [Elim' a] -> [Elim' (Named_ a)]
    nameFirstIfHidden :: forall t a.
    Dom (MetaNameSuggestion, t) -> [Elim' a] -> [Elim' (Named_ a)]
    nameFirstIfHidden Dom (MetaNameSuggestion, t)
    dom (I.Apply (Arg ArgInfo
    info a
    e) : [Elim' a]
    es) | ArgInfo -> Bool
    forall a. LensHiding a => a -> Bool
    notVisible ArgInfo
    info =
      Arg (Named_ a) -> Elim' (Named_ a)
    forall a. Arg a -> Elim' a
    I.Apply (ArgInfo -> Named_ a -> Arg (Named_ a)
    forall e. ArgInfo -> e -> Arg e
    Arg ArgInfo
    info (Maybe (WithOrigin (Ranged MetaNameSuggestion)) -> a -> Named_ a
    forall name a. Maybe name -> a -> Named name a
    Named (WithOrigin (Ranged MetaNameSuggestion)
    -> Maybe (WithOrigin (Ranged MetaNameSuggestion))
    forall a. a -> Maybe a
    Just (WithOrigin (Ranged MetaNameSuggestion)
     -> Maybe (WithOrigin (Ranged MetaNameSuggestion)))
    -> WithOrigin (Ranged MetaNameSuggestion)
    -> Maybe (WithOrigin (Ranged MetaNameSuggestion))
    forall a b. (a -> b) -> a -> b
    $ Origin
    -> Ranged MetaNameSuggestion
    -> WithOrigin (Ranged MetaNameSuggestion)
    forall a. Origin -> a -> WithOrigin a
    WithOrigin Origin
    Inserted (Ranged MetaNameSuggestion
     -> WithOrigin (Ranged MetaNameSuggestion))
    -> Ranged MetaNameSuggestion
    -> WithOrigin (Ranged MetaNameSuggestion)
    forall a b. (a -> b) -> a -> b
    $ MetaNameSuggestion -> Ranged MetaNameSuggestion
    forall a. a -> Ranged a
    unranged (MetaNameSuggestion -> Ranged MetaNameSuggestion)
    -> MetaNameSuggestion -> Ranged MetaNameSuggestion
    forall a b. (a -> b) -> a -> b
    $ (MetaNameSuggestion, t) -> MetaNameSuggestion
    forall a b. (a, b) -> a
    fst ((MetaNameSuggestion, t) -> MetaNameSuggestion)
    -> (MetaNameSuggestion, t) -> MetaNameSuggestion
    forall a b. (a -> b) -> a -> b
    $ Dom (MetaNameSuggestion, t) -> (MetaNameSuggestion, t)
    forall t e. Dom' t e -> e
    unDom Dom (MetaNameSuggestion, t)
    dom) a
    e)) Elim' (Named_ a) -> [Elim' (Named_ a)] -> [Elim' (Named_ a)]
    forall a. a -> [a] -> [a]
    :
      (Elim' a -> Elim' (Named_ a)) -> [Elim' a] -> [Elim' (Named_ a)]
    forall a b. (a -> b) -> [a] -> [b]
    map ((a -> Named_ a) -> Elim' a -> Elim' (Named_ a)
    forall a b. (a -> b) -> Elim' a -> Elim' b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap a -> Named_ a
    forall a name. a -> Named name a
    unnamed) [Elim' a]
    es
    nameFirstIfHidden Dom (MetaNameSuggestion, t)
    _ [Elim' a]
    es =
      (Elim' a -> Elim' (Named_ a)) -> [Elim' a] -> [Elim' (Named_ a)]
    forall a b. (a -> b) -> [a] -> [b]
    map ((a -> Named_ a) -> Elim' a -> Elim' (Named_ a)
    forall a b. (a -> b) -> Elim' a -> Elim' b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap a -> Named_ a
    forall a name. a -> Named name a
    unnamed) [Elim' a]
    es

    instance Reify i => Reify (Named n i) where
      type ReifiesTo (Named n i) = Named n (ReifiesTo i)

      reify :: forall (m :: * -> *).
    MonadReify m =>
    Named n i -> m (ReifiesTo (Named n i))
    reify = (i -> m (ReifiesTo i)) -> Named n i -> m (Named n (ReifiesTo i))
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Named n a -> f (Named n b)
    traverse i -> m (ReifiesTo i)
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    forall (m :: * -> *). MonadReify m => i -> m (ReifiesTo i)
    reify
      reifyWhen :: forall (m :: * -> *).
    MonadReify m =>
    Bool -> Named n i -> m (ReifiesTo (Named n i))
    reifyWhen Bool
    b = (i -> m (ReifiesTo i)) -> Named n i -> m (Named n (ReifiesTo i))
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Named n a -> f (Named n b)
    traverse (Bool -> i -> m (ReifiesTo i)
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    Bool -> i -> m (ReifiesTo i)
    forall (m :: * -> *). MonadReify m => Bool -> i -> m (ReifiesTo i)
    reifyWhen Bool
    b)

    -- | Skip reification of implicit and irrelevant args if option is off.
    instance Reify i => Reify (Arg i) where
      type ReifiesTo (Arg i) = Arg (ReifiesTo i)

      reify :: forall (m :: * -> *).
    MonadReify m =>
    Arg i -> m (ReifiesTo (Arg i))
    reify (Arg ArgInfo
    info i
    i) = ArgInfo -> ReifiesTo i -> Arg (ReifiesTo i)
    forall e. ArgInfo -> e -> Arg e
    Arg ArgInfo
    info (ReifiesTo i -> Arg (ReifiesTo i))
    -> m (ReifiesTo i) -> m (Arg (ReifiesTo i))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ((Bool -> i -> m (ReifiesTo i)) -> i -> Bool -> m (ReifiesTo i)
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip Bool -> i -> m (ReifiesTo i)
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    Bool -> i -> m (ReifiesTo i)
    forall (m :: * -> *). MonadReify m => Bool -> i -> m (ReifiesTo i)
    reifyWhen i
    i (Bool -> m (ReifiesTo i)) -> m Bool -> m (ReifiesTo i)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< m Bool
    condition)
        where condition :: m Bool
    condition = (Bool -> m Bool
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (ArgInfo -> Hiding
    argInfoHiding ArgInfo
    info Hiding -> Hiding -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Hiding
    Hidden) m Bool -> m Bool -> m Bool
    forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
    `or2M` m Bool
    forall (m :: * -> *). HasOptions m => m Bool
    showImplicitArguments)
                  m Bool -> m Bool -> m Bool
    forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
    `and2M` (Bool -> m Bool
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Bool -> Bool
    not (Bool -> Bool) -> Bool -> Bool
    forall a b. (a -> b) -> a -> b
    $ ArgInfo -> Bool
    forall a. LensRelevance a => a -> Bool
    isIrrelevant ArgInfo
    info) m Bool -> m Bool -> m Bool
    forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
    `or2M` m Bool
    forall (m :: * -> *). HasOptions m => m Bool
    showIrrelevantArguments)
      reifyWhen :: forall (m :: * -> *).
    MonadReify m =>
    Bool -> Arg i -> m (ReifiesTo (Arg i))
    reifyWhen Bool
    b Arg i
    i = (i -> m (ReifiesTo i)) -> Arg i -> m (Arg (ReifiesTo i))
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Arg a -> f (Arg b)
    traverse (Bool -> i -> m (ReifiesTo i)
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    Bool -> i -> m (ReifiesTo i)
    forall (m :: * -> *). MonadReify m => Bool -> i -> m (ReifiesTo i)
    reifyWhen Bool
    b) Arg i
    i
    {-# SPECIALIZE reify :: Reify i => Arg i -> TCM (ReifiesTo (Arg i)) #-}

    -- instance Reify Elim Expr where
    --   reifyWhen = reifyWhenE
    --   reify = \case
    --     I.IApply x y r -> appl "iapply" <$> reify (defaultArg r :: Arg Term)
    --     I.Apply v -> appl "apply" <$> reify v
    --     I.Proj f  -> appl "proj"  <$> reify ((defaultArg $ I.Def f []) :: Arg Term)
    --     where
    --       appl :: String -> Arg Expr -> Expr
    --       appl s v = A.App exprInfo (A.Lit empty (LitString s)) $ fmap unnamed v

    data NamedClause = NamedClause QName Bool I.Clause
      -- ^ Also tracks whether module parameters should be dropped from the patterns.

    -- The Monoid instance for Data.Map doesn't require that the values are a
    -- monoid.
    newtype MonoidMap k v = MonoidMap { forall k v. MonoidMap k v -> Map k v
    _unMonoidMap :: Map.Map k v }

    instance (Ord k, Monoid v) => Semigroup (MonoidMap k v) where
      MonoidMap Map k v
    m1 <> :: MonoidMap k v -> MonoidMap k v -> MonoidMap k v
    <> MonoidMap Map k v
    m2 = Map k v -> MonoidMap k v
    forall k v. Map k v -> MonoidMap k v
    MonoidMap ((v -> v -> v) -> Map k v -> Map k v -> Map k v
    forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
    Map.unionWith v -> v -> v
    forall a. Monoid a => a -> a -> a
    mappend Map k v
    m1 Map k v
    m2)

    instance (Ord k, Monoid v) => Monoid (MonoidMap k v) where
      mempty :: MonoidMap k v
    mempty = Map k v -> MonoidMap k v
    forall k v. Map k v -> MonoidMap k v
    MonoidMap Map k v
    forall k a. Map k a
    Map.empty
      mappend :: MonoidMap k v -> MonoidMap k v -> MonoidMap k v
    mappend = MonoidMap k v -> MonoidMap k v -> MonoidMap k v
    forall a. Semigroup a => a -> a -> a
    (<>)

    -- | Removes argument names.  Preserves names present in the source.
    removeNameUnlessUserWritten :: (LensNamed a, LensOrigin (NameOf a)) => a -> a
    removeNameUnlessUserWritten :: forall a. (LensNamed a, LensOrigin (NameOf a)) => a -> a
    removeNameUnlessUserWritten a
    a
      | (NameOf a -> Origin
    forall a. LensOrigin a => a -> Origin
    getOrigin (NameOf a -> Origin) -> Maybe (NameOf a) -> Maybe Origin
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> a -> Maybe (NameOf a)
    forall a. LensNamed a => a -> Maybe (NameOf a)
    getNameOf a
    a) Maybe Origin -> Maybe Origin -> Bool
    forall a. Eq a => a -> a -> Bool
    == Origin -> Maybe Origin
    forall a. a -> Maybe a
    Just Origin
    UserWritten = a
    a
      | Bool
    otherwise = Maybe (NameOf a) -> a -> a
    forall a. LensNamed a => Maybe (NameOf a) -> a -> a
    setNameOf Maybe (NameOf a)
    forall a. Maybe a
    Nothing a
    a

    {-# SPECIALIZE stripImplicits :: Set Name  -> A.Patterns -> A.Patterns -> TCM A.Patterns #-}
    -- | Removes implicit arguments that are not needed, that is, that don't bind
    --   any variables that are actually used and doesn't do pattern matching.
    --   Doesn't strip any arguments that were written explicitly by the user.
    stripImplicits :: MonadReify m
      => Set Name -- ^ Variables to always include (occurs on RHS of clause)
      -> A.Patterns -> A.Patterns -> m A.Patterns
    stripImplicits :: forall (m :: * -> *).
    MonadReify m =>
    Set Name -> Patterns -> Patterns -> m Patterns
    stripImplicits Set Name
    toKeep Patterns
    params Patterns
    ps = do
      -- if --show-implicit we don't need the names
      m Bool -> m Patterns -> m Patterns -> m Patterns
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
    ifM m Bool
    forall (m :: * -> *). HasOptions m => m Bool
    showImplicitArguments (Patterns -> m Patterns
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Patterns -> m Patterns) -> Patterns -> m Patterns
    forall a b. (a -> b) -> a -> b
    $ (Arg (Named_ Pattern) -> Arg (Named_ Pattern))
    -> Patterns -> Patterns
    forall a b. (a -> b) -> [a] -> [b]
    map ((Named_ Pattern -> Named_ Pattern)
    -> Arg (Named_ Pattern) -> Arg (Named_ Pattern)
    forall a b. (a -> b) -> Arg a -> Arg b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Named_ Pattern -> Named_ Pattern
    forall a. (LensNamed a, LensOrigin (NameOf a)) => a -> a
    removeNameUnlessUserWritten) Patterns
    ps) (m Patterns -> m Patterns) -> m Patterns -> m Patterns
    forall a b. (a -> b) -> a -> b
    $ do
        MetaNameSuggestion -> Nat -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    MetaNameSuggestion -> Nat -> TCMT IO Doc -> m ()
    reportSDoc MetaNameSuggestion
    "reify.implicit" Nat
    100 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
    forall a b. (a -> b) -> a -> b
    $ Doc -> TCMT IO Doc
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Doc -> TCMT IO Doc) -> Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    vcat
          [ Doc
    "stripping implicits"
          , Nat -> Doc -> Doc
    forall a. Nat -> Doc a -> Doc a
    nest Nat
    2 (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ Doc
    "ps   =" Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> Patterns -> Doc
    forall a. Show a => a -> Doc
    pshow Patterns
    ps
          ]
        let ps' :: Patterns
    ps' = Patterns -> Patterns
    blankDots (Patterns -> Patterns) -> Patterns -> Patterns
    forall a b. (a -> b) -> a -> b
    $ Patterns -> Patterns
    strip Patterns
    ps
        MetaNameSuggestion -> Nat -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    MetaNameSuggestion -> Nat -> TCMT IO Doc -> m ()
    reportSDoc MetaNameSuggestion
    "reify.implicit" Nat
    100 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
    forall a b. (a -> b) -> a -> b
    $ Doc -> TCMT IO Doc
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Doc -> TCMT IO Doc) -> Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    vcat
          [ Nat -> Doc -> Doc
    forall a. Nat -> Doc a -> Doc a
    nest Nat
    2 (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ Doc
    "ps'  =" Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> Patterns -> Doc
    forall a. Show a => a -> Doc
    pshow Patterns
    ps'
          ]
        Patterns -> m Patterns
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Patterns
    ps'
        where
          -- Replace variables in dot patterns by an underscore _ if they are hidden
          -- in the pattern. This is slightly nicer than making the implicts explicit.
          blankDots :: Patterns -> Patterns
    blankDots Patterns
    ps = Set Name -> Patterns -> Patterns
    forall a. BlankVars a => Set Name -> a -> a
    blank (Patterns -> Set Name
    forall a. Binder a => a -> Set Name
    varsBoundIn (Patterns -> Set Name) -> Patterns -> Set Name
    forall a b. (a -> b) -> a -> b
    $ Patterns
    params Patterns -> Patterns -> Patterns
    forall a. [a] -> [a] -> [a]
    ++ Patterns
    ps) Patterns
    ps

          strip :: Patterns -> Patterns
    strip Patterns
    ps = Bool -> Patterns -> Patterns
    stripArgs Bool
    True Patterns
    ps
            where
              stripArgs :: Bool -> Patterns -> Patterns
    stripArgs Bool
    _ [] = []
              stripArgs Bool
    fixedPos (Arg (Named_ Pattern)
    a : Patterns
    as)
                -- A hidden non-UserWritten variable is removed if not needed for
                -- correct position of the following hidden arguments.
                | Arg (Named_ Pattern) -> Bool
    canStrip Arg (Named_ Pattern)
    a =
                     if   (Arg (Named_ Pattern) -> Bool) -> Patterns -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all Arg (Named_ Pattern) -> Bool
    canStrip (Patterns -> Bool) -> Patterns -> Bool
    forall a b. (a -> b) -> a -> b
    $ (Arg (Named_ Pattern) -> Bool) -> Patterns -> Patterns
    forall a. (a -> Bool) -> [a] -> [a]
    takeWhile Arg (Named_ Pattern) -> Bool
    forall {a}. (LensHiding a, LensNamed a, IsProjP a) => a -> Bool
    isUnnamedHidden Patterns
    as
                     then Bool -> Patterns -> Patterns
    stripArgs Bool
    False Patterns
    as
                     else Patterns
    goWild
                -- Other arguments are kept.
                | Bool
    otherwise = Bool -> Arg (Named_ Pattern) -> Arg (Named_ Pattern)
    forall {f :: * -> *} {b}.
    (Functor f, LensNamed b, LensOrigin (NameOf b)) =>
    Bool -> f b -> f b
    stripName Bool
    fixedPos (Arg (Named_ Pattern) -> Arg (Named_ Pattern)
    stripArg Arg (Named_ Pattern)
    a) Arg (Named_ Pattern) -> Patterns -> Patterns
    forall a. a -> [a] -> [a]
    : Bool -> Patterns -> Patterns
    stripArgs Bool
    True Patterns
    as
                where
                  a' :: Arg (Named_ Pattern)
    a'     = Arg (Named_ Pattern) -> Pattern -> Arg (Named_ Pattern)
    forall a b. NamedArg a -> b -> NamedArg b
    setNamedArg Arg (Named_ Pattern)
    a (Pattern -> Arg (Named_ Pattern))
    -> Pattern -> Arg (Named_ 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
    Info.PatRange (Range -> PatInfo) -> Range -> PatInfo
    forall a b. (a -> b) -> a -> b
    $ Arg (Named_ Pattern) -> Range
    forall a. HasRange a => a -> Range
    getRange Arg (Named_ Pattern)
    a
                  goWild :: Patterns
    goWild = Bool -> Arg (Named_ Pattern) -> Arg (Named_ Pattern)
    forall {f :: * -> *} {b}.
    (Functor f, LensNamed b, LensOrigin (NameOf b)) =>
    Bool -> f b -> f b
    stripName Bool
    fixedPos Arg (Named_ Pattern)
    a' Arg (Named_ Pattern) -> Patterns -> Patterns
    forall a. a -> [a] -> [a]
    : Bool -> Patterns -> Patterns
    stripArgs Bool
    True Patterns
    as

              stripName :: Bool -> f b -> f b
    stripName Bool
    True  = (b -> b) -> f b -> f b
    forall a b. (a -> b) -> f a -> f b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap b -> b
    forall a. (LensNamed a, LensOrigin (NameOf a)) => a -> a
    removeNameUnlessUserWritten
              stripName Bool
    False = f b -> f b
    forall a. a -> a
    id

              -- TODO: vars appearing in EqualPs shouldn't be stripped.
              canStrip :: Arg (Named_ Pattern) -> Bool
    canStrip Arg (Named_ Pattern)
    a = [Bool] -> Bool
    forall (t :: * -> *). Foldable t => t Bool -> Bool
    and
                [ Arg (Named_ Pattern) -> Bool
    forall a. LensHiding a => a -> Bool
    notVisible Arg (Named_ Pattern)
    a
                , Arg (Named_ Pattern) -> Origin
    forall a. LensOrigin a => a -> Origin
    getOrigin Arg (Named_ Pattern)
    a Origin -> [Origin] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `notElem` [ Origin
    UserWritten , Origin
    CaseSplit ]
                , (WithOrigin (Ranged MetaNameSuggestion) -> Origin
    forall a. LensOrigin a => a -> Origin
    getOrigin (WithOrigin (Ranged MetaNameSuggestion) -> Origin)
    -> Maybe (WithOrigin (Ranged MetaNameSuggestion)) -> Maybe Origin
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Arg (Named_ Pattern) -> Maybe (NameOf (Arg (Named_ Pattern)))
    forall a. LensNamed a => a -> Maybe (NameOf a)
    getNameOf Arg (Named_ Pattern)
    a) Maybe Origin -> Maybe Origin -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Origin -> Maybe Origin
    forall a. a -> Maybe a
    Just Origin
    UserWritten
                , Pattern -> Bool
    forall {e}. Pattern' e -> Bool
    varOrDot (Arg (Named_ Pattern) -> Pattern
    forall a. NamedArg a -> a
    namedArg Arg (Named_ Pattern)
    a)
                , Bool -> Bool
    not (Bool -> Bool) -> Bool -> Bool
    forall a b. (a -> b) -> a -> b
    $ Pattern -> Bool
    mustKeepVar (Arg (Named_ Pattern) -> Pattern
    forall a. NamedArg a -> a
    namedArg Arg (Named_ Pattern)
    a)
                ]

              mustKeepVar :: Pattern -> Bool
    mustKeepVar (A.VarP (A.BindName Name
    x)) = Name -> Set Name -> Bool
    forall a. Ord a => a -> Set a -> Bool
    Set.member Name
    x Set Name
    toKeep
              mustKeepVar Pattern
    _                       = Bool
    False

              isUnnamedHidden :: a -> Bool
    isUnnamedHidden a
    x = a -> Bool
    forall a. LensHiding a => a -> Bool
    notVisible a
    x Bool -> Bool -> Bool
    && Maybe (NameOf a) -> Bool
    forall a. Maybe a -> Bool
    isNothing (a -> Maybe (NameOf a)
    forall a. LensNamed a => a -> Maybe (NameOf a)
    getNameOf a
    x) Bool -> Bool -> Bool
    && Maybe (ProjOrigin, AmbiguousQName) -> Bool
    forall a. Maybe a -> Bool
    isNothing (a -> Maybe (ProjOrigin, AmbiguousQName)
    forall a. IsProjP a => a -> Maybe (ProjOrigin, AmbiguousQName)
    isProjP a
    x)

              stripArg :: Arg (Named_ Pattern) -> Arg (Named_ Pattern)
    stripArg Arg (Named_ Pattern)
    a = (Named_ Pattern -> Named_ Pattern)
    -> Arg (Named_ Pattern) -> Arg (Named_ Pattern)
    forall a b. (a -> b) -> Arg a -> Arg b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((Pattern -> Pattern) -> Named_ Pattern -> Named_ Pattern
    forall a b.
    (a -> b)
    -> Named (WithOrigin (Ranged MetaNameSuggestion)) a
    -> Named (WithOrigin (Ranged MetaNameSuggestion)) b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Pattern -> Pattern
    stripPat) Arg (Named_ Pattern)
    a

              stripPat :: Pattern -> Pattern
    stripPat = \case
                p :: Pattern
    p@(A.VarP BindName
    _)        -> Pattern
    p
                A.ConP ConPatInfo
    i AmbiguousQName
    c Patterns
    ps       -> ConPatInfo -> AmbiguousQName -> Patterns -> Pattern
    forall e. ConPatInfo -> AmbiguousQName -> NAPs e -> Pattern' e
    A.ConP ConPatInfo
    i AmbiguousQName
    c (Patterns -> Pattern) -> Patterns -> Pattern
    forall a b. (a -> b) -> a -> b
    $ Bool -> Patterns -> Patterns
    stripArgs Bool
    True Patterns
    ps
                p :: Pattern
    p@A.ProjP{}         -> Pattern
    p
                p :: Pattern
    p@(A.DefP PatInfo
    _ AmbiguousQName
    _ Patterns
    _)    -> Pattern
    p
                p :: Pattern
    p@(A.DotP PatInfo
    _ Expr
    _e)     -> Pattern
    p
                p :: Pattern
    p@(A.WildP PatInfo
    _)       -> Pattern
    p
                p :: Pattern
    p@(A.AbsurdP PatInfo
    _)     -> Pattern
    p
                p :: Pattern
    p@(A.LitP PatInfo
    _ Literal
    _)      -> Pattern
    p
                A.AsP PatInfo
    i BindName
    x Pattern
    p         -> PatInfo -> BindName -> Pattern -> Pattern
    forall e. PatInfo -> BindName -> Pattern' e -> Pattern' e
    A.AsP PatInfo
    i BindName
    x (Pattern -> Pattern) -> Pattern -> Pattern
    forall a b. (a -> b) -> a -> b
    $ Pattern -> Pattern
    stripPat Pattern
    p
                A.PatternSynP PatInfo
    _ AmbiguousQName
    _ Patterns
    _ -> Pattern
    forall a. HasCallStack => a
    __IMPOSSIBLE__
                A.RecP KwRange
    kwr ConPatInfo
    i [FieldAssignment' Pattern]
    fs     -> KwRange -> ConPatInfo -> [FieldAssignment' Pattern] -> Pattern
    forall e.
    KwRange
    -> ConPatInfo -> [FieldAssignment' (Pattern' e)] -> Pattern' e
    A.RecP KwRange
    kwr ConPatInfo
    i ([FieldAssignment' Pattern] -> Pattern)
    -> [FieldAssignment' Pattern] -> Pattern
    forall a b. (a -> b) -> a -> b
    $ (FieldAssignment' Pattern -> FieldAssignment' Pattern)
    -> [FieldAssignment' Pattern] -> [FieldAssignment' Pattern]
    forall a b. (a -> b) -> [a] -> [b]
    map ((Pattern -> Pattern)
    -> FieldAssignment' Pattern -> FieldAssignment' Pattern
    forall a b. (a -> b) -> FieldAssignment' a -> FieldAssignment' b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Pattern -> Pattern
    stripPat) [FieldAssignment' Pattern]
    fs  -- TODO Andreas: is this right?
                p :: Pattern
    p@A.EqualP{}        -> Pattern
    p -- EqualP cannot be blanked.
                A.WithP PatInfo
    i Pattern
    p         -> PatInfo -> Pattern -> Pattern
    forall e. PatInfo -> Pattern' e -> Pattern' e
    A.WithP PatInfo
    i (Pattern -> Pattern) -> Pattern -> Pattern
    forall a b. (a -> b) -> a -> b
    $ Pattern -> Pattern
    stripPat Pattern
    p -- TODO #2822: right?

              varOrDot :: Pattern' e -> Bool
    varOrDot A.VarP{}      = Bool
    True
              varOrDot A.WildP{}     = Bool
    True
              varOrDot A.DotP{}      = Bool
    True
              varOrDot (A.ConP ConPatInfo
    cpi AmbiguousQName
    _ NAPs e
    ps) | ConPatInfo -> ConInfo
    conPatOrigin ConPatInfo
    cpi ConInfo -> ConInfo -> Bool
    forall a. Eq a => a -> a -> Bool
    == ConInfo
    ConOSystem
                                     = ConPatInfo -> ConPatLazy
    conPatLazy ConPatInfo
    cpi ConPatLazy -> ConPatLazy -> Bool
    forall a. Eq a => a -> a -> Bool
    == ConPatLazy
    ConPatLazy Bool -> Bool -> Bool
    || (NamedArg (Pattern' e) -> Bool) -> NAPs e -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all (Pattern' e -> Bool
    varOrDot (Pattern' e -> Bool)
    -> (NamedArg (Pattern' e) -> Pattern' e)
    -> NamedArg (Pattern' e)
    -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . NamedArg (Pattern' e) -> Pattern' e
    forall a. NamedArg a -> a
    namedArg) NAPs e
    ps
              varOrDot Pattern' e
    _             = Bool
    False

    {-# SPECIALIZE blankNotInScope :: BlankVars a => a -> TCM a #-}
    {-# SPECIALIZE blankNotInScope :: Expr -> TCM Expr #-}
    -- | @blankNotInScope e@ replaces variables in expression @e@ with @_@
    -- if they are currently not in scope.
    blankNotInScope :: (MonadTCEnv m, MonadDebug m, BlankVars a) => a -> m a
    blankNotInScope :: forall (m :: * -> *) a.
    (MonadTCEnv m, MonadDebug m, BlankVars a) =>
    a -> m a
    blankNotInScope a
    e = do
      ctxNames <- m [Name]
    forall (m :: * -> *). MonadTCEnv m => m [Name]
    getContextNames
      letNames <- map fst <$> getLetBindings
      let names = [Name] -> Set Name
    forall a. Ord a => [a] -> Set a
    Set.fromList ([Name] -> Set Name) -> ([Name] -> [Name]) -> [Name] -> Set Name
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Name -> Bool) -> [Name] -> [Name]
    forall a. (a -> Bool) -> [a] -> [a]
    filter ((NameInScope -> NameInScope -> Bool
    forall a. Eq a => a -> a -> Bool
    == NameInScope
    C.InScope) (NameInScope -> Bool) -> (Name -> NameInScope) -> Name -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Name -> NameInScope
    forall a. LensInScope a => a -> NameInScope
    C.isInScope) ([Name] -> Set Name) -> [Name] -> Set Name
    forall a b. (a -> b) -> a -> b
    $ [Name]
    ctxNames [Name] -> [Name] -> [Name]
    forall a. [a] -> [a] -> [a]
    ++ [Name]
    letNames
      reportSDoc "reify.blank" 80 . pure $ "names in scope for blanking:" <+> pretty names
      return $ blank names e

    -- | @blank bound e@ replaces all variables in expression @e@ that are not in @bound@ by
    --   an underscore @_@. It is used for printing dot patterns: we don't want to
    --   make implicit variables explicit, so we blank them out in the dot patterns
    --   instead (this is fine since dot patterns can be inferred anyway).

    class BlankVars a where
      blank :: Set Name -> a -> a

      default blank :: (Functor f, BlankVars b, f b ~ a) => Set Name -> a -> a
      blank = (b -> b) -> a -> a
    (b -> b) -> f b -> f b
    forall a b. (a -> b) -> f a -> f b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((b -> b) -> a -> a) -> (Set Name -> b -> b) -> Set Name -> a -> a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Set Name -> b -> b
    forall a. BlankVars a => Set Name -> a -> a
    blank

    instance BlankVars a => BlankVars (Arg a)
    instance BlankVars a => BlankVars (Named s a)
    instance BlankVars a => BlankVars [a]
    instance BlankVars a => BlankVars (List1 a)
    instance BlankVars a => BlankVars (FieldAssignment' a)
    -- instance BlankVars a => BlankVars (A.Pattern' a)         -- see case EqualP !

    instance (BlankVars a, BlankVars b) => BlankVars (a, b) where
      blank :: Set Name -> (a, b) -> (a, b)
    blank Set Name
    bound (a
    x, b
    y) = (Set Name -> a -> a
    forall a. BlankVars a => Set Name -> a -> a
    blank Set Name
    bound a
    x, Set Name -> b -> b
    forall a. BlankVars a => Set Name -> a -> a
    blank Set Name
    bound b
    y)

    instance (BlankVars a, BlankVars b) => BlankVars (Either a b) where
      blank :: Set Name -> Either a b -> Either a b
    blank Set Name
    bound (Left a
    x)  = a -> Either a b
    forall a b. a -> Either a b
    Left (a -> Either a b) -> a -> Either a b
    forall a b. (a -> b) -> a -> b
    $ Set Name -> a -> a
    forall a. BlankVars a => Set Name -> a -> a
    blank Set Name
    bound a
    x
      blank Set Name
    bound (Right b
    y) = b -> Either a b
    forall a b. b -> Either a b
    Right (b -> Either a b) -> b -> Either a b
    forall a b. (a -> b) -> a -> b
    $ Set Name -> b -> b
    forall a. BlankVars a => Set Name -> a -> a
    blank Set Name
    bound b
    y

    instance BlankVars A.ProblemEq where
      blank :: Set Name -> ProblemEq -> ProblemEq
    blank Set Name
    bound = ProblemEq -> ProblemEq
    forall a. a -> a
    id

    instance BlankVars A.Clause where
      blank :: Set Name -> Clause -> Clause
    blank Set Name
    bound (A.Clause LHS
    lhs [ProblemEq]
    strippedPats RHS
    rhs WhereDeclarations
    wh Catchall
    ca)
        | WhereDeclarations -> Bool
    forall a. Null a => a -> Bool
    null WhereDeclarations
    wh =
            LHS
    -> [ProblemEq] -> RHS -> WhereDeclarations -> Catchall -> Clause
    forall lhs.
    lhs
    -> [ProblemEq]
    -> RHS
    -> WhereDeclarations
    -> Catchall
    -> Clause' lhs
    A.Clause (Set Name -> LHS -> LHS
    forall a. BlankVars a => Set Name -> a -> a
    blank Set Name
    bound' LHS
    lhs)
                     (Set Name -> [ProblemEq] -> [ProblemEq]
    forall a. BlankVars a => Set Name -> a -> a
    blank Set Name
    bound' [ProblemEq]
    strippedPats)
                     (Set Name -> RHS -> RHS
    forall a. BlankVars a => Set Name -> a -> a
    blank Set Name
    bound' RHS
    rhs) WhereDeclarations
    noWhereDecls Catchall
    ca
        | Bool
    otherwise = Clause
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        where bound' :: Set Name
    bound' = LHS -> Set Name
    forall a. Binder a => a -> Set Name
    varsBoundIn LHS
    lhs Set Name -> Set Name -> Set Name
    forall a. Ord a => Set a -> Set a -> Set a
    `Set.union` Set Name
    bound

    instance BlankVars A.LHS where
      blank :: Set Name -> LHS -> LHS
    blank Set Name
    bound (A.LHS LHSInfo
    i LHSCore
    core) = LHSInfo -> LHSCore -> LHS
    A.LHS LHSInfo
    i (LHSCore -> LHS) -> LHSCore -> LHS
    forall a b. (a -> b) -> a -> b
    $ Set Name -> LHSCore -> LHSCore
    forall a. BlankVars a => Set Name -> a -> a
    blank Set Name
    bound LHSCore
    core

    instance BlankVars A.LHSCore where
      blank :: Set Name -> LHSCore -> LHSCore
    blank Set Name
    bound (A.LHSHead QName
    f Patterns
    ps) = QName -> Patterns -> LHSCore
    forall e. QName -> [NamedArg (Pattern' e)] -> LHSCore' e
    A.LHSHead QName
    f (Patterns -> LHSCore) -> Patterns -> LHSCore
    forall a b. (a -> b) -> a -> b
    $ Set Name -> Patterns -> Patterns
    forall a. BlankVars a => Set Name -> a -> a
    blank Set Name
    bound Patterns
    ps
      blank Set Name
    bound (A.LHSProj AmbiguousQName
    p NamedArg LHSCore
    b Patterns
    ps) = (NamedArg LHSCore -> Patterns -> LHSCore)
    -> (NamedArg LHSCore, Patterns) -> LHSCore
    forall a b c. (a -> b -> c) -> (a, b) -> c
    uncurry (AmbiguousQName -> NamedArg LHSCore -> Patterns -> LHSCore
    forall e.
    AmbiguousQName
    -> NamedArg (LHSCore' e) -> [NamedArg (Pattern' e)] -> LHSCore' e
    A.LHSProj AmbiguousQName
    p) ((NamedArg LHSCore, Patterns) -> LHSCore)
    -> (NamedArg LHSCore, Patterns) -> LHSCore
    forall a b. (a -> b) -> a -> b
    $ Set Name
    -> (NamedArg LHSCore, Patterns) -> (NamedArg LHSCore, Patterns)
    forall a. BlankVars a => Set Name -> a -> a
    blank Set Name
    bound (NamedArg LHSCore
    b, Patterns
    ps)
      blank Set Name
    bound (A.LHSWith LHSCore
    h List1 (Arg Pattern)
    wps Patterns
    ps) = ((LHSCore, List1 (Arg Pattern)) -> Patterns -> LHSCore)
    -> ((LHSCore, List1 (Arg Pattern)), Patterns) -> LHSCore
    forall a b c. (a -> b -> c) -> (a, b) -> c
    uncurry ((LHSCore -> List1 (Arg Pattern) -> Patterns -> LHSCore)
    -> (LHSCore, List1 (Arg Pattern)) -> Patterns -> LHSCore
    forall a b c. (a -> b -> c) -> (a, b) -> c
    uncurry LHSCore -> List1 (Arg Pattern) -> Patterns -> LHSCore
    forall e.
    LHSCore' e
    -> List1 (Arg (Pattern' e))
    -> [NamedArg (Pattern' e)]
    -> LHSCore' e
    A.LHSWith) (((LHSCore, List1 (Arg Pattern)), Patterns) -> LHSCore)
    -> ((LHSCore, List1 (Arg Pattern)), Patterns) -> LHSCore
    forall a b. (a -> b) -> a -> b
    $ Set Name
    -> ((LHSCore, List1 (Arg Pattern)), Patterns)
    -> ((LHSCore, List1 (Arg Pattern)), Patterns)
    forall a. BlankVars a => Set Name -> a -> a
    blank Set Name
    bound ((LHSCore
    h, List1 (Arg Pattern)
    wps), Patterns
    ps)

    instance BlankVars A.Pattern where
      blank :: Set Name -> Pattern -> Pattern
    blank Set Name
    bound Pattern
    p = case Pattern
    p of
        A.VarP BindName
    _      -> Pattern
    p   -- do not blank pattern vars
        A.ConP ConPatInfo
    c AmbiguousQName
    i Patterns
    ps -> ConPatInfo -> AmbiguousQName -> Patterns -> Pattern
    forall e. ConPatInfo -> AmbiguousQName -> NAPs e -> Pattern' e
    A.ConP ConPatInfo
    c AmbiguousQName
    i (Patterns -> Pattern) -> Patterns -> Pattern
    forall a b. (a -> b) -> a -> b
    $ Set Name -> Patterns -> Patterns
    forall a. BlankVars a => Set Name -> a -> a
    blank Set Name
    bound Patterns
    ps
        A.ProjP{}     -> Pattern
    p
        A.DefP PatInfo
    i AmbiguousQName
    f Patterns
    ps -> PatInfo -> AmbiguousQName -> Patterns -> Pattern
    forall e. PatInfo -> AmbiguousQName -> NAPs e -> Pattern' e
    A.DefP PatInfo
    i AmbiguousQName
    f (Patterns -> Pattern) -> Patterns -> Pattern
    forall a b. (a -> b) -> a -> b
    $ Set Name -> Patterns -> Patterns
    forall a. BlankVars a => Set Name -> a -> a
    blank Set Name
    bound Patterns
    ps
        A.DotP PatInfo
    i Expr
    e    -> PatInfo -> Expr -> Pattern
    forall e. PatInfo -> e -> Pattern' e
    A.DotP PatInfo
    i (Expr -> Pattern) -> Expr -> Pattern
    forall a b. (a -> b) -> a -> b
    $ Set Name -> Expr -> Expr
    forall a. BlankVars a => Set Name -> a -> a
    blank Set Name
    bound Expr
    e
        A.WildP PatInfo
    _     -> Pattern
    p
        A.AbsurdP PatInfo
    _   -> Pattern
    p
        A.LitP PatInfo
    _ Literal
    _    -> Pattern
    p
        A.AsP PatInfo
    i BindName
    n Pattern
    p   -> PatInfo -> BindName -> Pattern -> Pattern
    forall e. PatInfo -> BindName -> Pattern' e -> Pattern' e
    A.AsP PatInfo
    i BindName
    n (Pattern -> Pattern) -> Pattern -> Pattern
    forall a b. (a -> b) -> a -> b
    $ Set Name -> Pattern -> Pattern
    forall a. BlankVars a => Set Name -> a -> a
    blank Set Name
    bound Pattern
    p
        A.PatternSynP PatInfo
    _ AmbiguousQName
    _ Patterns
    _ -> Pattern
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        A.RecP KwRange
    kwr ConPatInfo
    i [FieldAssignment' Pattern]
    fs -> KwRange -> ConPatInfo -> [FieldAssignment' Pattern] -> Pattern
    forall e.
    KwRange
    -> ConPatInfo -> [FieldAssignment' (Pattern' e)] -> Pattern' e
    A.RecP KwRange
    kwr ConPatInfo
    i ([FieldAssignment' Pattern] -> Pattern)
    -> [FieldAssignment' Pattern] -> Pattern
    forall a b. (a -> b) -> a -> b
    $ Set Name
    -> [FieldAssignment' Pattern] -> [FieldAssignment' Pattern]
    forall a. BlankVars a => Set Name -> a -> a
    blank Set Name
    bound [FieldAssignment' Pattern]
    fs
        A.EqualP{}    -> Pattern
    p
        A.WithP PatInfo
    i Pattern
    p   -> PatInfo -> Pattern -> Pattern
    forall e. PatInfo -> Pattern' e -> Pattern' e
    A.WithP PatInfo
    i (Set Name -> Pattern -> Pattern
    forall a. BlankVars a => Set Name -> a -> a
    blank Set Name
    bound Pattern
    p)

    instance BlankVars A.Expr where
      blank :: Set Name -> Expr -> Expr
    blank Set Name
    bound Expr
    e = case Expr
    e of
        A.ScopedExpr ScopeInfo
    i Expr
    e         -> ScopeInfo -> Expr -> Expr
    A.ScopedExpr ScopeInfo
    i (Expr -> Expr) -> Expr -> Expr
    forall a b. (a -> b) -> a -> b
    $ Set Name -> Expr -> Expr
    forall a. BlankVars a => Set Name -> a -> a
    blank Set Name
    bound Expr
    e
        A.Var Name
    x                  -> if Name
    x Name -> Set Name -> Bool
    forall a. Ord a => a -> Set a -> Bool
    `Set.member` Set Name
    bound then Expr
    e
                                    else MetaInfo -> Expr
    A.Underscore MetaInfo
    emptyMetaInfo  -- Here is the action!
        A.Def' QName
    _ Suffix
    _               -> Expr
    e
        A.Proj{}                 -> Expr
    e
        A.Con AmbiguousQName
    _                  -> Expr
    e
        A.Lit ExprInfo
    _ Literal
    _                -> Expr
    e
        A.QuestionMark{}         -> Expr
    e
        A.Underscore MetaInfo
    _           -> Expr
    e
        A.Dot ExprInfo
    i Expr
    e                -> ExprInfo -> Expr -> Expr
    A.Dot ExprInfo
    i (Expr -> Expr) -> Expr -> Expr
    forall a b. (a -> b) -> a -> b
    $ Set Name -> Expr -> Expr
    forall a. BlankVars a => Set Name -> a -> a
    blank Set Name
    bound Expr
    e
        A.App AppInfo
    i Expr
    e1 Arg (Named_ Expr)
    e2            -> (Expr -> Arg (Named_ Expr) -> Expr)
    -> (Expr, Arg (Named_ Expr)) -> Expr
    forall a b c. (a -> b -> c) -> (a, b) -> c
    uncurry (AppInfo -> Expr -> Arg (Named_ Expr) -> Expr
    A.App AppInfo
    i) ((Expr, Arg (Named_ Expr)) -> Expr)
    -> (Expr, Arg (Named_ Expr)) -> Expr
    forall a b. (a -> b) -> a -> b
    $ Set Name -> (Expr, Arg (Named_ Expr)) -> (Expr, Arg (Named_ Expr))
    forall a. BlankVars a => Set Name -> a -> a
    blank Set Name
    bound (Expr
    e1, Arg (Named_ Expr)
    e2)
        A.WithApp ExprInfo
    i Expr
    e List1 Expr
    es         -> (Expr -> List1 Expr -> Expr) -> (Expr, List1 Expr) -> Expr
    forall a b c. (a -> b -> c) -> (a, b) -> c
    uncurry (ExprInfo -> Expr -> List1 Expr -> Expr
    A.WithApp ExprInfo
    i) ((Expr, List1 Expr) -> Expr) -> (Expr, List1 Expr) -> Expr
    forall a b. (a -> b) -> a -> b
    $ Set Name -> (Expr, List1 Expr) -> (Expr, List1 Expr)
    forall a. BlankVars a => Set Name -> a -> a
    blank Set Name
    bound (Expr
    e, List1 Expr
    es)
        A.Lam ExprInfo
    i LamBinding
    b Expr
    e              -> let bound' :: Set Name
    bound' = LamBinding -> Set Name
    forall a. Binder a => a -> Set Name
    varsBoundIn LamBinding
    b Set Name -> Set Name -> Set Name
    forall a. Ord a => Set a -> Set a -> Set a
    `Set.union` Set Name
    bound
                                    in  ExprInfo -> LamBinding -> Expr -> Expr
    A.Lam ExprInfo
    i (Set Name -> LamBinding -> LamBinding
    forall a. BlankVars a => Set Name -> a -> a
    blank Set Name
    bound LamBinding
    b) (Set Name -> Expr -> Expr
    forall a. BlankVars a => Set Name -> a -> a
    blank Set Name
    bound' Expr
    e)
        A.AbsurdLam ExprInfo
    _ Hiding
    _          -> Expr
    e
        A.ExtendedLam ExprInfo
    i DefInfo' Expr
    d Erased
    e QName
    f List1 Clause
    cs -> ExprInfo
    -> DefInfo' Expr -> Erased -> QName -> List1 Clause -> Expr
    A.ExtendedLam ExprInfo
    i DefInfo' Expr
    d Erased
    e QName
    f (List1 Clause -> Expr) -> List1 Clause -> Expr
    forall a b. (a -> b) -> a -> b
    $ Set Name -> List1 Clause -> List1 Clause
    forall a. BlankVars a => Set Name -> a -> a
    blank Set Name
    bound List1 Clause
    cs
        A.Pi ExprInfo
    i Telescope1
    tel Expr
    e             -> let bound' :: Set Name
    bound' = Telescope1 -> Set Name
    forall a. Binder a => a -> Set Name
    varsBoundIn Telescope1
    tel Set Name -> Set Name -> Set Name
    forall a. Ord a => Set a -> Set a -> Set a
    `Set.union` Set Name
    bound
                                    in  (Telescope1 -> Expr -> Expr) -> (Telescope1, Expr) -> Expr
    forall a b c. (a -> b -> c) -> (a, b) -> c
    uncurry (ExprInfo -> Telescope1 -> Expr -> Expr
    A.Pi ExprInfo
    i) ((Telescope1, Expr) -> Expr) -> (Telescope1, Expr) -> Expr
    forall a b. (a -> b) -> a -> b
    $ Set Name -> (Telescope1, Expr) -> (Telescope1, Expr)
    forall a. BlankVars a => Set Name -> a -> a
    blank Set Name
    bound' (Telescope1
    tel, Expr
    e)
        A.Generalized {}         -> Expr
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        A.Fun ExprInfo
    i Arg Expr
    a Expr
    b              -> (Arg Expr -> Expr -> Expr) -> (Arg Expr, Expr) -> Expr
    forall a b c. (a -> b -> c) -> (a, b) -> c
    uncurry (ExprInfo -> Arg Expr -> Expr -> Expr
    A.Fun ExprInfo
    i) ((Arg Expr, Expr) -> Expr) -> (Arg Expr, Expr) -> Expr
    forall a b. (a -> b) -> a -> b
    $ Set Name -> (Arg Expr, Expr) -> (Arg Expr, Expr)
    forall a. BlankVars a => Set Name -> a -> a
    blank Set Name
    bound (Arg Expr
    a, Expr
    b)
        A.Let ExprInfo
    _ List1 LetBinding
    _ Expr
    _              -> Expr
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        A.Rec KwRange
    kwr ExprInfo
    i RecordAssigns
    es           -> KwRange -> ExprInfo -> RecordAssigns -> Expr
    A.Rec KwRange
    kwr ExprInfo
    i (RecordAssigns -> Expr) -> RecordAssigns -> Expr
    forall a b. (a -> b) -> a -> b
    $ Set Name -> RecordAssigns -> RecordAssigns
    forall a. BlankVars a => Set Name -> a -> a
    blank Set Name
    bound RecordAssigns
    es
        A.RecUpdate KwRange
    kwr ExprInfo
    i Expr
    e Assigns
    es   -> (Expr -> Assigns -> Expr) -> (Expr, Assigns) -> Expr
    forall a b c. (a -> b -> c) -> (a, b) -> c
    uncurry (KwRange -> ExprInfo -> Expr -> Assigns -> Expr
    A.RecUpdate KwRange
    kwr ExprInfo
    i) ((Expr, Assigns) -> Expr) -> (Expr, Assigns) -> Expr
    forall a b. (a -> b) -> a -> b
    $ Set Name -> (Expr, Assigns) -> (Expr, Assigns)
    forall a. BlankVars a => Set Name -> a -> a
    blank Set Name
    bound (Expr
    e, Assigns
    es)
        A.Quote {}               -> Expr
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        A.QuoteTerm {}           -> Expr
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        A.Unquote {}             -> Expr
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        A.DontCare Expr
    v             -> Expr -> Expr
    A.DontCare (Expr -> Expr) -> Expr -> Expr
    forall a b. (a -> b) -> a -> b
    $ Set Name -> Expr -> Expr
    forall a. BlankVars a => Set Name -> a -> a
    blank Set Name
    bound Expr
    v
        A.PatternSyn {}          -> Expr
    e
        A.Macro {}               -> Expr
    e

    instance BlankVars A.ModuleName where
      blank :: Set Name -> ModuleName -> ModuleName
    blank Set Name
    bound = ModuleName -> ModuleName
    forall a. a -> a
    id

    instance BlankVars RHS where
      blank :: Set Name -> RHS -> RHS
    blank Set Name
    bound (RHS Expr
    e Maybe Expr
    mc)             = Expr -> Maybe Expr -> RHS
    RHS (Set Name -> Expr -> Expr
    forall a. BlankVars a => Set Name -> a -> a
    blank Set Name
    bound Expr
    e) Maybe Expr
    mc
      blank Set Name
    bound RHS
    AbsurdRHS              = RHS
    AbsurdRHS
      blank Set Name
    bound (WithRHS QName
    _ List1 WithExpr
    es List1 Clause
    clauses) = RHS
    forall a. HasCallStack => a
    __IMPOSSIBLE__ -- NZ
      blank Set Name
    bound (RewriteRHS [RewriteEqn]
    xes [ProblemEq]
    spats RHS
    rhs WhereDeclarations
    _) = RHS
    forall a. HasCallStack => a
    __IMPOSSIBLE__ -- NZ

    instance BlankVars A.LamBinding where
      blank :: Set Name -> LamBinding -> LamBinding
    blank Set Name
    bound b :: LamBinding
    b@A.DomainFree{} = LamBinding
    b
      blank Set Name
    bound (A.DomainFull TypedBinding
    bs) = TypedBinding -> LamBinding
    A.DomainFull (TypedBinding -> LamBinding) -> TypedBinding -> LamBinding
    forall a b. (a -> b) -> a -> b
    $ Set Name -> TypedBinding -> TypedBinding
    forall a. BlankVars a => Set Name -> a -> a
    blank Set Name
    bound TypedBinding
    bs

    instance BlankVars TypedBinding where
      blank :: Set Name -> TypedBinding -> TypedBinding
    blank Set Name
    bound (TBind Range
    r TypedBindingInfo
    t List1 (Arg (Named (WithOrigin (Ranged MetaNameSuggestion)) Binder))
    n Expr
    e) = Range
    -> TypedBindingInfo
    -> List1
         (Arg (Named (WithOrigin (Ranged MetaNameSuggestion)) Binder))
    -> Expr
    -> TypedBinding
    TBind Range
    r TypedBindingInfo
    t List1 (Arg (Named (WithOrigin (Ranged MetaNameSuggestion)) Binder))
    n (Expr -> TypedBinding) -> Expr -> TypedBinding
    forall a b. (a -> b) -> a -> b
    $ Set Name -> Expr -> Expr
    forall a. BlankVars a => Set Name -> a -> a
    blank Set Name
    bound Expr
    e
      blank Set Name
    bound (TLet Range
    _ List1 LetBinding
    _)    = TypedBinding
    forall a. HasCallStack => a
    __IMPOSSIBLE__ -- Since the internal syntax has no let bindings left

    -- | Collect the binders in some abstract syntax lhs.

    class Binder a where
      varsBoundIn :: a -> Set Name

      default varsBoundIn :: (Foldable f, Binder b, f b ~ a) => a -> Set Name
      varsBoundIn = (b -> Set Name) -> f b -> Set Name
    forall m a. Monoid m => (a -> m) -> f a -> m
    forall (t :: * -> *) m a.
    (Foldable t, Monoid m) =>
    (a -> m) -> t a -> m
    foldMap b -> Set Name
    forall a. Binder a => a -> Set Name
    varsBoundIn

    instance Binder A.LHS where
      varsBoundIn :: LHS -> Set Name
    varsBoundIn (A.LHS LHSInfo
    _ LHSCore
    core) = LHSCore -> Set Name
    forall a. Binder a => a -> Set Name
    varsBoundIn LHSCore
    core

    instance Binder A.LHSCore where
      varsBoundIn :: LHSCore -> Set Name
    varsBoundIn (A.LHSHead QName
    _ Patterns
    ps)     = Patterns -> Set Name
    forall a. Binder a => a -> Set Name
    varsBoundIn Patterns
    ps
      varsBoundIn (A.LHSProj AmbiguousQName
    _ NamedArg LHSCore
    b Patterns
    ps)   = (NamedArg LHSCore, Patterns) -> Set Name
    forall a. Binder a => a -> Set Name
    varsBoundIn (NamedArg LHSCore
    b, Patterns
    ps)
      varsBoundIn (A.LHSWith LHSCore
    h List1 (Arg Pattern)
    wps Patterns
    ps) = ((LHSCore, List1 (Arg Pattern)), Patterns) -> Set Name
    forall a. Binder a => a -> Set Name
    varsBoundIn ((LHSCore
    h, List1 (Arg Pattern)
    wps), Patterns
    ps)

    instance Binder A.Pattern where
      varsBoundIn :: Pattern -> Set Name
    varsBoundIn = (Pattern' (ADotT Pattern) -> Set Name) -> Pattern -> Set Name
    forall p m.
    (APatternLike p, Monoid m) =>
    (Pattern' (ADotT p) -> m) -> p -> m
    foldAPattern ((Pattern' (ADotT Pattern) -> Set Name) -> Pattern -> Set Name)
    -> (Pattern' (ADotT Pattern) -> Set Name) -> Pattern -> Set Name
    forall a b. (a -> b) -> a -> b
    $ \case
        A.VarP BindName
    x            -> BindName -> Set Name
    forall a. Binder a => a -> Set Name
    varsBoundIn BindName
    x
        A.AsP PatInfo
    _ BindName
    x Pattern' (ADotT Pattern)
    _         -> Set Name
    forall a. Null a => a
    empty    -- Not x because of #2414 (?)
        A.ConP ConPatInfo
    _ AmbiguousQName
    _ NAPs (ADotT Pattern)
    _        -> Set Name
    forall a. Null a => a
    empty
        A.ProjP{}           -> Set Name
    forall a. Null a => a
    empty
        A.DefP PatInfo
    _ AmbiguousQName
    _ NAPs (ADotT Pattern)
    _        -> Set Name
    forall a. Null a => a
    empty
        A.WildP{}           -> Set Name
    forall a. Null a => a
    empty
        A.DotP{}            -> Set Name
    forall a. Null a => a
    empty
        A.AbsurdP{}         -> Set Name
    forall a. Null a => a
    empty
        A.LitP{}            -> Set Name
    forall a. Null a => a
    empty
        A.PatternSynP PatInfo
    _ AmbiguousQName
    _ NAPs (ADotT Pattern)
    _ -> Set Name
    forall a. Null a => a
    empty
        A.RecP KwRange
    _ ConPatInfo
    _ [FieldAssignment' (Pattern' (ADotT Pattern))]
    _        -> Set Name
    forall a. Null a => a
    empty
        A.EqualP{}          -> Set Name
    forall a. Null a => a
    empty
        A.WithP PatInfo
    _ Pattern' (ADotT Pattern)
    _         -> Set Name
    forall a. Null a => a
    empty

    instance Binder a => Binder (A.Binder' a) where
      varsBoundIn :: Binder' a -> Set Name
    varsBoundIn (A.Binder Maybe Pattern
    p BinderNameOrigin
    _ a
    n) = (Maybe Pattern, a) -> Set Name
    forall a. Binder a => a -> Set Name
    varsBoundIn (Maybe Pattern
    p, a
    n)

    instance Binder A.LamBinding where
      varsBoundIn :: LamBinding -> Set Name
    varsBoundIn (A.DomainFree TacticAttribute' Expr
    _ Arg (Named (WithOrigin (Ranged MetaNameSuggestion)) Binder)
    x) = Arg (Named (WithOrigin (Ranged MetaNameSuggestion)) Binder)
    -> Set Name
    forall a. Binder a => a -> Set Name
    varsBoundIn Arg (Named (WithOrigin (Ranged MetaNameSuggestion)) Binder)
    x
      varsBoundIn (A.DomainFull TypedBinding
    b)   = TypedBinding -> Set Name
    forall a. Binder a => a -> Set Name
    varsBoundIn TypedBinding
    b

    instance Binder TypedBinding where
      varsBoundIn :: TypedBinding -> Set Name
    varsBoundIn (TBind Range
    _ TypedBindingInfo
    _ List1 (Arg (Named (WithOrigin (Ranged MetaNameSuggestion)) Binder))
    xs Expr
    _) = List1 (Arg (Named (WithOrigin (Ranged MetaNameSuggestion)) Binder))
    -> Set Name
    forall a. Binder a => a -> Set Name
    varsBoundIn List1 (Arg (Named (WithOrigin (Ranged MetaNameSuggestion)) Binder))
    xs
      varsBoundIn (TLet Range
    _ List1 LetBinding
    bs)      = List1 LetBinding -> Set Name
    forall a. Binder a => a -> Set Name
    varsBoundIn List1 LetBinding
    bs

    instance Binder BindName where
      varsBoundIn :: BindName -> Set Name
    varsBoundIn BindName
    x = Name -> Set Name
    forall el coll. Singleton el coll => el -> coll
    singleton (BindName -> Name
    unBind BindName
    x)

    instance Binder A.LetBinding where
      varsBoundIn :: LetBinding -> Set Name
    varsBoundIn (LetBind LetInfo
    _ ArgInfo
    _ BindName
    x Expr
    _ Expr
    _) = BindName -> Set Name
    forall a. Binder a => a -> Set Name
    varsBoundIn BindName
    x
      varsBoundIn (LetAxiom LetInfo
    _ ArgInfo
    _ BindName
    x Expr
    _)  = BindName -> Set Name
    forall a. Binder a => a -> Set Name
    varsBoundIn BindName
    x
      varsBoundIn (LetPatBind LetInfo
    _ Pattern
    p Expr
    _)  = Pattern -> Set Name
    forall a. Binder a => a -> Set Name
    varsBoundIn Pattern
    p
      varsBoundIn LetApply{}          = Set Name
    forall a. Null a => a
    empty
      varsBoundIn LetOpen{}           = Set Name
    forall a. Null a => a
    empty

    instance Binder a => Binder (FieldAssignment' a)
    instance Binder a => Binder (Arg a)
    instance Binder a => Binder (Named x a)
    instance Binder a => Binder [a]
    instance Binder a => Binder (List1 a)
    instance Binder a => Binder (Maybe a)

    instance (Binder a, Binder b) => Binder (a, b) where
      varsBoundIn :: (a, b) -> Set Name
    varsBoundIn (a
    x, b
    y) = a -> Set Name
    forall a. Binder a => a -> Set Name
    varsBoundIn a
    x Set Name -> Set Name -> Set Name
    forall a. Ord a => Set a -> Set a -> Set a
    `Set.union` b -> Set Name
    forall a. Binder a => a -> Set Name
    varsBoundIn b
    y

    {-# SPECIALIZE reifyPatterns :: [NamedArg I.DeBruijnPattern] -> TCM [NamedArg A.Pattern] #-}
    -- | Assumes that pattern variables have been added to the context already.
    --   Picks pattern variable names from context.
    reifyPatterns :: MonadReify m => [NamedArg I.DeBruijnPattern] -> m [NamedArg A.Pattern]
    reifyPatterns :: forall (m :: * -> *).
    MonadReify m =>
    [NamedArg DeBruijnPattern] -> m Patterns
    reifyPatterns = (NamedArg DeBruijnPattern -> m (Arg (Named_ Pattern)))
    -> [NamedArg DeBruijnPattern] -> m Patterns
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM ((NamedArg DeBruijnPattern -> m (Arg (Named_ Pattern)))
     -> [NamedArg DeBruijnPattern] -> m Patterns)
    -> (NamedArg DeBruijnPattern -> m (Arg (Named_ Pattern)))
    -> [NamedArg DeBruijnPattern]
    -> m Patterns
    forall a b. (a -> b) -> a -> b
    $ (Arg (Named_ Pattern) -> Arg (Named_ Pattern)
    forall p. NamedArg p -> NamedArg p
    stripNameFromExplicit (Arg (Named_ Pattern) -> Arg (Named_ Pattern))
    -> (Arg (Named_ Pattern) -> Arg (Named_ Pattern))
    -> Arg (Named_ Pattern)
    -> Arg (Named_ Pattern)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Arg (Named_ Pattern) -> Arg (Named_ Pattern)
    forall p. IsProjP p => NamedArg p -> NamedArg p
    stripHidingFromPostfixProj) (Arg (Named_ Pattern) -> Arg (Named_ Pattern))
    -> (NamedArg DeBruijnPattern -> m (Arg (Named_ Pattern)))
    -> NamedArg DeBruijnPattern
    -> m (Arg (Named_ Pattern))
    forall (m :: * -> *) b c a.
    Functor m =>
    (b -> c) -> (a -> m b) -> a -> m c
    <.>
                           (Named_ DeBruijnPattern -> m (Named_ Pattern))
    -> NamedArg DeBruijnPattern -> m (Arg (Named_ Pattern))
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Arg a -> f (Arg b)
    traverse ((DeBruijnPattern -> m Pattern)
    -> Named_ DeBruijnPattern -> m (Named_ Pattern)
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b)
    -> Named (WithOrigin (Ranged MetaNameSuggestion)) a
    -> f (Named (WithOrigin (Ranged MetaNameSuggestion)) b)
    traverse DeBruijnPattern -> m Pattern
    forall (m :: * -> *). MonadReify m => DeBruijnPattern -> m Pattern
    reifyPat)
      where
        -- #4399 strip also empty names
        stripNameFromExplicit :: NamedArg p -> NamedArg p
        stripNameFromExplicit :: forall p. NamedArg p -> NamedArg p
    stripNameFromExplicit NamedArg p
    a
          | NamedArg p -> Bool
    forall a. LensHiding a => a -> Bool
    visible NamedArg p
    a Bool -> Bool -> Bool
    || Bool
    -> (MetaNameSuggestion -> Bool) -> Maybe MetaNameSuggestion -> Bool
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe Bool
    True ((Bool -> Bool -> Bool)
    -> (MetaNameSuggestion -> Bool)
    -> (MetaNameSuggestion -> Bool)
    -> MetaNameSuggestion
    -> Bool
    forall a b c.
    (a -> b -> c)
    -> (MetaNameSuggestion -> a)
    -> (MetaNameSuggestion -> b)
    -> MetaNameSuggestion
    -> c
    forall (f :: * -> *) a b c.
    Applicative f =>
    (a -> b -> c) -> f a -> f b -> f c
    liftA2 Bool -> Bool -> Bool
    (||) MetaNameSuggestion -> Bool
    forall a. Null a => a -> Bool
    null MetaNameSuggestion -> Bool
    forall a. IsNoName a => a -> Bool
    isNoName) (NamedArg p -> Maybe MetaNameSuggestion
    forall a.
    (LensNamed a, NameOf a ~ WithOrigin (Ranged MetaNameSuggestion)) =>
    a -> Maybe MetaNameSuggestion
    bareNameOf NamedArg p
    a) =
              (Named (WithOrigin (Ranged MetaNameSuggestion)) p
     -> Named (WithOrigin (Ranged MetaNameSuggestion)) p)
    -> NamedArg p -> NamedArg p
    forall a b. (a -> b) -> Arg a -> Arg b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (p -> Named (WithOrigin (Ranged MetaNameSuggestion)) p
    forall a name. a -> Named name a
    unnamed (p -> Named (WithOrigin (Ranged MetaNameSuggestion)) p)
    -> (Named (WithOrigin (Ranged MetaNameSuggestion)) p -> p)
    -> Named (WithOrigin (Ranged MetaNameSuggestion)) p
    -> Named (WithOrigin (Ranged MetaNameSuggestion)) p
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Named (WithOrigin (Ranged MetaNameSuggestion)) p -> p
    forall name a. Named name a -> a
    namedThing) NamedArg p
    a
          | Bool
    otherwise = NamedArg p
    a

        stripHidingFromPostfixProj :: IsProjP p => NamedArg p -> NamedArg p
        stripHidingFromPostfixProj :: forall p. IsProjP p => NamedArg p -> NamedArg p
    stripHidingFromPostfixProj NamedArg p
    a = case NamedArg p -> Maybe (ProjOrigin, AmbiguousQName)
    forall a. IsProjP a => a -> Maybe (ProjOrigin, AmbiguousQName)
    isProjP NamedArg p
    a of
          Just (ProjOrigin
    o, AmbiguousQName
    _) | ProjOrigin
    o ProjOrigin -> ProjOrigin -> Bool
    forall a. Eq a => a -> a -> Bool
    /= ProjOrigin
    ProjPrefix -> Hiding -> NamedArg p -> NamedArg p
    forall a. LensHiding a => Hiding -> a -> a
    setHiding Hiding
    NotHidden NamedArg p
    a
          Maybe (ProjOrigin, AmbiguousQName)
    _                             -> NamedArg p
    a

        reifyPat :: MonadReify m => I.DeBruijnPattern -> m A.Pattern
        reifyPat :: forall (m :: * -> *). MonadReify m => DeBruijnPattern -> m Pattern
    reifyPat DeBruijnPattern
    p = do
         MetaNameSuggestion -> Nat -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    MetaNameSuggestion -> Nat -> TCMT IO Doc -> m ()
    reportSDoc MetaNameSuggestion
    "reify.pat" Nat
    80 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
    forall a b. (a -> b) -> a -> b
    $ Doc -> TCMT IO Doc
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Doc -> TCMT IO Doc) -> Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ Doc
    "reifying pattern" Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> DeBruijnPattern -> Doc
    forall a. Pretty a => a -> Doc
    pretty DeBruijnPattern
    p
         keepVars <- PragmaOptions -> Bool
    optKeepPatternVariables (PragmaOptions -> Bool) -> m PragmaOptions -> m Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m PragmaOptions
    forall (m :: * -> *). HasOptions m => m PragmaOptions
    pragmaOptions
         case p of
          -- Possibly expanded literal pattern (see #4215)
          DeBruijnPattern
    p | Just (PatternInfo PatOrigin
    PatOLit [Name]
    asB) <- DeBruijnPattern -> Maybe PatternInfo
    forall x. Pattern' x -> Maybe PatternInfo
    patternInfo DeBruijnPattern
    p -> do
            Term -> m Term
    forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
    reduce (DeBruijnPattern -> Term
    I.patternToTerm DeBruijnPattern
    p) m Term -> (Term -> m Pattern) -> m Pattern
    forall a b. m a -> (a -> m b) -> m b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
              I.Lit Literal
    l -> [Name] -> m Pattern -> m Pattern
    forall (m :: * -> *). Functor m => [Name] -> m Pattern -> m Pattern
    addAsBindings [Name]
    asB (m Pattern -> m Pattern) -> m Pattern -> m Pattern
    forall a b. (a -> b) -> a -> b
    $ Pattern -> m Pattern
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Pattern -> m Pattern) -> Pattern -> m Pattern
    forall a b. (a -> b) -> a -> b
    $ PatInfo -> Literal -> Pattern
    forall e. PatInfo -> Literal -> Pattern' e
    A.LitP PatInfo
    forall a. Null a => a
    empty Literal
    l
              Term
    _       -> m Pattern
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          I.VarP PatternInfo
    i DBPatVar
    x -> [Name] -> m Pattern -> m Pattern
    forall (m :: * -> *). Functor m => [Name] -> m Pattern -> m Pattern
    addAsBindings (PatternInfo -> [Name]
    patAsNames PatternInfo
    i) (m Pattern -> m Pattern) -> m Pattern -> m Pattern
    forall a b. (a -> b) -> a -> b
    $ case PatternInfo -> PatOrigin
    patOrigin PatternInfo
    i of
            o :: PatOrigin
    o@PatOrigin
    PatODot  -> PatOrigin -> Term -> m Pattern
    forall (m :: * -> *).
    MonadReify m =>
    PatOrigin -> Term -> m Pattern
    reifyDotP PatOrigin
    o (Term -> m Pattern) -> Term -> m Pattern
    forall a b. (a -> b) -> a -> b
    $ Nat -> Term
    var (Nat -> Term) -> Nat -> Term
    forall a b. (a -> b) -> a -> b
    $ DBPatVar -> Nat
    dbPatVarIndex DBPatVar
    x
            PatOrigin
    PatOWild   -> Pattern -> m Pattern
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Pattern -> m Pattern) -> Pattern -> m Pattern
    forall a b. (a -> b) -> a -> b
    $ PatInfo -> Pattern
    forall e. PatInfo -> Pattern' e
    A.WildP PatInfo
    patNoRange
            PatOrigin
    PatOAbsurd -> Pattern -> m Pattern
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Pattern -> m Pattern) -> Pattern -> m Pattern
    forall a b. (a -> b) -> a -> b
    $ PatInfo -> Pattern
    forall e. PatInfo -> Pattern' e
    A.AbsurdP PatInfo
    patNoRange
            PatOrigin
    _          -> DBPatVar -> m Pattern
    forall (m :: * -> *). MonadReify m => DBPatVar -> m Pattern
    reifyVarP DBPatVar
    x
          I.DotP PatternInfo
    i Term
    v -> [Name] -> m Pattern -> m Pattern
    forall (m :: * -> *). Functor m => [Name] -> m Pattern -> m Pattern
    addAsBindings (PatternInfo -> [Name]
    patAsNames PatternInfo
    i) (m Pattern -> m Pattern) -> m Pattern -> m Pattern
    forall a b. (a -> b) -> a -> b
    $ case PatternInfo -> PatOrigin
    patOrigin PatternInfo
    i of
            PatOrigin
    PatOWild   -> Pattern -> m Pattern
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Pattern -> m Pattern) -> Pattern -> m Pattern
    forall a b. (a -> b) -> a -> b
    $ PatInfo -> Pattern
    forall e. PatInfo -> Pattern' e
    A.WildP PatInfo
    patNoRange
            PatOrigin
    PatOAbsurd -> Pattern -> m Pattern
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Pattern -> m Pattern) -> Pattern -> m Pattern
    forall a b. (a -> b) -> a -> b
    $ PatInfo -> Pattern
    forall e. PatInfo -> Pattern' e
    A.AbsurdP PatInfo
    patNoRange
            -- If Agda turned a user variable @x@ into @.x@, print it back as @x@.
            o :: PatOrigin
    o@(PatOVar Name
    x) | I.Var Nat
    i [] <- Term
    v -> do
              x' <- Nat -> m Name
    forall (m :: * -> *). (MonadDebug m, MonadTCEnv m) => Nat -> m Name
    nameOfBV Nat
    i
              if nameConcrete x == nameConcrete x' then
                return $ A.VarP $ mkBindName x'
              else
                reifyDotP o v
            PatOrigin
    o -> PatOrigin -> Term -> m Pattern
    forall (m :: * -> *).
    MonadReify m =>
    PatOrigin -> Term -> m Pattern
    reifyDotP PatOrigin
    o Term
    v
          I.LitP PatternInfo
    i Literal
    l  -> [Name] -> m Pattern -> m Pattern
    forall (m :: * -> *). Functor m => [Name] -> m Pattern -> m Pattern
    addAsBindings (PatternInfo -> [Name]
    patAsNames PatternInfo
    i) (m Pattern -> m Pattern) -> m Pattern -> m Pattern
    forall a b. (a -> b) -> a -> b
    $ Pattern -> m Pattern
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Pattern -> m Pattern) -> Pattern -> m Pattern
    forall a b. (a -> b) -> a -> b
    $ PatInfo -> Literal -> Pattern
    forall e. PatInfo -> Literal -> Pattern' e
    A.LitP PatInfo
    forall a. Null a => a
    empty Literal
    l
          I.ProjP ProjOrigin
    o QName
    d -> Pattern -> m Pattern
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Pattern -> m Pattern) -> Pattern -> m Pattern
    forall a b. (a -> b) -> a -> b
    $ PatInfo -> ProjOrigin -> AmbiguousQName -> Pattern
    forall e. PatInfo -> ProjOrigin -> AmbiguousQName -> Pattern' e
    A.ProjP PatInfo
    patNoRange ProjOrigin
    o (AmbiguousQName -> Pattern) -> AmbiguousQName -> Pattern
    forall a b. (a -> b) -> a -> b
    $ QName -> AmbiguousQName
    unambiguous QName
    d
          I.ConP ConHead
    c ConPatternInfo
    cpi [NamedArg DeBruijnPattern]
    ps | ConPatternInfo -> Bool
    conPRecord ConPatternInfo
    cpi -> [Name] -> m Pattern -> m Pattern
    forall (m :: * -> *). Functor m => [Name] -> m Pattern -> m Pattern
    addAsBindings (PatternInfo -> [Name]
    patAsNames (PatternInfo -> [Name]) -> PatternInfo -> [Name]
    forall a b. (a -> b) -> a -> b
    $ ConPatternInfo -> PatternInfo
    conPInfo ConPatternInfo
    cpi) (m Pattern -> m Pattern) -> m Pattern -> m Pattern
    forall a b. (a -> b) -> a -> b
    $
            case PatternInfo -> PatOrigin
    patOrigin (ConPatternInfo -> PatternInfo
    conPInfo ConPatternInfo
    cpi) of
              PatOrigin
    PatOWild   -> Pattern -> m Pattern
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Pattern -> m Pattern) -> Pattern -> m Pattern
    forall a b. (a -> b) -> a -> b
    $ PatInfo -> Pattern
    forall e. PatInfo -> Pattern' e
    A.WildP PatInfo
    patNoRange
              PatOrigin
    PatOAbsurd -> Pattern -> m Pattern
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Pattern -> m Pattern) -> Pattern -> m Pattern
    forall a b. (a -> b) -> a -> b
    $ PatInfo -> Pattern
    forall e. PatInfo -> Pattern' e
    A.AbsurdP PatInfo
    patNoRange
              PatOVar Name
    x | Bool
    keepVars -> Pattern -> m Pattern
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Pattern -> m Pattern) -> Pattern -> m Pattern
    forall a b. (a -> b) -> a -> b
    $ BindName -> Pattern
    forall e. BindName -> Pattern' e
    A.VarP (BindName -> Pattern) -> BindName -> Pattern
    forall a b. (a -> b) -> a -> b
    $ Name -> BindName
    mkBindName Name
    x
              PatOrigin
    _               -> ConHead
    -> ConPatternInfo -> [NamedArg DeBruijnPattern] -> m Pattern
    forall (m :: * -> *).
    MonadReify m =>
    ConHead
    -> ConPatternInfo -> [NamedArg DeBruijnPattern] -> m Pattern
    reifyConP ConHead
    c ConPatternInfo
    cpi [NamedArg DeBruijnPattern]
    ps
          I.ConP ConHead
    c ConPatternInfo
    cpi [NamedArg DeBruijnPattern]
    ps -> [Name] -> m Pattern -> m Pattern
    forall (m :: * -> *). Functor m => [Name] -> m Pattern -> m Pattern
    addAsBindings (PatternInfo -> [Name]
    patAsNames (PatternInfo -> [Name]) -> PatternInfo -> [Name]
    forall a b. (a -> b) -> a -> b
    $ ConPatternInfo -> PatternInfo
    conPInfo ConPatternInfo
    cpi) (m Pattern -> m Pattern) -> m Pattern -> m Pattern
    forall a b. (a -> b) -> a -> b
    $ ConHead
    -> ConPatternInfo -> [NamedArg DeBruijnPattern] -> m Pattern
    forall (m :: * -> *).
    MonadReify m =>
    ConHead
    -> ConPatternInfo -> [NamedArg DeBruijnPattern] -> m Pattern
    reifyConP ConHead
    c ConPatternInfo
    cpi [NamedArg DeBruijnPattern]
    ps
          I.DefP PatternInfo
    i QName
    f [NamedArg DeBruijnPattern]
    ps  -> [Name] -> m Pattern -> m Pattern
    forall (m :: * -> *). Functor m => [Name] -> m Pattern -> m Pattern
    addAsBindings (PatternInfo -> [Name]
    patAsNames PatternInfo
    i) (m Pattern -> m Pattern) -> m Pattern -> m Pattern
    forall a b. (a -> b) -> a -> b
    $ case PatternInfo -> PatOrigin
    patOrigin PatternInfo
    i of
            PatOrigin
    PatOWild   -> Pattern -> m Pattern
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Pattern -> m Pattern) -> Pattern -> m Pattern
    forall a b. (a -> b) -> a -> b
    $ PatInfo -> Pattern
    forall e. PatInfo -> Pattern' e
    A.WildP PatInfo
    patNoRange
            PatOrigin
    PatOAbsurd -> Pattern -> m Pattern
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Pattern -> m Pattern) -> Pattern -> m Pattern
    forall a b. (a -> b) -> a -> b
    $ PatInfo -> Pattern
    forall e. PatInfo -> Pattern' e
    A.AbsurdP PatInfo
    patNoRange
            PatOVar Name
    x | Bool
    keepVars -> Pattern -> m Pattern
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Pattern -> m Pattern) -> Pattern -> m Pattern
    forall a b. (a -> b) -> a -> b
    $ BindName -> Pattern
    forall e. BindName -> Pattern' e
    A.VarP (BindName -> Pattern) -> BindName -> Pattern
    forall a b. (a -> b) -> a -> b
    $ Name -> BindName
    mkBindName Name
    x
            PatOrigin
    _ -> PatInfo -> AmbiguousQName -> Patterns -> Pattern
    forall e. PatInfo -> AmbiguousQName -> NAPs e -> Pattern' e
    A.DefP PatInfo
    patNoRange (QName -> AmbiguousQName
    unambiguous QName
    f) (Patterns -> Pattern) -> m Patterns -> m Pattern
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [NamedArg DeBruijnPattern] -> m Patterns
    forall (m :: * -> *).
    MonadReify m =>
    [NamedArg DeBruijnPattern] -> m Patterns
    reifyPatterns [NamedArg DeBruijnPattern]
    ps
          I.IApplyP PatternInfo
    i Term
    _ Term
    _ DBPatVar
    x -> [Name] -> m Pattern -> m Pattern
    forall (m :: * -> *). Functor m => [Name] -> m Pattern -> m Pattern
    addAsBindings (PatternInfo -> [Name]
    patAsNames PatternInfo
    i) (m Pattern -> m Pattern) -> m Pattern -> m Pattern
    forall a b. (a -> b) -> a -> b
    $ case PatternInfo -> PatOrigin
    patOrigin PatternInfo
    i of
            o :: PatOrigin
    o@PatOrigin
    PatODot  -> PatOrigin -> Term -> m Pattern
    forall (m :: * -> *).
    MonadReify m =>
    PatOrigin -> Term -> m Pattern
    reifyDotP PatOrigin
    o (Term -> m Pattern) -> Term -> m Pattern
    forall a b. (a -> b) -> a -> b
    $ Nat -> Term
    var (Nat -> Term) -> Nat -> Term
    forall a b. (a -> b) -> a -> b
    $ DBPatVar -> Nat
    dbPatVarIndex DBPatVar
    x
            PatOrigin
    PatOWild   -> Pattern -> m Pattern
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Pattern -> m Pattern) -> Pattern -> m Pattern
    forall a b. (a -> b) -> a -> b
    $ PatInfo -> Pattern
    forall e. PatInfo -> Pattern' e
    A.WildP PatInfo
    patNoRange
            PatOrigin
    PatOAbsurd -> Pattern -> m Pattern
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Pattern -> m Pattern) -> Pattern -> m Pattern
    forall a b. (a -> b) -> a -> b
    $ PatInfo -> Pattern
    forall e. PatInfo -> Pattern' e
    A.AbsurdP PatInfo
    patNoRange
            PatOrigin
    _          -> DBPatVar -> m Pattern
    forall (m :: * -> *). MonadReify m => DBPatVar -> m Pattern
    reifyVarP DBPatVar
    x

        reifyVarP :: MonadReify m => DBPatVar -> m A.Pattern
        reifyVarP :: forall (m :: * -> *). MonadReify m => DBPatVar -> m Pattern
    reifyVarP DBPatVar
    x = do
          n <- Nat -> m Name
    forall (m :: * -> *). (MonadDebug m, MonadTCEnv m) => Nat -> m Name
    nameOfBV (Nat -> m Name) -> Nat -> m Name
    forall a b. (a -> b) -> a -> b
    $ DBPatVar -> Nat
    dbPatVarIndex DBPatVar
    x
          let y = DBPatVar -> MetaNameSuggestion
    dbPatVarName DBPatVar
    x
          if | y == "_" -> return $ A.VarP $ mkBindName n
               -- Andreas, 2017-09-03: TODO for #2580
               -- Patterns @VarP "()"@ should have been replaced by @AbsurdP@, but the
               -- case splitter still produces them.
             | prettyShow (nameConcrete n) == "()" -> return $ A.VarP (mkBindName n)
               -- Andreas, 2017-09-03, issue #2729
               -- Restore original pattern name.  AbstractToConcrete picks unique names.
             | otherwise -> return $ A.VarP $
                 mkBindName n { nameConcrete = C.simpleName y }

        reifyDotP :: MonadReify m => PatOrigin -> Term -> m A.Pattern
        reifyDotP :: forall (m :: * -> *).
    MonadReify m =>
    PatOrigin -> Term -> m Pattern
    reifyDotP PatOrigin
    o Term
    v = do
          keepVars <- PragmaOptions -> Bool
    optKeepPatternVariables (PragmaOptions -> Bool) -> m PragmaOptions -> m Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m PragmaOptions
    forall (m :: * -> *). HasOptions m => m PragmaOptions
    pragmaOptions
          if | PatOVar x <- o , keepVars       -> return $ A.VarP $ mkBindName x
             | PatOSplitArg x <- o , keepVars  -> A.VarP . mkBindName <$> freshName noRange x
             | otherwise                       -> A.DotP patNoRange <$> reify v

        reifyConP :: MonadReify m
                  => ConHead -> ConPatternInfo -> [NamedArg DeBruijnPattern]
                  -> m A.Pattern
        reifyConP :: forall (m :: * -> *).
    MonadReify m =>
    ConHead
    -> ConPatternInfo -> [NamedArg DeBruijnPattern] -> m Pattern
    reifyConP ConHead
    c ConPatternInfo
    cpi [NamedArg DeBruijnPattern]
    ps = do
          Pattern -> m Pattern
    forall (m :: * -> *). MonadReify m => Pattern -> m Pattern
    tryRecPFromConP (Pattern -> m Pattern) -> m Pattern -> m Pattern
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< do ConPatInfo -> AmbiguousQName -> Patterns -> Pattern
    forall e. ConPatInfo -> AmbiguousQName -> NAPs e -> Pattern' e
    A.ConP ConPatInfo
    ci (QName -> AmbiguousQName
    unambiguous (ConHead -> QName
    conName ConHead
    c)) (Patterns -> Pattern) -> m Patterns -> m Pattern
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [NamedArg DeBruijnPattern] -> m Patterns
    forall (m :: * -> *).
    MonadReify m =>
    [NamedArg DeBruijnPattern] -> m Patterns
    reifyPatterns [NamedArg DeBruijnPattern]
    ps
          where
            ci :: ConPatInfo
    ci = ConInfo -> PatInfo -> ConPatLazy -> ConPatInfo
    ConPatInfo ConInfo
    origin PatInfo
    patNoRange ConPatLazy
    lazy
            lazy :: ConPatLazy
    lazy | ConPatternInfo -> Bool
    conPLazy ConPatternInfo
    cpi = ConPatLazy
    ConPatLazy
                 | Bool
    otherwise    = ConPatLazy
    ConPatEager
            origin :: ConInfo
    origin = ConPatternInfo -> ConInfo
    fromConPatternInfo ConPatternInfo
    cpi

        addAsBindings :: Functor m => [A.Name] -> m A.Pattern -> m A.Pattern
        addAsBindings :: forall (m :: * -> *). Functor m => [Name] -> m Pattern -> m Pattern
    addAsBindings [Name]
    xs m Pattern
    p = (Name -> m Pattern -> m Pattern)
    -> m Pattern -> [Name] -> m Pattern
    forall a b. (a -> b -> b) -> b -> [a] -> b
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr ((Pattern -> Pattern) -> m Pattern -> m Pattern
    forall a b. (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((Pattern -> Pattern) -> m Pattern -> m Pattern)
    -> (Name -> Pattern -> Pattern) -> Name -> m Pattern -> m Pattern
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PatInfo -> BindName -> Pattern -> Pattern
    forall e. PatInfo -> BindName -> Pattern' e -> Pattern' e
    AsP PatInfo
    patNoRange (BindName -> Pattern -> Pattern)
    -> (Name -> BindName) -> Name -> Pattern -> Pattern
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Name -> BindName
    mkBindName) m Pattern
    p [Name]
    xs

    {-# SPECIALIZE tryRecPFromConP :: A.Pattern -> TCM A.Pattern #-}
    -- | If the record constructor is generated or the user wrote a record pattern,
    --   turn constructor pattern into record pattern.
    --   Otherwise, keep constructor pattern.
    tryRecPFromConP :: MonadReify m => A.Pattern -> m A.Pattern
    tryRecPFromConP :: forall (m :: * -> *). MonadReify m => Pattern -> m Pattern
    tryRecPFromConP Pattern
    p = do
      let fallback :: m Pattern
    fallback = Pattern -> m Pattern
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Pattern
    p
      case Pattern
    p of
        A.ConP ConPatInfo
    ci AmbiguousQName
    c Patterns
    ps -> do
            MetaNameSuggestion -> Nat -> MetaNameSuggestion -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    MetaNameSuggestion -> Nat -> MetaNameSuggestion -> m ()
    reportSLn MetaNameSuggestion
    "reify.pat" Nat
    60 (MetaNameSuggestion -> m ()) -> MetaNameSuggestion -> m ()
    forall a b. (a -> b) -> a -> b
    $ MetaNameSuggestion
    "tryRecPFromConP " MetaNameSuggestion -> MetaNameSuggestion -> MetaNameSuggestion
    forall a. [a] -> [a] -> [a]
    ++ AmbiguousQName -> MetaNameSuggestion
    forall a. Pretty a => a -> MetaNameSuggestion
    prettyShow AmbiguousQName
    c
            m (Maybe (QName, RecordData))
    -> m Pattern -> ((QName, RecordData) -> m Pattern) -> m Pattern
    forall (m :: * -> *) a b.
    Monad m =>
    m (Maybe a) -> m b -> (a -> m b) -> m b
    caseMaybeM (QName -> m (Maybe (QName, RecordData))
    forall (m :: * -> *).
    HasConstInfo m =>
    QName -> m (Maybe (QName, RecordData))
    isRecordConstructor (QName -> m (Maybe (QName, RecordData)))
    -> QName -> m (Maybe (QName, RecordData))
    forall a b. (a -> b) -> a -> b
    $ AmbiguousQName -> QName
    headAmbQ AmbiguousQName
    c) m Pattern
    fallback (((QName, RecordData) -> m Pattern) -> m Pattern)
    -> ((QName, RecordData) -> m Pattern) -> m Pattern
    forall a b. (a -> b) -> a -> b
    $ \ (QName
    r, RecordData
    def) -> do
              -- If the record constructor is generated or the user wrote a record pattern,
              -- print record pattern.
              -- Otherwise, print constructor pattern.
              if RecordData -> Bool
    _recNamedCon RecordData
    def Bool -> Bool -> Bool
    && ConPatInfo -> ConInfo
    conPatOrigin ConPatInfo
    ci ConInfo -> ConInfo -> Bool
    forall a. Eq a => a -> a -> Bool
    /= ConInfo
    ConORec then m Pattern
    fallback else do
                let fs :: [Dom' Term Name]
    fs = RecordData -> [Dom' Term Name]
    recordFieldNames RecordData
    def
                Bool -> m () -> m ()
    forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
    unless ([Dom' Term Name] -> Nat
    forall a. [a] -> Nat
    forall (t :: * -> *) a. Foldable t => t a -> Nat
    length [Dom' Term Name]
    fs Nat -> Nat -> Bool
    forall a. Eq a => a -> a -> Bool
    == Patterns -> Nat
    forall a. [a] -> Nat
    forall (t :: * -> *) a. Foldable t => t a -> Nat
    length Patterns
    ps) m ()
    forall a. HasCallStack => a
    __IMPOSSIBLE__
                Pattern -> m Pattern
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Pattern -> m Pattern) -> Pattern -> m Pattern
    forall a b. (a -> b) -> a -> b
    $ KwRange -> ConPatInfo -> [FieldAssignment' Pattern] -> Pattern
    forall e.
    KwRange
    -> ConPatInfo -> [FieldAssignment' (Pattern' e)] -> Pattern' e
    A.RecP KwRange
    forall a. Null a => a
    empty ConPatInfo
    ci ([FieldAssignment' Pattern] -> Pattern)
    -> [FieldAssignment' Pattern] -> Pattern
    forall a b. (a -> b) -> a -> b
    $ (Dom' Term Name
     -> Arg (Named_ Pattern) -> FieldAssignment' Pattern)
    -> [Dom' Term Name] -> Patterns -> [FieldAssignment' Pattern]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith Dom' Term Name -> Arg (Named_ Pattern) -> FieldAssignment' Pattern
    forall {t} {a}. Dom' t Name -> NamedArg a -> FieldAssignment' a
    mkFA [Dom' Term Name]
    fs Patterns
    ps
            where
              mkFA :: Dom' t Name -> NamedArg a -> FieldAssignment' a
    mkFA Dom' t Name
    ax NamedArg a
    nap = Name -> a -> FieldAssignment' a
    forall a. Name -> a -> FieldAssignment' a
    FieldAssignment (Dom' t Name -> Name
    forall t e. Dom' t e -> e
    unDom Dom' t Name
    ax) (NamedArg a -> a
    forall a. NamedArg a -> a
    namedArg NamedArg a
    nap)
        Pattern
    _ -> m Pattern
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    {-# SPECIALIZE recOrCon :: QName -> ConOrigin -> [Arg Expr] -> TCM A.Expr #-}
    -- | If the record constructor is generated or the user wrote a record expression,
    --   turn constructor expression into record expression.
    --   Otherwise, keep constructor expression.
    recOrCon :: MonadReify m => QName -> ConOrigin -> [Arg Expr] -> m A.Expr
    recOrCon :: forall (m :: * -> *).
    MonadReify m =>
    QName -> ConInfo -> [Arg Expr] -> m Expr
    recOrCon QName
    c ConInfo
    co [Arg Expr]
    es = do
      MetaNameSuggestion -> Nat -> MetaNameSuggestion -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    MetaNameSuggestion -> Nat -> MetaNameSuggestion -> m ()
    reportSLn MetaNameSuggestion
    "reify.expr" Nat
    60 (MetaNameSuggestion -> m ()) -> MetaNameSuggestion -> m ()
    forall a b. (a -> b) -> a -> b
    $ MetaNameSuggestion
    "recOrCon " MetaNameSuggestion -> MetaNameSuggestion -> MetaNameSuggestion
    forall a. [a] -> [a] -> [a]
    ++ QName -> MetaNameSuggestion
    forall a. Pretty a => a -> MetaNameSuggestion
    prettyShow QName
    c
      m (Maybe (QName, RecordData))
    -> m Expr -> ((QName, RecordData) -> m Expr) -> m Expr
    forall (m :: * -> *) a b.
    Monad m =>
    m (Maybe a) -> m b -> (a -> m b) -> m b
    caseMaybeM (QName -> m (Maybe (QName, RecordData))
    forall (m :: * -> *).
    HasConstInfo m =>
    QName -> m (Maybe (QName, RecordData))
    isRecordConstructor QName
    c) m Expr
    fallback (((QName, RecordData) -> m Expr) -> m Expr)
    -> ((QName, RecordData) -> m Expr) -> m Expr
    forall a b. (a -> b) -> a -> b
    $ \ (QName
    r, RecordData
    def) -> do
        -- If the record constructor is generated or the user wrote a record expression,
        -- print record expression.
        -- Otherwise, print constructor expression.
        if RecordData -> Bool
    _recNamedCon RecordData
    def Bool -> Bool -> Bool
    && ConInfo
    co ConInfo -> ConInfo -> Bool
    forall a. Eq a => a -> a -> Bool
    /= ConInfo
    ConORec then m Expr
    fallback else do
          let fs :: [Dom' Term Name]
    fs = RecordData -> [Dom' Term Name]
    recordFieldNames RecordData
    def
          Bool -> m () -> m ()
    forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
    unless ([Dom' Term Name] -> Nat
    forall a. [a] -> Nat
    forall (t :: * -> *) a. Foldable t => t a -> Nat
    length [Dom' Term Name]
    fs Nat -> Nat -> Bool
    forall a. Eq a => a -> a -> Bool
    == [Arg Expr] -> Nat
    forall a. [a] -> Nat
    forall (t :: * -> *) a. Foldable t => t a -> Nat
    length [Arg Expr]
    es) m ()
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          Expr -> m Expr
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Expr -> m Expr) -> Expr -> m Expr
    forall a b. (a -> b) -> a -> b
    $ KwRange -> ExprInfo -> RecordAssigns -> Expr
    A.Rec KwRange
    forall a. Null a => a
    empty ExprInfo
    forall a. Null a => a
    empty (RecordAssigns -> Expr) -> RecordAssigns -> Expr
    forall a b. (a -> b) -> a -> b
    $ (Dom' Term Name -> Arg Expr -> RecordAssign)
    -> [Dom' Term Name] -> [Arg Expr] -> RecordAssigns
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith Dom' Term Name -> Arg Expr -> RecordAssign
    forall {t} {b} {b}.
    Dom' t Name -> Arg b -> Either (FieldAssignment' b) b
    mkFA [Dom' Term Name]
    fs [Arg Expr]
    es
      where
      fallback :: m Expr
    fallback = Expr -> [Arg Expr] -> m Expr
    forall (m :: * -> *). MonadReify m => Expr -> [Arg Expr] -> m Expr
    apps (AmbiguousQName -> Expr
    A.Con (QName -> AmbiguousQName
    unambiguous QName
    c)) [Arg Expr]
    es
      mkFA :: Dom' t Name -> Arg b -> Either (FieldAssignment' b) b
    mkFA Dom' t Name
    ax  = FieldAssignment' b -> Either (FieldAssignment' b) b
    forall a b. a -> Either a b
    Left (FieldAssignment' b -> Either (FieldAssignment' b) b)
    -> (Arg b -> FieldAssignment' b)
    -> Arg b
    -> Either (FieldAssignment' b) b
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Name -> b -> FieldAssignment' b
    forall a. Name -> a -> FieldAssignment' a
    FieldAssignment (Dom' t Name -> Name
    forall t e. Dom' t e -> e
    unDom Dom' t Name
    ax) (b -> FieldAssignment' b)
    -> (Arg b -> b) -> Arg b -> FieldAssignment' b
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Arg b -> b
    forall e. Arg e -> e
    unArg

    instance Reify (QNamed I.Clause) where
      type ReifiesTo (QNamed I.Clause) = A.Clause

      reify :: forall (m :: * -> *).
    MonadReify m =>
    QNamed Clause -> m (ReifiesTo (QNamed Clause))
    reify (QNamed QName
    f Clause
    cl) = NamedClause -> m (ReifiesTo NamedClause)
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    forall (m :: * -> *).
    MonadReify m =>
    NamedClause -> m (ReifiesTo NamedClause)
    reify (QName -> Bool -> Clause -> NamedClause
    NamedClause QName
    f Bool
    True Clause
    cl); {-# INLINE reify #-}

    instance Reify NamedClause where
      type ReifiesTo NamedClause = A.Clause

      reify :: forall (m :: * -> *).
    MonadReify m =>
    NamedClause -> m (ReifiesTo NamedClause)
    reify (NamedClause QName
    f Bool
    toDrop Clause
    cl) = Tele (Dom Type)
    -> m (ReifiesTo NamedClause) -> m (ReifiesTo NamedClause)
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Tele (Dom Type) -> m a -> m a
    addContext (Clause -> Tele (Dom Type)
    clauseTel Clause
    cl) (m (ReifiesTo NamedClause) -> m (ReifiesTo NamedClause))
    -> m (ReifiesTo NamedClause) -> m (ReifiesTo NamedClause)
    forall a b. (a -> b) -> a -> b
    $ do
        MetaNameSuggestion -> Nat -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    MetaNameSuggestion -> Nat -> TCMT IO Doc -> m ()
    reportSDoc MetaNameSuggestion
    "reify.clause" Nat
    60 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
    forall a b. (a -> b) -> a -> b
    $ Doc -> TCMT IO Doc
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Doc -> TCMT IO Doc) -> Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    vcat
          [ Doc
    "reifying NamedClause"
          , Doc
    "  f      =" Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> QName -> Doc
    forall a. Pretty a => a -> Doc
    pretty QName
    f
          , Doc
    "  toDrop =" Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> Bool -> Doc
    forall a. Show a => a -> Doc
    pshow Bool
    toDrop
          , Doc
    "  cl     =" Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> Clause -> Doc
    forall a. Pretty a => a -> Doc
    pretty Clause
    cl
          ]

        let clBody :: Maybe Term
    clBody = Clause -> Maybe Term
    clauseBody Clause
    cl
            rhsVars :: [Nat]
    rhsVars = [Nat] -> (Term -> [Nat]) -> Maybe Term -> [Nat]
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe [] Term -> [Nat]
    forall a c t. (IsVarSet a c, Singleton Nat c, Free t) => t -> c
    freeVars Maybe Term
    clBody

        rhsBody     <- (Term -> m Expr) -> Maybe Term -> m (Maybe Expr)
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Maybe a -> f (Maybe b)
    traverse Term -> m Expr
    Term -> m (ReifiesTo Term)
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    forall (m :: * -> *). MonadReify m => Term -> m (ReifiesTo Term)
    reify Maybe Term
    clBody
        rhsVarNames <- mapM nameOfBV' rhsVars
        let rhsUsedNames = Set Name -> (Expr -> Set Name) -> Maybe Expr -> Set Name
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe Set Name
    forall a. Monoid a => a
    mempty Expr -> Set Name
    allUsedNames Maybe Expr
    rhsBody
            rhsUsedVars  = [Nat
    i | (Nat
    i, Just Name
    n) <- [Nat] -> [Maybe Name] -> [(Nat, Maybe Name)]
    forall a b. [a] -> [b] -> [(a, b)]
    zip [Nat]
    rhsVars [Maybe Name]
    rhsVarNames, Name
    n Name -> Set Name -> Bool
    forall a. Ord a => a -> Set a -> Bool
    `Set.member` Set Name
    rhsUsedNames]

        reportSDoc "reify.clause" 60 $ return $ "RHS:" <+> pretty clBody
        reportSDoc "reify.clause" 60 $ return $ "variables occurring on RHS:" <+> pretty rhsVars
          <+> "variable names:" <+> pretty rhsVarNames
          <+> parens (maybe "no clause body" (const "there was a clause body") clBody)
        reportSDoc "reify.clause" 60 $ return $ "names occurring on RHS" <+> pretty (Set.toList rhsUsedNames)

        let ell = Clause -> ExpandedEllipsis
    clauseEllipsis Clause
    cl
        ps  <- reifyPatterns $ namedClausePats cl
        lhs <- uncurry (SpineLHS $ empty { lhsEllipsis = ell }) <$> reifyDisplayFormP f ps []
        -- Unless @toDrop@ we have already dropped the module patterns from the clauses
        -- (e.g. for extended lambdas). We still get here with toDrop = True and
        -- pattern lambdas when doing make-case, so take care to drop the right
        -- number of parameters.
        (params , lhs) <- if not toDrop then return ([] , lhs) else do
          nfv <- getDefModule f >>= \case
            Left SigError
    _  -> Nat -> m Nat
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Nat
    0
            Right ModuleName
    m -> Tele (Dom Type) -> Nat
    forall a. Sized a => a -> Nat
    size (Tele (Dom Type) -> Nat) -> m (Tele (Dom Type)) -> m Nat
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ModuleName -> m (Tele (Dom Type))
    forall (m :: * -> *).
    (Functor m, ReadTCState m) =>
    ModuleName -> m (Tele (Dom Type))
    lookupSection ModuleName
    m
          return $ splitParams nfv lhs
        lhs <- stripImps rhsUsedNames params lhs
        let rhs    = Maybe Expr -> RHS -> (Expr -> RHS) -> RHS
    forall a b. Maybe a -> b -> (a -> b) -> b
    caseMaybe Maybe Expr
    rhsBody RHS
    AbsurdRHS ((Expr -> RHS) -> RHS) -> (Expr -> RHS) -> RHS
    forall a b. (a -> b) -> a -> b
    $ \ Expr
    e -> Expr -> Maybe Expr -> RHS
    RHS Expr
    e Maybe Expr
    forall a. Maybe a
    Nothing
            result = LHS
    -> [ProblemEq] -> RHS -> WhereDeclarations -> Catchall -> Clause
    forall lhs.
    lhs
    -> [ProblemEq]
    -> RHS
    -> WhereDeclarations
    -> Catchall
    -> Clause' lhs
    A.Clause (SpineLHS -> LHS
    forall a b. LHSToSpine a b => b -> a
    spineToLhs SpineLHS
    lhs) [] RHS
    rhs WhereDeclarations
    A.noWhereDecls (Clause -> Catchall
    I.clauseCatchall Clause
    cl)
        return result
        where
          splitParams :: Nat -> SpineLHS -> (Patterns, SpineLHS)
    splitParams Nat
    n (SpineLHS LHSInfo
    i QName
    f Patterns
    ps) =
            let (Patterns
    params , Patterns
    pats) = Nat -> Patterns -> (Patterns, Patterns)
    forall a. Nat -> [a] -> ([a], [a])
    splitAt Nat
    n Patterns
    ps
            in  (Patterns
    params , LHSInfo -> QName -> Patterns -> SpineLHS
    SpineLHS LHSInfo
    i QName
    f Patterns
    pats)
          stripImps :: MonadReify m => Set Name -> [NamedArg A.Pattern] -> SpineLHS -> m SpineLHS
          stripImps :: forall (m :: * -> *).
    MonadReify m =>
    Set Name -> Patterns -> SpineLHS -> m SpineLHS
    stripImps Set Name
    rhsUsedNames Patterns
    params (SpineLHS LHSInfo
    i QName
    f Patterns
    ps) =  LHSInfo -> QName -> Patterns -> SpineLHS
    SpineLHS LHSInfo
    i QName
    f (Patterns -> SpineLHS) -> m Patterns -> m SpineLHS
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Set Name -> Patterns -> Patterns -> m Patterns
    forall (m :: * -> *).
    MonadReify m =>
    Set Name -> Patterns -> Patterns -> m Patterns
    stripImplicits Set Name
    rhsUsedNames Patterns
    params Patterns
    ps
    {-# SPECIALIZE reify :: NamedClause -> TCM (ReifiesTo NamedClause) #-}

    instance Reify (QNamed System) where
      type ReifiesTo (QNamed System) = [A.Clause]

      reify :: forall (m :: * -> *).
    MonadReify m =>
    QNamed System -> m (ReifiesTo (QNamed System))
    reify (QNamed QName
    f (System Tele (Dom Type)
    tel [(Face, Term)]
    sys)) = Tele (Dom Type)
    -> m (ReifiesTo (QNamed System)) -> m (ReifiesTo (QNamed System))
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Tele (Dom Type) -> m a -> m a
    addContext Tele (Dom Type)
    tel (m (ReifiesTo (QNamed System)) -> m (ReifiesTo (QNamed System)))
    -> m (ReifiesTo (QNamed System)) -> m (ReifiesTo (QNamed System))
    forall a b. (a -> b) -> a -> b
    $ do
        MetaNameSuggestion -> Nat -> [MetaNameSuggestion] -> m ()
    forall a (m :: * -> *).
    (ReportS a, MonadDebug m) =>
    MetaNameSuggestion -> Nat -> a -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    MetaNameSuggestion -> Nat -> [MetaNameSuggestion] -> m ()
    reportS MetaNameSuggestion
    "reify.system" Nat
    40 ([MetaNameSuggestion] -> m ()) -> [MetaNameSuggestion] -> m ()
    forall a b. (a -> b) -> a -> b
    $ Tele (Dom Type) -> MetaNameSuggestion
    forall a. Show a => a -> MetaNameSuggestion
    show Tele (Dom Type)
    tel MetaNameSuggestion -> [MetaNameSuggestion] -> [MetaNameSuggestion]
    forall a. a -> [a] -> [a]
    : ((Face, Term) -> MetaNameSuggestion)
    -> [(Face, Term)] -> [MetaNameSuggestion]
    forall a b. (a -> b) -> [a] -> [b]
    map (Face, Term) -> MetaNameSuggestion
    forall a. Show a => a -> MetaNameSuggestion
    show [(Face, Term)]
    sys
        view <- m (Term -> IntervalView)
    forall (m :: * -> *). HasBuiltins m => m (Term -> IntervalView)
    intervalView'
        unview <- intervalUnview'
        sys <- flip filterM sys $ \ (Face
    phi,Term
    t) -> do
          Face -> ((Term, Bool) -> m Bool) -> m Bool
    forall (f :: * -> *) (m :: * -> *) a.
    (Foldable f, Monad m) =>
    f a -> (a -> m Bool) -> m Bool
    forallM Face
    phi (((Term, Bool) -> m Bool) -> m Bool)
    -> ((Term, Bool) -> m Bool) -> m Bool
    forall a b. (a -> b) -> a -> b
    $ \ (Term
    u,Bool
    b) -> do
            u <- Term -> m Term
    forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
    reduce Term
    u
            return $ case (view u, b) of
              (IntervalView
    IZero, Bool
    True) -> Bool
    False
              (IntervalView
    IOne, Bool
    False) -> Bool
    False
              (IntervalView, Bool)
    _ -> Bool
    True
        forM sys $ \ (Face
    alpha,Term
    u) -> do
          ps <- [NamedArg DeBruijnPattern] -> m Patterns
    forall (m :: * -> *).
    MonadReify m =>
    [NamedArg DeBruijnPattern] -> m Patterns
    reifyPatterns ([NamedArg DeBruijnPattern] -> m Patterns)
    -> [NamedArg DeBruijnPattern] -> m Patterns
    forall a b. (a -> b) -> a -> b
    $ Tele (Dom Type) -> [NamedArg DeBruijnPattern]
    forall a t. DeBruijn a => Tele (Dom t) -> [NamedArg a]
    teleNamedArgs Tele (Dom Type)
    tel
          ps <- List1.ifNull alpha (pure ps) {-else-} \ List1 (Term, Bool)
    alpha -> do
            ep <- (List1 (Expr, Expr) -> Pattern)
    -> m (List1 (Expr, Expr)) -> m Pattern
    forall a b. (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (PatInfo -> List1 (Expr, Expr) -> Pattern
    forall e. PatInfo -> List1 (e, e) -> Pattern' e
    A.EqualP PatInfo
    patNoRange) (m (List1 (Expr, Expr)) -> m Pattern)
    -> (((Term, Bool) -> m (Expr, Expr)) -> m (List1 (Expr, Expr)))
    -> ((Term, Bool) -> m (Expr, Expr))
    -> m Pattern
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . List1 (Term, Bool)
    -> ((Term, Bool) -> m (Expr, Expr)) -> m (List1 (Expr, Expr))
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    t a -> (a -> m b) -> m (t b)
    forM List1 (Term, Bool)
    alpha (((Term, Bool) -> m (Expr, Expr)) -> m Pattern)
    -> ((Term, Bool) -> m (Expr, Expr)) -> m Pattern
    forall a b. (a -> b) -> a -> b
    $ \ (Term
    phi,Bool
    b) -> do
              let
                  d :: Bool -> Term
    d Bool
    True = IntervalView -> Term
    unview IntervalView
    IOne
                  d Bool
    False = IntervalView -> Term
    unview IntervalView
    IZero
              (Term, Term) -> m (ReifiesTo (Term, Term))
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    forall (m :: * -> *).
    MonadReify m =>
    (Term, Term) -> m (ReifiesTo (Term, Term))
    reify (Term
    phi, Bool -> Term
    d Bool
    b)
            pure $ ps ++ [defaultNamedArg ep]

          lhs <- SpineLHS empty f <$> stripImplicits mempty [] ps
          rhs <- reify u <&> (`RHS` Nothing)
          return $ A.Clause (spineToLhs lhs) [] rhs A.noWhereDecls empty
    {-# SPECIALIZE reify :: QNamed System -> TCM (ReifiesTo (QNamed System)) #-}

    instance Reify I.Type where
        type ReifiesTo I.Type = A.Type

        reifyWhen :: forall (m :: * -> *).
    MonadReify m =>
    Bool -> Type -> m (ReifiesTo Type)
    reifyWhen = Bool -> Type -> m (ReifiesTo Type)
    forall i (m :: * -> *).
    (Reify i, MonadReify m, Underscore (ReifiesTo i)) =>
    Bool -> i -> m (ReifiesTo i)
    reifyWhenE; {-# INLINE reifyWhen #-}
        reify :: forall (m :: * -> *). MonadReify m => Type -> m (ReifiesTo Type)
    reify (I.El Sort
    _ Term
    t) = Term -> m (ReifiesTo Term)
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    forall (m :: * -> *). MonadReify m => Term -> m (ReifiesTo Term)
    reify Term
    t; {-# INLINE reify #-}

    instance Reify Sort where
        type ReifiesTo Sort = Expr

        reifyWhen :: forall (m :: * -> *).
    MonadReify m =>
    Bool -> Sort -> m (ReifiesTo Sort)
    reifyWhen = Bool -> Sort -> m (ReifiesTo Sort)
    forall i (m :: * -> *).
    (Reify i, MonadReify m, Underscore (ReifiesTo i)) =>
    Bool -> i -> m (ReifiesTo i)
    reifyWhenE

        reify :: forall (m :: * -> *). MonadReify m => Sort -> m (ReifiesTo Sort)
    reify Sort
    s = do
          s <- Sort -> m Sort
    forall a (m :: * -> *).
    (InstantiateFull a, MonadReduce m) =>
    a -> m a
    instantiateFull Sort
    s
          SortKit{..} <- infallibleSortKit
          case s of
            I.Univ Univ
    u (I.ClosedLevel Integer
    0) -> Expr -> m Expr
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Expr -> m Expr) -> Expr -> m Expr
    forall a b. (a -> b) -> a -> b
    $ QName -> Suffix -> Expr
    A.Def' (UnivSize -> Univ -> QName
    nameOfUniv UnivSize
    USmall Univ
    u) Suffix
    A.NoSuffix
            I.Univ Univ
    u (I.ClosedLevel Integer
    n) -> Expr -> m Expr
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Expr -> m Expr) -> Expr -> m Expr
    forall a b. (a -> b) -> a -> b
    $ QName -> Suffix -> Expr
    A.Def' (UnivSize -> Univ -> QName
    nameOfUniv UnivSize
    USmall Univ
    u) (Integer -> Suffix
    A.Suffix Integer
    n)
            I.Univ Univ
    u Level
    a -> do
              a <- Level -> m (ReifiesTo Level)
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    forall (m :: * -> *). MonadReify m => Level -> m (ReifiesTo Level)
    reify Level
    a
              return $ A.App defaultAppInfo_ (A.Def $ nameOfUniv USmall u) (defaultNamedArg a)
            I.Inf Univ
    u Integer
    0 -> Expr -> m Expr
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Expr -> m Expr) -> Expr -> m Expr
    forall a b. (a -> b) -> a -> b
    $ QName -> Suffix -> Expr
    A.Def' (UnivSize -> Univ -> QName
    nameOfUniv UnivSize
    ULarge Univ
    u) Suffix
    A.NoSuffix
            I.Inf Univ
    u Integer
    n -> Expr -> m Expr
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Expr -> m Expr) -> Expr -> m Expr
    forall a b. (a -> b) -> a -> b
    $ QName -> Suffix -> Expr
    A.Def' (UnivSize -> Univ -> QName
    nameOfUniv UnivSize
    ULarge Univ
    u) (Integer -> Suffix
    A.Suffix Integer
    n)
            Sort
    I.SizeUniv  -> do
              sizeU <- QName -> Maybe QName -> QName
    forall a. a -> Maybe a -> a
    fromMaybe QName
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe QName -> QName) -> m (Maybe QName) -> m QName
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> BuiltinId -> m (Maybe QName)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe QName)
    getBuiltinName' BuiltinId
    builtinSizeUniv
              return $ A.Def sizeU
            Sort
    I.LockUniv  -> do
              lockU <- QName -> Maybe QName -> QName
    forall a. a -> Maybe a -> a
    fromMaybe QName
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe QName -> QName) -> m (Maybe QName) -> m QName
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> PrimitiveId -> m (Maybe QName)
    forall (m :: * -> *) a.
    (HasBuiltins m, IsBuiltin a) =>
    a -> m (Maybe QName)
    getName' PrimitiveId
    builtinLockUniv
              return $ A.Def lockU
            Sort
    I.LevelUniv -> do
              levelU <- QName -> Maybe QName -> QName
    forall a. a -> Maybe a -> a
    fromMaybe QName
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe QName -> QName) -> m (Maybe QName) -> m QName
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> BuiltinId -> m (Maybe QName)
    forall (m :: * -> *) a.
    (HasBuiltins m, IsBuiltin a) =>
    a -> m (Maybe QName)
    getName' BuiltinId
    builtinLevelUniv
              return $ A.Def levelU
            Sort
    I.IntervalUniv -> do
              intervalU <- QName -> Maybe QName -> QName
    forall a. a -> Maybe a -> a
    fromMaybe QName
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe QName -> QName) -> m (Maybe QName) -> m QName
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> BuiltinId -> m (Maybe QName)
    forall (m :: * -> *) a.
    (HasBuiltins m, IsBuiltin a) =>
    a -> m (Maybe QName)
    getName' BuiltinId
    builtinIntervalUniv
              return $ A.Def intervalU
            I.PiSort Dom' Term Term
    a Sort
    s1 Abs Sort
    s2 -> do
              pis <- MetaNameSuggestion -> m Name
    forall a (m :: * -> *).
    (FreshName a, MonadFresh NameId m) =>
    a -> m Name
    forall (m :: * -> *).
    MonadFresh NameId m =>
    MetaNameSuggestion -> m Name
    freshName_ (MetaNameSuggestion
    "piSort" :: String) -- TODO: hack
              (e1,e2) <- reify (s1, I.Lam defaultArgInfo $ fmap Sort s2)
              let app Expr
    x Expr
    y = AppInfo -> Expr -> Arg (Named_ Expr) -> Expr
    A.App AppInfo
    defaultAppInfo_ Expr
    x (Expr -> Arg (Named_ Expr)
    forall a. a -> NamedArg a
    defaultNamedArg Expr
    y)
              return $ A.Var pis `app` e1 `app` e2
            I.FunSort Sort
    s1 Sort
    s2 -> do
              funs <- MetaNameSuggestion -> m Name
    forall a (m :: * -> *).
    (FreshName a, MonadFresh NameId m) =>
    a -> m Name
    forall (m :: * -> *).
    MonadFresh NameId m =>
    MetaNameSuggestion -> m Name
    freshName_ (MetaNameSuggestion
    "funSort" :: String) -- TODO: hack
              (e1,e2) <- reify (s1 , s2)
              let app Expr
    x Expr
    y = AppInfo -> Expr -> Arg (Named_ Expr) -> Expr
    A.App AppInfo
    defaultAppInfo_ Expr
    x (Expr -> Arg (Named_ Expr)
    forall a. a -> NamedArg a
    defaultNamedArg Expr
    y)
              return $ A.Var funs `app` e1 `app` e2
            I.UnivSort Sort
    s -> do
              univs <- MetaNameSuggestion -> m Name
    forall a (m :: * -> *).
    (FreshName a, MonadFresh NameId m) =>
    a -> m Name
    forall (m :: * -> *).
    MonadFresh NameId m =>
    MetaNameSuggestion -> m Name
    freshName_ (MetaNameSuggestion
    "univSort" :: String) -- TODO: hack
              e <- reify s
              return $ A.App defaultAppInfo_ (A.Var univs) $ defaultNamedArg e
            I.MetaS MetaId
    x Elims
    es -> Term -> m (ReifiesTo Term)
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    forall (m :: * -> *). MonadReify m => Term -> m (ReifiesTo Term)
    reify (Term -> m (ReifiesTo Term)) -> Term -> m (ReifiesTo Term)
    forall a b. (a -> b) -> a -> b
    $ MetaId -> Elims -> Term
    I.MetaV MetaId
    x Elims
    es
            I.DefS QName
    d Elims
    es -> Term -> m (ReifiesTo Term)
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    forall (m :: * -> *). MonadReify m => Term -> m (ReifiesTo Term)
    reify (Term -> m (ReifiesTo Term)) -> Term -> m (ReifiesTo Term)
    forall a b. (a -> b) -> a -> b
    $ QName -> Elims -> Term
    I.Def QName
    d Elims
    es
            I.DummyS MetaNameSuggestion
    s -> Expr -> m Expr
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Expr -> m Expr) -> Expr -> m Expr
    forall a b. (a -> b) -> a -> b
    $ ExprInfo -> Literal -> Expr
    A.Lit ExprInfo
    forall a. Null a => a
    empty (Literal -> Expr) -> Literal -> Expr
    forall a b. (a -> b) -> a -> b
    $ Text -> Literal
    LitString (Text -> Literal) -> Text -> Literal
    forall a b. (a -> b) -> a -> b
    $ MetaNameSuggestion -> Text
    T.pack MetaNameSuggestion
    s
    {-# SPECIALIZE reify :: Sort -> TCM (ReifiesTo Sort) #-}

    instance Reify Level where
      type ReifiesTo Level = Expr

      reifyWhen :: forall (m :: * -> *).
    MonadReify m =>
    Bool -> Level -> m (ReifiesTo Level)
    reifyWhen = Bool -> Level -> m (ReifiesTo Level)
    forall i (m :: * -> *).
    (Reify i, MonadReify m, Underscore (ReifiesTo i)) =>
    Bool -> i -> m (ReifiesTo i)
    reifyWhenE
      reify :: forall (m :: * -> *). MonadReify m => Level -> m (ReifiesTo Level)
    reify Level
    l   = m Bool
    -> m (ReifiesTo Level)
    -> m (ReifiesTo Level)
    -> m (ReifiesTo Level)
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
    ifM m Bool
    forall (m :: * -> *). HasBuiltins m => m Bool
    haveLevels (Term -> m Expr
    Term -> m (ReifiesTo Term)
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    forall (m :: * -> *). MonadReify m => Term -> m (ReifiesTo Term)
    reify (Term -> m Expr) -> m Term -> m Expr
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Level -> m Term
    forall (m :: * -> *). HasBuiltins m => Level -> m Term
    reallyUnLevelView Level
    l) (m (ReifiesTo Level) -> m (ReifiesTo Level))
    -> m (ReifiesTo Level) -> m (ReifiesTo Level)
    forall a b. (a -> b) -> a -> b
    $ {-else-} do
        -- Andreas, 2017-09-18, issue #2754
        -- While type checking the level builtins, they are not
        -- available for debug printing.  Thus, print some garbage instead.
        name <- MetaNameSuggestion -> m Name
    forall a (m :: * -> *).
    (FreshName a, MonadFresh NameId m) =>
    a -> m Name
    forall (m :: * -> *).
    MonadFresh NameId m =>
    MetaNameSuggestion -> m Name
    freshName_ (MetaNameSuggestion
    ".#Lacking_Level_Builtins#" :: String)
        return $ A.Var name
    {-# SPECIALIZE reify :: Level -> TCM (ReifiesTo Level) #-}

    instance (Free i, Reify i) => Reify (Abs i) where
      type ReifiesTo (Abs i) = (Name, ReifiesTo i)

      reify :: forall (m :: * -> *).
    MonadReify m =>
    Abs i -> m (ReifiesTo (Abs i))
    reify (NoAbs MetaNameSuggestion
    x i
    v) = MetaNameSuggestion -> m Name
    forall a (m :: * -> *).
    (FreshName a, MonadFresh NameId m) =>
    a -> m Name
    forall (m :: * -> *).
    MonadFresh NameId m =>
    MetaNameSuggestion -> m Name
    freshName_ MetaNameSuggestion
    x m Name -> (Name -> m (Name, ReifiesTo i)) -> m (Name, ReifiesTo i)
    forall a b. m a -> (a -> m b) -> m b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \Name
    name -> (Name
    name,) (ReifiesTo i -> (Name, ReifiesTo i))
    -> m (ReifiesTo i) -> m (Name, ReifiesTo i)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> i -> m (ReifiesTo i)
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    forall (m :: * -> *). MonadReify m => i -> m (ReifiesTo i)
    reify i
    v
      reify (Abs MetaNameSuggestion
    s i
    v) = do

        -- If the bound variable is free in the body, then the name "_" is
        -- replaced by "z".
        s <- MetaNameSuggestion -> m MetaNameSuggestion
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (MetaNameSuggestion -> m MetaNameSuggestion)
    -> MetaNameSuggestion -> m MetaNameSuggestion
    forall a b. (a -> b) -> a -> b
    $ if MetaNameSuggestion -> Bool
    forall a. Underscore a => a -> Bool
    isUnderscore MetaNameSuggestion
    s Bool -> Bool -> Bool
    && Nat
    0 Nat -> i -> Bool
    forall a. Free a => Nat -> a -> Bool
    `freeIn` i
    v then MetaNameSuggestion
    "z" else MetaNameSuggestion
    s

        x <- C.setNotInScope <$> freshName_ s
        e <- addContext x -- type doesn't matter
             $ reify v
        return (x,e)
    {-# SPECIALIZE reify :: (Free i, Reify i) -> Abs i -> TCM (ReifiesTo (Abs i)) #-}

    instance Reify I.Telescope where
      type ReifiesTo I.Telescope = A.Telescope

      reify :: forall (m :: * -> *).
    MonadReify m =>
    Tele (Dom Type) -> m (ReifiesTo (Tele (Dom Type)))
    reify Tele (Dom Type)
    EmptyTel = [TypedBinding] -> m [TypedBinding]
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return []
      reify (ExtendTel Dom Type
    arg Abs (Tele (Dom Type))
    tel) = do
        Arg info e <- Dom Type -> m (ReifiesTo (Dom Type))
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    forall (m :: * -> *).
    MonadReify m =>
    Dom Type -> m (ReifiesTo (Dom Type))
    reify Dom Type
    arg
        (x, bs)  <- reify tel
        let r    = Expr -> Range
    forall a. HasRange a => a -> Range
    getRange Expr
    e
            name = Dom Type -> Maybe (WithOrigin (Ranged MetaNameSuggestion))
    forall t e.
    Dom' t e -> Maybe (WithOrigin (Ranged MetaNameSuggestion))
    domName Dom Type
    arg
        tac <- TacticAttribute <$> do traverse (Ranged noRange <.> reify) $ domTactic arg
        let xs = Arg (Named (WithOrigin (Ranged MetaNameSuggestion)) Binder)
    -> List1
         (Arg (Named (WithOrigin (Ranged MetaNameSuggestion)) Binder))
    forall el coll. Singleton el coll => el -> coll
    singleton (Arg (Named (WithOrigin (Ranged MetaNameSuggestion)) Binder)
     -> List1
          (Arg (Named (WithOrigin (Ranged MetaNameSuggestion)) Binder)))
    -> Arg (Named (WithOrigin (Ranged MetaNameSuggestion)) Binder)
    -> List1
         (Arg (Named (WithOrigin (Ranged MetaNameSuggestion)) Binder))
    forall a b. (a -> b) -> a -> b
    $ ArgInfo
    -> Named (WithOrigin (Ranged MetaNameSuggestion)) Binder
    -> Arg (Named (WithOrigin (Ranged MetaNameSuggestion)) Binder)
    forall e. ArgInfo -> e -> Arg e
    Arg ArgInfo
    info (Named (WithOrigin (Ranged MetaNameSuggestion)) Binder
     -> Arg (Named (WithOrigin (Ranged MetaNameSuggestion)) Binder))
    -> Named (WithOrigin (Ranged MetaNameSuggestion)) Binder
    -> Arg (Named (WithOrigin (Ranged MetaNameSuggestion)) Binder)
    forall a b. (a -> b) -> a -> b
    $ Maybe (WithOrigin (Ranged MetaNameSuggestion))
    -> Binder -> Named (WithOrigin (Ranged MetaNameSuggestion)) Binder
    forall name a. Maybe name -> a -> Named name a
    Named Maybe (WithOrigin (Ranged MetaNameSuggestion))
    name (Binder -> Named (WithOrigin (Ranged MetaNameSuggestion)) Binder)
    -> Binder -> Named (WithOrigin (Ranged MetaNameSuggestion)) Binder
    forall a b. (a -> b) -> a -> b
    $ Name -> Binder
    A.mkBinder_ Name
    x
        return $ TBind r (TypedBindingInfo tac (domIsFinite arg)) xs e : bs
    {-# SPECIALIZE reify :: I.Telescope -> TCM (ReifiesTo I.Telescope) #-}

    instance Reify i => Reify (Dom i) where
        type ReifiesTo (Dom i) = Arg (ReifiesTo i)

        reify :: forall (m :: * -> *).
    MonadReify m =>
    Dom i -> m (ReifiesTo (Dom i))
    reify (Dom{domInfo :: forall t e. Dom' t e -> ArgInfo
    domInfo = ArgInfo
    info, unDom :: forall t e. Dom' t e -> e
    unDom = i
    i}) = ArgInfo -> ReifiesTo i -> Arg (ReifiesTo i)
    forall e. ArgInfo -> e -> Arg e
    Arg ArgInfo
    info (ReifiesTo i -> Arg (ReifiesTo i))
    -> m (ReifiesTo i) -> m (Arg (ReifiesTo i))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> i -> m (ReifiesTo i)
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    forall (m :: * -> *). MonadReify m => i -> m (ReifiesTo i)
    reify i
    i
        {-# INLINE reify #-}

    instance Reify ContextEntry where
      type ReifiesTo ContextEntry = A.TypedBinding

      reify :: forall (m :: * -> *).
    MonadReify m =>
    ContextEntry -> m (ReifiesTo ContextEntry)
    reify (CtxVar Name
    x Dom Type
    a) = do
        Arg info (y,t) <- Dom' Term (Name, Type) -> m (ReifiesTo (Dom' Term (Name, Type)))
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    forall (m :: * -> *).
    MonadReify m =>
    Dom' Term (Name, Type) -> m (ReifiesTo (Dom' Term (Name, Type)))
    reify (Dom' Term (Name, Type) -> m (ReifiesTo (Dom' Term (Name, Type))))
    -> Dom' Term (Name, Type) -> m (ReifiesTo (Dom' Term (Name, Type)))
    forall a b. (a -> b) -> a -> b
    $ (Name
    x,) (Type -> (Name, Type)) -> Dom Type -> Dom' Term (Name, Type)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Dom Type
    a
        let r = Name -> Range
    forall a. HasRange a => a -> Range
    getRange Name
    x
            name = Dom Type -> Maybe (WithOrigin (Ranged MetaNameSuggestion))
    forall t e.
    Dom' t e -> Maybe (WithOrigin (Ranged MetaNameSuggestion))
    domName Dom Type
    a
            xs = Arg (Named (WithOrigin (Ranged MetaNameSuggestion)) Binder)
    -> List1
         (Arg (Named (WithOrigin (Ranged MetaNameSuggestion)) Binder))
    forall el coll. Singleton el coll => el -> coll
    singleton (Arg (Named (WithOrigin (Ranged MetaNameSuggestion)) Binder)
     -> List1
          (Arg (Named (WithOrigin (Ranged MetaNameSuggestion)) Binder)))
    -> Arg (Named (WithOrigin (Ranged MetaNameSuggestion)) Binder)
    -> List1
         (Arg (Named (WithOrigin (Ranged MetaNameSuggestion)) Binder))
    forall a b. (a -> b) -> a -> b
    $ ArgInfo
    -> Named (WithOrigin (Ranged MetaNameSuggestion)) Binder
    -> Arg (Named (WithOrigin (Ranged MetaNameSuggestion)) Binder)
    forall e. ArgInfo -> e -> Arg e
    Arg ArgInfo
    info (Named (WithOrigin (Ranged MetaNameSuggestion)) Binder
     -> Arg (Named (WithOrigin (Ranged MetaNameSuggestion)) Binder))
    -> Named (WithOrigin (Ranged MetaNameSuggestion)) Binder
    -> Arg (Named (WithOrigin (Ranged MetaNameSuggestion)) Binder)
    forall a b. (a -> b) -> a -> b
    $ Maybe (WithOrigin (Ranged MetaNameSuggestion))
    -> Binder -> Named (WithOrigin (Ranged MetaNameSuggestion)) Binder
    forall name a. Maybe name -> a -> Named name a
    Named Maybe (WithOrigin (Ranged MetaNameSuggestion))
    name (Binder -> Named (WithOrigin (Ranged MetaNameSuggestion)) Binder)
    -> Binder -> Named (WithOrigin (Ranged MetaNameSuggestion)) Binder
    forall a b. (a -> b) -> a -> b
    $ Name -> Binder
    A.mkBinder_ Name
    y
        tac <- TacticAttribute <$> do traverse (Ranged noRange <.> reify) $ domTactic a
        return $ TBind r (TypedBindingInfo tac (domIsFinite a)) xs t

    instance Reify i => Reify (I.Elim' i)  where
      type ReifiesTo (I.Elim' i) = I.Elim' (ReifiesTo i)

      reify :: forall (m :: * -> *).
    MonadReify m =>
    Elim' i -> m (ReifiesTo (Elim' i))
    reify = (i -> m (ReifiesTo i)) -> Elim' i -> m (Elim' (ReifiesTo i))
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Elim' a -> f (Elim' b)
    traverse i -> m (ReifiesTo i)
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    forall (m :: * -> *). MonadReify m => i -> m (ReifiesTo i)
    reify
      reifyWhen :: forall (m :: * -> *).
    MonadReify m =>
    Bool -> Elim' i -> m (ReifiesTo (Elim' i))
    reifyWhen Bool
    b = (i -> m (ReifiesTo i)) -> Elim' i -> m (Elim' (ReifiesTo i))
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Elim' a -> f (Elim' b)
    traverse (Bool -> i -> m (ReifiesTo i)
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    Bool -> i -> m (ReifiesTo i)
    forall (m :: * -> *). MonadReify m => Bool -> i -> m (ReifiesTo i)
    reifyWhen Bool
    b)

    instance Reify i => Reify [i] where
      type ReifiesTo [i] = [ReifiesTo i]

      reify :: forall (m :: * -> *). MonadReify m => [i] -> m (ReifiesTo [i])
    reify = (i -> m (ReifiesTo i)) -> [i] -> m [ReifiesTo i]
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> [a] -> f [b]
    traverse i -> m (ReifiesTo i)
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    forall (m :: * -> *). MonadReify m => i -> m (ReifiesTo i)
    reify
      reifyWhen :: forall (m :: * -> *).
    MonadReify m =>
    Bool -> [i] -> m (ReifiesTo [i])
    reifyWhen Bool
    b = (i -> m (ReifiesTo i)) -> [i] -> m [ReifiesTo i]
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> [a] -> f [b]
    traverse (Bool -> i -> m (ReifiesTo i)
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    Bool -> i -> m (ReifiesTo i)
    forall (m :: * -> *). MonadReify m => Bool -> i -> m (ReifiesTo i)
    reifyWhen Bool
    b)

    instance Reify i => Reify (List1 i) where
      type ReifiesTo (List1 i) = List1 (ReifiesTo i)

      reify :: forall (m :: * -> *).
    MonadReify m =>
    List1 i -> m (ReifiesTo (List1 i))
    reify = (i -> m (ReifiesTo i)) -> List1 i -> m (NonEmpty (ReifiesTo i))
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> NonEmpty a -> f (NonEmpty b)
    traverse i -> m (ReifiesTo i)
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    forall (m :: * -> *). MonadReify m => i -> m (ReifiesTo i)
    reify
      reifyWhen :: forall (m :: * -> *).
    MonadReify m =>
    Bool -> List1 i -> m (ReifiesTo (List1 i))
    reifyWhen Bool
    b = (i -> m (ReifiesTo i)) -> List1 i -> m (NonEmpty (ReifiesTo i))
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> NonEmpty a -> f (NonEmpty b)
    traverse (Bool -> i -> m (ReifiesTo i)
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    Bool -> i -> m (ReifiesTo i)
    forall (m :: * -> *). MonadReify m => Bool -> i -> m (ReifiesTo i)
    reifyWhen Bool
    b)

    instance (Reify i1, Reify i2) => Reify (i1, i2) where
        type ReifiesTo (i1, i2) = (ReifiesTo i1, ReifiesTo i2)
        reify :: forall (m :: * -> *).
    MonadReify m =>
    (i1, i2) -> m (ReifiesTo (i1, i2))
    reify (i1
    x,i2
    y) = (,) (ReifiesTo i1 -> ReifiesTo i2 -> (ReifiesTo i1, ReifiesTo i2))
    -> m (ReifiesTo i1)
    -> m (ReifiesTo i2 -> (ReifiesTo i1, ReifiesTo i2))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> i1 -> m (ReifiesTo i1)
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    forall (m :: * -> *). MonadReify m => i1 -> m (ReifiesTo i1)
    reify i1
    x m (ReifiesTo i2 -> (ReifiesTo i1, ReifiesTo i2))
    -> m (ReifiesTo i2) -> m (ReifiesTo i1, ReifiesTo i2)
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> i2 -> m (ReifiesTo i2)
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    forall (m :: * -> *). MonadReify m => i2 -> m (ReifiesTo i2)
    reify i2
    y

    instance (Reify i1, Reify i2, Reify i3) => Reify (i1,i2,i3) where
        type ReifiesTo (i1, i2, i3) = (ReifiesTo i1, ReifiesTo i2, ReifiesTo i3)
        reify :: forall (m :: * -> *).
    MonadReify m =>
    (i1, i2, i3) -> m (ReifiesTo (i1, i2, i3))
    reify (i1
    x,i2
    y,i3
    z) = (,,) (ReifiesTo i1
     -> ReifiesTo i2
     -> ReifiesTo i3
     -> (ReifiesTo i1, ReifiesTo i2, ReifiesTo i3))
    -> m (ReifiesTo i1)
    -> m (ReifiesTo i2
          -> ReifiesTo i3 -> (ReifiesTo i1, ReifiesTo i2, ReifiesTo i3))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> i1 -> m (ReifiesTo i1)
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    forall (m :: * -> *). MonadReify m => i1 -> m (ReifiesTo i1)
    reify i1
    x m (ReifiesTo i2
       -> ReifiesTo i3 -> (ReifiesTo i1, ReifiesTo i2, ReifiesTo i3))
    -> m (ReifiesTo i2)
    -> m (ReifiesTo i3 -> (ReifiesTo i1, ReifiesTo i2, ReifiesTo i3))
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> i2 -> m (ReifiesTo i2)
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    forall (m :: * -> *). MonadReify m => i2 -> m (ReifiesTo i2)
    reify i2
    y m (ReifiesTo i3 -> (ReifiesTo i1, ReifiesTo i2, ReifiesTo i3))
    -> m (ReifiesTo i3) -> m (ReifiesTo i1, ReifiesTo i2, ReifiesTo i3)
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> i3 -> m (ReifiesTo i3)
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    forall (m :: * -> *). MonadReify m => i3 -> m (ReifiesTo i3)
    reify i3
    z

    instance (Reify i1, Reify i2, Reify i3, Reify i4) => Reify (i1,i2,i3,i4) where
        type ReifiesTo (i1, i2, i3, i4) = (ReifiesTo i1, ReifiesTo i2, ReifiesTo i3, ReifiesTo i4)
        reify :: forall (m :: * -> *).
    MonadReify m =>
    (i1, i2, i3, i4) -> m (ReifiesTo (i1, i2, i3, i4))
    reify (i1
    x,i2
    y,i3
    z,i4
    w) = (,,,) (ReifiesTo i1
     -> ReifiesTo i2
     -> ReifiesTo i3
     -> ReifiesTo i4
     -> (ReifiesTo i1, ReifiesTo i2, ReifiesTo i3, ReifiesTo i4))
    -> m (ReifiesTo i1)
    -> m (ReifiesTo i2
          -> ReifiesTo i3
          -> ReifiesTo i4
          -> (ReifiesTo i1, ReifiesTo i2, ReifiesTo i3, ReifiesTo i4))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> i1 -> m (ReifiesTo i1)
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    forall (m :: * -> *). MonadReify m => i1 -> m (ReifiesTo i1)
    reify i1
    x m (ReifiesTo i2
       -> ReifiesTo i3
       -> ReifiesTo i4
       -> (ReifiesTo i1, ReifiesTo i2, ReifiesTo i3, ReifiesTo i4))
    -> m (ReifiesTo i2)
    -> m (ReifiesTo i3
          -> ReifiesTo i4
          -> (ReifiesTo i1, ReifiesTo i2, ReifiesTo i3, ReifiesTo i4))
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> i2 -> m (ReifiesTo i2)
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    forall (m :: * -> *). MonadReify m => i2 -> m (ReifiesTo i2)
    reify i2
    y m (ReifiesTo i3
       -> ReifiesTo i4
       -> (ReifiesTo i1, ReifiesTo i2, ReifiesTo i3, ReifiesTo i4))
    -> m (ReifiesTo i3)
    -> m (ReifiesTo i4
          -> (ReifiesTo i1, ReifiesTo i2, ReifiesTo i3, ReifiesTo i4))
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> i3 -> m (ReifiesTo i3)
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    forall (m :: * -> *). MonadReify m => i3 -> m (ReifiesTo i3)
    reify i3
    z m (ReifiesTo i4
       -> (ReifiesTo i1, ReifiesTo i2, ReifiesTo i3, ReifiesTo i4))
    -> m (ReifiesTo i4)
    -> m (ReifiesTo i1, ReifiesTo i2, ReifiesTo i3, ReifiesTo i4)
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> i4 -> m (ReifiesTo i4)
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    forall (m :: * -> *). MonadReify m => i4 -> m (ReifiesTo i4)
    reify i4
    w