#9821: DeriveAnyClass support for higher-kinded classes + some more comments -------------------------------------+------------------------------------- Reporter: dreixel | Owner: dreixel Type: bug | Status: patch Priority: normal | Milestone: 8.2.1 Component: Compiler | Version: 7.9 Resolution: | Keywords: Generics Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #5462, #9968, | Differential Rev(s): Phab:D2961 #12144 | Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): This is respoinding to [https://phabricator.haskell.org/D2961#inline-25611], concerning the way to use implication constraints to simplify the `DeriveAnyClass` implementation. The original idea is in [https://phabricator.haskell.org/D2961#inline-25543], where I said: I think it would help to explain more carefully what is happening here. How come we don't need to look at the data constructors any more? Example: {{{ class Foo a where bar :: Ix b => a -> b -> String default bar :: (Show a, Ix b) => a -> b -> String bar x y = show x baz :: Eq a => a -> a -> Bool default baz :: (Ord a, Show a) => a -> a -> Bool baz x y = compare x y == EQ }}} Given {{{ deriving instance Foo (Maybe d) }}} we behave as if you had written {{{ instance ??? => Foo (Maybe d) where {} }}} (that is, using the default methods from the class decl), and that in turn means {{{ instance ??? => Foo (Maybe d) where bar = $gdm_bar baz = $gdm_baz }}} where {{{ $gdm_bar :: forall a. Foo a => forall b. (Show a, Ix b) => a -> b -> String }}} is the generic default method defined by the class declaratation. Our task is to figure out what "???" should be. Answer: enough constraints to satisfy the Wanteds arising from the calls of $gdm_bar and $gdm_baz. So we end up with two sets of constraints to simplify: {{{ bar: (Givens: [Ix b], Wanteds: [Show (Maybe d), Ix b]) baz: (Givens: [Eq (Maybe d)], Wanteds: [Ord (Maybe d), Show (Maybe d)]) }}} Important: note that * the Givens come from the ordinary method type, while * the Wanteds come from the generic method. These are just implication constraints. We can combine them into a single constraint: {{{ (forall b. Ix b => Show (Maybe d), Ix b) /\ (forall . Eq (Maybe d) => Ord (Maybe d), Show (Maybe d)) }}} Notice that the type variables from the head of the instance decl (just `d` in this case) are global to this constraint, but any local quantification of the generic default method (e.g. `b` in the case of `bar`) are locally scoped to each implication, as they obviously should be. Now we solve this constraint, getting the residual constraint (RC) {{{ (forall b. Ix b => Show d) /\ (forall . Eq (Maybe b) => Ord d, Show d) }}} Now we need to hoist those constraints out of the implications to become our candidates for the "???". That is done by `approximateWC`, which will return {{{ (Show d, Ord d, Show d) }}} Now we can use `mkMinimalBySCs` to remove superclasses and duplicates, giving {{{ (Show d, Ord d) }}} And that's what we need for the "???". -------------- But we aren't done yet! Suppose we had written {{{ bar :: a -> b -> String default bar :: (Show a, C a b) => a -> b -> String }}} I've replaced `Ix b` by `C b` and I've removed it from the vanilla sig for `Bar`. Now the implication constraint will be {{{ forall b. () => Show (Maybe d), C (Maybe d) b }}} Suppose we have `instance Read p => C (Maybe p) q`. Then after simplification, we get the residual constraint (RC): {{{ forall b. () => (Show d, Read d) }}} and all is well. But suppose we had no such instance, or we had an instance like `instance C p q => C (Maybe p) q`. Then we'd finish up with the residual consraint (RC): {{{ forall b. () => (Show d, C d b) }}} and now `approximateWC` will produce only `Show d` from this, becuase `(C d b)` is captured by the `forall b`. What do to? Easy! Once we have decided "???" should be CX, say, just emit this implication (to be solved later): {{{ forall d. CX => RC }}} where RC is the residual constraint we computed earlier. Bingo! From CX we'll be able to solve all the constraints that `approximateWC` extracted, and we'll be left with the error that we want to report for that `(C d b)` constraint. ------------------ This may seem complicated, but it's '''exactly what happens in `TcSimplify.simplifyInfer`'''. It does a bit more besides (figuring out what type variables to quantify over), but it makes a good guide. We might ultimately wat to share code, but for now I think it's easier to do one step at a time. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9821#comment:14 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler