Opened 4 years ago
Closed 4 years ago
#10715 closed bug (fixed)
Possible regression in Coercible a (X a) between 7.8 and 7.10
Reported by: | inaki | Owned by: | goldfire |
---|---|---|---|
Priority: | normal | Milestone: | 7.10.3 |
Component: | Compiler | Version: | 7.10.1 |
Keywords: | Cc: | goldfire | |
Operating System: | Unknown/Multiple | Architecture: | Unknown/Multiple |
Type of failure: | GHC rejects valid program | Test Case: | typecheck/should_fail/T10715{,b} |
Blocked By: | Blocking: | ||
Related Tickets: | Differential Rev(s): | Phab:D1263 | |
Wiki Page: |
Description (last modified by )
In upgrading to7.10, code of the form
{-# LANGUAGE FlexibleContexts #-} import Data.Coerce (coerce, Coercible) data X a doCoerce :: Coercible a (X a) => a -> X a doCoerce = coerce
fails to compile in 7.10.1 and 7.10.2 with the error
testCoerce.hs:6:13: Could not deduce (a ~ X a) from the context (Coercible a (X a)) bound by the type signature for doCoerce :: Coercible a (X a) => a -> X a at testCoerce.hs:6:13-41 ‘a’ is a rigid type variable bound by the type signature for doCoerce :: Coercible a (X a) => a -> X a at testCoerce.hs:6:13 Relevant role signatures: type role X phantom In the ambiguity check for the type signature for ‘doCoerce’: doCoerce :: forall a. Coercible a (X a) => a -> X a To defer the ambiguity check to use sites, enable AllowAmbiguousTypes In the type signature for ‘doCoerce’: doCoerce :: Coercible a (X a) => a -> X a
while it works in 7.8.4.
Surprisingly (to me at least), the code works in 7.10.1 and 7.10.2 if I change it to
{-# LANGUAGE FlexibleContexts #-} import Data.Coerce (coerce, Coercible) data X a doCoerce :: Coercible a (X b) => a -> X a doCoerce = coerce
while it fails to compile in 7.8.4 with the error
testCoerce.hs:6:13: Could not coerce from ‘a’ to ‘X b0’ because ‘a’ and ‘X b0’ are different types. arising from the ambiguity check for ‘doCoerce’ from the context (Coercible a (X b)) bound by the type signature for doCoerce :: Coercible a (X b) => a -> X a at testCoerce.hs:6:13-41 The type variable ‘b0’ is ambiguous In the ambiguity check for: forall a b. Coercible a (X b) => a -> X a To defer the ambiguity check to use sites, enable AllowAmbiguousTypes In the type signature for ‘doCoerce’: doCoerce :: Coercible a (X b) => a -> X a
The coercion pattern may look a bit funny, but it is rather useful when one has newtypes of the form
newtype Y = Y (ForeignPtr Y)
which appear naturally when writing bindings to C libraries, and one wants to get access to the underlying ForeignPtr from Y (here X is ForeignPtr). The relevant Coercible instance here is Coercible Y (ForeignPtr Y), as above.
I would have expected the version with context "Coercible a (X a)" to be accepted, as 7.8.4 does, since it seems to be a specialization of the more general coerce, but maybe I am missing something?
Change History (18)
comment:1 Changed 4 years ago by
Description: | modified (diff) |
---|
comment:2 Changed 4 years ago by
Cc: | goldfire added |
---|
comment:3 follow-ups: 4 5 Changed 4 years ago by
comment:4 Changed 4 years ago by
Replying to simonpj:
Maybe we should do the same for
Coercible
?
The problem is that occurs-checks for representational equality don't necessarily mean failure. For example a ~R b a
is solvable if b
becomes the Identity
newtype. However, I do think that a ~R X a
is an error if X
is known to be a datatype. (That is, generative w.r.t. representational equality.)
But this will still fail:
oops :: Coercible a (b a) => a -> b a oops = coerce
Perhaps a way forward is to detect when an occurs-check problem has happened and add a NB: The solver for Coercible constraints is incomplete
in the error? Not really sure what to do here, beyond making occurs-check a hard failure when there is a generative type somewhere.
comment:5 Changed 4 years ago by
Replying to simonpj:
Thanks for the explanation! This makes it clear what happens. Just to state what I expected from reading the docs at https://hackage.haskell.org/package/base-4.8.1.0/docs/Data-Coerce.html, the following works:
{-# LANGUAGE FlexibleContexts, MultiParamTypeClasses, FlexibleInstances #-} -- import Data.Coerce (coerce, Coercible) data X a class Coercible a b where coerce :: a -> b newtype Y = Y (X Y) instance Coercible Y (X Y) where coerce (Y x) = x doCoerce :: Coercible a (X a) => a -> X a doCoerce = coerce test :: Y -> X Y test = doCoerce
which embodies what I understand the docs to be saying: because of the newtype, there is (morally) an instance of Coercible Y (X Y). But somehow the actual behavior of Coercible in 7.10 seems different.
- It wouldn't help your use-case. But do you have to use
Y
in this strange recursive way. Why not do this?newtype FY = FY (ForeignPtr Y) data Y
With the recursive definition for every newtype we automatically know the type of the ForeignPtr inside, while these ForeignPtrs still have distinct types, which comes handy on a number of occasions. It is also the way c2hs defines newtypes, for example
{# pointer *GIBaseInfo as BaseInfo newtype #}
becomes
newtype BaseInfo = BaseInfo (Ptr (BaseInfo))
so it is a fairly common idiom in the wild.
comment:6 follow-up: 8 Changed 4 years ago by
I'm all for ForeignPtrs having distinct types. I just don't understand why it has to be a recursive type. What's wrong with this?
newtype FY = FY (ForeignPtr Y) data Y
(except that it isn't what c2hs does today)
comment:7 follow-up: 10 Changed 4 years ago by
Owner: | set to goldfire |
---|
In response to comment:5: Despite appearances to the contrary, Coercible
is not a class. It is much more a special operator, right along the lines of ~
.
(Historical note: when we started developing the idea that became Coercible
, we thought it would indeed be a normal class, but with compiler-generated instances. And it started life that way. But when pushed, the limitations of the class-based solver became too much, and so Coercible
evolved. The code in GHC that solves Coercible
constraints is closely tied to solving of normal equality constraints, and not at all related to the code that solves class constraints.)
Perhaps the user manual should be updated to reflect this fact about Coercible
.
Regardless of the solution we settle on, this is in my area, so I'll adopt the ticket.
comment:8 Changed 4 years ago by
In response to simonpj:
I'm all for ForeignPtrs having distinct types. I just don't understand why it has to be a recursive type. What's wrong with this?
newtype FY = FY (ForeignPtr Y) data Y(except that it isn't what c2hs does today)
Certainly nothing! In code I write by hand I can easily do this.
comment:10 follow-up: 12 Changed 4 years ago by
Replying to goldfire:
In response to comment:5: Despite appearances to the contrary,
Coercible
is not a class. It is much more a special operator, right along the lines of~
.(Historical note: when we started developing the idea that became
Coercible
, we thought it would indeed be a normal class, but with compiler-generated instances. And it started life that way. But when pushed, the limitations of the class-based solver became too much, and soCoercible
evolved. The code in GHC that solvesCoercible
constraints is closely tied to solving of normal equality constraints, and not at all related to the code that solves class constraints.)Perhaps the user manual should be updated to reflect this fact about
Coercible
.
Thanks for the explanation! An explanation of the subtleties when using Coercible in the manual would certainly help.
Another related counterintuitive fact is that coerce itself works fine with the recursive newtype, the following works:
import Data.Coerce (coerce, Coercible) data X a --doCoerce :: Coercible a (X a) => a -> X a --doCoerce = coerce newtype Y = Y (X Y) test :: Y -> X Y test = coerce
but it see no way of writing doCoerce in a way that makes ghc 7.10 happy.
comment:11 follow-up: 13 Changed 4 years ago by
Richard , would it be unreasonable to support recursive newtypes where the occurrences of the newtype are all in phantom positions?
comment:12 Changed 4 years ago by
Replying to inaki:
but it see no way of writing doCoerce in a way that makes ghc 7.10 happy.
Well, the "surprising"
doCoerce :: Coercible a (X b) => a -> X a doCoerce = coerce
definition works in 7.10, but this does not work in 7.8, which I also want to support in my code if at all possible.
comment:13 Changed 4 years ago by
Replying to nomeata:
Richard , would it be unreasonable to support recursive newtypes where the occurrences of the newtype are all in phantom positions?
In a word: maybe. Though I haven't actually sat down to prove it, I very strongly suspect that solving for Coercible
is undecidable in the presence of recursive newtypes. In effect, we are solving for equirecursive type equality. This can be done, but the algorithm I have to hand (from Pierce's TAPL, Chapter 21) requires (translating to the language of Coercible
) that there be only one way to decompose an equality. But that's not true here! If we have [W] N a ~R N b
, where N
is a newtype, there are two ways forward: unwrap the newtype and try again, or look at the type parameters a
and b
(according to N
's parameter's role). So Pierce's algorithm doesn't work out.
We are left, then, with an incomplete algorithm. I'm confident that we could keep adding special cases to this algorithm to cover yet-weirder scenarios, but I think it's best to wait until we have a better motivation. (This ticket doesn't qualify, because there is a better way to do what the author wants.)
comment:14 Changed 4 years ago by
Differential Rev(s): | → Phab:D1263 |
---|---|
Status: | new → patch |
comment:16 Changed 4 years ago by
Milestone: | → 7.10.3 |
---|---|
Status: | patch → merge |
Test Case: | → typecheck/should_fail/T10715{,b} |
Merge only if convenient -- this does nothing but improve error messages.
comment:18 Changed 4 years ago by
Resolution: | → fixed |
---|---|
Status: | merge → closed |
Interesting. HEAD reports
which is even more confusing!
Here's what is happening
Coercible a ty
as a representational equality constrainta ~R ty
.a ~R ty
, it tries to rewrites other constraints mentioninga
, by replacinga
withty
.ty
mentionsa
, so we could rewrite forever; a kind of occurs-check problem. And indeed, if we had something like we really wouldn't expect much to happen because the constraint can't possibly be satisfied.a ~R X b
, we CAN use it to rewrite the wanted constraint, to getX b ~R X a
. And that is soluble by decomposition becauseX
's first argument is phantom. Hence your "Surprisingly to me" discovery.Coercible
? That would at least give a better error message than "can't deduce A from A"!Y
in this strange recursive way. Why not do this?