-- editorconfig-checker-disable-file
-- | 'Eq' instances for core data types.

{-# OPTIONS_GHC -fno-warn-orphans #-}

{-# LANGUAGE FlexibleInstances    #-}
{-# LANGUAGE RankNTypes           #-}
{-# LANGUAGE TypeApplications     #-}
{-# LANGUAGE TypeFamilies         #-}
{-# LANGUAGE TypeOperators        #-}
{-# LANGUAGE UndecidableInstances #-}

module PlutusCore.Core.Instance.Eq () where

import PlutusPrelude

import PlutusCore.Core.Type
import PlutusCore.DeBruijn
import PlutusCore.Eq
import PlutusCore.Name.Unique
import PlutusCore.Rename.Monad

import Universe

instance (GEq uni, Eq ann) => Eq (Type TyName uni ann) where
    Type TyName uni ann
ty1 == :: Type TyName uni ann -> Type TyName uni ann -> Bool
== Type TyName uni ann
ty2 = forall ren. Monoid ren => EqRename ren -> Bool
runEqRename @TypeRenaming (EqRename TypeRenaming -> Bool) -> EqRename TypeRenaming -> Bool
forall a b. (a -> b) -> a -> b
$ Type TyName uni ann -> Type TyName uni ann -> EqRename TypeRenaming
forall ren (uni :: * -> *) ann tyname.
(HasRenaming ren TypeUnique, GEq uni, Eq ann) =>
EqRenameOf ren (Type tyname uni ann)
eqTypeM Type TyName uni ann
ty1 Type TyName uni ann
ty2

instance
        ( GEq uni, Closed uni, uni `Everywhere` Eq, Eq fun, Eq ann
        ) => Eq (Term TyName Name uni fun ann) where
    Term TyName Name uni fun ann
term1 == :: Term TyName Name uni fun ann
-> Term TyName Name uni fun ann -> Bool
== Term TyName Name uni fun ann
term2 = EqRename ScopedRenaming -> Bool
forall ren. Monoid ren => EqRename ren -> Bool
runEqRename (EqRename ScopedRenaming -> Bool)
-> EqRename ScopedRenaming -> Bool
forall a b. (a -> b) -> a -> b
$ Term TyName Name uni fun ann
-> Term TyName Name uni fun ann -> EqRename ScopedRenaming
forall (uni :: * -> *) fun ann tyname name.
(GEq uni, Closed uni, Everywhere uni Eq, Eq fun, Eq ann) =>
EqRenameOf ScopedRenaming (Term tyname name uni fun ann)
eqTermM Term TyName Name uni fun ann
term1 Term TyName Name uni fun ann
term2

-- Simple Structural Equality of a `Term NamedDeBruijn`. This implies three things:
-- b) We do not do equality "modulo starting index". E.g. `LamAbs 0 (Var 0) /= LamAbs 1 (Var 1)`.
-- c) We do not do equality ""modulo annotations".
-- Note that we ignore the name part in case of the nameddebruijn
-- If a user wants to ignore annotations he must prior do `void <$> term`, to throw away any annotations.
deriving stock instance
   (GEq uni, Closed uni, uni `Everywhere` Eq, Eq fun, Eq ann) =>
   Eq (Term NamedTyDeBruijn NamedDeBruijn uni fun ann)

deriving stock instance
   (GEq uni, Closed uni, uni `Everywhere` Eq, Eq fun, Eq ann) =>
   Eq (Term TyDeBruijn DeBruijn uni fun ann)

deriving stock instance
   (GEq uni, Closed uni, uni `Everywhere` Eq, Eq ann) =>
   Eq (Type NamedTyDeBruijn uni ann)

deriving stock instance
   (GEq uni, Closed uni, uni `Everywhere` Eq, Eq ann) =>
   Eq (Type TyDeBruijn uni ann)

deriving stock instance (GEq uni, Closed uni, uni `Everywhere` Eq, Eq fun, Eq ann,
                  Eq (Term tyname name uni fun ann)
                  ) =>  Eq (Program tyname name uni fun ann)

type EqRenameOf ren a = HasUniques a => a -> a -> EqRename ren

{- Note [No catch-all]
Catch-all clauses like @f _x = <...>@ have the disadvantage that if somebody adds a new constructor
to the definition of the type of @_x@, then GHC will not warn us about @f@ potentially no longer
being defined correctly. This is especially pronounced for equality checking functions, having

    _ == _ = False

as the last clause of '(==)' makes it much trickier to spot that a new clause needs to be added if
the type of the arguments get extended with a new constructor. For this reason in equality checking
functions we always match on the first argument exhaustively even if it means having a wall of

    C1 == _ = False
    C2 == _ = False
    <...>
    Cn == _ = False

This way we get a warning from GHC about non-exhaustive pattern matching if the type of the
arguments gets extended with additional constructors.
-}

-- See Note [Modulo alpha].
-- See Note [Scope tracking]
-- See Note [Side tracking]
-- See Note [No catch-all].
-- | Check equality of two 'Type's.
eqTypeM :: (HasRenaming ren TypeUnique, GEq uni, Eq ann) => EqRenameOf ren (Type tyname uni ann)
eqTypeM :: forall ren (uni :: * -> *) ann tyname.
(HasRenaming ren TypeUnique, GEq uni, Eq ann) =>
EqRenameOf ren (Type tyname uni ann)
eqTypeM (TyVar ann
ann1 tyname
name1) (TyVar ann
ann2 tyname
name2) = do
    ann -> ann -> EqRename ren
forall a ren. Eq a => a -> a -> EqRename ren
eqM ann
ann1 ann
ann2
    tyname -> tyname -> EqRename ren
forall ren unique name.
(HasRenaming ren unique, HasUnique name unique, Eq unique) =>
name -> name -> EqRename ren
eqNameM tyname
name1 tyname
name2
eqTypeM (TyLam ann
ann1 tyname
name1 Kind ann
kind1 Type tyname uni ann
ty1) (TyLam ann
ann2 tyname
name2 Kind ann
kind2 Type tyname uni ann
ty2) = do
    ann -> ann -> EqRename ren
forall a ren. Eq a => a -> a -> EqRename ren
eqM ann
ann1 ann
ann2
    Kind ann -> Kind ann -> EqRename ren
forall a ren. Eq a => a -> a -> EqRename ren
eqM Kind ann
kind1 Kind ann
kind2
    tyname -> tyname -> EqRename ren -> EqRename ren
forall ren unique name (m :: * -> *) c.
(HasRenaming ren unique, HasUnique name unique, Monad m) =>
name
-> name
-> RenameT (Bilateral ren) m c
-> RenameT (Bilateral ren) m c
withTwinBindings tyname
name1 tyname
name2 (EqRename ren -> EqRename ren) -> EqRename ren -> EqRename ren
forall a b. (a -> b) -> a -> b
$ Type tyname uni ann -> Type tyname uni ann -> EqRename ren
forall ren (uni :: * -> *) ann tyname.
(HasRenaming ren TypeUnique, GEq uni, Eq ann) =>
EqRenameOf ren (Type tyname uni ann)
eqTypeM Type tyname uni ann
ty1 Type tyname uni ann
ty2
eqTypeM (TyForall ann
ann1 tyname
name1 Kind ann
kind1 Type tyname uni ann
ty1) (TyForall ann
ann2 tyname
name2 Kind ann
kind2 Type tyname uni ann
ty2) = do
    ann -> ann -> EqRename ren
forall a ren. Eq a => a -> a -> EqRename ren
eqM ann
ann1 ann
ann2
    Kind ann -> Kind ann -> EqRename ren
forall a ren. Eq a => a -> a -> EqRename ren
eqM Kind ann
kind1 Kind ann
kind2
    tyname -> tyname -> EqRename ren -> EqRename ren
forall ren unique name (m :: * -> *) c.
(HasRenaming ren unique, HasUnique name unique, Monad m) =>
name
-> name
-> RenameT (Bilateral ren) m c
-> RenameT (Bilateral ren) m c
withTwinBindings tyname
name1 tyname
name2 (EqRename ren -> EqRename ren) -> EqRename ren -> EqRename ren
forall a b. (a -> b) -> a -> b
$ Type tyname uni ann -> Type tyname uni ann -> EqRename ren
forall ren (uni :: * -> *) ann tyname.
(HasRenaming ren TypeUnique, GEq uni, Eq ann) =>
EqRenameOf ren (Type tyname uni ann)
eqTypeM Type tyname uni ann
ty1 Type tyname uni ann
ty2
eqTypeM (TyIFix ann
ann1 Type tyname uni ann
pat1 Type tyname uni ann
arg1) (TyIFix ann
ann2 Type tyname uni ann
pat2 Type tyname uni ann
arg2) = do
    ann -> ann -> EqRename ren
forall a ren. Eq a => a -> a -> EqRename ren
eqM ann
ann1 ann
ann2
    Type tyname uni ann -> Type tyname uni ann -> EqRename ren
forall ren (uni :: * -> *) ann tyname.
(HasRenaming ren TypeUnique, GEq uni, Eq ann) =>
EqRenameOf ren (Type tyname uni ann)
eqTypeM Type tyname uni ann
pat1 Type tyname uni ann
pat2
    Type tyname uni ann -> Type tyname uni ann -> EqRename ren
forall ren (uni :: * -> *) ann tyname.
(HasRenaming ren TypeUnique, GEq uni, Eq ann) =>
EqRenameOf ren (Type tyname uni ann)
eqTypeM Type tyname uni ann
arg1 Type tyname uni ann
arg2
eqTypeM (TyApp ann
ann1 Type tyname uni ann
fun1 Type tyname uni ann
arg1) (TyApp ann
ann2 Type tyname uni ann
fun2 Type tyname uni ann
arg2) = do
    ann -> ann -> EqRename ren
forall a ren. Eq a => a -> a -> EqRename ren
eqM ann
ann1 ann
ann2
    Type tyname uni ann -> Type tyname uni ann -> EqRename ren
forall ren (uni :: * -> *) ann tyname.
(HasRenaming ren TypeUnique, GEq uni, Eq ann) =>
EqRenameOf ren (Type tyname uni ann)
eqTypeM Type tyname uni ann
fun1 Type tyname uni ann
fun2
    Type tyname uni ann -> Type tyname uni ann -> EqRename ren
forall ren (uni :: * -> *) ann tyname.
(HasRenaming ren TypeUnique, GEq uni, Eq ann) =>
EqRenameOf ren (Type tyname uni ann)
eqTypeM Type tyname uni ann
arg1 Type tyname uni ann
arg2
eqTypeM (TyFun ann
ann1 Type tyname uni ann
dom1 Type tyname uni ann
cod1) (TyFun ann
ann2 Type tyname uni ann
dom2 Type tyname uni ann
cod2) = do
    ann -> ann -> EqRename ren
forall a ren. Eq a => a -> a -> EqRename ren
eqM ann
ann1 ann
ann2
    Type tyname uni ann -> Type tyname uni ann -> EqRename ren
forall ren (uni :: * -> *) ann tyname.
(HasRenaming ren TypeUnique, GEq uni, Eq ann) =>
EqRenameOf ren (Type tyname uni ann)
eqTypeM Type tyname uni ann
dom1 Type tyname uni ann
dom2
    Type tyname uni ann -> Type tyname uni ann -> EqRename ren
forall ren (uni :: * -> *) ann tyname.
(HasRenaming ren TypeUnique, GEq uni, Eq ann) =>
EqRenameOf ren (Type tyname uni ann)
eqTypeM Type tyname uni ann
cod1 Type tyname uni ann
cod2
eqTypeM (TyBuiltin ann
ann1 SomeTypeIn uni
someUni1) (TyBuiltin ann
ann2 SomeTypeIn uni
someUni2) = do
    ann -> ann -> EqRename ren
forall a ren. Eq a => a -> a -> EqRename ren
eqM ann
ann1 ann
ann2
    SomeTypeIn uni -> SomeTypeIn uni -> EqRename ren
forall a ren. Eq a => a -> a -> EqRename ren
eqM SomeTypeIn uni
someUni1 SomeTypeIn uni
someUni2
eqTypeM (TySOP ann
ann1 [[Type tyname uni ann]]
tyls1) (TySOP ann
ann2 [[Type tyname uni ann]]
tyls2) = do
    ann -> ann -> EqRename ren
forall a ren. Eq a => a -> a -> EqRename ren
eqM ann
ann1 ann
ann2
    case [[Type tyname uni ann]]
-> [[Type tyname uni ann]]
-> Maybe [([Type tyname uni ann], [Type tyname uni ann])]
forall a b. [a] -> [b] -> Maybe [(a, b)]
zipExact [[Type tyname uni ann]]
tyls1 [[Type tyname uni ann]]
tyls2 of
        Just [([Type tyname uni ann], [Type tyname uni ann])]
ps -> [([Type tyname uni ann], [Type tyname uni ann])]
-> (([Type tyname uni ann], [Type tyname uni ann]) -> EqRename ren)
-> EqRename ren
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
t a -> (a -> f b) -> f ()
for_ [([Type tyname uni ann], [Type tyname uni ann])]
ps ((([Type tyname uni ann], [Type tyname uni ann]) -> EqRename ren)
 -> EqRename ren)
-> (([Type tyname uni ann], [Type tyname uni ann]) -> EqRename ren)
-> EqRename ren
forall a b. (a -> b) -> a -> b
$ \([Type tyname uni ann]
ptys1, [Type tyname uni ann]
ptys2) -> case [Type tyname uni ann]
-> [Type tyname uni ann]
-> Maybe [(Type tyname uni ann, Type tyname uni ann)]
forall a b. [a] -> [b] -> Maybe [(a, b)]
zipExact [Type tyname uni ann]
ptys1 [Type tyname uni ann]
ptys2 of
          Just [(Type tyname uni ann, Type tyname uni ann)]
tys -> [(Type tyname uni ann, Type tyname uni ann)]
-> ((Type tyname uni ann, Type tyname uni ann) -> EqRename ren)
-> EqRename ren
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
t a -> (a -> f b) -> f ()
for_ [(Type tyname uni ann, Type tyname uni ann)]
tys (((Type tyname uni ann, Type tyname uni ann) -> EqRename ren)
 -> EqRename ren)
-> ((Type tyname uni ann, Type tyname uni ann) -> EqRename ren)
-> EqRename ren
forall a b. (a -> b) -> a -> b
$ \(Type tyname uni ann
ty1, Type tyname uni ann
ty2) -> Type tyname uni ann -> Type tyname uni ann -> EqRename ren
forall ren (uni :: * -> *) ann tyname.
(HasRenaming ren TypeUnique, GEq uni, Eq ann) =>
EqRenameOf ren (Type tyname uni ann)
eqTypeM Type tyname uni ann
ty1 Type tyname uni ann
ty2
          Maybe [(Type tyname uni ann, Type tyname uni ann)]
Nothing  -> EqRename ren
forall a. RenameT (Bilateral ren) Maybe a
forall (f :: * -> *) a. Alternative f => f a
empty
        Maybe [([Type tyname uni ann], [Type tyname uni ann])]
Nothing -> EqRename ren
forall a. RenameT (Bilateral ren) Maybe a
forall (f :: * -> *) a. Alternative f => f a
empty
eqTypeM TyVar{}     Type tyname uni ann
_ = EqRename ren
forall a. RenameT (Bilateral ren) Maybe a
forall (f :: * -> *) a. Alternative f => f a
empty
eqTypeM TyLam{}     Type tyname uni ann
_ = EqRename ren
forall a. RenameT (Bilateral ren) Maybe a
forall (f :: * -> *) a. Alternative f => f a
empty
eqTypeM TyForall{}  Type tyname uni ann
_ = EqRename ren
forall a. RenameT (Bilateral ren) Maybe a
forall (f :: * -> *) a. Alternative f => f a
empty
eqTypeM TyIFix{}    Type tyname uni ann
_ = EqRename ren
forall a. RenameT (Bilateral ren) Maybe a
forall (f :: * -> *) a. Alternative f => f a
empty
eqTypeM TyApp{}     Type tyname uni ann
_ = EqRename ren
forall a. RenameT (Bilateral ren) Maybe a
forall (f :: * -> *) a. Alternative f => f a
empty
eqTypeM TyFun{}     Type tyname uni ann
_ = EqRename ren
forall a. RenameT (Bilateral ren) Maybe a
forall (f :: * -> *) a. Alternative f => f a
empty
eqTypeM TyBuiltin{} Type tyname uni ann
_ = EqRename ren
forall a. RenameT (Bilateral ren) Maybe a
forall (f :: * -> *) a. Alternative f => f a
empty
eqTypeM TySOP{} Type tyname uni ann
_ = EqRename ren
forall a. RenameT (Bilateral ren) Maybe a
forall (f :: * -> *) a. Alternative f => f a
empty

-- See Note [Modulo alpha].
-- See Note [Scope tracking]
-- See Note [Side tracking]
-- See Note [No catch-all].
-- | Check equality of two 'Term's.
eqTermM
    :: (GEq uni, Closed uni, uni `Everywhere` Eq, Eq fun, Eq ann)
    => EqRenameOf ScopedRenaming (Term tyname name uni fun ann)
eqTermM :: forall (uni :: * -> *) fun ann tyname name.
(GEq uni, Closed uni, Everywhere uni Eq, Eq fun, Eq ann) =>
EqRenameOf ScopedRenaming (Term tyname name uni fun ann)
eqTermM (LamAbs ann
ann1 name
name1 Type tyname uni ann
ty1 Term tyname name uni fun ann
body1) (LamAbs ann
ann2 name
name2 Type tyname uni ann
ty2 Term tyname name uni fun ann
body2) = do
    ann -> ann -> EqRename ScopedRenaming
forall a ren. Eq a => a -> a -> EqRename ren
eqM ann
ann1 ann
ann2
    Type tyname uni ann
-> Type tyname uni ann -> EqRename ScopedRenaming
forall ren (uni :: * -> *) ann tyname.
(HasRenaming ren TypeUnique, GEq uni, Eq ann) =>
EqRenameOf ren (Type tyname uni ann)
eqTypeM Type tyname uni ann
ty1 Type tyname uni ann
ty2
    name -> name -> EqRename ScopedRenaming -> EqRename ScopedRenaming
forall ren unique name (m :: * -> *) c.
(HasRenaming ren unique, HasUnique name unique, Monad m) =>
name
-> name
-> RenameT (Bilateral ren) m c
-> RenameT (Bilateral ren) m c
withTwinBindings name
name1 name
name2 (EqRename ScopedRenaming -> EqRename ScopedRenaming)
-> EqRename ScopedRenaming -> EqRename ScopedRenaming
forall a b. (a -> b) -> a -> b
$ Term tyname name uni fun ann
-> Term tyname name uni fun ann -> EqRename ScopedRenaming
forall (uni :: * -> *) fun ann tyname name.
(GEq uni, Closed uni, Everywhere uni Eq, Eq fun, Eq ann) =>
EqRenameOf ScopedRenaming (Term tyname name uni fun ann)
eqTermM Term tyname name uni fun ann
body1 Term tyname name uni fun ann
body2
eqTermM (TyAbs ann
ann1 tyname
name1 Kind ann
kind1 Term tyname name uni fun ann
body1) (TyAbs ann
ann2 tyname
name2 Kind ann
kind2 Term tyname name uni fun ann
body2) = do
    ann -> ann -> EqRename ScopedRenaming
forall a ren. Eq a => a -> a -> EqRename ren
eqM ann
ann1 ann
ann2
    Kind ann -> Kind ann -> EqRename ScopedRenaming
forall a ren. Eq a => a -> a -> EqRename ren
eqM Kind ann
kind1 Kind ann
kind2
    tyname
-> tyname -> EqRename ScopedRenaming -> EqRename ScopedRenaming
forall ren unique name (m :: * -> *) c.
(HasRenaming ren unique, HasUnique name unique, Monad m) =>
name
-> name
-> RenameT (Bilateral ren) m c
-> RenameT (Bilateral ren) m c
withTwinBindings tyname
name1 tyname
name2 (EqRename ScopedRenaming -> EqRename ScopedRenaming)
-> EqRename ScopedRenaming -> EqRename ScopedRenaming
forall a b. (a -> b) -> a -> b
$ Term tyname name uni fun ann
-> Term tyname name uni fun ann -> EqRename ScopedRenaming
forall (uni :: * -> *) fun ann tyname name.
(GEq uni, Closed uni, Everywhere uni Eq, Eq fun, Eq ann) =>
EqRenameOf ScopedRenaming (Term tyname name uni fun ann)
eqTermM Term tyname name uni fun ann
body1 Term tyname name uni fun ann
body2
eqTermM (IWrap ann
ann1 Type tyname uni ann
pat1 Type tyname uni ann
arg1 Term tyname name uni fun ann
term1) (IWrap ann
ann2 Type tyname uni ann
pat2 Type tyname uni ann
arg2 Term tyname name uni fun ann
term2) = do
    ann -> ann -> EqRename ScopedRenaming
forall a ren. Eq a => a -> a -> EqRename ren
eqM ann
ann1 ann
ann2
    Type tyname uni ann
-> Type tyname uni ann -> EqRename ScopedRenaming
forall ren (uni :: * -> *) ann tyname.
(HasRenaming ren TypeUnique, GEq uni, Eq ann) =>
EqRenameOf ren (Type tyname uni ann)
eqTypeM Type tyname uni ann
pat1 Type tyname uni ann
pat2
    Type tyname uni ann
-> Type tyname uni ann -> EqRename ScopedRenaming
forall ren (uni :: * -> *) ann tyname.
(HasRenaming ren TypeUnique, GEq uni, Eq ann) =>
EqRenameOf ren (Type tyname uni ann)
eqTypeM Type tyname uni ann
arg1 Type tyname uni ann
arg2
    Term tyname name uni fun ann
-> Term tyname name uni fun ann -> EqRename ScopedRenaming
forall (uni :: * -> *) fun ann tyname name.
(GEq uni, Closed uni, Everywhere uni Eq, Eq fun, Eq ann) =>
EqRenameOf ScopedRenaming (Term tyname name uni fun ann)
eqTermM Term tyname name uni fun ann
term1 Term tyname name uni fun ann
term2
eqTermM (Apply ann
ann1 Term tyname name uni fun ann
fun1 Term tyname name uni fun ann
arg1) (Apply ann
ann2 Term tyname name uni fun ann
fun2 Term tyname name uni fun ann
arg2) = do
    ann -> ann -> EqRename ScopedRenaming
forall a ren. Eq a => a -> a -> EqRename ren
eqM ann
ann1 ann
ann2
    Term tyname name uni fun ann
-> Term tyname name uni fun ann -> EqRename ScopedRenaming
forall (uni :: * -> *) fun ann tyname name.
(GEq uni, Closed uni, Everywhere uni Eq, Eq fun, Eq ann) =>
EqRenameOf ScopedRenaming (Term tyname name uni fun ann)
eqTermM Term tyname name uni fun ann
fun1 Term tyname name uni fun ann
fun2
    Term tyname name uni fun ann
-> Term tyname name uni fun ann -> EqRename ScopedRenaming
forall (uni :: * -> *) fun ann tyname name.
(GEq uni, Closed uni, Everywhere uni Eq, Eq fun, Eq ann) =>
EqRenameOf ScopedRenaming (Term tyname name uni fun ann)
eqTermM Term tyname name uni fun ann
arg1 Term tyname name uni fun ann
arg2
eqTermM (Unwrap ann
ann1 Term tyname name uni fun ann
term1) (Unwrap ann
ann2 Term tyname name uni fun ann
term2) = do
    ann -> ann -> EqRename ScopedRenaming
forall a ren. Eq a => a -> a -> EqRename ren
eqM ann
ann1 ann
ann2
    Term tyname name uni fun ann
-> Term tyname name uni fun ann -> EqRename ScopedRenaming
forall (uni :: * -> *) fun ann tyname name.
(GEq uni, Closed uni, Everywhere uni Eq, Eq fun, Eq ann) =>
EqRenameOf ScopedRenaming (Term tyname name uni fun ann)
eqTermM Term tyname name uni fun ann
term1 Term tyname name uni fun ann
term2
eqTermM (Error ann
ann1 Type tyname uni ann
ty1) (Error ann
ann2 Type tyname uni ann
ty2) = do
    ann -> ann -> EqRename ScopedRenaming
forall a ren. Eq a => a -> a -> EqRename ren
eqM ann
ann1 ann
ann2
    Type tyname uni ann
-> Type tyname uni ann -> EqRename ScopedRenaming
forall ren (uni :: * -> *) ann tyname.
(HasRenaming ren TypeUnique, GEq uni, Eq ann) =>
EqRenameOf ren (Type tyname uni ann)
eqTypeM Type tyname uni ann
ty1 Type tyname uni ann
ty2
eqTermM (TyInst ann
ann1 Term tyname name uni fun ann
term1 Type tyname uni ann
ty1) (TyInst ann
ann2 Term tyname name uni fun ann
term2 Type tyname uni ann
ty2) = do
    ann -> ann -> EqRename ScopedRenaming
forall a ren. Eq a => a -> a -> EqRename ren
eqM ann
ann1 ann
ann2
    Term tyname name uni fun ann
-> Term tyname name uni fun ann -> EqRename ScopedRenaming
forall (uni :: * -> *) fun ann tyname name.
(GEq uni, Closed uni, Everywhere uni Eq, Eq fun, Eq ann) =>
EqRenameOf ScopedRenaming (Term tyname name uni fun ann)
eqTermM Term tyname name uni fun ann
term1 Term tyname name uni fun ann
term2
    Type tyname uni ann
-> Type tyname uni ann -> EqRename ScopedRenaming
forall ren (uni :: * -> *) ann tyname.
(HasRenaming ren TypeUnique, GEq uni, Eq ann) =>
EqRenameOf ren (Type tyname uni ann)
eqTypeM Type tyname uni ann
ty1 Type tyname uni ann
ty2
eqTermM (Var ann
ann1 name
name1) (Var ann
ann2 name
name2) = do
    ann -> ann -> EqRename ScopedRenaming
forall a ren. Eq a => a -> a -> EqRename ren
eqM ann
ann1 ann
ann2
    name -> name -> EqRename ScopedRenaming
forall ren unique name.
(HasRenaming ren unique, HasUnique name unique, Eq unique) =>
name -> name -> EqRename ren
eqNameM name
name1 name
name2
eqTermM (Constant ann
ann1 Some (ValueOf uni)
con1) (Constant ann
ann2 Some (ValueOf uni)
con2) = do
    ann -> ann -> EqRename ScopedRenaming
forall a ren. Eq a => a -> a -> EqRename ren
eqM ann
ann1 ann
ann2
    Some (ValueOf uni) -> Some (ValueOf uni) -> EqRename ScopedRenaming
forall a ren. Eq a => a -> a -> EqRename ren
eqM Some (ValueOf uni)
con1 Some (ValueOf uni)
con2
eqTermM (Builtin ann
ann1 fun
bi1) (Builtin ann
ann2 fun
bi2) = do
    ann -> ann -> EqRename ScopedRenaming
forall a ren. Eq a => a -> a -> EqRename ren
eqM ann
ann1 ann
ann2
    fun -> fun -> EqRename ScopedRenaming
forall a ren. Eq a => a -> a -> EqRename ren
eqM fun
bi1 fun
bi2
eqTermM (Constr ann
ann1 Type tyname uni ann
ty1 Word64
i1 [Term tyname name uni fun ann]
args1) (Constr ann
ann2 Type tyname uni ann
ty2 Word64
i2 [Term tyname name uni fun ann]
args2) = do
    ann -> ann -> EqRename ScopedRenaming
forall a ren. Eq a => a -> a -> EqRename ren
eqM ann
ann1 ann
ann2
    Type tyname uni ann
-> Type tyname uni ann -> EqRename ScopedRenaming
forall ren (uni :: * -> *) ann tyname.
(HasRenaming ren TypeUnique, GEq uni, Eq ann) =>
EqRenameOf ren (Type tyname uni ann)
eqTypeM Type tyname uni ann
ty1 Type tyname uni ann
ty2
    Word64 -> Word64 -> EqRename ScopedRenaming
forall a ren. Eq a => a -> a -> EqRename ren
eqM Word64
i1 Word64
i2
    case [Term tyname name uni fun ann]
-> [Term tyname name uni fun ann]
-> Maybe
     [(Term tyname name uni fun ann, Term tyname name uni fun ann)]
forall a b. [a] -> [b] -> Maybe [(a, b)]
zipExact [Term tyname name uni fun ann]
args1 [Term tyname name uni fun ann]
args2 of
        Just [(Term tyname name uni fun ann, Term tyname name uni fun ann)]
ps -> [(Term tyname name uni fun ann, Term tyname name uni fun ann)]
-> ((Term tyname name uni fun ann, Term tyname name uni fun ann)
    -> EqRename ScopedRenaming)
-> EqRename ScopedRenaming
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
t a -> (a -> f b) -> f ()
for_ [(Term tyname name uni fun ann, Term tyname name uni fun ann)]
ps (((Term tyname name uni fun ann, Term tyname name uni fun ann)
  -> EqRename ScopedRenaming)
 -> EqRename ScopedRenaming)
-> ((Term tyname name uni fun ann, Term tyname name uni fun ann)
    -> EqRename ScopedRenaming)
-> EqRename ScopedRenaming
forall a b. (a -> b) -> a -> b
$ \(Term tyname name uni fun ann
t1, Term tyname name uni fun ann
t2) -> Term tyname name uni fun ann
-> Term tyname name uni fun ann -> EqRename ScopedRenaming
forall (uni :: * -> *) fun ann tyname name.
(GEq uni, Closed uni, Everywhere uni Eq, Eq fun, Eq ann) =>
EqRenameOf ScopedRenaming (Term tyname name uni fun ann)
eqTermM Term tyname name uni fun ann
t1 Term tyname name uni fun ann
t2
        Maybe
  [(Term tyname name uni fun ann, Term tyname name uni fun ann)]
Nothing -> EqRename ScopedRenaming
forall a. RenameT (Bilateral ScopedRenaming) Maybe a
forall (f :: * -> *) a. Alternative f => f a
empty
eqTermM (Case ann
ann1 Type tyname uni ann
ty1 Term tyname name uni fun ann
a1 [Term tyname name uni fun ann]
cs1) (Case ann
ann2 Type tyname uni ann
ty2 Term tyname name uni fun ann
a2 [Term tyname name uni fun ann]
cs2) = do
    ann -> ann -> EqRename ScopedRenaming
forall a ren. Eq a => a -> a -> EqRename ren
eqM ann
ann1 ann
ann2
    Type tyname uni ann
-> Type tyname uni ann -> EqRename ScopedRenaming
forall ren (uni :: * -> *) ann tyname.
(HasRenaming ren TypeUnique, GEq uni, Eq ann) =>
EqRenameOf ren (Type tyname uni ann)
eqTypeM Type tyname uni ann
ty1 Type tyname uni ann
ty2
    Term tyname name uni fun ann
-> Term tyname name uni fun ann -> EqRename ScopedRenaming
forall (uni :: * -> *) fun ann tyname name.
(GEq uni, Closed uni, Everywhere uni Eq, Eq fun, Eq ann) =>
EqRenameOf ScopedRenaming (Term tyname name uni fun ann)
eqTermM Term tyname name uni fun ann
a1 Term tyname name uni fun ann
a2
    case [Term tyname name uni fun ann]
-> [Term tyname name uni fun ann]
-> Maybe
     [(Term tyname name uni fun ann, Term tyname name uni fun ann)]
forall a b. [a] -> [b] -> Maybe [(a, b)]
zipExact [Term tyname name uni fun ann]
cs1 [Term tyname name uni fun ann]
cs2 of
        Just [(Term tyname name uni fun ann, Term tyname name uni fun ann)]
ps -> [(Term tyname name uni fun ann, Term tyname name uni fun ann)]
-> ((Term tyname name uni fun ann, Term tyname name uni fun ann)
    -> EqRename ScopedRenaming)
-> EqRename ScopedRenaming
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
t a -> (a -> f b) -> f ()
for_ [(Term tyname name uni fun ann, Term tyname name uni fun ann)]
ps (((Term tyname name uni fun ann, Term tyname name uni fun ann)
  -> EqRename ScopedRenaming)
 -> EqRename ScopedRenaming)
-> ((Term tyname name uni fun ann, Term tyname name uni fun ann)
    -> EqRename ScopedRenaming)
-> EqRename ScopedRenaming
forall a b. (a -> b) -> a -> b
$ \(Term tyname name uni fun ann
t1, Term tyname name uni fun ann
t2) -> Term tyname name uni fun ann
-> Term tyname name uni fun ann -> EqRename ScopedRenaming
forall (uni :: * -> *) fun ann tyname name.
(GEq uni, Closed uni, Everywhere uni Eq, Eq fun, Eq ann) =>
EqRenameOf ScopedRenaming (Term tyname name uni fun ann)
eqTermM Term tyname name uni fun ann
t1 Term tyname name uni fun ann
t2
        Maybe
  [(Term tyname name uni fun ann, Term tyname name uni fun ann)]
Nothing -> EqRename ScopedRenaming
forall a. RenameT (Bilateral ScopedRenaming) Maybe a
forall (f :: * -> *) a. Alternative f => f a
empty
eqTermM LamAbs{}   Term tyname name uni fun ann
_ = EqRename ScopedRenaming
forall a. RenameT (Bilateral ScopedRenaming) Maybe a
forall (f :: * -> *) a. Alternative f => f a
empty
eqTermM TyAbs{}    Term tyname name uni fun ann
_ = EqRename ScopedRenaming
forall a. RenameT (Bilateral ScopedRenaming) Maybe a
forall (f :: * -> *) a. Alternative f => f a
empty
eqTermM IWrap{}    Term tyname name uni fun ann
_ = EqRename ScopedRenaming
forall a. RenameT (Bilateral ScopedRenaming) Maybe a
forall (f :: * -> *) a. Alternative f => f a
empty
eqTermM Apply{}    Term tyname name uni fun ann
_ = EqRename ScopedRenaming
forall a. RenameT (Bilateral ScopedRenaming) Maybe a
forall (f :: * -> *) a. Alternative f => f a
empty
eqTermM Unwrap{}   Term tyname name uni fun ann
_ = EqRename ScopedRenaming
forall a. RenameT (Bilateral ScopedRenaming) Maybe a
forall (f :: * -> *) a. Alternative f => f a
empty
eqTermM Error{}    Term tyname name uni fun ann
_ = EqRename ScopedRenaming
forall a. RenameT (Bilateral ScopedRenaming) Maybe a
forall (f :: * -> *) a. Alternative f => f a
empty
eqTermM TyInst{}   Term tyname name uni fun ann
_ = EqRename ScopedRenaming
forall a. RenameT (Bilateral ScopedRenaming) Maybe a
forall (f :: * -> *) a. Alternative f => f a
empty
eqTermM Var{}      Term tyname name uni fun ann
_ = EqRename ScopedRenaming
forall a. RenameT (Bilateral ScopedRenaming) Maybe a
forall (f :: * -> *) a. Alternative f => f a
empty
eqTermM Constant{} Term tyname name uni fun ann
_ = EqRename ScopedRenaming
forall a. RenameT (Bilateral ScopedRenaming) Maybe a
forall (f :: * -> *) a. Alternative f => f a
empty
eqTermM Builtin{}  Term tyname name uni fun ann
_ = EqRename ScopedRenaming
forall a. RenameT (Bilateral ScopedRenaming) Maybe a
forall (f :: * -> *) a. Alternative f => f a
empty
eqTermM Constr{}  Term tyname name uni fun ann
_ = EqRename ScopedRenaming
forall a. RenameT (Bilateral ScopedRenaming) Maybe a
forall (f :: * -> *) a. Alternative f => f a
empty
eqTermM Case{}  Term tyname name uni fun ann
_ = EqRename ScopedRenaming
forall a. RenameT (Bilateral ScopedRenaming) Maybe a
forall (f :: * -> *) a. Alternative f => f a
empty