    {-# OPTIONS_GHC -Wunused-imports #-}

    -- | Functions for abstracting terms over other terms.

    module Agda.TypeChecking.Abstract where

    import Prelude hiding ( null )

    import Control.Monad
    import Control.Monad.Except

    import Data.Function ( on )
    import qualified Data.HashMap.Strict as HMap

    import Agda.Syntax.Common
    import Agda.Syntax.Position ( Range )
    import Agda.Syntax.Internal

    import Agda.TypeChecking.Free ( freeIn )
    import Agda.TypeChecking.MetaVars
    import Agda.TypeChecking.Monad
    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.TypeChecking.Warnings ( warning )

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

    import Agda.Utils.Impossible

    -- | @abstractType r a v b[v] = b@ where @a : v@.
    abstractType ::
         Range     -- ^ Range of the @rewrite@ expression, if any, otherwise empty.
      -> Type      -- ^ Type of the term to abstract.
      -> Term      -- ^ Term to abstract.
      -> Type      -- ^ Type to abstract in.
      -> TCM Type  -- ^ Type with hole (de Bruijn index 0) for the abstracted term.
    abstractType :: Range -> Type -> Term -> Type -> TCM Type
    abstractType Range
    r Type
    a Term
    v (El Sort' Term
    s Term
    b) = do

      c <- Sort' Term -> Term -> Type
    forall t a. Sort' t -> a -> Type'' t a
    El (Nat -> Term -> Sort' Term -> Sort' Term
    forall a. AbsTerm a => Nat -> Term -> a -> a
    absTerm Nat
    0 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
      unless (null r || 0 `freeIn` c) do
        -- Andreas, 2025-07-03, issue #7973
        -- If with abstraction did not abstract anything, warn the user.
        setCurrentRange r $ warning RewritesNothing
      return c

    -- | @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
      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
    <$> Range -> Type -> Term -> Type -> TCM Type
    abstractType Range
    forall a. Null a => a
    empty Type
    a Term
    v Type
    b
      reportSDoc "tc.abstract" 50 $
        sep [ "piAbstract" <+> sep [ prettyTCM v <+> ":", nest 2 $ prettyTCM a ]
            , nest 2 $ "from" <+> prettyTCM b
            , nest 2 $ "-->" <+> prettyTCM fun ]
      reportSDoc "tc.abstract" 70 $
        sep [ "piAbstract" <+> sep [ (text . show) v <+> ":", nest 2 $ (text . show) a ]
            , nest 2 $ "from" <+> (text . show) b
            , nest 2 $ "-->" <+> (text . show) fun ]
      return 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
      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
    <$> Range -> Type -> Term -> Type -> TCM Type
    abstractType Range
    forall a. Null a => a
    empty Type
    a Term
    v Type
    b
      eq <- addContext ("w" :: String, defaultDom a) $ do
        -- manufacture the type @w ≡ v@
        eqName <- primEqualityName
        eqTy <- defType <$> getConstInfo eqName
        -- E.g. @eqTy = eqTel → Set a@ where @eqTel = {a : Level} {A : Set a} (x y : A)@.
        TelV eqTel _ <- telView eqTy
        tel  <- newTelMeta (telFromList $ dropEnd 3 $ telToList eqTel)
        let eq = QName -> [Elim] -> Term
    Def QName
    eqName ([Elim] -> Term) -> [Elim] -> Term
    forall a b. (a -> b) -> a -> b
    $ (Arg Term -> Elim) -> Args -> [Elim]
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Term -> Elim
    forall a. Arg a -> Elim' a
    Apply
                     (Args -> [Elim]) -> Args -> [Elim]
    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]
    ++ [ Hiding -> Arg Term -> Arg Term
    forall a. LensHiding a => Hiding -> a -> a
    setHiding Hiding
    Hidden (Arg Term -> Arg Term) -> Arg Term -> Arg Term
    forall a b. (a -> b) -> a -> b
    $ Term -> Arg Term
    forall a. a -> Arg a
    defaultArg (Term -> Arg Term) -> Term -> Arg Term
    forall a b. (a -> b) -> a -> b
    $ Nat -> Term -> Term
    forall a. Subst a => Nat -> a -> a
    raise Nat
    1 (Term -> Term) -> Term -> Term
    forall a b. (a -> b) -> a -> b
    $ Type -> Term
    forall t a. Type'' t a -> a
    unEl Type
    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)
                        ]
        -- Since the result of this function will be type-checked in
        -- `withFunctionType`, we can be a little lazy here and put
        -- a meta for the sort.
        sort <- newSortMeta
        return $ El sort eq

      pure $ mkPi (setHiding (getHiding info) $ defaultDom ("w", a))
           $ mkPi (setHiding NotHidden        $ defaultDom ("eq", eq))
           $ b
    piAbstract (Arg ArgInfo
    info (Term
    prf, EqualityViewType eqt :: EqualityTypeData
    eqt@(EqualityTypeData Range
    r Sort' Term
    _ QName
    _ Args
    _ (Arg ArgInfo
    _ Term
    a) Arg Term
    v Arg Term
    _))) Type
    b = do
      s <- Term -> TCMT IO (Sort' Term)
    forall (m :: * -> *).
    (PureTCM m, MonadBlock m, MonadConstraint m) =>
    Term -> m (Sort' Term)
    sortOf Term
    a
      let prfTy :: Type
          prfTy = EqualityTypeData -> Type
    forall a. EqualityUnview a => a -> Type
    equalityUnview EqualityTypeData
    eqt
          vTy   = Sort' Term -> Term -> Type
    forall t a. Sort' t -> a -> Type'' t a
    El Sort' Term
    s Term
    a
      -- Andreas, 2025-07-03, issue #7973
      -- We alert the user when the lhs of the equality proof could not be abstracted
      -- but not when the equality proof itself could not be abstracted.
      -- Only the former means that the rewrite did not fire.
      b <- abstractType empty prfTy prf b  -- @empty@ means do not warn
      b <- addContext ("w" :: String, defaultDom prfTy) $
             -- Passing range @r@ here means warn if abstraction failed to abstract anything.
             abstractType r (raise 1 vTy) (unArg $ raise 1 v) b
      return . funType "lhs" vTy . funType "equality" eqTy' . swap01 $ 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 :: EqualityTypeData
        eqt1 :: EqualityTypeData
    eqt1  = Nat -> EqualityTypeData -> EqualityTypeData
    forall a. Subst a => Nat -> a -> a
    raise Nat
    1 EqualityTypeData
    eqt
        eqTy' :: Type
        eqTy' :: Type
    eqTy' = EqualityTypeData -> Type
    forall a. EqualityUnview a => a -> Type
    equalityUnview (EqualityTypeData -> Type) -> EqualityTypeData -> Type
    forall a b. (a -> b) -> a -> b
    $ EqualityTypeData
    eqt1{ _eqtLhs = _eqtLhs eqt1 $> var 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] -> [Elim] -> Maybe [Elim]
    isPrefixOf [Elim]
    us [Elim]
    vs = do
        (vs1, vs2) <- Nat -> [Elim] -> Maybe ([Elim], [Elim])
    forall n a. Integral n => n -> [a] -> Maybe ([a], [a])
    splitExactlyAt ([Elim] -> Nat
    forall a. [a] -> Nat
    forall (t :: * -> *) a. Foldable t => t a -> Nat
    length [Elim]
    us) [Elim]
    vs
        guard $ equalSy us vs1
        return vs2

    instance IsPrefixOf Args where
      isPrefixOf :: Args -> Args -> Maybe [Elim]
    isPrefixOf Args
    us Args
    vs = do
        (vs1, vs2) <- Nat -> Args -> Maybe (Args, Args)
    forall n a. Integral n => n -> [a] -> Maybe ([a], [a])
    splitExactlyAt (Args -> Nat
    forall a. [a] -> Nat
    forall (t :: * -> *) a. Foldable t => t a -> Nat
    length Args
    us) Args
    vs
        guard $ equalSy us vs1
        return $ map Apply vs2

    instance IsPrefixOf Term where
      isPrefixOf :: Term -> Term -> Maybe [Elim]
    isPrefixOf Term
    u Term
    v =
        case (Term
    u, Term
    v) of
          (Var   Nat
    i [Elim]
    us, Var   Nat
    j [Elim]
    vs) | Nat
    i Nat -> Nat -> Bool
    forall a. Eq a => a -> a -> Bool
    == Nat
    j  -> [Elim]
    us [Elim] -> [Elim] -> Maybe [Elim]
    forall a. IsPrefixOf a => a -> a -> Maybe [Elim]
    `isPrefixOf` [Elim]
    vs
          (Def   QName
    f [Elim]
    us, Def   QName
    g [Elim]
    vs) | QName
    f QName -> QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == QName
    g  -> [Elim]
    us [Elim] -> [Elim] -> Maybe [Elim]
    forall a. IsPrefixOf a => a -> a -> Maybe [Elim]
    `isPrefixOf` [Elim]
    vs
          (Con ConHead
    c ConInfo
    _ [Elim]
    us, Con ConHead
    d ConInfo
    _ [Elim]
    vs) | ConHead
    c ConHead -> ConHead -> Bool
    forall a. Eq a => a -> a -> Bool
    == ConHead
    d  -> [Elim]
    us [Elim] -> [Elim] -> Maybe [Elim]
    forall a. IsPrefixOf a => a -> a -> Maybe [Elim]
    `isPrefixOf` [Elim]
    vs
          (MetaV MetaId
    x [Elim]
    us, MetaV MetaId
    y [Elim]
    vs) | MetaId
    x MetaId -> MetaId -> Bool
    forall a. Eq a => a -> a -> Bool
    == MetaId
    y  -> [Elim]
    us [Elim] -> [Elim] -> Maybe [Elim]
    forall a. IsPrefixOf a => a -> a -> Maybe [Elim]
    `isPrefixOf` [Elim]
    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] -> Maybe [Elim]
    forall a b. Maybe a -> Maybe b -> Maybe b
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> [Elim] -> Maybe [Elim]
    forall a. a -> Maybe a
    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
    forall (m :: * -> *). MonadPretty m => Term -> 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
    forall (m :: * -> *). MonadPretty m => Type -> 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
    forall (m :: * -> *). MonadPretty m => Term -> 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
    forall (m :: * -> *). MonadPretty m => Type -> 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 ] ]

      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 a b. TCMT IO (a -> b) -> TCMT IO a -> TCMT IO b
    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
    forall (m :: * -> *). MonadFresh NameId m => String -> m Name
    freshName_ (String
    "hole" :: String)
      noMutualBlock $ addConstant' hole defaultArgInfo a defaultAxiom

      args <- map Apply <$> getContextArgs
      let n = [Elim] -> Nat
    forall a. [a] -> Nat
    forall (t :: * -> *) a. Foldable t => t a -> Nat
    length [Elim]
    args

      let abstr Type
    b Term
    v = do
            m <- TCMT IO Nat
    forall (m :: * -> *). MonadTCEnv m => m Nat
    getContextSize
            let (a', u') = raise (m - n) (a, u)
            case u' `isPrefixOf` v of
              Maybe [Elim]
    Nothing -> Term -> TCMT IO Term
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Term
    v
              Just [Elim]
    es -> do -- Check that the types match.
                s <- TCMT IO TCState
    forall (m :: * -> *). MonadTCState m => m TCState
    getTC
                do  noConstraints $ equalType a' b
                    putTC s
                    return $ Def hole (raise (m - n) args ++ es)
                  `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
    forall (m :: * -> *). MonadPretty m => Term -> 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
    forall (m :: * -> *). MonadPretty m => Type -> m Doc
    prettyTCM Type
    b ] ]
                    Term -> TCMT IO Term
    forall a. a -> TCMT IO a
    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.
      res <- catchError_ (checkInternal' (defaultAction { preAction = abstr }) v CmpLeq 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
    forall (m :: * -> *). MonadPretty m => Term -> 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
    forall (m :: * -> *). MonadPretty m => Type -> m Doc
    prettyTCM Type
    b))
            Term -> TCMT IO Term
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Term
    v
      reportSDoc "tc.abstract" 50 $ "Resulting abstraction" <?> prettyTCM res
      modifySignature $ updateDefinitions $ HMap.delete hole
      return $ absTerm 0 (Def hole args) res

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

    class AbsTerm a where
      -- | @subst j u . absTerm j u == id@
      absTerm ::
           Nat   -- ^ De Bruijn index that should be the placeholder for the abstracted term.
        -> Term  -- ^ Term to abstract.
        -> a     -- ^ Where to abstract.
        -> a     -- ^ If the given de Bruijn index is free in the result, abstraction actually happened.

    instance AbsTerm Term where
      absTerm :: Nat -> Term -> Term -> Term
    absTerm Nat
    j Term
    u Term
    v
        | Just [Elim]
    es <- Term
    u Term -> Term -> Maybe [Elim]
    forall a. IsPrefixOf a => a -> a -> Maybe [Elim]
    `isPrefixOf` Term
    v = Nat -> [Elim] -> Term
    Var Nat
    j ([Elim] -> Term) -> [Elim] -> Term
    forall a b. (a -> b) -> a -> b
    $ [Elim] -> [Elim]
    forall b. AbsTerm b => b -> b
    absT [Elim]
    es
        | Bool
    otherwise                   =
        case Term
    v of
    -- Andreas, 2013-10-20: the original impl. works only at base types
    --    v | u == v  -> Var j []  -- incomplete see succeed/WithOfFunctionType
          Var Nat
    i [Elim]
    vs    -> Nat -> [Elim] -> Term
    Var (if Nat
    i Nat -> Nat -> Bool
    forall a. Ord a => a -> a -> Bool
    < Nat
    j then Nat
    i else Nat
    i Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    + Nat
    1) ([Elim] -> Term) -> [Elim] -> Term
    forall a b. (a -> b) -> a -> b
    $ [Elim] -> [Elim]
    forall b. AbsTerm b => b -> b
    absT [Elim]
    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]
    vs    -> QName -> [Elim] -> Term
    Def QName
    c ([Elim] -> Term) -> [Elim] -> Term
    forall a b. (a -> b) -> a -> b
    $ [Elim] -> [Elim]
    forall b. AbsTerm b => b -> b
    absT [Elim]
    vs
          Con ConHead
    c ConInfo
    ci [Elim]
    vs -> ConHead -> ConInfo -> [Elim] -> Term
    Con ConHead
    c ConInfo
    ci ([Elim] -> Term) -> [Elim] -> Term
    forall a b. (a -> b) -> a -> b
    $ [Elim] -> [Elim]
    forall b. AbsTerm b => b -> b
    absT [Elim]
    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]
    vs  -> MetaId -> [Elim] -> Term
    MetaV MetaId
    m ([Elim] -> Term) -> [Elim] -> Term
    forall a b. (a -> b) -> a -> b
    $ [Elim] -> [Elim]
    forall b. AbsTerm b => b -> b
    absT [Elim]
    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]
    es   -> String -> [Elim] -> Term
    Dummy String
    s ([Elim] -> Term) -> [Elim] -> Term
    forall a b. (a -> b) -> a -> b
    $ [Elim] -> [Elim]
    forall b. AbsTerm b => b -> b
    absT [Elim]
    es
          where
            absT :: AbsTerm b => b -> b
            absT :: forall b. AbsTerm b => b -> b
    absT b
    x = Nat -> Term -> b -> b
    forall a. AbsTerm a => Nat -> Term -> a -> a
    absTerm Nat
    j Term
    u b
    x

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

    instance AbsTerm Sort where
      absTerm :: Nat -> Term -> Sort' Term -> Sort' Term
    absTerm Nat
    j Term
    u = \case
        Univ Univ
    u Level
    n   -> Univ -> Level -> Sort' Term
    forall t. Univ -> Level' t -> Sort' t
    Univ Univ
    u (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{}    -> Sort' Term
    s
        Sort' Term
    SizeUniv   -> Sort' Term
    forall t. Sort' t
    SizeUniv
        Sort' Term
    LockUniv   -> Sort' Term
    forall t. Sort' t
    LockUniv
        Sort' Term
    LevelUniv  -> Sort' Term
    forall t. Sort' t
    LevelUniv
        Sort' Term
    IntervalUniv -> Sort' Term
    forall t. Sort' t
    IntervalUniv
        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]
    es -> MetaId -> [Elim] -> Sort' Term
    forall t. MetaId -> [Elim' t] -> Sort' t
    MetaS MetaId
    x ([Elim] -> Sort' Term) -> [Elim] -> Sort' Term
    forall a b. (a -> b) -> a -> b
    $ [Elim] -> [Elim]
    forall b. AbsTerm b => b -> b
    absS [Elim]
    es
        DefS QName
    d [Elim]
    es  -> QName -> [Elim] -> Sort' Term
    forall t. QName -> [Elim' t] -> Sort' t
    DefS QName
    d ([Elim] -> Sort' Term) -> [Elim] -> Sort' Term
    forall a b. (a -> b) -> a -> b
    $ [Elim] -> [Elim]
    forall b. AbsTerm b => b -> b
    absS [Elim]
    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 = Nat -> Term -> b -> b
    forall a. AbsTerm a => Nat -> Term -> a -> a
    absTerm Nat
    j Term
    u b
    x

    instance AbsTerm Level where
      absTerm :: Nat -> Term -> Level -> Level
    absTerm Nat
    j 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
    $ Nat -> Term -> [PlusLevel' Term] -> [PlusLevel' Term]
    forall a. AbsTerm a => Nat -> Term -> a -> a
    absTerm Nat
    j Term
    u [PlusLevel' Term]
    as

    instance AbsTerm PlusLevel where
      absTerm :: Nat -> Term -> PlusLevel' Term -> PlusLevel' Term
    absTerm Nat
    j 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
    $ Nat -> Term -> Term -> Term
    forall a. AbsTerm a => Nat -> Term -> a -> a
    absTerm Nat
    j Term
    u Term
    l

    instance AbsTerm a => AbsTerm (Elim' a) where
      absTerm :: Nat -> Term -> Elim' a -> Elim' a
    absTerm Nat
    j = (a -> a) -> Elim' a -> Elim' a
    forall a b. (a -> b) -> Elim' a -> Elim' b
    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
    . Nat -> Term -> a -> a
    forall a. AbsTerm a => Nat -> Term -> a -> a
    absTerm Nat
    j

    instance AbsTerm a => AbsTerm (Arg a) where
      absTerm :: Nat -> Term -> Arg a -> Arg a
    absTerm Nat
    j = (a -> a) -> Arg a -> Arg a
    forall a b. (a -> b) -> Arg a -> Arg b
    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
    . Nat -> Term -> a -> a
    forall a. AbsTerm a => Nat -> Term -> a -> a
    absTerm Nat
    j

    instance AbsTerm a => AbsTerm (Dom a) where
      absTerm :: Nat -> Term -> Dom a -> Dom a
    absTerm Nat
    j = (a -> a) -> Dom a -> Dom a
    forall a b. (a -> b) -> Dom' Term a -> Dom' Term b
    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
    . Nat -> Term -> a -> a
    forall a. AbsTerm a => Nat -> Term -> a -> a
    absTerm Nat
    j

    instance AbsTerm a => AbsTerm [a] where
      absTerm :: Nat -> Term -> [a] -> [a]
    absTerm Nat
    j = (a -> a) -> [a] -> [a]
    forall a b. (a -> b) -> [a] -> [b]
    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
    . Nat -> Term -> a -> a
    forall a. AbsTerm a => Nat -> Term -> a -> a
    absTerm Nat
    j

    instance AbsTerm a => AbsTerm (Maybe a) where
      absTerm :: Nat -> Term -> Maybe a -> Maybe a
    absTerm Nat
    j = (a -> a) -> Maybe a -> Maybe a
    forall a b. (a -> b) -> Maybe a -> Maybe b
    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
    . Nat -> Term -> a -> a
    forall a. AbsTerm a => Nat -> Term -> a -> a
    absTerm Nat
    j

    instance (TermSubst a, AbsTerm a) => AbsTerm (Abs a) where
      absTerm :: Nat -> Term -> Abs a -> Abs a
    absTerm Nat
    j 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
    $ Nat -> Term -> a -> a
    forall a. AbsTerm a => Nat -> Term -> a -> a
    absTerm Nat
    j Term
    u a
    v
      absTerm Nat
    j 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
    $ Nat -> Term -> a -> a
    forall a. AbsTerm a => Nat -> Term -> a -> a
    absTerm (Nat
    j Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    + Nat
    1) (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 :: Nat -> Term -> (a, b) -> (a, b)
    absTerm Nat
    j Term
    u (a
    x, b
    y) = (Nat -> Term -> a -> a
    forall a. AbsTerm a => Nat -> Term -> a -> a
    absTerm Nat
    j Term
    u a
    x, Nat -> Term -> b -> b
    forall a. AbsTerm a => Nat -> Term -> a -> a
    absTerm Nat
    j 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 a. [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 a. [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]
    vs, Var Nat
    i'   [Elim]
    vs') -> Nat
    i Nat -> Nat -> Bool
    forall a. Eq a => a -> a -> Bool
    == Nat
    i' Bool -> Bool -> Bool
    && [Elim] -> [Elim] -> Bool
    forall a. EqualSy a => a -> a -> Bool
    equalSy [Elim]
    vs [Elim]
    vs'
        (Con ConHead
    c ConInfo
    _ [Elim]
    es, Con ConHead
    c' ConInfo
    _ [Elim]
    es') -> ConHead
    c ConHead -> ConHead -> Bool
    forall a. Eq a => a -> a -> Bool
    == ConHead
    c' Bool -> Bool -> Bool
    && [Elim] -> [Elim] -> Bool
    forall a. EqualSy a => a -> a -> Bool
    equalSy [Elim]
    es [Elim]
    es'
        (Def   QName
    f [Elim]
    es, Def   QName
    f' [Elim]
    es') -> QName
    f QName -> QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == QName
    f' Bool -> Bool -> Bool
    && [Elim] -> [Elim] -> Bool
    forall a. EqualSy a => a -> a -> Bool
    equalSy [Elim]
    es [Elim]
    es'
        (MetaV MetaId
    x [Elim]
    es, MetaV MetaId
    x' [Elim]
    es') -> MetaId
    x MetaId -> MetaId -> Bool
    forall a. Eq a => a -> a -> Bool
    == MetaId
    x' Bool -> Bool -> Bool
    && [Elim] -> [Elim] -> Bool
    forall a. EqualSy a => a -> a -> Bool
    equalSy [Elim]
    es [Elim]
    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
        (Univ Univ
    u Level
    l  , Univ Univ
    u' Level
    l'  ) -> Univ
    u Univ -> Univ -> Bool
    forall a. Eq a => a -> a -> Bool
    == Univ
    u' Bool -> Bool -> Bool
    && Level -> Level -> Bool
    forall a. EqualSy a => a -> a -> Bool
    equalSy Level
    l Level
    l'
        (Inf Univ
    u Integer
    m   , Inf Univ
    u' Integer
    n    ) -> Univ
    u Univ -> Univ -> Bool
    forall a. Eq a => a -> a -> Bool
    == Univ
    u' Bool -> Bool -> Bool
    && Integer
    m Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == Integer
    n
        (Sort' Term
    SizeUniv  , Sort' Term
    SizeUniv    ) -> Bool
    True
        (Sort' Term
    LevelUniv , Sort' Term
    LevelUniv   ) -> 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]
    es, MetaS MetaId
    x' [Elim]
    es') -> MetaId
    x MetaId -> MetaId -> Bool
    forall a. Eq a => a -> a -> Bool
    == MetaId
    x' Bool -> Bool -> Bool
    && [Elim] -> [Elim] -> Bool
    forall a. EqualSy a => a -> a -> Bool
    equalSy [Elim]
    es [Elim]
    es'
        (DefS  QName
    d [Elim]
    es, DefS  QName
    d' [Elim]
    es') -> QName
    d QName -> QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == QName
    d' Bool -> Bool -> Bool
    && [Elim] -> [Elim] -> Bool
    forall a. EqualSy a => a -> a -> Bool
    equalSy [Elim]
    es [Elim]
    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 Maybe NamedName
    x Bool
    f Maybe Term
    _tac a
    a) d' :: Dom a
    d'@(Dom ArgInfo
    ai' Maybe NamedName
    x' Bool
    f' 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
    f Bool -> Bool -> Bool
    forall a. Eq a => a -> a -> Bool
    == Bool
    f'
        , 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 (==).