How is it possible to discharge Show instance of Sigma?

[tomjaguarpaw]

Consider the program below. I think it's uncontroversial (although there's a possibility that I've misunderstood how Apply instances are supposed to be written). This is probably the simplest possible program of this sort, yet I don't see how I can show mySigma.

The error message mentions Show (Apply Id x) but what it really wants is forall (x :: ()). Show (Apply Id x) (via ShowApply/ShowApply'). I don't see how that can possibly be discharged.

Is there an example somewhere showing how this Show instance is supposed to be used in practice?

data SUnit (a :: ()) where
  MkSUnit :: SUnit '()

type instance Sing = SUnit

instance SingI '() where
  sing = MkSUnit

instance Show (SUnit a) where
  show MkSUnit = "MkSUnit"

type Id :: () ~> Type
data Id t = MkId

type instance Apply Id '() = ()

mySigma :: Sigma () Id
mySigma = MkSUnit :&: ()

example = show mySigma

---

test18.hs:111:11: error:
    • No instance for (Show (Apply Id x)) arising from a use of ‘show’
    • In the expression: show mySigma
      In an equation for ‘example’: example = show mySigma
    |
111 | example = show mySigma
    |           ^^^^^^^^^^^^

[RyanGlScott]

Yeah, this is admittedly somewhat unsatisfactory. I adapted the implementation of Sigma's Show instance from a trick that I use to define Show instances for singleton types, which is described at length here. In both types of Show instances, I have to discharge constraints that look like this:

forall a. Show (f a)

In the case of singleton types, f is something like SUnit, and it is quite easy to discharge a forall a. Show (SUnit a) constraint, since we can define a Show (SUnit a) instance with no other constraints on the a.

In the case of sigma types, however, f is something Apply Id. It's trickier to resolve a forall a. Show (Apply Id a) constraint, as we must be able to reduce Apply Id a to something Show-able without knowing what a is. That is not possible with the definition of Id that you give:

type instance Apply Id '() = ()

But note that if you change this code such that it no longer scrutinizes the second argument:

type instance Apply Id _ = ()

Then Apply Id a evaluates to () for all a, and then your code typechecks:

λ> example
"MkSUnit :&: ()"

But yes, this is rather limited in practice, since most type families will actually want to scrutinize the argument in some way, thereby defeating this trick. Sadly, I don't know of another way to define this Show instance.

[int-index]

without knowing what a is

Is this a necessary restriction? Sigma contains a singleton, so pattern matching on it should reveal what a is. Here's an idea. Define a helper class

type WithDict c = forall r. (c => r) -> r

class ConstraintFromSing c k t where
  constraintFromSing :: Proxy c -> Sing (a :: k) -> WithDict (c (t @@ fst))

The Show instance for Sigma s t could require ConstraintFromSing Show s t

- instance (ShowSing s, ShowApply t) => Show (Sigma s t) where
+ instance (ShowSing s, ConstraintFromSing Show s t) => Show (Sigma s t) where
    showsPrec p ((a :: Sing (fst :: s)) :&: b) = showParen (p >= 5) $
+     constraintFromSing (Proxy @Show) a $
      showsPrec 5 a . showString " :&: " . showsPrec 5 b
        :: ShowApply' t fst => ShowS

while the definition of SUnit would be accompanied by the following instance

instance c (t @@ '()) => ConstraintFromSing c () t where
  constraintFromSing _ MkSUnit cont = cont

This generalizes to other singleton types, I believe, e.g.

instance (c (t @@ True), c (t @@ False)) => ConstraintFromSing c Bool t where
  constraintFromSing _ STrue  cont = cont
  constraintFromSing _ SFalse cont = cont

I haven't tried to compile any of the above, but it might work.

[RyanGlScott]

That's quite clever. A bit of shame that we'd need to derive an instance of yet another type class for everything, but perhaps that can't be helped. (Unless there's a way to define ConstraintFromSing in terms of existing singletons classes, but I can't figure out a way to do so.)

[tomjaguarpaw]

Ah, it seems that it can work even if Apply scrutinises its argument, as long as it returns something uniform that can be universally shown, such as a GADT:

data Foo (a :: ()) where
  MkFoo :: Foo '()

type FooT :: () ~> Type
data FooT t = MkFooT

instance Show (Foo a) where
  show MkFoo = "MkFoo"

type instance Apply FooT t = Foo t

mySigma :: Sigma () FooT
mySigma = MkSUnit :&: MkFoo

example = show mySigma

[googleson78]

@tomjaguarpaw

Well, technically Apply isn't scrutinising its argument, so it can freely reduce, because it doesn't need to match on t. After that, we don't need to look at t, because Foo has a show regardless of what t is, so essentially nothing is forcing scrutinisation.

[tomjaguarpaw]

Instead of ConstraintFromSing Show s t could we have forall a. SingI a => Show (t @@ i)? We do something similar in our work codebase. It works mostly fine, except it would be useful if we had https://gitlab.haskell.org/ghc/ghc/-/issues/14822.

[tomjaguarpaw]

I see, fair enough, in which case the key is to return something with a universal Show instance. It turns out that's still too restrictive in practice, as generally you want to use it on something with a universal show instance constrained by SingI a =>.

[RyanGlScott]

Instead of ConstraintFromSing Show s t could we have forall a. SingI a => Show (t @@ i)? We do something similar in our work codebase.

Oh, that is an interesting idea. Can you write out a full Show instance for Sigma to demonstrate how this works? (I'm sure it's possible, but it's a bit tricky to use a quantified constraint with a type family such as @@ in the head of the constraint.)

It works mostly fine, except it would be useful if we had https://gitlab.haskell.org/ghc/ghc/-/issues/14822.

I'm not sure what you mean here. Can you elaborate a bit more?

[tomjaguarpaw]

Can you write out a full Show instance

Yes, you can do this:

class MyShow a where
  myshow :: a -> String

class c (f @@ i) => CApply c f i where

instance c (f @@ i) => CApply c f i where

instance
  forall t f.
  (ShowSing t, forall (a :: t). SingI a => CApply MyShow f a) =>
  MyShow (Sigma t f) where
  myshow ((s :: Sing i) :&: f) =
    show s ++ " " ++ withSingC @_ @(CApply MyShow f) @i s (myshow f)

withSingC ::
  forall t c i r.
  (forall (a :: t). SingI a => c a) =>
  Sing i ->
  (c i => r) ->
  r
withSingC = withSingI

At work we don't use Apply/@@, we just pay the cost of always using a newtype, which feels quite low relative to the cost of having to deal with Apply everywhere, because we're not doing any type level computation. Then we just have

type Some :: forall (t :: Type). (t -> Type) -> Type
data Some f where Some :: SingI i => f i -> Some f

instance (forall i. SingI i => Show (f i)) => Show (Some f) where
  show (Some f) = show f

I'm not sure what you mean here. Can you elaborate a bit more?

The problem with the quantified constraint, that GHC14822 would fix, is that it's really hard to dispatch the (forall i. SingI i => Show (f i)) constraint unless things are set up perfectly from the start. For example, consider the program below. GN and GN2 are two different newtypes of the same type family. GN has the "incorrect" context on its Show instance, Show (G i). This will cause problems later. GN2 has the "correct" context, SingI i. This won't cause any problems.

In cases where i is known I can convert from the "incorrect" to the "correct" context just by pattern matching on the SingI, as in showGN. But I can't recover the necessary context where i is universally quantified, for example in Show (Some GN). Even though I can create forall i. SingI i :- Show (GN i) there is no way of using this to conjure up the constraint forall i. SingI => Show (GN i). That's a big impediment to using quantified constraints! It means you need to have everything exactly lined up correctly ahead of time to be able to dispatch them.

---

data SBool (i :: Bool) where
  STrue :: SBool True
  SFalse :: SBool False

type family G i where
  G True = () -- Doesn't really matter what these are
  G False = ()

newtype GN i = MkGN (G i)

-- "Incorrect" Show instance
deriving instance Show (G i) => Show (GN i)

newtype GN2 i = MkGN2 (G i)

-- "Correct" Show instance
instance SingI i => Show (GN2 i) where
  show = error "This can be derived using Generic. Not bothering here."

type instance Sing = SBool

instance SingI True where sing = STrue
instance SingI False where sing = SFalse

-- I can recover the "correct" context.
showGN :: forall (i :: Bool). SingI i => GN i -> String
showGN = case sing @i of
  STrue -> show
  SFalse -> show

example1 :: Some GN
example1 = Some (MkGN () :: GN True)

-- There's no way of recovering the "correct" context here
-- Could not deduce (Show (G i)) arising from a use of ‘show’
-- example2 :: String
-- example2 = show example1

example3 :: Some GN2
example3 = Some (MkGN2 () :: GN2 True)

example4 :: String
example4 = show example3

[RyanGlScott]

Ah, I see what you mean now. Indeed, if you used a forall (a :: t). SingI a => CApply Show f a constraint in the Show instance for Sigma, then you still wouldn't be able to call show mySigma on your original mySigma :: Sigma () Id example from https://github.com/goldfirere/singletons/issues/579#issue-2019096984, since GHC would still complain thusly:

    • Could not deduce (Show (Apply Id a)) arising from a use of ‘show’
      from the context: SingI a

Since the quantified constraint requires SingI (a :: ()), it feels like one ought to be able to match on sing :: Sing '() and convince GHC that a ~ '(). This would cause Apply Id '() to reduce to () and all would be well. But as you say, it's not straightforward to do this at the level of constraints, which is where GHC#14822 enters the picture. I think I'm following now.