Welcome to the Functional Programming Zulip Chat Archive. You can join the chat here.
Just started to read and understand how Data.Constraint.Extras is used/works (it used in aeson-gadt-th that derives JSON automatically for GADTs). Someone recently opened a PR to add module documentation, which seems pretty useful: https://github.com/obsidiansystems/constraints-extras/blob/develop/src/Data/Constraint/Extras.hs
Note that this library is based on ekmett's Data.Constraint
This trips me up:
type Has (c :: k -> Constraint) f = (ArgDict c f, ConstraintsFor f c)
ArgDict is a class, not a type. How can it be in the RHS of a type declaration?
Oh, right. Has is not of kind Type (which is what a regular type declaration would get you), but of Constraint. Specifically, it is referred to as "constraint synonym" (which is a kind of type synonym). This is enabled by the XConstraintKinds extension.
Correction: aeson-gadt does not use the constraint libraries. Though the two are usually used in conjunction, especially when using libraries like dependent-sum
I'm yet to revisit this and write a short tutorial on the topic (got too much on plate) but for now, this PR might of be interest: it improves the documentation of dependent-sum with helpful pointers to where ArgDict from constraints-extras fits in: https://github.com/mokus0/dependent-sum/pull/42/files