<html><head><meta http-equiv="Content-Type" content="text/html charset=utf-8"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;" class="">I was just writing a blog post related to that.<div class=""><br class=""></div><div class="">You’d need to use</div><div class=""><br class=""></div><div class="">newtype GTag xs a = GTag { unTag :: NS ((:~:) a) xs }</div><div class=""><br class=""></div><div class="">Then you can recover needed type equality.</div><div class=""><br class=""></div><div class=""><a href="https://gist.github.com/phadej/bfdffc3bd5ba6ce4f586bb988a8d399c" class="">https://gist.github.com/phadej/bfdffc3bd5ba6ce4f586bb988a8d399c</a></div><div class=""><br class=""></div><div class="">Alternatively:</div><div class="">You could use `NS Proxy xs`, but than it’s much easier to make a mistake.</div><div class=""><br class=""></div><div class="">- Oleg<br class=""><div class=""><br class=""></div><div class=""><br class=""></div><div class=""><br class=""><div><blockquote type="cite" class=""><div class="">On 20 Nov 2016, at 19:27, Anders Papitto <<a href="mailto:anderspapitto@gmail.com" class="">anderspapitto@gmail.com</a>> wrote:</div><br class="Apple-interchange-newline"><div class=""><div dir="ltr" class=""><div class=""><div class="">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 (<a href="https://github.com/anderspapitto/reflex-sumtype-render/blob/master/src/ReflexHelpers.hs" target="_blank" class="">https://github.com/<wbr class="">anderspapitto/reflex-sumtype-<wbr class="">render/blob/master/src/<wbr class="">ReflexHelpers.hs</a>).<br class=""><br class=""></div><div class="">I put this question on stackoverflow as well a day ago (<a href="http://stackoverflow.com/questions/40698207/how-can-i-write-this-geq-instance" target="_blank" class="">http://stackoverflow.com/<wbr class="">questions/40698207/how-can-i-<wbr class="">write-this-geq-instance</a>).<br class=""></div><div class=""><br class=""></div>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.<br class=""><br class=""></div>Note that I'm making use of the generics-sop library, which is where NP and NS and I come from.<br class=""><br class=""><span style="font-family:monospace,monospace" class="">{-# LANGUAGE GADTs #-}<br class="">{-# LANGUAGE DataKinds #-}<br class="">{-# LANGUAGE TypeOperators #-}<br class="">{-# LANGUAGE KindSignatures #-}<br class="">{-# LANGUAGE RankNTypes #-}<br class=""><br class="">module Foo where<br class=""><br class="">import Data.GADT.Compare<br class="">import Generics.SOP<br class="">import qualified GHC.Generics as GHC<br class=""><br class="">data Quux i xs where Quux :: Quux (NP I xs) xs<br class=""><br class="">newtype GTag t i = GTag { unTag :: NS (Quux i) (Code t) }<br class=""><br class="">instance GEq (GTag t) where<br class=""> -- I don't know how to do this<br class=""> geq (GTag (S x)) (GTag (S y)) =<br class=""> let _ = x `geq` y<br class=""> in undefined</span></div>
_______________________________________________<br class="">Haskell-Cafe mailing list<br class="">To (un)subscribe, modify options or view archives go to:<br class=""><a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe" class="">http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe</a><br class="">Only members subscribed via the mailman list are allowed to post.</div></blockquote></div><br class=""></div></div></body></html>