[GHC] #8851: Standalone deriving and GND behave differently
#8851: Standalone deriving and GND behave differently ------------------------------------+------------------------------------- Reporter: simonpj | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.6.3 Keywords: | Operating System: Unknown/Multiple Architecture: Unknown/Multiple | Type of failure: None/Unknown Difficulty: Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | ------------------------------------+------------------------------------- Sergey Tromimovich writes: Trying to build random packages with fresh ghc-7.8.1-rc2 I've come up with a strange bit: https://github.com/trofi/Idris- dev/commit/9f93122ba1aa075c2fa1555fea68a6c403697e04 Is it an intended behaviour that standalone deriving (A) {{{ deriving instance Parsing IdrisInnerParser }}} is capable of doing more, than a deriving clause (B) {{{ newtype IdrisInnerParser a = IdrisInnerParser { runInnerParser :: Parser a } deriving (Parsing) }}} where the class is defined thus {{{ class Alternative m => Parsing m where .... notFollowedBy :: (Monad m, Show a) => m a -> m () notFollowedBy p = try ((try p >>= unexpected . show) <|> pure ()) }}} The error message from the (B) is {{{ [50 of 75] Compiling Idris.ParseHelpers ( src/Idris/ParseHelpers.hs, dist/build/Idris/ParseHelpers.o ) src/Idris/ParseHelpers.hs:40:97: Could not coerce from ‘Monad Parser’ to ‘Monad IdrisInnerParser’ because the first type argument of ‘Monad’ has role Nominal, but the arguments ‘Parser’ and ‘IdrisInnerParser’ differ arising from the coercion of the method ‘notFollowedBy’ from type ‘forall a. (Monad Parser, Show a) => Parser a -> Parser ()’ to type ‘forall a. (Monad IdrisInnerParser, Show a) => IdrisInnerParser a -> IdrisInnerParser ()’ Possible fix: use a standalone 'deriving instance' declaration, so you can specify the instance context yourself When deriving the instance for (Parsing IdrisInnerParser) }}} Answer: no they should not behave differently. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8851 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8851: Standalone deriving and GND behave differently --------------------------------------------+------------------------------ Reporter: simonpj | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type checker) | Version: 7.8.1-rc1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: None/Unknown | Unknown/Multiple Test Case: | Difficulty: Unknown Blocking: | Blocked By: | Related Tickets: --------------------------------------------+------------------------------ Changes (by nomeata): * cc: mail@… (added) * version: 7.6.3 => 7.8.1-rc1 * component: Compiler => Compiler (Type checker) Comment: I’m trying to wrap my head around which of the two behaviours is correct. Richard, can you enlighten me? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8851#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8851: Standalone deriving and GND behave differently --------------------------------------------+------------------------------ Reporter: simonpj | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type checker) | Version: 7.8.1-rc1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: None/Unknown | Unknown/Multiple Test Case: | Difficulty: Unknown Blocking: | Blocked By: | Related Tickets: --------------------------------------------+------------------------------ Comment (by simonpj): To me rejection (B) looks right. After all, is it safe to coerce between `(Monad Parser)` to `(Monad InnerIdrisParser)`? They might have very different instances. See Section 3.4 of the [http://research.microsoft.com/en- us/um/people/simonpj/papers/ext-f/ Safe Coercions paper]. Simon -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8851#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8851: Standalone deriving and GND behave differently --------------------------------------------+------------------------------ Reporter: simonpj | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type checker) | Version: 7.8.1-rc1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: None/Unknown | Unknown/Multiple Test Case: | Difficulty: Unknown Blocking: | Blocked By: | Related Tickets: --------------------------------------------+------------------------------ Comment (by nomeata): That’s my gut feeling as well. But what if the type checker resolves the constraints in `forall a. (Monad IdrisInnerParser, Show a) => IdrisInnerParser a -> IdrisInnerParser ()’` before coerce is being called, so that it would only have to coerce `forall a. (Show a) => IdrisInnerParser a -> IdrisInnerParser ()’, and that would be fine. This is probably what is happening in case (A) (otherwise the result would not role-type-check). -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8851#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8851: Standalone deriving and GND behave differently --------------------------------------------+------------------------------ Reporter: simonpj | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type checker) | Version: 7.8.1-rc1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: None/Unknown | Unknown/Multiple Test Case: | Difficulty: Unknown Blocking: | Blocked By: | Related Tickets: --------------------------------------------+------------------------------ Changes (by goldfire): * owner: => goldfire Comment: I took a briefish look at this yesterday and am somewhat confused, but I'll take a closer look and submit a fix in the next few days. I actually think acceptance is correct because of Joachim's (nomeata's) reasoning. It is indeed unsafe to convert a ''dictionary'' for `Monad Parser` to a ''dictionary'' for `Monad InnerIdrisParser`. But, the `notFollowedBy` function takes this dictionary as a parameter, and so coherence is somehow not an issue. Even as I'm writing this, I don't fully believe it, but my hunch is still that "accept" is the right answer. I'll elaborate more when I can put some more consecutive cycles into this. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8851#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8851: Standalone deriving and GND behave differently --------------------------------------------+------------------------------ Reporter: simonpj | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type checker) | Version: 7.8.1-rc1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: None/Unknown | Unknown/Multiple Test Case: | Difficulty: Unknown Blocking: | Blocked By: | Related Tickets: --------------------------------------------+------------------------------ Comment (by simonpj): Aha. Right. Suppose we have {{{ class C r where op :: forall a. theta => op_ty newtype T a = MkT rep_ty deriving( C ) }}} Then the both newtype deriving and standalone deriving should succeed if this will typecheck {{{ instance C rep_ty => C (T a) where op = coerce (op :: op_ty[rep_ty/r] }}} When will this typecheck? Notice that we instantiate `op` (like any other variable occurrence) at its occurrence site, which throws the instantiated `theta` into the constraints to be solved. Answer: when * `Coercible (op_ty[rep_ty/r]) (op_ty[N a/r])` holds * Assuming `C rep_ty` and `theta[T a/r]`, we can prove `theta[rep_ty/r]` In this case, `theta[rep_ty/r]` is simply `Monad IdrisInlineParser` which holds from a top-level instance, not from any of the local "assuming.." parts. So I think the `deriving` mechanism should check this second bullet. I believe that "standalone deriving" is deliberately [http://www.haskell.org/ghc/docs/latest/html/users_guide/deriving.html #stand-alone-deriving more gung-ho]: it simply generates the boilerplate and tries to typecheck it. The `deriving` clause makes checks up-front so that the generated code is certain to typecheck. We just need to fix those up-front checks. Thanks for looking at this Richard. Simon -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8851#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8851: Standalone deriving and GND behave differently --------------------------------------------+------------------------------ Reporter: simonpj | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type checker) | Version: 7.8.1-rc1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: None/Unknown | Unknown/Multiple Test Case: | Difficulty: Unknown Blocking: | Blocked By: | Related Tickets: --------------------------------------------+------------------------------ Changes (by slyfox): * cc: slyfox@… (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8851#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8851: Standalone deriving and GND behave differently --------------------------------------------+------------------------------ Reporter: simonpj | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type checker) | Version: 7.8.1-rc1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: None/Unknown | Unknown/Multiple Test Case: | Difficulty: Unknown Blocking: | Blocked By: | Related Tickets: --------------------------------------------+------------------------------ Comment (by goldfire): I agree fully with Simon's analysis. But, the solution to this problem gets involved with areas of GHC that I'm not terribly familiar with, and I need some guidance before proceeding. The interesting bit is `simplifyDeriv` in !TcDeriv, which has this chunk: {{{ ; wanted <- mapM (\(PredOrigin t o) -> newFlatWanted o (substTy skol_subst t)) theta ; (residual_wanted, _ev_binds1) <- solveWantedsTcM (mkFlatWC wanted) }}} I can understand quite clearly what this is doing. It's creating a new `wanted` constraint for each (skolemised) predicate in `theta`. Then, we throw the set of wanteds into the constraint solver and see what comes out. Processing that happens below here figures out if `residual_wanted` indicates success or failure. The problem is that we now wish to do all of the above with some assumptions. My first thought was to create an implication constraint for this, but it's not clear to me the right way to set it up. I found `checkConstraints`, which seems quite relevant, but I'm not sure what to pass for its `thing_inside`. Change the `newFlatWanted` to something that ''emits'' the wanteds? Then, what do I pass to `solveWantedsTcM`? Do I really want `solveWantedsTcMWithEvBinds`? But, that functions takes an `EvBindsVar`, and `checkConstraints` gives me a `TcEvBinds`, which may or may not contain the `EvBindsVar`. (I believe that, in this case, it ''will'' always contain the `EvBindsVar`, but this seems like a silly thing to rely on.) In any case, I'm not sure which lever will drive the ship to safety and which knob will sink the whole lot. Any advice is appreciated, or if you're short of time, you're welcome to yank this bug from me and fix it yourself. In any case, I will need to learn about these interactions quite soon in other work, so the timing is perfect. Thanks! -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8851#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8851: Standalone deriving and GND behave differently
--------------------------------------------+------------------------------
Reporter: simonpj | Owner: goldfire
Type: bug | Status: new
Priority: normal | Milestone:
Component: Compiler (Type checker) | Version: 7.8.1-rc1
Resolution: | Keywords:
Operating System: Unknown/Multiple | Architecture:
Type of failure: None/Unknown | Unknown/Multiple
Test Case: | Difficulty: Unknown
Blocking: | Blocked By:
| Related Tickets:
--------------------------------------------+------------------------------
Comment (by Richard Eisenberg
#8851: Standalone deriving and GND behave differently -------------------------------------------------+------------------------- Reporter: simonpj | Owner: Type: bug | goldfire Priority: normal | Status: new Component: Compiler (Type checker) | Milestone: Resolution: | Version: Operating System: Unknown/Multiple | 7.8.1-rc1 Type of failure: None/Unknown | Keywords: Test Case: | Architecture: deriving/should_compile/T8851 | Unknown/Multiple Blocking: | Difficulty: | Unknown | Blocked By: | Related Tickets: -------------------------------------------------+------------------------- Changes (by goldfire): * testcase: => deriving/should_compile/T8851 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8851#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8851: Standalone deriving and GND behave differently -------------------------------------------------+------------------------- Reporter: simonpj | Owner: Type: bug | Status: new Priority: normal | Milestone: 7.8.1 Component: Compiler (Type checker) | Version: Resolution: | 7.8.1-rc1 Operating System: Unknown/Multiple | Keywords: Type of failure: None/Unknown | Architecture: Test Case: | Unknown/Multiple deriving/should_compile/T8851 | Difficulty: Blocking: | Unknown | Blocked By: | Related Tickets: -------------------------------------------------+------------------------- Changes (by goldfire): * owner: goldfire => * milestone: => 7.8.1 Comment: I'm giving up ownership of this ticket as I'm not sure how to proceed without guidance. With some advice in hand, I'm happy to take this on again. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8851#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8851: Standalone deriving and GND behave differently -------------------------------------------------+------------------------- Reporter: simonpj | Owner: Type: bug | Status: new Priority: normal | Milestone: 7.8.1 Component: Compiler (Type checker) | Version: Resolution: | 7.8.1-rc1 Operating System: Unknown/Multiple | Keywords: Type of failure: None/Unknown | Architecture: Test Case: | Unknown/Multiple deriving/should_compile/T8851 | Difficulty: Blocking: | Unknown | Blocked By: | Related Tickets: -------------------------------------------------+------------------------- Comment (by simonpj): I've reflected on this some more. First, standalone deriving has always been more aggressive than a deriving clause: * A deriving clause makes conservative checks that should ensure that the generated boilerplate code never fails to type check. * Standalone deriving makes weaker checks (enough to ensure that the boilerplate code can be generated in the first place), but then generates the code and risks that it might not typecheck. The reason for this is that it's too hard to predict exactly what will succeed; see #3102 for the origin of this change. The only down-side of the standalone-deriving story is that the error message may refer to (generated boilerplate) code that you didn't write. You could also argue that it's confusing to conflate (a) standalone vs attached-to-decl, with (b) conservative vs aggressive. Well, yes. After all, as you'll see from the description of this ticket, it confused even me and I wrote the implementation! Second, a deriving clause is not given the context of the instance declaration, so it has to infer it: {{{ data T a = T1 [a] | T2 (Tree a) deriving( Ord ) generates instance ( ??? ) => Ord (T a) where ... }}} We have to infer the `???`. It does this by generating (in this example) an `Ord` constraint for each constructor argument (in this case `(Ord [a], Ord (Tree a))`) and simplifying. But what we want for this `Coercible` case is not to ''infer'' a context, but rather to ''check'' that certain wanted constraints can be deduced from other given constraints, and to do so method-by-method. There is no code path to do this right now. Bottom line: we can always make the (necessarily-conservative) deriving- clause checks more permissive, but doing so adds code and complexity. I'm inclined instead to declare this case to be an example of where you must use a standalone-deriving clause. In short I propose no action. I'll update the user manual (which does mention this point) be more explicit. Simon -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8851#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8851: Standalone deriving and GND behave differently
-------------------------------------------------+-------------------------
Reporter: simonpj | Owner:
Type: bug | Status: new
Priority: normal | Milestone: 7.8.1
Component: Compiler (Type checker) | Version:
Resolution: | 7.8.1-rc1
Operating System: Unknown/Multiple | Keywords:
Type of failure: None/Unknown | Architecture:
Test Case: | Unknown/Multiple
deriving/should_compile/T8851 | Difficulty:
Blocking: | Unknown
| Blocked By:
| Related Tickets:
-------------------------------------------------+-------------------------
Comment (by Simon Peyton Jones
#8851: Standalone deriving and GND behave differently -------------------------------------------------+------------------------- Reporter: simonpj | Owner: Type: bug | Status: new Priority: normal | Milestone: 7.8.1 Component: Compiler (Type checker) | Version: Resolution: | 7.8.1-rc2 Operating System: Unknown/Multiple | Keywords: Type of failure: None/Unknown | Architecture: Test Case: | Unknown/Multiple deriving/should_compile/T8851 | Difficulty: Blocking: | Unknown | Blocked By: | Related Tickets: -------------------------------------------------+------------------------- Changes (by thoughtpolice): * version: 7.8.1-rc1 => 7.8.1-rc2 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8851#comment:13 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8851: Standalone deriving and GND behave differently -------------------------------------------------+------------------------- Reporter: simonpj | Owner: Type: bug | Status: new Priority: normal | Milestone: 7.8.1 Component: Compiler (Type checker) | Version: Resolution: | 7.8.1-rc2 Operating System: Unknown/Multiple | Keywords: Type of failure: None/Unknown | Architecture: Test Case: | Unknown/Multiple deriving/should_compile/T8851 | Difficulty: Blocking: | Unknown | Blocked By: | Related Tickets: -------------------------------------------------+------------------------- Comment (by goldfire): You have a better perspective on the difficulty of implementation here, so I'm happy enough to agree. It does seem a little silly that we can accept `deriving instance Parsing MyParser` (with no context at all) but not `newtype MyParser ... deriving Parsing`. But, this behavior is fully consistent with the articulation of the two `deriving` features, so there's nothing wrong with it. And, keeping the code simpler when the fix for users is so trivial is a good thing. Thanks for taking another look. We should modify the test case to reflect this change. I can do that later this week when I spend some time working on GHC. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8851#comment:14 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8851: Standalone deriving and GND behave differently -------------------------------------------------+------------------------- Reporter: simonpj | Owner: Type: bug | Status: merge Priority: normal | Milestone: 7.8.1 Component: Compiler (Type checker) | Version: Resolution: | 7.8.1-rc2 Operating System: Unknown/Multiple | Keywords: Type of failure: None/Unknown | Architecture: Test Case: | Unknown/Multiple deriving/should_compile/T8851 | Difficulty: Blocking: | Unknown | Blocked By: | Related Tickets: -------------------------------------------------+------------------------- Changes (by simonpj): * status: new => merge Comment: Please merge the documentation changes to 7.8 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8851#comment:15 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8851: Standalone deriving and GND behave differently
-------------------------------------------------+-------------------------
Reporter: simonpj | Owner:
Type: bug | Status: merge
Priority: normal | Milestone: 7.8.1
Component: Compiler (Type checker) | Version:
Resolution: | 7.8.1-rc2
Operating System: Unknown/Multiple | Keywords:
Type of failure: None/Unknown | Architecture:
Test Case: | Unknown/Multiple
deriving/should_compile/T8851 | Difficulty:
Blocking: | Unknown
| Blocked By:
| Related Tickets:
-------------------------------------------------+-------------------------
Comment (by Richard Eisenberg
#8851: Standalone deriving and GND behave differently -----------------------------------------------+--------------------------- Reporter: simonpj | Owner: Type: bug | Status: merge Priority: normal | Milestone: 7.8.1 Component: Compiler (Type checker) | Version: Resolution: | 7.8.1-rc2 Operating System: Unknown/Multiple | Keywords: Type of failure: None/Unknown | Architecture: Test Case: deriving/should_fail/T8851 | Unknown/Multiple Blocking: | Difficulty: Unknown | Blocked By: | Related Tickets: -----------------------------------------------+--------------------------- Changes (by goldfire): * testcase: deriving/should_compile/T8851 => deriving/should_fail/T8851 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8851#comment:17 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8851: Standalone deriving and GND behave differently -----------------------------------------------+--------------------------- Reporter: simonpj | Owner: Type: bug | Status: closed Priority: normal | Milestone: 7.8.1 Component: Compiler (Type checker) | Version: Resolution: fixed | 7.8.1-rc2 Operating System: Unknown/Multiple | Keywords: Type of failure: None/Unknown | Architecture: Test Case: deriving/should_fail/T8851 | Unknown/Multiple Blocking: | Difficulty: Unknown | Blocked By: | Related Tickets: -----------------------------------------------+--------------------------- Changes (by thoughtpolice): * status: merge => closed * resolution: => fixed Comment: Merged in 7.8. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8851#comment:18 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC