How can I write this GEq instance?

Question

I have datatypes Tup2List and GTag (from the answer to How can I produce a Tag type for any datatype for use with DSum, without Template Haskell?)

I want to write a GEq instance for GTag t, which I think requires also having one for Tup2List. How can I write this instance?

My guess at why it doesn't work is because there's no such thing as a partial Refl - you need to match the whole structure all at once for the compiler to give you the Refl, whereas I'm trying to just unwrap the outermost constructor and then recurse.

Here's my code, with undefined filling in for the parts I don't know how to write.

{-# 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 Tup2List :: * -> [*] -> * where
  Tup0 :: Tup2List () '[]
  Tup1 :: Tup2List x '[ x ]
  TupS :: Tup2List r (x ': xs) -> Tup2List (a, r) (a ': x ': xs)

instance GEq (Tup2List t) where
  geq Tup0     Tup0     = Just Refl
  geq Tup1     Tup1     = Just Refl
  geq (TupS x) (TupS y) = 
    case x `geq` y of
      Just Refl -> Just Refl
      Nothing   -> Nothing

newtype GTag t i = GTag { unTag :: NS (Tup2List i) (Code t) }

instance GEq (GTag t) where
  geq (GTag (Z x)) (GTag (Z y)) = undefined -- x `geq` y
  geq (GTag (S _)) (GTag (Z _)) = Nothing
  geq (GTag (Z _)) (GTag (S _)) = Nothing
  geq (GTag (S x)) (GTag (S y)) = undefined -- x `geq` y

EDIT: I've changed my datatypes around, but i'm still facing the same core problem. The current definitions are

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)) = undefined

Answer 1

Here's my take on this. Personally, I don't see much point in allowing to derive a tag type for sum types which have 0 or more than one field, so I'm going to simplify Tup2List away. Its presence is orthogonal to the question at hand.

So I'm going to define GTag as follows:

type GTag t = GTag_ (Code t)
newtype GTag_ t a = GTag { unGTag :: NS ((:~:) '[a]) t }

pattern P0 :: () => (ys ~ ('[t] ': xs)) => GTag_ ys t
pattern P0 = GTag (Z Refl)

pattern P1 :: () => (ys ~ (x0 ': '[t] ': xs)) => GTag_ ys t
pattern P1 = GTag (S (Z Refl))

pattern P2 :: () => (ys ~ (x0 ': x1 ': '[t] ': xs)) => GTag_ ys t
pattern P2 = GTag (S (S (Z Refl)))

pattern P3 :: () => (ys ~ (x0 ': x1 ': x2 ': '[t] ': xs)) => GTag_ ys t
pattern P3 = GTag (S (S (S (Z Refl))))

pattern P4 :: () => (ys ~ (x0 ': x1 ': x2 ': x3 ': '[t] ': xs)) => GTag_ ys t
pattern P4 = GTag (S (S (S (S (Z Refl)))))

The main difference is to define GTag_ without an occurrence of Code. This will make recursion easier, because you don't get a requirement that the recursive case has to be expressible as an application of Code again.

The secondary difference, as mentioned before, is the use of (:~:) '[a] to force single-argument constructors rather than the more complicated Tup2List.

Here's a variant of your original example:

data SomeUserType = Foo Int | Bar Char | Baz (Bool, String)
  deriving (GHC.Generic)

instance Generic SomeUserType

The argument of Baz is now written a a pair explicitly, to adhere to the "single argument" requirement.

Example dependent sums:

ex1, ex2, ex3 :: DSum (GTag SomeUserType) Maybe
ex1 = P0 ==> 3
ex2 = P1 ==> 'x'
ex3 = P2 ==> (True, "foo")

Now the instances:

instance GShow (GTag_ t) where
  gshowsPrec _n = go 0
    where
      go :: Int -> GTag_ t a -> ShowS
      go k (GTag (Z Refl)) = showString ("P" ++ show k)
      go k (GTag (S i))    = go (k + 1) (GTag i)

instance All2 (Compose Show f) t => ShowTag (GTag_ t) f where
  showTaggedPrec (GTag (Z Refl)) = showsPrec
  showTaggedPrec (GTag (S i))    = showTaggedPrec (GTag i)

instance GEq (GTag_ t) where
  geq (GTag (Z Refl)) (GTag (Z Refl)) = Just Refl
  geq (GTag (S i))    (GTag (S j))    = geq (GTag i) (GTag j)
  geq _               _               = Nothing

instance All2 (Compose Eq f) t => EqTag (GTag_ t) f where
  eqTagged (GTag (Z Refl)) (GTag (Z Refl)) = (==)
  eqTagged (GTag (S i))    (GTag (S j))    = eqTagged (GTag i) (GTag j)
  eqTagged _               _               = \ _ _ -> False

And some examples of their use:

GHCi> (ex1, ex2, ex3)
(P0 :=> Just 3,P1 :=> Just 'x',P2 :=> Just (True,"foo"))
GHCi> ex1 == ex1
True
GHCi> ex1 == ex2
False