API returns can sometimes introduce shadowing

[brprice]

This is a tracking issue for some things I am currently working on.

Ideally, if a program does not contain any shadowing and an action is called which doesn't explicitly introduce shadowing (i.e. is not something like renaming a let to a specific name which causes shadowing), then there should me no shadowing in the resulting program. [This is obviously too hopeful for evaluation, since inlining lets etc can cause shadowing, etc]. However, this is not currently the case:

• substTy can introduce shadowing (in both directions, though I only exhibit shadowing an outer here, as that is difficult to fix; it could do a renaming that shadows an inner binder, but this is easy to fix), and this infects (i.e. the assertion in the code that the generated names will not enter the user's program is wrong, at least if you consider the metadata, and (potentially) evaluation)
  • metadata "checked at" etc for the result of ∀ AA. ∀ a . ∀ BB . AA ∋ Λ BB ?
  • metadata shadows a Λ-bound var in result of ? ∋ Λ a2. Λb. (? : ∀a.∀b.b) b
  • evaluation of case-of-known-constructor: due to annotation with the constructor's arguments' types with a substitution applied
• the result of evaluating a case-of-known-constructor (due to annotation with the constructor's arguments' types -- these types may have a ∀ which is shadowed by some lambda we are under), I imagine that any solution for the above cases will also apply here.
• result of evaluating doing an inline-a-let (or, with "Pushing down" let bindings #44, pushing a let through a binder)
• evaluating (Λa. e : ∀b.T)S to lettype b=S in (lettype a=S in e):T: the b may shadow something in S or e -- see fix: EvalFull duplicated IDs and captures variables in BETA reduction #511 for the capture analogue
• Eval when renaming a let can shadow an outer binder (if it happens to be named the same as the "fresh" name we generate) or an inner binder (ditto, and if it is hidden under a binder shadowing the let).
• Eval: potentially other places that use makeSafeLetBinding (since it may bind a new name, and is ignorant of the wider context)
• Similarly in EvalFull, whenever we rename or make a let we do not look at outer binders for shadowing (and are a bit inconsistent whether we look for inner binders)
• (Note that there is a utility mkFreshName that should be used in these places)
• mkFreshName does not look in annotations or type applications (indeed, any type children), and this affects lots of actions, e.g. ConstructLam: e.g. we get shadowing for actionTest NoSmartHoles ((emptyHole anntforall "a7" KType tEmptyHole )anntEmptyHole) [Move Child1, ConstructLam Nothing] (lam "a7" (emptyHoleanntforall "a7" KType tEmptyHole)ann tEmptyHole) which unexpectly passes

[brprice]

This has been addressed, other than the metadata issue.

• Metadata issues are now tracked in Shadowing and metadata #556
• We have fixed the remaining issues and have a test in Ensure API calls do not introduce shadowing #559 (some issues had been dealt with prior to that pr also)