list : type -> type.
bool : type.
true : bool.
false : bool.
nil : list T.
cons : T -> list T -> list T.
snoc : list T -> T -> list T -> type.
snoc/nil : snoc nil M (cons M nil).
snoc/cons : snoc (cons N S) M (cons N S')
<- snoc S M S'.
%query 1 1 snoc (cons true (cons false nil)) true X.
Then the following code actually works in Twelf and does the right thing. The embedding consists of the declaration of t and obj, replacing every instance of type with t, and wrapping every base type with obj.
t : type.
obj : t -> type.
list : t -> t.
bool : t.
true : obj bool.
false : obj bool.
nil : obj (list T).
cons : obj T -> obj (list T) -> obj (list T).
snoc : obj (list T) -> obj T -> obj (list T) -> t.
snoc/nil : obj (snoc nil M (cons M nil)).
snoc/cons : obj (snoc (cons N S) M (cons N S'))
<- obj (snoc S M S').
%query 1 1 obj (snoc (cons true (cons false nil)) true X).
I guess some notions of glomming your whole signature into one type are usually considered dirty (at least in the absence of refinements to keep them separate), but here you really do have the type index to keep everything just as obviously adequate as before.
It's still sort of obviously bad in that it infects your whole signature, and again I'm pretty sure it's not actually a novel technique, but there might still be something to be said for the fact that the domain of the translation (i.e. LF with base-type polymorphism proper) probably has a reasonable metatheory itself.
