Unfriendly error with unspecified coeffect type + you can specify arbitrary vars for types

[GuiltyDolphin]

On commit 6a38f01 (dev-minor).

With the following program (in a file prog.gr):

prog : forall a s. a [s] -> a [s]
prog t = t

I get the following error message:

Checking prog.gr...
Type checking failed: prog.gr:
Unbound type variable: prog.gr:2:1:
`_ks` is not quantified

Which ain't very friendly.

By using the debug option I was able to find that the program was interpreted as:

prog
  : forall {a`0 : _ka, s`1 : _ks} . a`0 [s`1] -> a`0 [s`1]
prog t`2 = t`2

So it's wanting me to specify a coeffect type, which I don't really want to do (implicit forall would be nice?).

But then I thought, hang on, what about that _ka? It didn't complain about that, so I tried the following:

prog : forall {a : ka, s : Nat} . a [s] -> a [s]
prog t = t

Which type-checks, which is concerning, because what is ka here??? And why is it treating "type variables" so different to grade variables?