[GHC] #9131: Experiment with a dedicated solver for Coercible

[GHC]

#9131: Experiment with a dedicated solver for Coercible
------------------------------------+-------------------------------------
       Reporter:  nomeata           |             Owner:
           Type:  task              |            Status:  new
       Priority:  low               |         Milestone:
      Component:  Compiler          |           Version:  7.8.2
       Keywords:                    |  Operating System:  Unknown/Multiple
   Architecture:  Unknown/Multiple  |   Type of failure:  None/Unknown
     Difficulty:  Unknown           |         Test Case:
     Blocked By:                    |          Blocking:
Related Tickets:                    |
------------------------------------+-------------------------------------
 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...

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/9131>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler