Problem with Show instance for heterogeneous list

Learn
#1

I try to define a Show instance for my heterogeneous list HList. The code is at the bottom of this post.

#1 below works, but I wanted a Show instance that looks more like the way a regular list shows, e.g. something like [1,"abc",True,3.1].

#2 attempts this, but I get stuck at the following error on show x. I don’t want to add a Show context to the definition of the data constructor Cons, because not all HLists will have only Show-able element types.

• Could not deduce (Show a2) arising from a use of ‘show’
  from the context: (Show a, Show (HList as))
...
  Possible fix:
    add (Show a2) to the context of the data constructor ‘Cons’
• In the first argument of ‘(:)’, namely ‘show x’
  In the expression: show x : toStringList xs

#3 attempts to move the helper function toStringList outside of the Show instance for HList, so I can specify the type constraint. In this case the error shifts to the recursive call toStringList xs:

• Could not deduce (Show a0) arising from a use of ‘toStringList’
  from the context: (Show a, Show (HList as))
...
• In the second argument of ‘(:)’, namely ‘toStringList xs’
  In the expression: show x : toStringList xs
  In an equation for ‘toStringList’:
      toStringList (Cons x xs) = show x : toStringList xs

What’s missing or wrong? How do I complete either #2 or #3 to get a Show instance for HList constructed the way I want?

{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}

import Data.List (intercalate)

data HList :: [*] -> * where
  Nil :: HList '[]
  Cons :: a -> HList as -> HList (a ': as)

instance Show (HList '[]) where
  show Nil = "[]"

-- #1: this works, but it's not what I wanted
{- instance (Show a, Show (HList as)) => Show (HList (a ': as)) where
  show (Cons x xs) = show x ++ " : " ++ show xs
 -}

-- #2: fails on `show x`
instance (Show a, Show (HList as)) => Show (HList (a ': as)) where
  show xs@(Cons _ _) = "[" ++ (intercalate "," . toStringList $ xs) ++ "]"
    where toStringList :: HList (as :: [*]) -> [String]
          toStringList (Cons x xs) = show x : toStringList xs
          toStringList Nil = []

-- #3: fails on `toStringList xs`
toStringList :: (Show a, Show (HList as)) => HList (a ': as) -> [String]
toStringList (Cons x Nil) = [show x]
toStringList (Cons x xs) = show x : toStringList xs
#2

You have to get a Show instance for the other elements of the list (because Show (HList as) is too indirect and not enough). You could do that with a type family:

{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE UndecidableInstances #-}

import Data.List (intercalate)
import Data.Kind

data HList :: [*] -> * where
  Nil :: HList '[]
  Cons :: a -> HList as -> HList (a ': as)

type family AllShow xs :: Constraint where
  AllShow '[] = ()
  AllShow (x ': xs) = (Show x, AllShow xs)

instance AllShow as => Show (HList as) where
  show xs = "[" ++ intercalate "," (toStringList xs) ++ "]"
    where toStringList :: AllShow bs => HList bs -> [String]
          toStringList (Cons x xs) = show x : toStringList xs
          toStringList Nil = []
2 Likes
#3

Thanks Jaro, for the example.

I guess my follow up question, then, is why does #1 above work? What’s different between #1, uncommented below, and #2/#3 which fail?

{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}

import Data.List (intercalate)

data HList :: [*] -> * where
  Nil :: HList '[]
  Cons :: a -> HList as -> HList (a ': as)

instance Show (HList '[]) where
  show Nil = "[]"

-- #1: this works, but it's not what I wanted
instance (Show a, Show (HList as)) => Show (HList (a ': as)) where
  show (Cons x xs) = show x ++ " : " ++ show xs

In #2 ghc can’t derive a Show instance for the head of the HList in the inner toStringList. I can try to modify the inner toStringList, but it ends up looking like #3.

In #3, i.e.

-- repeating the same code that occurs before #2
...

instance (Show a, Show (HList as)) => Show (HList (a ': as)) where
  show xs@(Cons _ _) = "[" ++ (intercalate "," . toStringList $ xs) ++ "]"
  -- inner toStringList removed from #2

-- #3: fails on `toStringList xs`
toStringList :: (Show a, Show (HList as)) => HList (a ': as) -> [String]
toStringList (Cons x Nil) = [show x]
toStringList (Cons x xs) = show x : toStringList xs

it looks to me like I can’t define the helper function toStringList, which helps to define the Show instance for HList, at the same time as I’m defining the Show instance for HList. It looks like the difficulty is a mutual recursion of the constraint, if that makes sense. (Not sure how else to describe it.) In order to deduce Show (HList as) in toStringList, I need to use the Show instance for HList, which is defined in terms of toStringList. Either the construction leads to a logical ambiguity or error which the type checker correctly complains about, or the construction is unambiguous but beyond what the type checker can resolve without more machinery like type families.

On the other hand, in #1 the “constraint recursion” is simple enough to be resolved.

#4

In #1 the constraint needed by show xs is exactly the constraint provided, namely Show (HList as), GHC doesn’t have to do any further instance resolution.

In #2 as you say a show instance for the head of the list is required, but it is not given in the type signature of toStringList and remember that type variables are not scoped so the as in that type signature is not the same as the as in the instance declaration (between instance and where).

In #3 the recursive call toStringList xs knows that as ~ a' : as' and it requires Show a' and Show (Hlist as') but those cannot be recovered from the Show (HList as) because instances are not bijective in the sense that if you know an instance exists then you cannot assume all constraints for that instance are also satisfied, because we have things like overlapping instances. So Show (HList as) and as ~ a' : as' doesn’t give us Show a' and Show (HList as'). I remember this coming up in a reddit discussion recently: https://reddit.com/r/haskell/comments/o0cq0o/video_ghc_sometimes_infers_the_wrong_type_richard/h1yri95/

Edit: fixed the reddit link.

#5

The constraint (Show a, Show (HList as)) is not enough to satisfy the constraints of the recursive call to toStringList - it does not guarantee that the head of as satissfies the Show contraint. However, AllShow is strong enough: AllShow (a : as) implies AllShow as.