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.