Finding an implementation (of show) for an inductively defined type

user_2129302 0
Viewed 74

The following snippet was from (https://stackoverflow.com/a/37461290/2129302):

tensor : Vect n Nat -> Type -> Type
tensor []        a = a
tensor (m :: ms) a = Vect m (tensor ms a)

I'd like to define the following:

mkStr : (Show a) => tensor shape a -> String
mkStr x = show x

But instead this gives the following error:

Can't find implementation for Show (tensor shape a)

However, on the REPL I can run "show [some tensor value...]". Why is this and what can I do to fix it?

dependent-type idris typeclass polymorphism
1 Answers

You're not showing a, you're showing tensor shape a. Thus, the following should work and you need to write type in the next way:

mkStr : (Show (tensor shape a)) => tensor shape a -> String
mkStr x = show x
user_29005020
Related