Hello!
The topic of using GADTs comes up every now and then. Personally I find that when I’m using GADTs in an attempt to optimize code I almost always quickly run into some “surprise” that doesn’t pass the type checker as I expected and then I need to spend time trying to figure it out. From what I’ve heard, that is not at all uncommon. OTOH, I’ve found polymorphic variants relatively straightforward to use and they apply to many uses. The problem with polymorphic variants, however, is that thay are compiled inefficiently (they use more memory and matching on them is less efficient).
I just discovered a kind of pattern for working with GADTs that seems to allow one to rather mechanically achieve what one could achieve easily with polymorphic variants, which is to specifically only allow / match a subset of the constructors depending on context (possibly different subsets in different contexts), using GADTs. I’m not claiming in any way that this is the first time the pattern has been discovered or that this technique would be the only or the best way to use GADTs. Far from it. I do, however, very much like the mechanical nature of this pattern. If I had known this pattern earlier, it would have saved me many hours of pulling out my hair!
So, here is a link to the gist: A pattern for using GADTs to subset cases.
I’ve now used this pattern in several cases and all of them have worked out nicely and mechanically.