I'm trying to define pairs using ur:?PLF:
theory pairs : ur:?PLF =
pair : {a : type} a ⟶ a ⟶ (a ⟶ a ⟶ a) ⟶ a ❙ // okay ❙
pair_kind = {a : type} a ⟶ a ⟶ (a ⟶ a ⟶ a) ⟶ a ❙ // not okay ❙
❚
The declaration of pair type-checks as I would expect.
However, the definition of pair_kind does not.
Is this expected behaviour? I don't understand what's going on.
You're using PLF, which extends LF with shallow polymorphism - shallow meaning that quantification over types is only allowed on the outside of types.
In order to make that work, an expression {a : type} ... is not allowed to be typed itself, otherwise you could freely quantify over types unrestrictedly.
The way this works in PLF is that expressions of the form {a : type} ... are inhabitable but - as I mentioned - not typed. Inhabitable meaning, it is allowed to occur as a "type" of a constant. Since it's not typed, you can't use a constant of that type (like pair) in an expression unless you provide the type arguments. So pair does not have a type, but pair A (for some type A) does.
That's why pair : {a : type} ... is accepted.
When you do pair_kind = {a : type} ..., you provide the expression as a definiens and do not provide a type, which means MMT will try to infer one - and (since this expression is not typed) fail.
If you want pair_kind to work, you need to use a stronger type system. For example ?LFHierarchy in LFX, which has a cumulative universe hierarchy (U n for every positive integer n) and defines type as U 0 and kind as U 1.