Leftist Tree in Dyalog APL -- can it be made more compact/idiomatic?
I think your code generally looks good.

Comments

I recommend annotating functions with what the structure of their argument(s) and result are, especially when not just simple arrays, at the top of the function, rather than relying on code comments to reveal this.

Take benefit of dyadic functions

If you define Insert and Pop as dyadic functions both code and usage can be simplified. You can even let ⍬ be the default left argument, allowing easy initialisation of a tree.

Insert←{ ⍝ Insert item ⍵ into leftist tree ⍺, returning the resulting tree
    ⍺←⍬              ⍝ default to init
    1 ⍵ ⍬ ⍬ Merge ⍺ 
}


h←Insert 2
h Insert←10
h Insert←9

s←Insert 3
s Insert←6


Full variable names or not?

This is a personal style thing. Some people prefer mathematical-looking single-letter variables, others like full variable names that obviate comments. However, at least be consistent. (I've also moved the first element of ⍵ to become ⍺, as per above.)

Pop←{ ⍝ Pop off smallest element from a leftist tree
    0=≢⍺:⍬
    (value left right)←⍵
    (left Merge right) value
}


Unnecessary naming

⍺ and ⍵ are well understood to be the left and right arguments. I don't think renaming them t1 and t2 brings much, other than the ability to create matching keyN variables. However, here you only ever use key2 once, and its definition is very simple, and in fact as short or shorter than any appropriate name, so you might as well use it inline, freeing up key to only apply to ⍵:

Merge←{ ⍝ Merge leftist trees ⍺ and ⍵
    0=≢⍺:⍵ ⋄ 0=≢⍵:⍺                              ⍝ If either is a leaf, return the other
    (key left right)←1↓⍺
    key&gt;1⌷⍵:⍵∇⍺                                  ⍝ Flip to ensure smallest is root of merged
    merged←right∇⍵                               ⍝ Merge rightwards
    (⊃left)≥⊃merged:(1+⊃merged) key left merged  ⍝ Right is shorter
    (1+⊃left) key merged left                    ⍝ Left is shorter; make it the new right
}