Ctypes and heterogeneous list typing problem

[Joel]

@lukstafi

Why would it not be possible? Seems possible on first glance (but I’m too tired to try today).

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.”