[SOLVED] How to implement `Show` interface for parameterized tuple?

How to implement `Show` interface for parameterized tuple?

I have Coord function that transforms an n-dimensional size to the type of coordinates bounded by given size: Coord [2,3] = (Fin 2, Fin 3).

import Data.Fin
import Data.List

Size : Type
Size = List Nat

Coord : Size -> Type
Coord [] = ()
Coord s@(_ :: _) = foldr1 (,) $ map Fin s

How can I implement Show interface for Coord s?

If I understand it correctly, the problem is that with s erased at compile time there is no way to know what the actual type of Coord s is. So my best attempt is this abomination:

show' : {s : Size} -> Coord s -> String
show' {s=[]} = show
show' {s=[_]} = show
show' {s=[_,_]} = show
show' = ?show'_rhs

{s : Size} -> Show (Coord s) where
  show = show'

foo : {s : Size} -> Coord s -> String
foo x = show' x -- compiles and works
foo x = show x  -- error

Error: While processing right hand side of foo. Can't find an implementation for Show (Coord s).
 22 | foo : {s : Size} -> Coord s -> String
 23 | foo x = show' x
 24 | foo x = show x
              ^^^^^^

Solution

(,) already has a Show implemention. Coords is just an alias not a datatype, it can't have separate interface implementations.