For pivoting? I don't know about dependent types, sometimes it's possible in theory to know the type of the pivot columns because you know the possible combinat

For pivoting? I don't know about dependent types, sometimes it's possible in theory to know the type of the pivot columns because you know the possible combinations of column fields that you're pivoting from, but is that dependent-typable? I think there's a kind of Motte and Bailey that goes on with people who think typesystems are the one true god. They choose the simplest typesystem as their example of the cognitive/learning overhead, (say C#?) But if you question the limitations they go to "but it's possible in X obscure typesystem".