    {-# 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'(..))
    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.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.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.Utils.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' Bool TCState
    -> (Bool -> Bool) -> TCMT IO (ReifiesTo i) -> TCMT IO (ReifiesTo i)
    forall (m :: * -> *) a b.
    ReadTCState m =>
    Lens' a TCState -> (a -> a) -> m b -> m b
    locallyTCState Lens' Bool TCState
    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)
    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

    -- | 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 ------------------------------------

    -- | 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 (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 (Named_ Expr)
    arg <- Arg (Named_ Expr) -> m (ReifiesTo (Arg (Named_ Expr)))
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    reify Arg (Named_ Expr)
    arg  -- This replaces the arg by _ if irrelevant
      Bool
    dontShowImp <- 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
    showImplicitArguments
      let hd :: Expr
    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
      Expr -> [Elim' (Named_ Expr)] -> m Expr
    forall (m :: * -> *).
    MonadReify m =>
    Expr -> [Elim' (Named_ Expr)] -> m Expr
    nelims Expr
    hd [Elim' (Named_ Expr)]
    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

    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

    -- | 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 (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 --------------

    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)
    reify i
    i
    reifyWhenE Bool
    False i
    t = ReifiesTo i -> m (ReifiesTo i)
    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)
    reify

    instance Reify Bool where
        type ReifiesTo Bool = Bool
        reify :: forall (m :: * -> *). MonadReify m => Bool -> m (ReifiesTo Bool)
    reify = Bool -> m (ReifiesTo Bool)
    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 (ReifiesTo Name)
    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 (ReifiesTo Expr)
    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 x :: MetaId
    x@(MetaId Nat
    n) = do
          Bool
    b <- (TCEnv -> Bool) -> m Bool
    forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
    asksTC TCEnv -> Bool
    envPrintMetasBare
          MetaInfo
    mi  <- MetaVariable -> MetaInfo
    mvInfo (MetaVariable -> MetaInfo) -> m MetaVariable -> m MetaInfo
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> MetaId -> m MetaVariable
    forall (m :: * -> *).
    (MonadFail m, ReadTCState m) =>
    MetaId -> m MetaVariable
    lookupMeta MetaId
    x
          let mi' :: MetaInfo
    mi' = MetaInfo :: Range -> ScopeInfo -> Maybe MetaId -> String -> MetaInfo
    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 :: String
    metaNameSuggestion = if Bool
    b then String
    "" else MetaInfo -> String
    miNameSuggestion MetaInfo
    mi
                     }
              underscore :: m Expr
    underscore = Expr -> m Expr
    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
          MetaId -> m (Maybe InteractionId)
    forall (m :: * -> *).
    ReadTCState m =>
    MetaId -> m (Maybe InteractionId)
    isInteractionMeta MetaId
    x m (Maybe InteractionId)
    -> (Maybe InteractionId -> m Expr) -> m Expr
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
            Maybe InteractionId
    Nothing | Bool
    b -> do
              InteractionId
    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
              InteractionId -> MetaId -> m ()
    forall (m :: * -> *).
    MonadInteractionPoints m =>
    InteractionId -> MetaId -> m ()
    connectInteractionPoint InteractionId
    ii MetaId
    x
              Expr -> m Expr
    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
            Just InteractionId
    ii | Bool
    b -> m Expr
    underscore
            Maybe InteractionId
    Nothing     -> m Expr
    underscore
            Just InteractionId
    ii     -> Expr -> m Expr
    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

    -- Does not print with-applications correctly:
    -- instance Reify DisplayTerm Expr where
    --   reifyWhen = reifyWhenE
    --   reify d = reifyTerm False $ dtermToTerm d

    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 -> Bool -> Term -> m Expr
    forall (m :: * -> *). MonadReify m => Bool -> Term -> m Expr
    reifyTerm Bool
    False Term
    v
        DDot  Term
    v -> Term -> m (ReifiesTo Term)
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    reify Term
    v
        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)
    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)
    reify [Elim' DisplayTerm]
    es
        DWithApp DisplayTerm
    u [DisplayTerm]
    us Elims
    es0 -> do
          (Expr
    e, [Expr]
    es) <- (DisplayTerm, [DisplayTerm])
    -> m (ReifiesTo (DisplayTerm, [DisplayTerm]))
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    reify (DisplayTerm
    u, [DisplayTerm]
    us)
          Expr -> [Elim' Expr] -> m Expr
    forall (m :: * -> *).
    MonadReify m =>
    Expr -> [Elim' Expr] -> m Expr
    elims (if [Expr] -> Bool
    forall a. Null a => a -> Bool
    null [Expr]
    es then Expr
    e else ExprInfo -> Expr -> [Expr] -> Expr
    A.WithApp ExprInfo
    noExprInfo Expr
    e [Expr]
    es) ([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)
    reify Elims
    es0

    -- | @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
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    reify

    -- | @reifyDisplayFormP@ tries to recursively
    --   rewrite a lhs with a display form.
    --
    --   Note: we are not necessarily in the empty context upon entry!
    reifyDisplayFormP
      :: 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 (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?
        Maybe DisplayTerm
    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..]
        String -> Nat -> String -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Nat -> String -> m ()
    reportSLn String
    "reify.display" Nat
    60 (String -> m ()) -> String -> m ()
    forall a b. (a -> b) -> a -> b
    $
          String
    "display form of " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ QName -> String
    forall a. Pretty a => a -> String
    prettyShow QName
    f String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Patterns -> String
    forall a. Show a => a -> String
    show Patterns
    ps String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Patterns -> String
    forall a. Show a => a -> String
    show Patterns
    wps String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ":\n  " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Maybe DisplayTerm -> String
    forall a. Show a => a -> String
    show Maybe DisplayTerm
    md
        case Maybe DisplayTerm
    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?
            (QName
    f', Patterns
    ps', Patterns
    wps') <- Patterns -> DisplayTerm -> m (QName, Patterns, Patterns)
    forall (m :: * -> *).
    MonadReify m =>
    Patterns -> DisplayTerm -> m (QName, Patterns, Patterns)
    displayLHS Patterns
    ps DisplayTerm
    d
            String -> Nat -> TCM Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Nat -> TCM Doc -> m ()
    reportSDoc String
    "reify.display" Nat
    70 (TCM Doc -> m ()) -> TCM Doc -> m ()
    forall a b. (a -> b) -> a -> b
    $ do
              Doc
    doc <- SpineLHS -> TCM Doc
    forall a (m :: * -> *).
    (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
    a -> m Doc
    prettyA (SpineLHS -> TCM Doc) -> SpineLHS -> TCM Doc
    forall a b. (a -> b) -> a -> b
    $ LHSInfo -> QName -> Patterns -> SpineLHS
    SpineLHS LHSInfo
    forall a. Null a => a
    empty QName
    f' (Patterns
    ps' Patterns -> Patterns -> Patterns
    forall a. [a] -> [a] -> [a]
    ++ Patterns
    wps' Patterns -> Patterns -> Patterns
    forall a. [a] -> [a] -> [a]
    ++ Patterns
    wps)
              Doc -> TCM Doc
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Doc -> TCM Doc) -> Doc -> TCM Doc
    forall a b. (a -> b) -> a -> b
    $ [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    vcat
                [ Doc
    "rewritten lhs to"
                , Doc
    "  lhs' = " Doc -> Doc -> Doc
    <+> Doc
    doc
                ]
            QName -> Patterns -> Patterns -> m (QName, Patterns)
    forall (m :: * -> *).
    MonadReify m =>
    QName -> Patterns -> Patterns -> m (QName, Patterns)
    reifyDisplayFormP QName
    f' Patterns
    ps' (Patterns
    wps' Patterns -> Patterns -> Patterns
    forall a. [a] -> [a] -> [a]
    ++ Patterns
    wps)
          Maybe DisplayTerm
    _ -> do
            String -> Nat -> String -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Nat -> String -> m ()
    reportSLn String
    "reify.display" Nat
    70 (String -> m ()) -> String -> m ()
    forall a b. (a -> b) -> a -> b
    $ String
    "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 (DWithApp DisplayTerm
    d [DisplayTerm]
    ds Elims
    es) =
          DisplayTerm -> Bool
    okDisplayForm DisplayTerm
    d Bool -> Bool -> Bool
    && (DisplayTerm -> Bool) -> [DisplayTerm] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all DisplayTerm -> Bool
    okDisplayTerm [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.
        okDisplayForm (DTerm (I.Def QName
    f Elims
    vs)) = (Elim' Term -> Bool) -> Elims -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all Elim' Term -> Bool
    okElim Elims
    vs
        okDisplayForm (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
        okDisplayForm DDot{}               = Bool
    False
        okDisplayForm DCon{}               = Bool
    False
        okDisplayForm DTerm{}              = Bool
    False

        okDisplayTerm :: DisplayTerm -> Bool
        okDisplayTerm :: DisplayTerm -> Bool
    okDisplayTerm (DTerm Term
    v) = Term -> Bool
    okTerm Term
    v
        okDisplayTerm DDot{}    = Bool
    True
        okDisplayTerm DCon{}    = Bool
    True
        okDisplayTerm DDef{}    = Bool
    False
        okDisplayTerm DisplayTerm
    _         = 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 [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) [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 (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)) = (QName
    f, (Elim' Term -> Elim' DisplayTerm) -> Elims -> [Elim' DisplayTerm]
    forall a b. (a -> b) -> [a] -> [b]
    map ((Term -> DisplayTerm) -> Elim' Term -> Elim' DisplayTerm
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Term -> DisplayTerm
    DTerm) 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 :: forall (m :: * -> *).
    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
            Patterns
    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)
    mapM Elim' DisplayTerm -> m (Arg (Named_ Pattern))
    forall (m :: * -> *).
    MonadReify m =>
    Elim' DisplayTerm -> m (Arg (Named_ Pattern))
    elimToPat [Elim' DisplayTerm]
    vs
            Patterns
    wps <- (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)
    mapM ((Pattern -> Pattern)
    -> Arg (Named_ Pattern) -> Arg (Named_ Pattern)
    forall a b. (a -> b) -> NamedArg a -> NamedArg b
    updateNamedArg (PatInfo -> Pattern -> Pattern
    forall e. PatInfo -> Pattern' e -> Pattern' e
    A.WithP PatInfo
    forall a. Null a => a
    empty) (Arg (Named_ Pattern) -> Arg (Named_ Pattern))
    -> (Elim' DisplayTerm -> m (Arg (Named_ Pattern)))
    -> Elim' DisplayTerm
    -> m (Arg (Named_ Pattern))
    forall (m :: * -> *) b c a.
    Functor m =>
    (b -> c) -> (a -> m b) -> a -> m c
    <.> Elim' DisplayTerm -> m (Arg (Named_ Pattern))
    forall (m :: * -> *).
    MonadReify m =>
    Elim' DisplayTerm -> m (Arg (Named_ Pattern))
    elimToPat) [Elim' DisplayTerm]
    es
            (QName, Patterns, Patterns) -> m (QName, Patterns, Patterns)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (QName
    f, Patterns
    ps, Patterns
    wps)
          where
            argToPat :: MonadReify m => Arg DisplayTerm -> m (NamedArg A.Pattern)
            argToPat :: forall (m :: * -> *).
    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)
    traverse DisplayTerm -> m (Named_ Pattern)
    forall (m :: * -> *).
    MonadReify m =>
    DisplayTerm -> m (Named_ Pattern)
    termToPat Arg DisplayTerm
    arg

            elimToPat :: MonadReify m => I.Elim' DisplayTerm -> m (NamedArg A.Pattern)
            elimToPat :: forall (m :: * -> *).
    MonadReify m =>
    Elim' DisplayTerm -> m (Arg (Named_ Pattern))
    elimToPat (I.IApply DisplayTerm
    _ DisplayTerm
    _ DisplayTerm
    r) = Arg DisplayTerm -> m (Arg (Named_ Pattern))
    forall (m :: * -> *).
    MonadReify m =>
    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) = Arg DisplayTerm -> m (Arg (Named_ Pattern))
    forall (m :: * -> *).
    MonadReify m =>
    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 (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 :: forall (m :: * -> *).
    MonadReify m =>
    DisplayTerm -> m (Named_ Pattern)
    termToPat (DTerm (I.Var Nat
    n [])) = Named_ Pattern -> m (Named_ Pattern)
    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 (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)
    mapM Arg DisplayTerm -> m (Arg (Named_ Pattern))
    forall (m :: * -> *).
    MonadReify m =>
    Arg DisplayTerm -> m (Arg (Named_ Pattern))
    argToPat [Arg DisplayTerm]
    vs

            termToPat (DTerm (I.Con ConHead
    c ConInfo
    ci Elims
    vs)) = (Pattern -> Named_ Pattern) -> m Pattern -> m (Named_ Pattern)
    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)
    mapM (Elim' DisplayTerm -> m (Arg (Named_ Pattern))
    forall (m :: * -> *).
    MonadReify m =>
    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 (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Term -> DisplayTerm
    DTerm) Elims
    vs

            termToPat (DTerm (I.Def QName
    _ [])) = Named_ Pattern -> m (Named_ Pattern)
    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 (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 (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)             = 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
    <$> Term -> m Expr
    forall (m :: * -> *). MonadReify m => Term -> m Expr
    termToExpr Term
    v
            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)
    reify DisplayTerm
    v

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

            argsToExpr :: MonadReify m => I.Args -> m [Arg A.Expr]
            argsToExpr :: forall (m :: * -> *). 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)
    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)
    traverse Term -> m Expr
    forall (m :: * -> *). MonadReify m => Term -> m Expr
    termToExpr)

            -- TODO: restructure this to avoid having to repeat the code for reify
            termToExpr :: MonadReify m => Term -> m A.Expr
            termToExpr :: forall (m :: * -> *). MonadReify m => Term -> m Expr
    termToExpr Term
    v = do
              String -> Nat -> String -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Nat -> String -> m ()
    reportSLn String
    "reify.display" Nat
    60 (String -> m ()) -> String -> m ()
    forall a b. (a -> b) -> a -> b
    $ String
    "termToExpr " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Term -> String
    forall a. Show a => a -> String
    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)
    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]
    forall (m :: * -> *). 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)
    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]
    forall (m :: * -> *). 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)
    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@.
                  Expr
    e <- if Nat
    n Nat -> Nat -> Bool
    forall a. Ord a => a -> a -> Bool
    < Nat
    len
                       then Expr -> m Expr
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Expr -> m Expr) -> Expr -> m Expr
    forall a b. (a -> b) -> a -> b
    $ Pattern -> Expr
    A.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)
    reify (Nat -> Term
    I.var (Nat
    n Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    - Nat
    len))
                  Expr -> [Arg Expr] -> m Expr
    forall (m :: * -> *). MonadReify m => Expr -> [Arg Expr] -> m Expr
    apps Expr
    e ([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]
    forall (m :: * -> *). MonadReify m => Args -> m [Arg Expr]
    argsToExpr Args
    vs
                Term
    _ -> Expr -> m Expr
    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 (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

    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

    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
       String -> Nat -> String -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Nat -> String -> m ()
    reportSLn String
    "reify.def" Nat
    100 (String -> m ()) -> String -> m ()
    forall a b. (a -> b) -> a -> b
    $ String
    "reifying def path " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ (QName, Elims) -> String
    forall a. Show a => a -> String
    show (QName
    x,Elims
    es)
       Maybe QName
    mpath  <- String -> m (Maybe QName)
    forall (m :: * -> *). HasBuiltins m => String -> m (Maybe QName)
    getBuiltinName' String
    builtinPath
       Maybe QName
    mpathp <- String -> m (Maybe QName)
    forall (m :: * -> *). HasBuiltins m => String -> m (Maybe QName)
    getBuiltinName' String
    builtinPathP
       let fallback :: m (QName, Elims)
    fallback = (QName, Elims) -> m (QName, Elims)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (QName
    x,Elims
    es)
       case (,) (QName -> QName -> (QName, QName))
    -> Maybe QName -> Maybe (QName -> (QName, QName))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Maybe QName
    mpath Maybe (QName -> (QName, QName))
    -> Maybe QName -> Maybe (QName, QName)
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Maybe QName
    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 String
    _ Term
    b)    -> Term -> Maybe Term
    forall a. a -> Maybe a
    Just Term
    b
                    I.Lam ArgInfo
    _ (Abs   String
    _ 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 (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 (m :: * -> *) a. Monad m => a -> m a
    return (QName
    x,Elims
    es)

    reifyTerm :: MonadReify m => Bool -> Term -> m Expr
    reifyTerm :: forall (m :: * -> *). MonadReify m => Bool -> Term -> m Expr
    reifyTerm Bool
    expandAnonDefs0 Term
    v0 = do
      -- Jesper 2018-11-02: If 'PrintMetasBare', drop all meta eliminations.
      Bool
    metasBare <- (TCEnv -> Bool) -> m Bool
    forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
    asksTC TCEnv -> Bool
    envPrintMetasBare
      Term
    v <- Term -> m Term
    forall a (m :: * -> *). (Instantiate a, MonadReduce m) => a -> m a
    instantiate Term
    v0 m Term -> (Term -> m Term) -> m Term
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
        I.MetaV MetaId
    x Elims
    _ | Bool
    metasBare -> Term -> m Term
    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 (m :: * -> *) a. Monad m => a -> m a
    return Term
    v
      -- Ulf 2014-07-10: Don't expand anonymous when display forms are disabled
      -- (i.e. when we don't care about nice printing)
      Bool
    expandAnonDefs <- Bool -> m Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    expandAnonDefs0 m Bool -> m Bool -> m Bool
    forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
    `and2M` m Bool
    forall (m :: * -> *). MonadTCEnv m => m Bool
    displayFormsEnabled
      -- Andreas, 2016-07-21 if --postfix-projections
      -- then we print system-generated projections as postfix, else prefix.
      Bool
    havePfp <- PragmaOptions -> Bool
    optPostfixProjections (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
      let pred :: ProjOrigin -> Bool
    pred = if Bool
    havePfp then (ProjOrigin -> ProjOrigin -> Bool
    forall a. Eq a => a -> a -> Bool
    == ProjOrigin
    ProjPrefix) else (ProjOrigin -> ProjOrigin -> Bool
    forall a. Eq a => a -> a -> Bool
    /= ProjOrigin
    ProjPostfix)
      case (ProjOrigin -> Bool) -> Term -> Term
    unSpine' ProjOrigin -> Bool
    pred Term
    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 String
    name <- QName -> Maybe String
    getGeneralizedFieldName QName
    p -> do
          let fakeName :: Name
    fakeName = (QName -> Name
    qnameName QName
    p) {nameConcrete :: Name
    nameConcrete = String -> Name
    C.simpleName String
    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)
    reify Elims
    es
        I.Var Nat
    n Elims
    es -> do
          Name
    x <- m Name -> m (Maybe Name) -> m Name
    forall (m :: * -> *) a. Monad m => m a -> m (Maybe a) -> m a
    fromMaybeM (String -> m Name
    forall a (m :: * -> *).
    (FreshName a, MonadFresh NameId m) =>
    a -> m Name
    freshName_ (String -> m Name) -> String -> m Name
    forall a b. (a -> b) -> a -> b
    $ String
    "@" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Nat -> String
    forall a. Show a => a -> String
    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 :: * -> *).
    (Applicative m, MonadFail m, MonadTCEnv m) =>
    Nat -> m (Maybe Name)
    nameOfBV' Nat
    n
          Expr -> [Elim' Expr] -> m Expr
    forall (m :: * -> *).
    MonadReify m =>
    Expr -> [Elim' Expr] -> m Expr
    elims (Name -> Expr
    A.Var Name
    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)
    reify Elims
    es
        I.Def QName
    x Elims
    es -> do
          String -> Nat -> TCM Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Nat -> TCM Doc -> m ()
    reportSDoc String
    "reify.def" Nat
    80 (TCM Doc -> m ()) -> TCM Doc -> m ()
    forall a b. (a -> b) -> a -> b
    $ Doc -> TCM Doc
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Doc -> TCM Doc) -> Doc -> TCM Doc
    forall a b. (a -> b) -> a -> b
    $ Doc
    "reifying def" Doc -> Doc -> Doc
    <+> QName -> Doc
    forall a. Pretty a => a -> Doc
    pretty QName
    x
          (QName
    x, Elims
    es) <- QName -> Elims -> m (QName, Elims)
    forall (m :: * -> *).
    MonadReify m =>
    QName -> Elims -> m (QName, Elims)
    reifyPathPConstAsPath QName
    x Elims
    es
          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
    $ Bool -> QName -> Elims -> m Expr
    forall (m :: * -> *).
    MonadReify m =>
    Bool -> QName -> Elims -> m Expr
    reifyDef Bool
    expandAnonDefs QName
    x Elims
    es
        I.Con ConHead
    c ConInfo
    ci Elims
    vs -> do
          let x :: QName
    x = ConHead -> QName
    conName ConHead
    c
          Bool
    isR <- QName -> m Bool
    forall (m :: * -> *).
    (MonadTCEnv m, HasConstInfo m) =>
    QName -> m Bool
    isGeneratedRecordConstructor QName
    x
          if Bool
    isR Bool -> Bool -> Bool
    || ConInfo
    ci ConInfo -> ConInfo -> Bool
    forall a. Eq a => a -> a -> Bool
    == ConInfo
    ConORec
            then do
              Bool
    showImp <- m Bool
    forall (m :: * -> *). HasOptions m => m Bool
    showImplicitArguments
              let keep :: (Dom Name, Expr) -> Bool
    keep (Dom Name
    a, Expr
    v) = Bool
    showImp Bool -> Bool -> Bool
    || Dom Name -> Bool
    forall a. LensHiding a => a -> Bool
    visible Dom Name
    a
              QName
    r <- QName -> m QName
    forall (m :: * -> *). HasConstInfo m => QName -> m QName
    getConstructorData QName
    x
              [Dom Name]
    xs <- [Dom Name] -> Maybe [Dom Name] -> [Dom Name]
    forall a. a -> Maybe a -> a
    fromMaybe [Dom Name]
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe [Dom Name] -> [Dom Name])
    -> m (Maybe [Dom Name]) -> m [Dom Name]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> m (Maybe [Dom Name])
    forall (m :: * -> *).
    (HasConstInfo m, ReadTCState m) =>
    QName -> m (Maybe [Dom Name])
    getRecordFieldNames_ QName
    r
              [Expr]
    vs <- (Arg Expr -> Expr) -> [Arg Expr] -> [Expr]
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Expr -> Expr
    forall e. Arg e -> e
    unArg ([Arg Expr] -> [Expr]) -> m [Arg Expr] -> m [Expr]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Args -> m (ReifiesTo Args)
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    reify (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
    vs)
              Expr -> m Expr
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Expr -> m Expr) -> Expr -> m Expr
    forall a b. (a -> b) -> a -> b
    $ ExprInfo -> RecordAssigns -> Expr
    A.Rec ExprInfo
    noExprInfo (RecordAssigns -> Expr) -> RecordAssigns -> Expr
    forall a b. (a -> b) -> a -> b
    $ ((Dom Name, Expr) -> Either (FieldAssignment' Expr) ModuleName)
    -> [(Dom Name, Expr)] -> RecordAssigns
    forall a b. (a -> b) -> [a] -> [b]
    map (FieldAssignment' Expr -> Either (FieldAssignment' Expr) ModuleName
    forall a b. a -> Either a b
    Left (FieldAssignment' Expr
     -> Either (FieldAssignment' Expr) ModuleName)
    -> ((Dom Name, Expr) -> FieldAssignment' Expr)
    -> (Dom Name, Expr)
    -> Either (FieldAssignment' Expr) ModuleName
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Name -> Expr -> FieldAssignment' Expr)
    -> (Name, Expr) -> FieldAssignment' Expr
    forall a b c. (a -> b -> c) -> (a, b) -> c
    uncurry Name -> Expr -> FieldAssignment' Expr
    forall a. Name -> a -> FieldAssignment' a
    FieldAssignment ((Name, Expr) -> FieldAssignment' Expr)
    -> ((Dom Name, Expr) -> (Name, Expr))
    -> (Dom Name, Expr)
    -> FieldAssignment' Expr
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Dom Name -> Name) -> (Dom Name, Expr) -> (Name, Expr)
    forall a c b. (a -> c) -> (a, b) -> (c, b)
    mapFst Dom Name -> Name
    forall t e. Dom' t e -> e
    unDom) ([(Dom Name, Expr)] -> RecordAssigns)
    -> [(Dom Name, Expr)] -> RecordAssigns
    forall a b. (a -> b) -> a -> b
    $ ((Dom Name, Expr) -> Bool)
    -> [(Dom Name, Expr)] -> [(Dom Name, Expr)]
    forall a. (a -> Bool) -> [a] -> [a]
    filter (Dom Name, Expr) -> Bool
    keep ([(Dom Name, Expr)] -> [(Dom Name, Expr)])
    -> [(Dom Name, Expr)] -> [(Dom Name, Expr)]
    forall a b. (a -> b) -> a -> b
    $ [Dom Name] -> [Expr] -> [(Dom Name, Expr)]
    forall a b. [a] -> [b] -> [(a, b)]
    zip [Dom Name]
    xs [Expr]
    vs
            else QName -> Elims -> m Expr -> m Expr
    forall (m :: * -> *).
    MonadReify m =>
    QName -> Elims -> m Expr -> m Expr
    reifyDisplayForm QName
    x Elims
    vs (m Expr -> m Expr) -> m Expr -> m Expr
    forall a b. (a -> b) -> a -> b
    $ do
              Definition
    def <- QName -> m Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    x
              let Constructor {conPars :: Defn -> Nat
    conPars = Nat
    np} = Definition -> Defn
    theDef Definition
    def
              -- if we are the the module that defines constructor x
              -- then we have to drop at least the n module parameters
              Nat
    n <- QName -> m Nat
    forall (m :: * -> *).
    (Functor m, Applicative m, ReadTCState m, MonadTCEnv m) =>
    QName -> m Nat
    getDefFreeVars QName
    x
              -- the number of parameters is greater (if the data decl has
              -- extra parameters) or equal (if not) to n
              Bool -> m () -> m ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when (Nat
    n Nat -> Nat -> Bool
    forall a. Ord a => a -> a -> Bool
    > Nat
    np) m ()
    forall a. HasCallStack => a
    __IMPOSSIBLE__
              let h :: Expr
    h = AmbiguousQName -> Expr
    A.Con (QName -> AmbiguousQName
    unambiguous QName
    x)
              if Elims -> Bool
    forall a. Null a => a -> Bool
    null Elims
    vs
                then Expr -> m Expr
    forall (m :: * -> *) a. Monad m => a -> m a
    return Expr
    h
                else do
                  [Arg Expr]
    es <- Args -> m (ReifiesTo Args)
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    reify ((Elim' Term -> Arg Term) -> Elims -> Args
    forall a b. (a -> b) -> [a] -> [b]
    map (Arg Term -> Maybe (Arg Term) -> Arg Term
    forall a. a -> Maybe a -> a
    fromMaybe Arg Term
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe (Arg Term) -> Arg Term)
    -> (Elim' Term -> Maybe (Arg Term)) -> Elim' Term -> Arg Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Elim' Term -> Maybe (Arg Term)
    forall a. Elim' a -> Maybe (Arg a)
    isApplyElim) Elims
    vs)
                  -- 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 Nat
    np Nat -> Nat -> Bool
    forall a. Eq a => a -> a -> Bool
    == Nat
    0
                    then Expr -> [Arg Expr] -> m Expr
    forall (m :: * -> *). MonadReify m => Expr -> [Arg Expr] -> m Expr
    apps Expr
    h [Arg Expr]
    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 Telescope
    tel Type
    _ <- Type -> m (TelV Type)
    forall (m :: * -> *).
    (MonadReduce m, MonadAddContext m) =>
    Type -> m (TelV Type)
    telView (Definition -> Type
    defType Definition
    def)
                      let ([Dom (String, Type)]
    pars, [Dom (String, Type)]
    rest) = Nat
    -> [Dom (String, Type)]
    -> ([Dom (String, Type)], [Dom (String, Type)])
    forall a. Nat -> [a] -> ([a], [a])
    splitAt Nat
    np ([Dom (String, Type)]
     -> ([Dom (String, Type)], [Dom (String, Type)]))
    -> [Dom (String, Type)]
    -> ([Dom (String, Type)], [Dom (String, Type)])
    forall a b. (a -> b) -> a -> b
    $ Telescope -> [Dom (String, Type)]
    forall t. Tele (Dom t) -> [Dom (String, t)]
    telToList Telescope
    tel
                      case [Dom (String, Type)]
    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 (String, Type)]
    _) | ArgInfo -> Bool
    forall a. LensHiding a => a -> Bool
    notVisible ArgInfo
    info -> do
                          let us :: [Arg Expr]
    us = [Dom (String, Type)]
    -> (Dom (String, Type) -> Arg Expr) -> [Arg Expr]
    forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
    for (Nat -> [Dom (String, Type)] -> [Dom (String, Type)]
    forall a. Nat -> [a] -> [a]
    drop Nat
    n [Dom (String, Type)]
    pars) ((Dom (String, Type) -> Arg Expr) -> [Arg Expr])
    -> (Dom (String, 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 (String, 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
          (Name
    x,Expr
    e) <- Abs Term -> m (ReifiesTo (Abs Term))
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    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.
          ArgInfo
    info <- m Bool -> m ArgInfo -> m ArgInfo -> m ArgInfo
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
    ifM m Bool
    forall (m :: * -> *). HasOptions m => m Bool
    showImplicitArguments (ArgInfo -> m ArgInfo
    forall (m :: * -> *) a. Monad m => a -> m a
    return (ArgInfo -> m ArgInfo) -> ArgInfo -> m ArgInfo
    forall a b. (a -> b) -> a -> b
    $ Origin -> ArgInfo -> ArgInfo
    forall a. LensOrigin a => Origin -> a -> a
    setOrigin Origin
    UserWritten ArgInfo
    info) (ArgInfo -> m ArgInfo
    forall (m :: * -> *) a. Monad m => a -> m a
    return ArgInfo
    info)
          Expr -> m Expr
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Expr -> m Expr) -> Expr -> m Expr
    forall a b. (a -> b) -> a -> b
    $ ExprInfo -> LamBinding -> Expr -> Expr
    A.Lam ExprInfo
    exprNoRange (Arg (Named (WithOrigin (Ranged String)) Binder) -> LamBinding
    mkDomainFree (Arg (Named (WithOrigin (Ranged String)) Binder) -> LamBinding)
    -> Arg (Named (WithOrigin (Ranged String)) Binder) -> LamBinding
    forall a b. (a -> b) -> a -> b
    $ ArgInfo
    -> Binder -> Arg (Named (WithOrigin (Ranged String)) Binder)
    forall a. ArgInfo -> a -> NamedArg a
    unnamedArg ArgInfo
    info (Binder -> Arg (Named (WithOrigin (Ranged String)) Binder))
    -> Binder -> Arg (Named (WithOrigin (Ranged String)) Binder)
    forall a b. (a -> b) -> a -> b
    $ Name -> Binder
    mkBinder_ Name
    x) Expr
    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)
    reify Literal
    l
        I.Level Level
    l      -> Level -> m (ReifiesTo Level)
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    reify Level
    l
        I.Pi Dom Type
    a Abs Type
    b       -> case Abs Type
    b of
            NoAbs String
    _ Type
    b'
              | Dom Type -> Bool
    forall a. LensHiding a => a -> Bool
    visible 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)
    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).
              | 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)
    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 (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)
    reify Dom Type
    a)
          where
            mkPi :: Abs Type -> Arg Expr -> m Expr
    mkPi Abs Type
    b (Arg ArgInfo
    info Expr
    a') = do
              Maybe Expr
    tac <- (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)
    traverse Term -> m Expr
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    reify (Maybe Term -> m (Maybe Expr)) -> Maybe Term -> m (Maybe Expr)
    forall a b. (a -> b) -> a -> b
    $ Dom Type -> Maybe Term
    forall t e. Dom' t e -> Maybe t
    domTactic Dom Type
    a
              (Name
    x, Expr
    b) <- Abs Type -> m (ReifiesTo (Abs Type))
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    reify Abs Type
    b
              let xs :: List1 (Arg (Named (WithOrigin (Ranged String)) Binder))
    xs = Arg (Named (WithOrigin (Ranged String)) Binder)
    -> List1 (Arg (Named (WithOrigin (Ranged String)) Binder))
    forall el coll. Singleton el coll => el -> coll
    singleton (Arg (Named (WithOrigin (Ranged String)) Binder)
     -> List1 (Arg (Named (WithOrigin (Ranged String)) Binder)))
    -> Arg (Named (WithOrigin (Ranged String)) Binder)
    -> List1 (Arg (Named (WithOrigin (Ranged String)) Binder))
    forall a b. (a -> b) -> a -> b
    $ ArgInfo
    -> Named (WithOrigin (Ranged String)) Binder
    -> Arg (Named (WithOrigin (Ranged String)) Binder)
    forall e. ArgInfo -> e -> Arg e
    Arg ArgInfo
    info (Named (WithOrigin (Ranged String)) Binder
     -> Arg (Named (WithOrigin (Ranged String)) Binder))
    -> Named (WithOrigin (Ranged String)) Binder
    -> Arg (Named (WithOrigin (Ranged String)) Binder)
    forall a b. (a -> b) -> a -> b
    $ Maybe (WithOrigin (Ranged String))
    -> Binder -> Named (WithOrigin (Ranged String)) Binder
    forall name a. Maybe name -> a -> Named name a
    Named (Dom Type -> Maybe (WithOrigin (Ranged String))
    forall t e. Dom' t e -> Maybe (WithOrigin (Ranged String))
    domName Dom Type
    a) (Binder -> Named (WithOrigin (Ranged String)) Binder)
    -> Binder -> Named (WithOrigin (Ranged String)) Binder
    forall a b. (a -> b) -> a -> b
    $ Name -> Binder
    mkBinder_ Name
    x
              Expr -> m Expr
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Expr -> m Expr) -> Expr -> m Expr
    forall a b. (a -> b) -> a -> b
    $ ExprInfo -> Telescope1 -> Expr -> Expr
    A.Pi ExprInfo
    noExprInfo (TypedBinding -> Telescope1
    forall el coll. Singleton el coll => el -> coll
    singleton (TypedBinding -> Telescope1) -> TypedBinding -> Telescope1
    forall a b. (a -> b) -> a -> b
    $ Range
    -> Maybe Expr
    -> List1 (Arg (Named (WithOrigin (Ranged String)) Binder))
    -> Expr
    -> TypedBinding
    TBind Range
    forall a. Range' a
    noRange Maybe Expr
    tac List1 (Arg (Named (WithOrigin (Ranged String)) Binder))
    xs Expr
    a') Expr
    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
              Bool
    df <- (TCEnv -> Bool) -> m Bool
    forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
    asksTC TCEnv -> Bool
    envPrintDomainFreePi
              Bool -> m Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Bool -> m Bool) -> Bool -> m Bool
    forall a b. (a -> b) -> a -> b
    $ Bool
    df Bool -> Bool -> Bool
    && Nat -> a -> Bool
    forall a. Free a => Nat -> a -> Bool
    freeIn Nat
    0 a
    b Bool -> Bool -> Bool
    && t -> Bool
    forall t. Free t => t -> Bool
    closed t
    a

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

              [Elim' Expr]
    es' <- Elims -> m (ReifiesTo Elims)
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    reify Elims
    es

              MetaVariable
    mv <- MetaId -> m MetaVariable
    forall (m :: * -> *).
    (MonadFail m, ReadTCState m) =>
    MetaId -> m MetaVariable
    lookupMeta MetaId
    x
              (Maybe (Substitution' Term)
    msub1,Telescope
    meta_tel,Maybe (Substitution' Term)
    msub2) <- do
                CheckpointId
    local_chkpt <- Lens' CheckpointId TCEnv -> m CheckpointId
    forall (m :: * -> *) a. MonadTCEnv m => Lens' a TCEnv -> m a
    viewTC Lens' CheckpointId TCEnv
    eCurrentCheckpoint
                (CheckpointId
    chkpt, Telescope
    tel, Maybe (Substitution' Term)
    msub2) <- MetaVariable
    -> (Range
        -> m (CheckpointId, Telescope, Maybe (Substitution' Term)))
    -> m (CheckpointId, Telescope, Maybe (Substitution' Term))
    forall (m :: * -> *) a c b.
    (MonadTCEnv m, ReadTCState m, LensClosure a c) =>
    c -> (a -> m b) -> m b
    enterClosure MetaVariable
    mv ((Range -> m (CheckpointId, Telescope, Maybe (Substitution' Term)))
     -> m (CheckpointId, Telescope, Maybe (Substitution' Term)))
    -> (Range
        -> m (CheckpointId, Telescope, Maybe (Substitution' Term)))
    -> m (CheckpointId, Telescope, Maybe (Substitution' Term))
    forall a b. (a -> b) -> a -> b
    $ \ Range
    _ ->
                                   (,,) (CheckpointId
     -> Telescope
     -> Maybe (Substitution' Term)
     -> (CheckpointId, Telescope, Maybe (Substitution' Term)))
    -> m CheckpointId
    -> m (Telescope
          -> Maybe (Substitution' Term)
          -> (CheckpointId, Telescope, Maybe (Substitution' Term)))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Lens' CheckpointId TCEnv -> m CheckpointId
    forall (m :: * -> *) a. MonadTCEnv m => Lens' a TCEnv -> m a
    viewTC Lens' CheckpointId TCEnv
    eCurrentCheckpoint
                                        m (Telescope
       -> Maybe (Substitution' Term)
       -> (CheckpointId, Telescope, Maybe (Substitution' Term)))
    -> m Telescope
    -> m (Maybe (Substitution' Term)
          -> (CheckpointId, Telescope, Maybe (Substitution' Term)))
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> m Telescope
    forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
    getContextTelescope
                                        m (Maybe (Substitution' Term)
       -> (CheckpointId, Telescope, Maybe (Substitution' Term)))
    -> m (Maybe (Substitution' Term))
    -> m (CheckpointId, Telescope, Maybe (Substitution' Term))
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Lens' (Maybe (Substitution' Term)) TCEnv
    -> m (Maybe (Substitution' Term))
    forall (m :: * -> *) a. MonadTCEnv m => Lens' a TCEnv -> m a
    viewTC ((Map CheckpointId (Substitution' Term)
     -> f (Map CheckpointId (Substitution' Term)))
    -> TCEnv -> f TCEnv
    Lens' (Map CheckpointId (Substitution' Term)) TCEnv
    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'
         (Maybe (Substitution' Term))
         (Map CheckpointId (Substitution' Term))
    forall k v. Ord k => k -> Lens' (Maybe v) (Map k v)
    key CheckpointId
    local_chkpt)
                (,,) (Maybe (Substitution' Term)
     -> Telescope
     -> Maybe (Substitution' Term)
     -> (Maybe (Substitution' Term), Telescope,
         Maybe (Substitution' Term)))
    -> m (Maybe (Substitution' Term))
    -> m (Telescope
          -> Maybe (Substitution' Term)
          -> (Maybe (Substitution' Term), Telescope,
              Maybe (Substitution' Term)))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Lens' (Maybe (Substitution' Term)) TCEnv
    -> m (Maybe (Substitution' Term))
    forall (m :: * -> *) a. MonadTCEnv m => Lens' a TCEnv -> m a
    viewTC ((Map CheckpointId (Substitution' Term)
     -> f (Map CheckpointId (Substitution' Term)))
    -> TCEnv -> f TCEnv
    Lens' (Map CheckpointId (Substitution' Term)) TCEnv
    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'
         (Maybe (Substitution' Term))
         (Map CheckpointId (Substitution' Term))
    forall k v. Ord k => k -> Lens' (Maybe v) (Map k v)
    key CheckpointId
    chkpt) m (Telescope
       -> Maybe (Substitution' Term)
       -> (Maybe (Substitution' Term), Telescope,
           Maybe (Substitution' Term)))
    -> m Telescope
    -> m (Maybe (Substitution' Term)
          -> (Maybe (Substitution' Term), Telescope,
              Maybe (Substitution' Term)))
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Telescope -> m Telescope
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Telescope
    tel m (Maybe (Substitution' Term)
       -> (Maybe (Substitution' Term), Telescope,
           Maybe (Substitution' Term)))
    -> m (Maybe (Substitution' Term))
    -> m (Maybe (Substitution' Term), Telescope,
          Maybe (Substitution' Term))
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Maybe (Substitution' Term) -> m (Maybe (Substitution' Term))
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Maybe (Substitution' Term)
    msub2

              Bool
    opt_show_ids <- m Bool
    forall (m :: * -> *). HasOptions m => m Bool
    showIdentitySubstitutions
              let
                  addNames :: [name] -> [Elim' a] -> [Elim' (Named name a)]
    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 (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 :: Permutation
    p = MetaVariable -> Permutation
    mvPermutation MetaVariable
    mv
                  applyPerm :: Permutation -> [a] -> [a]
    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 :: [WithOrigin (Ranged String)]
    names = (String -> WithOrigin (Ranged String))
    -> [String] -> [WithOrigin (Ranged String)]
    forall a b. (a -> b) -> [a] -> [b]
    map (Origin -> Ranged String -> WithOrigin (Ranged String)
    forall a. Origin -> a -> WithOrigin a
    WithOrigin Origin
    Inserted (Ranged String -> WithOrigin (Ranged String))
    -> (String -> Ranged String)
    -> String
    -> WithOrigin (Ranged String)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . String -> Ranged String
    forall a. a -> Ranged a
    unranged) ([String] -> [WithOrigin (Ranged String)])
    -> [String] -> [WithOrigin (Ranged String)]
    forall a b. (a -> b) -> a -> b
    $ Permutation
    p Permutation -> [String] -> [String]
    forall a. Permutation -> [a] -> [a]
    `applyPerm` Telescope -> [String]
    teleNames Telescope
    meta_tel
                  named_es' :: [Elim' (Named_ Expr)]
    named_es' = [WithOrigin (Ranged String)]
    -> [Elim' Expr] -> [Elim' (Named_ Expr)]
    forall {name} {a}. [name] -> [Elim' a] -> [Elim' (Named name a)]
    addNames [WithOrigin (Ranged String)]
    names [Elim' Expr]
    es'

                  dropIdentitySubs :: Substitution' Term -> Substitution' Term -> [Elim' (Named_ Expr)]
    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` (Telescope -> Args
    forall a t. DeBruijn a => Tele (Dom t) -> [Arg a]
    teleArgs Telescope
    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 String)] -> Nat
    forall a. Sized a => a -> Nat
    size [WithOrigin (Ranged String)]
    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' :: [Elim' (Named_ Expr)]
    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'

              Expr -> [Elim' (Named_ Expr)] -> m Expr
    forall (m :: * -> *).
    MonadReify m =>
    Expr -> [Elim' (Named_ Expr)] -> m Expr
    nelims Expr
    x' [Elim' (Named_ Expr)]
    simpl_named_es'

        I.DontCare Term
    v -> do
          Bool
    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 | Bool
    showIrr   -> Bool -> Term -> m Expr
    forall (m :: * -> *). MonadReify m => Bool -> Term -> m Expr
    reifyTerm Bool
    expandAnonDefs Term
    v
             | Bool
    otherwise -> Expr -> m Expr
    forall (m :: * -> *) a. Monad m => a -> m a
    return Expr
    forall a. Underscore a => a
    underscore
        I.Dummy String
    s [] -> Expr -> m Expr
    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 (String -> Text
    T.pack String
    s)
        I.Dummy String
    "applyE" Elims
    es | I.Apply (Arg ArgInfo
    _ Term
    h) : Elims
    es' <- Elims
    es -> do
                                Expr
    h <- Term -> m (ReifiesTo Term)
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    reify Term
    h
                                [Elim' Expr]
    es' <- Elims -> m (ReifiesTo Elims)
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    reify Elims
    es'
                                Expr -> [Elim' Expr] -> m Expr
    forall (m :: * -> *).
    MonadReify m =>
    Expr -> [Elim' Expr] -> m Expr
    elims Expr
    h [Elim' Expr]
    es'
                            | Bool
    otherwise -> m Expr
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        I.Dummy String
    s Elims
    es -> do
          Expr
    s <- Term -> m (ReifiesTo Term)
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    reify (String -> Elims -> Term
    I.Dummy String
    s [])
          [Elim' Expr]
    es <- Elims -> m (ReifiesTo Elims)
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    reify Elims
    es
          Expr -> [Elim' Expr] -> m Expr
    forall (m :: * -> *).
    MonadReify m =>
    Expr -> [Elim' Expr] -> m Expr
    elims Expr
    s [Elim' Expr]
    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
          Reduced () Term
    r <- QName -> Elims -> m (Reduced () Term)
    forall (m :: * -> *).
    PureTCM m =>
    QName -> Elims -> m (Reduced () Term)
    reduceDefCopy QName
    x Elims
    es
          case Reduced () Term
    r of
            YesReduction Simplification
    _ Term
    v -> do
              String -> Nat -> [String] -> m ()
    forall a (m :: * -> *).
    (ReportS a, MonadDebug m) =>
    String -> Nat -> a -> m ()
    reportS String
    "reify.anon" Nat
    60
                [ String
    "reduction on defined ident. in anonymous module"
                , String
    "x = " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ QName -> String
    forall a. Pretty a => a -> String
    prettyShow QName
    x
                , String
    "v = " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Term -> String
    forall a. Show a => a -> String
    show Term
    v
                ]
              Term -> m (ReifiesTo Term)
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    reify Term
    v
            NoReduction () -> do
              String -> Nat -> [String] -> m ()
    forall a (m :: * -> *).
    (ReportS a, MonadDebug m) =>
    String -> Nat -> a -> m ()
    reportS String
    "reify.anon" Nat
    60
                [ String
    "no reduction on defined ident. in anonymous module"
                , String
    "x  = " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ QName -> String
    forall a. Pretty a => a -> String
    prettyShow QName
    x
                , String
    "es = " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Elims -> String
    forall a. Show a => a -> String
    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
          String -> Nat -> String -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Nat -> String -> m ()
    reportSLn String
    "reify.def" Nat
    60 (String -> m ()) -> String -> m ()
    forall a b. (a -> b) -> a -> b
    $ String
    "reifying call to " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ QName -> String
    forall a. Pretty a => a -> String
    prettyShow QName
    x
          -- We should drop this many arguments from the local context.
          Nat
    n <- QName -> m Nat
    forall (m :: * -> *).
    (Functor m, Applicative m, ReadTCState m, MonadTCEnv m) =>
    QName -> m Nat
    getDefFreeVars QName
    x
          String -> Nat -> String -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Nat -> String -> m ()
    reportSLn String
    "reify.def" Nat
    70 (String -> m ()) -> String -> m ()
    forall a b. (a -> b) -> a -> b
    $ String
    "freeVars for " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ QName -> String
    forall a. Pretty a => a -> String
    prettyShow QName
    x String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " = " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Nat -> String
    forall a. Show a => a -> String
    show Nat
    n
          -- If the definition is not (yet) in the signature,
          -- we just do the obvious.
          let fallback :: SigError -> m Expr
    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)
    reify (Nat -> Elims -> Elims
    forall a. Nat -> [a] -> [a]
    drop Nat
    n Elims
    es)
          m (Either SigError Definition)
    -> (SigError -> m Expr) -> (Definition -> m Expr) -> m Expr
    forall (m :: * -> *) a b c.
    Monad m =>
    m (Either a b) -> (a -> m c) -> (b -> m c) -> m c
    caseEitherM (QName -> m (Either SigError Definition)
    forall (m :: * -> *).
    HasConstInfo m =>
    QName -> m (Either SigError Definition)
    getConstInfo' QName
    x) SigError -> m Expr
    fallback ((Definition -> m Expr) -> m Expr)
    -> (Definition -> m Expr) -> m Expr
    forall a b. (a -> b) -> a -> b
    $ \ 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 (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 (t :: * -> *) a. Foldable t => t a -> Nat
    length Elims
    es -> do -- We don't have all arguments before the absurd one!
                            let name :: DeBruijnPattern -> String
    name (I.VarP PatternInfo
    _ DBPatVar
    x) = String -> String
    patVarNameToString (String -> String) -> String -> String
    forall a b. (a -> b) -> a -> b
    $ DBPatVar -> String
    dbPatVarName DBPatVar
    x
                                name DeBruijnPattern
    _            = String
    forall a. HasCallStack => a
    __IMPOSSIBLE__  -- only variables before absurd pattern
                                vars :: [(ArgInfo, String)]
    vars = (NamedArg DeBruijnPattern -> (ArgInfo, String))
    -> [NamedArg DeBruijnPattern] -> [(ArgInfo, String)]
    forall a b. (a -> b) -> [a] -> [b]
    map (NamedArg DeBruijnPattern -> ArgInfo
    forall a. LensArgInfo a => a -> ArgInfo
    getArgInfo (NamedArg DeBruijnPattern -> ArgInfo)
    -> (NamedArg DeBruijnPattern -> String)
    -> NamedArg DeBruijnPattern
    -> (ArgInfo, String)
    forall (a :: * -> * -> *) b c c'.
    Arrow a =>
    a b c -> a b c' -> a b (c, c')
    &&& DeBruijnPattern -> String
    name (DeBruijnPattern -> String)
    -> (NamedArg DeBruijnPattern -> DeBruijnPattern)
    -> NamedArg DeBruijnPattern
    -> String
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . NamedArg DeBruijnPattern -> DeBruijnPattern
    forall a. NamedArg a -> a
    namedArg) ([NamedArg DeBruijnPattern] -> [(ArgInfo, String)])
    -> [NamedArg DeBruijnPattern] -> [(ArgInfo, String)]
    forall a b. (a -> b) -> a -> b
    $ Nat -> [NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern]
    forall a. Nat -> [a] -> [a]
    drop (Elims -> 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
                                  Name
    x <- a -> m Name
    forall a (m :: * -> *).
    (FreshName a, MonadFresh NameId m) =>
    a -> m Name
    freshName_ a
    s
                                  (Expr -> Expr) -> m (Expr -> Expr)
    forall (m :: * -> *) a. Monad m => a -> m a
    return ((Expr -> Expr) -> m (Expr -> Expr))
    -> (Expr -> Expr) -> m (Expr -> Expr)
    forall a b. (a -> b) -> a -> b
    $ ExprInfo -> LamBinding -> Expr -> Expr
    A.Lam ExprInfo
    exprNoRange (Arg (Named (WithOrigin (Ranged String)) Binder) -> LamBinding
    A.mkDomainFree (Arg (Named (WithOrigin (Ranged String)) Binder) -> LamBinding)
    -> Arg (Named (WithOrigin (Ranged String)) Binder) -> LamBinding
    forall a b. (a -> b) -> a -> b
    $ ArgInfo
    -> Binder -> Arg (Named (WithOrigin (Ranged String)) Binder)
    forall a. ArgInfo -> a -> NamedArg a
    unnamedArg ArgInfo
    i (Binder -> Arg (Named (WithOrigin (Ranged String)) Binder))
    -> Binder -> Arg (Named (WithOrigin (Ranged String)) Binder)
    forall a b. (a -> b) -> a -> b
    $ Name -> Binder
    A.mkBinder_ Name
    x)
                            ((Expr -> Expr) -> Expr -> Expr) -> Expr -> [Expr -> Expr] -> Expr
    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, String) -> m (Expr -> Expr))
    -> [(ArgInfo, String)] -> m [Expr -> Expr]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM (ArgInfo, String) -> m (Expr -> Expr)
    forall {m :: * -> *} {a}.
    (FreshName a, MonadFresh NameId m) =>
    (ArgInfo, a) -> m (Expr -> Expr)
    lam [(ArgInfo, String)]
    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)
    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.
            Bool
    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!
            [QName]
    alreadyPrinting <- Lens' [QName] TCEnv -> m [QName]
    forall (m :: * -> *) a. MonadTCEnv m => Lens' a TCEnv -> m a
    viewTC Lens' [QName] TCEnv
    ePrintingPatternLambdas

            Maybe (Nat, Maybe System)
    extLam <- case Defn
    def of
              Function{ funExtLam :: Defn -> Maybe ExtLamInfo
    funExtLam = Just{}, funProjection :: Defn -> Maybe Projection
    funProjection = Just{} } -> 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))
    -> (Telescope -> (Nat, Maybe System))
    -> Telescope
    -> Maybe (Nat, Maybe System)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (,Maybe System -> Maybe System
    forall a. Maybe a -> Maybe a
    Strict.toLazy Maybe System
    sys) (Nat -> (Nat, Maybe System))
    -> (Telescope -> Nat) -> Telescope -> (Nat, Maybe System)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Telescope -> Nat
    forall a. Sized a => a -> Nat
    size (Telescope -> Maybe (Nat, Maybe System))
    -> m Telescope -> m (Maybe (Nat, Maybe System))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ModuleName -> m Telescope
    forall (m :: * -> *).
    (Functor m, ReadTCState m) =>
    ModuleName -> m Telescope
    lookupSection ModuleName
    m
              Defn
    _ -> Maybe (Nat, Maybe System) -> m (Maybe (Nat, Maybe System))
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe (Nat, Maybe System)
    forall a. Maybe a
    Nothing
            case Maybe (Nat, Maybe System)
    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' [QName] TCEnv -> ([QName] -> [QName]) -> m Expr -> m Expr
    forall (m :: * -> *) a b.
    MonadTCEnv m =>
    Lens' a TCEnv -> (a -> a) -> m b -> m b
    locallyTC Lens' [QName] TCEnv
    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
                  (Definition -> [Clause]
    defClauses Definition
    defn) Elims
    es

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

                Function{ funProjection :: Defn -> Maybe Projection
    funProjection = Just Projection{ projIndex :: Projection -> Nat
    projIndex = Nat
    np } } | Nat
    np Nat -> Nat -> Bool
    forall a. Ord a => a -> a -> Bool
    > Nat
    0 -> do
                  String -> Nat -> String -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Nat -> String -> m ()
    reportSLn String
    "reify.def" Nat
    70 (String -> m ()) -> String -> m ()
    forall a b. (a -> b) -> a -> b
    $ String
    "  def. is a projection with projIndex = " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Nat -> String
    forall a. Show a => a -> String
    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 Telescope
    tel Type
    _ <- 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 ([Dom (String, Type)]
    as, [Dom (String, Type)]
    rest) = Nat
    -> [Dom (String, Type)]
    -> ([Dom (String, Type)], [Dom (String, Type)])
    forall a. Nat -> [a] -> ([a], [a])
    splitAt (Nat
    np Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    - Nat
    1) ([Dom (String, Type)]
     -> ([Dom (String, Type)], [Dom (String, Type)]))
    -> [Dom (String, Type)]
    -> ([Dom (String, Type)], [Dom (String, Type)])
    forall a b. (a -> b) -> a -> b
    $ Telescope -> [Dom (String, Type)]
    forall t. Tele (Dom t) -> [Dom (String, t)]
    telToList Telescope
    tel
                      dom :: Dom (String, Type)
    dom = Dom (String, Type) -> [Dom (String, Type)] -> Dom (String, Type)
    forall a. a -> [a] -> a
    headWithDefault Dom (String, Type)
    forall a. HasCallStack => a
    __IMPOSSIBLE__ [Dom (String, Type)]
    rest

                  -- These are the dropped projection arguments
                  ScopeInfo
    scope <- m ScopeInfo
    forall (m :: * -> *). ReadTCState m => m ScopeInfo
    getScope
                  let underscore :: Expr
    underscore = MetaInfo -> Expr
    A.Underscore (MetaInfo -> Expr) -> MetaInfo -> Expr
    forall a b. (a -> b) -> a -> b
    $ MetaInfo
    Info.emptyMetaInfo { metaScope :: ScopeInfo
    metaScope = ScopeInfo
    scope }
                  let pad :: [NamedArg Expr]
                      pad :: [Arg (Named_ Expr)]
    pad = [Dom (String, Type)]
    -> (Dom (String, Type) -> Arg (Named_ Expr)) -> [Arg (Named_ Expr)]
    forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
    for [Dom (String, Type)]
    as ((Dom (String, Type) -> Arg (Named_ Expr)) -> [Arg (Named_ Expr)])
    -> (Dom (String, 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 = (String
    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 String)) -> Expr -> Named_ Expr
    forall name a. Maybe name -> a -> Named name a
    Named (WithOrigin (Ranged String) -> Maybe (WithOrigin (Ranged String))
    forall a. a -> Maybe a
    Just (WithOrigin (Ranged String) -> Maybe (WithOrigin (Ranged String)))
    -> WithOrigin (Ranged String) -> Maybe (WithOrigin (Ranged String))
    forall a b. (a -> b) -> a -> b
    $ Origin -> Ranged String -> WithOrigin (Ranged String)
    forall a. Origin -> a -> WithOrigin a
    WithOrigin Origin
    Inserted (Ranged String -> WithOrigin (Ranged String))
    -> Ranged String -> WithOrigin (Ranged String)
    forall a b. (a -> b) -> a -> b
    $ String -> Ranged String
    forall a. a -> Ranged a
    unranged String
    x) Expr
    underscore
                          -- TODO #3353 Origin from Dom?

                  -- Now pad' ++ es' = drop n (pad ++ es)
                  let pad' :: [Arg (Named_ Expr)]
    pad' = Nat -> [Arg (Named_ Expr)] -> [Arg (Named_ Expr)]
    forall a. Nat -> [a] -> [a]
    drop Nat
    n [Arg (Named_ Expr)]
    pad
                      es' :: Elims
    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.
                  Bool
    showImp <- m Bool
    forall (m :: * -> *). HasOptions m => m Bool
    showImplicitArguments

                  -- Get the visible arguments of the padding and the rest
                  -- after the last visible argument.
                  let ([Arg (Named_ Expr)]
    padVisNamed, [Arg (Named_ Expr)]
    padRest) = (Arg (Named_ Expr) -> Bool)
    -> [Arg (Named_ Expr)]
    -> ([Arg (Named_ Expr)], [Arg (Named_ Expr)])
    forall a. (a -> Bool) -> [a] -> ([a], [a])
    filterAndRest Arg (Named_ Expr) -> Bool
    forall a. LensHiding a => a -> Bool
    visible [Arg (Named_ Expr)]
    pad'

                  -- Remove the names from the visible arguments.
                  let padVis :: [Arg (Named_ Expr)]
    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 (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)]
    padTail = (Arg (Named_ Expr) -> Bool)
    -> [Arg (Named_ Expr)] -> [Arg (Named_ Expr)]
    forall a. (a -> Bool) -> [a] -> [a]
    filter (Dom (String, Type) -> Arg (Named_ Expr) -> Bool
    forall a b. (LensHiding a, LensHiding b) => a -> b -> Bool
    sameHiding Dom (String, Type)
    dom) [Arg (Named_ Expr)]
    padRest

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

                  ([Arg (Named_ Expr)], [Elim' (Named_ Term)])
    -> m ([Arg (Named_ Expr)], [Elim' (Named_ Term)])
    forall (m :: * -> *) a. Monad m => a -> m a
    return (([Arg (Named_ Expr)], [Elim' (Named_ Term)])
     -> m ([Arg (Named_ Expr)], [Elim' (Named_ Term)]))
    -> ([Arg (Named_ Expr)], [Elim' (Named_ Term)])
    -> m ([Arg (Named_ Expr)], [Elim' (Named_ Term)])
    forall a b. (a -> b) -> a -> b
    $ if [Arg (Named_ Expr)] -> Bool
    forall a. Null a => a -> Bool
    null [Arg (Named_ Expr)]
    padTail Bool -> Bool -> Bool
    || Bool -> Bool
    not Bool
    showImp
                    then ([Arg (Named_ Expr)]
    padVis           , (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 (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Term -> Named_ Term
    forall a name. a -> Named name a
    unnamed) Elims
    es')
                    else ([Arg (Named_ Expr)]
    padVis [Arg (Named_ Expr)] -> [Arg (Named_ Expr)] -> [Arg (Named_ Expr)]
    forall a. [a] -> [a] -> [a]
    ++ [Arg (Named_ Expr)]
    padSame, Dom (String, Type) -> Elims -> [Elim' (Named_ Term)]
    forall t a. Dom (String, t) -> [Elim' a] -> [Elim' (Named_ a)]
    nameFirstIfHidden Dom (String, Type)
    dom Elims
    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 (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 (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)

               String -> Nat -> TCM Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Nat -> TCM Doc -> m ()
    reportSDoc String
    "reify.def" Nat
    100 (TCM Doc -> m ()) -> TCM Doc -> m ()
    forall a b. (a -> b) -> a -> b
    $ Doc -> TCM Doc
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Doc -> TCM Doc) -> Doc -> TCM Doc
    forall a b. (a -> b) -> a -> b
    $ [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    vcat
                 [ Doc
    "  pad =" Doc -> Doc -> Doc
    <+> [Arg (Named_ Expr)] -> Doc
    forall a. Show a => a -> Doc
    pshow [Arg (Named_ Expr)]
    pad
                 , Doc
    "  nes =" Doc -> Doc -> Doc
    <+> [Elim' (Named_ Term)] -> Doc
    forall a. Show a => a -> Doc
    pshow [Elim' (Named_ Term)]
    nes
                 ]
               let hd0 :: Expr
    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
    hd = (Expr -> Arg (Named_ Expr) -> Expr)
    -> Expr -> [Arg (Named_ Expr)] -> Expr
    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
               Expr -> [Elim' (Named_ Expr)] -> m Expr
    forall (m :: * -> *).
    MonadReify m =>
    Expr -> [Elim' (Named_ Expr)] -> m Expr
    nelims Expr
    hd ([Elim' (Named_ Expr)] -> m Expr)
    -> m [Elim' (Named_ Expr)] -> m Expr
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< [Elim' (Named_ Term)] -> m (ReifiesTo [Elim' (Named_ Term)])
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    reify [Elim' (Named_ Term)]
    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
    i Nat
    npars Maybe System
    msys [Clause]
    cls Elims
    es = do
          String -> Nat -> String -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Nat -> String -> m ()
    reportSLn String
    "reify.def" Nat
    10 (String -> m ()) -> String -> m ()
    forall a b. (a -> b) -> a -> b
    $ String
    "reifying extended lambda " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ QName -> String
    forall a. Pretty a => a -> String
    prettyShow QName
    x
          String -> Nat -> String -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Nat -> String -> m ()
    reportSLn String
    "reify.def" Nat
    50 (String -> m ()) -> String -> m ()
    forall a b. (a -> b) -> a -> b
    $ Doc -> String
    render (Doc -> String) -> Doc -> String
    forall a b. (a -> b) -> a -> b
    $ Nat -> Doc -> Doc
    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
    <+> Nat -> Doc
    forall a. Pretty a => a -> Doc
    pretty Nat
    npars
            , Doc
    "es    =" Doc -> Doc -> Doc
    <+> [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
    <+> [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@).
          [Clause]
    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)
    mapM (NamedClause -> m Clause
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    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]
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    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
    cx     = Name -> Name
    nameConcrete (Name -> Name) -> Name -> Name
    forall a b. (a -> b) -> a -> b
    $ QName -> Name
    qnameName QName
    x
              dInfo :: DefInfo' Expr
    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 :: Erased
    erased = case ArgInfo -> Quantity
    forall a. LensQuantity a => a -> Quantity
    getQuantity ArgInfo
    i 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__
          Expr -> [Elim' Expr] -> m Expr
    forall (m :: * -> *).
    MonadReify m =>
    Expr -> [Elim' Expr] -> m Expr
    elims (ExprInfo
    -> DefInfo' Expr -> Erased -> QName -> List1 Clause -> Expr
    A.ExtendedLam ExprInfo
    exprNoRange DefInfo' Expr
    dInfo Erased
    erased QName
    x (List1 Clause -> Expr) -> List1 Clause -> Expr
    forall a b. (a -> b) -> a -> b
    $
                 [Clause] -> List1 Clause
    forall a. [a] -> NonEmpty a
    List1.fromList [Clause]
    cls)
            ([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)
    reify Elims
    rest

    -- | @nameFirstIfHidden (x:a) ({e} es) = {x = e} es@
    nameFirstIfHidden :: Dom (ArgName, t) -> [Elim' a] -> [Elim' (Named_ a)]
    nameFirstIfHidden :: forall t a. Dom (String, t) -> [Elim' a] -> [Elim' (Named_ a)]
    nameFirstIfHidden Dom (String, 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 (WithOrigin (Ranged String)) a)
    -> Elim' (Named (WithOrigin (Ranged String)) a)
    forall a. Arg a -> Elim' a
    I.Apply (ArgInfo
    -> Named (WithOrigin (Ranged String)) a
    -> Arg (Named (WithOrigin (Ranged String)) a)
    forall e. ArgInfo -> e -> Arg e
    Arg ArgInfo
    info (Maybe (WithOrigin (Ranged String))
    -> a -> Named (WithOrigin (Ranged String)) a
    forall name a. Maybe name -> a -> Named name a
    Named (WithOrigin (Ranged String) -> Maybe (WithOrigin (Ranged String))
    forall a. a -> Maybe a
    Just (WithOrigin (Ranged String) -> Maybe (WithOrigin (Ranged String)))
    -> WithOrigin (Ranged String) -> Maybe (WithOrigin (Ranged String))
    forall a b. (a -> b) -> a -> b
    $ Origin -> Ranged String -> WithOrigin (Ranged String)
    forall a. Origin -> a -> WithOrigin a
    WithOrigin Origin
    Inserted (Ranged String -> WithOrigin (Ranged String))
    -> Ranged String -> WithOrigin (Ranged String)
    forall a b. (a -> b) -> a -> b
    $ String -> Ranged String
    forall a. a -> Ranged a
    unranged (String -> Ranged String) -> String -> Ranged String
    forall a b. (a -> b) -> a -> b
    $ (String, t) -> String
    forall a b. (a, b) -> a
    fst ((String, t) -> String) -> (String, t) -> String
    forall a b. (a -> b) -> a -> b
    $ Dom (String, t) -> (String, t)
    forall t e. Dom' t e -> e
    unDom Dom (String, t)
    dom) a
    e)) Elim' (Named (WithOrigin (Ranged String)) a)
    -> [Elim' (Named (WithOrigin (Ranged String)) a)]
    -> [Elim' (Named (WithOrigin (Ranged String)) a)]
    forall a. a -> [a] -> [a]
    :
      (Elim' a -> Elim' (Named (WithOrigin (Ranged String)) a))
    -> [Elim' a] -> [Elim' (Named (WithOrigin (Ranged String)) a)]
    forall a b. (a -> b) -> [a] -> [b]
    map ((a -> Named (WithOrigin (Ranged String)) a)
    -> Elim' a -> Elim' (Named (WithOrigin (Ranged String)) a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap a -> Named (WithOrigin (Ranged String)) a
    forall a name. a -> Named name a
    unnamed) [Elim' a]
    es
    nameFirstIfHidden Dom (String, t)
    _ [Elim' a]
    es =
      (Elim' a -> Elim' (Named (WithOrigin (Ranged String)) a))
    -> [Elim' a] -> [Elim' (Named (WithOrigin (Ranged String)) a)]
    forall a b. (a -> b) -> [a] -> [b]
    map ((a -> Named (WithOrigin (Ranged String)) a)
    -> Elim' a -> Elim' (Named (WithOrigin (Ranged String)) a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap a -> Named (WithOrigin (Ranged String)) 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)
    traverse i -> m (ReifiesTo i)
    forall i (m :: * -> *).
    (Reify i, 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)
    traverse (Bool -> i -> m (ReifiesTo i)
    forall i (m :: * -> *).
    (Reify i, 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)
    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 (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 (m :: * -> *) a. Monad m => a -> m a
    return (ArgInfo -> Relevance
    forall a. LensRelevance a => a -> Relevance
    getRelevance ArgInfo
    info Relevance -> Relevance -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Relevance
    Irrelevant) 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)
    traverse (Bool -> i -> m (ReifiesTo i)
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    Bool -> i -> m (ReifiesTo i)
    reifyWhen Bool
    b) Arg i
    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

    -- | 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 => A.Patterns -> A.Patterns -> m A.Patterns
    stripImplicits :: forall (m :: * -> *).
    MonadReify m =>
    Patterns -> Patterns -> m Patterns
    stripImplicits 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 (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 (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
        String -> Nat -> TCM Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Nat -> TCM Doc -> m ()
    reportSDoc String
    "reify.implicit" Nat
    100 (TCM Doc -> m ()) -> TCM Doc -> m ()
    forall a b. (a -> b) -> a -> b
    $ Doc -> TCM Doc
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Doc -> TCM Doc) -> Doc -> TCM Doc
    forall a b. (a -> b) -> a -> b
    $ [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    vcat
          [ Doc
    "stripping implicits"
          , Nat -> Doc -> Doc
    nest Nat
    2 (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ Doc
    "ps   =" Doc -> Doc -> Doc
    <+> 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
    forall {e}. [NamedArg (Pattern' e)] -> [NamedArg (Pattern' e)]
    strip Patterns
    ps
        String -> Nat -> TCM Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Nat -> TCM Doc -> m ()
    reportSDoc String
    "reify.implicit" Nat
    100 (TCM Doc -> m ()) -> TCM Doc -> m ()
    forall a b. (a -> b) -> a -> b
    $ Doc -> TCM Doc
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Doc -> TCM Doc) -> Doc -> TCM Doc
    forall a b. (a -> b) -> a -> b
    $ [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    vcat
          [ Nat -> Doc -> Doc
    nest Nat
    2 (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ Doc
    "ps'  =" Doc -> Doc -> Doc
    <+> Patterns -> Doc
    forall a. Show a => a -> Doc
    pshow Patterns
    ps'
          ]
        Patterns -> m Patterns
    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 :: [NamedArg (Pattern' e)] -> [NamedArg (Pattern' e)]
    strip [NamedArg (Pattern' e)]
    ps = Bool -> [NamedArg (Pattern' e)] -> [NamedArg (Pattern' e)]
    forall {e}.
    Bool -> [NamedArg (Pattern' e)] -> [NamedArg (Pattern' e)]
    stripArgs Bool
    True [NamedArg (Pattern' e)]
    ps
            where
              stripArgs :: Bool -> [NamedArg (Pattern' e)] -> [NamedArg (Pattern' e)]
    stripArgs Bool
    _ [] = []
              stripArgs Bool
    fixedPos (NamedArg (Pattern' e)
    a : [NamedArg (Pattern' e)]
    as)
                -- A hidden non-UserWritten variable is removed if not needed for
                -- correct position of the following hidden arguments.
                | NamedArg (Pattern' e) -> Bool
    forall {e}. NamedArg (Pattern' e) -> Bool
    canStrip NamedArg (Pattern' e)
    a =
                     if   (NamedArg (Pattern' e) -> Bool) -> [NamedArg (Pattern' e)] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all NamedArg (Pattern' e) -> Bool
    forall {e}. NamedArg (Pattern' e) -> Bool
    canStrip ([NamedArg (Pattern' e)] -> Bool)
    -> [NamedArg (Pattern' e)] -> Bool
    forall a b. (a -> b) -> a -> b
    $ (NamedArg (Pattern' e) -> Bool)
    -> [NamedArg (Pattern' e)] -> [NamedArg (Pattern' e)]
    forall a. (a -> Bool) -> [a] -> [a]
    takeWhile NamedArg (Pattern' e) -> Bool
    forall {a}. (LensHiding a, LensNamed a, IsProjP a) => a -> Bool
    isUnnamedHidden [NamedArg (Pattern' e)]
    as
                     then Bool -> [NamedArg (Pattern' e)] -> [NamedArg (Pattern' e)]
    stripArgs Bool
    False [NamedArg (Pattern' e)]
    as
                     else [NamedArg (Pattern' e)]
    goWild
                -- Other arguments are kept.
                | Bool
    otherwise = Bool -> NamedArg (Pattern' e) -> NamedArg (Pattern' e)
    forall {f :: * -> *} {b}.
    (Functor f, LensNamed b, LensOrigin (NameOf b)) =>
    Bool -> f b -> f b
    stripName Bool
    fixedPos (NamedArg (Pattern' e) -> NamedArg (Pattern' e)
    stripArg NamedArg (Pattern' e)
    a) NamedArg (Pattern' e)
    -> [NamedArg (Pattern' e)] -> [NamedArg (Pattern' e)]
    forall a. a -> [a] -> [a]
    : Bool -> [NamedArg (Pattern' e)] -> [NamedArg (Pattern' e)]
    stripArgs Bool
    True [NamedArg (Pattern' e)]
    as
                where
                  a' :: NamedArg (Pattern' e)
    a'     = NamedArg (Pattern' e) -> Pattern' e -> NamedArg (Pattern' e)
    forall a b. NamedArg a -> b -> NamedArg b
    setNamedArg NamedArg (Pattern' e)
    a (Pattern' e -> NamedArg (Pattern' e))
    -> Pattern' e -> NamedArg (Pattern' e)
    forall a b. (a -> b) -> a -> b
    $ PatInfo -> Pattern' e
    forall e. PatInfo -> Pattern' e
    A.WildP (PatInfo -> Pattern' e) -> PatInfo -> Pattern' e
    forall a b. (a -> b) -> a -> b
    $ Range -> PatInfo
    Info.PatRange (Range -> PatInfo) -> Range -> PatInfo
    forall a b. (a -> b) -> a -> b
    $ NamedArg (Pattern' e) -> Range
    forall a. HasRange a => a -> Range
    getRange NamedArg (Pattern' e)
    a
                  goWild :: [NamedArg (Pattern' e)]
    goWild = Bool -> NamedArg (Pattern' e) -> NamedArg (Pattern' e)
    forall {f :: * -> *} {b}.
    (Functor f, LensNamed b, LensOrigin (NameOf b)) =>
    Bool -> f b -> f b
    stripName Bool
    fixedPos NamedArg (Pattern' e)
    a' NamedArg (Pattern' e)
    -> [NamedArg (Pattern' e)] -> [NamedArg (Pattern' e)]
    forall a. a -> [a] -> [a]
    : Bool -> [NamedArg (Pattern' e)] -> [NamedArg (Pattern' e)]
    stripArgs Bool
    True [NamedArg (Pattern' e)]
    as

              stripName :: Bool -> f b -> f b
    stripName Bool
    True  = (b -> b) -> f b -> 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 :: NamedArg (Pattern' e) -> Bool
    canStrip NamedArg (Pattern' e)
    a = [Bool] -> Bool
    forall (t :: * -> *). Foldable t => t Bool -> Bool
    and
                [ NamedArg (Pattern' e) -> Bool
    forall a. LensHiding a => a -> Bool
    notVisible NamedArg (Pattern' e)
    a
                , NamedArg (Pattern' e) -> Origin
    forall a. LensOrigin a => a -> Origin
    getOrigin NamedArg (Pattern' e)
    a Origin -> [Origin] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `notElem` [ Origin
    UserWritten , Origin
    CaseSplit ]
                , (WithOrigin (Ranged String) -> Origin
    forall a. LensOrigin a => a -> Origin
    getOrigin (WithOrigin (Ranged String) -> Origin)
    -> Maybe (WithOrigin (Ranged String)) -> Maybe Origin
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> NamedArg (Pattern' e) -> Maybe (NameOf (NamedArg (Pattern' e)))
    forall a. LensNamed a => a -> Maybe (NameOf a)
    getNameOf NamedArg (Pattern' e)
    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' e -> Bool
    forall {e}. Pattern' e -> Bool
    varOrDot (NamedArg (Pattern' e) -> Pattern' e
    forall a. NamedArg a -> a
    namedArg NamedArg (Pattern' e)
    a)
                ]

              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 :: NamedArg (Pattern' e) -> NamedArg (Pattern' e)
    stripArg NamedArg (Pattern' e)
    a = (Named_ (Pattern' e) -> Named_ (Pattern' e))
    -> NamedArg (Pattern' e) -> NamedArg (Pattern' e)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((Pattern' e -> Pattern' e)
    -> Named_ (Pattern' e) -> Named_ (Pattern' e)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Pattern' e -> Pattern' e
    stripPat) NamedArg (Pattern' e)
    a

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

              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

    -- | @blankNotInScope e@ replaces variables in expression @e@ with @_@
    -- if they are currently not in scope.
    blankNotInScope :: (MonadTCEnv m, BlankVars a) => a -> m a
    blankNotInScope :: forall (m :: * -> *) a. (MonadTCEnv m, BlankVars a) => a -> m a
    blankNotInScope a
    e = do
      Set Name
    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) -> m [Name] -> m (Set Name)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m [Name]
    forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m [Name]
    getContextNames
      a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (a -> m a) -> a -> m a
    forall a b. (a -> b) -> a -> b
    $ Set Name -> a -> a
    forall a. BlankVars a => Set Name -> a -> a
    blank Set Name
    names a
    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) -> f b -> f b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((b -> b) -> f b -> f b)
    -> (Set Name -> b -> b) -> Set Name -> f b -> f b
    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 Bool
    ca)
        | WhereDeclarations -> Bool
    forall a. Null a => a -> Bool
    null WhereDeclarations
    wh =
            LHS -> [ProblemEq] -> RHS -> WhereDeclarations -> Bool -> Clause
    forall lhs.
    lhs
    -> [ProblemEq] -> RHS -> WhereDeclarations -> Bool -> 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 Bool
    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 [Arg Pattern]
    wps Patterns
    ps) = ((LHSCore, [Arg Pattern]) -> Patterns -> LHSCore)
    -> ((LHSCore, [Arg Pattern]), Patterns) -> LHSCore
    forall a b c. (a -> b -> c) -> (a, b) -> c
    uncurry ((LHSCore -> [Arg Pattern] -> Patterns -> LHSCore)
    -> (LHSCore, [Arg Pattern]) -> Patterns -> LHSCore
    forall a b c. (a -> b -> c) -> (a, b) -> c
    uncurry LHSCore -> [Arg Pattern] -> Patterns -> LHSCore
    forall e.
    LHSCore' e
    -> [Arg (Pattern' e)] -> [NamedArg (Pattern' e)] -> LHSCore' e
    A.LHSWith) (((LHSCore, [Arg Pattern]), Patterns) -> LHSCore)
    -> ((LHSCore, [Arg Pattern]), Patterns) -> LHSCore
    forall a b. (a -> b) -> a -> b
    $ Set Name
    -> ((LHSCore, [Arg Pattern]), Patterns)
    -> ((LHSCore, [Arg Pattern]), Patterns)
    forall a. BlankVars a => Set Name -> a -> a
    blank Set Name
    bound ((LHSCore
    h, [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 PatInfo
    i [FieldAssignment' Pattern]
    fs   -> PatInfo -> [FieldAssignment' Pattern] -> Pattern
    forall e. PatInfo -> [FieldAssignment' (Pattern' e)] -> Pattern' e
    A.RecP PatInfo
    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)
        A.AnnP PatInfo
    i Expr
    a Pattern
    p  -> PatInfo -> Expr -> Pattern -> Pattern
    forall e. PatInfo -> e -> Pattern' e -> Pattern' e
    A.AnnP PatInfo
    i (Set Name -> Expr -> Expr
    forall a. BlankVars a => Set Name -> a -> a
    blank Set Name
    bound Expr
    a) (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 [Expr]
    es         -> (Expr -> [Expr] -> Expr) -> (Expr, [Expr]) -> Expr
    forall a b c. (a -> b -> c) -> (a, b) -> c
    uncurry (ExprInfo -> Expr -> [Expr] -> Expr
    A.WithApp ExprInfo
    i) ((Expr, [Expr]) -> Expr) -> (Expr, [Expr]) -> Expr
    forall a b. (a -> b) -> a -> b
    $ Set Name -> (Expr, [Expr]) -> (Expr, [Expr])
    forall a. BlankVars a => Set Name -> a -> a
    blank Set Name
    bound (Expr
    e, [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 ExprInfo
    i RecordAssigns
    es               -> ExprInfo -> RecordAssigns -> Expr
    A.Rec 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 ExprInfo
    i Expr
    e Assigns
    es       -> (Expr -> Assigns -> Expr) -> (Expr, Assigns) -> Expr
    forall a b c. (a -> b -> c) -> (a, b) -> c
    uncurry (ExprInfo -> Expr -> Assigns -> Expr
    A.RecUpdate 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.ETel Telescope
    _                 -> Expr
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        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
    _ [WithExpr]
    es [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 Maybe Expr
    t List1 (Arg (Named (WithOrigin (Ranged String)) Binder))
    n Expr
    e) = Range
    -> Maybe Expr
    -> List1 (Arg (Named (WithOrigin (Ranged String)) Binder))
    -> Expr
    -> TypedBinding
    TBind Range
    r Maybe Expr
    t List1 (Arg (Named (WithOrigin (Ranged String)) 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 (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 [Arg Pattern]
    wps Patterns
    ps) = ((LHSCore, [Arg Pattern]), Patterns) -> Set Name
    forall a. Binder a => a -> Set Name
    varsBoundIn ((LHSCore
    h, [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 PatInfo
    _ [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
        A.AnnP{}            -> 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 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 Maybe Expr
    _ Arg (Named (WithOrigin (Ranged String)) Binder)
    x) = Arg (Named (WithOrigin (Ranged String)) Binder) -> Set Name
    forall a. Binder a => a -> Set Name
    varsBoundIn Arg (Named (WithOrigin (Ranged String)) 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
    _ Maybe Expr
    _ List1 (Arg (Named (WithOrigin (Ranged String)) Binder))
    xs Expr
    _) = List1 (Arg (Named (WithOrigin (Ranged String)) Binder)) -> Set Name
    forall a. Binder a => a -> Set Name
    varsBoundIn List1 (Arg (Named (WithOrigin (Ranged String)) 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 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 (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
      varsBoundIn LetDeclaredVariable{} = 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

    -- | 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)
    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 (WithOrigin (Ranged String)) 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)
    traverse ((DeBruijnPattern -> m Pattern)
    -> Named (WithOrigin (Ranged String)) DeBruijnPattern
    -> m (Named_ Pattern)
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t 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 -> (String -> Bool) -> Maybe String -> Bool
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe Bool
    True ((Bool -> Bool -> Bool)
    -> (String -> Bool) -> (String -> Bool) -> String -> Bool
    forall (f :: * -> *) a b c.
    Applicative f =>
    (a -> b -> c) -> f a -> f b -> f c
    liftA2 Bool -> Bool -> Bool
    (||) String -> Bool
    forall a. Null a => a -> Bool
    null String -> Bool
    forall a. IsNoName a => a -> Bool
    isNoName) (NamedArg p -> Maybe String
    forall a.
    (LensNamed a, NameOf a ~ WithOrigin (Ranged String)) =>
    a -> Maybe String
    bareNameOf NamedArg p
    a) =
              (Named (WithOrigin (Ranged String)) p
     -> Named (WithOrigin (Ranged String)) p)
    -> NamedArg p -> NamedArg p
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (p -> Named (WithOrigin (Ranged String)) p
    forall a name. a -> Named name a
    unnamed (p -> Named (WithOrigin (Ranged String)) p)
    -> (Named (WithOrigin (Ranged String)) p -> p)
    -> Named (WithOrigin (Ranged String)) p
    -> Named (WithOrigin (Ranged String)) p
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Named (WithOrigin (Ranged String)) 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
         String -> Nat -> TCM Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Nat -> TCM Doc -> m ()
    reportSDoc String
    "reify.pat" Nat
    80 (TCM Doc -> m ()) -> TCM Doc -> m ()
    forall a b. (a -> b) -> a -> b
    $ Doc -> TCM Doc
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Doc -> TCM Doc) -> Doc -> TCM Doc
    forall a b. (a -> b) -> a -> b
    $ Doc
    "reifying pattern" Doc -> Doc -> Doc
    <+> DeBruijnPattern -> Doc
    forall a. Pretty a => a -> Doc
    pretty DeBruijnPattern
    p
         Bool
    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 DeBruijnPattern
    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 (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 (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 (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 (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 (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 (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
              Name
    x' <- Nat -> m Name
    forall (m :: * -> *).
    (Applicative m, MonadFail m, MonadTCEnv m) =>
    Nat -> m Name
    nameOfBV Nat
    i
              if Name -> Name
    nameConcrete Name
    x Name -> Name -> Bool
    forall a. Eq a => a -> a -> Bool
    == Name -> Name
    nameConcrete Name
    x' then
                Pattern -> m Pattern
    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'
              else
                PatOrigin -> Term -> m Pattern
    forall (m :: * -> *).
    MonadReify m =>
    PatOrigin -> Term -> m Pattern
    reifyDotP PatOrigin
    o Term
    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 (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 (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 (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 (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 (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 (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 (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 (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 (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 (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
          Name
    n <- Nat -> m Name
    forall (m :: * -> *).
    (Applicative m, MonadFail 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 :: String
    y = DBPatVar -> String
    dbPatVarName DBPatVar
    x
          if | String
    y String -> String -> Bool
    forall a. Eq a => a -> a -> Bool
    == String
    "_" -> Pattern -> m Pattern
    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
    n
               -- Andreas, 2017-09-03: TODO for #2580
               -- Patterns @VarP "()"@ should have been replaced by @AbsurdP@, but the
               -- case splitter still produces them.
             | Name -> String
    forall a. Pretty a => a -> String
    prettyShow (Name -> Name
    nameConcrete Name
    n) String -> String -> Bool
    forall a. Eq a => a -> a -> Bool
    == String
    "()" -> Pattern -> m Pattern
    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 (Name -> BindName
    mkBindName Name
    n)
               -- Andreas, 2017-09-03, issue #2729
               -- Restore original pattern name.  AbstractToConcrete picks unique names.
             | Bool
    otherwise -> Pattern -> m Pattern
    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
    n { nameConcrete :: Name
    nameConcrete = String -> Name
    C.simpleName String
    y }

        reifyDotP :: MonadReify m => PatOrigin -> Term -> m A.Pattern
        reifyDotP :: forall (m :: * -> *).
    MonadReify m =>
    PatOrigin -> Term -> m Pattern
    reifyDotP PatOrigin
    o Term
    v = do
          Bool
    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 Name
    x <- PatOrigin
    o , Bool
    keepVars       -> Pattern -> m Pattern
    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
             | Bool
    otherwise                       -> PatInfo -> Expr -> Pattern
    forall e. PatInfo -> e -> Pattern' e
    A.DotP PatInfo
    patNoRange (Expr -> Pattern) -> m Expr -> m Pattern
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Term -> m (ReifiesTo Term)
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    reify Term
    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 (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr ((Pattern -> Pattern) -> m Pattern -> m Pattern
    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

    -- | 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 (m :: * -> *) a. Monad m => a -> m a
    return Pattern
    p
      case Pattern
    p of
        A.ConP ConPatInfo
    ci AmbiguousQName
    c Patterns
    ps -> do
            String -> Nat -> String -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Nat -> String -> m ()
    reportSLn String
    "reify.pat" Nat
    60 (String -> m ()) -> String -> m ()
    forall a b. (a -> b) -> a -> b
    $ String
    "tryRecPFromConP " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ AmbiguousQName -> String
    forall a. Pretty a => a -> String
    prettyShow AmbiguousQName
    c
            m (Maybe (QName, Defn))
    -> m Pattern -> ((QName, Defn) -> 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, Defn))
    forall (m :: * -> *).
    HasConstInfo m =>
    QName -> m (Maybe (QName, Defn))
    isRecordConstructor (QName -> m (Maybe (QName, Defn)))
    -> QName -> m (Maybe (QName, Defn))
    forall a b. (a -> b) -> a -> b
    $ AmbiguousQName -> QName
    headAmbQ AmbiguousQName
    c) m Pattern
    fallback (((QName, Defn) -> m Pattern) -> m Pattern)
    -> ((QName, Defn) -> m Pattern) -> m Pattern
    forall a b. (a -> b) -> a -> b
    $ \ (QName
    r, Defn
    def) -> do
              -- If the record constructor is generated or the user wrote a record pattern,
              -- print record pattern.
              -- Otherwise, print constructor pattern.
              if Defn -> Bool
    recNamedCon Defn
    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
                [Dom Name]
    fs <- [Dom Name] -> Maybe [Dom Name] -> [Dom Name]
    forall a. a -> Maybe a -> a
    fromMaybe [Dom Name]
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe [Dom Name] -> [Dom Name])
    -> m (Maybe [Dom Name]) -> m [Dom Name]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> m (Maybe [Dom Name])
    forall (m :: * -> *).
    (HasConstInfo m, ReadTCState m) =>
    QName -> m (Maybe [Dom Name])
    getRecordFieldNames_ QName
    r
                Bool -> m () -> m ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless ([Dom Name] -> Nat
    forall (t :: * -> *) a. Foldable t => t a -> Nat
    length [Dom Name]
    fs Nat -> Nat -> Bool
    forall a. Eq a => a -> a -> Bool
    == Patterns -> Nat
    forall (t :: * -> *) a. Foldable t => t a -> Nat
    length Patterns
    ps) m ()
    forall a. HasCallStack => a
    __IMPOSSIBLE__
                Pattern -> m Pattern
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Pattern -> m Pattern) -> Pattern -> m Pattern
    forall a b. (a -> b) -> a -> b
    $ PatInfo -> [FieldAssignment' Pattern] -> Pattern
    forall e. PatInfo -> [FieldAssignment' (Pattern' e)] -> Pattern' e
    A.RecP PatInfo
    patNoRange ([FieldAssignment' Pattern] -> Pattern)
    -> [FieldAssignment' Pattern] -> Pattern
    forall a b. (a -> b) -> a -> b
    $ (Dom Name -> Arg (Named_ Pattern) -> FieldAssignment' Pattern)
    -> [Dom Name] -> Patterns -> [FieldAssignment' Pattern]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith Dom Name -> Arg (Named_ Pattern) -> FieldAssignment' Pattern
    forall {t} {a}. Dom' t Name -> NamedArg a -> FieldAssignment' a
    mkFA [Dom 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__

    -- | 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
      String -> Nat -> String -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Nat -> String -> m ()
    reportSLn String
    "reify.expr" Nat
    60 (String -> m ()) -> String -> m ()
    forall a b. (a -> b) -> a -> b
    $ String
    "recOrCon " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ QName -> String
    forall a. Pretty a => a -> String
    prettyShow QName
    c
      m (Maybe (QName, Defn))
    -> m Expr -> ((QName, Defn) -> 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, Defn))
    forall (m :: * -> *).
    HasConstInfo m =>
    QName -> m (Maybe (QName, Defn))
    isRecordConstructor QName
    c) m Expr
    fallback (((QName, Defn) -> m Expr) -> m Expr)
    -> ((QName, Defn) -> m Expr) -> m Expr
    forall a b. (a -> b) -> a -> b
    $ \ (QName
    r, Defn
    def) -> do
        -- If the record constructor is generated or the user wrote a record expression,
        -- print record expression.
        -- Otherwise, print constructor expression.
        if Defn -> Bool
    recNamedCon Defn
    def Bool -> Bool -> Bool
    && ConInfo
    co ConInfo -> ConInfo -> Bool
    forall a. Eq a => a -> a -> Bool
    /= ConInfo
    ConORec then m Expr
    fallback else do
          [Dom Name]
    fs <- [Dom Name] -> Maybe [Dom Name] -> [Dom Name]
    forall a. a -> Maybe a -> a
    fromMaybe [Dom Name]
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe [Dom Name] -> [Dom Name])
    -> m (Maybe [Dom Name]) -> m [Dom Name]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> m (Maybe [Dom Name])
    forall (m :: * -> *).
    (HasConstInfo m, ReadTCState m) =>
    QName -> m (Maybe [Dom Name])
    getRecordFieldNames_ QName
    r
          Bool -> m () -> m ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless ([Dom Name] -> Nat
    forall (t :: * -> *) a. Foldable t => t a -> Nat
    length [Dom Name]
    fs Nat -> Nat -> Bool
    forall a. Eq a => a -> a -> Bool
    == [Arg Expr] -> Nat
    forall (t :: * -> *) a. Foldable t => t a -> Nat
    length [Arg Expr]
    es) m ()
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          Expr -> m Expr
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Expr -> m Expr) -> Expr -> m Expr
    forall a b. (a -> b) -> a -> b
    $ ExprInfo -> RecordAssigns -> Expr
    A.Rec ExprInfo
    forall a. Null a => a
    empty (RecordAssigns -> Expr) -> RecordAssigns -> Expr
    forall a b. (a -> b) -> a -> b
    $ (Dom Name -> Arg Expr -> Either (FieldAssignment' Expr) ModuleName)
    -> [Dom Name] -> [Arg Expr] -> RecordAssigns
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith Dom Name -> Arg Expr -> Either (FieldAssignment' Expr) ModuleName
    forall {t} {b} {b}.
    Dom' t Name -> Arg b -> Either (FieldAssignment' b) b
    mkFA [Dom 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)
    reify (QName -> Bool -> Clause -> NamedClause
    NamedClause QName
    f Bool
    True Clause
    cl)

    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) = Telescope -> m Clause -> m Clause
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext (Clause -> Telescope
    clauseTel Clause
    cl) (m Clause -> m Clause) -> m Clause -> m Clause
    forall a b. (a -> b) -> a -> b
    $ do
        String -> Nat -> TCM Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Nat -> TCM Doc -> m ()
    reportSDoc String
    "reify.clause" Nat
    60 (TCM Doc -> m ()) -> TCM Doc -> m ()
    forall a b. (a -> b) -> a -> b
    $ Doc -> TCM Doc
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Doc -> TCM Doc) -> Doc -> TCM 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
    <+> QName -> Doc
    forall a. Pretty a => a -> Doc
    pretty QName
    f
          , Doc
    "  toDrop =" Doc -> Doc -> Doc
    <+> Bool -> Doc
    forall a. Show a => a -> Doc
    pshow Bool
    toDrop
          , Doc
    "  cl     =" Doc -> Doc -> Doc
    <+> Clause -> Doc
    forall a. Pretty a => a -> Doc
    pretty Clause
    cl
          ]
        let ell :: ExpandedEllipsis
    ell = Clause -> ExpandedEllipsis
    clauseEllipsis Clause
    cl
        Patterns
    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
    $ Clause -> [NamedArg DeBruijnPattern]
    namedClausePats Clause
    cl
        SpineLHS
    lhs <- (QName -> Patterns -> SpineLHS) -> (QName, Patterns) -> SpineLHS
    forall a b c. (a -> b -> c) -> (a, b) -> c
    uncurry (LHSInfo -> QName -> Patterns -> SpineLHS
    SpineLHS (LHSInfo -> QName -> Patterns -> SpineLHS)
    -> LHSInfo -> QName -> Patterns -> SpineLHS
    forall a b. (a -> b) -> a -> b
    $ LHSInfo
    forall a. Null a => a
    empty { lhsEllipsis :: ExpandedEllipsis
    lhsEllipsis = ExpandedEllipsis
    ell }) ((QName, Patterns) -> SpineLHS)
    -> m (QName, Patterns) -> m SpineLHS
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> Patterns -> Patterns -> m (QName, Patterns)
    forall (m :: * -> *).
    MonadReify m =>
    QName -> Patterns -> Patterns -> m (QName, Patterns)
    reifyDisplayFormP QName
    f Patterns
    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.
        (Patterns
    params , SpineLHS
    lhs) <- if Bool -> Bool
    not Bool
    toDrop then (Patterns, SpineLHS) -> m (Patterns, SpineLHS)
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([] , SpineLHS
    lhs) else do
          Nat
    nfv <- QName -> m (Either SigError ModuleName)
    forall (m :: * -> *).
    HasConstInfo m =>
    QName -> m (Either SigError ModuleName)
    getDefModule QName
    f m (Either SigError ModuleName)
    -> (Either SigError ModuleName -> m Nat) -> m Nat
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
            Left SigError
    _  -> Nat -> m Nat
    forall (m :: * -> *) a. Monad m => a -> m a
    return Nat
    0
            Right ModuleName
    m -> Telescope -> Nat
    forall a. Sized a => a -> Nat
    size (Telescope -> Nat) -> m Telescope -> m Nat
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ModuleName -> m Telescope
    forall (m :: * -> *).
    (Functor m, ReadTCState m) =>
    ModuleName -> m Telescope
    lookupSection ModuleName
    m
          (Patterns, SpineLHS) -> m (Patterns, SpineLHS)
    forall (m :: * -> *) a. Monad m => a -> m a
    return ((Patterns, SpineLHS) -> m (Patterns, SpineLHS))
    -> (Patterns, SpineLHS) -> m (Patterns, SpineLHS)
    forall a b. (a -> b) -> a -> b
    $ Nat -> SpineLHS -> (Patterns, SpineLHS)
    splitParams Nat
    nfv SpineLHS
    lhs
        SpineLHS
    lhs <- Patterns -> SpineLHS -> m SpineLHS
    forall (m :: * -> *).
    MonadReify m =>
    Patterns -> SpineLHS -> m SpineLHS
    stripImps Patterns
    params SpineLHS
    lhs
        String -> Nat -> TCM Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Nat -> TCM Doc -> m ()
    reportSDoc String
    "reify.clause" Nat
    100 (TCM Doc -> m ()) -> TCM Doc -> m ()
    forall a b. (a -> b) -> a -> b
    $ Doc -> TCM Doc
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Doc -> TCM Doc) -> Doc -> TCM Doc
    forall a b. (a -> b) -> a -> b
    $ Doc
    "reifying NamedClause, lhs =" Doc -> Doc -> Doc
    <?> SpineLHS -> Doc
    forall a. Show a => a -> Doc
    pshow SpineLHS
    lhs
        RHS
    rhs <- Maybe Term -> m RHS -> (Term -> m RHS) -> m RHS
    forall a b. Maybe a -> b -> (a -> b) -> b
    caseMaybe (Clause -> Maybe Term
    clauseBody Clause
    cl) (RHS -> m RHS
    forall (m :: * -> *) a. Monad m => a -> m a
    return RHS
    AbsurdRHS) ((Term -> m RHS) -> m RHS) -> (Term -> m RHS) -> m RHS
    forall a b. (a -> b) -> a -> b
    $ \ Term
    e ->
          Expr -> Maybe Expr -> RHS
    RHS (Expr -> Maybe Expr -> RHS) -> m Expr -> m (Maybe Expr -> RHS)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Term -> m (ReifiesTo Term)
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    reify Term
    e m (Maybe Expr -> RHS) -> m (Maybe Expr) -> m RHS
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Maybe Expr -> m (Maybe Expr)
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Maybe Expr
    forall a. Maybe a
    Nothing
        String -> Nat -> TCM Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Nat -> TCM Doc -> m ()
    reportSDoc String
    "reify.clause" Nat
    100 (TCM Doc -> m ()) -> TCM Doc -> m ()
    forall a b. (a -> b) -> a -> b
    $ Doc -> TCM Doc
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Doc -> TCM Doc) -> Doc -> TCM Doc
    forall a b. (a -> b) -> a -> b
    $ Doc
    "reifying NamedClause, rhs =" Doc -> Doc -> Doc
    <?> RHS -> Doc
    forall a. Show a => a -> Doc
    pshow RHS
    rhs
        let result :: Clause
    result = LHS -> [ProblemEq] -> RHS -> WhereDeclarations -> Bool -> Clause
    forall lhs.
    lhs
    -> [ProblemEq] -> RHS -> WhereDeclarations -> Bool -> Clause' lhs
    A.Clause (SpineLHS -> LHS
    forall a b. LHSToSpine a b => b -> a
    spineToLhs SpineLHS
    lhs) [] RHS
    rhs WhereDeclarations
    A.noWhereDecls (Clause -> Bool
    I.clauseCatchall Clause
    cl)
        String -> Nat -> TCM Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Nat -> TCM Doc -> m ()
    reportSDoc String
    "reify.clause" Nat
    100 (TCM Doc -> m ()) -> TCM Doc -> m ()
    forall a b. (a -> b) -> a -> b
    $ Doc -> TCM Doc
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Doc -> TCM Doc) -> Doc -> TCM Doc
    forall a b. (a -> b) -> a -> b
    $ Doc
    "reified NamedClause, result =" Doc -> Doc -> Doc
    <?> Clause -> Doc
    forall a. Show a => a -> Doc
    pshow Clause
    result
        Clause -> m Clause
    forall (m :: * -> *) a. Monad m => a -> m a
    return Clause
    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 => [NamedArg A.Pattern] -> SpineLHS -> m SpineLHS
          stripImps :: forall (m :: * -> *).
    MonadReify m =>
    Patterns -> SpineLHS -> m SpineLHS
    stripImps 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
    <$> Patterns -> Patterns -> m Patterns
    forall (m :: * -> *).
    MonadReify m =>
    Patterns -> Patterns -> m Patterns
    stripImplicits Patterns
    params Patterns
    ps

    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 Telescope
    tel [(Face, Term)]
    sys)) = Telescope -> m [Clause] -> m [Clause]
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext Telescope
    tel (m [Clause] -> m [Clause]) -> m [Clause] -> m [Clause]
    forall a b. (a -> b) -> a -> b
    $ do
        String -> Nat -> [String] -> m ()
    forall a (m :: * -> *).
    (ReportS a, MonadDebug m) =>
    String -> Nat -> a -> m ()
    reportS String
    "reify.system" Nat
    40 ([String] -> m ()) -> [String] -> m ()
    forall a b. (a -> b) -> a -> b
    $ Telescope -> String
    forall a. Show a => a -> String
    show Telescope
    tel String -> [String] -> [String]
    forall a. a -> [a] -> [a]
    : ((Face, Term) -> String) -> [(Face, Term)] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map (Face, Term) -> String
    forall a. Show a => a -> String
    show [(Face, Term)]
    sys
        Term -> IntervalView
    view <- m (Term -> IntervalView)
    forall (m :: * -> *). HasBuiltins m => m (Term -> IntervalView)
    intervalView'
        IntervalView -> Term
    unview <- m (IntervalView -> Term)
    forall (m :: * -> *). HasBuiltins m => m (IntervalView -> Term)
    intervalUnview'
        [(Face, Term)]
    sys <- (((Face, Term) -> m Bool) -> [(Face, Term)] -> m [(Face, Term)])
    -> [(Face, Term)] -> ((Face, Term) -> m Bool) -> m [(Face, Term)]
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip ((Face, Term) -> m Bool) -> [(Face, Term)] -> m [(Face, Term)]
    forall (m :: * -> *) a.
    Applicative m =>
    (a -> m Bool) -> [a] -> m [a]
    filterM [(Face, Term)]
    sys (((Face, Term) -> m Bool) -> m [(Face, Term)])
    -> ((Face, Term) -> m Bool) -> m [(Face, Term)]
    forall a b. (a -> b) -> a -> b
    $ \ (Face
    phi,Term
    t) -> do
          Face -> ((Term, Bool) -> m Bool) -> m Bool
    forall (f :: * -> *) (m :: * -> *) a.
    (Functor f, Foldable f, Monad m) =>
    f a -> (a -> m Bool) -> m Bool
    allM 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
            Term
    u <- Term -> m Term
    forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
    reduce Term
    u
            Bool -> m Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Bool -> m Bool) -> Bool -> m Bool
    forall a b. (a -> b) -> a -> b
    $ case (Term -> IntervalView
    view Term
    u, Bool
    b) of
              (IntervalView
    IZero, Bool
    True) -> Bool
    False
              (IntervalView
    IOne, Bool
    False) -> Bool
    False
              (IntervalView, Bool)
    _ -> Bool
    True
        [(Face, Term)] -> ((Face, Term) -> m Clause) -> m [Clause]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    t a -> (a -> m b) -> m (t b)
    forM [(Face, Term)]
    sys (((Face, Term) -> m Clause) -> m [Clause])
    -> ((Face, Term) -> m Clause) -> m [Clause]
    forall a b. (a -> b) -> a -> b
    $ \ (Face
    alpha,Term
    u) -> do
          RHS
    rhs <- Expr -> Maybe Expr -> RHS
    RHS (Expr -> Maybe Expr -> RHS) -> m Expr -> m (Maybe Expr -> RHS)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Term -> m (ReifiesTo Term)
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    reify Term
    u m (Maybe Expr -> RHS) -> m (Maybe Expr) -> m RHS
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Maybe Expr -> m (Maybe Expr)
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Maybe Expr
    forall a. Maybe a
    Nothing
          Pattern
    ep <- ([(Expr, Expr)] -> Pattern) -> m [(Expr, Expr)] -> m Pattern
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (PatInfo -> [(Expr, Expr)] -> Pattern
    forall e. PatInfo -> [(e, e)] -> Pattern' e
    A.EqualP PatInfo
    patNoRange) (m [(Expr, Expr)] -> m Pattern)
    -> (((Term, Bool) -> m (Expr, Expr)) -> m [(Expr, Expr)])
    -> ((Term, Bool) -> m (Expr, Expr))
    -> m Pattern
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Face -> ((Term, Bool) -> m (Expr, Expr)) -> m [(Expr, Expr)]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    t a -> (a -> m b) -> m (t b)
    forM Face
    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)
    reify (Term
    phi, Bool -> Term
    d Bool
    b)

          Patterns
    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
    $ Telescope -> [NamedArg DeBruijnPattern]
    forall a. DeBruijn a => Telescope -> [NamedArg a]
    teleNamedArgs Telescope
    tel
          Patterns
    ps <- Patterns -> Patterns -> m Patterns
    forall (m :: * -> *).
    MonadReify m =>
    Patterns -> Patterns -> m Patterns
    stripImplicits [] (Patterns -> m Patterns) -> Patterns -> m Patterns
    forall a b. (a -> b) -> a -> b
    $ Patterns
    ps Patterns -> Patterns -> Patterns
    forall a. [a] -> [a] -> [a]
    ++ [Pattern -> Arg (Named_ Pattern)
    forall a. a -> NamedArg a
    defaultNamedArg Pattern
    ep]
          let
            lhs :: SpineLHS
    lhs = LHSInfo -> QName -> Patterns -> SpineLHS
    SpineLHS LHSInfo
    forall a. Null a => a
    empty QName
    f Patterns
    ps
            result :: Clause
    result = LHS -> [ProblemEq] -> RHS -> WhereDeclarations -> Bool -> Clause
    forall lhs.
    lhs
    -> [ProblemEq] -> RHS -> WhereDeclarations -> Bool -> Clause' lhs
    A.Clause (SpineLHS -> LHS
    forall a b. LHSToSpine a b => b -> a
    spineToLhs SpineLHS
    lhs) [] RHS
    rhs WhereDeclarations
    A.noWhereDecls Bool
    False
          Clause -> m Clause
    forall (m :: * -> *) a. Monad m => a -> m a
    return Clause
    result

    instance Reify Type where
        type ReifiesTo Type = Expr

        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
        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)
    reify Term
    t

    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
          Sort
    s <- Sort -> m Sort
    forall a (m :: * -> *).
    (InstantiateFull a, MonadReduce m) =>
    a -> m a
    instantiateFull Sort
    s
          SortKit{QName
    IsFibrant -> QName
    nameOfSetOmega :: SortKit -> IsFibrant -> QName
    nameOfSSet :: SortKit -> QName
    nameOfProp :: SortKit -> QName
    nameOfSet :: SortKit -> QName
    nameOfSetOmega :: IsFibrant -> QName
    nameOfSSet :: QName
    nameOfProp :: QName
    nameOfSet :: QName
    ..} <- m SortKit
    forall (m :: * -> *). HasBuiltins m => m SortKit
    sortKit
          case Sort
    s of
            I.Type (I.ClosedLevel Integer
    0) -> Expr -> m Expr
    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' QName
    nameOfSet Suffix
    A.NoSuffix
            I.Type (I.ClosedLevel Integer
    n) -> Expr -> m Expr
    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' QName
    nameOfSet (Integer -> Suffix
    A.Suffix Integer
    n)
            I.Type Level
    a -> do
              Expr
    a <- Level -> m (ReifiesTo Level)
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    reify Level
    a
              Expr -> m Expr
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Expr -> m Expr) -> Expr -> m Expr
    forall a b. (a -> b) -> a -> b
    $ AppInfo -> Expr -> Arg (Named_ Expr) -> Expr
    A.App AppInfo
    defaultAppInfo_ (QName -> Expr
    A.Def QName
    nameOfSet) (Expr -> Arg (Named_ Expr)
    forall a. a -> NamedArg a
    defaultNamedArg Expr
    a)
            I.Prop (I.ClosedLevel Integer
    0) -> Expr -> m Expr
    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' QName
    nameOfProp Suffix
    A.NoSuffix
            I.Prop (I.ClosedLevel Integer
    n) -> Expr -> m Expr
    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' QName
    nameOfProp (Integer -> Suffix
    A.Suffix Integer
    n)
            I.Prop Level
    a -> do
              Expr
    a <- Level -> m (ReifiesTo Level)
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    reify Level
    a
              Expr -> m Expr
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Expr -> m Expr) -> Expr -> m Expr
    forall a b. (a -> b) -> a -> b
    $ AppInfo -> Expr -> Arg (Named_ Expr) -> Expr
    A.App AppInfo
    defaultAppInfo_ (QName -> Expr
    A.Def QName
    nameOfProp) (Expr -> Arg (Named_ Expr)
    forall a. a -> NamedArg a
    defaultNamedArg Expr
    a)
            I.Inf IsFibrant
    f Integer
    0 -> Expr -> m Expr
    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' (IsFibrant -> QName
    nameOfSetOmega IsFibrant
    f) Suffix
    A.NoSuffix
            I.Inf IsFibrant
    f Integer
    n -> Expr -> m Expr
    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' (IsFibrant -> QName
    nameOfSetOmega IsFibrant
    f) (Integer -> Suffix
    A.Suffix Integer
    n)
            I.SSet Level
    a  -> do
              I.Def QName
    sset [] <- Term -> Maybe Term -> Term
    forall a. a -> Maybe a -> a
    fromMaybe Term
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe Term -> Term) -> m (Maybe Term) -> m Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> String -> m (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => String -> m (Maybe Term)
    getBuiltin' String
    builtinStrictSet
              Expr
    a <- Level -> m (ReifiesTo Level)
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    reify Level
    a
              Expr -> m Expr
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Expr -> m Expr) -> Expr -> m Expr
    forall a b. (a -> b) -> a -> b
    $ AppInfo -> Expr -> Arg (Named_ Expr) -> Expr
    A.App AppInfo
    defaultAppInfo_ (QName -> Expr
    A.Def QName
    sset) (Expr -> Arg (Named_ Expr)
    forall a. a -> NamedArg a
    defaultNamedArg Expr
    a)
            Sort
    I.SizeUniv  -> do
              I.Def QName
    sizeU [] <- Term -> Maybe Term -> Term
    forall a. a -> Maybe a -> a
    fromMaybe Term
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe Term -> Term) -> m (Maybe Term) -> m Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> String -> m (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => String -> m (Maybe Term)
    getBuiltin' String
    builtinSizeUniv
              Expr -> m Expr
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Expr -> m Expr) -> Expr -> m Expr
    forall a b. (a -> b) -> a -> b
    $ QName -> Expr
    A.Def QName
    sizeU
            Sort
    I.LockUniv  -> do
              QName
    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
    <$> String -> m (Maybe QName)
    forall (m :: * -> *). HasBuiltins m => String -> m (Maybe QName)
    getName' String
    builtinLockUniv
              Expr -> m Expr
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Expr -> m Expr) -> Expr -> m Expr
    forall a b. (a -> b) -> a -> b
    $ QName -> Expr
    A.Def QName
    lockU
            I.PiSort Dom' Term Term
    a Sort
    s1 Abs Sort
    s2 -> do
              Name
    pis <- String -> m Name
    forall a (m :: * -> *).
    (FreshName a, MonadFresh NameId m) =>
    a -> m Name
    freshName_ (String
    "piSort" :: String) -- TODO: hack
              (Expr
    e1,Expr
    e2) <- (Sort, Term) -> m (ReifiesTo (Sort, Term))
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    reify (Sort
    s1, ArgInfo -> Abs Term -> Term
    I.Lam ArgInfo
    defaultArgInfo (Abs Term -> Term) -> Abs Term -> Term
    forall a b. (a -> b) -> a -> b
    $ (Sort -> Term) -> Abs Sort -> Abs Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Sort -> Term
    Sort Abs Sort
    s2)
              let app :: Expr -> Expr -> Expr
    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)
              Expr -> m Expr
    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
    pis Expr -> Expr -> Expr
    `app` Expr
    e1 Expr -> Expr -> Expr
    `app` Expr
    e2
            I.FunSort Sort
    s1 Sort
    s2 -> do
              Name
    funs <- String -> m Name
    forall a (m :: * -> *).
    (FreshName a, MonadFresh NameId m) =>
    a -> m Name
    freshName_ (String
    "funSort" :: String) -- TODO: hack
              (Expr
    e1,Expr
    e2) <- (Sort, Sort) -> m (ReifiesTo (Sort, Sort))
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    reify (Sort
    s1 , Sort
    s2)
              let app :: Expr -> Expr -> Expr
    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)
              Expr -> m Expr
    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
    funs Expr -> Expr -> Expr
    `app` Expr
    e1 Expr -> Expr -> Expr
    `app` Expr
    e2
            I.UnivSort Sort
    s -> do
              Name
    univs <- String -> m Name
    forall a (m :: * -> *).
    (FreshName a, MonadFresh NameId m) =>
    a -> m Name
    freshName_ (String
    "univSort" :: String) -- TODO: hack
              Expr
    e <- Sort -> m (ReifiesTo Sort)
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    reify Sort
    s
              Expr -> m Expr
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Expr -> m Expr) -> Expr -> m Expr
    forall a b. (a -> b) -> a -> b
    $ AppInfo -> Expr -> Arg (Named_ Expr) -> Expr
    A.App AppInfo
    defaultAppInfo_ (Name -> Expr
    A.Var Name
    univs) (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
            I.MetaS MetaId
    x Elims
    es -> Term -> m (ReifiesTo Term)
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    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)
    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 String
    s -> Expr -> m Expr
    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
    $ String -> Text
    T.pack String
    s

    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 Expr -> m Expr -> m Expr
    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
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    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 Expr -> m Expr) -> m Expr -> m Expr
    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
    name <- String -> m Name
    forall a (m :: * -> *).
    (FreshName a, MonadFresh NameId m) =>
    a -> m Name
    freshName_ (String
    ".#Lacking_Level_Builtins#" :: String)
        Expr -> m Expr
    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

    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 String
    x i
    v) = String -> m Name
    forall a (m :: * -> *).
    (FreshName a, MonadFresh NameId m) =>
    a -> m Name
    freshName_ String
    x m Name -> (Name -> m (Name, ReifiesTo i)) -> m (Name, ReifiesTo i)
    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)
    reify i
    v
      reify (Abs String
    s i
    v) = do

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

        Name
    x <- Name -> Name
    forall a. LensInScope a => a -> a
    C.setNotInScope (Name -> Name) -> m Name -> m Name
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> String -> m Name
    forall a (m :: * -> *).
    (FreshName a, MonadFresh NameId m) =>
    a -> m Name
    freshName_ String
    s
        ReifiesTo i
    e <- Name -> m (ReifiesTo i) -> m (ReifiesTo i)
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext Name
    x -- type doesn't matter
             (m (ReifiesTo i) -> m (ReifiesTo i))
    -> m (ReifiesTo i) -> m (ReifiesTo i)
    forall a b. (a -> b) -> a -> b
    $ i -> m (ReifiesTo i)
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    reify i
    v
        (Name, ReifiesTo i) -> m (Name, ReifiesTo i)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Name
    x,ReifiesTo i
    e)

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

      reify :: forall (m :: * -> *).
    MonadReify m =>
    Telescope -> m (ReifiesTo Telescope)
    reify Telescope
    EmptyTel = Telescope -> m Telescope
    forall (m :: * -> *) a. Monad m => a -> m a
    return []
      reify (ExtendTel Dom Type
    arg Abs Telescope
    tel) = do
        Arg ArgInfo
    info Expr
    e <- Dom Type -> m (ReifiesTo (Dom Type))
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    reify Dom Type
    arg
        (Name
    x, Telescope
    bs)  <- Abs Telescope -> m (ReifiesTo (Abs Telescope))
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    reify Abs Telescope
    tel
        let r :: Range
    r    = Expr -> Range
    forall a. HasRange a => a -> Range
    getRange Expr
    e
            name :: Maybe (WithOrigin (Ranged String))
    name = Dom Type -> Maybe (WithOrigin (Ranged String))
    forall t e. Dom' t e -> Maybe (WithOrigin (Ranged String))
    domName Dom Type
    arg
        Maybe Expr
    tac <- (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)
    traverse Term -> m Expr
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    reify (Maybe Term -> m (Maybe Expr)) -> Maybe Term -> m (Maybe Expr)
    forall a b. (a -> b) -> a -> b
    $ Dom Type -> Maybe Term
    forall t e. Dom' t e -> Maybe t
    domTactic Dom Type
    arg
        let xs :: List1 (Arg (Named (WithOrigin (Ranged String)) Binder))
    xs = Arg (Named (WithOrigin (Ranged String)) Binder)
    -> List1 (Arg (Named (WithOrigin (Ranged String)) Binder))
    forall el coll. Singleton el coll => el -> coll
    singleton (Arg (Named (WithOrigin (Ranged String)) Binder)
     -> List1 (Arg (Named (WithOrigin (Ranged String)) Binder)))
    -> Arg (Named (WithOrigin (Ranged String)) Binder)
    -> List1 (Arg (Named (WithOrigin (Ranged String)) Binder))
    forall a b. (a -> b) -> a -> b
    $ ArgInfo
    -> Named (WithOrigin (Ranged String)) Binder
    -> Arg (Named (WithOrigin (Ranged String)) Binder)
    forall e. ArgInfo -> e -> Arg e
    Arg ArgInfo
    info (Named (WithOrigin (Ranged String)) Binder
     -> Arg (Named (WithOrigin (Ranged String)) Binder))
    -> Named (WithOrigin (Ranged String)) Binder
    -> Arg (Named (WithOrigin (Ranged String)) Binder)
    forall a b. (a -> b) -> a -> b
    $ Maybe (WithOrigin (Ranged String))
    -> Binder -> Named (WithOrigin (Ranged String)) Binder
    forall name a. Maybe name -> a -> Named name a
    Named Maybe (WithOrigin (Ranged String))
    name (Binder -> Named (WithOrigin (Ranged String)) Binder)
    -> Binder -> Named (WithOrigin (Ranged String)) Binder
    forall a b. (a -> b) -> a -> b
    $ Name -> Binder
    A.mkBinder_ Name
    x
        Telescope -> m Telescope
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Telescope -> m Telescope) -> Telescope -> m Telescope
    forall a b. (a -> b) -> a -> b
    $ Range
    -> Maybe Expr
    -> List1 (Arg (Named (WithOrigin (Ranged String)) Binder))
    -> Expr
    -> TypedBinding
    TBind Range
    r Maybe Expr
    tac List1 (Arg (Named (WithOrigin (Ranged String)) Binder))
    xs Expr
    e TypedBinding -> Telescope -> Telescope
    forall a. a -> [a] -> [a]
    : Telescope
    bs

    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)
    reify i
    i

    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)
    traverse i -> m (ReifiesTo i)
    forall i (m :: * -> *).
    (Reify i, 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)
    traverse (Bool -> i -> m (ReifiesTo i)
    forall i (m :: * -> *).
    (Reify i, 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)
    traverse i -> m (ReifiesTo i)
    forall i (m :: * -> *).
    (Reify i, 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)
    traverse (Bool -> i -> m (ReifiesTo i)
    forall i (m :: * -> *).
    (Reify i, 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)
    reify i1
    x m (ReifiesTo i2 -> (ReifiesTo i1, ReifiesTo i2))
    -> m (ReifiesTo i2) -> m (ReifiesTo i1, ReifiesTo i2)
    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)
    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)
    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 (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)
    reify i2
    y m (ReifiesTo i3 -> (ReifiesTo i1, ReifiesTo i2, ReifiesTo i3))
    -> m (ReifiesTo i3) -> m (ReifiesTo i1, ReifiesTo i2, ReifiesTo i3)
    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)
    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)
    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 (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)
    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 (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)
    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 (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)
    reify i4
    w