[GHC] #11008: GND with Type Families
#11008: GND with Type Families -------------------------------------+------------------------------------- Reporter: crockeea | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.10.2 Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- In the following code: {{{ {-# LANGUAGE TypeFamilies, FlexibleContexts, UndecidableInstances #-} class C r type family F r newtype Foo r = Foo r instance (C (F r), Eq r) => Eq (Foo r) newtype Bar r = Bar (Foo r) deriving (Eq) }}} GHC produces the error {{{ No instance for (C (F r)) arising from the 'deriving' clause of a data type declaration Possible fix: use a standalone 'deriving instance' declaration, so you can specify the instance context yourself When deriving the instance for (Eq (Bar r)) }}} If I enable `StandaloneDeriving`, I am able to derive the instance: `deriving instance (Eq (Foo r)) => Eq (Bar r)` [https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/deriving.htm... #newtype-deriving The docs] indicate that this is exactly the instance that should be generated by GND for `newtype T v1..vn = MkT (t vk+1..vn) deriving (C t1..tj)`, where my code uses the following parameters: {{{ T = Bar v1 = r n = 1 MkT = Bar t = Foo r k= 1 C = Eq j = 0 }}} and all of the conditions enumerated in the docs seem to be met. Furthermore, `Bar` seems to fit squarely into the format of `data T1` in section 7.5.1 of the same documentation, which indicates it should not need `StandaloneDeriving`. It seems that the type family constraint on the `Eq` instance for `Foo` is causing the problem, but it's not clear why I'm forced to write a standalone instance that is identical to the one that should be generated by GND. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11008 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11008: Difficulties around inferring exotic contexts -------------------------------------+------------------------------------- Reporter: crockeea | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.10.2 Resolution: | Keywords: 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 by design. GHC refuses to infer so-called exotic contexts, believing that sufficiently exotic contexts should be written by the user. This behavior is independent of whether GND or other `deriving` features are used. Here is an extreme example: {{{ data X a b = MkX (a -> b) deriving Eq }}} This fails, complaining about a missing `Eq (a -> b)` instance. (My choice of `data` vs. `newtype` is utterly irrelevant here.) But I can write this: {{{ deriving instance Eq (a -> b) => Eq (X a b) }}} Should GHC infer the context automatically here? I think not -- it masks a deeper problem. Now, returning to the original post: should GHC infer that context? It looks just like the example I just gave, where the context requires an `Eq` constraint on some other type constructor. It all boils down to yet another knob we can turn in the internals of GHC. It's a very easy knob to turn, with no interactions throughout the code. See the relevant function [https://github.com/ghc/ghc/blob/8f5ad1a009eddd05447ff8057792b4d03983cd35/com... here], with a Note directly above. If you can suggest a better setting for the knob, go right ahead. :) Regardless, we should document this in the manual somewhere, as it is all user-facing. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11008#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11008: Difficulties around inferring exotic contexts -------------------------------------+------------------------------------- Reporter: crockeea | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.10.2 Resolution: | Keywords: 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 crockeea): With the deriving clause, which instance does GHC try to create? 1. instance (Eq (Foo r)) => Eq (Bar r) 2. instance (C (F r), Eq r) => Eq (Bar r) If option 1, GHC has no business inspecting the constraints on the `Foo r` instance. If option 2, why? Is it due to [https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/deriving.htm... #newtype-deriving slower instances]? In either case, since I *have* a matching `Eq` instance for `Foo`, GHC should assume that I knew what I was doing when I wrote it, and just use it. This doesn't change the behavior when no matching instance is found, like in your example. Whatever the result, the docs definitely need to be clearer. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11008#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11008: Difficulties around inferring exotic contexts -------------------------------------+------------------------------------- Reporter: crockeea | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.10.2 Resolution: | Keywords: 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): Replying to [comment:2 crockeea]:
With the deriving clause, which instance does GHC try to create?
1. `instance (Eq (Foo r)) => Eq (Bar r)` 2. `instance (C (F r), Eq r) => Eq (Bar r)`
In either case, since I *have* a matching `Eq` instance for `Foo`, GHC should assume that I knew what I was doing when I wrote it, and just use it. This doesn't change the behavior when no matching instance is found,
Option 1. But it then tries to simplify the constraint, finding the minimal set of constraints that imply `Eq (Foo r)`. Here, minimal does not mean smallest, but instead minimal in a logical sense -- as in, the minimum set of assumptions that proves the desired constraint. So, option 1 very quickly becomes option 2. Note that if we didn't try to simplify, then you'd end up with constraints like `Eq (Maybe a)` a lot, and these would be rejected. like in your example. But you have no matching instance for `C (F r)`. So I'm not sure how GHC should recognize the difference. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11008#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11008: Difficulties around inferring exotic contexts -------------------------------------+------------------------------------- Reporter: crockeea | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.10.2 Resolution: | Keywords: 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 crockeea): Without knowing anything about the internals of GHC, it seems there are two ways to simplify instance contexts: either we "simplify and reject" if they are "exotic" (in the case of GND instances), or just "simplify and typecheck" (in the case of hand-written instances of any variety). So if an instance head matches (Eq (Foo r)), trigger the "simplify and typecheck" rather than "simplify and reject exotic constraints" behavior. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11008#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11008: Difficulties around inferring exotic contexts -------------------------------------+------------------------------------- Reporter: crockeea | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.10.2 Resolution: | Keywords: 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): I'm sorry -- I'm afraid I don't understand your last comment. Or, rather, my understanding leads me directly to the behavior we currently have: check derived instances for exotic contexts and reject if exotic, but skip the exotic-check for hand-written instances (including standalone- deriving). (Note that there is no GND in sight here -- just normal `deriving`.) Perhaps illustrate your idea with a few examples? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11008#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11008: Difficulties around inferring exotic contexts -------------------------------------+------------------------------------- Reporter: crockeea | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.10.2 Resolution: | Keywords: 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 crockeea): All I'm suggesting is that rather than the iterative process of 1. GHC writes an instance 2. GHC checks for a (single?) matching instance head for all constraints 3. GHC simplifies those constraints 4. Go to step 1 until minimal constraints found (which I refer to as the "simplify and reject" method), GHC could get to step 3, and then just continue to simplify the constraints ''without'' checking for matching instances on all ''simplified'' constraints (i.e. more like how a function (presumably) simplifies constraints, which I refer to as the "simplify and typecheck" method, where no rejection occurs if no matching instance is found). Thus GHC would still require a standalone instance for `data X a b = MkX (a -> b) deriving Eq` because step (in the first round) would fail. The idea is that the above process would allow auto-deriving when a single matching instance is found for the unsimplified context. In the case of overlapping or missing instances, I have no opinion on the behavior. Maybe this approach is too ad-hoc, but I think it would result in expected behavior. My main reasons for this are that 1. If there's a single instance in scope, GHC should assume I know how to use it. 2. Writing the standalone instance `deriving instance (Eq (Foo r)) => Eq (Bar r)` does ''nothing'' to help me understand the exotic nature of the instance. [Not that I feel like I want advice in this area, mind you. I want GHC to assume I know what I'm doing.] -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11008#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11008: Difficulties around inferring exotic contexts -------------------------------------+------------------------------------- Reporter: crockeea | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.10.2 Resolution: | Keywords: 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): Replying to [comment:6 crockeea]:
1. GHC writes an instance 2. GHC checks for a (single?) matching instance head for all constraints 3. GHC simplifies those constraints 4. Go to step 1 until minimal constraints found
I'm afraid I still don't understand. (I really don't! I'm not trying to be obtuse. It comes naturally.) Do you mean to go back to step 2? Then I think I understand.
(which I refer to as the "simplify and reject" method), GHC could get to step 3,
and then just continue to simplify the constraints ''without'' checking for matching instances on all ''simplified'' constraints (i.e. more like how a function (presumably) simplifies constraints, which I refer to as
But now I'm lost again. How could we jump to step 3 without going through step 2? Step 2, as I understand it, is the step that actually finds a matching instance head, from which we can simplify. Step 3 would require the output of step 2 as its input. To be concrete, suppose we have a constraint `Eq [(a, Int)]`. I understand step 2 as identifying the instance head `Eq [b]`, which then, in step 3, uses its constraint `Eq b` to simplify the original constraint to `Eq (a, Int)`. So step 2 seems vital. the "simplify and typecheck" method, where no rejection occurs if no matching instance is found). This seems to suggest just omitting the "exotic constraint" check. Because functions don't have that check. Otherwise, I don't see a difference between what goes on with `deriving` and what goes on with functions. The simplification algorithm looks the same to me.
Thus GHC would still require a standalone instance for `data X a b = MkX
The idea is that the above process would allow auto-deriving when a single matching instance is found for the unsimplified context. In the case of overlapping or missing instances, I have no opinion on the behavior.
Maybe this approach is too ad-hoc, but I think it would result in expected behavior.
My main reasons for this are that 1. If there's a single instance in scope, GHC should assume I know how to use it. 2. Writing the standalone instance `deriving instance (Eq (Foo r)) => Eq (Bar r)` does ''nothing'' to help me understand the exotic nature of
(a -> b) deriving Eq` because step (in the first round) would fail. Which step did you mean? the instance. [Not that I feel like I want advice in this area, mind you. I want GHC to assume I know what I'm doing.] This part makes more sense to me. But then, consider the following: {{{ data X a b = MkX (a -> b) deriving instance Eq (a -> b) => Eq (X a b) data Y a b = MkY (X a b) deriving Eq }}} My understanding tells me that this should work under your proposal. This is because `Y` uses `X`'s instance, which GHC assumes is appropriate. Maybe I can paraphrase your idea: 1. GHC generates a set of constraints appropriate for deriving a given class. (That is, for `deriving (Eq X)`, this would be `Eq (a -> b)`.) These are all considered "unsimplified" constraints. 2. GHC tries to simplify all constraints. Any constraint produced as an output of simplification is considered "simplified". This step repeats until it can make no more progress. 3. GHC checks the "unsimplified" constraints, if there are any left, to make sure they are not exotic. It does ''not'' check "simplified" constraints. 4. If there are no exotic "unsimplified" constraints, accept the declaration. Is that about right? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11008#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11008: Difficulties around inferring exotic contexts -------------------------------------+------------------------------------- Reporter: crockeea | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.10.2 Resolution: | Keywords: 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 crockeea): Replying to [comment:7 goldfire]:
I'm afraid I still don't understand. (I really don't! I'm not trying to be obtuse. It comes naturally.) I'm quite sure your confusion is my fault. It's hard for me to talk reasonably about this since I know so little about how it works.
Do you mean to go back to step 2? Then I think I understand. Yes, I did mean step 2.
But now I'm lost again. How could we jump to step 3 without going through step 2? Step 2, as I understand it, is the step that actually finds a matching instance head, from which we can simplify. Ah, that makes sense. (Told you I don't know what I'm saying!) So GHC doesn't simplify constraints in functions? This is where the confusion arises for me. I can write: `foo a@(Foo _) = a == a` and GHC is perfectly happy to infer the context.
This seems to suggest just omitting the "exotic constraint" check. Because functions don't have that check. Right! This is what I'm trying to get at.
Which step did you mean? Step 2, where we check for a matching instance head.
But then, consider the following:
{{{ data X a b = MkX (a -> b) deriving instance Eq (a -> b) => Eq (X a b)
data Y a b = MkY (X a b) deriving Eq }}}
My understanding tells me that this should work under your proposal. This is because `Y` uses `X`'s instance, which GHC assumes is appropriate. Under my proposal, GHC would accept your example. And this makes sense to me: GHC has (rightly) forced me to write an "explicit" instance for `X` (a standalone instance instead of an auto-derived one) which should tip me off that I'm doing something weird. At that point GHC has done its due diligence to warn me, it should then accept the instance for `Y` without question.
Maybe I can paraphrase your idea:
1. GHC generates a set of constraints appropriate for deriving a given class. (That is, for `deriving (Eq X)`, this would be `Eq (a -> b)`.) These are all considered "unsimplified" constraints. 2. GHC tries to simplify all constraints. Any constraint produced as an output of simplification is considered "simplified". This step repeats until it can make no more progress. 3. GHC checks the "unsimplified" constraints, if there are any left, to make sure they are not exotic. It does ''not'' check "simplified" constraints. 4. If there are no exotic "unsimplified" constraints, accept the declaration.
Is that about right? Well, almost. It seems that my original example would not be accepted with this algorithm because `C (F r)` can't be simplified, but also doesn't have a matching instance. I'll try one more time:
1. GHC generates a set of constraints for deriving a given class. (For example, `deriving (Eq X)` would generate the context `Eq (a -> b)`. For the purposes of this algorithm, let's just use this example. 2. GHC tries to simplify the constraint `Eq (a -> b)`. If it can, go to step 3. Otherwise, throw an error and require StandaloneDeriving. 3. GHC found a matching instance for `Eq (a -> b)` (is this equivalent to "GHC was able to simplify the constraint `Eq (a -> b)`"?). Assume that the instance `Eq (a -> b)` has already been simplified to something like `(C a b) => Eq (a -> b)`. Then rewrite the auto-generated instance `(Eq (a -> b)) => Eq (X a b)` to the ''already simplified'' instance `(C a b) => Eq (X a b)`, without doing **any** checks on constraints `(C a b)` at all. (They already typecheck, and since there is a matching instance, GHC will ignore anything exotic about it.) Thanks for your patience while I try to figure out what I mean! -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11008#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11008: Difficulties around inferring exotic contexts -------------------------------------+------------------------------------- Reporter: crockeea | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.10.2 Resolution: | Keywords: 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): I think our algorithms are the same. Mine accepts your original example, because it simplifies `Eq (Foo r)` to get `C (F r)`, so in my terminology, `C (F r)` is considered "simplified". Now that we have an idea of what we're talking about, we can think about whether or not it is actually a good idea. I'm inclined to think it is. One tiny, easily-surmountable wrinkle is that we'd need to check for `FlexibleContexts` and/or `UndecidableInstances` and/or ... before accepting the constraint. But that's fairly routine. I'd want Simon's opinion on this before rubber stamping it. And then there's the matter of implementation. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11008#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11008: Difficulties around inferring exotic contexts -------------------------------------+------------------------------------- Reporter: crockeea | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.10.2 Resolution: | Keywords: 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 simonpj): If you want an opinion, and you propose something different than what currently happens, can you write the wiki page? Selfishly I don't want to wade through the long thread to find out what you are discussing. Thanks Simon -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11008#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11008: Difficulties around inferring exotic contexts -------------------------------------+------------------------------------- Reporter: crockeea | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.10.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * cc: RyanGlScott (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11008#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11008: Difficulties around inferring exotic contexts -------------------------------------+------------------------------------- Reporter: crockeea | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.10.2 Resolution: | Keywords: deriving Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #15868 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * keywords: => deriving * related: => #15868 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11008#comment:12 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC