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 inaki)

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 inaki

Description: modified (diff)

comment:2 Changed 4 years ago by nomeata

Cc: goldfire added

comment:3 Changed 4 years ago by simonpj

Interesting. HEAD reports

T10715.hs:8:13: error:
    Could not deduce: Coercible a (X a)
    from the context: Coercible a (X a)

which is even more confusing!

Here's what is happening

  • GHC treats Coercible a ty as a representational equality constraint a ~R ty.
  • Given an equlity a ~R ty, it tries to rewrites other constraints mentioning a, by replacing a with ty.
  • But here it can't do that, because ty mentions a, so we could rewrite forever; a kind of occurs-check problem. And indeed, if we had something like
    f :: (a ~ [a]) => blah
    
    we really wouldn't expect much to happen because the constraint can't possibly be satisfied.
  • However, if the given equality is a ~R X b, we CAN use it to rewrite the wanted constraint, to get X b ~R X a. And that is soluble by decomposition because X's first argument is phantom. Hence your "Surprisingly to me" discovery.
  • If you write a type signature like
    f :: (a ~ [a]) => blah
    
    you get an error like
    T10715.hs:15:8: error:
        Couldn't match type ‘a’ with ‘[a]’
        ‘a’ is a rigid type variable bound by
            the type signature for: foo :: (a ~ [a]) => a -> [a] -> Bool
            at T10715.hs:15:8
        Inaccessible code in
          the type signature for: foo :: (a ~ [a]) => a -> [a] -> Bool
    
    Maybe we should do the same for Coercible? That would at least give a better error message than "can't deduce A from A"!
  • 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
    

comment:4 in reply to:  3 Changed 4 years ago by goldfire

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 in reply to:  3 Changed 4 years ago by inaki

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 Changed 4 years ago by 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)

comment:7 Changed 4 years ago by goldfire

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 in reply to:  6 Changed 4 years ago by inaki

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.

Last edited 4 years ago by inaki (previous) (diff)

comment:9 Changed 4 years ago by simonpj

OK. So let's fix c2hs!

comment:10 in reply to:  7 ; Changed 4 years ago by inaki

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

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 Changed 4 years ago by nomeata

Richard , would it be unreasonable to support recursive newtypes where the occurrences of the newtype are all in phantom positions?

comment:12 in reply to:  10 Changed 4 years ago by inaki

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 in reply to:  11 Changed 4 years ago by goldfire

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 goldfire

Differential Rev(s): Phab:D1263
Status: newpatch

comment:15 Changed 4 years ago by Richard Eisenberg <eir@…>

In 2f9809ef/ghc:

Slightly better `Coercible` errors.

This makes two real changes:
 - Equalities like (a ~R [a]) really *are* insoluble. Previously,
   GHC refused to give up when an occurs check bit on a representational
   equality. But for datatypes, it really should bail.

 - Now, GHC will sometimes report an occurs check error (in cases above)
   for representational equalities. Previously, it never did.

This "fixes" #10715, where by "fix", I mean clarifies the error message.
It's unclear how to do more to fix that ticket.

Test cases: typecheck/should_fail/T10715{,b}

comment:16 Changed 4 years ago by goldfire

Milestone: 7.10.3
Status: patchmerge
Test Case: typecheck/should_fail/T10715{,b}

Merge only if convenient -- this does nothing but improve error messages.

comment:17 Changed 4 years ago by bgamari

Merged to ghc-7.10.

comment:18 Changed 4 years ago by bgamari

Resolution: fixed
Status: mergeclosed
Note: See TracTickets for help on using tickets.