{-# LANGUAGE DataKinds #-}
{-# LANGUAGE MagicHash #-}
{-# LANGUAGE UnboxedTuples #-}

{-# OPTIONS_GHC -fworker-wrapper-cbv #-}
{-# OPTIONS_GHC -Wunused-imports #-}
-- {-# OPTIONS_GHC -ddump-simpl -dsuppress-all -dno-suppress-type-signatures -ddump-to-file -dno-typeable-binds #-}

-- | 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 Mikan.TypeChecking.SyntacticEquality
  ( checkSyntacticEquality
  , SynEq
  )
  where

import GHC.Exts
  ( Int#, isTrue#
  , oneShot
  , RuntimeRep(..)
  )

import Mikan.Syntax.Common
import Mikan.Syntax.Internal

import Mikan.TypeChecking.Monad.Base (MonadReduce(..), ReduceM(..), ReduceEnv , askR)

import Mikan.TypeChecking.Reduce
import Mikan.TypeChecking.Substitute

import Mikan.Utils.ExpandCase
import Mikan.Utils.Unsafe (unsafeComparePointers)


{-# INLINE checkSyntacticEquality #-}
-- | Syntactic equality check for terms.
--
-- Morally,  'checkSyntacticEquality' behaves as if it were
-- implemented as:
--
-- @
-- checkSyntacticEquality v v' s f = do
--   (v, v') <- instantiateFull (v, v')
--   if v == v' then s v v' else f v v'
-- @
--
-- with the follow caveat:
--
-- * Both @v@ and @v'@ are only guaranteed to fully instantiated to the
--   depth at which they are syntactically equal.
checkSyntacticEquality
  :: (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.
(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
  env <- ReduceM ReduceEnv -> m ReduceEnv
forall a. ReduceM a -> m a
forall (m :: * -> *) a. MonadReduce m => ReduceM a -> m a
liftReduce ReduceM ReduceEnv
askR
  runSynEqA env (synEq u v) s f

--------------------------------------------------------------------------------
-- The syntactic equality applicative

-- | The syntactic equality checking appicative.
newtype SynEqA a =
  -- | Morally, @SynEqA a@ is @StateT Bool ReduceM (a, a)@.
  --
  -- However, if we unfold the latter type using 'Mikan.Utils.StrictState.StateT',
  -- we get
  --
  -- > Bool -> ReduceEnv -> (# (a, a), Bool #)
  --
  -- This type is somewhat suboptimal: both the inner @(a,a)@ tuple and the
  -- 'Bool's are lifted, which adds extra pointer indirections and thunk checks.
  SynEqA# { forall a. SynEqA a -> ReduceEnv -> Int# -> (# a, a, Int# #)
unSynEqA# :: ReduceEnv -> Int# -> (# a, a, Int# #) }

{-# INLINE runSynEqA #-}
-- | Run the syntactic equality checker in a 'ReduceEnv'.
runSynEqA
  :: ReduceEnv
  -> SynEqA a
  -> (a -> a -> r)
  -- ^ Continuation used upon success.
  -> (a -> a -> r)
  -- ^ Continuation used upon failure.
  -> r
runSynEqA :: forall a r.
ReduceEnv -> SynEqA a -> (a -> a -> r) -> (a -> a -> r) -> r
runSynEqA ReduceEnv
env SynEqA a
m a -> a -> r
t a -> a -> r
f =
  let !(# a
a, a
a', Int#
eq #) = SynEqA a -> ReduceEnv -> Int# -> (# a, a, Int# #)
forall a. SynEqA a -> ReduceEnv -> Int# -> (# a, a, Int# #)
unSynEqA# SynEqA a
m ReduceEnv
env Int#
1#
  in if Int# -> Bool
isTrue# Int#
eq then a -> a -> r
t a
a a
a' else a -> a -> r
f a
a a
a'

instance Functor SynEqA where
  {-# INLINE fmap #-}
  fmap :: forall a b. (a -> b) -> SynEqA a -> SynEqA b
fmap a -> b
f SynEqA a
aa = (ReduceEnv -> Int# -> (# b, b, Int# #)) -> SynEqA b
forall a. (ReduceEnv -> Int# -> (# a, a, Int# #)) -> SynEqA a
SynEqA# ((ReduceEnv -> Int# -> (# b, b, Int# #)) -> SynEqA b)
-> (ReduceEnv -> Int# -> (# b, b, Int# #)) -> SynEqA b
forall a b. (a -> b) -> a -> b
$ (ReduceEnv -> Int# -> (# b, b, Int# #))
-> ReduceEnv -> Int# -> (# b, b, Int# #)
forall a b. (a -> b) -> a -> b
oneShot \ReduceEnv
env Int#
eq ->
    let
      !(# a
a, a
a', Int#
eqa #) = SynEqA a -> ReduceEnv -> Int# -> (# a, a, Int# #)
forall a. SynEqA a -> ReduceEnv -> Int# -> (# a, a, Int# #)
unSynEqA# SynEqA a
aa ReduceEnv
env Int#
eq
      b :: b
b = a -> b
f a
a
      b' :: b
b' = a -> b
f a
a'
    -- Using a bang patterns here makes GHC force b' before
    -- b, which can re-order exceptions thrown by the conversion
    -- checker.
    in b
b b -> (# b, b, Int# #) -> (# b, b, Int# #)
forall a b. a -> b -> b
`seq` b
b' b -> (# b, b, Int# #) -> (# b, b, Int# #)
forall a b. a -> b -> b
`seq` (# b
b, b
b', Int#
eqa #)

instance Applicative SynEqA where
  {-# INLINE pure #-}
  pure :: forall a. a -> SynEqA a
pure = \a
a -> (ReduceEnv -> Int# -> (# a, a, Int# #)) -> SynEqA a
forall a. (ReduceEnv -> Int# -> (# a, a, Int# #)) -> SynEqA a
SynEqA# ((ReduceEnv -> Int# -> (# a, a, Int# #)) -> SynEqA a)
-> (ReduceEnv -> Int# -> (# a, a, Int# #)) -> SynEqA a
forall a b. (a -> b) -> a -> b
$ (ReduceEnv -> Int# -> (# a, a, Int# #))
-> ReduceEnv -> Int# -> (# a, a, Int# #)
forall a b. (a -> b) -> a -> b
oneShot \ReduceEnv
env Int#
eq -> (# a
a, a
a, Int#
eq #)

  {-# INLINE (<*>) #-}
  SynEqA (a -> b)
ff <*> :: forall a b. SynEqA (a -> b) -> SynEqA a -> SynEqA b
<*> SynEqA a
aa = (ReduceEnv -> Int# -> (# b, b, Int# #)) -> SynEqA b
forall a. (ReduceEnv -> Int# -> (# a, a, Int# #)) -> SynEqA a
SynEqA# ((ReduceEnv -> Int# -> (# b, b, Int# #)) -> SynEqA b)
-> (ReduceEnv -> Int# -> (# b, b, Int# #)) -> SynEqA b
forall a b. (a -> b) -> a -> b
$ (ReduceEnv -> Int# -> (# b, b, Int# #))
-> ReduceEnv -> Int# -> (# b, b, Int# #)
forall a b. (a -> b) -> a -> b
oneShot \ReduceEnv
env Int#
eq ->
    let
      !(# a -> b
f, a -> b
f', Int#
eqf #) = SynEqA (a -> b) -> ReduceEnv -> Int# -> (# a -> b, a -> b, Int# #)
forall a. SynEqA a -> ReduceEnv -> Int# -> (# a, a, Int# #)
unSynEqA# SynEqA (a -> b)
ff ReduceEnv
env Int#
eq
      !(# a
a, a
a', Int#
eqa #) = SynEqA a -> ReduceEnv -> Int# -> (# a, a, Int# #)
forall a. SynEqA a -> ReduceEnv -> Int# -> (# a, a, Int# #)
unSynEqA# SynEqA a
aa ReduceEnv
env Int#
eqf
      b :: b
b = a -> b
f a
a
      b' :: b
b' = a -> b
f' a
a'
    in b
b b -> (# b, b, Int# #) -> (# b, b, Int# #)
forall a b. a -> b -> b
`seq` b
b' b -> (# b, b, Int# #) -> (# b, b, Int# #)
forall a b. a -> b -> b
`seq` (# b
b, b
b', Int#
eqa #)

instance ExpandCase ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA a) where
  type Result ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA a) = (# a, a, Int# #)

  {-# INLINE expand #-}
  expand :: ((SynEqA a
  -> Result ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA a))
 -> Result ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA a))
-> SynEqA a
expand (SynEqA a
 -> Result ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA a))
-> Result ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA a)
k = (ReduceEnv -> Int# -> (# a, a, Int# #)) -> SynEqA a
forall a. (ReduceEnv -> Int# -> (# a, a, Int# #)) -> SynEqA a
SynEqA# ((ReduceEnv -> Int# -> (# a, a, Int# #)) -> SynEqA a)
-> (ReduceEnv -> Int# -> (# a, a, Int# #)) -> SynEqA a
forall a b. (a -> b) -> a -> b
$ (ReduceEnv -> Int# -> (# a, a, Int# #))
-> ReduceEnv -> Int# -> (# a, a, Int# #)
forall a b. (a -> b) -> a -> b
oneShot \ReduceEnv
env Int#
eq -> (SynEqA a
 -> Result ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA a))
-> Result ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA a)
k ((SynEqA a -> (# a, a, Int# #)) -> SynEqA a -> (# a, a, Int# #)
forall a b. (a -> b) -> a -> b
oneShot \SynEqA a
act -> SynEqA a -> ReduceEnv -> Int# -> (# a, a, Int# #)
forall a. SynEqA a -> ReduceEnv -> Int# -> (# a, a, Int# #)
unSynEqA# SynEqA a
act ReduceEnv
env Int#
eq)

{-# INLINE inequal #-}
-- | Return, flagging inequalty.
inequal :: a -> a -> SynEqA a
inequal :: forall a. a -> a -> SynEqA a
inequal a
x a
y = (ReduceEnv -> Int# -> (# a, a, Int# #)) -> SynEqA a
forall a. (ReduceEnv -> Int# -> (# a, a, Int# #)) -> SynEqA a
SynEqA# ((ReduceEnv -> Int# -> (# a, a, Int# #)) -> SynEqA a)
-> (ReduceEnv -> Int# -> (# a, a, Int# #)) -> SynEqA a
forall a b. (a -> b) -> a -> b
$ (ReduceEnv -> Int# -> (# a, a, Int# #))
-> ReduceEnv -> Int# -> (# a, a, Int# #)
forall a b. (a -> b) -> a -> b
oneShot \ReduceEnv
env Int#
_ -> (# a
x, a
y, Int#
0# #)

{-# INLINE equal #-}
-- | Return, preserving the equality flag.
equal :: a -> a -> SynEqA a
equal :: forall a. a -> a -> SynEqA a
equal a
x a
y = (ReduceEnv -> Int# -> (# a, a, Int# #)) -> SynEqA a
forall a. (ReduceEnv -> Int# -> (# a, a, Int# #)) -> SynEqA a
SynEqA# ((ReduceEnv -> Int# -> (# a, a, Int# #)) -> SynEqA a)
-> (ReduceEnv -> Int# -> (# a, a, Int# #)) -> SynEqA a
forall a b. (a -> b) -> a -> b
$ (ReduceEnv -> Int# -> (# a, a, Int# #))
-> ReduceEnv -> Int# -> (# a, a, Int# #)
forall a b. (a -> b) -> a -> b
oneShot \ReduceEnv
env Int#
eq -> (# a
x, a
y, Int#
eq #)

{-# INLINE synInstantiate #-}
-- | Instantiate a pair of arguments, and invoke the continuation.
synInstantiate :: (Instantiate a) => a -> a -> (a -> a -> SynEqA b) -> SynEqA b
synInstantiate :: forall a b.
Instantiate a =>
a -> a -> (a -> a -> SynEqA b) -> SynEqA b
synInstantiate a
a a
a' a -> a -> SynEqA b
k = (ReduceEnv -> Int# -> (# b, b, Int# #)) -> SynEqA b
forall a. (ReduceEnv -> Int# -> (# a, a, Int# #)) -> SynEqA a
SynEqA# ((ReduceEnv -> Int# -> (# b, b, Int# #)) -> SynEqA b)
-> (ReduceEnv -> Int# -> (# b, b, Int# #)) -> SynEqA b
forall a b. (a -> b) -> a -> b
$ (ReduceEnv -> Int# -> (# b, b, Int# #))
-> ReduceEnv -> Int# -> (# b, b, Int# #)
forall a b. (a -> b) -> a -> b
oneShot \ReduceEnv
env Int#
eq ->
  let
    v :: a
v = ReduceM a -> ReduceEnv -> a
forall a. ReduceM a -> ReduceEnv -> a
unReduceM (a -> ReduceM a
forall t. Instantiate t => t -> ReduceM t
instantiate' a
a) ReduceEnv
env
    v' :: a
v' = ReduceM a -> ReduceEnv -> a
forall a. ReduceM a -> ReduceEnv -> a
unReduceM (a -> ReduceM a
forall t. Instantiate t => t -> ReduceM t
instantiate' a
a') ReduceEnv
env
  in a
v a -> (# b, b, Int# #) -> (# b, b, Int# #)
forall a b. a -> b -> b
`seq` a
v' a -> (# b, b, Int# #) -> (# b, b, Int# #)
forall a b. a -> b -> b
`seq` (SynEqA b -> ReduceEnv -> Int# -> (# b, b, Int# #)
forall a. SynEqA a -> ReduceEnv -> Int# -> (# a, a, Int# #)
unSynEqA# (a -> a -> SynEqA b
k a
v a
v') ReduceEnv
env Int#
eq)

--------------------------------------------------------------------------------
-- SynEq instances

-- | A type is 'SynEq' if it can be checked for syntactic equality.
class SynEq a where
  -- | Unconditionally equate and instantiate one layer.
  synEq :: a -> a -> SynEqA a

{-# INLINE synEq' #-}
-- | Only equate and instantiate if the rest of the structure seen so far is syntactically equal.
synEq' :: (SynEq a) => a -> a -> SynEqA a
synEq' :: forall a. SynEq a => a -> a -> SynEqA a
synEq' a
a a
a' = (ReduceEnv -> Int# -> (# a, a, Int# #)) -> SynEqA a
forall a. (ReduceEnv -> Int# -> (# a, a, Int# #)) -> SynEqA a
SynEqA# ((ReduceEnv -> Int# -> (# a, a, Int# #)) -> SynEqA a)
-> (ReduceEnv -> Int# -> (# a, a, Int# #)) -> SynEqA a
forall a b. (a -> b) -> a -> b
$ (ReduceEnv -> Int# -> (# a, a, Int# #))
-> ReduceEnv -> Int# -> (# a, a, Int# #)
forall a b. (a -> b) -> a -> b
oneShot \ReduceEnv
env Int#
eq ->
  -- Re-using 'eq' on both branches makes GHC much more willing to make join points.
  if Int# -> Bool
isTrue# Int#
eq then
    SynEqA a -> ReduceEnv -> Int# -> (# a, a, Int# #)
forall a. SynEqA a -> ReduceEnv -> Int# -> (# a, a, Int# #)
unSynEqA# (a -> a -> SynEqA a
forall a. SynEq a => a -> a -> SynEqA a
synEq a
a a
a') ReduceEnv
env Int#
eq
  else
    (# a
a, a
a', Int#
eq #)

instance SynEq Bool where
  synEq :: Bool -> Bool -> SynEqA Bool
synEq Bool
x Bool
y = ((SynEqA Bool
  -> Result
       ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA Bool))
 -> Result
      ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA Bool))
-> SynEqA Bool
forall a.
ExpandCase LiftedRep a =>
((a -> Result LiftedRep a) -> Result LiftedRep a) -> a
expand \SynEqA Bool
-> Result
     ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA Bool)
ret ->
    if Bool
x Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool
y then
      SynEqA Bool
-> Result
     ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA Bool)
ret (SynEqA Bool
 -> Result
      ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA Bool))
-> SynEqA Bool
-> Result
     ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA Bool)
forall a b. (a -> b) -> a -> b
$ Bool -> Bool -> SynEqA Bool
forall a. a -> a -> SynEqA a
equal Bool
x Bool
y
    else
      SynEqA Bool
-> Result
     ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA Bool)
ret (SynEqA Bool
 -> Result
      ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA Bool))
-> SynEqA Bool
-> Result
     ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA Bool)
forall a b. (a -> b) -> a -> b
$ Bool -> Bool -> SynEqA Bool
forall a. a -> a -> SynEqA a
inequal Bool
x Bool
y

instance SynEq Term where
  synEq :: Term -> Term -> SynEqA Term
synEq Term
v Term
v' = ((SynEqA Term
  -> Result
       ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA Term))
 -> Result
      ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA Term))
-> SynEqA Term
forall a.
ExpandCase LiftedRep a =>
((a -> Result LiftedRep a) -> Result LiftedRep a) -> a
expand \SynEqA Term
-> Result
     ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA Term)
ret ->
    if Term -> Term -> Bool
forall a. a -> a -> Bool
unsafeComparePointers Term
v Term
v' then
      SynEqA Term
-> Result
     ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA Term)
ret (SynEqA Term
 -> Result
      ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA Term))
-> SynEqA Term
-> Result
     ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA Term)
forall a b. (a -> b) -> a -> b
$ Term -> Term -> SynEqA Term
forall a. a -> a -> SynEqA a
equal Term
v Term
v'
    else SynEqA Term
-> Result
     ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA Term)
ret (SynEqA Term
 -> Result
      ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA Term))
-> SynEqA Term
-> Result
     ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA Term)
forall a b. (a -> b) -> a -> b
$ Term -> Term -> (Term -> Term -> SynEqA Term) -> SynEqA Term
forall a b.
Instantiate a =>
a -> a -> (a -> a -> SynEqA b) -> SynEqA b
synInstantiate Term
v Term
v' \Term
v Term
v' -> ((SynEqA Term
  -> Result
       ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA Term))
 -> Result
      ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA Term))
-> SynEqA Term
forall a.
ExpandCase LiftedRep a =>
((a -> Result LiftedRep a) -> Result LiftedRep a) -> a
expand \SynEqA Term
-> Result
     ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA Term)
ret -> case (Term
v, Term
v') of
      -- Avoid hitting the global shared variable cache:  if the two neutrals are could be shared
      -- via the cache (i.e: they are smaller than 'varTableSize' and have no spines)
      -- then the previous 'unsafeComparePointers' check will succeed, as they should
      -- have originated from the table to begin with!
      (Var   Int
i Elims
vs, Var   Int
i' Elims
vs')  | Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
i' -> SynEqA Term
-> Result
     ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA Term)
ret (SynEqA Term
 -> Result
      ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA Term))
-> SynEqA Term
-> Result
     ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA Term)
forall a b. (a -> b) -> a -> b
$ Int -> Elims -> Term
unsharedVar Int
i (Elims -> Term) -> SynEqA Elims -> SynEqA Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Elims -> Elims -> SynEqA Elims
forall a. SynEq a => a -> a -> SynEqA 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' -> SynEqA Term
-> Result
     ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA Term)
ret (SynEqA Term
 -> Result
      ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA Term))
-> SynEqA Term
-> Result
     ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA Term)
forall a b. (a -> b) -> a -> b
$ ConHead -> ConInfo -> Elims -> Term
Con ConHead
c (ConInfo -> ConInfo -> ConInfo
bestConInfo ConInfo
i ConInfo
i') (Elims -> Term) -> SynEqA Elims -> SynEqA Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Elims -> Elims -> SynEqA Elims
forall a. SynEq a => a -> a -> SynEqA 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' -> SynEqA Term
-> Result
     ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA Term)
ret (SynEqA Term
 -> Result
      ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA Term))
-> SynEqA Term
-> Result
     ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA Term)
forall a b. (a -> b) -> a -> b
$ QName -> Elims -> Term
Def QName
f (Elims -> Term) -> SynEqA Elims -> SynEqA Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Elims -> Elims -> SynEqA Elims
forall a. SynEq a => a -> a -> SynEqA 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' -> SynEqA Term
-> Result
     ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA Term)
ret (SynEqA Term
 -> Result
      ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA Term))
-> SynEqA Term
-> Result
     ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA Term)
forall a b. (a -> b) -> a -> b
$ MetaId -> Elims -> Term
MetaV MetaId
x (Elims -> Term) -> SynEqA Elims -> SynEqA Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Elims -> Elims -> SynEqA Elims
forall a. SynEq a => a -> a -> SynEqA 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' -> SynEqA Term
-> Result
     ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA Term)
ret (SynEqA Term
 -> Result
      ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA Term))
-> SynEqA Term
-> Result
     ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA Term)
forall a b. (a -> b) -> a -> b
$ Term -> SynEqA Term
forall a. a -> SynEqA a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term -> SynEqA Term) -> Term -> SynEqA Term
forall a b. (a -> b) -> a -> b
$ Term
v
      (Lam   ArgInfo
h Abs Term
b , Lam   ArgInfo
h' Abs Term
b' )            -> SynEqA Term
-> Result
     ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA Term)
ret (SynEqA Term
 -> Result
      ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA Term))
-> SynEqA Term
-> Result
     ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA Term)
forall a b. (a -> b) -> a -> b
$ ArgInfo -> Abs Term -> Term
Lam (ArgInfo -> Abs Term -> Term)
-> SynEqA ArgInfo -> SynEqA (Abs Term -> Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ArgInfo -> ArgInfo -> SynEqA ArgInfo
forall a. SynEq a => a -> a -> SynEqA a
synEq ArgInfo
h ArgInfo
h' SynEqA (Abs Term -> Term) -> SynEqA (Abs Term) -> SynEqA Term
forall a b. SynEqA (a -> b) -> SynEqA a -> SynEqA b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Abs Term -> Abs Term -> SynEqA (Abs Term)
forall a. SynEq a => a -> a -> SynEqA a
synEq' Abs Term
b Abs Term
b'
      (Level Level
l   , Level Level
l'    )            -> SynEqA Term
-> Result
     ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA Term)
ret (SynEqA Term
 -> Result
      ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA Term))
-> SynEqA Term
-> Result
     ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA Term)
forall a b. (a -> b) -> a -> b
$ Level -> Term
levelTm (Level -> Term) -> SynEqA Level -> SynEqA Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Level -> Level -> SynEqA Level
forall a. SynEq a => a -> a -> SynEqA a
synEq Level
l Level
l'
      (Sort  Sort
s   , Sort  Sort
s'    )            -> SynEqA Term
-> Result
     ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA Term)
ret (SynEqA Term
 -> Result
      ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA Term))
-> SynEqA Term
-> Result
     ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA Term)
forall a b. (a -> b) -> a -> b
$ Sort -> Term
Sort (Sort -> Term) -> SynEqA Sort -> SynEqA Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Sort -> Sort -> SynEqA Sort
forall a. SynEq a => a -> a -> SynEqA a
synEq Sort
s Sort
s'
      (Pi    Dom Type
a Abs Type
b , Pi    Dom Type
a' Abs Type
b' )            -> SynEqA Term
-> Result
     ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA Term)
ret (SynEqA Term
 -> Result
      ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA Term))
-> SynEqA Term
-> Result
     ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA Term)
forall a b. (a -> b) -> a -> b
$ Dom Type -> Abs Type -> Term
Pi (Dom Type -> Abs Type -> Term)
-> SynEqA (Dom Type) -> SynEqA (Abs Type -> Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Dom Type -> Dom Type -> SynEqA (Dom Type)
forall a. SynEq a => a -> a -> SynEqA a
synEq Dom Type
a Dom Type
a' SynEqA (Abs Type -> Term) -> SynEqA (Abs Type) -> SynEqA Term
forall a b. SynEqA (a -> b) -> SynEqA a -> SynEqA b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Abs Type -> Abs Type -> SynEqA (Abs Type)
forall a. SynEq a => a -> a -> SynEqA a
synEq' Abs Type
b Abs Type
b'
      -- 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.
      (DontCare Term
u, DontCare Term
u' )            -> SynEqA Term
-> Result
     ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA Term)
ret (SynEqA Term
 -> Result
      ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA Term))
-> SynEqA Term
-> Result
     ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA Term)
forall a b. (a -> b) -> a -> b
$ Term -> Term
DontCare (Term -> Term) -> SynEqA Term -> SynEqA Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> Term -> SynEqA Term
forall a. SynEq a => a -> a -> SynEqA a
synEq Term
u Term
u'
      (Dummy{}   , Dummy{}     )            -> SynEqA Term
-> Result
     ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA Term)
ret (SynEqA Term
 -> Result
      ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA Term))
-> SynEqA Term
-> Result
     ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA Term)
forall a b. (a -> b) -> a -> b
$ Term -> Term -> SynEqA Term
forall a. a -> a -> SynEqA a
equal Term
v Term
v'
      (Term, Term)
_                                     -> SynEqA Term
-> Result
     ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA Term)
ret (SynEqA Term
 -> Result
      ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA Term))
-> SynEqA Term
-> Result
     ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA Term)
forall a b. (a -> b) -> a -> b
$ Term -> Term -> SynEqA Term
forall a. a -> a -> SynEqA a
inequal Term
v Term
v'

-- | Returns levels in canonical form.
instance SynEq Level where
  synEq :: Level -> Level -> SynEqA Level
synEq Level
l Level
l' = ((SynEqA Level
  -> Result
       ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA Level))
 -> Result
      ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA Level))
-> SynEqA Level
forall a.
ExpandCase LiftedRep a =>
((a -> Result LiftedRep a) -> Result LiftedRep a) -> a
expand \SynEqA Level
-> Result
     ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA Level)
ret -> case (Level
l, Level
l') of
    (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'   -> SynEqA Level
-> Result
     ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA Level)
ret (SynEqA Level
 -> Result
      ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA Level))
-> SynEqA Level
-> Result
     ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA Level)
forall a b. (a -> b) -> a -> b
$ Integer -> [PlusLevel] -> Level
levelMax Integer
n ([PlusLevel] -> Level) -> SynEqA [PlusLevel] -> SynEqA Level
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [PlusLevel] -> [PlusLevel] -> SynEqA [PlusLevel]
forall a. SynEq a => a -> a -> SynEqA a
synEq [PlusLevel]
vs [PlusLevel]
vs'
      | Bool
otherwise -> SynEqA Level
-> Result
     ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA Level)
ret (SynEqA Level
 -> Result
      ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA Level))
-> SynEqA Level
-> Result
     ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA Level)
forall a b. (a -> b) -> a -> b
$ Level -> Level -> SynEqA Level
forall a. a -> a -> SynEqA a
inequal Level
l Level
l'

instance SynEq PlusLevel where
  synEq :: PlusLevel -> PlusLevel -> SynEqA PlusLevel
synEq PlusLevel
l PlusLevel
l' = ((SynEqA PlusLevel
  -> Result
       ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA PlusLevel))
 -> Result
      ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA PlusLevel))
-> SynEqA PlusLevel
forall a.
ExpandCase LiftedRep a =>
((a -> Result LiftedRep a) -> Result LiftedRep a) -> a
expand \SynEqA PlusLevel
-> Result
     ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA PlusLevel)
ret -> case (PlusLevel
l, PlusLevel
l') of
    (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'   -> SynEqA PlusLevel
-> Result
     ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA PlusLevel)
ret (SynEqA PlusLevel
 -> Result
      ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA PlusLevel))
-> SynEqA PlusLevel
-> Result
     ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA PlusLevel)
forall a b. (a -> b) -> a -> b
$ Integer -> Term -> PlusLevel
forall t. Integer -> t -> PlusLevel' t
Plus Integer
n (Term -> PlusLevel) -> SynEqA Term -> SynEqA PlusLevel
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> Term -> SynEqA Term
forall a. SynEq a => a -> a -> SynEqA a
synEq Term
v Term
v'
      | Bool
otherwise -> SynEqA PlusLevel
-> Result
     ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA PlusLevel)
ret (SynEqA PlusLevel
 -> Result
      ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA PlusLevel))
-> SynEqA PlusLevel
-> Result
     ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA PlusLevel)
forall a b. (a -> b) -> a -> b
$ PlusLevel -> PlusLevel -> SynEqA PlusLevel
forall a. a -> a -> SynEqA a
inequal PlusLevel
l PlusLevel
l'

instance SynEq Sort where
  synEq :: Sort -> Sort -> SynEqA Sort
synEq Sort
s Sort
s' = ((SynEqA Sort
  -> Result
       ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA Sort))
 -> Result
      ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA Sort))
-> SynEqA Sort
forall a.
ExpandCase LiftedRep a =>
((a -> Result LiftedRep a) -> Result LiftedRep a) -> a
expand \SynEqA Sort
-> Result
     ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA Sort)
ret ->
    if Sort -> Sort -> Bool
forall a. a -> a -> Bool
unsafeComparePointers Sort
s Sort
s' then
      SynEqA Sort
-> Result
     ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA Sort)
ret (SynEqA Sort
 -> Result
      ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA Sort))
-> SynEqA Sort
-> Result
     ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA Sort)
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> SynEqA Sort
forall a. a -> a -> SynEqA a
equal Sort
s Sort
s'
    else SynEqA Sort
-> Result
     ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA Sort)
ret (SynEqA Sort
 -> Result
      ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA Sort))
-> SynEqA Sort
-> Result
     ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA Sort)
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> (Sort -> Sort -> SynEqA Sort) -> SynEqA Sort
forall a b.
Instantiate a =>
a -> a -> (a -> a -> SynEqA b) -> SynEqA b
synInstantiate Sort
s Sort
s' \Sort
s Sort
s' -> ((SynEqA Sort
  -> Result
       ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA Sort))
 -> Result
      ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA Sort))
-> SynEqA Sort
forall a.
ExpandCase LiftedRep a =>
((a -> Result LiftedRep a) -> Result LiftedRep a) -> a
expand \SynEqA Sort
-> Result
     ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA Sort)
ret -> case (Sort
s, Sort
s') of
      (Univ Univ
u Level
l, Univ Univ
u' Level
l')      | Univ
u Univ -> Univ -> Bool
forall a. Eq a => a -> a -> Bool
== Univ
u'         -> SynEqA Sort
-> Result
     ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA Sort)
ret (SynEqA Sort
 -> Result
      ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA Sort))
-> SynEqA Sort
-> Result
     ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA Sort)
forall a b. (a -> b) -> a -> b
$ Univ -> Level -> Sort
forall t. Univ -> Level' t -> Sort' t
Univ Univ
u (Level -> Sort) -> SynEqA Level -> SynEqA Sort
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Level -> Level -> SynEqA Level
forall a. SynEq a => a -> a -> SynEqA 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')               -> SynEqA Sort
-> Result
     ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA Sort)
ret (SynEqA Sort
 -> Result
      ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA Sort))
-> SynEqA Sort
-> Result
     ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA Sort)
forall a b. (a -> b) -> a -> b
$ Dom' Term Term -> Sort -> Abs Sort -> Sort
forall t. Dom' t t -> Sort' t -> Abs (Sort' t) -> Sort' t
PiSort (Dom' Term Term -> Sort -> Abs Sort -> Sort)
-> SynEqA (Dom' Term Term) -> SynEqA (Sort -> Abs Sort -> Sort)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Dom' Term Term -> Dom' Term Term -> SynEqA (Dom' Term Term)
forall a. SynEq a => a -> a -> SynEqA a
synEq Dom' Term Term
a Dom' Term Term
a' SynEqA (Sort -> Abs Sort -> Sort)
-> SynEqA Sort -> SynEqA (Abs Sort -> Sort)
forall a b. SynEqA (a -> b) -> SynEqA a -> SynEqA b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Sort -> Sort -> SynEqA Sort
forall a. SynEq a => a -> a -> SynEqA a
synEq' Sort
b Sort
b' SynEqA (Abs Sort -> Sort) -> SynEqA (Abs Sort) -> SynEqA Sort
forall a b. SynEqA (a -> b) -> SynEqA a -> SynEqA b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Abs Sort -> Abs Sort -> SynEqA (Abs Sort)
forall a. SynEq a => a -> a -> SynEqA a
synEq' Abs Sort
c Abs Sort
c'
      (FunSort Sort
a Sort
b, FunSort Sort
a' Sort
b')                  -> SynEqA Sort
-> Result
     ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA Sort)
ret (SynEqA Sort
 -> Result
      ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA Sort))
-> SynEqA Sort
-> Result
     ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA Sort)
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
forall t. Sort' t -> Sort' t -> Sort' t
FunSort (Sort -> Sort -> Sort) -> SynEqA Sort -> SynEqA (Sort -> Sort)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Sort -> Sort -> SynEqA Sort
forall a. SynEq a => a -> a -> SynEqA a
synEq Sort
a Sort
a' SynEqA (Sort -> Sort) -> SynEqA Sort -> SynEqA Sort
forall a b. SynEqA (a -> b) -> SynEqA a -> SynEqA b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Sort -> Sort -> SynEqA Sort
forall a. SynEq a => a -> a -> SynEqA a
synEq' Sort
b Sort
b'
      (UnivSort Sort
a, UnivSort Sort
a')                     -> SynEqA Sort
-> Result
     ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA Sort)
ret (SynEqA Sort
 -> Result
      ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA Sort))
-> SynEqA Sort
-> Result
     ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA Sort)
forall a b. (a -> b) -> a -> b
$ Sort -> Sort
forall t. Sort' t -> Sort' t
UnivSort (Sort -> Sort) -> SynEqA Sort -> SynEqA Sort
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Sort -> Sort -> SynEqA Sort
forall a. SynEq a => a -> a -> SynEqA a
synEq Sort
a Sort
a'
      (Sort
LevelUniv, Sort
LevelUniv  )                      -> SynEqA Sort
-> Result
     ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA Sort)
ret (SynEqA Sort
 -> Result
      ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA Sort))
-> SynEqA Sort
-> Result
     ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA Sort)
forall a b. (a -> b) -> a -> b
$ Sort -> SynEqA Sort
forall a. a -> SynEqA a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Sort
s
      (Sort
IntervalUniv, Sort
IntervalUniv)                  -> SynEqA Sort
-> Result
     ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA Sort)
ret (SynEqA Sort
 -> Result
      ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA Sort))
-> SynEqA Sort
-> Result
     ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA Sort)
forall a b. (a -> b) -> a -> b
$ Sort -> SynEqA Sort
forall a. a -> SynEqA a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Sort
s
      (Sort
CofUniv, Sort
CofUniv)                            -> SynEqA Sort
-> Result
     ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA Sort)
ret (SynEqA Sort
 -> Result
      ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA Sort))
-> SynEqA Sort
-> Result
     ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA Sort)
forall a b. (a -> b) -> a -> b
$ Sort -> SynEqA Sort
forall a. a -> SynEqA a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Sort
s
      (Inf Univ
u Integer
m , Inf Univ
u' Integer
n)        | Univ
u Univ -> Univ -> Bool
forall a. Eq a => a -> a -> Bool
== Univ
u', Integer
m Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
n -> SynEqA Sort
-> Result
     ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA Sort)
ret (SynEqA Sort
 -> Result
      ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA Sort))
-> SynEqA Sort
-> Result
     ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA Sort)
forall a b. (a -> b) -> a -> b
$ Sort -> SynEqA Sort
forall a. a -> SynEqA a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Sort
s
      (MetaS MetaId
x Elims
es , MetaS MetaId
x' Elims
es') | MetaId
x MetaId -> MetaId -> Bool
forall a. Eq a => a -> a -> Bool
== MetaId
x'         -> SynEqA Sort
-> Result
     ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA Sort)
ret (SynEqA Sort
 -> Result
      ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA Sort))
-> SynEqA Sort
-> Result
     ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA Sort)
forall a b. (a -> b) -> a -> b
$ MetaId -> Elims -> Sort
forall t. MetaId -> [Elim' t] -> Sort' t
MetaS MetaId
x (Elims -> Sort) -> SynEqA Elims -> SynEqA Sort
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Elims -> Elims -> SynEqA Elims
forall a. SynEq a => a -> a -> SynEqA 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'         -> SynEqA Sort
-> Result
     ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA Sort)
ret (SynEqA Sort
 -> Result
      ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA Sort))
-> SynEqA Sort
-> Result
     ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA Sort)
forall a b. (a -> b) -> a -> b
$ QName -> Elims -> Sort
forall t. QName -> [Elim' t] -> Sort' t
DefS QName
d  (Elims -> Sort) -> SynEqA Elims -> SynEqA Sort
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Elims -> Elims -> SynEqA Elims
forall a. SynEq a => a -> a -> SynEqA a
synEq Elims
es Elims
es'
      (DummyS{}, DummyS{})                          -> SynEqA Sort
-> Result
     ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA Sort)
ret (SynEqA Sort
 -> Result
      ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA Sort))
-> SynEqA Sort
-> Result
     ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA Sort)
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> SynEqA Sort
forall a. a -> a -> SynEqA a
equal Sort
s Sort
s'
      (Sort, Sort)
_                                             -> SynEqA Sort
-> Result
     ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA Sort)
ret (SynEqA Sort
 -> Result
      ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA Sort))
-> SynEqA Sort
-> Result
     ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA Sort)
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> SynEqA Sort
forall a. a -> a -> SynEqA a
inequal Sort
s Sort
s'

-- | Syntactic equality ignores sorts.
instance SynEq Type where
  synEq :: Type -> Type -> SynEqA Type
synEq Type
x Type
y = ((SynEqA Type
  -> Result
       ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA Type))
 -> Result
      ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA Type))
-> SynEqA Type
forall a.
ExpandCase LiftedRep a =>
((a -> Result LiftedRep a) -> Result LiftedRep a) -> a
expand \SynEqA Type
-> Result
     ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA Type)
ret -> case (Type
x, Type
y) of
    (El Sort
s Term
t, El Sort
s' Term
t') -> SynEqA Type
-> Result
     ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA Type)
ret (SynEqA Type
 -> Result
      ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA Type))
-> SynEqA Type
-> Result
     ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA Type)
forall a b. (a -> b) -> a -> b
$ (Term -> Type) -> (Term -> Type) -> SynEqA (Term -> Type)
forall a. a -> a -> SynEqA a
equal (Sort -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El Sort
s) (Sort -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El Sort
s') SynEqA (Term -> Type) -> SynEqA Term -> SynEqA Type
forall a b. SynEqA (a -> b) -> SynEqA a -> SynEqA b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term -> Term -> SynEqA Term
forall a. SynEq a => a -> a -> SynEqA a
synEq Term
t Term
t'

instance SynEq a => SynEq [a] where
  {-# SPECIALIZE instance SynEq Elims #-}
  {-# SPECIALIZE instance SynEq [PlusLevel] #-}
  synEq :: [a] -> [a] -> SynEqA [a]
synEq [a]
as [a]
as' = ((SynEqA [a]
  -> Result
       ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA [a]))
 -> Result
      ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA [a]))
-> SynEqA [a]
forall a.
ExpandCase LiftedRep a =>
((a -> Result LiftedRep a) -> Result LiftedRep a) -> a
expand \SynEqA [a]
-> Result ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA [a])
ret -> case ([a]
as, [a]
as') of
    ([], [])       -> SynEqA [a]
-> Result ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA [a])
ret (SynEqA [a]
 -> Result
      ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA [a]))
-> SynEqA [a]
-> Result ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA [a])
forall a b. (a -> b) -> a -> b
$ [a] -> SynEqA [a]
forall a. a -> SynEqA a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
    (a
a:[a]
as, a
a':[a]
as') -> SynEqA [a]
-> Result ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA [a])
ret (SynEqA [a]
 -> Result
      ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA [a]))
-> SynEqA [a]
-> Result ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA [a])
forall a b. (a -> b) -> a -> b
$ (:) (a -> [a] -> [a]) -> SynEqA a -> SynEqA ([a] -> [a])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> a -> SynEqA a
forall a. SynEq a => a -> a -> SynEqA a
synEq' a
a a
a' SynEqA ([a] -> [a]) -> SynEqA [a] -> SynEqA [a]
forall a b. SynEqA (a -> b) -> SynEqA a -> SynEqA b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [a] -> [a] -> SynEqA [a]
forall a. SynEq a => a -> a -> SynEqA a
synEq [a]
as [a]
as'
    ([a]
as, [a]
as')      -> SynEqA [a]
-> Result ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA [a])
ret (SynEqA [a]
 -> Result
      ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA [a]))
-> SynEqA [a]
-> Result ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA [a])
forall a b. (a -> b) -> a -> b
$ [a] -> [a] -> SynEqA [a]
forall a. a -> a -> SynEqA a
inequal [a]
as [a]
as'

