Name hygiene in expanded structure command

[gebner]

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
  • Reduced the issue to a self-contained, reproducible test case.

Description

When a macro expands to a structure, name resolution fails in fields with dependent types.

Steps to Reproduce

macro "foo" : command =>
  `(structure Foo where
      val : Nat
      prop : val = 42)

foo

Expected behavior: foo declares the structure Foo

Actual behavior: foo fails with unknown identifier 'val✝'

Versions

Nightly from November 12.

[Kha]

Hygiene of compound identifiers is not something we have really tackled yet (and for which we can't defer to Racket). Not sure when we'll get to it, there are a few fundamental issues to solve/decide on.

[Kha]

That is, this specific issue is simple to solve I believe. The hard part is to make Foo.prop and x.prop and { prop := ... } work.

[leodemoura]

I fixed the issue above.

That is, this specific issue is simple to solve I believe. The hard part is to make Foo.prop and x.prop and { prop := ... } work.

The only one that does not work yet is Foo.prop. Not sure how critical it is.

[gebner]

At least for my application, this was enough. I could remove the $value:ident : $ty workaround I was using before.