Hello! I'm having a lot of trouble writing a Data.GADT.Compare.GEq instance - can anyone help me fill in the blank? For context - I'm generating Tag types automatically for using with DSum, and I need a GEq instance. That's part of an attempt to add efficient rendering of sum types to Reflex/Reflex-Dom (https://github.com/anderspapitto/reflex-sumtype- render/blob/master/src/ReflexHelpers.hs). I put this question on stackoverflow as well a day ago ( http://stackoverflow.com/questions/40698207/how-can-i- write-this-geq-instance). Here's the code (it's a full, standalone file - you can copy it into Foo.hs and run ghc to see the full error I'm facing). The error I get is that when I try to recursively call geq on the unwrapped x and y, I can't because ghc considers them to have different types - Quux a and Quux b. However, the whole point of why I'm trying to call geq is to see if a and b are the same, so I'm pretty confused. Note that I'm making use of the generics-sop library, which is where NP and NS and I come from. {-# LANGUAGE GADTs #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE RankNTypes #-} module Foo where import Data.GADT.Compare import Generics.SOP import qualified GHC.Generics as GHC data Quux i xs where Quux :: Quux (NP I xs) xs newtype GTag t i = GTag { unTag :: NS (Quux i) (Code t) } instance GEq (GTag t) where -- I don't know how to do this geq (GTag (S x)) (GTag (S y)) = let _ = x `geq` y in undefined