Experiment with a dedicated solver for Coercible
This is something that I might want to do some time; it should not distract us from working and improving the current design and implementation. But I think it should be explored.
Coercible appears as a type class, we have instances to explain it, and use the existing solver to solve them. The last part sometimes causes problems:
- the order the instances are tried matters, there might be dead ends (#9117 (closed))
- recursive newtypes are not handled as good as they could be.
It would be worth exploring if a dedicated solver for
Coercible constraints could solve these issues. It could replace the existing
getCoercibleInst. Given a constraint
Coercible s t it would solve it completely, do nothing or (and this is not planned out yet) return some sufficient and in some sense primitive constraint that should appear in inferred type signatures etc.
Ideally we could still explain
Coercible in terms of the instances written in the ICFP’14 paper, and simply state „GHC will find a solution using these instances, if there are any.“ instead of „The usual solver is employed, it might run into dead ends (or not, hard to tell).“
When tackling this task, I should do something that I keep postponing (because I don’t like to admit my lack of knowlege about that) but I think is really important: What are the theoretical properties of solving
Coercible constraints? Is it even decidable? Semi decidable? Are there existing standard algorithms? How does this relate to SMT solving? And why don’t I know these things...