This also can be used to just create nicer error messages which is why you see it a lot. Instead of just saying “No instance for X” you’ll get “Cannot satisfy X ~ A” which suggests what X was supposed to be! This is another place you see these equalities showing up for what appears to be no good reason.
The last place I’ve used them is in very type-crazy code (my serv library to be specific) where they help direct type reduction to not get stuck. If the type family head is just a variable then it’ll always reduce and you can scoop up needed equalities later in the constraint solving portion of the algorithm. This is super black magic though.
This also can be used to just create nicer error messages which is why you see it a lot. Instead of just saying “No instance for X” you’ll get “Cannot satisfy X ~ A” which suggests what X was supposed to be! This is another place you see these equalities showing up for what appears to be no good reason.
The last place I’ve used them is in very type-crazy code (my serv library to be specific) where they help direct type reduction to not get stuck. If the type family head is just a variable then it’ll always reduce and you can scoop up needed equalities later in the constraint solving portion of the algorithm. This is super black magic though.