    -- | Functions for abstracting terms over other terms.
    module Agda.TypeChecking.Abstract where

    import Control.Monad
    import Control.Monad.Except

    import Data.Function
    import qualified Data.HashMap.Strict as HMap

    import Agda.Syntax.Common
    import Agda.Syntax.Internal

    import Agda.TypeChecking.MetaVars
    import Agda.TypeChecking.Monad
    import Agda.TypeChecking.Monad.Builtin ( equalityUnview, primEqualityName )
    import Agda.TypeChecking.Substitute
    import Agda.TypeChecking.CheckInternal
    import Agda.TypeChecking.Conversion
    import Agda.TypeChecking.Constraints
    import Agda.TypeChecking.Pretty
    import Agda.TypeChecking.Sort
    import Agda.TypeChecking.Telescope

    import Agda.Utils.Functor
    import Agda.Utils.List ( splitExactlyAt, dropEnd )
    import Agda.Utils.Impossible

    -- | @abstractType a v b[v] = b@ where @a : v@.
    abstractType :: Type -> Term -> Type -> TCM Type
    abstractType :: Type -> Term -> Type -> TCM Type
    abstractType Type
    a Term
    v (El Sort' Term
    s Term
    b) = Sort' Term -> Term -> Type
    forall t a. Sort' t -> a -> Type'' t a
    El (Term -> Sort' Term -> Sort' Term
    forall a. AbsTerm a => Term -> a -> a
    absTerm Term
    v Sort' Term
    s) (Term -> Type) -> TCMT IO Term -> TCM Type
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Type -> Term -> Type -> Term -> TCMT IO Term
    abstractTerm Type
    a Term
    v (Sort' Term -> Type
    sort Sort' Term
    s) Term
    b

    -- | @piAbstractTerm NotHidden v a b[v] = (w : a) -> b[w]@
    --   @piAbstractTerm Hidden    v a b[v] = {w : a} -> b[w]@
    piAbstractTerm :: ArgInfo -> Term -> Type -> Type -> TCM Type
    piAbstractTerm :: ArgInfo -> Term -> Type -> Type -> TCM Type
    piAbstractTerm ArgInfo
    info Term
    v Type
    a Type
    b = do
      Type
    fun <- Dom (String, Type) -> Type -> Type
    mkPi (ArgInfo -> Dom (String, Type) -> Dom (String, Type)
    forall a. LensArgInfo a => ArgInfo -> a -> a
    setArgInfo ArgInfo
    info (Dom (String, Type) -> Dom (String, Type))
    -> Dom (String, Type) -> Dom (String, Type)
    forall a b. (a -> b) -> a -> b
    $ (String, Type) -> Dom (String, Type)
    forall a. a -> Dom a
    defaultDom (String
    "w", Type
    a)) (Type -> Type) -> TCM Type -> TCM Type
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Type -> Term -> Type -> TCM Type
    abstractType Type
    a Term
    v Type
    b
      String -> Nat -> TCMT IO Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Nat -> TCMT IO Doc -> m ()
    reportSDoc String
    "tc.abstract" Nat
    50 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $
        [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep [ TCMT IO Doc
    "piAbstract" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep [ Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Term
    v TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> TCMT IO Doc
    ":", Nat -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
    nest Nat
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ Type -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Type
    a ]
            , Nat -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
    nest Nat
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "from" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Type -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Type
    b
            , Nat -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
    nest Nat
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "-->" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Type -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Type
    fun ]
      String -> Nat -> TCMT IO Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Nat -> TCMT IO Doc -> m ()
    reportSDoc String
    "tc.abstract" Nat
    70 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $
        [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep [ TCMT IO Doc
    "piAbstract" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep [ (String -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => String -> m Doc
    text (String -> TCMT IO Doc) -> (Term -> String) -> Term -> TCMT IO Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Term -> String
    forall a. Show a => a -> String
    show) Term
    v TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> TCMT IO Doc
    ":", Nat -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
    nest Nat
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ (String -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => String -> m Doc
    text (String -> TCMT IO Doc) -> (Type -> String) -> Type -> TCMT IO Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Type -> String
    forall a. Show a => a -> String
    show) Type
    a ]
            , Nat -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
    nest Nat
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "from" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> (String -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => String -> m Doc
    text (String -> TCMT IO Doc) -> (Type -> String) -> Type -> TCMT IO Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Type -> String
    forall a. Show a => a -> String
    show) Type
    b
            , Nat -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
    nest Nat
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "-->" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> (String -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => String -> m Doc
    text (String -> TCMT IO Doc) -> (Type -> String) -> Type -> TCMT IO Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Type -> String
    forall a. Show a => a -> String
    show) Type
    fun ]
      Type -> TCM Type
    forall (m :: * -> *) a. Monad m => a -> m a
    return Type
    fun

    -- | @piAbstract (v, a) b[v] = (w : a) -> b[w]@
    --
    --   For the inspect idiom, it does something special:
    --   @piAbstract (v, a) b[v] = (w : a) {w' : Eq a w v} -> b[w]
    --
    --   For @rewrite@, it does something special:
    --   @piAbstract (prf, Eq a v v') b[v,prf] = (w : a) (w' : Eq a w v') -> b[w,w']@

    piAbstract :: Arg (Term, EqualityView) -> Type -> TCM Type
    piAbstract :: Arg (Term, EqualityView) -> Type -> TCM Type
    piAbstract (Arg ArgInfo
    info (Term
    v, OtherType Type
    a)) Type
    b = ArgInfo -> Term -> Type -> Type -> TCM Type
    piAbstractTerm ArgInfo
    info Term
    v Type
    a Type
    b
    piAbstract (Arg ArgInfo
    info (Term
    v, IdiomType Type
    a)) Type
    b = do
      Type
    b  <- Nat -> Type -> Type
    forall a. Subst a => Nat -> a -> a
    raise Nat
    1 (Type -> Type) -> TCM Type -> TCM Type
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Type -> Term -> Type -> TCM Type
    abstractType Type
    a Term
    v Type
    b
      Type
    eq <- (String, Dom Type) -> TCM Type -> TCM Type
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext (String
    "w" :: String, Type -> Dom Type
    forall a. a -> Dom a
    defaultDom Type
    a) (TCM Type -> TCM Type) -> TCM Type -> TCM Type
    forall a b. (a -> b) -> a -> b
    $ do
        -- manufacture the type @w ≡ v@
        QName
    eqName <- TCM QName
    primEqualityName
        Type
    eqTy <- Definition -> Type
    defType (Definition -> Type) -> TCMT IO Definition -> TCM Type
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> TCMT IO Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    eqName
        -- E.g. @eqTy = eqTel → Set a@ where @eqTel = {a : Level} {A : Set a} (x y : A)@.
        TelV Tele (Dom Type)
    eqTel Type
    _ <- Type -> TCMT IO (TelV Type)
    forall (m :: * -> *).
    (MonadReduce m, MonadAddContext m) =>
    Type -> m (TelV Type)
    telView Type
    eqTy
        Args
    tel  <- Tele (Dom Type) -> TCMT IO Args
    forall (m :: * -> *).
    MonadMetaSolver m =>
    Tele (Dom Type) -> m Args
    newTelMeta (ListTel -> Tele (Dom Type)
    telFromList (ListTel -> Tele (Dom Type)) -> ListTel -> Tele (Dom Type)
    forall a b. (a -> b) -> a -> b
    $ Nat -> ListTel -> ListTel
    forall a. Nat -> [a] -> [a]
    dropEnd Nat
    2 (ListTel -> ListTel) -> ListTel -> ListTel
    forall a b. (a -> b) -> a -> b
    $ Tele (Dom Type) -> ListTel
    forall t. Tele (Dom t) -> [Dom (String, t)]
    telToList Tele (Dom Type)
    eqTel)
        let eq :: Term
    eq = QName -> [Elim' Term] -> Term
    Def QName
    eqName ([Elim' Term] -> Term) -> [Elim' Term] -> Term
    forall a b. (a -> b) -> a -> b
    $ (Arg Term -> Elim' Term) -> Args -> [Elim' Term]
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Term -> Elim' Term
    forall a. Arg a -> Elim' a
    Apply
                     (Args -> [Elim' Term]) -> Args -> [Elim' Term]
    forall a b. (a -> b) -> a -> b
    $ (Arg Term -> Arg Term) -> Args -> Args
    forall a b. (a -> b) -> [a] -> [b]
    map (Hiding -> Arg Term -> Arg Term
    forall a. LensHiding a => Hiding -> a -> a
    setHiding Hiding
    Hidden) Args
    tel
                     -- we write `v ≡ w` because this equality is typically used to
                     -- get `v` to unfold to whatever pattern was used to refine `w`
                     -- in a with-clause.
                     -- If we were to write `w ≡ v`, we would often need to take the
                     -- symmetric of the proof we get to make use of `rewrite`.
                     Args -> Args -> Args
    forall a. [a] -> [a] -> [a]
    ++ [ Term -> Arg Term
    forall a. a -> Arg a
    defaultArg (Nat -> Term -> Term
    forall a. Subst a => Nat -> a -> a
    raise Nat
    1 Term
    v)
                        , Term -> Arg Term
    forall a. a -> Arg a
    defaultArg (Nat -> Term
    var Nat
    0)
                        ]
        Sort' Term
    sort <- TCMT IO (Sort' Term)
    forall (m :: * -> *). MonadMetaSolver m => m (Sort' Term)
    newSortMeta
        let ty :: Type
    ty = Sort' Term -> Term -> Type
    forall t a. Sort' t -> a -> Type'' t a
    El Sort' Term
    sort Term
    eq
        Type
    ty Type -> TCMT IO () -> TCM Type
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ Type -> TCMT IO ()
    forall (m :: * -> *). MonadCheckInternal m => Type -> m ()
    checkType Type
    ty

      Type -> TCM Type
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Type -> TCM Type) -> Type -> TCM Type
    forall a b. (a -> b) -> a -> b
    $ Dom (String, Type) -> Type -> Type
    mkPi (Hiding -> Dom (String, Type) -> Dom (String, Type)
    forall a. LensHiding a => Hiding -> a -> a
    setHiding (ArgInfo -> Hiding
    forall a. LensHiding a => a -> Hiding
    getHiding ArgInfo
    info) (Dom (String, Type) -> Dom (String, Type))
    -> Dom (String, Type) -> Dom (String, Type)
    forall a b. (a -> b) -> a -> b
    $ (String, Type) -> Dom (String, Type)
    forall a. a -> Dom a
    defaultDom (String
    "w", Type
    a))
           (Type -> Type) -> Type -> Type
    forall a b. (a -> b) -> a -> b
    $ Dom (String, Type) -> Type -> Type
    mkPi (Hiding -> Dom (String, Type) -> Dom (String, Type)
    forall a. LensHiding a => Hiding -> a -> a
    setHiding Hiding
    NotHidden        (Dom (String, Type) -> Dom (String, Type))
    -> Dom (String, Type) -> Dom (String, Type)
    forall a b. (a -> b) -> a -> b
    $ (String, Type) -> Dom (String, Type)
    forall a. a -> Dom a
    defaultDom (String
    "eq", Type
    eq))
           (Type -> Type) -> Type -> Type
    forall a b. (a -> b) -> a -> b
    $ Type
    b
    piAbstract (Arg ArgInfo
    info (Term
    prf, eqt :: EqualityView
    eqt@(EqualityType Sort' Term
    _ QName
    _ Args
    _ (Arg ArgInfo
    _ Term
    a) Arg Term
    v Arg Term
    _))) Type
    b = do
      Sort' Term
    s <- Term -> TCMT IO (Sort' Term)
    forall (m :: * -> *).
    (PureTCM m, MonadBlock m) =>
    Term -> m (Sort' Term)
    sortOf Term
    a
      let prfTy :: Type
    prfTy = EqualityView -> Type
    equalityUnview EqualityView
    eqt
          vTy :: Type
    vTy   = Sort' Term -> Term -> Type
    forall t a. Sort' t -> a -> Type'' t a
    El Sort' Term
    s Term
    a
      Type
    b <- Type -> Term -> Type -> TCM Type
    abstractType Type
    prfTy Term
    prf Type
    b
      Type
    b <- (String, Dom Type) -> TCM Type -> TCM Type
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext (String
    "w" :: String, Type -> Dom Type
    forall a. a -> Dom a
    defaultDom Type
    prfTy) (TCM Type -> TCM Type) -> TCM Type -> TCM Type
    forall a b. (a -> b) -> a -> b
    $
             Type -> Term -> Type -> TCM Type
    abstractType (Nat -> Type -> Type
    forall a. Subst a => Nat -> a -> a
    raise Nat
    1 Type
    vTy) (Arg Term -> Term
    forall e. Arg e -> e
    unArg (Arg Term -> Term) -> Arg Term -> Term
    forall a b. (a -> b) -> a -> b
    $ Nat -> Arg Term -> Arg Term
    forall a. Subst a => Nat -> a -> a
    raise Nat
    1 Arg Term
    v) Type
    b
      Type -> TCM Type
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Type -> TCM Type) -> (Type -> Type) -> Type -> TCM Type
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . String -> Type -> Type -> Type
    funType String
    "lhs" Type
    vTy (Type -> Type) -> (Type -> Type) -> Type -> Type
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . String -> Type -> Type -> Type
    funType String
    "equality" Type
    eqTy' (Type -> Type) -> (Type -> Type) -> Type -> Type
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Type -> Type
    forall a. TermSubst a => a -> a
    swap01 (Type -> TCM Type) -> Type -> TCM Type
    forall a b. (a -> b) -> a -> b
    $ Type
    b
      where
        funType :: String -> Type -> Type -> Type
    funType String
    str Type
    a = Dom (String, Type) -> Type -> Type
    mkPi (Dom (String, Type) -> Type -> Type)
    -> Dom (String, Type) -> Type -> Type
    forall a b. (a -> b) -> a -> b
    $ ArgInfo -> Dom (String, Type) -> Dom (String, Type)
    forall a. LensArgInfo a => ArgInfo -> a -> a
    setArgInfo ArgInfo
    info (Dom (String, Type) -> Dom (String, Type))
    -> Dom (String, Type) -> Dom (String, Type)
    forall a b. (a -> b) -> a -> b
    $ (String, Type) -> Dom (String, Type)
    forall a. a -> Dom a
    defaultDom (String
    str, Type
    a)
        -- Abstract the lhs (@a@) of the equality only.
        eqt1 :: EqualityView
    eqt1  = Nat -> EqualityView -> EqualityView
    forall a. Subst a => Nat -> a -> a
    raise Nat
    1 EqualityView
    eqt
        eqTy' :: Type
    eqTy' = EqualityView -> Type
    equalityUnview (EqualityView -> Type) -> EqualityView -> Type
    forall a b. (a -> b) -> a -> b
    $ EqualityView
    eqt1 { eqtLhs :: Arg Term
    eqtLhs = EqualityView -> Arg Term
    eqtLhs EqualityView
    eqt1 Arg Term -> Term -> Arg Term
    forall (f :: * -> *) a b. Functor f => f a -> b -> f b
    $> Nat -> Term
    var Nat
    0 }

    -- | @isPrefixOf u v = Just es@ if @v == u `applyE` es@.
    class IsPrefixOf a where
      isPrefixOf :: a -> a -> Maybe Elims

    instance IsPrefixOf Elims where
      isPrefixOf :: [Elim' Term] -> [Elim' Term] -> Maybe [Elim' Term]
    isPrefixOf [Elim' Term]
    us [Elim' Term]
    vs = do
        ([Elim' Term]
    vs1, [Elim' Term]
    vs2) <- Nat -> [Elim' Term] -> Maybe ([Elim' Term], [Elim' Term])
    forall n a. Integral n => n -> [a] -> Maybe ([a], [a])
    splitExactlyAt ([Elim' Term] -> Nat
    forall (t :: * -> *) a. Foldable t => t a -> Nat
    length [Elim' Term]
    us) [Elim' Term]
    vs
        Bool -> Maybe ()
    forall (f :: * -> *). Alternative f => Bool -> f ()
    guard (Bool -> Maybe ()) -> Bool -> Maybe ()
    forall a b. (a -> b) -> a -> b
    $ [Elim' Term] -> [Elim' Term] -> Bool
    forall a. EqualSy a => a -> a -> Bool
    equalSy [Elim' Term]
    us [Elim' Term]
    vs1
        [Elim' Term] -> Maybe [Elim' Term]
    forall (m :: * -> *) a. Monad m => a -> m a
    return [Elim' Term]
    vs2

    instance IsPrefixOf Args where
      isPrefixOf :: Args -> Args -> Maybe [Elim' Term]
    isPrefixOf Args
    us Args
    vs = do
        (Args
    vs1, Args
    vs2) <- Nat -> Args -> Maybe (Args, Args)
    forall n a. Integral n => n -> [a] -> Maybe ([a], [a])
    splitExactlyAt (Args -> Nat
    forall (t :: * -> *) a. Foldable t => t a -> Nat
    length Args
    us) Args
    vs
        Bool -> Maybe ()
    forall (f :: * -> *). Alternative f => Bool -> f ()
    guard (Bool -> Maybe ()) -> Bool -> Maybe ()
    forall a b. (a -> b) -> a -> b
    $ Args -> Args -> Bool
    forall a. EqualSy a => a -> a -> Bool
    equalSy Args
    us Args
    vs1
        [Elim' Term] -> Maybe [Elim' Term]
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([Elim' Term] -> Maybe [Elim' Term])
    -> [Elim' Term] -> Maybe [Elim' Term]
    forall a b. (a -> b) -> a -> b
    $ (Arg Term -> Elim' Term) -> Args -> [Elim' Term]
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Term -> Elim' Term
    forall a. Arg a -> Elim' a
    Apply Args
    vs2

    instance IsPrefixOf Term where
      isPrefixOf :: Term -> Term -> Maybe [Elim' Term]
    isPrefixOf Term
    u Term
    v =
        case (Term
    u, Term
    v) of
          (Var   Nat
    i [Elim' Term]
    us, Var   Nat
    j [Elim' Term]
    vs) | Nat
    i Nat -> Nat -> Bool
    forall a. Eq a => a -> a -> Bool
    == Nat
    j  -> [Elim' Term]
    us [Elim' Term] -> [Elim' Term] -> Maybe [Elim' Term]
    forall a. IsPrefixOf a => a -> a -> Maybe [Elim' Term]
    `isPrefixOf` [Elim' Term]
    vs
          (Def   QName
    f [Elim' Term]
    us, Def   QName
    g [Elim' Term]
    vs) | QName
    f QName -> QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == QName
    g  -> [Elim' Term]
    us [Elim' Term] -> [Elim' Term] -> Maybe [Elim' Term]
    forall a. IsPrefixOf a => a -> a -> Maybe [Elim' Term]
    `isPrefixOf` [Elim' Term]
    vs
          (Con ConHead
    c ConInfo
    _ [Elim' Term]
    us, Con ConHead
    d ConInfo
    _ [Elim' Term]
    vs) | ConHead
    c ConHead -> ConHead -> Bool
    forall a. Eq a => a -> a -> Bool
    == ConHead
    d  -> [Elim' Term]
    us [Elim' Term] -> [Elim' Term] -> Maybe [Elim' Term]
    forall a. IsPrefixOf a => a -> a -> Maybe [Elim' Term]
    `isPrefixOf` [Elim' Term]
    vs
          (MetaV MetaId
    x [Elim' Term]
    us, MetaV MetaId
    y [Elim' Term]
    vs) | MetaId
    x MetaId -> MetaId -> Bool
    forall a. Eq a => a -> a -> Bool
    == MetaId
    y  -> [Elim' Term]
    us [Elim' Term] -> [Elim' Term] -> Maybe [Elim' Term]
    forall a. IsPrefixOf a => a -> a -> Maybe [Elim' Term]
    `isPrefixOf` [Elim' Term]
    vs
          (Term
    u, Term
    v) -> Bool -> Maybe ()
    forall (f :: * -> *). Alternative f => Bool -> f ()
    guard (Term -> Term -> Bool
    forall a. EqualSy a => a -> a -> Bool
    equalSy Term
    u Term
    v) Maybe () -> Maybe [Elim' Term] -> Maybe [Elim' Term]
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> [Elim' Term] -> Maybe [Elim' Term]
    forall (m :: * -> *) a. Monad m => a -> m a
    return []

    -- Type-based abstraction. Needed if u is a constructor application (#745).
    abstractTerm :: Type -> Term -> Type -> Term -> TCM Term
    abstractTerm :: Type -> Term -> Type -> Term -> TCMT IO Term
    abstractTerm Type
    a u :: Term
    u@Con{} Type
    b Term
    v = do
      String -> Nat -> TCMT IO Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Nat -> TCMT IO Doc -> m ()
    reportSDoc String
    "tc.abstract" Nat
    50 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $
        [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep [ TCMT IO Doc
    "Abstracting"
            , Nat -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
    nest Nat
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep [ Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Term
    u TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> TCMT IO Doc
    ":", Nat -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
    nest Nat
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ Type -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Type
    a ]
            , TCMT IO Doc
    "over"
            , Nat -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
    nest Nat
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep [ Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Term
    v TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> TCMT IO Doc
    ":", Nat -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
    nest Nat
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ Type -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Type
    b ] ]
      String -> Nat -> TCMT IO Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Nat -> TCMT IO Doc -> m ()
    reportSDoc String
    "tc.abstract" Nat
    70 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $
        [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep [ TCMT IO Doc
    "Abstracting"
            , Nat -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
    nest Nat
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep [ (String -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => String -> m Doc
    text (String -> TCMT IO Doc) -> (Term -> String) -> Term -> TCMT IO Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Term -> String
    forall a. Show a => a -> String
    show) Term
    u TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> TCMT IO Doc
    ":", Nat -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
    nest Nat
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ (String -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => String -> m Doc
    text (String -> TCMT IO Doc) -> (Type -> String) -> Type -> TCMT IO Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Type -> String
    forall a. Show a => a -> String
    show) Type
    a ]
            , TCMT IO Doc
    "over"
            , Nat -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
    nest Nat
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep [ (String -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => String -> m Doc
    text (String -> TCMT IO Doc) -> (Term -> String) -> Term -> TCMT IO Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Term -> String
    forall a. Show a => a -> String
    show) Term
    v TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> TCMT IO Doc
    ":", Nat -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
    nest Nat
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ (String -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => String -> m Doc
    text (String -> TCMT IO Doc) -> (Type -> String) -> Type -> TCMT IO Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Type -> String
    forall a. Show a => a -> String
    show) Type
    b ] ]

      QName
    hole <- ModuleName -> Name -> QName
    qualify (ModuleName -> Name -> QName)
    -> TCMT IO ModuleName -> TCMT IO (Name -> QName)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCMT IO ModuleName
    forall (m :: * -> *). MonadTCEnv m => m ModuleName
    currentModule TCMT IO (Name -> QName) -> TCMT IO Name -> TCM QName
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> String -> TCMT IO Name
    forall a (m :: * -> *).
    (FreshName a, MonadFresh NameId m) =>
    a -> m Name
    freshName_ (String
    "hole" :: String)
      TCMT IO () -> TCMT IO ()
    forall a. TCM a -> TCM a
    noMutualBlock (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ QName -> ArgInfo -> QName -> Type -> Defn -> TCMT IO ()
    addConstant' QName
    hole ArgInfo
    defaultArgInfo QName
    hole Type
    a Defn
    defaultAxiom

      [Elim' Term]
    args <- (Arg Term -> Elim' Term) -> Args -> [Elim' Term]
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Term -> Elim' Term
    forall a. Arg a -> Elim' a
    Apply (Args -> [Elim' Term]) -> TCMT IO Args -> TCMT IO [Elim' Term]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCMT IO Args
    forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Args
    getContextArgs
      let n :: Nat
    n = [Elim' Term] -> Nat
    forall (t :: * -> *) a. Foldable t => t a -> Nat
    length [Elim' Term]
    args

      let abstr :: Type -> Term -> TCMT IO Term
    abstr Type
    b Term
    v = do
            Nat
    m <- TCMT IO Nat
    forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Nat
    getContextSize
            let (Type
    a', Term
    u') = Nat -> (Type, Term) -> (Type, Term)
    forall a. Subst a => Nat -> a -> a
    raise (Nat
    m Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    - Nat
    n) (Type
    a, Term
    u)
            case Term
    u' Term -> Term -> Maybe [Elim' Term]
    forall a. IsPrefixOf a => a -> a -> Maybe [Elim' Term]
    `isPrefixOf` Term
    v of
              Maybe [Elim' Term]
    Nothing -> Term -> TCMT IO Term
    forall (m :: * -> *) a. Monad m => a -> m a
    return Term
    v
              Just [Elim' Term]
    es -> do -- Check that the types match.
                TCState
    s <- TCMT IO TCState
    forall (m :: * -> *). MonadTCState m => m TCState
    getTC
                do  TCMT IO () -> TCMT IO ()
    forall (m :: * -> *) a.
    (MonadConstraint m, MonadWarning m, MonadError TCErr m,
     MonadFresh ProblemId m) =>
    m a -> m a
    noConstraints (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ Type -> Type -> TCMT IO ()
    forall (m :: * -> *). MonadConversion m => Type -> Type -> m ()
    equalType Type
    a' Type
    b
                    TCState -> TCMT IO ()
    forall (m :: * -> *). MonadTCState m => TCState -> m ()
    putTC TCState
    s
                    Term -> TCMT IO Term
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Term -> TCMT IO Term) -> Term -> TCMT IO Term
    forall a b. (a -> b) -> a -> b
    $ QName -> [Elim' Term] -> Term
    Def QName
    hole (Nat -> [Elim' Term] -> [Elim' Term]
    forall a. Subst a => Nat -> a -> a
    raise (Nat
    m Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    - Nat
    n) [Elim' Term]
    args [Elim' Term] -> [Elim' Term] -> [Elim' Term]
    forall a. [a] -> [a] -> [a]
    ++ [Elim' Term]
    es)
                  TCMT IO Term -> (TCErr -> TCMT IO Term) -> TCMT IO Term
    forall e (m :: * -> *) a.
    MonadError e m =>
    m a -> (e -> m a) -> m a
    `catchError` \ TCErr
    _ -> do
                    String -> Nat -> TCMT IO Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Nat -> TCMT IO Doc -> m ()
    reportSDoc String
    "tc.abstract.ill-typed" Nat
    50 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $
                      [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep [ TCMT IO Doc
    "Skipping ill-typed abstraction"
                          , Nat -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
    nest Nat
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep [ Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Term
    v TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> TCMT IO Doc
    ":", Nat -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
    nest Nat
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ Type -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Type
    b ] ]
                    Term -> TCMT IO Term
    forall (m :: * -> *) a. Monad m => a -> m a
    return Term
    v

      -- #2763: This can fail if the user is with-abstracting incorrectly (for
      -- instance, abstracting over a first component of a sigma without also
      -- abstracting the second component). In this case we skip abstraction
      -- altogether and let the type check of the final with-function type produce
      -- the error message.
      Term
    res <- TCMT IO Term -> (TCErr -> TCMT IO Term) -> TCMT IO Term
    forall a. TCM a -> (TCErr -> TCM a) -> TCM a
    catchError_ (Action (TCMT IO) -> Term -> Comparison -> Type -> TCMT IO Term
    forall (m :: * -> *).
    MonadCheckInternal m =>
    Action m -> Term -> Comparison -> Type -> m Term
    checkInternal' (Action (TCMT IO)
    forall (m :: * -> *). PureTCM m => Action m
    defaultAction { preAction :: Type -> Term -> TCMT IO Term
    preAction = Type -> Term -> TCMT IO Term
    abstr }) Term
    v Comparison
    CmpLeq Type
    b) ((TCErr -> TCMT IO Term) -> TCMT IO Term)
    -> (TCErr -> TCMT IO Term) -> TCMT IO Term
    forall a b. (a -> b) -> a -> b
    $ \ TCErr
    err -> do
            String -> Nat -> TCMT IO Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Nat -> TCMT IO Doc -> m ()
    reportSDoc String
    "tc.abstract.ill-typed" Nat
    40 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $
              TCMT IO Doc
    "Skipping typed abstraction over ill-typed term" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <?> (Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Term
    v TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <?> (TCMT IO Doc
    ":" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Type -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Type
    b))
            Term -> TCMT IO Term
    forall (m :: * -> *) a. Monad m => a -> m a
    return Term
    v
      String -> Nat -> TCMT IO Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Nat -> TCMT IO Doc -> m ()
    reportSDoc String
    "tc.abstract" Nat
    50 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "Resulting abstraction" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <?> Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Term
    res
      (Signature -> Signature) -> TCMT IO ()
    forall (m :: * -> *).
    MonadTCState m =>
    (Signature -> Signature) -> m ()
    modifySignature ((Signature -> Signature) -> TCMT IO ())
    -> (Signature -> Signature) -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ (Definitions -> Definitions) -> Signature -> Signature
    updateDefinitions ((Definitions -> Definitions) -> Signature -> Signature)
    -> (Definitions -> Definitions) -> Signature -> Signature
    forall a b. (a -> b) -> a -> b
    $ QName -> Definitions -> Definitions
    forall k v. (Eq k, Hashable k) => k -> HashMap k v -> HashMap k v
    HMap.delete QName
    hole
      Term -> TCMT IO Term
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Term -> TCMT IO Term) -> Term -> TCMT IO Term
    forall a b. (a -> b) -> a -> b
    $ Term -> Term -> Term
    forall a. AbsTerm a => Term -> a -> a
    absTerm (QName -> [Elim' Term] -> Term
    Def QName
    hole [Elim' Term]
    args) Term
    res

    abstractTerm Type
    _ Term
    u Type
    _ Term
    v = Term -> TCMT IO Term
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Term -> TCMT IO Term) -> Term -> TCMT IO Term
    forall a b. (a -> b) -> a -> b
    $ Term -> Term -> Term
    forall a. AbsTerm a => Term -> a -> a
    absTerm Term
    u Term
    v -- Non-constructors can use untyped abstraction

    class AbsTerm a where
      -- | @subst u . absTerm u == id@
      absTerm :: Term -> a -> a

    instance AbsTerm Term where
      absTerm :: Term -> Term -> Term
    absTerm Term
    u Term
    v | Just [Elim' Term]
    es <- Term
    u Term -> Term -> Maybe [Elim' Term]
    forall a. IsPrefixOf a => a -> a -> Maybe [Elim' Term]
    `isPrefixOf` Term
    v = Nat -> [Elim' Term] -> Term
    Var Nat
    0 ([Elim' Term] -> Term) -> [Elim' Term] -> Term
    forall a b. (a -> b) -> a -> b
    $ [Elim' Term] -> [Elim' Term]
    forall b. AbsTerm b => b -> b
    absT [Elim' Term]
    es
                  | Bool
    otherwise                   =
        case Term
    v of
    -- Andreas, 2013-10-20: the original impl. works only at base types
    --    v | u == v  -> Var 0 []  -- incomplete see succeed/WithOfFunctionType
          Var Nat
    i [Elim' Term]
    vs    -> Nat -> [Elim' Term] -> Term
    Var (Nat
    i Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    + Nat
    1) ([Elim' Term] -> Term) -> [Elim' Term] -> Term
    forall a b. (a -> b) -> a -> b
    $ [Elim' Term] -> [Elim' Term]
    forall b. AbsTerm b => b -> b
    absT [Elim' Term]
    vs
          Lam ArgInfo
    h Abs Term
    b     -> ArgInfo -> Abs Term -> Term
    Lam ArgInfo
    h (Abs Term -> Term) -> Abs Term -> Term
    forall a b. (a -> b) -> a -> b
    $ Abs Term -> Abs Term
    forall b. AbsTerm b => b -> b
    absT Abs Term
    b
          Def QName
    c [Elim' Term]
    vs    -> QName -> [Elim' Term] -> Term
    Def QName
    c ([Elim' Term] -> Term) -> [Elim' Term] -> Term
    forall a b. (a -> b) -> a -> b
    $ [Elim' Term] -> [Elim' Term]
    forall b. AbsTerm b => b -> b
    absT [Elim' Term]
    vs
          Con ConHead
    c ConInfo
    ci [Elim' Term]
    vs -> ConHead -> ConInfo -> [Elim' Term] -> Term
    Con ConHead
    c ConInfo
    ci ([Elim' Term] -> Term) -> [Elim' Term] -> Term
    forall a b. (a -> b) -> a -> b
    $ [Elim' Term] -> [Elim' Term]
    forall b. AbsTerm b => b -> b
    absT [Elim' Term]
    vs
          Pi Dom Type
    a Abs Type
    b      -> (Dom Type -> Abs Type -> Term) -> (Dom Type, Abs Type) -> Term
    forall a b c. (a -> b -> c) -> (a, b) -> c
    uncurry Dom Type -> Abs Type -> Term
    Pi ((Dom Type, Abs Type) -> Term) -> (Dom Type, Abs Type) -> Term
    forall a b. (a -> b) -> a -> b
    $ (Dom Type, Abs Type) -> (Dom Type, Abs Type)
    forall b. AbsTerm b => b -> b
    absT (Dom Type
    a, Abs Type
    b)
          Lit Literal
    l       -> Literal -> Term
    Lit Literal
    l
          Level Level
    l     -> Level -> Term
    Level (Level -> Term) -> Level -> Term
    forall a b. (a -> b) -> a -> b
    $ Level -> Level
    forall b. AbsTerm b => b -> b
    absT Level
    l
          Sort Sort' Term
    s      -> Sort' Term -> Term
    Sort (Sort' Term -> Term) -> Sort' Term -> Term
    forall a b. (a -> b) -> a -> b
    $ Sort' Term -> Sort' Term
    forall b. AbsTerm b => b -> b
    absT Sort' Term
    s
          MetaV MetaId
    m [Elim' Term]
    vs  -> MetaId -> [Elim' Term] -> Term
    MetaV MetaId
    m ([Elim' Term] -> Term) -> [Elim' Term] -> Term
    forall a b. (a -> b) -> a -> b
    $ [Elim' Term] -> [Elim' Term]
    forall b. AbsTerm b => b -> b
    absT [Elim' Term]
    vs
          DontCare Term
    mv -> Term -> Term
    DontCare (Term -> Term) -> Term -> Term
    forall a b. (a -> b) -> a -> b
    $ Term -> Term
    forall b. AbsTerm b => b -> b
    absT Term
    mv
          Dummy String
    s [Elim' Term]
    es   -> String -> [Elim' Term] -> Term
    Dummy String
    s ([Elim' Term] -> Term) -> [Elim' Term] -> Term
    forall a b. (a -> b) -> a -> b
    $ [Elim' Term] -> [Elim' Term]
    forall b. AbsTerm b => b -> b
    absT [Elim' Term]
    es
          where
            absT :: AbsTerm b => b -> b
            absT :: forall b. AbsTerm b => b -> b
    absT b
    x = Term -> b -> b
    forall a. AbsTerm a => Term -> a -> a
    absTerm Term
    u b
    x

    instance AbsTerm Type where
      absTerm :: Term -> Type -> Type
    absTerm Term
    u (El Sort' Term
    s Term
    v) = Sort' Term -> Term -> Type
    forall t a. Sort' t -> a -> Type'' t a
    El (Term -> Sort' Term -> Sort' Term
    forall a. AbsTerm a => Term -> a -> a
    absTerm Term
    u Sort' Term
    s) (Term -> Term -> Term
    forall a. AbsTerm a => Term -> a -> a
    absTerm Term
    u Term
    v)

    instance AbsTerm Sort where
      absTerm :: Term -> Sort' Term -> Sort' Term
    absTerm Term
    u = \case
        Type Level
    n     -> Level -> Sort' Term
    forall t. Level' t -> Sort' t
    Type (Level -> Sort' Term) -> Level -> Sort' Term
    forall a b. (a -> b) -> a -> b
    $ Level -> Level
    forall b. AbsTerm b => b -> b
    absS Level
    n
        Prop Level
    n     -> Level -> Sort' Term
    forall t. Level' t -> Sort' t
    Prop (Level -> Sort' Term) -> Level -> Sort' Term
    forall a b. (a -> b) -> a -> b
    $ Level -> Level
    forall b. AbsTerm b => b -> b
    absS Level
    n
        s :: Sort' Term
    s@(Inf IsFibrant
    f Integer
    n)-> Sort' Term
    s
        SSet Level
    n     -> Level -> Sort' Term
    forall t. Level' t -> Sort' t
    SSet (Level -> Sort' Term) -> Level -> Sort' Term
    forall a b. (a -> b) -> a -> b
    $ Level -> Level
    forall b. AbsTerm b => b -> b
    absS Level
    n
        Sort' Term
    SizeUniv   -> Sort' Term
    forall t. Sort' t
    SizeUniv
        Sort' Term
    LockUniv   -> Sort' Term
    forall t. Sort' t
    LockUniv
        PiSort Dom' Term Term
    a Sort' Term
    s1 Abs (Sort' Term)
    s2 -> Dom' Term Term -> Sort' Term -> Abs (Sort' Term) -> Sort' Term
    forall t. Dom' t t -> Sort' t -> Abs (Sort' t) -> Sort' t
    PiSort (Dom' Term Term -> Dom' Term Term
    forall b. AbsTerm b => b -> b
    absS Dom' Term Term
    a) (Sort' Term -> Sort' Term
    forall b. AbsTerm b => b -> b
    absS Sort' Term
    s1) (Abs (Sort' Term) -> Abs (Sort' Term)
    forall b. AbsTerm b => b -> b
    absS Abs (Sort' Term)
    s2)
        FunSort Sort' Term
    s1 Sort' Term
    s2 -> Sort' Term -> Sort' Term -> Sort' Term
    forall t. Sort' t -> Sort' t -> Sort' t
    FunSort (Sort' Term -> Sort' Term
    forall b. AbsTerm b => b -> b
    absS Sort' Term
    s1) (Sort' Term -> Sort' Term
    forall b. AbsTerm b => b -> b
    absS Sort' Term
    s2)
        UnivSort Sort' Term
    s -> Sort' Term -> Sort' Term
    forall t. Sort' t -> Sort' t
    UnivSort (Sort' Term -> Sort' Term) -> Sort' Term -> Sort' Term
    forall a b. (a -> b) -> a -> b
    $ Sort' Term -> Sort' Term
    forall b. AbsTerm b => b -> b
    absS Sort' Term
    s
        MetaS MetaId
    x [Elim' Term]
    es -> MetaId -> [Elim' Term] -> Sort' Term
    forall t. MetaId -> [Elim' t] -> Sort' t
    MetaS MetaId
    x ([Elim' Term] -> Sort' Term) -> [Elim' Term] -> Sort' Term
    forall a b. (a -> b) -> a -> b
    $ [Elim' Term] -> [Elim' Term]
    forall b. AbsTerm b => b -> b
    absS [Elim' Term]
    es
        DefS QName
    d [Elim' Term]
    es  -> QName -> [Elim' Term] -> Sort' Term
    forall t. QName -> [Elim' t] -> Sort' t
    DefS QName
    d ([Elim' Term] -> Sort' Term) -> [Elim' Term] -> Sort' Term
    forall a b. (a -> b) -> a -> b
    $ [Elim' Term] -> [Elim' Term]
    forall b. AbsTerm b => b -> b
    absS [Elim' Term]
    es
        s :: Sort' Term
    s@DummyS{} -> Sort' Term
    s
        where
          absS :: AbsTerm b => b -> b
          absS :: forall b. AbsTerm b => b -> b
    absS b
    x = Term -> b -> b
    forall a. AbsTerm a => Term -> a -> a
    absTerm Term
    u b
    x

    instance AbsTerm Level where
      absTerm :: Term -> Level -> Level
    absTerm Term
    u (Max Integer
    n [PlusLevel' Term]
    as) = Integer -> [PlusLevel' Term] -> Level
    forall t. Integer -> [PlusLevel' t] -> Level' t
    Max Integer
    n ([PlusLevel' Term] -> Level) -> [PlusLevel' Term] -> Level
    forall a b. (a -> b) -> a -> b
    $ Term -> [PlusLevel' Term] -> [PlusLevel' Term]
    forall a. AbsTerm a => Term -> a -> a
    absTerm Term
    u [PlusLevel' Term]
    as

    instance AbsTerm PlusLevel where
      absTerm :: Term -> PlusLevel' Term -> PlusLevel' Term
    absTerm Term
    u (Plus Integer
    n Term
    l) = Integer -> Term -> PlusLevel' Term
    forall t. Integer -> t -> PlusLevel' t
    Plus Integer
    n (Term -> PlusLevel' Term) -> Term -> PlusLevel' Term
    forall a b. (a -> b) -> a -> b
    $ Term -> Term -> Term
    forall a. AbsTerm a => Term -> a -> a
    absTerm Term
    u Term
    l

    instance AbsTerm a => AbsTerm (Elim' a) where
      absTerm :: Term -> Elim' a -> Elim' a
    absTerm = (a -> a) -> Elim' a -> Elim' a
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((a -> a) -> Elim' a -> Elim' a)
    -> (Term -> a -> a) -> Term -> Elim' a -> Elim' a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Term -> a -> a
    forall a. AbsTerm a => Term -> a -> a
    absTerm

    instance AbsTerm a => AbsTerm (Arg a) where
      absTerm :: Term -> Arg a -> Arg a
    absTerm = (a -> a) -> Arg a -> Arg a
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((a -> a) -> Arg a -> Arg a)
    -> (Term -> a -> a) -> Term -> Arg a -> Arg a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Term -> a -> a
    forall a. AbsTerm a => Term -> a -> a
    absTerm

    instance AbsTerm a => AbsTerm (Dom a) where
      absTerm :: Term -> Dom a -> Dom a
    absTerm = (a -> a) -> Dom a -> Dom a
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((a -> a) -> Dom a -> Dom a)
    -> (Term -> a -> a) -> Term -> Dom a -> Dom a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Term -> a -> a
    forall a. AbsTerm a => Term -> a -> a
    absTerm

    instance AbsTerm a => AbsTerm [a] where
      absTerm :: Term -> [a] -> [a]
    absTerm = (a -> a) -> [a] -> [a]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((a -> a) -> [a] -> [a]) -> (Term -> a -> a) -> Term -> [a] -> [a]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Term -> a -> a
    forall a. AbsTerm a => Term -> a -> a
    absTerm

    instance AbsTerm a => AbsTerm (Maybe a) where
      absTerm :: Term -> Maybe a -> Maybe a
    absTerm = (a -> a) -> Maybe a -> Maybe a
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((a -> a) -> Maybe a -> Maybe a)
    -> (Term -> a -> a) -> Term -> Maybe a -> Maybe a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Term -> a -> a
    forall a. AbsTerm a => Term -> a -> a
    absTerm

    instance (TermSubst a, AbsTerm a) => AbsTerm (Abs a) where
      absTerm :: Term -> Abs a -> Abs a
    absTerm Term
    u (NoAbs String
    x a
    v) = String -> a -> Abs a
    forall a. String -> a -> Abs a
    NoAbs String
    x (a -> Abs a) -> a -> Abs a
    forall a b. (a -> b) -> a -> b
    $ Term -> a -> a
    forall a. AbsTerm a => Term -> a -> a
    absTerm Term
    u a
    v
      absTerm Term
    u (Abs   String
    x a
    v) = String -> a -> Abs a
    forall a. String -> a -> Abs a
    Abs String
    x (a -> Abs a) -> a -> Abs a
    forall a b. (a -> b) -> a -> b
    $ a -> a
    forall a. TermSubst a => a -> a
    swap01 (a -> a) -> a -> a
    forall a b. (a -> b) -> a -> b
    $ Term -> a -> a
    forall a. AbsTerm a => Term -> a -> a
    absTerm (Nat -> Term -> Term
    forall a. Subst a => Nat -> a -> a
    raise Nat
    1 Term
    u) a
    v

    instance (AbsTerm a, AbsTerm b) => AbsTerm (a, b) where
      absTerm :: Term -> (a, b) -> (a, b)
    absTerm Term
    u (a
    x, b
    y) = (Term -> a -> a
    forall a. AbsTerm a => Term -> a -> a
    absTerm Term
    u a
    x, Term -> b -> b
    forall a. AbsTerm a => Term -> a -> a
    absTerm Term
    u b
    y)

    -- | This swaps @var 0@ and @var 1@.
    swap01 :: TermSubst a => a -> a
    swap01 :: forall a. TermSubst a => a -> a
    swap01 = Substitution' (SubstArg a) -> a -> a
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst (Substitution' (SubstArg a) -> a -> a)
    -> Substitution' (SubstArg a) -> a -> a
    forall a b. (a -> b) -> a -> b
    $ Nat -> Term
    var Nat
    1 Term -> Substitution' Term -> Substitution' Term
    forall a. a -> Substitution' a -> Substitution' a
    :# Nat -> Substitution' Term -> Substitution' Term
    forall a. Nat -> Substitution' a -> Substitution' a
    liftS Nat
    1 (Nat -> Substitution' Term
    forall a. Nat -> Substitution' a
    raiseS Nat
    1)

    -- ** Equality of terms for the sake of with-abstraction.

    -- The following could be parameterized by a record of flags
    -- what parts of the syntax tree should be ignored.
    -- For now, there is a fixed strategy.

    class EqualSy a where
      equalSy :: a -> a -> Bool

    instance EqualSy a => EqualSy [a] where
      equalSy :: [a] -> [a] -> Bool
    equalSy [a]
    us [a]
    vs = [Bool] -> Bool
    forall (t :: * -> *). Foldable t => t Bool -> Bool
    and ([Bool] -> Bool) -> [Bool] -> Bool
    forall a b. (a -> b) -> a -> b
    $ ([a] -> Nat
    forall (t :: * -> *) a. Foldable t => t a -> Nat
    length [a]
    us Nat -> Nat -> Bool
    forall a. Eq a => a -> a -> Bool
    == [a] -> Nat
    forall (t :: * -> *) a. Foldable t => t a -> Nat
    length [a]
    vs) Bool -> [Bool] -> [Bool]
    forall a. a -> [a] -> [a]
    : (a -> a -> Bool) -> [a] -> [a] -> [Bool]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith a -> a -> Bool
    forall a. EqualSy a => a -> a -> Bool
    equalSy [a]
    us [a]
    vs

    instance EqualSy Term where
      equalSy :: Term -> Term -> Bool
    equalSy = ((Term, Term) -> Bool) -> Term -> Term -> Bool
    forall a b c. ((a, b) -> c) -> a -> b -> c
    curry (((Term, Term) -> Bool) -> Term -> Term -> Bool)
    -> ((Term, Term) -> Bool) -> Term -> Term -> Bool
    forall a b. (a -> b) -> a -> b
    $ \case
        (Var Nat
    i   [Elim' Term]
    vs, Var Nat
    i'   [Elim' Term]
    vs') -> Nat
    i Nat -> Nat -> Bool
    forall a. Eq a => a -> a -> Bool
    == Nat
    i' Bool -> Bool -> Bool
    && [Elim' Term] -> [Elim' Term] -> Bool
    forall a. EqualSy a => a -> a -> Bool
    equalSy [Elim' Term]
    vs [Elim' Term]
    vs'
        (Con ConHead
    c ConInfo
    _ [Elim' Term]
    es, Con ConHead
    c' ConInfo
    _ [Elim' Term]
    es') -> ConHead
    c ConHead -> ConHead -> Bool
    forall a. Eq a => a -> a -> Bool
    == ConHead
    c' Bool -> Bool -> Bool
    && [Elim' Term] -> [Elim' Term] -> Bool
    forall a. EqualSy a => a -> a -> Bool
    equalSy [Elim' Term]
    es [Elim' Term]
    es'
        (Def   QName
    f [Elim' Term]
    es, Def   QName
    f' [Elim' Term]
    es') -> QName
    f QName -> QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == QName
    f' Bool -> Bool -> Bool
    && [Elim' Term] -> [Elim' Term] -> Bool
    forall a. EqualSy a => a -> a -> Bool
    equalSy [Elim' Term]
    es [Elim' Term]
    es'
        (MetaV MetaId
    x [Elim' Term]
    es, MetaV MetaId
    x' [Elim' Term]
    es') -> MetaId
    x MetaId -> MetaId -> Bool
    forall a. Eq a => a -> a -> Bool
    == MetaId
    x' Bool -> Bool -> Bool
    && [Elim' Term] -> [Elim' Term] -> Bool
    forall a. EqualSy a => a -> a -> Bool
    equalSy [Elim' Term]
    es [Elim' Term]
    es'
        (Lit   Literal
    l   , Lit   Literal
    l'    ) -> Literal
    l Literal -> Literal -> Bool
    forall a. Eq a => a -> a -> Bool
    == Literal
    l'
        (Lam   ArgInfo
    ai Abs Term
    b, Lam   ArgInfo
    ai' Abs Term
    b') -> ArgInfo -> ArgInfo -> Bool
    forall a. EqualSy a => a -> a -> Bool
    equalSy ArgInfo
    ai ArgInfo
    ai' Bool -> Bool -> Bool
    && Abs Term -> Abs Term -> Bool
    forall a. EqualSy a => a -> a -> Bool
    equalSy Abs Term
    b Abs Term
    b'
        (Level Level
    l   , Level Level
    l'    ) -> Level -> Level -> Bool
    forall a. EqualSy a => a -> a -> Bool
    equalSy Level
    l Level
    l'
        (Sort  Sort' Term
    s   , Sort  Sort' Term
    s'    ) -> Sort' Term -> Sort' Term -> Bool
    forall a. EqualSy a => a -> a -> Bool
    equalSy Sort' Term
    s Sort' Term
    s'
        (Pi    Dom Type
    a Abs Type
    b , Pi    Dom Type
    a' Abs Type
    b' ) -> Dom Type -> Dom Type -> Bool
    forall a. EqualSy a => a -> a -> Bool
    equalSy Dom Type
    a Dom Type
    a' Bool -> Bool -> Bool
    && Abs Type -> Abs Type -> Bool
    forall a. EqualSy a => a -> a -> Bool
    equalSy Abs Type
    b Abs Type
    b'
        (DontCare Term
    _, DontCare Term
    _  ) -> Bool
    True
           -- Irrelevant things are syntactically equal.
        (Dummy{}   , Term
    _           ) -> Bool
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        (Term
    _         , Dummy{}     ) -> Bool
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        (Term, Term)
    _ -> Bool
    False

    instance EqualSy Level where
      equalSy :: Level -> Level -> Bool
    equalSy (Max Integer
    n [PlusLevel' Term]
    vs) (Max Integer
    n' [PlusLevel' Term]
    vs') = Integer
    n Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == Integer
    n' Bool -> Bool -> Bool
    && [PlusLevel' Term] -> [PlusLevel' Term] -> Bool
    forall a. EqualSy a => a -> a -> Bool
    equalSy [PlusLevel' Term]
    vs [PlusLevel' Term]
    vs'

    instance EqualSy PlusLevel where
      equalSy :: PlusLevel' Term -> PlusLevel' Term -> Bool
    equalSy (Plus Integer
    n Term
    v) (Plus Integer
    n' Term
    v') = Integer
    n Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == Integer
    n' Bool -> Bool -> Bool
    && Term -> Term -> Bool
    forall a. EqualSy a => a -> a -> Bool
    equalSy Term
    v Term
    v'

    instance EqualSy Sort where
      equalSy :: Sort' Term -> Sort' Term -> Bool
    equalSy = ((Sort' Term, Sort' Term) -> Bool)
    -> Sort' Term -> Sort' Term -> Bool
    forall a b c. ((a, b) -> c) -> a -> b -> c
    curry (((Sort' Term, Sort' Term) -> Bool)
     -> Sort' Term -> Sort' Term -> Bool)
    -> ((Sort' Term, Sort' Term) -> Bool)
    -> Sort' Term
    -> Sort' Term
    -> Bool
    forall a b. (a -> b) -> a -> b
    $ \case
        (Type Level
    l    , Type Level
    l'     ) -> Level -> Level -> Bool
    forall a. EqualSy a => a -> a -> Bool
    equalSy Level
    l Level
    l'
        (Prop Level
    l    , Prop Level
    l'     ) -> Level -> Level -> Bool
    forall a. EqualSy a => a -> a -> Bool
    equalSy Level
    l Level
    l'
        (Inf IsFibrant
    f Integer
    m   , Inf IsFibrant
    f' Integer
    n    ) -> IsFibrant
    f IsFibrant -> IsFibrant -> Bool
    forall a. Eq a => a -> a -> Bool
    == IsFibrant
    f' Bool -> Bool -> Bool
    && Integer
    m Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == Integer
    n
        (SSet Level
    l    , SSet Level
    l'     ) -> Level -> Level -> Bool
    forall a. EqualSy a => a -> a -> Bool
    equalSy Level
    l Level
    l'
        (Sort' Term
    SizeUniv  , Sort' Term
    SizeUniv    ) -> Bool
    True
        (PiSort Dom' Term Term
    a Sort' Term
    b Abs (Sort' Term)
    c, PiSort Dom' Term Term
    a' Sort' Term
    b' Abs (Sort' Term)
    c') -> Dom' Term Term -> Dom' Term Term -> Bool
    forall a. EqualSy a => a -> a -> Bool
    equalSy Dom' Term Term
    a Dom' Term Term
    a' Bool -> Bool -> Bool
    && Sort' Term -> Sort' Term -> Bool
    forall a. EqualSy a => a -> a -> Bool
    equalSy Sort' Term
    b Sort' Term
    b' Bool -> Bool -> Bool
    && Abs (Sort' Term) -> Abs (Sort' Term) -> Bool
    forall a. EqualSy a => a -> a -> Bool
    equalSy Abs (Sort' Term)
    c Abs (Sort' Term)
    c'
        (FunSort Sort' Term
    a Sort' Term
    b, FunSort Sort' Term
    a' Sort' Term
    b') -> Sort' Term -> Sort' Term -> Bool
    forall a. EqualSy a => a -> a -> Bool
    equalSy Sort' Term
    a Sort' Term
    a' Bool -> Bool -> Bool
    && Sort' Term -> Sort' Term -> Bool
    forall a. EqualSy a => a -> a -> Bool
    equalSy Sort' Term
    b Sort' Term
    b'
        (UnivSort Sort' Term
    a, UnivSort Sort' Term
    a' ) -> Sort' Term -> Sort' Term -> Bool
    forall a. EqualSy a => a -> a -> Bool
    equalSy Sort' Term
    a Sort' Term
    a'
        (MetaS MetaId
    x [Elim' Term]
    es, MetaS MetaId
    x' [Elim' Term]
    es') -> MetaId
    x MetaId -> MetaId -> Bool
    forall a. Eq a => a -> a -> Bool
    == MetaId
    x' Bool -> Bool -> Bool
    && [Elim' Term] -> [Elim' Term] -> Bool
    forall a. EqualSy a => a -> a -> Bool
    equalSy [Elim' Term]
    es [Elim' Term]
    es'
        (DefS  QName
    d [Elim' Term]
    es, DefS  QName
    d' [Elim' Term]
    es') -> QName
    d QName -> QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == QName
    d' Bool -> Bool -> Bool
    && [Elim' Term] -> [Elim' Term] -> Bool
    forall a. EqualSy a => a -> a -> Bool
    equalSy [Elim' Term]
    es [Elim' Term]
    es'
        (DummyS{}  , Sort' Term
    _           ) -> Bool
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        (Sort' Term
    _         , DummyS{}    ) -> Bool
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        (Sort' Term, Sort' Term)
    _ -> Bool
    False

    -- | Ignores sorts.
    instance EqualSy Type where
      equalSy :: Type -> Type -> Bool
    equalSy = Term -> Term -> Bool
    forall a. EqualSy a => a -> a -> Bool
    equalSy (Term -> Term -> Bool) -> (Type -> Term) -> Type -> Type -> Bool
    forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
    `on` Type -> Term
    forall t a. Type'' t a -> a
    unEl

    instance EqualSy a => EqualSy (Elim' a) where
      equalSy :: Elim' a -> Elim' a -> Bool
    equalSy = ((Elim' a, Elim' a) -> Bool) -> Elim' a -> Elim' a -> Bool
    forall a b c. ((a, b) -> c) -> a -> b -> c
    curry (((Elim' a, Elim' a) -> Bool) -> Elim' a -> Elim' a -> Bool)
    -> ((Elim' a, Elim' a) -> Bool) -> Elim' a -> Elim' a -> Bool
    forall a b. (a -> b) -> a -> b
    $ \case
        (Proj ProjOrigin
    _ QName
    f, Proj ProjOrigin
    _ QName
    f') -> QName
    f QName -> QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == QName
    f'
        (Apply Arg a
    a, Apply Arg a
    a') -> Arg a -> Arg a -> Bool
    forall a. EqualSy a => a -> a -> Bool
    equalSy Arg a
    a Arg a
    a'
        (IApply a
    u a
    v a
    r, IApply a
    u' a
    v' a
    r') ->
               a -> a -> Bool
    forall a. EqualSy a => a -> a -> Bool
    equalSy a
    u a
    u'
            Bool -> Bool -> Bool
    && a -> a -> Bool
    forall a. EqualSy a => a -> a -> Bool
    equalSy a
    v a
    v'
            Bool -> Bool -> Bool
    && a -> a -> Bool
    forall a. EqualSy a => a -> a -> Bool
    equalSy a
    r a
    r'
        (Elim' a, Elim' a)
    _ -> Bool
    False

    -- | Ignores 'absName'.
    instance (Subst a, EqualSy a) => EqualSy (Abs a) where
      equalSy :: Abs a -> Abs a -> Bool
    equalSy = ((Abs a, Abs a) -> Bool) -> Abs a -> Abs a -> Bool
    forall a b c. ((a, b) -> c) -> a -> b -> c
    curry (((Abs a, Abs a) -> Bool) -> Abs a -> Abs a -> Bool)
    -> ((Abs a, Abs a) -> Bool) -> Abs a -> Abs a -> Bool
    forall a b. (a -> b) -> a -> b
    $ \case
        (NoAbs String
    _x a
    b, NoAbs String
    _x' a
    b') -> a -> a -> Bool
    forall a. EqualSy a => a -> a -> Bool
    equalSy a
    b a
    b' -- no need to raise if both are NoAbs
        (Abs a
    a         , Abs a
    a'          ) -> a -> a -> Bool
    forall a. EqualSy a => a -> a -> Bool
    equalSy (Abs a -> a
    forall a. Subst a => Abs a -> a
    absBody Abs a
    a) (Abs a -> a
    forall a. Subst a => Abs a -> a
    absBody Abs a
    a')

    -- | Ignore origin and free variables.
    instance EqualSy ArgInfo where
      equalSy :: ArgInfo -> ArgInfo -> Bool
    equalSy (ArgInfo Hiding
    h Modality
    m Origin
    _o FreeVariables
    _fv Annotation
    a) (ArgInfo Hiding
    h' Modality
    m' Origin
    _o' FreeVariables
    _fv' Annotation
    a') =
        Hiding
    h Hiding -> Hiding -> Bool
    forall a. Eq a => a -> a -> Bool
    == Hiding
    h' Bool -> Bool -> Bool
    && Modality
    m Modality -> Modality -> Bool
    forall a. Eq a => a -> a -> Bool
    == Modality
    m' Bool -> Bool -> Bool
    && Annotation
    a Annotation -> Annotation -> Bool
    forall a. Eq a => a -> a -> Bool
    == Annotation
    a'

    -- | Ignore the tactic.
    instance EqualSy a => EqualSy (Dom a) where
      equalSy :: Dom a -> Dom a -> Bool
    equalSy d :: Dom a
    d@(Dom ArgInfo
    ai Bool
    b Maybe NamedName
    x Maybe Term
    _tac a
    a) d' :: Dom a
    d'@(Dom ArgInfo
    ai' Bool
    b' Maybe NamedName
    x' Maybe Term
    _tac' a
    a') = [Bool] -> Bool
    forall (t :: * -> *). Foldable t => t Bool -> Bool
    and
        [ Maybe NamedName
    x Maybe NamedName -> Maybe NamedName -> Bool
    forall a. Eq a => a -> a -> Bool
    == Maybe NamedName
    x'
        , Bool
    b Bool -> Bool -> Bool
    forall a. Eq a => a -> a -> Bool
    == Bool
    b'
        , ArgInfo -> ArgInfo -> Bool
    forall a. EqualSy a => a -> a -> Bool
    equalSy ArgInfo
    ai ArgInfo
    ai'
        , a -> a -> Bool
    forall a. EqualSy a => a -> a -> Bool
    equalSy a
    a a
    a'
        ]

    -- | Ignores irrelevant arguments and modality.
    --   (And, of course, origin and free variables).
    instance EqualSy a => EqualSy (Arg a) where
      equalSy :: Arg a -> Arg a -> Bool
    equalSy (Arg (ArgInfo Hiding
    h Modality
    m Origin
    _o FreeVariables
    _fv Annotation
    a) a
    v) (Arg (ArgInfo Hiding
    h' Modality
    m' Origin
    _o' FreeVariables
    _fv' Annotation
    a') a
    v') =
        Hiding
    h Hiding -> Hiding -> Bool
    forall a. Eq a => a -> a -> Bool
    == Hiding
    h' Bool -> Bool -> Bool
    && (Modality -> Bool
    forall a. LensRelevance a => a -> Bool
    isIrrelevant Modality
    m Bool -> Bool -> Bool
    || Modality -> Bool
    forall a. LensRelevance a => a -> Bool
    isIrrelevant Modality
    m' Bool -> Bool -> Bool
    || a -> a -> Bool
    forall a. EqualSy a => a -> a -> Bool
    equalSy a
    v a
    v')
        -- Andreas, 2017-10-04, issue #2775,
        -- ignore irrelevant arguments during with-abstraction.
        -- 2019-07-05, issue #3889, don't ignore quantity during caching
        -- this is why we let equalSy replace (==).