#14333: GHC doesn't use the fact that Coercible is symmetric -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.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 goldfire): This is a good point. The problem is that `(a b) ~R# (c d)` tells you nothing at all about the relationship between any of the variables `a`, `b`, `c`, and `d`. This isn't a restriction in the solver, but simply a truism of representational equality. So when GHC knows `(a b) ~R# (c d)`, it is too stupid to figure out `(c d) ~R# (a b)`. I can thus boil down the problem even further: {{{#!hs bad :: Coercible (a b) (c d) => c d -> a b bad = coerce }}} will fail to type-check. (The version with argument & result swapped works fine.) Could the solver work around this? Maybe, with sufficient cleverness. (Unlike my concerns around recursive newtypes, I think this may be an engineering issue, not undecidability.) I don't think it would be easy though, requiring some kind of flattening logic akin to what GHC does for type families. Do you have a concrete use case? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14333#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler