#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 Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Iceland_jack): I think Richard was collecting examples of the `Coercible` solver wrt completeness -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15683#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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 Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (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`. [https://www.microsoft.com/en-us/research/publication/safe-coercions/ The paper] explains all this in some details. I don't see a decently feasibly way to fix this, I'm afraid. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15683#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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