Search code examples
polymorphismtypeclassdependent-typeidris

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

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?

Solution

  • 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