Idris2: Is there a way use implicits in interface implementations

Question

I'm following TDD with Idris using Idris2. I'm in chapter 6 working on the DataStore with schema. First of all for some context:

infixr 5 .+.

data Schema = SString
            | SInt
            | (.+.) Schema Schema

SchemaType : Schema -> Type
SchemaType SString = String
SchemaType SInt = Int
SchemaType (x .+. y) = (SchemaType x, SchemaType y)

At some point we want to format values of type SchemaType schema to display to the user. In the book this problem gets solved with a display function written like so:

display : SchemaType schema -> String
display {schema = SString} item = show item
display {schema = SInt} item = show item
display {schema = (x .+. y)} (iteml, itemr) = display iteml ++ ", " ++ display itemr

I wanna figure out if it's possible do get this working with the Show interface instead so I can just call show item.

I tried out the following:

Show (SchemaType schema) where
  show {schema = SString} item = show item  
  show {schema = SInt} item = show item
  show {schema = (x .+. y)} (x, y) = "(" ++ show x ++ ", " ++ show y ++ ")" 

But it tells me that schema will get erased and therefore cannot be used.

I've tried to get idris to keep it during runtime but I'm just guessing syntax and getting errors I don't really know how to interpret.

Attempt 1:

{schema:_} -> Show (SchemaType schema) where
  show {schema = SString} item = show item  
  show {schema = SInt} item = show item 
  show {schema = (x .+. y)} (x, y) = "(" ++ show x ++ ", " ++ show y ++ ")"

Throws:

Error: While processing left hand side of show. Can't match on ?postpone [no locals in scope] (Non linear pattern variable).

/home/stefan/dev/tdd-idris/SchemaDataStore.idr:27:33--27:34
 23 |
 24 | {schema:_} -> Show (SchemaType schema) where
 25 |   show {schema = SString} item = show item
 26 |   show {schema = SInt} item = show item
 27 |   show {schema = (x .+. y)} (x, y) = "(" ++ show x ++ ", " ++ show y ++ ")"
                                      ^

Attempt 2:

Show ({schema:_} -> SchemaType schema) where
  show {schema = SString} item = show item  
  show {schema = SInt} item = show item 
  show {schema = (x .+. y)} (x, y) = "(" ++ show x ++ ", " ++ show y ++ ")"

Throws:

Error: While processing left hand side of show. schema is not a valid argument in show ?item.

/home/stefan/dev/tdd-idris/SchemaDataStore.idr:25:3--25:31
 24 | Show ({schema:_} -> SchemaType schema) where
 25 |   show {schema = SString} item = show item
        ^^^^^^^^^^^^^^^^^^^^^^^^^^^^

Attempt 3

Show (SchemaType schema) where
  show item =
    case (schema, item) of
       (SString,  str)            => show str
       (SInt,     int)            => show int
       ((x .+. y), (left, right)) => "(" ++ show x ++ ", " ++ show y ++ ")"

Throws:

Error: While processing right hand side of show. Sorry, I can't find any elaboration which works. If Builtin.Pair: schema is not accessible in this context.

/home/stefan/dev/tdd-idris/SchemaDataStore.idr:26:11--26:17
 24 | Show (SchemaType schema) where
 25 |   show item =
 26 |     case (schema, item) of
                ^^^^^^

Can someone please enlighten me? Am I trying something that's not possible, did I just get the syntax wrong?

Answer 1

schema is not an argument to show. I think this is what you want:

{schema : _} -> Show (SchemaType schema) where
  show item =
    case (schema, item) of
       (SString,  str)            => show str
       (SInt,     int)            => show int
       ((x .+. y), (left, right)) => "(" ++ show x ++ ", " ++ show y ++ ")"

However that gives another error because type classes really only work well with data and you are using it with a function. Maybe someone on the Discord (in the tag description) knows how to make it work. The Idris stack overflow is not very active.