## #9131 closed task (fixed)

# Experiment with a dedicated solver for Coercible

Reported by: | nomeata | Owned by: | |
---|---|---|---|

Priority: | low | Milestone: | |

Component: | Compiler | Version: | 7.8.2 |

Keywords: | Cc: | ||

Operating System: | Unknown/Multiple | Architecture: | Unknown/Multiple |

Type of failure: | None/Unknown | Test Case: | |

Blocked By: | Blocking: | ||

Related Tickets: | Differential Rev(s): | ||

Wiki Page: |

### Description

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...

### Change History (9)

### comment:1 Changed 3 years ago by

### comment:2 Changed 3 years ago by

Hmmm... this makes sense. Solving for a `Coercible`

constraint involves "looking through" newtypes, which may be recursive. This is analogous to the situation with type families, where we require `UndecidableInstances`

to do this sort of thing. For good reasons, we can't require `UndecidableInstances`

for recursive newtypes. I'm not sure what the best solution here is, though. A part of me would like to define some subset of this problem for which we guarantee completeness (perhaps this subset is "non-recursive newtypes"), not unlike with type families.

Good idea to pursue this line.

### comment:3 Changed 3 years ago by

In effect we already *have* a separate solver, namely special-purpose handling of the `Coercible`

constraints, which works interleaved with the current one. Interleaving is good because the two interact. I'm not sure that anything would be gained by separating them out. Though perhaps the code could be separated in a more modular fashion.

Simon

### comment:4 Changed 3 years ago by

In effect we already have a separate solver, namely special-purpose handling of the Coercible constraints, which works interleaved with the current one.

I’d disagree. What we have is a custom lookup routine that creates the instances on demand instead of looking them up in the instance environment (and chooses one if there are several, i.e. the issue of ordering). How the instances are used to solve a constraint is still up to the general code, nothing `Coercible`

-specific in there.

### comment:5 Changed 3 years ago by

We are mostly arguing terminology here. Most solvers work by saying "let me take this goal, and solve it by breaking it up into sub-goals and solving those". That's exactly what the `Coercible`

-specific code does here. You do not need to use that language of "instances" unless you want to.

What the current solver does *not* do is *search*, exploring many different paths to solving the goal. And indeed search is problemantic when combined with the need to infer a substitution for unification variables.

Anyway, we don't need to discuss terminology! This ticket is really about whether a different solution strategy would be better. And thus far I don't see any candidates on the table.

Simon

### comment:6 Changed 3 years ago by

This ticket is really about whether a different solution strategy would be better.

Agreed :-)

### comment:7 Changed 21 months ago by

12 months later, and we really have a specific Coercible solver. Do we still need this ticket, which is very vaguely about “a different solution strategy”? Probably not. Richard, do you agree?

### comment:8 Changed 21 months ago by

Resolution: | → fixed |
---|---|

Status: | new → closed |

Agreed. This is essentially done.

The only part around here that's missing is some theoretical analysis of the new solver. It would be nice, for example, to have a proof that the solver is sound (only produces well-typed coercions) and to figure out what completeness property it has (it's certainly not totally complete).

But there's little sense in having a ticket against GHC for that task.

### comment:9 Changed 14 months ago by

For future reference:

commit 0cc47eb90805f3e166ac4d3991e66d3346ca05e7

Author: Richard Eisenberg <eir@cis.upenn.edu> Date: Fri Dec 12 17:19:21 2014 -0500 Rewrite `Coercible` solver Summary: This is a rewrite of the algorithm to solve for Coercible "instances". A preliminary form of these ideas is at https://ghc.haskell.org/trac/ghc/wiki/Design/NewCoercibleSolver The basic idea here is that the `EqPred` constructor of `PredTree` now is parameterised by a new type `EqRel` (where `data EqRel = NomEq | ReprEq`). Thus, every equality constraint can now talk about nominal equality (the usual case) or representational equality (the `Coercible` case). This is a change from the previous behavior where `Coercible` was just considered a regular class with a special case in `matchClassInst`. Because of this change, representational equalities are now canonicalized just like nominal ones, allowing more equalities to be solved -- in particular, the case at the top of #9117. A knock-on effect is that the flattener must be aware of the choice of equality relation, because the inert set now stores both representational inert equalities alongside the nominal inert equalities. Of course, we can use representational equalities to rewrite only within another representational equality -- thus the parameterization of the flattener. A nice side effect of this change is that I've introduced a new type `CtFlavour`, which tracks G vs. W vs. D, removing some ugliness in the flattener. This commit includes some refactoring as discussed on D546. It also removes the ability of Deriveds to rewrite Deriveds. This fixes bugs #9117 and #8984. Reviewers: simonpj, austin, nomeata Subscribers: carter, thomie Differential Revision: https://phabricator.haskell.org/D546 GHC Trac Issues: #9117, #8984

**Note:**See TracTickets for help on using tickets.

Pondering this a bit, I think it is unsolvable, as we can encode the problem of whether two simply typed lambda terms with fix are equivalent. (It’s simply typed because our types are kinded).

For

`fix :: (* -> *) -> *`

, we need(and similar code for

`fix`

at higher types).So given a lambda expression, we do full lambda lifting to give the lambdas names, eta-expand according to their type and turn them into newtypes.

This is not fully worked out yet, but it seems to be reasonable to assume that our

`Coercible`

solver will never be complete and we’ll live with some shortcomings anyways.