How to use interfaces with parameterized tuple?

Question

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

I'd like to use show and other functions like (==) with Coord s:

foo : Coord s -> String
foo x = show x

Error: While processing right hand side of foo. Can't find an implementation for Show (Coord s).

 22 | foo : Coord s -> String
 23 | foo x = show x
              ^^^^^^

Earlier I tried to implement Show (Coord s), but looks like it's impossible. Here is linked question about it.

Answer 1

You can make your own list like data type:

data Coords : List Nat -> Type where
    Nil : Coords []
    (::) : Fin x -> Coords xs -> Coords (x :: xs)

toList : Coords xs -> List Nat
toList [] = []
toList (x::xs) = finToNat x :: toList xs

example : Coords [2, 3]
example = [1, 2]

Show (Coords xs) where
    show cs = show $ toList cs

You can also try using Data.Vect.Quantifiers.All or Data.List.Quantifiers.All:

import Data.Vect
import Data.Vect.Quantifiers

example : All Fin [1, 2, 3]
example = [0, 1, 2]

-- not sure why this is isn't included with Idris
export
All (Show . p) xs => Show (All p xs) where
    show pxs = "[" ++ show' "" pxs ++ "]"
        where
            show' : String -> All (Show . p) xs' => All p xs' -> String
            show' acc @{[]} [] = acc
            show' acc @{[_]} [px] = acc ++ show px
            show' acc @{_ :: _} (px :: pxs) = show' (acc ++ show px ++ ", ") pxs

string : String
string = show example