Experiment with a dedicated solver for Coercible
|Reported by:||nomeata||Owned by:|
|Type of failure:||None/Unknown||Test Case:|
|Related Tickets:||Differential Revisions:|
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.
Currently 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)
- 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...