Unbound variable

[tsani]

Load this signature.

kind : type.
con : type.

lam : kind -> (con -> con) -> con.
app : con -> con -> con.

cn-of : con -> kind -> type.
cn-equiv : con -> con -> kind -> type.

cn-equiv/beta : cn-of C1 K1 ->
                  (cn-of a K1 -> cn-of (C2 a) (K2 a)) ->
                  cn-equiv (app (lam K1 C2) C1) (C2 C1) (K2 C1). % Unbound identifier K2.

Beluga reports an error on the commented line, saying K2 is unbound. This variable is free and should have been automatically abstracted!

[tsani]

This issue is less serious than I first thought. Binding a in the right place gives

kind : type.
con : type.

lam : kind -> (con -> con) -> con.
app : con -> con -> con.

cn-of : con -> kind -> type.
cn-equiv : con -> con -> kind -> type.

cn-equiv/beta : cn-of C1 K1 ->
                  ({a : con} cn-of a K1 -> cn-of (C2 a) (K2 a)) ->
                  cn-equiv (app (lam K1 C2) C1) (C2 C1) (K2 C1).

and Beluga no longer complains about an unbound variable K2.