is shadowing allowed in CoreSyn?

[Adam Megacz]

Hello!  I'm currently attempting to reconstruct natural deduction proofs
(with explicit contraction/exchange/weakening) in System FC from
CoreSyn.Expr's in order to carry out a transformation which is defined
by induction on proofs (rather than terms).  I have it working for
simple examples, and now I need to clean up the corner cases.  I have a
few questions about the exact rules for what is/isn't legal in
CoreSyn...

Is shadowing allowed in CoreSyn?  For example:

  (Lam x (Lam x e))

If it is okay, I assume it creates a situation where you may shadow, but
only if the variables have the same type.  In other words, you can't
represent this term without doing some \alpha-renaming:

  \lambda x:Int . \lambda x:Char . e

... since in CoreSyn the type annotation on the lambda is actually part
of the Var, not the Expr production for Lam.

Also, I noticed -- to my surprise -- that Let can be used to bind type
variables.  Can recursive-Let be used for type variables?  If so, it
would seem to step well outside of System F (or FC)...

I assume that (Case (Type t) v t' alts) is illegal; could somebody
confirm this?

Thanks,

  - a