Richard , would it be unreasonable to support recursive newtypes where
#10715: Possible regression in Coercible a (X a) between 7.8 and 7.10 -------------------------------------+------------------------------------- Reporter: inaki | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.10.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Revisions: -------------------------------------+------------------------------------- Comment (by goldfire): Replying to [comment:11 nomeata]: the occurrences of the newtype are all in phantom positions? In a word: maybe. Though I haven't actually sat down to prove it, I very strongly suspect that solving for `Coercible` is undecidable in the presence of recursive newtypes. In effect, we are solving for equirecursive type equality. This can be done, but the algorithm I have to hand (from Pierce's TAPL, Chapter 21) requires (translating to the language of `Coercible`) that there be only one way to decompose an equality. But that's not true here! If we have `[W] N a ~R N b`, where `N` is a newtype, there are //two// ways forward: unwrap the newtype and try again, or look at the type parameters `a` and `b` (according to `N`'s parameter's role). So Pierce's algorithm doesn't work out. We are left, then, with an incomplete algorithm. I'm confident that we could keep adding special cases to this algorithm to cover yet-weirder scenarios, but I think it's best to wait until we have a better motivation. (This ticket doesn't qualify, because there is a better way to do what the author wants.) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10715#comment:13 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler