locally-closed predicate does not type check

[pa-ba]

In the locally-nameless representation the generated locally-closed predicate does not type-check if there is a production that binds a variable for a different non-terminal.

In the example below, the production type_abs binds X, which is a variable for the non-terminal typ:

metavar tvar, X ::=
  {{ repr-locally-nameless }}

grammar

typ, T      :: '' ::=
  | X       ::    :: tvar
  | T -> T' ::    :: tfun

term, t :: '' ::=
  | t [ T ]  ::  :: tapp
  | /\ X . t ::  :: type_abs
   (+ bind X in t +)

In the generated Coq code, the case for the locally-closed predicate for the type_abs production does not type check because it uses open_typ_wrt_typ instead of open_term_wrt_typ:

 | lc_type_abs : forall (L:vars) (t:term),
      ( forall X , X \notin  L  -> lc_term  ( open_typ_wrt_typ t (tvar_f X) )  )  ->
     (lc_term (type_abs t)).