Just a hunch! Not super experienced with GADTs at all, just couldn’t think of how you could possibly express it in a type signature and so assumed that it wasn’t possible. If it is possible, I kind of imagine it’s one of those things you can do with GADTs but that require you to basically do proofs using witnesses and the like. A while back I remember trying the reverse a hlist twice puzzle and my takeaway was “here be dragons.”