<div dir="ltr"><div>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.<br><br></div>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.<br><br><span style="font-family:monospace,monospace">newtype OlegTag xs a = OlegTag { unTag :: NS ((:~:) a) xs }<br><br>instance GEq (OlegTag xs) where<br> geq (OlegTag (Z x)) (OlegTag (Z y)) =<br> case x `geq` y of _ -> undefined<br><br></span><br></div><div class="gmail_extra"><br><div class="gmail_quote">On Sun, Nov 20, 2016 at 10:37 AM, Oleg Grenrus <span dir="ltr"><<a href="mailto:oleg.grenrus@iki.fi" target="_blank">oleg.grenrus@iki.fi</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div style="word-wrap:break-word">I was just writing a blog post related to that.<div><br></div><div>You’d need to use</div><div><br></div><div>newtype GTag xs a = GTag { unTag :: NS ((:~:) a) xs }</div><div><br></div><div>Then you can recover needed type equality.</div><div><br></div><div><a href="https://gist.github.com/phadej/bfdffc3bd5ba6ce4f586bb988a8d399c" target="_blank">https://gist.github.com/<wbr>phadej/<wbr>bfdffc3bd5ba6ce4f586bb988a8d39<wbr>9c</a></div><div><br></div><div>Alternatively:</div><div>You could use `NS Proxy xs`, but than it’s much easier to make a mistake.</div><div><br></div><div>- Oleg<br><div><br></div><div><br></div><div><br><div><blockquote type="cite"><div><div class="h5"><div>On 20 Nov 2016, at 19:27, Anders Papitto <<a href="mailto:anderspapitto@gmail.com" target="_blank">anderspapitto@gmail.com</a>> wrote:</div><br class="m_2786706731787213254Apple-interchange-newline"></div></div><div><div><div class="h5"><div dir="ltr"><div><div>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">https://github.com/anderspapi<wbr>tto/reflex-sumtype-render/<wbr>blob/master/src/ReflexHelpers.<wbr>hs</a>).<br><br></div><div>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">http://stackoverflow.com/ques<wbr>tions/40698207/how-can-i-write<wbr>-this-geq-instance</a>).<br></div><div><br></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><br></div>Note that I'm making use of the generics-sop library, which is where NP and NS and I come from.<br><br><span style="font-family:monospace,monospace">{-# LANGUAGE GADTs #-}<br>{-# LANGUAGE DataKinds #-}<br>{-# LANGUAGE TypeOperators #-}<br>{-# LANGUAGE KindSignatures #-}<br>{-# LANGUAGE RankNTypes #-}<br><br>module Foo where<br><br>import Data.GADT.Compare<br>import Generics.SOP<br>import qualified GHC.Generics as GHC<br><br>data Quux i xs where Quux :: Quux (NP I xs) xs<br><br>newtype GTag t i = GTag { unTag :: NS (Quux i) (Code t) }<br><br>instance GEq (GTag t) where<br> -- I don't know how to do this<br> geq (GTag (S x)) (GTag (S y)) =<br> let _ = x `geq` y<br> in undefined</span></div></div></div>
______________________________<wbr>_________________<br>Haskell-Cafe mailing list<br>To (un)subscribe, modify options or view archives go to:<br><a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe" target="_blank">http://mail.haskell.org/cgi-<wbr>bin/mailman/listinfo/haskell-<wbr>cafe</a><br>Only members subscribed via the mailman list are allowed to post.</div></blockquote></div><br></div></div></div></blockquote></div><br></div>