-- | 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
  , checkSyntacticEquality'
  , syntacticEqualityFuelRemains
  )
  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(..), TCEnv(..), MonadTCEnv(..), pragmaOptions,
   isInstantiatedMeta)
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Substitute

import qualified Agda.Utils.Maybe.Strict as Strict
import Agda.Utils.Monad (ifM, and2M)

-- | Syntactic equality check for terms. If syntactic equality
-- checking has fuel left, then 'checkSyntacticEquality' behaves as if
-- it were implemented in the following way (which does not match the
-- given type signature), only that @v@ and @v'@ are only fully
-- instantiated to the depth where they are equal (and the amount of
-- fuel is reduced by one unit in the failure branch):
--   @
--      checkSyntacticEquality v v' s f = do
--        (v, v') <- instantiateFull (v, v')
--        if v == v' then s v v' else f v v'
--   @
-- If syntactic equality checking does not have fuel left, then
-- 'checkSyntacticEquality' instantiates the two terms and takes the
-- failure branch.
--
-- Note that in either case the returned values @v@ and @v'@ cannot be
-- @MetaV@s that are instantiated.

{-# SPECIALIZE checkSyntacticEquality ::
      Term -> Term ->
      (Term -> Term -> ReduceM a) ->
      (Term -> Term -> ReduceM a) ->
      ReduceM a #-}
{-# SPECIALIZE checkSyntacticEquality ::
      Type -> Type ->
      (Type -> Type -> ReduceM a) ->
      (Type -> Type -> ReduceM a) ->
      ReduceM a #-}
checkSyntacticEquality
  :: (Instantiate a, SynEq a, MonadReduce m)
  => a
  -> a
  -> (a -> a -> m b)  -- ^ Continuation used upon success.
  -> (a -> a -> m b)  -- ^ Continuation used upon failure, or if
                      --   syntactic equality checking has been turned
                      --   off.
  -> m b
checkSyntacticEquality :: forall a (m :: * -> *) b.
(Instantiate a, SynEq a, MonadReduce m) =>
a -> a -> (a -> a -> m b) -> (a -> a -> m b) -> m b
checkSyntacticEquality a
u a
v a -> a -> m b
s a -> a -> m b
f =
  forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM forall (m :: * -> *). MonadReduce m => m Bool
syntacticEqualityFuelRemains
  {-then-} (forall a (m :: * -> *) b.
(Instantiate a, SynEq a, MonadReduce m) =>
a -> a -> (a -> a -> m b) -> (a -> a -> m b) -> m b
checkSyntacticEquality' a
u a
v a -> a -> m b
s (\a
u a
v -> forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC TCEnv -> TCEnv
decreaseFuel (a -> a -> m b
f a
u a
v)))
  {-else-} (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry a -> a -> m b
f forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall a (m :: * -> *). (Instantiate a, MonadReduce m) => a -> m a
instantiate (a
u, a
v))
  where
  decreaseFuel :: TCEnv -> TCEnv
decreaseFuel TCEnv
env =
    case TCEnv -> Maybe Int
envSyntacticEqualityFuel TCEnv
env of
      Maybe Int
Strict.Nothing -> TCEnv
env
      Strict.Just Int
n  ->
        TCEnv
env { envSyntacticEqualityFuel :: Maybe Int
envSyntacticEqualityFuel = forall a. a -> Maybe a
Strict.Just (forall a. Enum a => a -> a
pred Int
n) }

-- | Syntactic equality check for terms without checking remaining fuel.

{-# SPECIALIZE checkSyntacticEquality' ::
      Term -> Term ->
      (Term -> Term -> ReduceM a) ->
      (Term -> Term -> ReduceM a) ->
      ReduceM a #-}
{-# SPECIALIZE checkSyntacticEquality' ::
      Type -> Type ->
      (Type -> Type -> ReduceM a) ->
      (Type -> Type -> ReduceM a) ->
      ReduceM a #-}
checkSyntacticEquality'
  :: (Instantiate a, SynEq a, MonadReduce m)
  => a
  -> a
  -> (a -> a -> m b)  -- ^ Continuation used upon success.
  -> (a -> a -> m b)  -- ^ Continuation used upon failure.
  -> m b
checkSyntacticEquality' :: forall a (m :: * -> *) b.
(Instantiate a, SynEq a, MonadReduce m) =>
a -> a -> (a -> a -> m b) -> (a -> a -> m b) -> m b
checkSyntacticEquality' a
u a
v a -> a -> m b
s a -> a -> m b
f = do
  ((a
u, a
v), Bool
equal) <- forall (m :: * -> *) a. MonadReduce m => ReduceM a -> m a
liftReduce forall a b. (a -> b) -> a -> b
$ forall a. SynEq a => a -> a -> SynEqM (a, a)
synEq a
u a
v forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
`runStateT` Bool
True
  if Bool
equal then a -> a -> m b
s a
u a
v else a -> a -> m b
f a
u a
v

-- | Does the syntactic equality check have any remaining fuel?

syntacticEqualityFuelRemains :: MonadReduce m => m Bool
syntacticEqualityFuelRemains :: forall (m :: * -> *). MonadReduce m => m Bool
syntacticEqualityFuelRemains = do
  Maybe Int
fuel <- TCEnv -> Maybe Int
envSyntacticEqualityFuel forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). MonadTCEnv m => m TCEnv
askTC
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ case Maybe Int
fuel of
    Maybe Int
Strict.Nothing -> Bool
True
    Strict.Just Int
n  -> Int
n forall a. Ord a => a -> a -> Bool
> Int
0

-- | 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 = forall s (m :: * -> *). MonadState s m => s -> m ()
put Bool
False forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> 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 = forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM forall s (m :: * -> *). MonadState s m => m s
get (a -> SynEqM a
cont a
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 forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
*** a -> b
f) 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 = 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 = (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
(***)) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f (a -> b, a -> b)
ff 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' = forall a. (a -> SynEqM a) -> a -> SynEqM a
ifEqual (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry 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 forall a. Eq a => a -> a -> Bool
== Bool
y    = forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
x, Bool
y)
  synEq Bool
x Bool
y | Bool
otherwise = 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') <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ 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 forall a. Eq a => a -> a -> Bool
== Int
i' -> Int -> Elims -> Term
Var Int
i   forall (f :: * -> *) a b.
Functor f =>
(a -> b) -> f (a, a) -> f (b, b)
<$$> 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 forall a. Eq a => a -> a -> Bool
== ConHead
c' -> ConHead -> ConInfo -> Elims -> Term
Con ConHead
c (ConInfo -> ConInfo -> ConInfo
bestConInfo ConInfo
i ConInfo
i') forall (f :: * -> *) a b.
Functor f =>
(a -> b) -> f (a, a) -> f (b, b)
<$$> 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 forall a. Eq a => a -> a -> Bool
== QName
f' -> QName -> Elims -> Term
Def QName
f   forall (f :: * -> *) a b.
Functor f =>
(a -> b) -> f (a, a) -> f (b, b)
<$$> 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 forall a. Eq a => a -> a -> Bool
== MetaId
x' -> MetaId -> Elims -> Term
MetaV MetaId
x forall (f :: * -> *) a b.
Functor f =>
(a -> b) -> f (a, a) -> f (b, b)
<$$> forall a. SynEq a => a -> a -> SynEqM (a, a)
synEq Elims
vs Elims
vs'
      (Lit   Literal
l   , Lit   Literal
l'    ) | Literal
l forall a. Eq a => a -> a -> Bool
== Literal
l' -> forall (f :: * -> *) a. Applicative f => a -> f (a, a)
pure2 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 forall (f :: * -> *) a b.
Functor f =>
(a -> b) -> f (a, a) -> f (b, b)
<$$> forall a. SynEq a => a -> a -> SynEqM (a, a)
synEq ArgInfo
h ArgInfo
h' forall (f :: * -> *) a b.
Applicative f =>
f (a -> b, a -> b) -> f (a, a) -> f (b, b)
<**> 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 forall (f :: * -> *) a b.
Functor f =>
(a -> b) -> f (a, a) -> f (b, b)
<$$> forall a. SynEq a => a -> a -> SynEqM (a, a)
synEq Level
l Level
l'
      (Sort  Sort
s   , Sort  Sort
s'    )           -> Sort -> Term
Sort    forall (f :: * -> *) a b.
Functor f =>
(a -> b) -> f (a, a) -> f (b, b)
<$$> 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      forall (f :: * -> *) a b.
Functor f =>
(a -> b) -> f (a, a) -> f (b, b)
<$$> forall a. SynEq a => a -> a -> SynEqM (a, a)
synEq Dom Type
a Dom Type
a' forall (f :: * -> *) a b.
Applicative f =>
f (a -> b, a -> b) -> f (a, a) -> f (b, b)
<**> 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 forall (f :: * -> *) a b.
Functor f =>
(a -> b) -> f (a, a) -> f (b, b)
<$$> 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{}     )           -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term
v, Term
v')
      (Term, Term)
_                                    -> forall a. a -> SynEqM a
inequal (Term
v, Term
v')

instance SynEq Level where
  synEq :: Level -> Level -> SynEqM (Level, Level)
synEq l :: Level
l@(Max Integer
n [PlusLevel]
vs) l' :: Level
l'@(Max Integer
n' [PlusLevel]
vs')
    | Integer
n forall a. Eq a => a -> a -> Bool
== Integer
n'   = Integer -> [PlusLevel] -> Level
levelMax Integer
n forall (f :: * -> *) a b.
Functor f =>
(a -> b) -> f (a, a) -> f (b, b)
<$$> forall a. SynEq a => a -> a -> SynEqM (a, a)
synEq [PlusLevel]
vs [PlusLevel]
vs'
    | Bool
otherwise = 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 forall a. Eq a => a -> a -> Bool
== Integer
n'   = forall t. Integer -> t -> PlusLevel' t
Plus Integer
n forall (f :: * -> *) a b.
Functor f =>
(a -> b) -> f (a, a) -> f (b, b)
<$$> forall a. SynEq a => a -> a -> SynEqM (a, a)
synEq Term
v Term
v'
    | Bool
otherwise = forall a. a -> SynEqM a
inequal (PlusLevel
l, PlusLevel
l')

instance SynEq Sort where
  synEq :: Sort -> Sort -> SynEqM (Sort, Sort)
synEq Sort
s Sort
s' = do
    (Sort
s, Sort
s') <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall t. Instantiate t => t -> ReduceM t
instantiate' (Sort
s, Sort
s')
    case (Sort
s, Sort
s') of
      (Type Level
l  , Type Level
l'   ) -> forall t. Level' t -> Sort' t
Type forall (f :: * -> *) a b.
Functor f =>
(a -> b) -> f (a, a) -> f (b, b)
<$$> forall a. SynEq a => a -> a -> SynEqM (a, a)
synEq Level
l Level
l'
      (PiSort Dom Term
a Sort
b Abs Sort
c, PiSort Dom Term
a' Sort
b' Abs Sort
c') -> Dom Term -> Sort -> Abs Sort -> Sort
piSort forall (f :: * -> *) a b.
Functor f =>
(a -> b) -> f (a, a) -> f (b, b)
<$$> forall a. SynEq a => a -> a -> SynEqM (a, a)
synEq Dom Term
a Dom Term
a' forall (f :: * -> *) a b.
Applicative f =>
f (a -> b, a -> b) -> f (a, a) -> f (b, b)
<**> forall a. SynEq a => a -> a -> SynEqM (a, a)
synEq' Sort
b Sort
b' forall (f :: * -> *) a b.
Applicative f =>
f (a -> b, a -> b) -> f (a, a) -> f (b, b)
<**> 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 forall (f :: * -> *) a b.
Functor f =>
(a -> b) -> f (a, a) -> f (b, b)
<$$> forall a. SynEq a => a -> a -> SynEqM (a, a)
synEq Sort
a Sort
a' forall (f :: * -> *) a b.
Applicative f =>
f (a -> b, a -> b) -> f (a, a) -> f (b, b)
<**> forall a. SynEq a => a -> a -> SynEqM (a, a)
synEq' Sort
b Sort
b'
      (UnivSort Sort
a, UnivSort Sort
a') -> forall t. Sort' t -> Sort' t
UnivSort forall (f :: * -> *) a b.
Functor f =>
(a -> b) -> f (a, a) -> f (b, b)
<$$> forall a. SynEq a => a -> a -> SynEqM (a, a)
synEq Sort
a Sort
a'
      (Sort
SizeUniv, Sort
SizeUniv  ) -> forall (f :: * -> *) a. Applicative f => a -> f (a, a)
pure2 Sort
s
      (Sort
LockUniv, Sort
LockUniv  ) -> forall (f :: * -> *) a. Applicative f => a -> f (a, a)
pure2 Sort
s
      (Sort
IntervalUniv, Sort
IntervalUniv) -> forall (f :: * -> *) a. Applicative f => a -> f (a, a)
pure2 Sort
s
      (Prop Level
l  , Prop Level
l'   ) -> forall t. Level' t -> Sort' t
Prop forall (f :: * -> *) a b.
Functor f =>
(a -> b) -> f (a, a) -> f (b, b)
<$$> 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 forall a. Eq a => a -> a -> Bool
== IsFibrant
f', Integer
m forall a. Eq a => a -> a -> Bool
== Integer
n -> forall (f :: * -> *) a. Applicative f => a -> f (a, a)
pure2 Sort
s
      (SSet Level
l  , SSet Level
l'   ) -> forall t. Level' t -> Sort' t
SSet forall (f :: * -> *) a b.
Functor f =>
(a -> b) -> f (a, a) -> f (b, b)
<$$> 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 forall a. Eq a => a -> a -> Bool
== MetaId
x' -> forall t. MetaId -> [Elim' t] -> Sort' t
MetaS MetaId
x forall (f :: * -> *) a b.
Functor f =>
(a -> b) -> f (a, a) -> f (b, b)
<$$> 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 forall a. Eq a => a -> a -> Bool
== QName
d' -> forall t. QName -> [Elim' t] -> Sort' t
DefS QName
d  forall (f :: * -> *) a b.
Functor f =>
(a -> b) -> f (a, a) -> f (b, b)
<$$> forall a. SynEq a => a -> a -> SynEqM (a, a)
synEq Elims
es Elims
es'
      (DummyS{}, DummyS{}) -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (Sort
s, Sort
s')
      (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') = (forall t a. Sort' t -> a -> Type'' t a
El Sort
s forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
*** forall t a. Sort' t -> a -> Type'' t a
El Sort
s') forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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'
    | forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
as forall a. Eq a => a -> a -> Bool
== forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
as' = forall a b. [(a, b)] -> ([a], [b])
unzip forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM forall a. SynEq a => a -> a -> SynEqM (a, a)
synEq' [a]
as [a]
as'
    | Bool
otherwise               = 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') = (,) forall (f :: * -> *) a b.
Functor f =>
(a -> b) -> f (a, a) -> f (b, b)
<$$> forall a. SynEq a => a -> a -> SynEqM (a, a)
synEq a
a a
a' forall (f :: * -> *) a b.
Applicative f =>
f (a -> b, a -> b) -> f (a, a) -> f (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 forall a. Eq a => a -> a -> Bool
== QName
f' -> forall (f :: * -> *) a. Applicative f => a -> f (a, a)
pure2 Elim' a
e
      (Apply Arg a
a, Apply Arg a
a') -> forall a. Arg a -> Elim' a
Apply forall (f :: * -> *) a b.
Functor f =>
(a -> b) -> f (a, a) -> f (b, b)
<$$> 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')
                          -> (forall a. a -> a -> a -> Elim' a
IApply a
u a
v forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
*** forall a. a -> a -> a -> Elim' a
IApply a
u' a
v') forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. SynEq a => a -> a -> SynEqM (a, a)
synEq a
r a
r'
      (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') -> (forall a. ArgName -> a -> Abs a
NoAbs ArgName
x forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
*** forall a. ArgName -> a -> Abs a
NoAbs ArgName
x') forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>  forall a. SynEq a => a -> a -> SynEqM (a, a)
synEq a
b a
b'
      (Abs   ArgName
x a
b, Abs   ArgName
x' a
b') -> (forall a. ArgName -> a -> Abs a
Abs ArgName
x forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
*** forall a. ArgName -> a -> Abs a
Abs ArgName
x') forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. SynEq a => a -> a -> SynEqM (a, a)
synEq a
b a
b'
      (Abs   ArgName
x a
b, NoAbs ArgName
x' a
b') -> forall a. ArgName -> a -> Abs a
Abs ArgName
x  forall (f :: * -> *) a b.
Functor f =>
(a -> b) -> f (a, a) -> f (b, b)
<$$> forall a. SynEq a => a -> a -> SynEqM (a, a)
synEq a
b (forall a. Subst a => Int -> a -> a
raise Int
1 a
b')  -- TODO: mkAbs?
      (NoAbs ArgName
x a
b, Abs   ArgName
x' a
b') -> forall a. ArgName -> a -> Abs a
Abs ArgName
x' forall (f :: * -> *) a b.
Functor f =>
(a -> b) -> f (a, a) -> f (b, b)
<$$> forall a. SynEq a => a -> a -> SynEqM (a, a)
synEq (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') = forall e. ArgInfo -> e -> Arg e
Arg forall (f :: * -> *) a b.
Functor f =>
(a -> b) -> f (a, a) -> f (b, b)
<$$> forall a. SynEq a => a -> a -> SynEqM (a, a)
synEq ArgInfo
ai ArgInfo
ai' forall (f :: * -> *) a b.
Applicative f =>
f (a -> b, a -> b) -> f (a, a) -> f (b, b)
<**> 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 Maybe NamedName
x Bool
f Maybe Term
t a
a) d' :: Dom a
d'@(Dom ArgInfo
ai' Maybe NamedName
x' Bool
f' Maybe Term
_ a
a')
    | Maybe NamedName
x forall a. Eq a => a -> a -> Bool
== Maybe NamedName
x'   = forall t e.
ArgInfo -> Maybe NamedName -> Bool -> Maybe t -> e -> Dom' t e
Dom forall (f :: * -> *) a b.
Functor f =>
(a -> b) -> f (a, a) -> f (b, b)
<$$> forall a. SynEq a => a -> a -> SynEqM (a, a)
synEq ArgInfo
ai ArgInfo
ai' forall (f :: * -> *) a b.
Applicative f =>
f (a -> b, a -> b) -> f (a, a) -> f (b, b)
<**> forall (f :: * -> *) a. Applicative f => a -> f (a, a)
pure2 Maybe NamedName
x forall (f :: * -> *) a b.
Applicative f =>
f (a -> b, a -> b) -> f (a, a) -> f (b, b)
<**> forall a. SynEq a => a -> a -> SynEqM (a, a)
synEq Bool
f Bool
f' forall (f :: * -> *) a b.
Applicative f =>
f (a -> b, a -> b) -> f (a, a) -> f (b, b)
<**> forall (f :: * -> *) a. Applicative f => a -> f (a, a)
pure2 Maybe Term
t forall (f :: * -> *) a b.
Applicative f =>
f (a -> b, a -> b) -> f (a, a) -> f (b, b)
<**> forall a. SynEq a => a -> a -> SynEqM (a, a)
synEq a
a a
a'
    | Bool
otherwise = forall a. a -> SynEqM a
inequal (Dom a
d, Dom a
d')

instance SynEq ArgInfo where
  synEq :: ArgInfo -> ArgInfo -> SynEqM (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 forall a. Eq a => a -> a -> Bool
== Hiding
h', forall a b. (LensModality a, LensModality b) => a -> b -> Bool
sameModality Modality
r Modality
r', Annotation
a forall a. Eq a => a -> a -> Bool
== Annotation
a' = forall (f :: * -> *) a. Applicative f => a -> f (a, a)
pure2 ArgInfo
ai
    | Bool
otherwise        = forall a. a -> SynEqM a
inequal (ArgInfo
ai, ArgInfo
ai')