[Haskell-cafe] SYB with class: Bug in Derive.hs module

[Andrea Vezzosi]

On Mon, Sep 3, 2012 at 2:53 PM, Roman Cheplyaka <roma at ro-che.info> wrote:
> * Andrea Vezzosi <sanzhiyan at gmail.com> [2012-09-03 12:50:03+0200]
>> > [...]
>>
>> This is pretty similar to what ended up being a ghc bug, fixed in 7.0 though:
>> http://hackage.haskell.org/trac/ghc/ticket/3731
>
> The difference between my test case and the one attached to the ticket
> is that here there's an explicitly circular instance generated by TH.
> In the "SYB with class" paper it is specifically said to be broken. So
> it looks more like a problem in the TH code rather than in GHC.

Right, it's debatable whether ghc should support these instances,
though in our case they are well-founded, it only has to produce code
that's lazy enough on the dictionaries as far as i can tell.

>> > The cause of this bug is a self-referencing instance created by
>> > deriveData:
>> >
>> >     instance (Data ctx Foo, Sat (ctx Foo)) => Data ctx Foo where ...
>> >
>> > What's the proper way to fix it?
>>
>> From a few tests it seems we no longer need the circular context hack
>> in ghc-7.4.1 to get the instance to typecheck, so we could side-step
>> the issue entirely by removing it from the generated code.
>
> Not sure what hack you're referring to.

I was going from memory and remembering that the additional Data ctx
Foo in the context was necessary to make the instance typecheck, and
calling that an hack.
(Now I think I was remembering some HappS code using syb-wc which had
to do that instead).

> As I understand it, the circular context arises as a special case of the
> context that includes all the "inner" types of a data type. It's not
> possible to get rid of this context entirely — for example, consider
>
>     data X a = X (Y a)
>
> where we really need the "Data ctx (Y a)" context (but perhaps it could
> be "Data ctx a" instead?).

(I don't think I like changing the produced code on the basis of which
instances are in scope, so I'd stick with "Data ctx (Y a)")

> So we need some criterion to decide whether a structural part of a data
> type should be included into the instance context.
>
> Does this make sense, or am I on the completely wrong track?

Yes that's correct, I meant to only filter out Data ctx (X a) in this
case, in general I propose to eliminate all the "Data ctx (X ..)" from
the context, when X is the data constructor for which we are making
the instance, but keep the corresponding "Sat (ctx (X ..))", do you
think this would break any instances that would otherwise work?

It'd be interesting to find out if we can make a sensible instance for
non-regular types like the following though:

data Z a = Z (Z (a,a)) | Leaf a

the instance we produce currently makes instance resolution
non-terminate and the instance we'd  produce under my proposal
wouldn't typecheck.

-- Andrea Vezzosi