[GHC] #9131: Experiment with a dedicated solver for Coercible
#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
#9131: Experiment with a dedicated solver for Coercible -------------------------------------+------------------------------------ Reporter: nomeata | Owner: Type: task | Status: new Priority: low | Milestone: Component: Compiler | Version: 7.8.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9131#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9131: Experiment with a dedicated solver for Coercible -------------------------------------+------------------------------------ Reporter: nomeata | Owner: Type: task | Status: new Priority: low | Milestone: Component: Compiler | Version: 7.8.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9131#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9131: Experiment with a dedicated solver for Coercible -------------------------------------+------------------------------------ Reporter: nomeata | Owner: Type: task | Status: new Priority: low | Milestone: Component: Compiler | Version: 7.8.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (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 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9131#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9131: Experiment with a dedicated solver for Coercible -------------------------------------+------------------------------------ Reporter: nomeata | Owner: Type: task | Status: new Priority: low | Milestone: Component: Compiler | Version: 7.8.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9131#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9131: Experiment with a dedicated solver for Coercible -------------------------------------+------------------------------------ Reporter: nomeata | Owner: Type: task | Status: new Priority: low | Milestone: Component: Compiler | Version: 7.8.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (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 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9131#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9131: Experiment with a dedicated solver for Coercible -------------------------------------+------------------------------------ Reporter: nomeata | Owner: Type: task | Status: new Priority: low | Milestone: Component: Compiler | Version: 7.8.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (by nomeata):
This ticket is really about whether a different solution strategy would be better.
Agreed :-) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9131#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9131: Experiment with a dedicated solver for Coercible -------------------------------------+------------------------------------- Reporter: nomeata | Owner: Type: task | Status: new Priority: low | Milestone: Component: Compiler | Version: 7.8.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: None/Unknown | Unknown/Multiple Blocked By: | Test Case: Related Tickets: | Blocking: | Differential Revisions: -------------------------------------+------------------------------------- Comment (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? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9131#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9131: Experiment with a dedicated solver for Coercible -------------------------------------+------------------------------------- Reporter: nomeata | Owner: Type: task | Status: closed Priority: low | Milestone: Component: Compiler | Version: 7.8.2 Resolution: fixed | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: None/Unknown | Unknown/Multiple Blocked By: | Test Case: Related Tickets: | Blocking: | Differential Revisions: -------------------------------------+------------------------------------- Changes (by goldfire): * status: new => closed * resolution: => fixed Comment: 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9131#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9131: Experiment with a dedicated solver for Coercible -------------------------------------+------------------------------------- Reporter: nomeata | Owner: (none) Type: task | Status: closed Priority: low | Milestone: Component: Compiler | Version: 7.8.2 Resolution: fixed | Keywords: Roles Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * keywords: => Roles -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9131#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC