[Haskell-cafe] difficulty writing GEq instance

[Anders Papitto]

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 <oleg.grenrus at iki.fi> 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 <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/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.
>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20161120/c0dee909/attachment.html>