Visible dependent quantification in Haskell

This post is based off of a talk I gave on March 8, 2019, that was unfortunately not recorded. In lieu of video, I decided to write this blog post so that I could share it with others. The slides of the talk are available here, although you do not need to read them in order to understand this post.

Continue reading »

How to derive Generic for (some) GADTs using QuantifiedConstraints

The Generic and Generic1 classes are extremely useful tools in a GHC programmer’s toolbox, but their utility is currently limited in the sense that one can only derive Generic instances for simple data types. By “simple”, I mean that GHC will simply error if you try to derive Generic a more sophisticated data type—a GADT—like this one:

Continue reading »