Keep module self reference ?

[fblanqui]

Dedukti seems to allow to have a file f.dk containing:

symbol const N : TYPE
symbol const z : f.N

Is it a desirable feature, or should we forbid this?

[fblanqui]

I do not think that this a desirable feature. I would prefer to disallow it in LP. Any opinion?

[rlepigre]

Yes, this is not a desirable "feature" at all, as I have said numerous times. The problem is, we can't fix it in Lambdapi if it is not fixed in Dedukti at the same time (or at least in the libraries that rely on this). Note also that it is not possible to (cleanly) disable this behavior only for the Lambdapi syntax, since this is a scoping-time check.

[francoisthire]

Can you comment a little bit why this is not a desirable feature? Do we know if Krajono/CoqInE/Holide generates such things?

[rlepigre]

Well, I don't know a single other language with that behavior. In OCaml for example, you cannot use M.f inside the definition of the module M itself. I don't remember what librairies used that, but I do remember that I had to add that for compatibility with Dedutki at some point.