A compound clause crisis

[RyanGlScott]

While pondering over the formalism last night, I came to rather startling realization that there's quite a glaring issue with deriving clauses using via that contain multiple types. First, consider this:

data Foo
  deriving (C1 a, C2 a) via (T a)

Ultimately, the issue boils down to one question: where does the type variable a in T a come from? Obviously, it has to be somewhere from within the classes C1 a or C2 a, but which one? Keep in mind that the code above is shorthand for:

data Foo
  deriving (forall a. C1 a, forall a. C2 a) via (T a)

That is, the as in C1 a and C2 a come from entirely different scopes. This makes the question of where the a in T a comes from extremely difficult to answer, because we could have arbitrarily many answers.

In fact, that's only the tip of the iceberg when it comes to scoping shenanigans. There's also this wacky example:

data Foo
  deriving (C1 a, C2 b) via (S a b)

This clearly can't compile at all—after all, that would generate the following instances:

instance C1 a Foo where
  c1 = coerce @(... S a b ...) @(... Foo ...) c1

instance C2 b Foo where
  c1 = coerce @(... S a b ...) @(... Foo ...) c1

In the C1 a Foo instance, b is out of scope, and in the C2 b Foo instance, a is out of scope!

Don't forget that you can also have zero classes in a deriving clause. That is, you could conceivably see something like this:

data Foo
  deriving () via A

Or even this, for added nausea:

data Foo
  deriving () via (B b)

This is all quite messy, and suggests that we need to think more carefully about how via should behave when multiple classes are given in a deriving clause. At the moment, I can see three ways to solve this problem:

1. The nuclear option: we enforce the requirement that when via is used, exactly one class must be given in the deriving clause. This would avoid all of the above issues entirely, but we would lose quite a bit of expressiveness with this option (after all, we have examples like deriving (Show, Num) via (WrappedApplicative T) currently). It would also be quite different from how other deriving strategies work.

2. When via appears next to multiple classes in a deriving clause, we treat it as a macro of sorts. That is, this:

   data Foo
    deriving (C1 a, C2 a) via (T a)

   Would translate to this behind the scenes:

   data Foo
    deriving (C1 a) via (T a)
    deriving (C2 a) via (T a)

   In other words, the type variables that appear in the via type would need to be a subset of the (set of datatype variables) ∪ (intersection of all type variables quantified in each derived class). This would make renaming/typechecking everything much simpler, since we can deal with each class's variable scoping separately, and it would also catch unruly examples like:

   data Foo
    deriving (C1 a, C2 b) via (S a b)

   Since that would translate to:

   data Foo
    deriving (C1 a) via (S a b)
    deriving (C2 b) via (S a b)

   Which makes the out-of-scope variables a and b obvious.

   The downside to this approach is that we'd have to "corrupt" the GHC AST a bit in order to accomplish this. Note that in this example:

   data Foo
    deriving (forall (a :: Bool). C1 a, forall (a :: ()). C2 a) via (T a)

   There are really two different T as, each with an a at a different kind! Thus, we cannot store this in the GHC AST as something like data DerivingClause = DerivingClauseVia [ClassType] ViaType—we really do need every ClassType to have its own ViaType, so we'd have to turn this into something like DerivingClauseVia [(ClassType, ViaType)]. It's a bit unsavory, but perhaps it's a necessary compromise.

3. We adopt a different scoping convention for deriving clauses with multiple classes. Recall that in a deriving clause, every class has its own distinct scope, so this:

   data Foo
    deriving (C1 a, C2 a) via (T a)

   Is shorthand for this:

   data Foo
    deriving (forall a. C1 a, forall a. C2 a) via (T a)

   Given that much of the difficulty stems from this convention, we could opt to change it. Instead of every class having its own scope, we could mandate that all of the classes scare the same scope. So we'd instead get something like this:

   data Foo
    deriving forall a. (C1 a, C2 a) via (T a)

   This way, we wouldn't need to do any kind of AST transmogrification—it would become completely unambiguous where each type variable in the via type comes from. A downside is that this convention alone wouldn't be enough to reject this example:

   data Foo
    deriving forall a b. (C1 a, C2 b) via (S a b)

   We'd need an additional check to make sure that the via type's set of variables is a subset of the (set of datatype variables) ∪ (intersection of all type variables that appear in each derived class).

   There'd also be another, more noticeable drawback in that some code which compiles today would no longer continue to compile. For instance, this code currently works in today's GHC:

   data Foo
    deriving (forall (a :: Bool). C1 a, forall (a :: ()). C2 a)

   But if we adopted the new scoping convention, we'd have to pick only one kind for a. Thus, we cannot have C1 a and C2 a kind-check and the same time, so this example would be rejected.

4. The same as option (3), except that we only adopt the new scoping convention for deriving clauses using the via strategy. This would allow this example to continue to compile:

   data Foo
    deriving (forall (a :: Bool). C1 a, forall (a :: ()). C2 a)

   It would share the other drawbacks of option (3), of course. Moreover, it might have an additional drawback in that there are two different scoping rules for deriving clauses depending on which strategy one picks, which users may find confusing.

What are your thoughts on the issue?

[int-index]

Option (2) is what I wanted to suggest when I started reading about the problem.

It's a bit unsavory

Why?

[RyanGlScott]

I meant "unsavory" in the sense that we will have to keep multiple copies of the via type around in the AST. It's not an especially egregious thing to do (especially since we might be moving in that direction for infix declarations soon), but it is something to consider when weighing the pros and cons.

[Icelandjack]

I haven't read all the details but

data Foo
  deriving (C1 a, C2 a) via (T a)

Ultimately, the issue boils down to one question: where does the type variable a in T a come from? Obviously, it has to be somewhere from within the classes C1 a or C2 a, but which one? ..

I'm unsure about this premise, I think we discussed something similar to this on Slack

newtype INT = INT Int deriving Num via (Const Int xx)

works fine without any type variable introduced by Num, unless I am mistaken. This could work as

-- show (INT 10) == "Const 10"
instance Show INT where
  show :: forall xx. INT -> String
  show = coerce (show @(Const INT xx))

-- show (INT 10) = "Const 10"
instance Show Int where
  show :: INT -> String
  show = coerce show' where
    show' :: forall xx. Const Int xx -> String
    show' = show

[RyanGlScott]

We could do something like this, but recall that we ultimately decided against this approach, since (1) it would require sprinkling uses of GHC.Exts.Any when compiling down to Core, which is fishy, and (2) having the ability to implicitly quantify variables in via types is of questionable utility in the first place.

But in any case, that's an orthogonal issue to what is being presented here. The problem is that the a in (T a) is clearly bound from somewhere in deriving (C1 a, C2 a), but there are multiple possible binding sites.

[Tritlo]

I think (2) is the way to go. It's what I would expect anyway, and if doing a similar thing is on the map for infix, I don't think it's a big con.

[RyanGlScott]

We've decided to go with option 2.