Merge pull request #353 from well-typed/rm-hs-eq-instances

Remove Eq instances for Hs AST (#351)

hs-bindgen/src/HsBindgen/Hs/AST.hs

@@ -64,21 +64,15 @@ module HsBindgen.Hs.AST (
 
 import HsBindgen.C.AST qualified as C
 import HsBindgen.C.Tc.Macro qualified as C
-import Data.GADT.Compare (GEq(geq), defaultEq)
-import Data.Type.Equality ((:~:)(Refl))
 import Data.Type.Nat as Nat
-import Data.Vec.Lazy qualified as Vec
-import Unsafe.Coerce (unsafeCoerce)
 
 import HsBindgen.Imports
 import HsBindgen.NameHint
 import HsBindgen.Hs.AST.Name
 import HsBindgen.Hs.AST.Type
 import HsBindgen.Orphans ()
-import HsBindgen.Util.TestEquality
 
 import DeBruijn
-import DeBruijn.Internal.Add (Add(UnsafeAdd))
 
 {-------------------------------------------------------------------------------
   Information about generated code
@@ -89,40 +83,39 @@ data Field = Field {
     , fieldType   :: HsType
     , fieldOrigin :: FieldOrigin
     }
-  deriving stock (Eq, Generic, Show)
+  deriving stock (Generic, Show)
 
 data FieldOrigin =
       FieldOriginNone
     | FieldOriginStructField C.StructField
-  deriving stock (Eq, Generic, Show)
+  deriving stock (Generic, Show)
 
 data Struct (n :: Nat) = Struct {
       structName   :: HsName NsTypeConstr
     , structConstr :: HsName NsConstr
     , structFields :: Vec n Field
     , structOrigin :: StructOrigin
     }
-  deriving stock (Eq, Generic, Show)
-  deriving GEq via ApEq Struct
+  deriving stock (Generic, Show)
 
 data StructOrigin =
       StructOriginStruct C.Struct
     | StructOriginEnum C.Enu
-  deriving stock (Eq, Generic, Show)
+  deriving stock (Generic, Show)
 
 data Newtype = Newtype {
       newtypeName   :: HsName NsTypeConstr
     , newtypeConstr :: HsName NsConstr
     , newtypeField  :: Field
     , newtypeOrigin :: NewtypeOrigin
     }
-  deriving stock (Eq, Generic, Show)
+  deriving stock (Generic, Show)
 
 data NewtypeOrigin =
       NewtypeOriginEnum C.Enu
     | NewtypeOriginTypedef C.Typedef
     | NewtypeOriginMacro C.Macro
-  deriving stock (Eq, Generic, Show)
+  deriving stock (Generic, Show)
 
 data ForeignImportDecl = ForeignImportDecl
     { foreignImportName       :: HsName NsVar
@@ -131,11 +124,11 @@ data ForeignImportDecl = ForeignImportDecl
     , foreignImportHeader     :: FilePath -- TODO: https://github.com/well-typed/hs-bindgen/issues/333
     , foreignImportDeclOrigin :: ForeignImportDeclOrigin
     }
-  deriving stock (Eq, Generic, Show)
+  deriving stock (Generic, Show)
 
 newtype ForeignImportDeclOrigin =
       ForeignImportDeclOriginFunction C.Function
-  deriving stock (Eq, Generic, Show)
+  deriving stock (Generic, Show)
 
 {-------------------------------------------------------------------------------
   Variable binding
@@ -147,13 +140,12 @@ data Lambda t ctx = Lambda
     NameHint  -- ^ name suggestion
     (t (S ctx)) -- ^ body
 
-deriving instance Eq   (t (S ctx)) => Eq   (Lambda t ctx)
 deriving instance Show (t (S ctx)) => Show (Lambda t ctx)
 
 -- | Applicative structure
 
 data Ap pure xs ctx = Ap (pure ctx) [xs ctx]
-  deriving stock (Eq, Generic, Show)
+  deriving stock (Generic, Show)
 
 {-------------------------------------------------------------------------------
   Declarations
@@ -173,22 +165,10 @@ data Decl where
 
 deriving instance Show Decl
 
-instance Eq Decl where
-  DeclData l == DeclData r = l `defaultEq` r
-  DeclEmpty l == DeclEmpty r = l == r
-  DeclNewtype l == DeclNewtype r = l == r
-  DeclPatSyn l == DeclPatSyn r = l == r
-  DeclInstance l == DeclInstance r = l == r
-  DeclNewtypeInstance tcL nameL == DeclNewtypeInstance tcR nameR =
-    tcL == tcR && nameL == nameR
-  DeclForeignImport l == DeclForeignImport r = l == r
-  DeclVar l == DeclVar r = l == r
-  _l == _r = False
-
 -- | Class instance names
 data TypeClass =
     Storable
-  deriving stock (Eq, Generic, Show)
+  deriving stock (Generic, Show)
 
 -- | Class instance declaration
 type InstanceDecl :: Star
@@ -197,10 +177,6 @@ data InstanceDecl where
 
 deriving instance Show InstanceDecl
 
-instance Eq InstanceDecl where
-  InstanceStorable sL iL == InstanceStorable sR iR =
-    sL `defaultEq` sR && iL == iR
-
 -- | Variable or function declaration.
 type VarDecl :: Star
 data VarDecl =
@@ -212,7 +188,7 @@ data VarDecl =
     -- | RHS of variable/function.
     , varDeclBody :: VarDeclRHS EmptyCtx
     }
-  deriving stock (Eq, Generic, Show)
+  deriving stock (Generic, Show)
 
 -- | A σ-type, of the form @forall tvs. ctxt => body@.
 type SigmaType :: Star
@@ -226,51 +202,33 @@ data SigmaType where
 
 deriving stock instance Show SigmaType
 
-instance Eq SigmaType where
-  ForallTy sL vL pL == ForallTy sR vR pR =
-    fromMaybe False $ do
-      Refl <- geqVec vL vR
-      return $ sL == sR && pL == pR
-
 -- | A φ-type, of the form @ctxt => body@.
 type PhiType :: Ctx -> Star
 data PhiType ctx
   = QuantTy
   { quantTyCts  :: [ClassTy ctx]
   , quantTyBody :: TauType ctx
   }
-  deriving stock (Eq, Generic, Show)
+  deriving stock (Generic, Show)
 
 -- | A τ-type: no quantification or contexts (i.e. no @forall@, no @=>@ arrows).
 type TauType :: Ctx -> Star
 data TauType ctx
   = FunTy (TauType ctx) (TauType ctx)
   | TyVarTy (Idx ctx)
   | TyConAppTy (TyConAppTy ctx)
-  deriving stock (Eq, Generic, Show)
+  deriving stock (Generic, Show)
 
 data TyConAppTy ctx where
   TyConApp :: C.DataTyCon arity -> Vec arity (TauType ctx) -> TyConAppTy ctx
 
 deriving stock instance Show (TyConAppTy ctx)
 
-instance Eq (TauType ctx) => Eq (TyConAppTy ctx) where
-  TyConApp dL vL == TyConApp dR vR =
-    fromMaybe False $ do
-      Refl <- geqVec vL vR
-      return $ dL == dR
-
 data ClassTy ctx where
   ClassTy :: C.ClassTyCon arity -> Vec arity (TauType ctx) -> ClassTy ctx
 
 deriving stock instance Show (ClassTy ctx)
 
-instance Eq (TauType ctx) => Eq (ClassTy ctx) where
-  ClassTy cL vL == ClassTy cR vR =
-    fromMaybe False $ do
-      Refl <- geqVec vL vR
-      return $ cL == cR
-
 -- | RHS of a variable or function declaration.
 type VarDeclRHS :: Ctx -> Star
 data VarDeclRHS ctx
@@ -280,7 +238,7 @@ data VarDeclRHS ctx
   | VarDeclLambda (Lambda VarDeclRHS ctx)
   | VarDeclApp VarDeclRHSAppHead [VarDeclRHS ctx]
   | VarDeclVar (Idx ctx)
-  deriving stock (Eq, Generic, Show)
+  deriving stock (Generic, Show)
 
 -- | The function at the head of an application in the Haskell translation
 -- of a C macro.
@@ -292,11 +250,6 @@ data VarDeclRHSAppHead
 
 deriving stock instance Show VarDeclRHSAppHead
 
-instance Eq VarDeclRHSAppHead where
-  InfixAppHead l == InfixAppHead r = l `defaultEq` r
-  VarAppHead l == VarAppHead r = l == r
-  _l == _r = False
-
 {-------------------------------------------------------------------------------
   Pattern Synonyms
 -------------------------------------------------------------------------------}
@@ -317,11 +270,11 @@ data PatSyn = PatSyn
     , patSynValue  :: Integer
     , patSynOrigin :: PatSynOrigin
     }
-  deriving stock (Eq, Generic, Show)
+  deriving stock (Generic, Show)
 
 newtype PatSynOrigin =
       PatSynOriginEnumValue C.EnumValue
-  deriving stock (Eq, Generic, Show)
+  deriving stock (Generic, Show)
 
 {-------------------------------------------------------------------------------
   'Storable'
@@ -339,7 +292,7 @@ data StorableInstance = StorableInstance
     , storablePeek      :: Lambda (Ap StructCon PeekByteOff) EmptyCtx
     , storablePoke      :: Lambda (Lambda (ElimStruct (Seq PokeByteOff))) EmptyCtx
     }
-  deriving stock (Eq, Generic, Show)
+  deriving stock (Generic, Show)
 
 -- | Call to 'peekByteOff'
 --
@@ -348,22 +301,22 @@ type PeekByteOff :: Ctx -> Star
 data PeekByteOff ctx = PeekByteOff
     (Idx ctx)
     Int
-  deriving stock (Eq, Generic, Show)
+  deriving stock (Generic, Show)
 
 -- | Call to 'pokeByteOff'
 --
 -- <https://hackage.haskell.org/package/base/docs/Foreign-Storable.html#v:pokeByteOff>
 type PokeByteOff :: Ctx -> Star
 data PokeByteOff ctx = PokeByteOff (Idx ctx) Int (Idx ctx)
-  deriving stock (Eq, Generic, Show)
+  deriving stock (Generic, Show)
 
 {-------------------------------------------------------------------------------
   Statements
 -------------------------------------------------------------------------------}
 
 -- | Simple sequential composition (no bindings)
 newtype Seq t ctx = Seq [t ctx]
-  deriving stock (Eq, Generic, Show)
+  deriving stock (Generic, Show)
 
 {-------------------------------------------------------------------------------
   Structs
@@ -375,9 +328,6 @@ data StructCon ctx where
 
 deriving instance Show (StructCon ctx)
 
-instance Eq (StructCon ctx) where
-  StructCon sL == StructCon sR = sL `defaultEq` sR
-
 -- | Case split for a struct
 type ElimStruct :: (Ctx -> Star) -> (Ctx -> Star)
 data ElimStruct t ctx where
@@ -390,17 +340,6 @@ data ElimStruct t ctx where
 
 deriving instance (forall ctx'. Show (t ctx')) => Show (ElimStruct t ctx)
 
-instance (forall ctx'. (Eq (t ctx'))) => Eq (ElimStruct t ctx) where
-  ElimStruct idxL sL addL tL == ElimStruct idxR sR addR tR =
-      fromMaybe False $ do
-        Refl <- geq (ApEq sL) (ApEq sR)
-        Refl <- geq idxL idxR
-        case eqAdds addL addR of
-          Refl -> return $ tL == tR
-    where
-      eqAdds :: Add n m pL -> Add n m pR -> pL :~: pR
-      eqAdds (UnsafeAdd !_) (UnsafeAdd !_) = unsafeCoerce Refl
-
 -- | Create 'ElimStruct' using kind-of HOAS interface.
 makeElimStruct :: forall n ctx t.
      SNatI n
@@ -425,15 +364,3 @@ makeElimStruct' :: forall m ctx t.
 makeElimStruct' Nat.SZ      kont = kont AZ IdWk VNil
 makeElimStruct' (Nat.SS' n) kont = makeElimStruct' n $ \add wk xs ->
     kont (AS add) (SkipWk wk) (IZ ::: fmap IS xs)
-
-{-------------------------------------------------------------------------------
-  Auxiliary functions
--------------------------------------------------------------------------------}
-
-geqVec :: forall n m a. Eq a => Vec n a -> Vec m a -> Maybe (n :~: m)
-geqVec l r = Vec.withDict l $ Vec.withDict r $
-    case Nat.eqNat @n @m of
-      Just Refl
-        | l == r    -> Just Refl
-        | otherwise -> Nothing
-      Nothing       -> Nothing

hs-bindgen/src/HsBindgen/Hs/AST/Type.hs

@@ -52,5 +52,5 @@ data HsType =
   | HsFunPtr HsType
   | HsIO HsType
   | HsFun HsType HsType
-  deriving stock (Eq, Generic, Show)
+  deriving stock (Generic, Show)