instance SynEq a => SynEq (Elim' a) where
  synEq :: Elim' a -> Elim' a -> SynEqA (Elim' a)
synEq Elim' a
e Elim' a
e' = ((SynEqA (Elim' a)
  -> Result
       ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA (Elim' a)))
 -> Result
      ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA (Elim' a)))
-> SynEqA (Elim' a)
forall a.
ExpandCase LiftedRep a =>
((a -> Result LiftedRep a) -> Result LiftedRep a) -> a
expand \SynEqA (Elim' a)
-> Result
     ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA (Elim' a))
ret ->
    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' -> SynEqA (Elim' a)
-> Result
     ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA (Elim' a))
ret (SynEqA (Elim' a)
 -> Result
      ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA (Elim' a)))
-> SynEqA (Elim' a)
-> Result
     ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA (Elim' a))
forall a b. (a -> b) -> a -> b
$ Elim' a -> SynEqA (Elim' a)
forall a. a -> SynEqA a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Elim' a
e
      (Apply Arg a
a, Apply Arg a
a') -> SynEqA (Elim' a)
-> Result
     ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA (Elim' a))
ret (SynEqA (Elim' a)
 -> Result
      ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA (Elim' a)))
-> SynEqA (Elim' a)
-> Result
     ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA (Elim' a))
forall a b. (a -> b) -> a -> b
$ Arg a -> Elim' a
forall a. Arg a -> Elim' a
Apply (Arg a -> Elim' a) -> SynEqA (Arg a) -> SynEqA (Elim' a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Arg a -> Arg a -> SynEqA (Arg a)
forall a. SynEq a => a -> a -> SynEqA a
synEq Arg a
a Arg a
a'
      (IApply a
u a
v a
r, IApply a
u' a
v' a
r')
                          -> SynEqA (Elim' a)
-> Result
     ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA (Elim' a))
ret (SynEqA (Elim' a)
 -> Result
      ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA (Elim' a)))
-> SynEqA (Elim' a)
-> Result
     ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA (Elim' a))
forall a b. (a -> b) -> a -> b
$ (a -> Elim' a) -> (a -> Elim' a) -> SynEqA (a -> Elim' a)
forall a. a -> a -> SynEqA a
equal (a -> a -> a -> Elim' a
forall a. a -> a -> a -> Elim' a
IApply a
u a
v) (a -> a -> a -> Elim' a
forall a. a -> a -> a -> Elim' a
IApply a
u' a
v') SynEqA (a -> Elim' a) -> SynEqA a -> SynEqA (Elim' a)
forall a b. SynEqA (a -> b) -> SynEqA a -> SynEqA b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> a -> a -> SynEqA a
forall a. SynEq a => a -> a -> SynEqA a
synEq a
r a
r'
      (Elim' a, Elim' a)
_                   -> SynEqA (Elim' a)
-> Result
     ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA (Elim' a))
ret (SynEqA (Elim' a)
 -> Result
      ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA (Elim' a)))
-> SynEqA (Elim' a)
-> Result
     ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA (Elim' a))
forall a b. (a -> b) -> a -> b
$ Elim' a -> Elim' a -> SynEqA (Elim' a)
forall a. a -> a -> SynEqA a
inequal Elim' a
e Elim' a
e'

instance (Subst a, SynEq a) => SynEq (Abs a) where
  synEq :: Abs a -> Abs a -> SynEqA (Abs a)
synEq Abs a
a Abs a
a' = ((SynEqA (Abs a)
  -> Result
       ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA (Abs a)))
 -> Result
      ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA (Abs a)))
-> SynEqA (Abs a)
forall a.
ExpandCase LiftedRep a =>
((a -> Result LiftedRep a) -> Result LiftedRep a) -> a
expand \SynEqA (Abs a)
-> Result
     ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA (Abs a))
ret ->
    case (Abs a
a, Abs a
a') of
      (NoAbs ArgName
x a
b, NoAbs ArgName
x' a
b') -> SynEqA (Abs a)
-> Result
     ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA (Abs a))
ret (SynEqA (Abs a)
 -> Result
      ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA (Abs a)))
-> SynEqA (Abs a)
-> Result
     ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA (Abs a))
forall a b. (a -> b) -> a -> b
$ (a -> Abs a) -> (a -> Abs a) -> SynEqA (a -> Abs a)
forall a. a -> a -> SynEqA a
equal (ArgName -> a -> Abs a
forall a. ArgName -> a -> Abs a
NoAbs ArgName
x) (ArgName -> a -> Abs a
forall a. ArgName -> a -> Abs a
NoAbs ArgName
x') SynEqA (a -> Abs a) -> SynEqA a -> SynEqA (Abs a)
forall a b. SynEqA (a -> b) -> SynEqA a -> SynEqA b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> a -> a -> SynEqA a
forall a. SynEq a => a -> a -> SynEqA a
synEq a
b a
b'
      (Abs   ArgName
x a
b, Abs   ArgName
x' a
b') -> SynEqA (Abs a)
-> Result
     ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA (Abs a))
ret (SynEqA (Abs a)
 -> Result
      ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA (Abs a)))
-> SynEqA (Abs a)
-> Result
     ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA (Abs a))
forall a b. (a -> b) -> a -> b
$ (a -> Abs a) -> (a -> Abs a) -> SynEqA (a -> Abs a)
forall a. a -> a -> SynEqA a
equal (ArgName -> a -> Abs a
forall a. ArgName -> a -> Abs a
Abs ArgName
x) (ArgName -> a -> Abs a
forall a. ArgName -> a -> Abs a
Abs ArgName
x') SynEqA (a -> Abs a) -> SynEqA a -> SynEqA (Abs a)
forall a b. SynEqA (a -> b) -> SynEqA a -> SynEqA b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> a -> a -> SynEqA a
forall a. SynEq a => a -> a -> SynEqA a
synEq a
b a
b'
      (Abs   ArgName
x a
b, NoAbs ArgName
x' a
b') -> SynEqA (Abs a)
-> Result
     ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA (Abs a))
ret (SynEqA (Abs a)
 -> Result
      ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA (Abs a)))
-> SynEqA (Abs a)
-> Result
     ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA (Abs a))
forall a b. (a -> b) -> a -> b
$ ArgName -> a -> Abs a
forall a. ArgName -> a -> Abs a
Abs ArgName
x  (a -> Abs a) -> SynEqA a -> SynEqA (Abs a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> a -> SynEqA a
forall a. SynEq a => a -> a -> SynEqA a
synEq a
b (Int -> a -> a
forall a. Subst a => Int -> a -> a
raise Int
1 a
b')
      (NoAbs ArgName
x a
b, Abs   ArgName
x' a
b') -> SynEqA (Abs a)
-> Result
     ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA (Abs a))
ret (SynEqA (Abs a)
 -> Result
      ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA (Abs a)))
-> SynEqA (Abs a)
-> Result
     ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA (Abs a))
forall a b. (a -> b) -> a -> b
$ ArgName -> a -> Abs a
forall a. ArgName -> a -> Abs a
Abs ArgName
x' (a -> Abs a) -> SynEqA a -> SynEqA (Abs a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> a -> SynEqA a
forall a. SynEq a => a -> a -> SynEqA a
synEq (Int -> a -> a
forall a. Subst a => Int -> a -> a
raise Int
1 a
b) a
b'

instance SynEq a => SynEq (Arg a) where
  synEq :: Arg a -> Arg a -> SynEqA (Arg a)
synEq Arg a
x Arg a
y = ((SynEqA (Arg a)
  -> Result
       ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA (Arg a)))
 -> Result
      ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA (Arg a)))
-> SynEqA (Arg a)
forall a.
ExpandCase LiftedRep a =>
((a -> Result LiftedRep a) -> Result LiftedRep a) -> a
expand \SynEqA (Arg a)
-> Result
     ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA (Arg a))
ret -> case (Arg a
x, Arg a
y) of
    -- NOTE: Do not ignore 'ArgInfo', or test/fail/UnequalHiding will pass.
    ((Arg ArgInfo
ai a
a), (Arg ArgInfo
ai' a
a')) -> SynEqA (Arg a)
-> Result
     ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA (Arg a))
ret (SynEqA (Arg a)
 -> Result
      ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA (Arg a)))
-> SynEqA (Arg a)
-> Result
     ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA (Arg a))
forall a b. (a -> b) -> a -> b
$ ArgInfo -> a -> Arg a
forall e. ArgInfo -> e -> Arg e
Arg (ArgInfo -> a -> Arg a) -> SynEqA ArgInfo -> SynEqA (a -> Arg a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ArgInfo -> ArgInfo -> SynEqA ArgInfo
forall a. SynEq a => a -> a -> SynEqA a
synEq ArgInfo
ai ArgInfo
ai' SynEqA (a -> Arg a) -> SynEqA a -> SynEqA (Arg a)
forall a b. SynEqA (a -> b) -> SynEqA a -> SynEqA b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> a -> a -> SynEqA a
forall a. SynEq a => a -> a -> SynEqA a
synEq a
a a
a'

-- | Ignores tactic argument annotations.
instance SynEq a => SynEq (Dom a) where
  synEq :: Dom a -> Dom a -> SynEqA (Dom a)
synEq Dom a
d Dom a
d' = ((SynEqA (Dom a)
  -> Result
       ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA (Dom a)))
 -> Result
      ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA (Dom a)))
-> SynEqA (Dom a)
forall a.
ExpandCase LiftedRep a =>
((a -> Result LiftedRep a) -> Result LiftedRep a) -> a
expand \SynEqA (Dom a)
-> Result
     ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA (Dom a))
ret -> case (Dom a
d, Dom a
d') of
    (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 Maybe NamedName -> Maybe NamedName -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe NamedName
x'   -> SynEqA (Dom a)
-> Result
     ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA (Dom a))
ret (SynEqA (Dom a)
 -> Result
      ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA (Dom a)))
-> SynEqA (Dom a)
-> Result
     ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA (Dom a))
forall a b. (a -> b) -> a -> b
$ ArgInfo -> Maybe NamedName -> Bool -> Maybe Term -> a -> Dom a
forall t e.
ArgInfo -> Maybe NamedName -> Bool -> Maybe t -> e -> Dom' t e
Dom (ArgInfo -> Maybe NamedName -> Bool -> Maybe Term -> a -> Dom a)
-> SynEqA ArgInfo
-> SynEqA (Maybe NamedName -> Bool -> Maybe Term -> a -> Dom a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ArgInfo -> ArgInfo -> SynEqA ArgInfo
forall a. SynEq a => a -> a -> SynEqA a
synEq ArgInfo
ai ArgInfo
ai' SynEqA (Maybe NamedName -> Bool -> Maybe Term -> a -> Dom a)
-> SynEqA (Maybe NamedName)
-> SynEqA (Bool -> Maybe Term -> a -> Dom a)
forall a b. SynEqA (a -> b) -> SynEqA a -> SynEqA b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Maybe NamedName -> SynEqA (Maybe NamedName)
forall a. a -> SynEqA a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe NamedName
x SynEqA (Bool -> Maybe Term -> a -> Dom a)
-> SynEqA Bool -> SynEqA (Maybe Term -> a -> Dom a)
forall a b. SynEqA (a -> b) -> SynEqA a -> SynEqA b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Bool -> Bool -> SynEqA Bool
forall a. SynEq a => a -> a -> SynEqA a
synEq Bool
f Bool
f'
                               SynEqA (Maybe Term -> a -> Dom a)
-> SynEqA (Maybe Term) -> SynEqA (a -> Dom a)
forall a b. SynEqA (a -> b) -> SynEqA a -> SynEqA b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Maybe Term -> SynEqA (Maybe Term)
forall a. a -> SynEqA a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe Term
t SynEqA (a -> Dom a) -> SynEqA a -> SynEqA (Dom a)
forall a b. SynEqA (a -> b) -> SynEqA a -> SynEqA b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> a -> a -> SynEqA a
forall a. SynEq a => a -> a -> SynEqA a
synEq a
a a
a'
      | Bool
otherwise -> SynEqA (Dom a)
-> Result
     ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA (Dom a))
ret (SynEqA (Dom a)
 -> Result
      ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA (Dom a)))
-> SynEqA (Dom a)
-> Result
     ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA (Dom a))
forall a b. (a -> b) -> a -> b
$ Dom a -> Dom a -> SynEqA (Dom a)
forall a. a -> a -> SynEqA a
inequal Dom a
d Dom a
d'

instance SynEq ArgInfo where
  synEq :: ArgInfo -> ArgInfo -> SynEqA ArgInfo
synEq ArgInfo
ai ArgInfo
ai' = ((SynEqA ArgInfo
  -> Result
       ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA ArgInfo))
 -> Result
      ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA ArgInfo))
-> SynEqA ArgInfo
forall a.
ExpandCase LiftedRep a =>
((a -> Result LiftedRep a) -> Result LiftedRep a) -> a
expand \SynEqA ArgInfo
-> Result
     ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA ArgInfo)
ret -> case (ArgInfo
ai, ArgInfo
ai') of
    (ai :: ArgInfo
ai@(ArgInfo Hiding
h Origin
_ FreeVariables
_), ai' :: ArgInfo
ai'@(ArgInfo Hiding
h' Origin
_ FreeVariables
_))
      | Hiding
h Hiding -> Hiding -> Bool
forall a. Eq a => a -> a -> Bool
== Hiding
h'   -> SynEqA ArgInfo
-> Result
     ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA ArgInfo)
ret (SynEqA ArgInfo
 -> Result
      ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA ArgInfo))
-> SynEqA ArgInfo
-> Result
     ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA ArgInfo)
forall a b. (a -> b) -> a -> b
$ ArgInfo -> SynEqA ArgInfo
forall a. a -> SynEqA a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ArgInfo
ai
      | Bool
otherwise -> SynEqA ArgInfo
-> Result
     ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA ArgInfo)
ret (SynEqA ArgInfo
 -> Result
      ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA ArgInfo))
-> SynEqA ArgInfo
-> Result
     ('TupleRep '[LiftedRep, LiftedRep, 'IntRep]) (SynEqA ArgInfo)
forall a b. (a -> b) -> a -> b
$ ArgInfo -> ArgInfo -> SynEqA ArgInfo
forall a. a -> a -> SynEqA a
inequal ArgInfo
ai ArgInfo
ai'