How to fix an inaccessible variable in idris2?

Question

I am having trouble to make a short idris2 code from the summer school course SPLV20 work. The error is at the last line:

module Text.Token

%default total

||| For a type `kind`, specify a way of converting the recognised
||| string into a value. ...

public export
interface TokenKind (k : Type) where
  ||| The type that a token of this kind converts to.
  TokType : k -> Type

  ||| Convert a recognised string into a value. The type is determined
  ||| by the kind of token.
  tokValue : (kind : k) -> String -> TokType kind

||| A token of a particular kind and the text that was recognised.
public export
record Token k where
  constructor Tok
  kind : k
  text : String

||| Get the value of a `Token k`. The resulting type depends upon
||| the kind of token.
public export
value : TokenKind k => (t : Token k) -> TokType (kind t)
value (Tok k x) = tokValue k x

The error says: While processing right hand side of value. {k:978} is not accessible in this context.

My current understanding is that k is a quantity 0 variable in the value function, so it cannot be used in the function body tokValue k x.

I tried to fix this by adding k as an implicit argument, value : TokenKind k => {k : Type} -> (t : Token k) -> TokType (kind t).

But now the types are wrong, and the system complains that:

While processing type of value. Can't find an implementation for TokenKind k.

I am only learning idris2 (0.60), and it's beyond me to fix this error.

My questions are:

1. Where in this file is the implementation of the TokenKind interface for the Token type? It seems to be hidden/implied and therefore I don't know how to provide the missing implementation.

2. How to fix the error about k being not accessible?