Module identifier quoting

[gabrielhdt]

There seem to be some incoherence in module name quoting. For instance, consider the following module

invalid-name.dk

0: Type.

and let's try to type check several modules.

M.dk

#REQUIRE invalid-name.

Checking that gives

$ dk check M.dk
[ERROR CODE:701] [M.dk] [line:1 column:16]
Lexer error: Unexpected characters '-'.

which seems reasonable. But

Mq.dk

#REQUIRE {|invalid-name|}.

does not work either, checking results in Lexer error: Unexpected characters '#'.. But not requiring anything is ok,

Mnothing.dk

1: {|invalid-name|}.0.

succeeds.