Opened 6 years ago

Closed 6 years ago

#8851 closed bug (fixed)

Standalone deriving and GND behave differently

Reported by: simonpj Owned by:
Priority: normal Milestone: 7.8.1
Component: Compiler (Type checker) Version: 7.8.1-rc2
Keywords: Cc: mail@…, slyfox@…
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case: deriving/should_fail/T8851
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

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.

Change History (18)

comment:1 Changed 6 years ago by nomeata

Cc: mail@… added
Component: CompilerCompiler (Type checker)
Version: 7.6.37.8.1-rc1

I’m trying to wrap my head around which of the two behaviours is correct. Richard, can you enlighten me?

comment:2 Changed 6 years ago 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 Safe Coercions paper.

Simon

comment:3 Changed 6 years ago 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).

comment:4 Changed 6 years ago by goldfire

Owner: set to goldfire

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.

comment:5 Changed 6 years ago 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 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

comment:6 Changed 6 years ago by slyfox

Cc: slyfox@… added

comment:7 Changed 6 years ago 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!

comment:8 Changed 6 years ago by Richard Eisenberg <eir@…>

comment:9 Changed 6 years ago by goldfire

Test Case: deriving/should_compile/T8851

comment:10 Changed 6 years ago by goldfire

Milestone: 7.8.1
Owner: goldfire deleted

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.

comment:11 Changed 6 years ago 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

comment:12 Changed 6 years ago by Simon Peyton Jones <simonpj@…>

In 9d14262299fe721e49eb0efadebca9d095c834b3/ghc:

Improve documentation of standalone deriving (c.f. Trac #8851)

comment:13 Changed 6 years ago by thoughtpolice

Version: 7.8.1-rc17.8.1-rc2

comment:14 Changed 6 years ago 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.

comment:15 Changed 6 years ago by simonpj

Status: newmerge

Please merge the documentation changes to 7.8

comment:16 Changed 6 years ago by Richard Eisenberg <eir@…>

In 8ee6162e9a3377cd4c79f49b63f92046b0d5c708/ghc:

Recharacterize test according to discussion in #8851.

comment:17 Changed 6 years ago by goldfire

Test Case: deriving/should_compile/T8851deriving/should_fail/T8851

comment:18 Changed 6 years ago by thoughtpolice

Resolution: fixed
Status: mergeclosed

Merged in 7.8.

Note: See TracTickets for help on using tickets.