Role: ~# should be ~R#

The following coercion showed up in Core. Richard Eisenberg pointed out that the ~# should be ~R#.

  <Tree N0 Int>_R -> NTCo:Sum[0] <Int>_R
    :: (Tree N0 Int -> Sum Int) ~# (Tree N0 Int -> Int)

I can dig up more information if needed.

Trac metadata

Trac field	Value
Version	7.8.2
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC	eir@cis.upenn.edu
Operating system
Architecture

changed weight to 5

added Tbug Trac import labels

I can't say for sure (would need to reproduce), but I think that a coercion (co1 -> co2) is represented by a TyConAppCo, which in turn carries a role. So it looks as if the role on that TyConAppCo with (->) in the type constructor position is plain wrong.

Is this with your plugin, or is this plain GHC? How can we reproduce?

Simon

I asked Conal to post the report. The problem is just in the pretty-printer, which should produce ~R# if the coercion is representational (as it is, in this case).

assigned to @rae

OK, Richard, so you know what's going on and can fix? Thanks.

Simon

Patch on the way...

Trac metadata

Trac field	Value
Test case	→ roles/should_compile/Roles13

mentioned in commit e79e2c39

closed

Trac metadata

Trac field	Value
Resolution	Unresolved → ResolvedFixed

added Pnormal label