I'm not totally familiar with Shen's syntax, but it looks like something interesting is going on here. In particular, the judgement `pop` is being automatically

I'm not totally familiar with Shen's syntax, but it looks like something interesting is going on here. In particular, the judgement `pop` is being automatically inferred and shown as impossible on the empty list. This is somewhat significantly more powerful than the similar Haskell technique. I'm not sure how Shen's type system works---perhaps some kind of subtyping is at play? Note, that power is a tradeoff in type systems. Typically, greater power can be beneficial for encoding more sophisticated predicates into the type system... but it'll almost certainly have consequences. Normally, power leads to a loss of inference, a need to pass around more type information to prove your claimed types, and/or loss of totality. Whether the power is worth it depends upon your domain.