#9117: Coercible constraint solver misses one -------------------------------------+------------------------------------ Reporter: goldfire | Owner: nomeata Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (by goldfire): Replying to [comment:5 nomeata]:
we don’t run into dead ends if we do on or the other first.
I don't agree here. Say we have {{{ newtype Phant a = MkPhant Char type role Phant representational ex1 :: Phant Bool ex1 = coerce (MkPhant 'x' :: Phant Int) }}} This should succeed if we use newtype-unwrapping instances first but should fail if we use the congruence case first. And, indeed, it fails! I think it should succeed. Regardless of what we decide to do about the original feature requested, I think the failure of this example is a proper bug. I believe that if we try the newtype-unwrapping instances first, the algorithm would be sound. Why? Because the congruence case can never be more powerful than the newtype-unwrapping case, due to role inference. That is, the roles on any type parameters of the newtype can never be more permissive than the roles on its representation type. So, we actually ''already'' have an ordering dependence on the cases, in order to avoid dead ends -- but we didn't realize it! Is there a problem with adding one more layer to this? :) For use cases, see [https://github.com/ekmett/roles/blob/master/src/Data/Roles.hs here], some experimentation Edward K has done regarding tracking roles in type variables. He has to use `eta` in a fair number of constructions. Fixing the original ticket would allow these to be proven sound instead of relying on `unsafeCoerce`. And, in response to Simon, yes that's true that the situation might change, but I don't see how that's problematic. These instances are intentionally "incoherent", so we are robust in the presence of a change in exactly ''how'' the instance is solved for. The "changed situation" shouldn't make a previously-allowable coercion become otherwise. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9117#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler