Don't ignore annotations on (U)PLC Term/Type equality

plutus-core/plutus-core/src/PlutusCore/Core/Instance/Eq.hs

@@ -11,7 +11,6 @@
 module PlutusCore.Core.Instance.Eq
     ( eqTypeM
     , eqTermM
-    , eqProgramM
     ) where
 
 import PlutusPrelude
@@ -23,58 +22,48 @@ import PlutusCore.Rename.Monad
 
 import Universe
 
--- See Note [Annotations and equality].
-
-instance Eq (Kind ann) where
-    Type _                == Type _                = True
-    KindArrow _ dom1 cod1 == KindArrow _ dom2 cod2 = dom1 == dom2 && cod1 == cod2
-    Type{}      == _                               = False
-    KindArrow{} == _                               = False
-
-instance Eq (Version ann) where
-    Version _ n1 m1 p1 == Version _ n2 m2 p2 = [n1, m1, p1] == [n2, m2, p2]
-
-instance (HasUniques (Type tyname uni ann), GEq uni) => Eq (Type tyname uni ann) where
+instance (HasUniques (Type tyname uni ann), GEq uni, Eq ann) => Eq (Type tyname uni ann) where
     ty1 == ty2 = runEqRename @TypeRenaming $ eqTypeM ty1 ty2
 
 instance
         ( HasUniques (Term tyname name uni fun ann)
-        , GEq uni, Closed uni, uni `Everywhere` Eq, Eq fun
+        , GEq uni, Closed uni, uni `Everywhere` Eq, Eq fun, Eq ann
         ) => Eq (Term tyname name uni fun ann) where
     term1 == term2 = runEqRename $ eqTermM term1 term2
 
-instance
-        ( HasUniques (Program tyname name uni fun ann)
-        , GEq uni, Closed uni, uni `Everywhere` Eq, Eq fun
-        ) => Eq (Program tyname name uni fun ann) where
-    prog1 == prog2 = runEqRename $ eqProgramM prog1 prog2
-
 type EqRenameOf ren a = HasUniques a => a -> a -> EqRename ren
 
 -- 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) => EqRenameOf ren (Type tyname uni ann)
-eqTypeM (TyVar _ name1) (TyVar _ name2) =
+eqTypeM :: (HasRenaming ren TypeUnique, GEq uni, Eq ann) => EqRenameOf ren (Type tyname uni ann)
+eqTypeM (TyVar ann1 name1) (TyVar ann2 name2) = do
+    eqM ann1 ann2
     eqNameM name1 name2
-eqTypeM (TyLam _ name1 kind1 ty1) (TyLam _ name2 kind2 ty2) = do
+eqTypeM (TyLam ann1 name1 kind1 ty1) (TyLam ann2 name2 kind2 ty2) = do
+    eqM ann1 ann2
     eqM kind1 kind2
     withTwinBindings name1 name2 $ eqTypeM ty1 ty2
-eqTypeM (TyForall _ name1 kind1 ty1) (TyForall _ name2 kind2 ty2) = do
+eqTypeM (TyForall ann1 name1 kind1 ty1) (TyForall ann2 name2 kind2 ty2) = do
+    eqM ann1 ann2
     eqM kind1 kind2
     withTwinBindings name1 name2 $ eqTypeM ty1 ty2
-eqTypeM (TyIFix _ pat1 arg1) (TyIFix _ pat2 arg2) = do
+eqTypeM (TyIFix ann1 pat1 arg1) (TyIFix ann2 pat2 arg2) = do
+    eqM ann1 ann2
     eqTypeM pat1 pat2
     eqTypeM arg1 arg2
-eqTypeM (TyApp _ fun1 arg1) (TyApp _ fun2 arg2) = do
+eqTypeM (TyApp ann1 fun1 arg1) (TyApp ann2 fun2 arg2) = do
+    eqM ann1 ann2
     eqTypeM fun1 fun2
     eqTypeM arg1 arg2
-eqTypeM (TyFun _ dom1 cod1) (TyFun _ dom2 cod2) = do
+eqTypeM (TyFun ann1 dom1 cod1) (TyFun ann2 dom2 cod2) = do
+    eqM ann1 ann2
     eqTypeM dom1 dom2
     eqTypeM cod1 cod2
-eqTypeM (TyBuiltin _ bi1) (TyBuiltin _ bi2) =
+eqTypeM (TyBuiltin ann1 bi1) (TyBuiltin ann2 bi2) = do
+    eqM ann1 ann2
     eqM bi1 bi2
 eqTypeM TyVar{}     _ = empty
 eqTypeM TyLam{}     _ = empty
@@ -90,33 +79,43 @@ eqTypeM TyBuiltin{} _ = empty
 -- See Note [No catch-all].
 -- | Check equality of two 'Term's.
 eqTermM
-    :: (GEq uni, Closed uni, uni `Everywhere` Eq, Eq fun)
+    :: (GEq uni, Closed uni, uni `Everywhere` Eq, Eq fun, Eq ann)
     => EqRenameOf ScopedRenaming (Term tyname name uni fun ann)
-eqTermM (LamAbs _ name1 ty1 body1) (LamAbs _ name2 ty2 body2) = do
+eqTermM (LamAbs ann1 name1 ty1 body1) (LamAbs ann2 name2 ty2 body2) = do
+    eqM ann1 ann2
     eqTypeM ty1 ty2
     withTwinBindings name1 name2 $ eqTermM body1 body2
-eqTermM (TyAbs _ name1 kind1 body1) (TyAbs _ name2 kind2 body2) = do
+eqTermM (TyAbs ann1 name1 kind1 body1) (TyAbs ann2 name2 kind2 body2) = do
+    eqM ann1 ann2
     eqM kind1 kind2
     withTwinBindings name1 name2 $ eqTermM body1 body2
-eqTermM (IWrap _ pat1 arg1 term1) (IWrap _ pat2 arg2 term2) = do
+eqTermM (IWrap ann1 pat1 arg1 term1) (IWrap ann2 pat2 arg2 term2) = do
+    eqM ann1 ann2
     eqTypeM pat1 pat2
     eqTypeM arg1 arg2
     eqTermM term1 term2
-eqTermM (Apply _ fun1 arg1) (Apply _ fun2 arg2) = do
+eqTermM (Apply ann1 fun1 arg1) (Apply ann2 fun2 arg2) = do
+    eqM ann1 ann2
     eqTermM fun1 fun2
     eqTermM arg1 arg2
-eqTermM (Unwrap _ term1) (Unwrap _ term2) =
+eqTermM (Unwrap ann1 term1) (Unwrap ann2 term2) = do
+    eqM ann1 ann2
     eqTermM term1 term2
-eqTermM (Error _ ty1) (Error _ ty2) =
+eqTermM (Error ann1 ty1) (Error ann2 ty2) = do
+    eqM ann1 ann2
     eqTypeM ty1 ty2
-eqTermM (TyInst _ term1 ty1) (TyInst _ term2 ty2) = do
+eqTermM (TyInst ann1 term1 ty1) (TyInst ann2 term2 ty2) = do
+    eqM ann1 ann2
     eqTermM term1 term2
     eqTypeM ty1 ty2
-eqTermM (Var _ name1) (Var _ name2) =
+eqTermM (Var ann1 name1) (Var ann2 name2) = do
+    eqM ann1 ann2
     eqNameM name1 name2
-eqTermM (Constant _ con1) (Constant _ con2) =
+eqTermM (Constant ann1 con1) (Constant ann2 con2) = do
+    eqM ann1 ann2
     eqM con1 con2
-eqTermM (Builtin _ bi1) (Builtin _ bi2) =
+eqTermM (Builtin ann1 bi1) (Builtin ann2 bi2) = do
+    eqM ann1 ann2
     eqM bi1 bi2
 eqTermM LamAbs{}   _ = empty
 eqTermM TyAbs{}    _ = empty
@@ -129,10 +128,6 @@ eqTermM Var{}      _ = empty
 eqTermM Constant{} _ = empty
 eqTermM Builtin{}  _ = empty
 
--- | Check equality of two 'Program's.
-eqProgramM
-    :: (GEq uni, Closed uni, uni `Everywhere` Eq, Eq fun)
-    => EqRenameOf ScopedRenaming (Program tyname name uni fun ann)
-eqProgramM (Program _ ver1 term1) (Program _ ver2 term2) = do
-    guard $ ver1 == ver2
-    eqTermM term1 term2
+deriving instance (HasUniques (Term tyname name uni fun ann)
+                  , GEq uni, Closed uni, uni `Everywhere` Eq, Eq fun, Eq ann
+                  ) =>  Eq (Program tyname name uni fun ann)

plutus-core/plutus-core/src/PlutusCore/Core/Type.hs

@@ -54,15 +54,10 @@ import Instances.TH.Lift ()
 import Language.Haskell.TH.Lift
 import Universe
 
-{- Note [Annotations and equality]
-Equality of two things does not depend on their annotations.
-So don't use @deriving Eq@ for things with annotations.
--}
-
 data Kind ann
     = Type ann
     | KindArrow ann (Kind ann) (Kind ann)
-    deriving (Show, Functor, Generic, NFData, Lift, Hashable)
+    deriving (Eq, Show, Functor, Generic, NFData, Lift, Hashable)
 
 -- | A 'Type' assigned to expressions.
 type Type :: GHC.Type -> (GHC.Type -> GHC.Type) -> GHC.Type -> GHC.Type
@@ -93,7 +88,7 @@ data Term tyname name uni fun ann
 -- | Version of Plutus Core to be used for the program.
 data Version ann
     = Version ann Natural Natural Natural
-    deriving (Show, Functor, Generic, NFData, Hashable)
+    deriving (Eq, Show, Functor, Generic, NFData, Hashable)
 
 -- | A 'Program' is simply a 'Term' coupled with a 'Version' of the core language.
 data Program tyname name uni fun ann = Program ann (Version ann) (Term tyname name uni fun ann)

plutus-core/plutus-core/src/PlutusCore/Error.hs

@@ -46,14 +46,6 @@ import Prettyprinter.Internal (Doc (Text))
 import Text.Megaparsec.Pos (SourcePos, sourcePosPretty)
 import Universe (Closed (Everywhere), GEq, GShow)
 
-{- Note [Annotations and equality]
-Equality of two errors DOES DEPEND on their annotations.
-So feel free to use @deriving Eq@ for errors.
-This is because even though we do care about errors having an 'Eq' instance (which is required for
-example by tests that do checks like @resOrErr == Right res@), we don't care much about actually
-checking errors for equality and @deriving Eq@ saves us a lot of boilerplate.
--}
-
 -- | Lifts an 'Either' into an error context where we can embed the 'Left' value into the error.
 throwingEither :: MonadError e m => AReview e t -> Either t a -> m a
 throwingEither r e = case e of

plutus-core/plutus-ir/src/PlutusIR/TypeCheck/Internal.hs

@@ -312,8 +312,8 @@ checkTypeFromBinding recurs = \case
        checkConRes :: Type TyName uni a -> PirTCEnv uni fun e ()
        checkConRes ty =
            -- We earlier checked that datacons' type is *-kinded (using checkKindBinding), but this is not enough:
-           -- we must also check that its result type is EXACTLY `[[TypeCon tyarg1] ... tyargn]`
-           when (funResultType ty /= appliedTyCon) .
+           -- we must also check that its result type is EXACTLY `[[TypeCon tyarg1] ... tyargn]` (ignoring annotations)
+           when (void (funResultType ty) /= void appliedTyCon) .
                throwing _TypeErrorExt $ MalformedDataConstrResType ann appliedTyCon
 
        -- if nonrec binding, make sure that type-constructor is not part of the data-constructor's argument types.

plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Core/Instance/Eq.hs

@@ -15,30 +15,37 @@ import PlutusCore.Rename.Monad
 
 import Universe
 
-instance (GEq uni, Closed uni, uni `Everywhere` Eq, Eq fun, HasUnique name TermUnique) =>
+instance (GEq uni, Closed uni, uni `Everywhere` Eq, Eq fun, HasUnique name TermUnique, Eq ann) =>
             Eq (Term name uni fun ann) where
     term1 == term2 = runEqRename $ eqTermM term1 term2
 
 -- | Check equality of two 'Term's.
 eqTermM
-    :: (GEq uni, Closed uni, uni `Everywhere` Eq, Eq fun, HasUnique name TermUnique)
+    :: (GEq uni, Closed uni, uni `Everywhere` Eq, Eq fun, Eq ann, HasUnique name TermUnique)
     => Term name uni fun ann -> Term name uni fun ann -> EqRename (Renaming TermUnique)
-eqTermM (Constant _ con1) (Constant _ con2) =
+eqTermM (Constant ann1 con1) (Constant ann2 con2) = do
+    eqM ann1 ann2
     eqM con1 con2
-eqTermM (Builtin _ bi1) (Builtin _ bi2) =
+eqTermM (Builtin ann1 bi1) (Builtin ann2 bi2) = do
+    eqM ann1 ann2
     eqM bi1 bi2
-eqTermM (Var _ name1) (Var _ name2) =
+eqTermM (Var ann1 name1) (Var ann2 name2) = do
+    eqM ann1 ann2
     eqNameM name1 name2
-eqTermM (LamAbs _ name1 body1) (LamAbs _ name2 body2) =
+eqTermM (LamAbs ann1 name1 body1) (LamAbs ann2 name2 body2) = do
+    eqM ann1 ann2
     withTwinBindings name1 name2 $ eqTermM body1 body2
-eqTermM (Apply _ fun1 arg1) (Apply _ fun2 arg2) = do
+eqTermM (Apply ann1 fun1 arg1) (Apply ann2 fun2 arg2) = do
+    eqM ann1 ann2
     eqTermM fun1 fun2
     eqTermM arg1 arg2
-eqTermM (Delay _ term1) (Delay _ term2) =
+eqTermM (Delay ann1 term1) (Delay ann2 term2) = do
+    eqM ann1 ann2
     eqTermM term1 term2
-eqTermM (Force _ term1) (Force _ term2) =
+eqTermM (Force ann1 term1) (Force ann2 term2) = do
+    eqM ann1 ann2
     eqTermM term1 term2
-eqTermM (Error _) (Error _) = pure ()
+eqTermM (Error ann1) (Error ann2) = eqM ann1 ann2
 eqTermM Constant{} _ = empty
 eqTermM Builtin{}  _ = empty
 eqTermM Var{}      _ = empty