#15683: coerce fails for Coercible type families -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.6.1 Resolution: | Keywords: TypeFamilies, | Coercible Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by goldfire): * keywords: TypeFamilies => TypeFamilies, Coercible * related: #8177 => Comment: 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.) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15683#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler