to_expr does not check that referenced parameters are in scope

[cipher1024]

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.
    • Specifically, check out the wishlist, open RFCs,
      or feature requests.
  • Reduced the issue to a self-contained, reproducible test case.

Description

[Description of the issue]

Steps to Reproduce

Create a Lean file with the following

section
parameter H : Type
def my_def := H
include H
lemma some_lemma
: Type :=
begin
   clear H,
   have := my_def,
   exact this
end
end

lemma some_lemma'
: Type :=
begin
   clear H,
   have := _root_.my_def H,
   exact this
end

Expected behavior: [What you expect to happen]

The two lemmas should fail for the same reason, "unknown identifier 'H'"

Actual behavior: [What actually happens]

In the first lemma, the script executes successfully and the resulting proof term is rejected with:

failed to add declaration to environment, it contains local constants

I believe to_expr should figure out that H is out of scope.

Reproduces how often: [What percentage of the time does it reproduce?]
100%

Versions

I'm on OSX 10.13.2

Lean (version 3.3.1, commit 368f17d, RELEASE)

Additional Information