defining type class instance on GADT

Question

Consider the following code

{-# LANGUAGE DataKinds             #-}
{-# LANGUAGE FlexibleContexts      #-}
{-# LANGUAGE GADTs                 #-}
{-# LANGUAGE KindSignatures        #-}
{-# LANGUAGE MultiParamTypeClasses #-}

module Test where

data Nat
    = Z
    | S Nat
    deriving Show

data Test foo (n :: Nat) where
    Final :: Test foo n
    Step :: foo n -> Test foo (S n) -> Test foo n

instance Show (foo n) => Show (Test foo n) where
    show Final           = "final"
    show (Step bar step) = show bar ++ show step

where Test is a GADT depending on a type parameter foo, which has kind Nat -> *.

The code above does not compile and I have the following error

• Could not deduce (Show (foo ('S n))) arising from a use of ‘show’
  from the context: Show (foo n)
    bound by the instance declaration at src/Test.hs:18:10-42
• In the second argument of ‘(++)’, namely ‘show step’
  In the expression: show bar ++ show step
  In an equation for ‘show’:
         show (Step bar step) = show bar ++ show step
   |
20 |     show (Step bar step) = show bar ++ show step
   |                                        ^^^^^^^^^

How can I state that Show (foo n) holds for every n, so that the compiler accepts it when it looks for Show (foo (S n))?

Answer 1

I think this would be a natural way:

class ShowAllNats f where showNat :: f (n :: Nat) -> String
instance ShowAllNats foo => Show (Test foo n) where
    show Final = "final"
    show (Step bar step) = showNat bar ++ show step

One can avoid an additional type class by existentially quantifying:

data Some f where Some :: f (n :: Nat) -> Some f
instance Show (Some foo) => Show (Test foo n) where
    show Final = "final"
    show (Step bar step) = show (Some bar) ++ show step