interface bug

[reswatson]

Something is wrong with interface elaboration. Tinyidris fails to compile and install as a result. But Tinyidris is correct/working Idris2 code. So it is a bug in the latest Idris2 version 0.3.0-bb59efa39.

Steps to Reproduce

install tinyidris with idris2 --build tinyidris.ipkg

Expected Behavior

installs without error

Observed Behavior

1/41: Building Data.Bool.Extra (src/Data/Bool/Extra.idr)
2/41: Building Text.Lexer.Core (src/Text/Lexer/Core.idr)
3/41: Building Text.Quantity (src/Text/Quantity.idr)
4/41: Building Text.Token (src/Text/Token.idr)
Error: While processing right hand side of value. {k:426} is not accessible in
this context.

src/Text/Token.idr:40:19--40:31
36 | ||| Get the value of a Token k. The resulting type depends upon
37 | ||| the kind of token.
38 | public export
39 | value : TokenKind k => (t : Token k) -> TokType (kind t)
40 | value (Tok k x) = tokValue k x
^^^^^^^^^^^^

Where is the bug?

src/Text/Token.idr is not bad code, but fails even to compile when tested. It can be used as self-contained code to isolate the bug. The interface elaboration seems to be failing to work when not working with a specific instance. It is the "TokenKind k => " part that seems to have lost functionality somewhere along the line. If k is replaced with a specific instance like 'Nat' the code can be made to work for that intance.

[gallais]

We've added the possibility to attach quantities to interface arguments.

In TinyIdris,

interface TokenKind (k : Type) where

should be

interface TokenKind (0 k : Type) where

to work with the current version of Idris.

[gallais]

I've started working on bringing the repo up to speed with current Idris. You can find
the current status here: https://github.com/gallais/SPLV20/tree/compat
I'm hoping to open a PR later this afternoon and hopefully we can get this merged in.

[gallais]

I've opened a PR with the fixed code so I'll close this.