    {-# OPTIONS_GHC -fwarn-missing-signatures #-}

    module Agda.Syntax.Translation.ReflectedToAbstract where

    import Control.Arrow        ( (***) )
    import Control.Monad        ( foldM )
    import Control.Monad.Except ( MonadError )
    import Control.Monad.Reader ( MonadReader(..), asks, reader, runReaderT )

    import Data.Maybe
    import Data.Set (Set)
    import qualified Data.Set as Set
    import Data.Text (Text)
    import qualified Data.Text as Text

    import Agda.Syntax.Literal
    import Agda.Syntax.Position
    import Agda.Syntax.Info
    import Agda.Syntax.Common
    import Agda.Syntax.Abstract
      ( Name, QName, QNamed(QNamed)
      , isNoName, nameConcrete, nextName, qualify, unambiguous
      )
    import qualified Agda.Syntax.Abstract as A
    import Agda.Syntax.Abstract.Pattern
    import Agda.Syntax.Reflected as R
    import Agda.Syntax.Internal (Dom,Dom'(..))

    import Agda.Interaction.Options (optUseUnicode, UnicodeOrAscii(..))
    import Agda.TypeChecking.Monad as M hiding (MetaInfo)
    import Agda.Syntax.Scope.Monad (getCurrentModule)

    import Agda.Utils.Impossible
    import Agda.Utils.Maybe
    import Agda.Utils.Monad
    import Agda.Utils.List
    import Agda.Utils.List1 (List1, pattern (:|))
    import qualified Agda.Utils.List1 as List1
    import Agda.Utils.Null
    import Agda.Syntax.Common.Pretty
    import Agda.Utils.Functor
    import Agda.Utils.Singleton
    import Agda.Utils.Size

    type Vars = [(Name,R.Type)]

    type MonadReflectedToAbstract m =
      ( MonadReader Vars m
      , MonadFresh NameId m
      , MonadError TCErr m
      , MonadTCEnv m
      , ReadTCState m
      , HasOptions m
      , HasBuiltins m
      , HasConstInfo m
      )

    -- | Adds a new unique name to the current context.
    --   NOTE: See @chooseName@ in @Agda.Syntax.Translation.AbstractToConcrete@ for similar logic.
    --   NOTE: See @freshConcreteName@ in @Agda.Syntax.Scope.Monad@ also for similar logic.
    withName :: MonadReflectedToAbstract m => String -> (Name -> m a) -> m a
    withName :: forall (m :: * -> *) a.
    MonadReflectedToAbstract m =>
    String -> (Name -> m a) -> m a
    withName String
    s = String -> Type -> (Name -> m a) -> m a
    forall (m :: * -> *) a.
    MonadReflectedToAbstract m =>
    String -> Type -> (Name -> m a) -> m a
    withVar String
    s Type
    R.Unknown

    withVar :: MonadReflectedToAbstract m => String -> R.Type -> (Name -> m a) -> m a
    withVar :: forall (m :: * -> *) a.
    MonadReflectedToAbstract m =>
    String -> Type -> (Name -> m a) -> m a
    withVar String
    s Type
    t Name -> m a
    f = do
      name <- String -> m Name
    forall a (m :: * -> *).
    (FreshName a, MonadFresh NameId m) =>
    a -> m Name
    forall (m :: * -> *). MonadFresh NameId m => String -> m Name
    freshName_ String
    s
      ctx  <- asks $ map $ nameConcrete . fst
      glyphMode <- optUseUnicode <$> M.pragmaOptions
      let freshNameMode = case UnicodeOrAscii
    glyphMode of
            UnicodeOrAscii
    UnicodeOk -> FreshNameMode
    A.UnicodeSubscript
            UnicodeOrAscii
    AsciiOnly -> FreshNameMode
    A.AsciiCounter
      let name' = Name -> [Name] -> Name
    forall a. a -> [a] -> a
    headWithDefault Name
    forall a. HasCallStack => a
    __IMPOSSIBLE__ ([Name] -> Name) -> [Name] -> Name
    forall a b. (a -> b) -> a -> b
    $ (Name -> Bool) -> [Name] -> [Name]
    forall a. (a -> Bool) -> [a] -> [a]
    filter ([Name] -> Name -> Bool
    forall {t :: * -> *}. Foldable t => t Name -> Name -> Bool
    notTaken [Name]
    ctx) ([Name] -> [Name]) -> [Name] -> [Name]
    forall a b. (a -> b) -> a -> b
    $ (Name -> Name) -> Name -> [Name]
    forall a. (a -> a) -> a -> [a]
    iterate (FreshNameMode -> Name -> Name
    nextName FreshNameMode
    freshNameMode) Name
    name
      local ((name,t):) $ f name'
      where
        notTaken :: t Name -> Name -> Bool
    notTaken t Name
    xs Name
    x = Name -> Bool
    forall a. IsNoName a => a -> Bool
    isNoName Name
    x Bool -> Bool -> Bool
    || Name -> Name
    nameConcrete Name
    x Name -> t Name -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `notElem` t Name
    xs

    withNames :: MonadReflectedToAbstract m => [String] -> ([Name] -> m a) -> m a
    withNames :: forall (m :: * -> *) a.
    MonadReflectedToAbstract m =>
    [String] -> ([Name] -> m a) -> m a
    withNames [String]
    ss = [(String, Type)] -> ([Name] -> m a) -> m a
    forall (m :: * -> *) a.
    MonadReflectedToAbstract m =>
    [(String, Type)] -> ([Name] -> m a) -> m a
    withVars ([(String, Type)] -> ([Name] -> m a) -> m a)
    -> [(String, Type)] -> ([Name] -> m a) -> m a
    forall a b. (a -> b) -> a -> b
    $ [String] -> [Type] -> [(String, Type)]
    forall a b. [a] -> [b] -> [(a, b)]
    zip [String]
    ss ([Type] -> [(String, Type)]) -> [Type] -> [(String, Type)]
    forall a b. (a -> b) -> a -> b
    $ Type -> [Type]
    forall a. a -> [a]
    repeat Type
    R.Unknown

    withVars :: MonadReflectedToAbstract m => [(String, R.Type)] -> ([Name] -> m a) -> m a
    withVars :: forall (m :: * -> *) a.
    MonadReflectedToAbstract m =>
    [(String, Type)] -> ([Name] -> m a) -> m a
    withVars [(String, Type)]
    ss [Name] -> m a
    f = case [(String, Type)]
    ss of
      []     -> [Name] -> m a
    f []
      ((String
    s,Type
    t):[(String, Type)]
    ss) -> String -> Type -> (Name -> m a) -> m a
    forall (m :: * -> *) a.
    MonadReflectedToAbstract m =>
    String -> Type -> (Name -> m a) -> m a
    withVar String
    s Type
    t ((Name -> m a) -> m a) -> (Name -> m a) -> m a
    forall a b. (a -> b) -> a -> b
    $ \Name
    n -> [(String, Type)] -> ([Name] -> m a) -> m a
    forall (m :: * -> *) a.
    MonadReflectedToAbstract m =>
    [(String, Type)] -> ([Name] -> m a) -> m a
    withVars [(String, Type)]
    ss (([Name] -> m a) -> m a) -> ([Name] -> m a) -> m a
    forall a b. (a -> b) -> a -> b
    $ \[Name]
    ns -> [Name] -> m a
    f (Name
    nName -> [Name] -> [Name]
    forall a. a -> [a] -> [a]
    :[Name]
    ns)

    -- | Returns the name and type of the variable with the given de Bruijn index.
    askVar :: MonadReflectedToAbstract m => Int -> m (Maybe (Name,R.Type))
    askVar :: forall (m :: * -> *).
    MonadReflectedToAbstract m =>
    Int -> m (Maybe (Name, Type))
    askVar Int
    i = ([(Name, Type)] -> Maybe (Name, Type)) -> m (Maybe (Name, Type))
    forall a. ([(Name, Type)] -> a) -> m a
    forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
    reader ([(Name, Type)] -> Int -> Maybe (Name, Type)
    forall a. [a] -> Int -> Maybe a
    !!! Int
    i)

    askName :: MonadReflectedToAbstract m => Int -> m (Maybe Name)
    askName :: forall (m :: * -> *).
    MonadReflectedToAbstract m =>
    Int -> m (Maybe Name)
    askName Int
    i = ((Name, Type) -> Name) -> Maybe (Name, Type) -> Maybe Name
    forall a b. (a -> b) -> Maybe a -> Maybe b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (Name, Type) -> Name
    forall a b. (a, b) -> a
    fst (Maybe (Name, Type) -> Maybe Name)
    -> m (Maybe (Name, Type)) -> m (Maybe Name)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Int -> m (Maybe (Name, Type))
    forall (m :: * -> *).
    MonadReflectedToAbstract m =>
    Int -> m (Maybe (Name, Type))
    askVar Int
    i

    class ToAbstract r where
      type AbsOfRef r
      toAbstract :: MonadReflectedToAbstract m => r -> m (AbsOfRef r)

      default toAbstract
        :: (Traversable t, ToAbstract s, t s ~ r, t (AbsOfRef s) ~ (AbsOfRef r))
        => MonadReflectedToAbstract m => r -> m (AbsOfRef r)
      toAbstract = (s -> m (AbsOfRef s)) -> t s -> m (t (AbsOfRef s))
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> t a -> f (t b)
    traverse s -> m (AbsOfRef s)
    forall r (m :: * -> *).
    (ToAbstract r, MonadReflectedToAbstract m) =>
    r -> m (AbsOfRef r)
    forall (m :: * -> *).
    MonadReflectedToAbstract m =>
    s -> m (AbsOfRef s)
    toAbstract

    -- | Translate reflected syntax to abstract, using the names from the current typechecking context.
    toAbstract_ ::
      (ToAbstract r
      , MonadFresh NameId m
      , MonadError TCErr m
      , MonadTCEnv m
      , ReadTCState m
      , HasOptions m
      , HasBuiltins m
      , HasConstInfo m
      ) => r -> m (AbsOfRef r)
    toAbstract_ :: forall r (m :: * -> *).
    (ToAbstract r, MonadFresh NameId m, MonadError TCErr m,
     MonadTCEnv m, ReadTCState m, HasOptions m, HasBuiltins m,
     HasConstInfo m) =>
    r -> m (AbsOfRef r)
    toAbstract_ = m (AbsOfRef r) -> m (AbsOfRef r)
    forall (m :: * -> *) a. ReadTCState m => m a -> m a
    withShowAllArguments (m (AbsOfRef r) -> m (AbsOfRef r))
    -> (r -> m (AbsOfRef r)) -> r -> m (AbsOfRef r)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . r -> m (AbsOfRef r)
    forall r (m :: * -> *).
    (ToAbstract r, MonadFresh NameId m, MonadError TCErr m,
     MonadTCEnv m, ReadTCState m, HasOptions m, HasBuiltins m,
     HasConstInfo m) =>
    r -> m (AbsOfRef r)
    toAbstractWithoutImplicit

    -- | Drop implicit arguments unless --show-implicit is on.
    toAbstractWithoutImplicit ::
      (ToAbstract r
      , MonadFresh NameId m
      , MonadError TCErr m
      , MonadTCEnv m
      , ReadTCState m
      , HasOptions m
      , HasBuiltins m
      , HasConstInfo m
      ) => r -> m (AbsOfRef r)
    toAbstractWithoutImplicit :: forall r (m :: * -> *).
    (ToAbstract r, MonadFresh NameId m, MonadError TCErr m,
     MonadTCEnv m, ReadTCState m, HasOptions m, HasBuiltins m,
     HasConstInfo m) =>
    r -> m (AbsOfRef r)
    toAbstractWithoutImplicit r
    x = do
      xs <- [Name] -> [Name]
    forall a. KillRange a => KillRangeT a
    killRange ([Name] -> [Name]) -> m [Name] -> m [Name]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m [Name]
    forall (m :: * -> *). MonadTCEnv m => m [Name]
    getContextNames'
      let ctx = [Name] -> [Type] -> [(Name, Type)]
    forall a b. [a] -> [b] -> [(a, b)]
    zip [Name]
    xs ([Type] -> [(Name, Type)]) -> [Type] -> [(Name, Type)]
    forall a b. (a -> b) -> a -> b
    $ Type -> [Type]
    forall a. a -> [a]
    repeat Type
    R.Unknown
      runReaderT (toAbstract x) ctx

    instance ToAbstract r => ToAbstract (Named name r) where
      type AbsOfRef (Named name r) = Named name (AbsOfRef r)

    instance ToAbstract r => ToAbstract (Arg r) where
      type AbsOfRef (Arg r) = NamedArg (AbsOfRef r)
      toAbstract :: forall (m :: * -> *).
    MonadReflectedToAbstract m =>
    Arg r -> m (AbsOfRef (Arg r))
    toAbstract (Arg ArgInfo
    i r
    x) = ArgInfo -> Named_ (AbsOfRef r) -> Arg (Named_ (AbsOfRef r))
    forall e. ArgInfo -> e -> Arg e
    Arg ArgInfo
    i (Named_ (AbsOfRef r) -> Arg (Named_ (AbsOfRef r)))
    -> m (Named_ (AbsOfRef r)) -> m (Arg (Named_ (AbsOfRef r)))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Named NamedName r -> m (AbsOfRef (Named NamedName r))
    forall r (m :: * -> *).
    (ToAbstract r, MonadReflectedToAbstract m) =>
    r -> m (AbsOfRef r)
    forall (m :: * -> *).
    MonadReflectedToAbstract m =>
    Named NamedName r -> m (AbsOfRef (Named NamedName r))
    toAbstract (r -> Named NamedName r
    forall a name. a -> Named name a
    unnamed r
    x)

    instance ToAbstract r => ToAbstract [Arg r] where
      type AbsOfRef [Arg r] = [NamedArg (AbsOfRef r)]

    -- instance ToAbstract r A.Expr => ToAbstract (Dom r, Name) (A.TypedBinding) where
    instance (ToAbstract r, AbsOfRef r ~ A.Expr) => ToAbstract (Dom r, Name) where
      type AbsOfRef (Dom r, Name) = A.TypedBinding
      toAbstract :: forall (m :: * -> *).
    MonadReflectedToAbstract m =>
    (Dom r, Name) -> m (AbsOfRef (Dom r, Name))
    toAbstract (Dom{domInfo :: forall t e. Dom' t e -> ArgInfo
    domInfo = ArgInfo
    i, domIsFinite :: forall t e. Dom' t e -> Bool
    domIsFinite = Bool
    isfin, unDom :: forall t e. Dom' t e -> e
    unDom = r
    x, domTactic :: forall t e. Dom' t e -> Maybe t
    domTactic = Maybe Term
    tac}, Name
    name) = do
        dom <- r -> m (AbsOfRef r)
    forall r (m :: * -> *).
    (ToAbstract r, MonadReflectedToAbstract m) =>
    r -> m (AbsOfRef r)
    forall (m :: * -> *).
    MonadReflectedToAbstract m =>
    r -> m (AbsOfRef r)
    toAbstract r
    x
        -- TODO(Amy): Anyone know why this discards the tactic? It was like
        -- that when I got here!
        return $ A.TBind noRange
          (A.TypedBindingInfo empty isfin)
          (singleton $ unnamedArg i $ A.mkBinder_ name)
          dom

    instance ToAbstract (A.Expr, Elim) where
      type AbsOfRef (A.Expr, Elim) = A.Expr
      toAbstract :: forall (m :: * -> *).
    MonadReflectedToAbstract m =>
    (Expr, Elim) -> m (AbsOfRef (Expr, Elim))
    toAbstract (Expr
    f, Apply Arg Type
    arg) = do
        arg     <- Arg Type -> m (AbsOfRef (Arg Type))
    forall r (m :: * -> *).
    (ToAbstract r, MonadReflectedToAbstract m) =>
    r -> m (AbsOfRef r)
    forall (m :: * -> *).
    MonadReflectedToAbstract m =>
    Arg Type -> m (AbsOfRef (Arg Type))
    toAbstract Arg Type
    arg
        showImp <- showImplicitArguments
        return $ if showImp || visible arg
                 then A.App (setOrigin Reflected defaultAppInfo_) f arg
                 else f

    instance ToAbstract (A.Expr, Elims) where
      type AbsOfRef (A.Expr, Elims) = A.Expr
      toAbstract :: forall (m :: * -> *).
    MonadReflectedToAbstract m =>
    (Expr, Elims) -> m (AbsOfRef (Expr, Elims))
    toAbstract (Expr
    f, Elims
    elims) = (Expr -> Elim -> m Expr) -> Expr -> Elims -> m Expr
    forall (t :: * -> *) (m :: * -> *) b a.
    (Foldable t, Monad m) =>
    (b -> a -> m b) -> b -> t a -> m b
    foldM (((Expr, Elim) -> m Expr) -> Expr -> Elim -> m Expr
    forall a b c. ((a, b) -> c) -> a -> b -> c
    curry (Expr, Elim) -> m Expr
    (Expr, Elim) -> m (AbsOfRef (Expr, Elim))
    forall r (m :: * -> *).
    (ToAbstract r, MonadReflectedToAbstract m) =>
    r -> m (AbsOfRef r)
    forall (m :: * -> *).
    MonadReflectedToAbstract m =>
    (Expr, Elim) -> m (AbsOfRef (Expr, Elim))
    toAbstract) Expr
    f Elims
    elims

    instance ToAbstract r => ToAbstract (R.Abs r) where
      type AbsOfRef (R.Abs r) = (AbsOfRef r, Name)
      toAbstract :: forall (m :: * -> *).
    MonadReflectedToAbstract m =>
    Abs r -> m (AbsOfRef (Abs r))
    toAbstract (Abs String
    s r
    x) = String -> (Name -> m (AbsOfRef (Abs r))) -> m (AbsOfRef (Abs r))
    forall (m :: * -> *) a.
    MonadReflectedToAbstract m =>
    String -> (Name -> m a) -> m a
    withName String
    s' ((Name -> m (AbsOfRef (Abs r))) -> m (AbsOfRef (Abs r)))
    -> (Name -> m (AbsOfRef (Abs r))) -> m (AbsOfRef (Abs r))
    forall a b. (a -> b) -> a -> b
    $ \Name
    name -> (,Name
    name) (AbsOfRef r -> (AbsOfRef r, Name))
    -> m (AbsOfRef r) -> m (AbsOfRef r, Name)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> r -> m (AbsOfRef r)
    forall r (m :: * -> *).
    (ToAbstract r, MonadReflectedToAbstract m) =>
    r -> m (AbsOfRef r)
    forall (m :: * -> *).
    MonadReflectedToAbstract m =>
    r -> m (AbsOfRef r)
    toAbstract r
    x
        where s' :: String
    s' = if (String -> Bool
    forall a. IsNoName a => a -> Bool
    isNoName String
    s) then String
    "z" else String
    s -- TODO: only do this when var is free

    instance ToAbstract Literal where
      type AbsOfRef Literal = A.Expr
      toAbstract :: forall (m :: * -> *).
    MonadReflectedToAbstract m =>
    Literal -> m (AbsOfRef Literal)
    toAbstract Literal
    l = Expr -> m Expr
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Expr -> m Expr) -> Expr -> m Expr
    forall a b. (a -> b) -> a -> b
    $ ExprInfo -> Literal -> Expr
    A.Lit ExprInfo
    forall a. Null a => a
    empty Literal
    l

    instance ToAbstract Term where
      type AbsOfRef Term = A.Expr
      toAbstract :: forall (m :: * -> *).
    MonadReflectedToAbstract m =>
    Type -> m (AbsOfRef Type)
    toAbstract = \case
        R.Var Int
    i Elims
    es -> do
          name <- Int -> m Name
    forall (m :: * -> *). MonadReflectedToAbstract m => Int -> m Name
    mkVarName Int
    i
          toAbstract (A.Var name, es)
        R.Con QName
    c Elims
    es -> (Expr, Elims) -> m (AbsOfRef (Expr, Elims))
    forall r (m :: * -> *).
    (ToAbstract r, MonadReflectedToAbstract m) =>
    r -> m (AbsOfRef r)
    forall (m :: * -> *).
    MonadReflectedToAbstract m =>
    (Expr, Elims) -> m (AbsOfRef (Expr, Elims))
    toAbstract (AmbiguousQName -> Expr
    A.Con (QName -> AmbiguousQName
    unambiguous (QName -> AmbiguousQName) -> QName -> AmbiguousQName
    forall a b. (a -> b) -> a -> b
    $ KillRangeT QName
    forall a. KillRange a => KillRangeT a
    killRange QName
    c), Elims
    es)
        R.Def QName
    f Elims
    es -> do
          af <- QName -> m Expr
    forall (m :: * -> *). HasConstInfo m => QName -> m Expr
    mkDef (KillRangeT QName
    forall a. KillRange a => KillRangeT a
    killRange QName
    f)
          toAbstract (af, es)
        R.Lam Hiding
    h Abs Type
    t  -> do
          (e, name) <- Abs Type -> m (AbsOfRef (Abs Type))
    forall r (m :: * -> *).
    (ToAbstract r, MonadReflectedToAbstract m) =>
    r -> m (AbsOfRef r)
    forall (m :: * -> *).
    MonadReflectedToAbstract m =>
    Abs Type -> m (AbsOfRef (Abs Type))
    toAbstract Abs Type
    t
          let info  = Hiding -> ArgInfo -> ArgInfo
    forall a. LensHiding a => Hiding -> a -> a
    setHiding Hiding
    h (ArgInfo -> ArgInfo) -> ArgInfo -> ArgInfo
    forall a b. (a -> b) -> a -> b
    $ Origin -> ArgInfo -> ArgInfo
    forall a. LensOrigin a => Origin -> a -> a
    setOrigin Origin
    Reflected ArgInfo
    defaultArgInfo
          return $ A.Lam exprNoRange (A.mkDomainFree $ unnamedArg info $ A.mkBinder_ name) e
        R.ExtLam List1 Clause
    cs Elims
    es -> do
          name <- String -> m Name
    forall a (m :: * -> *).
    (FreshName a, MonadFresh NameId m) =>
    a -> m Name
    forall (m :: * -> *). MonadFresh NameId m => String -> m Name
    freshName_ String
    extendedLambdaName
          m    <- getCurrentModule
          let qname   = ModuleName -> Name -> QName
    qualify ModuleName
    m Name
    name
              cname   = Name -> Name
    nameConcrete Name
    name
              defInfo = Name -> Fixity' -> Access -> IsAbstract -> Range -> DefInfo' Expr
    forall t.
    Name -> Fixity' -> Access -> IsAbstract -> Range -> DefInfo' t
    mkDefInfo Name
    cname Fixity'
    noFixity' Access
    PublicAccess IsAbstract
    ConcreteDef Range
    forall a. Range' a
    noRange
          cs <- toAbstract $ fmap (QNamed qname) cs
          toAbstract
            (A.ExtendedLam exprNoRange defInfo defaultErased qname cs, es)
        R.Pi Dom Type
    a Abs Type
    b   -> do
          (b, name) <- Abs Type -> m (AbsOfRef (Abs Type))
    forall r (m :: * -> *).
    (ToAbstract r, MonadReflectedToAbstract m) =>
    r -> m (AbsOfRef r)
    forall (m :: * -> *).
    MonadReflectedToAbstract m =>
    Abs Type -> m (AbsOfRef (Abs Type))
    toAbstract Abs Type
    b
          a         <- toAbstract (a, name)
          return $ A.Pi exprNoRange (singleton a) b
        R.Sort Sort
    s   -> Sort -> m (AbsOfRef Sort)
    forall r (m :: * -> *).
    (ToAbstract r, MonadReflectedToAbstract m) =>
    r -> m (AbsOfRef r)
    forall (m :: * -> *).
    MonadReflectedToAbstract m =>
    Sort -> m (AbsOfRef Sort)
    toAbstract Sort
    s
        R.Lit Literal
    l    -> Literal -> m (AbsOfRef Literal)
    forall r (m :: * -> *).
    (ToAbstract r, MonadReflectedToAbstract m) =>
    r -> m (AbsOfRef r)
    forall (m :: * -> *).
    MonadReflectedToAbstract m =>
    Literal -> m (AbsOfRef Literal)
    toAbstract Literal
    l
        R.Meta MetaId
    x Elims
    es    -> do
          info <- m MetaInfo
    forall (m :: * -> *). ReadTCState m => m MetaInfo
    mkMetaInfo
          let info' = MetaInfo
    info{ metaNumber = Just x }
          toAbstract (A.Underscore info', es)
        Type
    R.Unknown      -> MetaInfo -> Expr
    A.Underscore (MetaInfo -> Expr) -> m MetaInfo -> m Expr
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m MetaInfo
    forall (m :: * -> *). ReadTCState m => m MetaInfo
    mkMetaInfo

    mkMetaInfo :: ReadTCState m => m MetaInfo
    mkMetaInfo :: forall (m :: * -> *). ReadTCState m => m MetaInfo
    mkMetaInfo = do
      scope <- m ScopeInfo
    forall (m :: * -> *). ReadTCState m => m ScopeInfo
    getScope
      return $ emptyMetaInfo { metaScope = scope }

    mkDef :: HasConstInfo m => QName -> m A.Expr
    mkDef :: forall (m :: * -> *). HasConstInfo m => QName -> m Expr
    mkDef QName
    f = QName -> m Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    f m Definition -> (Definition -> Defn) -> m Defn
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> Definition -> Defn
    theDef m Defn -> (Defn -> Expr) -> m Expr
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \case

      Constructor{}
        -> AmbiguousQName -> Expr
    A.Con (AmbiguousQName -> Expr) -> AmbiguousQName -> Expr
    forall a b. (a -> b) -> a -> b
    $ QName -> AmbiguousQName
    unambiguous QName
    f

      Function{ funProjection :: Defn -> Either ProjectionLikenessMissing Projection
    funProjection = Right Projection{ projProper :: Projection -> Maybe QName
    projProper = Just{} } }
        -> ProjOrigin -> AmbiguousQName -> Expr
    A.Proj ProjOrigin
    ProjSystem (AmbiguousQName -> Expr) -> AmbiguousQName -> Expr
    forall a b. (a -> b) -> a -> b
    $ QName -> AmbiguousQName
    unambiguous QName
    f

      d :: Defn
    d@Function{} | Defn -> Bool
    isMacro Defn
    d
        -> QName -> Expr
    A.Macro QName
    f

      Defn
    _ -> QName -> Expr
    A.Def QName
    f

    mkApp :: A.Expr -> A.Expr -> A.Expr
    mkApp :: Expr -> Expr -> Expr
    mkApp Expr
    e1 Expr
    e2 = AppInfo -> Expr -> Arg (Named_ Expr) -> Expr
    A.App (Origin -> AppInfo -> AppInfo
    forall a. LensOrigin a => Origin -> a -> a
    setOrigin Origin
    Reflected AppInfo
    defaultAppInfo_) Expr
    e1 (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
    e2

    mkVar :: MonadReflectedToAbstract m => Int -> m (Name, R.Type)
    mkVar :: forall (m :: * -> *).
    MonadReflectedToAbstract m =>
    Int -> m (Name, Type)
    mkVar Int
    i = m (Maybe (Name, Type))
    -> ((Name, Type) -> m (Name, Type))
    -> m (Name, Type)
    -> m (Name, Type)
    forall (m :: * -> *) a b.
    Monad m =>
    m (Maybe a) -> (a -> m b) -> m b -> m b
    ifJustM (Int -> m (Maybe (Name, Type))
    forall (m :: * -> *).
    MonadReflectedToAbstract m =>
    Int -> m (Maybe (Name, Type))
    askVar Int
    i) (Name, Type) -> m (Name, Type)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (m (Name, Type) -> m (Name, Type))
    -> m (Name, Type) -> m (Name, Type)
    forall a b. (a -> b) -> a -> b
    $ do
      cxt   <- m Telescope
    forall (m :: * -> *). MonadTCEnv m => m Telescope
    getContextTelescope
      names <- asks $ drop (size cxt) . reverse . map fst
      withShowAllArguments' False $ typeError $ DeBruijnIndexOutOfScope i cxt names

    mkVarName :: MonadReflectedToAbstract m => Int -> m Name
    mkVarName :: forall (m :: * -> *). MonadReflectedToAbstract m => Int -> m Name
    mkVarName Int
    i = (Name, Type) -> Name
    forall a b. (a, b) -> a
    fst ((Name, Type) -> Name) -> m (Name, Type) -> m Name
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Int -> m (Name, Type)
    forall (m :: * -> *).
    MonadReflectedToAbstract m =>
    Int -> m (Name, Type)
    mkVar Int
    i

    instance ToAbstract Sort where
      type AbsOfRef Sort = A.Expr
      toAbstract :: forall (m :: * -> *).
    MonadReflectedToAbstract m =>
    Sort -> m (AbsOfRef Sort)
    toAbstract Sort
    s = do
        setName <- QName -> Maybe QName -> QName
    forall a. a -> Maybe a -> a
    fromMaybe QName
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe QName -> QName) -> m (Maybe QName) -> m QName
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> BuiltinId -> m (Maybe QName)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe QName)
    getBuiltinName' BuiltinId
    builtinSet
        propName <- fromMaybe __IMPOSSIBLE__ <$> getBuiltinName' builtinProp
        infName <- fromMaybe __IMPOSSIBLE__ <$> getBuiltinName' builtinSetOmega
        case s of
          SetS Type
    x -> Expr -> Expr -> Expr
    mkApp (QName -> Expr
    A.Def QName
    setName) (Expr -> Expr) -> m Expr -> m Expr
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Type -> m (AbsOfRef Type)
    forall r (m :: * -> *).
    (ToAbstract r, MonadReflectedToAbstract m) =>
    r -> m (AbsOfRef r)
    forall (m :: * -> *).
    MonadReflectedToAbstract m =>
    Type -> m (AbsOfRef Type)
    toAbstract Type
    x
          LitS Integer
    x -> Expr -> m Expr
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Expr -> m Expr) -> Expr -> m Expr
    forall a b. (a -> b) -> a -> b
    $ QName -> Suffix -> Expr
    A.Def' QName
    setName (Suffix -> Expr) -> Suffix -> Expr
    forall a b. (a -> b) -> a -> b
    $ Integer -> Suffix
    A.Suffix Integer
    x
          PropS Type
    x -> Expr -> Expr -> Expr
    mkApp (QName -> Expr
    A.Def QName
    propName) (Expr -> Expr) -> m Expr -> m Expr
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Type -> m (AbsOfRef Type)
    forall r (m :: * -> *).
    (ToAbstract r, MonadReflectedToAbstract m) =>
    r -> m (AbsOfRef r)
    forall (m :: * -> *).
    MonadReflectedToAbstract m =>
    Type -> m (AbsOfRef Type)
    toAbstract Type
    x
          PropLitS Integer
    x -> Expr -> m Expr
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Expr -> m Expr) -> Expr -> m Expr
    forall a b. (a -> b) -> a -> b
    $ QName -> Suffix -> Expr
    A.Def' QName
    propName (Suffix -> Expr) -> Suffix -> Expr
    forall a b. (a -> b) -> a -> b
    $ Integer -> Suffix
    A.Suffix Integer
    x
          InfS Integer
    x -> Expr -> m Expr
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Expr -> m Expr) -> Expr -> m Expr
    forall a b. (a -> b) -> a -> b
    $ QName -> Suffix -> Expr
    A.Def' QName
    infName (Suffix -> Expr) -> Suffix -> Expr
    forall a b. (a -> b) -> a -> b
    $ Integer -> Suffix
    A.Suffix Integer
    x
          Sort
    UnknownS -> Expr -> Expr -> Expr
    mkApp (QName -> Expr
    A.Def QName
    setName) (Expr -> Expr) -> (MetaInfo -> Expr) -> MetaInfo -> Expr
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . MetaInfo -> Expr
    A.Underscore (MetaInfo -> Expr) -> m MetaInfo -> m Expr
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m MetaInfo
    forall (m :: * -> *). ReadTCState m => m MetaInfo
    mkMetaInfo

    instance ToAbstract R.Pattern where
      type AbsOfRef R.Pattern = A.Pattern
      toAbstract :: forall (m :: * -> *).
    MonadReflectedToAbstract m =>
    Pattern -> m (AbsOfRef Pattern)
    toAbstract Pattern
    pat = case Pattern
    pat of
        R.ConP QName
    c [Arg Pattern]
    args -> do
          args <- [Arg Pattern] -> m (AbsOfRef [Arg Pattern])
    forall r (m :: * -> *).
    (ToAbstract r, MonadReflectedToAbstract m) =>
    r -> m (AbsOfRef r)
    forall (m :: * -> *).
    MonadReflectedToAbstract m =>
    [Arg Pattern] -> m (AbsOfRef [Arg Pattern])
    toAbstract [Arg Pattern]
    args
          return $ A.ConP (ConPatInfo ConOCon patNoRange ConPatEager) (unambiguous $ killRange c) args
        R.DotP Type
    t -> PatInfo -> Expr -> Pattern' Expr
    forall e. PatInfo -> e -> Pattern' e
    A.DotP PatInfo
    patNoRange (Expr -> Pattern' Expr) -> m Expr -> m (Pattern' Expr)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Type -> m (AbsOfRef Type)
    forall r (m :: * -> *).
    (ToAbstract r, MonadReflectedToAbstract m) =>
    r -> m (AbsOfRef r)
    forall (m :: * -> *).
    MonadReflectedToAbstract m =>
    Type -> m (AbsOfRef Type)
    toAbstract Type
    t
        R.VarP Int
    i -> do
          (x, _t) <- Int -> m (Name, Type)
    forall (m :: * -> *).
    MonadReflectedToAbstract m =>
    Int -> m (Name, Type)
    mkVar Int
    i
          return $ A.VarP $ A.mkBindName x
        R.LitP Literal
    l  -> AbsOfRef Pattern -> m (AbsOfRef Pattern)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (AbsOfRef Pattern -> m (AbsOfRef Pattern))
    -> AbsOfRef Pattern -> m (AbsOfRef Pattern)
    forall a b. (a -> b) -> a -> b
    $ PatInfo -> Literal -> Pattern' Expr
    forall e. PatInfo -> Literal -> Pattern' e
    A.LitP PatInfo
    patNoRange Literal
    l
        R.AbsurdP Int
    _i -> AbsOfRef Pattern -> m (AbsOfRef Pattern)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (AbsOfRef Pattern -> m (AbsOfRef Pattern))
    -> AbsOfRef Pattern -> m (AbsOfRef Pattern)
    forall a b. (a -> b) -> a -> b
    $ PatInfo -> Pattern' Expr
    forall e. PatInfo -> Pattern' e
    A.AbsurdP PatInfo
    patNoRange
        R.ProjP QName
    d -> AbsOfRef Pattern -> m (AbsOfRef Pattern)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (AbsOfRef Pattern -> m (AbsOfRef Pattern))
    -> AbsOfRef Pattern -> m (AbsOfRef Pattern)
    forall a b. (a -> b) -> a -> b
    $ PatInfo -> ProjOrigin -> AmbiguousQName -> Pattern' Expr
    forall e. PatInfo -> ProjOrigin -> AmbiguousQName -> Pattern' e
    A.ProjP PatInfo
    patNoRange ProjOrigin
    ProjSystem (AmbiguousQName -> Pattern' Expr)
    -> AmbiguousQName -> Pattern' Expr
    forall a b. (a -> b) -> a -> b
    $ QName -> AmbiguousQName
    unambiguous (QName -> AmbiguousQName) -> QName -> AmbiguousQName
    forall a b. (a -> b) -> a -> b
    $ KillRangeT QName
    forall a. KillRange a => KillRangeT a
    killRange QName
    d

    instance ToAbstract (QNamed R.Clause) where
      type AbsOfRef (QNamed R.Clause) = A.Clause

      toAbstract :: forall (m :: * -> *).
    MonadReflectedToAbstract m =>
    QNamed Clause -> m (AbsOfRef (QNamed Clause))
    toAbstract (QNamed QName
    name (R.Clause [(Text, Arg Type)]
    tel [Arg Pattern]
    pats Type
    rhs)) = [(String, Type)]
    -> ([Name] -> m (AbsOfRef (QNamed Clause)))
    -> m (AbsOfRef (QNamed Clause))
    forall (m :: * -> *) a.
    MonadReflectedToAbstract m =>
    [(String, Type)] -> ([Name] -> m a) -> m a
    withVars (((Text, Arg Type) -> (String, Type))
    -> [(Text, Arg Type)] -> [(String, Type)]
    forall a b. (a -> b) -> [a] -> [b]
    map (Text -> String
    Text.unpack (Text -> String)
    -> (Arg Type -> Type) -> (Text, Arg Type) -> (String, Type)
    forall b c b' c'. (b -> c) -> (b' -> c') -> (b, b') -> (c, c')
    forall (a :: * -> * -> *) b c b' c'.
    Arrow a =>
    a b c -> a b' c' -> a (b, b') (c, c')
    *** Arg Type -> Type
    forall e. Arg e -> e
    unArg) [(Text, Arg Type)]
    tel) (([Name] -> m (AbsOfRef (QNamed Clause)))
     -> m (AbsOfRef (QNamed Clause)))
    -> ([Name] -> m (AbsOfRef (QNamed Clause)))
    -> m (AbsOfRef (QNamed Clause))
    forall a b. (a -> b) -> a -> b
    $ \[Name]
    _ -> do
        [(Text, Arg Type)] -> [Arg Pattern] -> m ()
    forall (m :: * -> *).
    MonadReflectedToAbstract m =>
    [(Text, Arg Type)] -> [Arg Pattern] -> m ()
    checkClauseTelescopeBindings [(Text, Arg Type)]
    tel [Arg Pattern]
    pats
        pats <- [Arg Pattern] -> m (AbsOfRef [Arg Pattern])
    forall r (m :: * -> *).
    (ToAbstract r, MonadReflectedToAbstract m) =>
    r -> m (AbsOfRef r)
    forall (m :: * -> *).
    MonadReflectedToAbstract m =>
    [Arg Pattern] -> m (AbsOfRef [Arg Pattern])
    toAbstract [Arg Pattern]
    pats
        rhs  <- toAbstract rhs
        let lhs = SpineLHS -> LHS
    forall a b. LHSToSpine a b => b -> a
    spineToLhs (SpineLHS -> LHS) -> SpineLHS -> LHS
    forall a b. (a -> b) -> a -> b
    $ LHSInfo -> QName -> NAPs Expr -> SpineLHS
    A.SpineLHS LHSInfo
    forall a. Null a => a
    empty QName
    name NAPs Expr
    pats
        return $ A.Clause lhs [] (A.RHS rhs Nothing) A.noWhereDecls empty
      toAbstract (QNamed QName
    name (R.AbsurdClause [(Text, Arg Type)]
    tel [Arg Pattern]
    pats)) = [(String, Type)]
    -> ([Name] -> m (AbsOfRef (QNamed Clause)))
    -> m (AbsOfRef (QNamed Clause))
    forall (m :: * -> *) a.
    MonadReflectedToAbstract m =>
    [(String, Type)] -> ([Name] -> m a) -> m a
    withVars (((Text, Arg Type) -> (String, Type))
    -> [(Text, Arg Type)] -> [(String, Type)]
    forall a b. (a -> b) -> [a] -> [b]
    map (Text -> String
    Text.unpack (Text -> String)
    -> (Arg Type -> Type) -> (Text, Arg Type) -> (String, Type)
    forall b c b' c'. (b -> c) -> (b' -> c') -> (b, b') -> (c, c')
    forall (a :: * -> * -> *) b c b' c'.
    Arrow a =>
    a b c -> a b' c' -> a (b, b') (c, c')
    *** Arg Type -> Type
    forall e. Arg e -> e
    unArg) [(Text, Arg Type)]
    tel) (([Name] -> m (AbsOfRef (QNamed Clause)))
     -> m (AbsOfRef (QNamed Clause)))
    -> ([Name] -> m (AbsOfRef (QNamed Clause)))
    -> m (AbsOfRef (QNamed Clause))
    forall a b. (a -> b) -> a -> b
    $ \[Name]
    _ -> do
        [(Text, Arg Type)] -> [Arg Pattern] -> m ()
    forall (m :: * -> *).
    MonadReflectedToAbstract m =>
    [(Text, Arg Type)] -> [Arg Pattern] -> m ()
    checkClauseTelescopeBindings [(Text, Arg Type)]
    tel [Arg Pattern]
    pats
        pats <- [Arg Pattern] -> m (AbsOfRef [Arg Pattern])
    forall r (m :: * -> *).
    (ToAbstract r, MonadReflectedToAbstract m) =>
    r -> m (AbsOfRef r)
    forall (m :: * -> *).
    MonadReflectedToAbstract m =>
    [Arg Pattern] -> m (AbsOfRef [Arg Pattern])
    toAbstract [Arg Pattern]
    pats
        let lhs = SpineLHS -> LHS
    forall a b. LHSToSpine a b => b -> a
    spineToLhs (SpineLHS -> LHS) -> SpineLHS -> LHS
    forall a b. (a -> b) -> a -> b
    $ LHSInfo -> QName -> NAPs Expr -> SpineLHS
    A.SpineLHS LHSInfo
    forall a. Null a => a
    empty QName
    name NAPs Expr
    pats
        return $ A.Clause lhs [] A.AbsurdRHS A.noWhereDecls empty

    instance ToAbstract [QNamed R.Clause] where
      type AbsOfRef [QNamed R.Clause] = [A.Clause]
      toAbstract :: forall (m :: * -> *).
    MonadReflectedToAbstract m =>
    [QNamed Clause] -> m (AbsOfRef [QNamed Clause])
    toAbstract = (QNamed Clause -> m Clause) -> [QNamed Clause] -> m [Clause]
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> [a] -> f [b]
    traverse QNamed Clause -> m Clause
    QNamed Clause -> m (AbsOfRef (QNamed Clause))
    forall r (m :: * -> *).
    (ToAbstract r, MonadReflectedToAbstract m) =>
    r -> m (AbsOfRef r)
    forall (m :: * -> *).
    MonadReflectedToAbstract m =>
    QNamed Clause -> m (AbsOfRef (QNamed Clause))
    toAbstract

    instance ToAbstract (List1 (QNamed R.Clause)) where
      type AbsOfRef (List1 (QNamed R.Clause)) = List1 A.Clause
      toAbstract :: forall (m :: * -> *).
    MonadReflectedToAbstract m =>
    NonEmpty (QNamed Clause) -> m (AbsOfRef (NonEmpty (QNamed Clause)))
    toAbstract = (QNamed Clause -> m Clause)
    -> NonEmpty (QNamed Clause) -> m (List1 Clause)
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> NonEmpty a -> f (NonEmpty b)
    traverse QNamed Clause -> m Clause
    QNamed Clause -> m (AbsOfRef (QNamed Clause))
    forall r (m :: * -> *).
    (ToAbstract r, MonadReflectedToAbstract m) =>
    r -> m (AbsOfRef r)
    forall (m :: * -> *).
    MonadReflectedToAbstract m =>
    QNamed Clause -> m (AbsOfRef (QNamed Clause))
    toAbstract

    -- | Check that all variables in the telescope are bound in the left-hand side. Since we check the
    --   telescope by attaching type annotations to the pattern variables there needs to be somewhere to
    --   put the annotation. Also, since the lhs is where the variables are actually bound, missing a
    --   binding for a variable that's used later in the telescope causes unbound variable panic
    --   (see #5044).
    checkClauseTelescopeBindings :: MonadReflectedToAbstract m => [(Text, Arg R.Type)] -> [Arg R.Pattern] -> m ()
    checkClauseTelescopeBindings :: forall (m :: * -> *).
    MonadReflectedToAbstract m =>
    [(Text, Arg Type)] -> [Arg Pattern] -> m ()
    checkClauseTelescopeBindings [(Text, Arg Type)]
    tel [Arg Pattern]
    pats =
      case [Text] -> [Text]
    forall a. [a] -> [a]
    reverse [ Text
    x | ((Text
    x, Arg Type
    _), Int
    i) <- [(Text, Arg Type)] -> [Int] -> [((Text, Arg Type), Int)]
    forall a b. [a] -> [b] -> [(a, b)]
    zip ([(Text, Arg Type)] -> [(Text, Arg Type)]
    forall a. [a] -> [a]
    reverse [(Text, Arg Type)]
    tel) [Int
    0..], Bool -> Bool
    not (Bool -> Bool) -> Bool -> Bool
    forall a b. (a -> b) -> a -> b
    $ Int -> Set Int -> Bool
    forall a. Ord a => a -> Set a -> Bool
    Set.member Int
    i Set Int
    bs ] of
        [] -> () -> m ()
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
        [Text]
    xs -> Doc -> m ()
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    Doc -> m a
    genericDocError (Doc -> m ()) -> Doc -> m ()
    forall a b. (a -> b) -> a -> b
    $ [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    vcat
          [ [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    fsep (String -> [Doc]
    pwords String
    "Missing bindings for telescope" [Doc] -> [Doc] -> [Doc]
    forall a. [a] -> [a] -> [a]
    ++ [ [Text] -> Doc -> Doc
    forall a. Sized a => a -> Doc -> Doc
    pluralS [Text]
    xs Doc
    "variable" ])
            Doc -> Doc -> Doc
    <?> ([Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    fsep (Doc -> [Doc] -> [Doc]
    forall (t :: * -> *). Foldable t => Doc -> t Doc -> [Doc]
    punctuate Doc
    ", " ([Doc] -> [Doc]) -> [Doc] -> [Doc]
    forall a b. (a -> b) -> a -> b
    $ (Text -> Doc) -> [Text] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map (String -> Doc
    forall a. String -> Doc a
    text (String -> Doc) -> (Text -> String) -> Text -> Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Text -> String
    Text.unpack) [Text]
    xs) Doc -> Doc -> Doc
    forall a. Semigroup a => a -> a -> a
    <> Doc
    ".")
          , Doc
    "All variables in the clause telescope must be bound in the left-hand side."
          ]
      where
        bs :: Set Int
    bs = [Arg Pattern] -> Set Int
    boundVars [Arg Pattern]
    pats

        boundVars :: [Arg Pattern] -> Set Int
    boundVars = [Set Int] -> Set Int
    forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
    Set.unions ([Set Int] -> Set Int)
    -> ([Arg Pattern] -> [Set Int]) -> [Arg Pattern] -> Set Int
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Arg Pattern -> Set Int) -> [Arg Pattern] -> [Set Int]
    forall a b. (a -> b) -> [a] -> [b]
    map (Pattern -> Set Int
    bound (Pattern -> Set Int)
    -> (Arg Pattern -> Pattern) -> Arg Pattern -> Set Int
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Arg Pattern -> Pattern
    forall e. Arg e -> e
    unArg)
        bound :: Pattern -> Set Int
    bound (R.VarP Int
    i)    = Int -> Set Int
    forall a. a -> Set a
    Set.singleton Int
    i
        bound (R.ConP QName
    _ [Arg Pattern]
    ps) = [Arg Pattern] -> Set Int
    boundVars [Arg Pattern]
    ps
        bound R.DotP{}      = Set Int
    forall a. Set a
    Set.empty
        bound R.LitP{}      = Set Int
    forall a. Set a
    Set.empty
        bound (R.AbsurdP Int
    i) = Int -> Set Int
    forall a. a -> Set a
    Set.singleton Int
    i
        bound R.ProjP{}     = Set Int
    forall a. Set a
    Set.empty