[GHC] #9117: Coercible constraint solver misses one
#9117: Coercible constraint solver misses one
------------------------------------+-------------------------------------
Reporter: goldfire | Owner:
Type: bug | Status: new
Priority: normal | 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: |
------------------------------------+-------------------------------------
When I say
{{{
import Data.Type.Coercion
import Data.Coerce
eta :: Coercible f g => Coercion (f a) (g a)
eta = Coercion
}}}
I get
{{{
Could not coerce from ‘f a’ to ‘g a’
because ‘f a’ and ‘g a’ are different types.
arising from a use of ‘Coercion’
from the context (Coercible f g)
bound by the type signature for
eta :: Coercible f g => Coercion (f a) (g a)
at /Users/rae/temp/Roles.hs:6:8-44
In the expression: Coercion
In an equation for ‘eta’: eta = Coercion
}}}
But, this coercion is easily expressible in Core. If `(co :: f ~R# g)`
then `(co <a> :: f a ~R# g a)`, where `<a>` is the notation for a
reflexivity coercion for the type `a`. The constraint solver should be
able to do this.
--
Ticket URL:
#9117: Coercible constraint solver misses one -------------------------------------+------------------------------------ Reporter: goldfire | Owner: nomeata Type: bug | Status: new Priority: normal | 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: -------------------------------------+------------------------------------ Changes (by simonpj): * owner: => nomeata Comment: Good point. Joachim, might you look at this? Simon -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9117#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9117: Coercible constraint solver misses one -------------------------------------+------------------------------------ Reporter: goldfire | Owner: nomeata Type: bug | Status: new Priority: normal | 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): Is this subsumed by #8555? Do we want a general “instance” {{{Coercible f g => Coercion (f a) (g a)}}}? Wouldn’t that run into a dead end in situations like {{{ newtype Foo1 a = Foo1 (a,()) newtype Foo2 a = Foo2 (a,()) coerce :: Foo1 () -> Foo2 () }}} which might simplify this to {{{Coercible Foo1 Foo2}}} if that happens to happen before the newtype-unwrapping instance? So while it surely is possible to add that to the solver somehow, e.g. as a final thing to try, I’m not sure about all the implications. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9117#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9117: Coercible constraint solver misses one -------------------------------------+------------------------------------ Reporter: goldfire | Owner: nomeata Type: bug | Status: new Priority: normal | 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): I don't think it's related to #8555 at all. #8555 is to do with "given" constraints, whereas this ticket is entirely about wanted ones. But you make an excellent point about overlap with the newtype-unwrapping instances. I can't see an easy way round that. Simon -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9117#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9117: Coercible constraint solver misses one -------------------------------------+------------------------------------ Reporter: goldfire | Owner: nomeata Type: bug | Status: new Priority: normal | 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): But doesn't the constraint solver already deal with overlap somehow? For example, if we have `newtype MyMaybe a = Mk (Maybe a)`, and we want `Coercible (MyMaybe Int) (MyMaybe Age)`, there are two ways to get this.... unless there is a role annotation on `MyMaybe`, meaning only the unwrap-coerce-wrap solution is available, or unless the constructor is not available, when only the coerce-directly solution is available. So, if this all works, there has to be some way of dealing with the overlap and a small amount of "search". Is the case in this ticket somehow different/worse? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9117#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9117: Coercible constraint solver misses one -------------------------------------+------------------------------------ Reporter: goldfire | Owner: nomeata Type: bug | Status: new Priority: normal | 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):
So, if this all works, there has to be some way of dealing with the overlap and a small amount of "search".
Well, the way is „do whatever comes first“. It works because the rewrite system is confluent (I hope that’s the right term), i.e. we don’t run into dead ends if we do on or the other first.
Is the case in this ticket somehow different/worse?
Yes, as `Coercible Foo1 Foo2` would be a dead end. It ''might'' work to try `Coercible f g => Coercion (f a) (g a)` only if no other instance matches. The code is able to do so, but I don’t particularly like that. We can add it if we don’t have a better idea ''and'' there there is a use case for it. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9117#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9117: Coercible constraint solver misses one -------------------------------------+------------------------------------ Reporter: goldfire | Owner: nomeata Type: bug | Status: new Priority: normal | 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): The trouble with "no other instance matches" is that the situation might change as we solve other constraints and learn more. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9117#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9117: Coercible constraint solver misses one -------------------------------------+------------------------------------ Reporter: goldfire | Owner: nomeata Type: bug | Status: new Priority: normal | 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): Replying to [comment:5 nomeata]:
we don’t run into dead ends if we do on or the other first.
I don't agree here. Say we have {{{ newtype Phant a = MkPhant Char type role Phant representational ex1 :: Phant Bool ex1 = coerce (MkPhant 'x' :: Phant Int) }}} This should succeed if we use newtype-unwrapping instances first but should fail if we use the congruence case first. And, indeed, it fails! I think it should succeed. Regardless of what we decide to do about the original feature requested, I think the failure of this example is a proper bug. I believe that if we try the newtype-unwrapping instances first, the algorithm would be sound. Why? Because the congruence case can never be more powerful than the newtype-unwrapping case, due to role inference. That is, the roles on any type parameters of the newtype can never be more permissive than the roles on its representation type. So, we actually ''already'' have an ordering dependence on the cases, in order to avoid dead ends -- but we didn't realize it! Is there a problem with adding one more layer to this? :) For use cases, see [https://github.com/ekmett/roles/blob/master/src/Data/Roles.hs here], some experimentation Edward K has done regarding tracking roles in type variables. He has to use `eta` in a fair number of constructions. Fixing the original ticket would allow these to be proven sound instead of relying on `unsafeCoerce`. And, in response to Simon, yes that's true that the situation might change, but I don't see how that's problematic. These instances are intentionally "incoherent", so we are robust in the presence of a change in exactly ''how'' the instance is solved for. The "changed situation" shouldn't make a previously-allowable coercion become otherwise. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9117#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9117: Coercible constraint solver misses one -------------------------------------+------------------------------------ Reporter: goldfire | Owner: nomeata Type: bug | Status: new Priority: normal | 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):
So, we actually already have an ordering dependence on the cases, in order to avoid dead ends -- but we didn't realize it!
Well spotted. The fix for this should be simple, just re-order the cases in `getCoercibleInst`. I also believe that unwrapping `newtype`s should be strictly more powerful than the other. I’m still with Simon’s worries about changing situation. It is not coherence that we need to worry about, but, as you have just demonstrated, solvability. Adding the eta-contraction might give new possibilities to run into dead ends. But I’m still not able to give a good example of what I mean, so I guess I could just implement this and we’ll see what happens. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9117#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9117: Coercible constraint solver misses one -------------------------------------+------------------------------------ Reporter: goldfire | Owner: nomeata Type: bug | Status: new Priority: normal | 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): It strikes me that what we have here is a nice little programming- languages problem that would probably submit to standard techniques. Specifically, we have a specification of what things are coercible -- the typing rules for representational coercions -- and an algorithm for checking whether two things are coercible. The algorithm is straightforward and could be formalized beyond its Haskell implementation. Then, we could verify if the algorithm is sound and/or complete w.r.t. the specification. If it's not sound, we have the possibility of a Core Lint error. If it's not complete, we have the possibility of failing inappropriately. To be clear, I'm not quite volunteering to do this tonight or saying that it's an essential step, but it might be a nice thing to try if we want to understand this better. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9117#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9117: Coercible constraint solver misses one -------------------------------------+------------------------------------ Reporter: goldfire | Owner: nomeata Type: bug | Status: new Priority: normal | 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): The only reason for giving a role signature that is less permissive than the actual newtype-unwrapping is, well, to be more restrictive. So I think it'd be rather unusual both to give a role signature, and to expose the data constructor of the newtype. So I'm not too bothered about this particular dead end. But still, yes, putting the rules in the other order would be a good idea. (Make sure you add a `Note`!) I'm a bit bugged that `Coercible (N Age) (N Int)` might take a rather long way round (unwrapping multiple layers of newtype) rather than the short cut (try `(Coercible Age Int)`). But maybe I should not worry about that. As to the "knowing more later" stuff, I'm just referring to situations like `(alpha t1) ~ (alpha t2)` where `alpha` is a unification variable. As constraint solving progresses we may learn what `alpha` is -- but if we have already decomposed the application it may now be too late. It's difficult to use the approach that Richard describes, because it interacts with all the other constraint solving that is going on during type inference. NB that this "more info later" stuff does not apply to the reordering to apply newtype unwrapping before decomposition, because both newtype unwrapping and decomposition apply only when the head is a known type constructor. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9117#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
The only reason for giving a role signature that is less permissive than
#9117: Coercible constraint solver misses one -------------------------------------+------------------------------------ Reporter: goldfire | Owner: nomeata Type: bug | Status: new Priority: normal | 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): Replying to [comment:10 simonpj]: the actual newtype-unwrapping is, well, to be more restrictive. So I think it'd be rather unusual both to give a role signature, and to expose the data constructor of the newtype. So I'm not too bothered about this particular dead end. Actually, fixing this adds a nice feature to this whole area: the ability to have free conversions within a library but not to export this capability! If we have a newtype with a nominal role annotation, its constructor might be visible only among "friendly" modules, allowing the free conversion. Then, outside of the package, the constructor is inaccessible, so no conversions are possible. This ability was a desideratum at the beginning of the design process that we thought we threw away when we went with the idea of using class instances. But, now we have it back!
But still, yes, putting the rules in the other order would be a good idea. (Make sure you add a `Note`!) I'm a bit bugged that `Coercible (N Age) (N Int)` might take a rather long way round (unwrapping multiple layers of newtype) rather than the short cut (try `(Coercible Age Int)`). But maybe I should not worry about that.
You shouldn't worry about that. :) I conjecture that coercion optimization ''already'' fixes this problem. (See uses of `matchAxiom` in !OptCoercion.)
As to the "knowing more later" stuff, I'm just referring to situations
like `(alpha t1) ~ (alpha t2)` where `alpha` is a unification variable. As constraint solving progresses we may learn what `alpha` is -- but if we have already decomposed the application it may now be too late. It's difficult to use the approach that Richard describes, because it interacts with all the other constraint solving that is going on during type inference. Ah. Good point. I hadn't thought of it that way. You're right -- we need to be careful here. But, if #9123 gets solved in the way that we're thinking of solving it now, we will want the functionality originally requested in this ticket available. So, it may be worth doing some Hard Thinking about this and getting it right. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9117#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
Actually, fixing this adds a nice feature to this whole area: the ability to have free conversions within a library but not to export this capability! If we have a newtype with a nominal role annotation, its constructor might be visible only among "friendly" modules, allowing the free conversion. Then, outside of the package, the constructor is inaccessible, so no conversions are possible. This ability was a desideratum at the beginning of the design process that we thought we
#9117: Coercible constraint solver misses one -------------------------------------+------------------------------------ Reporter: goldfire | Owner: nomeata Type: bug | Status: new Priority: normal | 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): Replying to [comment:11 goldfire]: threw away when we went with the idea of using class instances. But, now we have it back! True, but only for newtypes, there is currently no way for „I want to coerce under `Set` in my own modules only.“, that would require the are- all-type-constructors-in-scope test again. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9117#comment:12 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9117: Coercible constraint solver misses one -------------------------------------+------------------------------------ Reporter: goldfire | Owner: nomeata Type: bug | Status: new Priority: normal | 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): Yes, but the library-writer could just use a newtype to get this functionality. For example, if the writer of `Set` wants coercions internally, they use `SetInternal` with no role annotations and then `Set` with a role annotation. It's a little bit of (compile-time-only) overhead, but it should be usable. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9117#comment:13 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9117: Coercible constraint solver misses one -------------------------------------+------------------------------------ Reporter: goldfire | Owner: nomeata Type: bug | Status: new Priority: normal | 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): Replying to [comment:13 goldfire]:
Yes, but the library-writer could just use a newtype to get this functionality. For example, if the writer of `Set` wants coercions internally, they use `SetInternal` with no role annotations and then `Set` with a role annotation. It's a little bit of (compile-time-only) overhead, but it should be usable.
Ah, right. I think we had this discussion before, and you told me that back then :-) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9117#comment:14 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9117: Coercible constraint solver misses one -------------------------------------+------------------------------------ Reporter: goldfire | Owner: nomeata Type: bug | Status: new Priority: normal | 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): OK, so I think at least part of this ticket has a conclusion: * We should try newtype unwrapping before trying decomposition. (But please let's try identity first of all in case the two types are identical.) * The reason for this ordering should be captured in a `Note` * I think it would also be highly worthwhile to start a new "user- documentation" page on the Haskell wiki, linked from [http://www.haskell.org/haskellwiki/GHC/Type_system GHC type system extensions]. This gives a user-updatable place to explain how to use the raw facilities. The points explained above in comments 11-14 are far from obvious, and it'd be great to have them articulated there. Joachim might you do these things? Thanks. That still leaves the original topic of the ticket (decomposing applications) open. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9117#comment:15 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9117: Coercible constraint solver misses one -------------------------------------+------------------------------------ Reporter: goldfire | Owner: nomeata Type: bug | Status: new Priority: normal | 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): I’ll do 1 and 2 (that’s why I already assigned the ticket to me) and might start on 3, although Richard appears to has a better overview, so I hope he’ll help me with that. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9117#comment:16 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9117: Coercible constraint solver misses one
-------------------------------------+------------------------------------
Reporter: goldfire | Owner: nomeata
Type: bug | Status: new
Priority: normal | 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 Joachim Breitner
#9117: Coercible constraint solver misses one
-------------------------------------+------------------------------------
Reporter: goldfire | Owner: nomeata
Type: bug | Status: new
Priority: normal | 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 Joachim Breitner
#9117: Coercible constraint solver misses one -------------------------------------+------------------------------------ Reporter: goldfire | Owner: nomeata Type: bug | Status: new Priority: normal | 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): I implemented the changed order (code is running a validate right now). There are still weird corner-cases. Consider: {{{ newtype Foo a = Foo (Foo a) newtype Age = MkAge Int ex1 :: (Foo Age) -> (Foo Int) ex1 = coerce }}} Previously, this would be solvable; now it starts unrolling the infinite newtype. (But we don’t have a good story for newtypes anyways). -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9117#comment:19 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9117: Coercible constraint solver misses one -------------------------------------+------------------------------------ Reporter: goldfire | Owner: nomeata Type: bug | Status: new Priority: normal | 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): Started http://www.haskell.org/haskellwiki/GHC/Coercible and added the bits about how to achieve different `Coercible` behaviour in internal and external code. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9117#comment:20 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9117: Coercible constraint solver misses one -------------------------------------+------------------------------------ Reporter: goldfire | Owner: nomeata Type: bug | Status: new Priority: normal | 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): Your non-terminating `Foo` example seems pathological, but what about this, somewhat more sensible example: {{{ newtype Bar a = Bar (Either a (Bar a)) x :: Bar Age x = coerce (Bar (Left (5 :: Int))) }}} This example works in 7.8.2. PS: Will contribute to the "Coercible" page in due course. Thanks for starting it. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9117#comment:21 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9117: Coercible constraint solver misses one -------------------------------------+------------------------------------ Reporter: goldfire | Owner: nomeata Type: bug | Status: new Priority: normal | 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): Yes, that’s a better example. So we have a dilemma: Should we support recursive newtypes better, or should we support different internal/external coercions better? Your trick in comment:13, shouldn’t that work for newtypes just as well? So maybe the original order was better after all... -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9117#comment:22 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9117: Coercible constraint solver misses one -------------------------------------+------------------------------------ Reporter: goldfire | Owner: nomeata Type: bug | Status: new Priority: normal | 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): I suppose it would. But, if we decide not to let my example in comment:7 work, we need to articulate this clearly somewhere. According to all the "rules" around `Coercible`, it would seem that the code in comment:7 should work and may surprise folks when it doesn't. I have to say I don't love the idea of not handling comment:7, but if we can't find a way to do it, it's not the end of the world. Would it make sense to detect the recursion and then switch techniques? Seems ad-hoc. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9117#comment:23 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9117: Coercible constraint solver misses one -------------------------------------+------------------------------------ Reporter: goldfire | Owner: nomeata Type: bug | Status: new Priority: normal | 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 the paper comments you write
Suppose module `A` uses `coerce` somewhere and contains a newtype whose constructor is not imported. We now modify `A` to import the constructor. Is it guaranteed that the use(s) of `coerce` will still work? We would want to offer such a guarantee I think.
We are unable to give this guarantee with either of the two solving strategies. Consider: {{{#!haskell module Foo where newtype Rec a = Rec a newtype Hide a = Hide (Rec a) module Bar where import Foo (Hide(Hide), Rec) ex :: Rec Age -> Hide Int ex = coerce }}} This works (`Hide` is unrolled, then we can lift through `Rec` and are done). If we also import `Rec`, then `Coercible (Rec Age) (Hide Int)` (where no lifting is possible yet, so the order does not matter) will cause it to loop. I couldn’t construct it with a less pathological newtype yet, though, as these will cause a proper data tycon to appear, then the newtypes on the RHS get unwrapped and eventually the terms on both sides match. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9117#comment:24 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9117: Coercible constraint solver misses one -------------------------------------+------------------------------------ Reporter: goldfire | Owner: nomeata Type: bug | Status: new Priority: normal | 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): You've revealed yet another interesting characteristic of this algorithm. The order ''of the coercion'' matters! Here is my test case: {{{ newtype Rec a = Rec (Rec a) newtype Hide a = Hide (Rec a) ex :: Hide Age -> Rec Int ex = coerce }}} (Note -- no module boundary.) This example (on GHC 7.8.2, without the updated solver earlier in this ticket) works fine. If I reverse the order of the coercion, though, it fails. This, of course, makes sense when thinking about the implementation, but it's weird if you don't think about that. This is all suggesting to me that the "correct" thing to do when recursion gets out of hand is not to immediately fail, but to try other techniques. I know this idea violates the maxim of "do no search", but I'm not sure what's so terrible about searching here. Getting back to your example, I posit that, with my ordering above (`Hide Int -> Rec Age`) the new solver will fail. This makes the new solver less (not?) dependent on coercion order. Is that better? Perhaps. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9117#comment:25 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9117: Coercible constraint solver misses one -------------------------------------+------------------------------------ Reporter: goldfire | Owner: nomeata Type: bug | Status: new Priority: normal | 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): I'm disinclined to get bent out of shape by pathologically recursive newtypes. Whereas the place this ticket started was with more reasonable cases. Simon -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9117#comment:26 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9117: Coercible constraint solver misses one -------------------------------------+------------------------------------ Reporter: goldfire | Owner: nomeata Type: bug | Status: new Priority: normal | 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): Fair enough. I believe any of these problems exist with non-pathologically recursive newtypes, such as my `Bar` example in comment:21. But, I'm also happy enough to say "caveat programmer" if they use recursive newtypes with `Coercible`. We should make sure to say that somewhere, though. If we neglect recursive newtypes (which is reasonable, I would say) then the reordered solver (as it is in HEAD, as I understand) seems better than the one released with 7.8.2. But, how are we faring on the original request at the top? PS: Just realized that I never contributed to the wiki page. Will do shortly. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9117#comment:27 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9117: Coercible constraint solver misses one -------------------------------------+------------------------------------ Reporter: goldfire | Owner: nomeata Type: bug | Status: new Priority: normal | 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): OK. Added section on [http://www.haskell.org/haskellwiki/GHC/Coercible the wiki page] about recursive newtypes. Let me know if there's something else that should be there -- I think Joachim addressed the other salient points well. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9117#comment:28 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9117: Coercible constraint solver misses one
-------------------------------------+------------------------------------
Reporter: goldfire | Owner: nomeata
Type: bug | Status: new
Priority: normal | 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 Simon Peyton Jones
#9117: Coercible constraint solver misses one -------------------------------------+------------------------------------ Reporter: goldfire | Owner: nomeata Type: bug | Status: new Priority: normal | 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): See also #9153 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9117#comment:30 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9117: Coercible constraint solver misses one -------------------------------------+------------------------------------- Reporter: goldfire | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 Resolution: | Keywords: Operating System: | Architecture: Unknown/Multiple Unknown/Multiple | Difficulty: Unknown Type of failure: | Blocked By: None/Unknown | Related Tickets: Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Changes (by nomeata): * owner: nomeata => Comment: This ticket started with `eta :: Coercible f g => Coercion (f a) (g a)` and then discussed the order of our existing solving steps (which was then changed). But nothing happened about `eta :: Coercible f g => Coercion (f a) (g a)`. Is there a real use case for this? Do we have an idea how to integrate that? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9117#comment:31 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9117: Coercible constraint solver misses one -------------------------------------+------------------------------------- Reporter: goldfire | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 Resolution: | Keywords: Operating System: | Architecture: Unknown/Multiple Unknown/Multiple | Difficulty: Unknown Type of failure: | Blocked By: None/Unknown | Related Tickets: Test Case: | Blocking: | Differential Revisions: Phab:D546 | -------------------------------------+------------------------------------- Changes (by goldfire): * differential: => Phab:D546 Comment: I've written a new solver for `Coercible`. It is able to solve for all the cases considered in this ticket. However, this comes at the cost of essentially ditching support for pathologically recursive newtypes (like `Fix`, or `newtype Loop = Loop Loop`). I think this exchange is a solid win. Still working out the final bugs; will set to "patch" when those are done. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9117#comment:32 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9117: Coercible constraint solver misses one
-------------------------------------+-------------------------------------
Reporter: goldfire | Owner:
Type: bug | Status: new
Priority: normal | Milestone:
Component: Compiler | Version: 7.8.2
Resolution: | Keywords:
Operating System: | Architecture: Unknown/Multiple
Unknown/Multiple | Difficulty: Unknown
Type of failure: | Blocked By:
None/Unknown | Related Tickets:
Test Case: |
Blocking: |
Differential Revisions: Phab:D546 |
-------------------------------------+-------------------------------------
Comment (by Richard Eisenberg
#9117: Coercible constraint solver misses one -------------------------------------+------------------------------------- Reporter: goldfire | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 Resolution: fixed | Keywords: Operating System: | Architecture: Unknown/Multiple Unknown/Multiple | Difficulty: Unknown Type of failure: | Blocked By: None/Unknown | Related Tickets: Test Case: | typecheck/should_compile/T9117{,_2,_3}| Blocking: | Differential Revisions: Phab:D546 | -------------------------------------+------------------------------------- Changes (by goldfire): * status: new => closed * testcase: => typecheck/should_compile/T9117{,_2,_3} * resolution: => fixed -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9117#comment:34 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9117: Coercible constraint solver misses one -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: bug | Status: closed Priority: normal | 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: | typecheck/should_compile/T9117{,_2,_3} Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D546 Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * keywords: => Roles -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9117#comment:35 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC