[Haskell-cafe] difficulty writing GEq instance

[Oleg Grenrus]

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 <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 <anderspapitto at gmail.com> 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/anderspapitto/reflex-sumtype-render/blob/master/src/ReflexHelpers.hs <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 <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.

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20161120/7c97be77/attachment.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 842 bytes
Desc: Message signed with OpenPGP using GPGMail
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20161120/7c97be77/attachment.sig>