#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 2 years ago by nomeata
comment:2 Changed 2 years ago by goldfire
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 2 years ago by simonpj
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 2 years ago by nomeata
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 2 years ago by simonpj
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 2 years ago by nomeata
This ticket is really about whether a different solution strategy would be better.
Agreed :-)
comment:7 Changed 15 months ago by nomeata
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 15 months ago by goldfire
- Resolution set to fixed
- Status changed from new to 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 7 months ago by thomie
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
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.