    -- | A syntactic equality check that takes meta instantiations into account,
    --   but does not reduce.  It replaces
    --   @
    --      (v, v') <- instantiateFull (v, v')
    --      v == v'
    --   @
    --   by a more efficient routine which only traverses and instantiates the terms
    --   as long as they are equal.

    module Agda.TypeChecking.SyntacticEquality (SynEq, checkSyntacticEquality) where

    import Control.Arrow            ( (***) )
    import Control.Monad            ( zipWithM )
    import Control.Monad.State      ( MonadState(..), StateT, runStateT )
    import Control.Monad.Trans      ( lift )

    import Agda.Interaction.Options ( optSyntacticEquality )

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

    import Agda.TypeChecking.Monad (ReduceM, MonadReduce(..), pragmaOptions, isInstantiatedMeta)
    import Agda.TypeChecking.Reduce
    import Agda.TypeChecking.Substitute

    import Agda.Utils.Monad (ifM)

    -- | Syntactic equality check for terms.
    --   @
    --      checkSyntacticEquality v v' = do
    --        (v, v') <- instantiateFull (v, v')
    --         return ((v, v'), v==v')
    --   @
    --   only that @v, v'@ are only fully instantiated to the depth
    --   where they are equal.
    --
    --   This means in particular that the returned @v,v'@ cannot be @MetaV@s
    --   that are instantiated.

    {-# SPECIALIZE checkSyntacticEquality :: Term -> Term -> ReduceM ((Term, Term), Bool) #-}
    {-# SPECIALIZE checkSyntacticEquality :: Type -> Type -> ReduceM ((Type, Type), Bool) #-}
    checkSyntacticEquality :: (Instantiate a, SynEq a, MonadReduce m) => a -> a -> m ((a, a), Bool)
    checkSyntacticEquality :: forall a (m :: * -> *).
    (Instantiate a, SynEq a, MonadReduce m) =>
    a -> a -> m ((a, a), Bool)
    checkSyntacticEquality a
    v a
    v' = ReduceM ((a, a), Bool) -> m ((a, a), Bool)
    forall (m :: * -> *) a. MonadReduce m => ReduceM a -> m a
    liftReduce (ReduceM ((a, a), Bool) -> m ((a, a), Bool))
    -> ReduceM ((a, a), Bool) -> m ((a, a), Bool)
    forall a b. (a -> b) -> a -> b
    $ do
      ReduceM Bool
    -> ReduceM ((a, a), Bool)
    -> ReduceM ((a, a), Bool)
    -> ReduceM ((a, a), Bool)
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
    ifM (PragmaOptions -> Bool
    optSyntacticEquality (PragmaOptions -> Bool) -> ReduceM PragmaOptions -> ReduceM Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ReduceM PragmaOptions
    forall (m :: * -> *). HasOptions m => m PragmaOptions
    pragmaOptions)
      {-then-} (a -> a -> SynEqM (a, a)
    forall a. SynEq a => a -> a -> SynEqM (a, a)
    synEq a
    v a
    v' SynEqM (a, a) -> Bool -> ReduceM ((a, a), Bool)
    forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
    `runStateT` Bool
    True)
      {-else-} ((,Bool
    False) ((a, a) -> ((a, a), Bool))
    -> ReduceM (a, a) -> ReduceM ((a, a), Bool)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (a, a) -> ReduceM (a, a)
    forall a (m :: * -> *). (Instantiate a, MonadReduce m) => a -> m a
    instantiate (a
    v,a
    v'))

    -- | Monad for checking syntactic equality
    type SynEqM = StateT Bool ReduceM

    -- | Return, flagging inequalty.
    inequal :: a -> SynEqM a
    inequal :: forall a. a -> SynEqM a
    inequal a
    a = Bool -> StateT Bool ReduceM ()
    forall s (m :: * -> *). MonadState s m => s -> m ()
    put Bool
    False StateT Bool ReduceM ()
    -> StateT Bool ReduceM a -> StateT Bool ReduceM a
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> a -> StateT Bool ReduceM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return a
    a

    -- | If inequality is flagged, return, else continue.
    ifEqual :: (a -> SynEqM a) -> (a -> SynEqM a)
    ifEqual :: forall a. (a -> SynEqM a) -> a -> SynEqM a
    ifEqual a -> SynEqM a
    cont a
    a = StateT Bool ReduceM Bool -> SynEqM a -> SynEqM a -> SynEqM a
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
    ifM StateT Bool ReduceM Bool
    forall s (m :: * -> *). MonadState s m => m s
    get (a -> SynEqM a
    cont a
    a) (a -> SynEqM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return a
    a)

    -- Since List2 is only Applicative, not a monad, I cannot
    -- define a List2T monad transformer, so we do it manually:

    (<$$>) :: Functor f => (a -> b) -> f (a, a) -> f (b, b)
    a -> b
    f <$$> :: forall (f :: * -> *) a b.
    Functor f =>
    (a -> b) -> f (a, a) -> f (b, b)
    <$$> f (a, a)
    xx = (a -> b
    f (a -> b) -> (a -> b) -> (a, a) -> (b, b)
    forall (a :: * -> * -> *) b c b' c'.
    Arrow a =>
    a b c -> a b' c' -> a (b, b') (c, c')
    *** a -> b
    f) ((a, a) -> (b, b)) -> f (a, a) -> f (b, b)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> f (a, a)
    xx

    pure2 :: Applicative f => a -> f (a, a)
    pure2 :: forall (f :: * -> *) a. Applicative f => a -> f (a, a)
    pure2 a
    a = (a, a) -> f (a, a)
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (a
    a, a
    a)

    (<**>) :: Applicative f => f (a -> b, a -> b) -> f (a, a) -> f (b, b)
    f (a -> b, a -> b)
    ff <**> :: forall (f :: * -> *) a b.
    Applicative f =>
    f (a -> b, a -> b) -> f (a, a) -> f (b, b)
    <**> f (a, a)
    xx = (((a -> b) -> (a -> b) -> (a, a) -> (b, b))
    -> (a -> b, a -> b) -> (a, a) -> (b, b)
    forall a b c. (a -> b -> c) -> (a, b) -> c
    uncurry (a -> b) -> (a -> b) -> (a, a) -> (b, b)
    forall (a :: * -> * -> *) b c b' c'.
    Arrow a =>
    a b c -> a b' c' -> a (b, b') (c, c')
    (***)) ((a -> b, a -> b) -> (a, a) -> (b, b))
    -> f (a -> b, a -> b) -> f ((a, a) -> (b, b))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> f (a -> b, a -> b)
    ff f ((a, a) -> (b, b)) -> f (a, a) -> f (b, b)
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> f (a, a)
    xx

    -- | Instantiate full as long as things are equal
    class SynEq a where
      synEq  :: a -> a -> SynEqM (a, a)
      synEq' :: a -> a -> SynEqM (a, a)
      synEq' a
    a a
    a' = ((a, a) -> SynEqM (a, a)) -> (a, a) -> SynEqM (a, a)
    forall a. (a -> SynEqM a) -> a -> SynEqM a
    ifEqual ((a -> a -> SynEqM (a, a)) -> (a, a) -> SynEqM (a, a)
    forall a b c. (a -> b -> c) -> (a, b) -> c
    uncurry a -> a -> SynEqM (a, a)
    forall a. SynEq a => a -> a -> SynEqM (a, a)
    synEq) (a
    a, a
    a')

    instance SynEq Bool where
      synEq :: Bool -> Bool -> SynEqM (Bool, Bool)
    synEq Bool
    x Bool
    y | Bool
    x Bool -> Bool -> Bool
    forall a. Eq a => a -> a -> Bool
    == Bool
    y    = (Bool, Bool) -> SynEqM (Bool, Bool)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Bool
    x, Bool
    y)
      synEq Bool
    x Bool
    y | Bool
    otherwise = (Bool, Bool) -> SynEqM (Bool, Bool)
    forall a. a -> SynEqM a
    inequal (Bool
    x, Bool
    y)

    -- | Syntactic term equality ignores 'DontCare' stuff.
    instance SynEq Term where
      synEq :: Term -> Term -> SynEqM (Term, Term)
    synEq Term
    v Term
    v' = do
        (Term
    v, Term
    v') <- ReduceM (Term, Term) -> SynEqM (Term, Term)
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (ReduceM (Term, Term) -> SynEqM (Term, Term))
    -> ReduceM (Term, Term) -> SynEqM (Term, Term)
    forall a b. (a -> b) -> a -> b
    $ (Term, Term) -> ReduceM (Term, Term)
    forall t. Instantiate t => t -> ReduceM t
    instantiate' (Term
    v, Term
    v')
        case (Term
    v, Term
    v') of
          (Var   Int
    i Elims
    vs, Var   Int
    i' Elims
    vs') | Int
    i Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    i' -> Int -> Elims -> Term
    Var Int
    i   (Elims -> Term)
    -> StateT Bool ReduceM (Elims, Elims) -> SynEqM (Term, Term)
    forall (f :: * -> *) a b.
    Functor f =>
    (a -> b) -> f (a, a) -> f (b, b)
    <$$> Elims -> Elims -> StateT Bool ReduceM (Elims, Elims)
    forall a. SynEq a => a -> a -> SynEqM (a, a)
    synEq Elims
    vs Elims
    vs'
          (Con ConHead
    c ConInfo
    i Elims
    vs, Con ConHead
    c' ConInfo
    i' Elims
    vs') | ConHead
    c ConHead -> ConHead -> Bool
    forall a. Eq a => a -> a -> Bool
    == ConHead
    c' -> ConHead -> ConInfo -> Elims -> Term
    Con ConHead
    c (ConInfo -> ConInfo -> ConInfo
    bestConInfo ConInfo
    i ConInfo
    i') (Elims -> Term)
    -> StateT Bool ReduceM (Elims, Elims) -> SynEqM (Term, Term)
    forall (f :: * -> *) a b.
    Functor f =>
    (a -> b) -> f (a, a) -> f (b, b)
    <$$> Elims -> Elims -> StateT Bool ReduceM (Elims, Elims)
    forall a. SynEq a => a -> a -> SynEqM (a, a)
    synEq Elims
    vs Elims
    vs'
          (Def   QName
    f Elims
    vs, Def   QName
    f' Elims
    vs') | QName
    f QName -> QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == QName
    f' -> QName -> Elims -> Term
    Def QName
    f   (Elims -> Term)
    -> StateT Bool ReduceM (Elims, Elims) -> SynEqM (Term, Term)
    forall (f :: * -> *) a b.
    Functor f =>
    (a -> b) -> f (a, a) -> f (b, b)
    <$$> Elims -> Elims -> StateT Bool ReduceM (Elims, Elims)
    forall a. SynEq a => a -> a -> SynEqM (a, a)
    synEq Elims
    vs Elims
    vs'
          (MetaV MetaId
    x Elims
    vs, MetaV MetaId
    x' Elims
    vs') | MetaId
    x MetaId -> MetaId -> Bool
    forall a. Eq a => a -> a -> Bool
    == MetaId
    x' -> MetaId -> Elims -> Term
    MetaV MetaId
    x (Elims -> Term)
    -> StateT Bool ReduceM (Elims, Elims) -> SynEqM (Term, Term)
    forall (f :: * -> *) a b.
    Functor f =>
    (a -> b) -> f (a, a) -> f (b, b)
    <$$> Elims -> Elims -> StateT Bool ReduceM (Elims, Elims)
    forall a. SynEq a => a -> a -> SynEqM (a, a)
    synEq Elims
    vs Elims
    vs'
          (Lit   Literal
    l   , Lit   Literal
    l'    ) | Literal
    l Literal -> Literal -> Bool
    forall a. Eq a => a -> a -> Bool
    == Literal
    l' -> Term -> SynEqM (Term, Term)
    forall (f :: * -> *) a. Applicative f => a -> f (a, a)
    pure2 (Term -> SynEqM (Term, Term)) -> Term -> SynEqM (Term, Term)
    forall a b. (a -> b) -> a -> b
    $ Term
    v
          (Lam   ArgInfo
    h Abs Term
    b , Lam   ArgInfo
    h' Abs Term
    b' )           -> ArgInfo -> Abs Term -> Term
    Lam (ArgInfo -> Abs Term -> Term)
    -> StateT Bool ReduceM (ArgInfo, ArgInfo)
    -> StateT Bool ReduceM (Abs Term -> Term, Abs Term -> Term)
    forall (f :: * -> *) a b.
    Functor f =>
    (a -> b) -> f (a, a) -> f (b, b)
    <$$> ArgInfo -> ArgInfo -> StateT Bool ReduceM (ArgInfo, ArgInfo)
    forall a. SynEq a => a -> a -> SynEqM (a, a)
    synEq ArgInfo
    h ArgInfo
    h' StateT Bool ReduceM (Abs Term -> Term, Abs Term -> Term)
    -> StateT Bool ReduceM (Abs Term, Abs Term) -> SynEqM (Term, Term)
    forall (f :: * -> *) a b.
    Applicative f =>
    f (a -> b, a -> b) -> f (a, a) -> f (b, b)
    <**> Abs Term -> Abs Term -> StateT Bool ReduceM (Abs Term, Abs Term)
    forall a. SynEq a => a -> a -> SynEqM (a, a)
    synEq Abs Term
    b Abs Term
    b'
          (Level Level
    l   , Level Level
    l'    )           -> Level -> Term
    levelTm (Level -> Term)
    -> StateT Bool ReduceM (Level, Level) -> SynEqM (Term, Term)
    forall (f :: * -> *) a b.
    Functor f =>
    (a -> b) -> f (a, a) -> f (b, b)
    <$$> Level -> Level -> StateT Bool ReduceM (Level, Level)
    forall a. SynEq a => a -> a -> SynEqM (a, a)
    synEq Level
    l Level
    l'
          (Sort  Sort
    s   , Sort  Sort
    s'    )           -> Sort -> Term
    Sort    (Sort -> Term)
    -> StateT Bool ReduceM (Sort, Sort) -> SynEqM (Term, Term)
    forall (f :: * -> *) a b.
    Functor f =>
    (a -> b) -> f (a, a) -> f (b, b)
    <$$> Sort -> Sort -> StateT Bool ReduceM (Sort, Sort)
    forall a. SynEq a => a -> a -> SynEqM (a, a)
    synEq Sort
    s Sort
    s'
          (Pi    Dom Type
    a Abs Type
    b , Pi    Dom Type
    a' Abs Type
    b' )           -> Dom Type -> Abs Type -> Term
    Pi      (Dom Type -> Abs Type -> Term)
    -> StateT Bool ReduceM (Dom Type, Dom Type)
    -> StateT Bool ReduceM (Abs Type -> Term, Abs Type -> Term)
    forall (f :: * -> *) a b.
    Functor f =>
    (a -> b) -> f (a, a) -> f (b, b)
    <$$> Dom Type -> Dom Type -> StateT Bool ReduceM (Dom Type, Dom Type)
    forall a. SynEq a => a -> a -> SynEqM (a, a)
    synEq Dom Type
    a Dom Type
    a' StateT Bool ReduceM (Abs Type -> Term, Abs Type -> Term)
    -> StateT Bool ReduceM (Abs Type, Abs Type) -> SynEqM (Term, Term)
    forall (f :: * -> *) a b.
    Applicative f =>
    f (a -> b, a -> b) -> f (a, a) -> f (b, b)
    <**> Abs Type -> Abs Type -> StateT Bool ReduceM (Abs Type, Abs Type)
    forall a. SynEq a => a -> a -> SynEqM (a, a)
    synEq' Abs Type
    b Abs Type
    b'
          (DontCare Term
    u, DontCare Term
    u' )           -> Term -> Term
    DontCare (Term -> Term) -> SynEqM (Term, Term) -> SynEqM (Term, Term)
    forall (f :: * -> *) a b.
    Functor f =>
    (a -> b) -> f (a, a) -> f (b, b)
    <$$> Term -> Term -> SynEqM (Term, Term)
    forall a. SynEq a => a -> a -> SynEqM (a, a)
    synEq Term
    u Term
    u'
             -- Irrelevant things are not syntactically equal. ALT:
             -- pure (u, u')
             -- Jesper, 2019-10-21: considering irrelevant things to be
             -- syntactically equal causes implicit arguments to go
             -- unsolved, so it is better to go under the DontCare.
          (Dummy{}   , Dummy{}     )           -> (Term, Term) -> SynEqM (Term, Term)
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Term
    v, Term
    v')
          (Term, Term)
    _                                    -> (Term, Term) -> SynEqM (Term, Term)
    forall a. a -> SynEqM a
    inequal (Term
    v, Term
    v')

    instance SynEq Level where
      synEq :: Level -> Level -> StateT Bool ReduceM (Level, Level)
    synEq l :: Level
    l@(Max Integer
    n [PlusLevel]
    vs) l' :: Level
    l'@(Max Integer
    n' [PlusLevel]
    vs')
        | Integer
    n Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == Integer
    n'   = Integer -> [PlusLevel] -> Level
    levelMax Integer
    n ([PlusLevel] -> Level)
    -> StateT Bool ReduceM ([PlusLevel], [PlusLevel])
    -> StateT Bool ReduceM (Level, Level)
    forall (f :: * -> *) a b.
    Functor f =>
    (a -> b) -> f (a, a) -> f (b, b)
    <$$> [PlusLevel]
    -> [PlusLevel] -> StateT Bool ReduceM ([PlusLevel], [PlusLevel])
    forall a. SynEq a => a -> a -> SynEqM (a, a)
    synEq [PlusLevel]
    vs [PlusLevel]
    vs'
        | Bool
    otherwise = (Level, Level) -> StateT Bool ReduceM (Level, Level)
    forall a. a -> SynEqM a
    inequal (Level
    l, Level
    l')

    instance SynEq PlusLevel where
      synEq :: PlusLevel -> PlusLevel -> SynEqM (PlusLevel, PlusLevel)
    synEq l :: PlusLevel
    l@(Plus Integer
    n Term
    v) l' :: PlusLevel
    l'@(Plus Integer
    n' Term
    v')
        | Integer
    n Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == Integer
    n'   = Integer -> Term -> PlusLevel
    forall t. Integer -> t -> PlusLevel' t
    Plus Integer
    n (Term -> PlusLevel)
    -> SynEqM (Term, Term) -> SynEqM (PlusLevel, PlusLevel)
    forall (f :: * -> *) a b.
    Functor f =>
    (a -> b) -> f (a, a) -> f (b, b)
    <$$> Term -> Term -> SynEqM (Term, Term)
    forall a. SynEq a => a -> a -> SynEqM (a, a)
    synEq Term
    v Term
    v'
        | Bool
    otherwise = (PlusLevel, PlusLevel) -> SynEqM (PlusLevel, PlusLevel)
    forall a. a -> SynEqM a
    inequal (PlusLevel
    l, PlusLevel
    l')

    instance SynEq Sort where
      synEq :: Sort -> Sort -> StateT Bool ReduceM (Sort, Sort)
    synEq Sort
    s Sort
    s' = do
        (Sort
    s, Sort
    s') <- ReduceM (Sort, Sort) -> StateT Bool ReduceM (Sort, Sort)
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (ReduceM (Sort, Sort) -> StateT Bool ReduceM (Sort, Sort))
    -> ReduceM (Sort, Sort) -> StateT Bool ReduceM (Sort, Sort)
    forall a b. (a -> b) -> a -> b
    $ (Sort, Sort) -> ReduceM (Sort, Sort)
    forall t. Instantiate t => t -> ReduceM t
    instantiate' (Sort
    s, Sort
    s')
        case (Sort
    s, Sort
    s') of
          (Type Level
    l  , Type Level
    l'   ) -> Level -> Sort
    forall t. Level' t -> Sort' t
    Type (Level -> Sort)
    -> StateT Bool ReduceM (Level, Level)
    -> StateT Bool ReduceM (Sort, Sort)
    forall (f :: * -> *) a b.
    Functor f =>
    (a -> b) -> f (a, a) -> f (b, b)
    <$$> Level -> Level -> StateT Bool ReduceM (Level, Level)
    forall a. SynEq a => a -> a -> SynEqM (a, a)
    synEq Level
    l Level
    l'
          (PiSort Dom' Term Term
    a Sort
    b Abs Sort
    c, PiSort Dom' Term Term
    a' Sort
    b' Abs Sort
    c') -> Dom' Term Term -> Sort -> Abs Sort -> Sort
    piSort (Dom' Term Term -> Sort -> Abs Sort -> Sort)
    -> StateT Bool ReduceM (Dom' Term Term, Dom' Term Term)
    -> StateT
         Bool ReduceM (Sort -> Abs Sort -> Sort, Sort -> Abs Sort -> Sort)
    forall (f :: * -> *) a b.
    Functor f =>
    (a -> b) -> f (a, a) -> f (b, b)
    <$$> Dom' Term Term
    -> Dom' Term Term
    -> StateT Bool ReduceM (Dom' Term Term, Dom' Term Term)
    forall a. SynEq a => a -> a -> SynEqM (a, a)
    synEq Dom' Term Term
    a Dom' Term Term
    a' StateT
      Bool ReduceM (Sort -> Abs Sort -> Sort, Sort -> Abs Sort -> Sort)
    -> StateT Bool ReduceM (Sort, Sort)
    -> StateT Bool ReduceM (Abs Sort -> Sort, Abs Sort -> Sort)
    forall (f :: * -> *) a b.
    Applicative f =>
    f (a -> b, a -> b) -> f (a, a) -> f (b, b)
    <**> Sort -> Sort -> StateT Bool ReduceM (Sort, Sort)
    forall a. SynEq a => a -> a -> SynEqM (a, a)
    synEq' Sort
    b Sort
    b' StateT Bool ReduceM (Abs Sort -> Sort, Abs Sort -> Sort)
    -> StateT Bool ReduceM (Abs Sort, Abs Sort)
    -> StateT Bool ReduceM (Sort, Sort)
    forall (f :: * -> *) a b.
    Applicative f =>
    f (a -> b, a -> b) -> f (a, a) -> f (b, b)
    <**> Abs Sort -> Abs Sort -> StateT Bool ReduceM (Abs Sort, Abs Sort)
    forall a. SynEq a => a -> a -> SynEqM (a, a)
    synEq' Abs Sort
    c Abs Sort
    c'
          (FunSort Sort
    a Sort
    b, FunSort Sort
    a' Sort
    b') -> Sort -> Sort -> Sort
    funSort (Sort -> Sort -> Sort)
    -> StateT Bool ReduceM (Sort, Sort)
    -> StateT Bool ReduceM (Sort -> Sort, Sort -> Sort)
    forall (f :: * -> *) a b.
    Functor f =>
    (a -> b) -> f (a, a) -> f (b, b)
    <$$> Sort -> Sort -> StateT Bool ReduceM (Sort, Sort)
    forall a. SynEq a => a -> a -> SynEqM (a, a)
    synEq Sort
    a Sort
    a' StateT Bool ReduceM (Sort -> Sort, Sort -> Sort)
    -> StateT Bool ReduceM (Sort, Sort)
    -> StateT Bool ReduceM (Sort, Sort)
    forall (f :: * -> *) a b.
    Applicative f =>
    f (a -> b, a -> b) -> f (a, a) -> f (b, b)
    <**> Sort -> Sort -> StateT Bool ReduceM (Sort, Sort)
    forall a. SynEq a => a -> a -> SynEqM (a, a)
    synEq' Sort
    b Sort
    b'
          (UnivSort Sort
    a, UnivSort Sort
    a') -> Sort -> Sort
    forall t. Sort' t -> Sort' t
    UnivSort (Sort -> Sort)
    -> StateT Bool ReduceM (Sort, Sort)
    -> StateT Bool ReduceM (Sort, Sort)
    forall (f :: * -> *) a b.
    Functor f =>
    (a -> b) -> f (a, a) -> f (b, b)
    <$$> Sort -> Sort -> StateT Bool ReduceM (Sort, Sort)
    forall a. SynEq a => a -> a -> SynEqM (a, a)
    synEq Sort
    a Sort
    a'
          (Sort
    SizeUniv, Sort
    SizeUniv  ) -> Sort -> StateT Bool ReduceM (Sort, Sort)
    forall (f :: * -> *) a. Applicative f => a -> f (a, a)
    pure2 Sort
    s
          (Sort
    LockUniv, Sort
    LockUniv  ) -> Sort -> StateT Bool ReduceM (Sort, Sort)
    forall (f :: * -> *) a. Applicative f => a -> f (a, a)
    pure2 Sort
    s
          (Prop Level
    l  , Prop Level
    l'   ) -> Level -> Sort
    forall t. Level' t -> Sort' t
    Prop (Level -> Sort)
    -> StateT Bool ReduceM (Level, Level)
    -> StateT Bool ReduceM (Sort, Sort)
    forall (f :: * -> *) a b.
    Functor f =>
    (a -> b) -> f (a, a) -> f (b, b)
    <$$> Level -> Level -> StateT Bool ReduceM (Level, Level)
    forall a. SynEq a => a -> a -> SynEqM (a, a)
    synEq 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', Integer
    m Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == Integer
    n -> Sort -> StateT Bool ReduceM (Sort, Sort)
    forall (f :: * -> *) a. Applicative f => a -> f (a, a)
    pure2 Sort
    s
          (SSet Level
    l  , SSet Level
    l'   ) -> Level -> Sort
    forall t. Level' t -> Sort' t
    SSet (Level -> Sort)
    -> StateT Bool ReduceM (Level, Level)
    -> StateT Bool ReduceM (Sort, Sort)
    forall (f :: * -> *) a b.
    Functor f =>
    (a -> b) -> f (a, a) -> f (b, b)
    <$$> Level -> Level -> StateT Bool ReduceM (Level, Level)
    forall a. SynEq a => a -> a -> SynEqM (a, a)
    synEq Level
    l Level
    l'
          (MetaS MetaId
    x Elims
    es , MetaS MetaId
    x' Elims
    es') | MetaId
    x MetaId -> MetaId -> Bool
    forall a. Eq a => a -> a -> Bool
    == MetaId
    x' -> MetaId -> Elims -> Sort
    forall t. MetaId -> [Elim' t] -> Sort' t
    MetaS MetaId
    x (Elims -> Sort)
    -> StateT Bool ReduceM (Elims, Elims)
    -> StateT Bool ReduceM (Sort, Sort)
    forall (f :: * -> *) a b.
    Functor f =>
    (a -> b) -> f (a, a) -> f (b, b)
    <$$> Elims -> Elims -> StateT Bool ReduceM (Elims, Elims)
    forall a. SynEq a => a -> a -> SynEqM (a, a)
    synEq Elims
    es Elims
    es'
          (DefS  QName
    d Elims
    es , DefS  QName
    d' Elims
    es') | QName
    d QName -> QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == QName
    d' -> QName -> Elims -> Sort
    forall t. QName -> [Elim' t] -> Sort' t
    DefS QName
    d  (Elims -> Sort)
    -> StateT Bool ReduceM (Elims, Elims)
    -> StateT Bool ReduceM (Sort, Sort)
    forall (f :: * -> *) a b.
    Functor f =>
    (a -> b) -> f (a, a) -> f (b, b)
    <$$> Elims -> Elims -> StateT Bool ReduceM (Elims, Elims)
    forall a. SynEq a => a -> a -> SynEqM (a, a)
    synEq Elims
    es Elims
    es'
          (DummyS{}, DummyS{}) -> (Sort, Sort) -> StateT Bool ReduceM (Sort, Sort)
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Sort
    s, Sort
    s')
          (Sort, Sort)
    _ -> (Sort, Sort) -> StateT Bool ReduceM (Sort, Sort)
    forall a. a -> SynEqM a
    inequal (Sort
    s, Sort
    s')

    -- | Syntactic equality ignores sorts.
    instance SynEq Type where
      synEq :: Type -> Type -> SynEqM (Type, Type)
    synEq (El Sort
    s Term
    t) (El Sort
    s' Term
    t') = (Sort -> Term -> Type
    forall t a. Sort' t -> a -> Type'' t a
    El Sort
    s (Term -> Type) -> (Term -> Type) -> (Term, Term) -> (Type, Type)
    forall (a :: * -> * -> *) b c b' c'.
    Arrow a =>
    a b c -> a b' c' -> a (b, b') (c, c')
    *** Sort -> Term -> Type
    forall t a. Sort' t -> a -> Type'' t a
    El Sort
    s') ((Term, Term) -> (Type, Type))
    -> SynEqM (Term, Term) -> SynEqM (Type, Type)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Term -> Term -> SynEqM (Term, Term)
    forall a. SynEq a => a -> a -> SynEqM (a, a)
    synEq Term
    t Term
    t'

    instance SynEq a => SynEq [a] where
      synEq :: [a] -> [a] -> SynEqM ([a], [a])
    synEq [a]
    as [a]
    as'
        | [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [a]
    as Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [a]
    as' = [(a, a)] -> ([a], [a])
    forall a b. [(a, b)] -> ([a], [b])
    unzip ([(a, a)] -> ([a], [a]))
    -> StateT Bool ReduceM [(a, a)] -> SynEqM ([a], [a])
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (a -> a -> StateT Bool ReduceM (a, a))
    -> [a] -> [a] -> StateT Bool ReduceM [(a, a)]
    forall (m :: * -> *) a b c.
    Applicative m =>
    (a -> b -> m c) -> [a] -> [b] -> m [c]
    zipWithM a -> a -> StateT Bool ReduceM (a, a)
    forall a. SynEq a => a -> a -> SynEqM (a, a)
    synEq' [a]
    as [a]
    as'
        | Bool
    otherwise               = ([a], [a]) -> SynEqM ([a], [a])
    forall a. a -> SynEqM a
    inequal ([a]
    as, [a]
    as')

    instance (SynEq a, SynEq b) => SynEq (a,b) where
      synEq :: (a, b) -> (a, b) -> SynEqM ((a, b), (a, b))
    synEq (a
    a,b
    b) (a
    a',b
    b') = (,) (a -> b -> (a, b))
    -> StateT Bool ReduceM (a, a)
    -> StateT Bool ReduceM (b -> (a, b), b -> (a, b))
    forall (f :: * -> *) a b.
    Functor f =>
    (a -> b) -> f (a, a) -> f (b, b)
    <$$> a -> a -> StateT Bool ReduceM (a, a)
    forall a. SynEq a => a -> a -> SynEqM (a, a)
    synEq a
    a a
    a' StateT Bool ReduceM (b -> (a, b), b -> (a, b))
    -> StateT Bool ReduceM (b, b) -> SynEqM ((a, b), (a, b))
    forall (f :: * -> *) a b.
    Applicative f =>
    f (a -> b, a -> b) -> f (a, a) -> f (b, b)
    <**> b -> b -> StateT Bool ReduceM (b, b)
    forall a. SynEq a => a -> a -> SynEqM (a, a)
    synEq b
    b b
    b'

    instance SynEq a => SynEq (Elim' a) where
      synEq :: Elim' a -> Elim' a -> SynEqM (Elim' a, Elim' a)
    synEq Elim' a
    e Elim' a
    e' =
        case (Elim' a
    e, Elim' a
    e') of
          (Proj ProjOrigin
    _ QName
    f, Proj ProjOrigin
    _ QName
    f') | QName
    f QName -> QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == QName
    f' -> Elim' a -> SynEqM (Elim' a, Elim' a)
    forall (f :: * -> *) a. Applicative f => a -> f (a, a)
    pure2 Elim' a
    e
          (Apply Arg a
    a, Apply Arg a
    a') -> Arg a -> Elim' a
    forall a. Arg a -> Elim' a
    Apply (Arg a -> Elim' a)
    -> StateT Bool ReduceM (Arg a, Arg a) -> SynEqM (Elim' a, Elim' a)
    forall (f :: * -> *) a b.
    Functor f =>
    (a -> b) -> f (a, a) -> f (b, b)
    <$$> Arg a -> Arg a -> StateT Bool ReduceM (Arg a, Arg a)
    forall a. SynEq a => a -> a -> SynEqM (a, a)
    synEq Arg a
    a Arg a
    a'
          (IApply a
    u a
    v a
    r, IApply a
    u' a
    v' a
    r')
                              -> (a -> a -> a -> Elim' a
    forall a. a -> a -> a -> Elim' a
    IApply a
    u a
    v (a -> Elim' a) -> (a -> Elim' a) -> (a, a) -> (Elim' a, Elim' a)
    forall (a :: * -> * -> *) b c b' c'.
    Arrow a =>
    a b c -> a b' c' -> a (b, b') (c, c')
    *** a -> a -> a -> Elim' a
    forall a. a -> a -> a -> Elim' a
    IApply a
    u' a
    v') ((a, a) -> (Elim' a, Elim' a))
    -> StateT Bool ReduceM (a, a) -> SynEqM (Elim' a, Elim' a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> a -> a -> StateT Bool ReduceM (a, a)
    forall a. SynEq a => a -> a -> SynEqM (a, a)
    synEq a
    r a
    r'
          (Elim' a, Elim' a)
    _                   -> (Elim' a, Elim' a) -> SynEqM (Elim' a, Elim' a)
    forall a. a -> SynEqM a
    inequal (Elim' a
    e, Elim' a
    e')

    instance (Subst a, SynEq a) => SynEq (Abs a) where
      synEq :: Abs a -> Abs a -> SynEqM (Abs a, Abs a)
    synEq Abs a
    a Abs a
    a' =
        case (Abs a
    a, Abs a
    a') of
          (NoAbs ArgName
    x a
    b, NoAbs ArgName
    x' a
    b') -> (ArgName -> a -> Abs a
    forall a. ArgName -> a -> Abs a
    NoAbs ArgName
    x (a -> Abs a) -> (a -> Abs a) -> (a, a) -> (Abs a, Abs a)
    forall (a :: * -> * -> *) b c b' c'.
    Arrow a =>
    a b c -> a b' c' -> a (b, b') (c, c')
    *** ArgName -> a -> Abs a
    forall a. ArgName -> a -> Abs a
    NoAbs ArgName
    x') ((a, a) -> (Abs a, Abs a))
    -> StateT Bool ReduceM (a, a) -> SynEqM (Abs a, Abs a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$>  a -> a -> StateT Bool ReduceM (a, a)
    forall a. SynEq a => a -> a -> SynEqM (a, a)
    synEq a
    b a
    b'
          (Abs   ArgName
    x a
    b, Abs   ArgName
    x' a
    b') -> (ArgName -> a -> Abs a
    forall a. ArgName -> a -> Abs a
    Abs ArgName
    x (a -> Abs a) -> (a -> Abs a) -> (a, a) -> (Abs a, Abs a)
    forall (a :: * -> * -> *) b c b' c'.
    Arrow a =>
    a b c -> a b' c' -> a (b, b') (c, c')
    *** ArgName -> a -> Abs a
    forall a. ArgName -> a -> Abs a
    Abs ArgName
    x') ((a, a) -> (Abs a, Abs a))
    -> StateT Bool ReduceM (a, a) -> SynEqM (Abs a, Abs a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> a -> a -> StateT Bool ReduceM (a, a)
    forall a. SynEq a => a -> a -> SynEqM (a, a)
    synEq a
    b a
    b'
          (Abs   ArgName
    x a
    b, NoAbs ArgName
    x' a
    b') -> ArgName -> a -> Abs a
    forall a. ArgName -> a -> Abs a
    Abs ArgName
    x  (a -> Abs a) -> StateT Bool ReduceM (a, a) -> SynEqM (Abs a, Abs a)
    forall (f :: * -> *) a b.
    Functor f =>
    (a -> b) -> f (a, a) -> f (b, b)
    <$$> a -> a -> StateT Bool ReduceM (a, a)
    forall a. SynEq a => a -> a -> SynEqM (a, a)
    synEq a
    b (Int -> a -> a
    forall a. Subst a => Int -> a -> a
    raise Int
    1 a
    b')  -- TODO: mkAbs?
          (NoAbs ArgName
    x a
    b, Abs   ArgName
    x' a
    b') -> ArgName -> a -> Abs a
    forall a. ArgName -> a -> Abs a
    Abs ArgName
    x' (a -> Abs a) -> StateT Bool ReduceM (a, a) -> SynEqM (Abs a, Abs a)
    forall (f :: * -> *) a b.
    Functor f =>
    (a -> b) -> f (a, a) -> f (b, b)
    <$$> a -> a -> StateT Bool ReduceM (a, a)
    forall a. SynEq a => a -> a -> SynEqM (a, a)
    synEq (Int -> a -> a
    forall a. Subst a => Int -> a -> a
    raise Int
    1 a
    b) a
    b'

    -- NOTE: Do not ignore 'ArgInfo', or test/fail/UnequalHiding will pass.
    instance SynEq a => SynEq (Arg a) where
      synEq :: Arg a -> Arg a -> SynEqM (Arg a, Arg a)
    synEq (Arg ArgInfo
    ai a
    a) (Arg ArgInfo
    ai' a
    a') = ArgInfo -> a -> Arg a
    forall e. ArgInfo -> e -> Arg e
    Arg (ArgInfo -> a -> Arg a)
    -> StateT Bool ReduceM (ArgInfo, ArgInfo)
    -> StateT Bool ReduceM (a -> Arg a, a -> Arg a)
    forall (f :: * -> *) a b.
    Functor f =>
    (a -> b) -> f (a, a) -> f (b, b)
    <$$> ArgInfo -> ArgInfo -> StateT Bool ReduceM (ArgInfo, ArgInfo)
    forall a. SynEq a => a -> a -> SynEqM (a, a)
    synEq ArgInfo
    ai ArgInfo
    ai' StateT Bool ReduceM (a -> Arg a, a -> Arg a)
    -> StateT Bool ReduceM (a, a) -> SynEqM (Arg a, Arg a)
    forall (f :: * -> *) a b.
    Applicative f =>
    f (a -> b, a -> b) -> f (a, a) -> f (b, b)
    <**> a -> a -> StateT Bool ReduceM (a, a)
    forall a. SynEq a => a -> a -> SynEqM (a, a)
    synEq a
    a a
    a'

    -- Ignore the tactic.
    instance SynEq a => SynEq (Dom a) where
      synEq :: Dom a -> Dom a -> SynEqM (Dom a, Dom a)
    synEq d :: Dom a
    d@(Dom ArgInfo
    ai Bool
    b Maybe NamedName
    x Maybe Term
    t a
    a) d' :: Dom a
    d'@(Dom ArgInfo
    ai' Bool
    b' Maybe NamedName
    x' Maybe Term
    _ a
    a')
        | Maybe NamedName
    x Maybe NamedName -> Maybe NamedName -> Bool
    forall a. Eq a => a -> a -> Bool
    == Maybe NamedName
    x'   = ArgInfo -> Bool -> Maybe NamedName -> Maybe Term -> a -> Dom a
    forall t e.
    ArgInfo -> Bool -> Maybe NamedName -> Maybe t -> e -> Dom' t e
    Dom (ArgInfo -> Bool -> Maybe NamedName -> Maybe Term -> a -> Dom a)
    -> StateT Bool ReduceM (ArgInfo, ArgInfo)
    -> StateT
         Bool
         ReduceM
         (Bool -> Maybe NamedName -> Maybe Term -> a -> Dom a,
          Bool -> Maybe NamedName -> Maybe Term -> a -> Dom a)
    forall (f :: * -> *) a b.
    Functor f =>
    (a -> b) -> f (a, a) -> f (b, b)
    <$$> ArgInfo -> ArgInfo -> StateT Bool ReduceM (ArgInfo, ArgInfo)
    forall a. SynEq a => a -> a -> SynEqM (a, a)
    synEq ArgInfo
    ai ArgInfo
    ai' StateT
      Bool
      ReduceM
      (Bool -> Maybe NamedName -> Maybe Term -> a -> Dom a,
       Bool -> Maybe NamedName -> Maybe Term -> a -> Dom a)
    -> SynEqM (Bool, Bool)
    -> StateT
         Bool
         ReduceM
         (Maybe NamedName -> Maybe Term -> a -> Dom a,
          Maybe NamedName -> Maybe Term -> a -> Dom a)
    forall (f :: * -> *) a b.
    Applicative f =>
    f (a -> b, a -> b) -> f (a, a) -> f (b, b)
    <**> Bool -> Bool -> SynEqM (Bool, Bool)
    forall a. SynEq a => a -> a -> SynEqM (a, a)
    synEq Bool
    b Bool
    b' StateT
      Bool
      ReduceM
      (Maybe NamedName -> Maybe Term -> a -> Dom a,
       Maybe NamedName -> Maybe Term -> a -> Dom a)
    -> StateT Bool ReduceM (Maybe NamedName, Maybe NamedName)
    -> StateT
         Bool ReduceM (Maybe Term -> a -> Dom a, Maybe Term -> a -> Dom a)
    forall (f :: * -> *) a b.
    Applicative f =>
    f (a -> b, a -> b) -> f (a, a) -> f (b, b)
    <**> Maybe NamedName
    -> StateT Bool ReduceM (Maybe NamedName, Maybe NamedName)
    forall (f :: * -> *) a. Applicative f => a -> f (a, a)
    pure2 Maybe NamedName
    x StateT
      Bool ReduceM (Maybe Term -> a -> Dom a, Maybe Term -> a -> Dom a)
    -> StateT Bool ReduceM (Maybe Term, Maybe Term)
    -> StateT Bool ReduceM (a -> Dom a, a -> Dom a)
    forall (f :: * -> *) a b.
    Applicative f =>
    f (a -> b, a -> b) -> f (a, a) -> f (b, b)
    <**> Maybe Term -> StateT Bool ReduceM (Maybe Term, Maybe Term)
    forall (f :: * -> *) a. Applicative f => a -> f (a, a)
    pure2 Maybe Term
    t StateT Bool ReduceM (a -> Dom a, a -> Dom a)
    -> StateT Bool ReduceM (a, a) -> SynEqM (Dom a, Dom a)
    forall (f :: * -> *) a b.
    Applicative f =>
    f (a -> b, a -> b) -> f (a, a) -> f (b, b)
    <**> a -> a -> StateT Bool ReduceM (a, a)
    forall a. SynEq a => a -> a -> SynEqM (a, a)
    synEq a
    a a
    a'
        | Bool
    otherwise = (Dom a, Dom a) -> SynEqM (Dom a, Dom a)
    forall a. a -> SynEqM a
    inequal (Dom a
    d, Dom a
    d')

    instance SynEq ArgInfo where
      synEq :: ArgInfo -> ArgInfo -> StateT Bool ReduceM (ArgInfo, ArgInfo)
    synEq ai :: ArgInfo
    ai@(ArgInfo Hiding
    h Modality
    r Origin
    o FreeVariables
    _ Annotation
    a) ai' :: ArgInfo
    ai'@(ArgInfo Hiding
    h' Modality
    r' Origin
    o' FreeVariables
    _ Annotation
    a')
        | Hiding
    h Hiding -> Hiding -> Bool
    forall a. Eq a => a -> a -> Bool
    == Hiding
    h', Modality -> Modality -> Bool
    forall a b. (LensModality a, LensModality b) => a -> b -> Bool
    sameModality Modality
    r Modality
    r', Annotation
    a Annotation -> Annotation -> Bool
    forall a. Eq a => a -> a -> Bool
    == Annotation
    a' = ArgInfo -> StateT Bool ReduceM (ArgInfo, ArgInfo)
    forall (f :: * -> *) a. Applicative f => a -> f (a, a)
    pure2 ArgInfo
    ai
        | Bool
    otherwise        = (ArgInfo, ArgInfo) -> StateT Bool ReduceM (ArgInfo, ArgInfo)
    forall a. a -> SynEqM a
    inequal (ArgInfo
    ai, ArgInfo
    ai')