Thanks Oleg. Could you expand on that a little more? I've read your post and tried a few things, but I'm still unable to write the instance (either for the original version I had, or for your modified version). This is all pretty new to me, so I can't quite follow the jump from your hint to a full typechecking solution. In particular, trying to compile this snippet gives the same error as I was facing originally - I'm still not able to recurse with geq x y. newtype OlegTag xs a = OlegTag { unTag :: NS ((:~:) a) xs } instance GEq (OlegTag xs) where geq (OlegTag (Z x)) (OlegTag (Z y)) = case x `geq` y of _ -> undefined On Sun, Nov 20, 2016 at 10:37 AM, Oleg Grenrus wrote:

I was just writing a blog post related to that.

You’d need to use

newtype GTag xs a = GTag { unTag :: NS ((:~:) a) xs }

Then you can recover needed type equality.

https://gist.github.com/phadej/bfdffc3bd5ba6ce4f586bb988a8d399c

Alternatively: You could use `NS Proxy xs`, but than it’s much easier to make a mistake.

- Oleg

On 20 Nov 2016, at 19:27, Anders Papitto wrote:

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/anderspapi tto/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 _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.