Opened 12 months ago

Last modified 12 months ago

#15683 new bug

coerce fails for Coercible type families

Reported by: Iceland_jack Owned by:
Priority: normal Milestone: 8.6.1
Component: Compiler Version: 8.6.1
Keywords: TypeFamilies, Coercible Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

I want to bring attention to this reddit post that boils down to

type family   X a
type instance X Int  = String
type instance X Bool = String

data T a = T (X a)

but not being able to coerce

coerce :: T Int -> T Bool

This gives the error “Couldn't match type ‘Int’ with ‘Bool’ arising from a use of ‘coerce’”.

Change History (5)

comment:1 Changed 12 months ago by Iceland_jack

I think Richard was collecting examples of the Coercible solver wrt completeness

comment:2 Changed 12 months ago by sam-barr

For reference, I (the OP of the reddit post) encountered this issue when trying to use idioms introduced in Trees That Grow. It would be useful to be able to coerce subtrees without explicit recursion when no further manipulation is required.

comment:3 Changed 12 months ago by simonpj

This is by design. You are expecting T Int and T Bool to be representationally equal because if you look at every field of every constructor of T, and reduce every type-family application therein, on the particular argument types Int and Bool, then the answers are reprsentationally equal. Quite true! But this could be laborious if T had many constructors

data T a = T1 (X a )
         | T2 [Y a] (Z [a])
         ..etc...

If you add type instance X Char = Char, then certainly T Int is not coercible to T Char, so that check would have to be done for every individual instantation -- and recursively so.

Instead, the type system analyses the data type declaration for T computes a single summary -- the "role signature" of T --that decides, one and for all, when (T t1) is representationally equal to T t2.

In this case, because of the possibility of type instance T Char = Char, the decision is that T t1 is coercible to T t2 only if t1 is (nominally) equal to t2.

The paper explains all this in some details. I don't see a decently feasibly way to fix this, I'm afraid.

comment:4 Changed 12 months ago by RyanGlScott

I think what you likely want is the ability to declare type families that aren't nominal in their arguments. Something like:

type role X representational
type family X a

To be clear, GHC doesn't currently grant the ability to do this, but if it hypothetically did, then this would solve your problem. This is the scope of #8177. I'd go as far to say that this ticket is a duplicate of that one—do you agree?

comment:5 Changed 12 months ago by goldfire

Keywords: Coercible added

I'm afraid I disagree with comment:4. That's a related concern, but different.

I think the solution to this problem is to have a lattice of roles. When we say, e.g., type role T nominal representational phantom, what we mean is:

  • T a b c is representationally equal to T d e f if a is nominally equal to d, b is representationally equal to e, and c is phantomly equal to f.

What you want to say here is

  • X a is representationally equal to X b if F a is representationally equal to F b.

We can imagine something like type role X representational(F) that means the phrase above. This could be checked easily. But it would need to come with a theory of GHC core for which we can prove type safety -- not a low bar.

So, it's conceivable that some research could produce what you want, but it's out of reach for now.

Note that this is not an infelicity of the solver, but an infelicity of the theory. (By contrast, #8177 is "just engineering" -- I don't think we'd need a new formal proof of safety to do it.)

Note: See TracTickets for help on using tickets.