[Haskell-cafe] difficulty writing GEq instance

[Anders Papitto]

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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20161120/2cd51f72/attachment.html>