Opened 10 months ago

Last modified 9 months ago

#9131 new task

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 Revisions:

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 (6)

comment:1 Changed 10 months ago by nomeata

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

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

newtype Fix1 f = Fix1 (f (Fix1 f))

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

module Lambda where

import Data.Coerce

newtype Fix1 f   = Fix1 (f (Fix1 f))
newtype Fix2 f x = Fix2 (f (Fix2 f) x)

-- lambda terms
-- a = λ f. λ y. f (f y)        :: (* -> *) -> * -> *
-- b = λ f. λ y. fix (λ x. f x) :: (* -> *) -> * -> *

-- lambda lifted
-- a1 f y = f (f y)
-- a f = a1 f

-- b1 f x = f x
-- b2 f y = fix (b1 f)
-- b f = b2 f

-- The newtypes

newtype A1 f y = A1 (f (f y))
newtype A y x  = A  (A1 y x)

newtype B1 f x = B1 (f x)
newtype B2 f y = B2 (Fix1 (B1 f))
newtype B f x  = B  (B2 f x)


-- Querying equivalence (Passing types with representational arguments as
-- parameters so that the solver doesn't stop at `Coercible (f ...) (f ...)`

ex :: A Maybe () -> B Maybe ()
ex = coerce

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.

comment:2 Changed 10 months 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 9 months 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 9 months 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 9 months 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 9 months ago by nomeata

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


Agreed :-)

Note: See TracTickets for help on using tickets.