Opened 15 months ago

Closed 8 months ago

#9117 closed bug (fixed)

Coercible constraint solver misses one

Reported by: goldfire Owned by:
Priority: normal Milestone:
Component: Compiler Version: 7.8.2
Keywords: Cc:
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 Revisions: Phab:D546

Description

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.

Change History (34)

comment:1 Changed 15 months ago by simonpj

  • Owner set to nomeata

Good point. Joachim, might you look at this?

Simon

comment:2 Changed 15 months ago 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.

comment:3 Changed 15 months ago 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

comment:4 Changed 15 months ago 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?

comment:5 follow-up: Changed 15 months ago 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.

comment:6 Changed 15 months ago by simonpj

The trouble with "no other instance matches" is that the situation might change as we solve other constraints and learn more.

comment:7 in reply to: ↑ 5 Changed 15 months ago by goldfire

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

comment:8 Changed 15 months ago 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 newtypes 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.

comment:9 Changed 15 months ago 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.

comment:10 follow-up: Changed 15 months ago 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.

comment:11 in reply to: ↑ 10 ; follow-up: Changed 15 months ago by goldfire

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

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.

comment:12 in reply to: ↑ 11 Changed 15 months ago by nomeata

Replying to goldfire:

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!

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.

comment:13 follow-up: Changed 15 months ago 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.

comment:14 in reply to: ↑ 13 Changed 15 months ago by nomeata

Replying to 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 :-)

comment:15 Changed 15 months ago 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 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.

comment:16 Changed 15 months ago 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.

comment:17 Changed 15 months ago by Joachim Breitner <mail@…>

In 7e78faf033405bd5f3b6b787343c98e33d767bda/ghc:

Coercible: Unwrap newtypes before coercing under tycons

This fixes parts of #9117.

comment:18 Changed 15 months ago by Joachim Breitner <mail@…>

In 94c57676d7f88cd9edcc522aa3dc3ec6e3ad6633/ghc:

Coercible: Test case for now broken(?) corner case

involving a non-terminating newtype. This worked before 7e78faf03.
Probably not a problem, but still better to have a test case for it. See
ticket #9117.

comment:19 Changed 15 months ago 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 recursive newtypes anyways).

Last edited 15 months ago by nomeata (previous) (diff)

comment:20 Changed 15 months ago 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.

comment:21 Changed 15 months ago 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.

comment:22 Changed 15 months ago 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...

comment:23 Changed 15 months ago 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.

comment:24 Changed 15 months ago 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:

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.

comment:25 Changed 15 months ago 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.

comment:26 Changed 15 months ago 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

comment:27 Changed 15 months ago 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.

comment:28 Changed 15 months ago by goldfire

OK. Added section on 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.

comment:29 Changed 14 months ago by Simon Peyton Jones <simonpj@…>

In 9e10963e394680dbb1b964c66cb428a2aa03df09/ghc:

Improve Note [Order of Coercible Instances] about Trac #9117

comment:30 Changed 14 months ago by simonpj

See also #9153

comment:31 Changed 10 months ago by nomeata

  • Owner nomeata deleted

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?

comment:32 Changed 8 months ago by goldfire

  • Differential Revisions set to Phab:D546

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.

comment:33 Changed 8 months ago by Richard Eisenberg <eir@…>

In 0cc47eb90805f3e166ac4d3991e66d3346ca05e7/ghc:

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

comment:34 Changed 8 months ago by goldfire

  • Resolution set to fixed
  • Status changed from new to closed
  • Test Case set to typecheck/should_compile/T9117{,_2,_3}
Note: See TracTickets for help on using tickets.