
#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