#8503: New GeneralizedNewtypeDeriving check still isn't permissive enough -------------------------------------+------------------------------------ Reporter: goldfire | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.7 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): Hold the phone! There is an easier solution to the original problem! In my first comment, I wanted a coercion `co :: forall (a :: *). Maybe (Maybe a) ~R NTMaybe (NTMaybe a)`, and then I proposed a possible value of that type that was ill-roled. But, here is a well-roled value: {{{ co = co1 ; co2 co1 :: forall (a :: *). Maybe (Maybe a) ~R Maybe (NT a) co1 = forall (a :: *). Maybe (sym NTCo <a>_N) co2 :: forall (a :: *). Maybe (NT a) ~R NT (NT a) co2 = forall (a :: *). sym NTCo <NT a>_N }}} If we convert the pieces one at a time and then use transitivity, we're all OK. I remember battling against this problem over the summer. So, now we have a new question: how to get GHC to find this solution? Luckily, we happen to have a solver lying around that does just that: the `Coercible` mechanism. I imagine we could get the GND code to just call the `Coercible` code for each method. In fact, I considered this approach when improving the GND mechanism a few weeks ago, but thought it was overkill. My guess is that this would Just Work, when implemented. It might simplify the code a bit, too, but be somewhat less efficient (at compile time) at doing GND. I think this is reasonable. Taking the idea a bit further, what if the `Coercible` mechanism can't derive a coercion for a particular method? It would have to produce unsolved `Coercible` constraints... which we could just add to the constraints on the GND instance! This would allow more GND's to work than we had hoped for, such as this example: {{{ type family F a class C a where meth :: a -> F a type instance F Int = Bool class C Int where meth = (> 0) type instance F Age = Bool newtype Age = MkAge Int deriving C -- just works, no extra constraints because F Age = F Int type instance F [a] = a class C [a] where meth = head type instance F (List a) = Int newtype List a = MkL [a] deriving C -- this would create an instance with head "instance (Coercible a Int) => C (List a) where ..." }}} This all seems quite reasonable behavior, though we would want to make sure we don't produce constraints like `Coercible Int Bool`. Thoughts? Is this a good plan? We could always, as a first pass, implement GND in terms of `Coercible` and fail if there are any unsolved constraints, working for `C Age` above but not `C (List a)`. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/8503#comment:9> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler