Opened 2 years ago

Last modified 11 months ago

#14331 new bug

Overzealous free-floating kind check causes deriving clause to be rejected

Reported by: RyanGlScott Owned by:
Priority: normal Milestone: 8.10.1
Component: Compiler (Type checker) Version: 8.2.1
Keywords: deriving Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC rejects valid program Test Case: deriving/should_compile/T14331
Blocked By: Blocking: #15376
Related Tickets: #15376 Differential Rev(s):
Wiki Page:

Description

GHC rejects this program:

{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
module Bug where

class C a b

data D = D deriving (C (a :: k))
GHCi, version 8.2.1: http://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug              ( Bug.hs, interpreted )

Bug.hs:8:1: error:
    Kind variable ‘k’ is implicitly bound in datatype
    ‘D’, but does not appear as the kind of any
    of its type variables. Perhaps you meant
    to bind it (with TypeInType) explicitly somewhere?
  |
8 | data D = D deriving (C (a :: k))
  | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

But it really shouldn't, since it's quite possible to write the code that is should generate:

instance C (a :: k) D

Curiously, this does not appear to happen for data family instances, as this typechecks:

{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
module Bug where

class C a b

data family D1
data instance D1 = D1 deriving (C (a :: k))

class E where
  data D2

instance E where
  data D2 = D2 deriving (C (a :: k))

Change History (68)

comment:1 Changed 2 years ago by RyanGlScott

I spoke too soon about that second program (with data families) working. It turns out that it's rejected on GHC HEAD:

GHCi, version 8.3.20171004: http://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug              ( Bug.hs, interpreted )

Bug.hs:10:1: error:
    • Kind variable ‘k’ is implicitly bound in data family
      ‘D1’, but does not appear as the kind of any
      of its type variables. Perhaps you meant
      to bind it (with TypeInType) explicitly somewhere?
    • In the data instance declaration for ‘D1’
   |
10 | data instance D1 = D1 deriving (C (a :: k))
   | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

Bug.hs:16:3: error:
    • Kind variable ‘k’ is implicitly bound in data family
      ‘D2’, but does not appear as the kind of any
      of its type variables. Perhaps you meant
      to bind it (with TypeInType) explicitly somewhere?
    • In the data instance declaration for ‘D2’
      In the instance declaration for ‘E’
   |
16 |   data D2 = D2 deriving (C (a :: k))
   |   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

comment:2 Changed 2 years ago by goldfire

I assume you really meant

data D = D deriving (forall k a. C (a :: k))

but that GHC doesn't quantify k the right way. So it's a bug in kind quantification, not the free-floating kind variable check.

(Sidenote: that forall isn't allowed there. But perhaps it should be incorporated into the recent proposal expanding where forall can be used.)

Last edited 2 years ago by goldfire (previous) (diff)

comment:3 in reply to:  2 Changed 2 years ago by RyanGlScott

Replying to goldfire:

I assume you really meant

data D = D deriving (forall k a. C (a :: k))

but that GHC doesn't quantify k the right way.

I most certainly didn't. (In fact, I've opened a separate bug about the fact that you can put foralls in deriving clauses, which horrifies me.)

It's somewhat surprising, but deriving clauses can bind type variables themselves. Note that this is currently accepted:

data D = D deriving (C a)

Here, a isn't bound by the data type D, so it is in fact bound in the deriving clause. By the same principle, deriving (C (a :: k)) should be allowed, and the free-floating kind check is mistaken to reject it.

comment:4 Changed 2 years ago by goldfire

So, if deriving (C (a :: k)) doesn't mean to quantify, what do you expect it to mean? I agree that the current error is wrong, but I'm not sure what behavior you want GHC to take here.

If you want GHC to accept your original declaration, creating instance forall k (a :: k). C a D, then we're basically in agreement.

comment:5 Changed 2 years ago by RyanGlScott

I meant exactly what I wrote in the original description: it should emit:

instance C (a :: k) D

After all, the user wrote deriving (C (a :: k)), and the data type is D. What you get after doing the whole deriving macro-application-eta-reduction-kind-unification shebang is C (a :: k) D.

comment:6 Changed 2 years ago by goldfire

But I see instance C (a :: k) D as fully equivalent to instance forall k (a :: k). C a D. They just make different things explicit, but both declarations have the same static and dynamic semantics.

And, I don't quite agree that clauses in a deriving are macro-like. They are types of kind ... -> Type -> Constraint, where the ... may be empty. My desire to put forall in there is more macro-like, I admit... but no more so than the syntax for pattern synonym types or even GADT constructor types.

I believe that you are genuinely confused here. But I'm afraid I'm equally confused as to why you're confused.

comment:7 in reply to:  6 Changed 2 years ago by RyanGlScott

Replying to goldfire:

But I see instance C (a :: k) D as fully equivalent to instance forall k (a :: k). C a D. They just make different things explicit, but both declarations have the same static and dynamic semantics.

Yes, agreed.

And, I don't quite agree that clauses in a deriving are macro-like. They are types of kind ... -> Type -> Constraint, where the ... may be empty.

Surely you mean kind k -> Constraint? You certainly can't say deriving Z, where class Z a b, for instance.

To elaborate what I mean by "macro" here: yes, the C c1 ... cn in deriving (C c1 ... cn) is a type, and one that is thrust into the typechecker at one point as a sanity-check to make sure you aren't writing utter garbage. But it's not like other types in that C c1 ... cn doesn't appear on its own in the emitted code—it only makes sense to talk about C c1 ... cn in the final program after it has been combined with its corresponding data type. Trying to stick foralls on just C c1 ... cn feels nonsensical, because the scoping needs to happen for the whole derived instance, not just C c1 ... cn, which happens to be one part of the recipe.

I believe that you are genuinely confused here. But I'm afraid I'm equally confused as to why you're confused.

The thing that I am confused on above all else is this business on skolems you mention in https://ghc.haskell.org/trac/ghc/ticket/14332#comment:9, and why the user-written kinds of a data type's type variables don't fall under the same scrutiny. I can't even begin to understand how this would work without an explanation of what is motivating this design choice.

comment:8 Changed 2 years ago by simonpj

Trying to stick foralls on just C c1 ... cn feels nonsensical,

You could try not thinking of them as foralls. Say

data D = D deriving ({k a}. C (a :: k))

where I'm using {k a} to bring k and a into scope.

But they ARE skolems. I'm sure you wouldn't be happy with

data D = D deriving( {a}. C a }

it the derived instance declaration ended up being

instance C Int D

where the a gets unified with Int somehow. (Fundeps or something.) This quantification is per-deriving-clause. If you say a you mean a and not Int!

why the user-written kinds of a data type's type variables don't fall under the same scrutiny

Because they are shared across the data type decl itself, and all the deriving clauses. So in

data Proxy k (a :: k) = Proxy deriving(  Functor, ...others... )

the Functor instance only makes sense when k=*, so we specialise it to that

  instance GHC.Base.Functor (Main.Proxy *) where

We can't turn that k into * in the decl without crippling Proxy.

To put it another way:

  • The kind binders in the data decl belong to the data decl
  • The freshly bound variables in the deriving clause belong to the instance decl
  • Naturally, the quantified variables of the data decl may be instantiated in the instance decl.

Does that help?

Is this essentially the same ticket as #14332? Can we combine?

comment:9 in reply to:  8 Changed 2 years ago by RyanGlScott

Replying to simonpj:

Does that help?

Thank you Simon, that was the careful explanation I was searching for. I think I'm sold on this idea now.

Is this essentially the same ticket as #14332? Can we combine?

I'm not sure. Do we know for sure that the bug described in this ticket is caused by a deficient treatment of quantification in deriving clauses?

comment:10 Changed 2 years ago by Simon Peyton Jones <simonpj@…>

In 82b77ec/ghc:

Do not quantify over deriving clauses

Trac #14331 showed that in a data type decl like

   data D = D deriving (C (a :: k))

we were quantifying D over the 'k' in the deriving clause.  Yikes.

Easily fixed, by deleting code in RnTypes.extractDataDefnKindVars

See the discussion on the ticket, esp comment:8.

comment:11 Changed 2 years ago by simonpj

Milestone: 8.2.2
Status: newmerge
Test Case: deriving/should_compile/T14331

OK I fixed the bug for this ticket. Remaining work is on #14332.

Merge if/when convenient.

comment:12 Changed 2 years ago by RyanGlScott

I still don't think this is quite right. Look at what happens now when you try to compile this variation of the original program:

{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
module Bug where

class C a b

data D a = D deriving (C (a :: k))
GHCi, version 8.3.20171011: http://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug              ( Bug.hs, interpreted )

Bug.hs:8:27: error:
    • Expected kind ‘k1’, but ‘a’ has kind ‘k’
    • In the first argument of ‘C’, namely ‘(a :: k)’
      In the data declaration for ‘D’
  |
8 | data D a = D deriving (C (a :: k))
  |                           ^

This is wrong—the a in D a and C a should have the same kind, since they're the same a.

comment:13 Changed 2 years ago by simonpj

I agree. After elaboration we expect

class C {k1 k2} (p::k1) (q::k2)
data D {k3} (r::k3) = D

instance forall {k2} k (a:k) (b:k2). C a (D {k2} b) where ...

So we instantiate the k3 belonging to the data declaration to k2 belonging to the instance. The forall k in the deriving clause is just the kind on a, the first parameter for C.

Right?

Why this doesn't work I don't know.

Version 0, edited 2 years ago by simonpj (next)

comment:14 Changed 2 years ago by RyanGlScott

Huh? That is not what I would have expected at all. I would have expected:

class C {k1 k2} (a :: k1) (b :: k2)
data D {k3} (r :: k3) = D

instance forall k1 (a :: k1). C a (D a) where ...

In other words, you should unify r with a. After all, the a in data D a = D deriving (C (a :: k)) is bound by the data type, not the deriving clause!

Now if you had chosen to use a different scoping with data D a = D deriving (forall (a :: k). C a), then I could see the instance being derived that you suggested. But I don't think users would expect that behavior to be the default (that is, in lieu of explicit foralls on a deriving clause, one should assume that the user-written type variables are bound by the data type if they appear in the <tvbs> in data D <tvbs>).

Last edited 2 years ago by RyanGlScott (previous) (diff)

comment:15 Changed 2 years ago by goldfire

For what it's worth, I agree with Ryan in what GHC should do here.

comment:16 Changed 2 years ago by simonpj

Ah yes, you're right. I was focusing on the k, but there's the a as well.

But then I'd say that the error message is dead right. Let's put the implicit binders in:

data D {k1} (a::k1) = D deriving (forall k. C (a :: k))

Look at that! a has kind k1; but in the deriving clause we claim that the occurrence of a has type k. Boom.

Last edited 2 years ago by simonpj (previous) (diff)

comment:17 Changed 2 years ago by RyanGlScott

I don't understand your reasoning in comment:16. After all, we don't reject this:

{-# LANGUAGE TypeInType #-}

import Data.Proxy

data Foo a = Foo (Proxy (a :: k))

After all, k is implicitly bound by the datatype D, so everything works out. The same situation applies in:

data D a = D deriving (C (a :: k))

Once again, k is implicitly bound by D, so k and the kind of a are one and the same.

comment:18 Changed 2 years ago by goldfire

I'm not convinced by comment:17, as I consider deriving clauses to be more separate from the definition. My reasoning is that we do unification for deriving. Thus, the kind k2 of a will be unified with the newly-quantified kind k, leading to an accepted definition.

comment:19 Changed 2 years ago by RyanGlScott

It will lead to an accepting definition, yes, but I don't think it's the definition you'd want (or at least, it seems to differ from the proposal I put forth in comment:14). If I understand your argument correctly, you want all type variables in a deriving clause's type to be scoped differently from the data type, and expect unification to save you in the end? That is, this:

data D a = D deriving (C (a :: k))

Would be treated like this?

data D {k1} (a1 :: k1) = D deriving (forall {j} k (a :: k). C @k @j a)

If so, we have a problem—the only kinds we'd unify are the j in C a :: j -> Constraint and Type (the kind of D a), so the instance we'd get in the end is:

instance forall {k1} k {a1 :: k1} (a :: k). C @k @Type a (D @k1 a1) where ...

Which is not what I'd expect, since a and a1 are distinct. The only way to ensure that they're the same is to interpret the scope like this:

data D {k} (a :: k) = D deriving (forall {j}. C @k @j a)

comment:20 Changed 2 years ago by goldfire

I think you don't understand correctly. (Perhaps because I've communicated poorly.)

The user writes

class C a b
data D c = D deriving (C (c :: k))

There is implicit lexical quantification in the deriving clause. ("Lexical" because it's all just based on reading the code -- no type-checking yet!) So, these declarations are understood to mean

class C a b
data D c = D deriving (forall k. C (c :: k))

We don't have to write forall for the class or data declarations, because the type variables there are understood to mean quantification. Note that I'm not quantifying over c in the deriving clause, because it's already in scope.

The initial declarations are processed without regard to the deriving clause, producing

class C {k1} {k2} (a :: k1) (b :: k2)
data D {k3} (c :: k3) = D

Now, we type-check

instance forall {c k}. C (c :: k) (D c)

where the C (c :: k) is taken from the deriving clause, and the quantified variables are not yet ordered. After type-checking, we get

instance forall (k :: Type) (c :: k). C {k} {Type} c (D {k} c)

as desired.

Note that the use of c in the deriving clause did not lead to unification. Instead, the fact that we know more about its kind does.

However, in writing this up, I discovered a new problem. When I write

class C2 a
data D b = D deriving C2

do I mean

instance C2 {k -> Type} D

or

instance C2 {Type} (D b)

? Both are well-kinded and sensible. Right now, we always choose the latter, but I'm not sure why.

comment:21 in reply to:  20 Changed 2 years ago by RyanGlScott

You're right, that should work out in the end. Thank you for the patient explanation, and sorry for being slow on the uptake.

Replying to goldfire:

However, in writing this up, I discovered a new problem. When I write

class C2 a
data D b = D deriving C2

do I mean

instance C2 {k -> Type} D

or

instance C2 {Type} (D b)

? Both are well-kinded and sensible. Right now, we always choose the latter, but I'm not sure why.

The usual convention for figuring out how many type variables to eta reduce from the datatype is to simply count the number of argument types in the kind k in deriving (Cls c1 ... cn :: k -> Constraint). In this example, the kind is just a plain kind variable, which we count as having zero arguments. Thus, we don't eta reduce any type variables, resulting in the latter instance.

This convention doesn't bother me that much, since if the user wanted to derive instance C2 D, they could just as well write data D a = D deriving (C2 :: (k -> Type) -> Constraint).

comment:22 Changed 2 years ago by goldfire

You're right that the user could specify this, but I see the original deriving as ambiguous -- only we don't report it as so. Worth fixing? I'm not sure.

comment:23 Changed 2 years ago by simonpj

Re comment:17, consider

data Foo a = Foo (Proxy (a :: k))
data D a = D deriving (C (a :: k))

You suggest that these are similar, but they aren't. After renaming we have

data Foo {k} a = Foo (Proxy (a :: k))
data D a = D deriving (forall {k}. C (a :: k))

Notice the different scoping of the two k's. So the two really aren't the same at all.

We could have specified different quantifaction semantics for Foo thus

data Foo a = Foo (forall {k}. Proxy (a :: k))

But we didn't, and for good reasons.

Likewise the tighter scoping in the deriving clause has a good justification.

comment:24 Changed 2 years ago by simonpj

Where are we on this?

I claim in commment:16 that the error message in comment:12 is spot on. So what remains is to document the behaviour.

The other loose end is Richard's "Howver, in writing this up..." point in comment:20. I agree with Ryan's response in comment:21. Do we need any futher documentation?

Last edited 2 years ago by simonpj (previous) (diff)

comment:25 Changed 2 years ago by RyanGlScott

Uh... are we reading the same ticket? Richard and I have come to the opposite conclusion, that the program in comment:12 should be accepted, according to the rationale in comment:20. (Richard and I initially differed on why that program should be accepted, but I came around to his explanation after some debate.)

comment:26 Changed 2 years ago by simonpj

Ah! I disagee with comment:20. Let's start with this, after renaming:

class C a b
data D c = D
  deriving (forall k. C (c :: k))

Now we typecheck the class and data D decls, but not yet the deriving part, yielding

class C {k1} {k2} (a:k1) (b:k2)
data D {k3} (c:k3) = D
  deriving (forall k. C (c :: k))

Now we move on to typechecking the deriving clause. Here we fail, becuase c has kind k3 but its occurrence in the deriving clause claims it has kind k, where those two binders are quite different. And that's just what the error message says.

To make it work, write

data D (c::k) = D deriving( D c )

comment:27 Changed 2 years ago by goldfire

I initially thought the same as comment:26, but then I realized that the logic in comment:26 also means that data Proxy a = P deriving Functor should fail. We allow unifying kind variables in a data declaration to be unified when processing a deriving clause. The program in comment:12 has the same action.

comment:28 Changed 2 years ago by simonpj

the logic in comment:26 also means that data Proxy a = P deriving Functor should fail

Not at all! After elaborating the data type decl we have

data P {k} (a::k) = P deriving( Functor )

Now we create an instance declaration in which we are free to instantiate k (and indeed a) as much as we plase:

instance Functor (P (*->*)) where ...

The quantified variables of the data type decl can freely be instantiated in the (derived) instance. We want the most general such instantiation so that the derived instance is applicable as much as poss; hence unification.

I have belatedly realised that the real stumbling block here is when the same variable appears both in the data type decl and in the deriving clause. For example, here's a case that does NOT have this problem:

-- C :: * -> * -> Constraint
data D k (a::k) = ... deriving( forall x. C x )

is fine: we get an instance looking like

instance forall x (b::*).  (...) => C x (D * b) where ...

The x from the deriving is universally quantified in the instance; the k and a are instantiated to * and b respectively; then we quantify over b.

But the nasty case is this:

data D k (a::k) = ... deriving( C2 k a )

The k and a belong both to the data decl (hence it's in the "freely instantiate" camp) but also belong somehow in the instance. Can I freely instantiate the k in the instance? And the k? It'd be very odd if I got an instance like

instance ... => C2 * a (D * a) where ...

because the deriving part explicitly said k not *.

This seems very hard to specify. It's much easier to think of the data type decl and the instance entirely separately.

Do we need the same variable to appear in both places? That is, what if we said that the type variables from the data type don't scope over the 'deriving' clause? Then

data D k (a::k) = ... deriving( C2 k a )

would mean

data D k (a::k) = ... deriving( forall kk aa. C2 kk aa )

where I've alpha-renamed to make it clear. What would go wrong if we did that?

Last edited 2 years ago by simonpj (previous) (diff)

comment:29 Changed 2 years ago by goldfire

I'm afraid I mostly disagree with comment:28.

Your first example is

-- C :: Type -> Type -> Constraint
data D k (a :: k) = ... deriving (forall x. C x)

I think we get an instance

instance forall x k (a :: k). (...) => C x (D k a)

No instantiation is needed to get D k a to have kind Type. But I'm not terribly bothered here -- I don't think the general argument is wrong, just the example.

In the next example (with C2), I'm not sure the kind of C2. Perhaps it's forall k -> k -> Type -> Constraint? But even so, we can get

instance ... => C2 k a (D k a)

without getting hurt.

Regardless, I don't see how this argument refutes comment:27. The example I was considering was

class C a b
data D a = D deriving (C (a :: k))

where the k in the deriving clause is not mentioned in the data declaration. Thus the concerns in comment:28 don't apply. The a is mentioned, but it needs no unification.

I do agree that this is hard to nail down. It seems, though, that one way forward is to say that any variables explicitly mentioned in the deriving clause are not free for unification. Other variables in the data decl but not in the deriving clause can be unified. This is a little strange perhaps, but not hard to articulate or understand. I do think it's worth asking if anyone ever really needs variables shared between the data decl and the deriving (Simon's last point in comment:28).

comment:30 in reply to:  29 Changed 2 years ago by RyanGlScott

Replying to goldfire:

I do think it's worth asking if anyone ever really needs variables shared between the data decl and the deriving (Simon's last point in comment:28).

We certainly do. Here's an example from #3955:

newtype T a x = T (Reader a x)
   deriving (Monad, MonadReader a)

comment:31 Changed 2 years ago by goldfire

Simon and I debated this all at some length this morning. We basically settled on agreeing to my paragraph at the end of comment:29. Spelling this out:

  1. The variables introduces in the data declaration head scope over the deriving clause. (Throughout this comment, newtype is treated identically to data.) This is true even for GADT-syntax declarations where any variables in the head typically have no scope.
  1. Any type variables mentioned in a deriving clause but not already in scope are brought into scope locally in that deriving clause. Independent comma-separated clauses are separate and quantify separately.
  1. The user may write an explicit forall in a deriving clause scoped over only one clause. If the user writes a forall, it must bind every type variable not brought into scope by the data declaration. This forall is understood as a scoping construct, not quite as a full-blooded forall, which normally requires its body to have kind TYPE r for some r.
  1. Process a data declaration on its own, without further regard to any deriving clauses.
  1. For each deriving clause:
    1. Let the kind of the head of the clause (the part without the forall) be ki and the set of variables locally quantified be bs. Let the head of the clause be drv.
    2. Instantiate ki with fresh unification variables for any kind variables in ki. (This is vanilla instantiation for an applied type.)
    3. Unify ki with kappa -> Constraint, getting a substitution for kappa; let the result of this substitution be ki2. (Issue an error if unification fails.)
    4. It is required that ki2 have the form ... -> Type or kappa2 for some unification variable kappa2. If ki2 is kappa2, then choose kappa2 := Type. Now, we have something of the form ... -> Type. Let the number of arguments in the ... be n.
    5. Let the set of variables mentioned in the deriving clause but not locally scoped (that is, they are also mentioned in the data declaration head) be as.
    6. It is an error if any variable in as is mentioned in any of the last n arguments in the data declaration head. Data family instances need even more checks.
    7. Drop the last n arguments (whether visible or invisible) to the datatype. Call the result ty.
    8. Replace any type variables in ty but not mentioned in the deriving clause with fresh unification variables.
    9. Unify the kind of ty with ki2, issuing an error if unification fails. Zonk ty, replacing any unfilled unification variable with fresh skolems. Call the set of these skolems sks.
    10. Produce instance forall {bs sks as}. ... => drv ty, where the braces around the variables is meant to imply that order does not matter; GHC will do a topological sort to get these variables in the right order.
    11. Solve for the unknown context ... and insert that into the declaration.
    12. Declare victory.

I think that does it. Simon had wanted a much more declarative specification (and I agree), but I'm stuck on how to write one at the moment. Let's perhaps agree on this algorithmic specification and then see if there are ways to clean it up.

Last edited 2 years ago by goldfire (previous) (diff)

comment:32 Changed 2 years ago by RyanGlScott

Thanks Richard, this looks wonderful. I have some questions/comments about your algorithm:

  1. What happens if the user writes an explicit forall in a deriving clause but leaves out a variable, such as in data Foo a = ... deriving (forall b. C b c)?

Also, in what sense is this not a "full-blooded forall"?

  1. c. I'm not sure I understand this business about kappa2 (or why you'd choose kappa2 := Type). Can you give an example of where this would arise?
  1. e. Some more validity checks that would need to be performed for data family instances are documented here.
  1. h. I was hoping for a little more detail on this skolem business. For instance, we'd want to reject data D = D deriving (forall k. C k) (where we have class C k (a :: k)) since the k is skolem, yes? (Disclaimer: due to my lack of experience with typechecker terminology, I'm guessing that "skolem" is a fancy way of saying "can't unify with other types". Please correct me if I'm off-track here.) Currently, this just says "replacing any unfilled unification variable with fresh skolems", which doesn't give me a sense of where the skolems are coming from.

Also, does the skolemicity only kick in if you write an explicit forall? Or would the k in data D = D deriving (C k) also get skolemized?

comment:33 in reply to:  32 ; Changed 2 years ago by goldfire

I've clarified point 3, above.

Replying to RyanGlScott:

  1. c. I'm not sure I understand this business about kappa2 (or why you'd choose kappa2 := Type). Can you give an example of where this would arise?
class C a
data D a = D deriving C

We see that C :: forall k. k -> Constraint. So we have ki = forall k. k -> Constraint. We then instantiate (note new step, above) to get ki = kappa3 -> Constraint, where kappa3 is a fresh unification variable. Unifying with kappa -> Constraint simply sets kappa := kappa3. So, ki2 is really just kappa3. This is the special case in (d).

What's really going on here is that both the following are well-kinded:

instance C D
instance C (D a)

We choose the second -- that's the kappa2 := Type. Alternatively, we could issue an error here; it's all a free design choice.

  1. e. Some more validity checks that would need to be performed for data family instances are documented here.

I've updated my algorithm. Thanks.

  1. h. I was hoping for a little more detail on this skolem business.

A skolem is a type variable that is held distinct from any other type. For example:

nid :: a -> a
nid True = False

This fails to type-check because, in the body of nid, a is a skolem. If it were a unification variable, we would just unify a := Bool. The "Practical Type Inference" paper has a good discussion of skolems.

In a deriving clause, any variable quantified in the clause is considered to be a skolem. These skolems are basically unrelated, though, to the skolems mentioned in step (i). The skolems in step (i) would come from something like this:

class C (a :: Type)
data D k (b :: k) = D deriving C

leads to

instance ... => C (D alpha beta)

where alpha and beta are unification variables. Because these variables are unconstrained, we wish to quantify over them, leading to the final instance declaration

instance forall a (b :: a). ... => C (D a b)

The a and b here are the fresh skolems of stem (i).

Your example is

class C j (a :: j)
data D = D deriving (forall k. C k)

Here, we learn that ki2 (of step (c)) is the skolem k. (This is a skolem because user-written variables are skolems, like in the nid example.) That is not of the form ... -> Type, nor is it a unification variable. (I just added the key qualifier "unification" to that step.) So we reject at this point.

Also, does the skolemicity only kick in if you write an explicit forall? Or would the k in data D = D deriving (C k) also get skolemized?

The user-written variables in a deriving clause are skolems whether or not they are explicitly quantified.

comment:34 in reply to:  33 Changed 2 years ago by RyanGlScott

Replying to goldfire:

class C a
data D a = D deriving C

We see that C :: forall k. k -> Constraint. So we have ki = forall k. k -> Constraint. We then instantiate (note new step, above) to get ki = kappa3 -> Constraint, where kappa3 is a fresh unification variable. Unifying with kappa -> Constraint simply sets kappa := kappa3. So, ki2 is really just kappa3. This is the special case in (d).

OK. My question is: why do we need to special-case this at all? After all, in step (i) we unify the kind of ty with ki2, and the kind of ty will always be of the form ... -> Type by virtue of the kind of ty coming from a data type. So we achieve the same effect without needing a special case at all. (In fact, this is currently what the implementation of TcDeriv does.)

comment:35 Changed 2 years ago by goldfire

But we can only get ty after dropping n arguments.

Relating this to the existing code in deriveTyData, what I've called ki2 is cls_arg_kind and what I've called n is n_args_to_drop. n_args_to_drop is computed by counting the number of args spun off by a call to splitFunTys cls_arg_kind. For a unification variable kappa, splitFunTys will return no arguments -- just like it would when cls_arg_kind is Type. So GHC currently behaves like my algorithm; I just have more checks here. However, calling splitFunTys on a unification variable is bogus, because that variable could potentially stand for anything, including a function. This bogus use happens to work out, but that's more luck than science in this case, I think.

comment:36 Changed 2 years ago by RyanGlScott

Alright, that sounds reasonable enough.

After thinking about this some more, though, I realized that there's another incongruity with your proposal and how TcDeriv currently operates. In particular, there can be more unification after part (i) if you are deriving Functor, Foldable, or Traversable. Here is an example of such a situation (taken from Trac #10561):

newtype Compose (f :: k2 -> Type) (g :: k1 -> k2) (x :: k1) =
    Compose (f (g a))
  deriving stock Functor

In part (i), we would unify Type -> Type (the kind of the argument to Functor) with k1 -> Type (the kind of Compose f g, giving us:

instance forall {k2 (f :: k2 -> Type) (g :: Type -> k2)}.
         (Functor f, Functor g) => Functor (Compose f g)

But note that this won't kind-check yet, since the kinds of f and g are still too general. This is where this code in TcDerivInfer kicks in: it takes every type on the RHS of the datatype that accepts one argument (in the example above, that would be f and g), unifies their kinds with Type -> Type, and applies the resulting substitution to the type variables. In the example above, this substitution would be [k2 |-> Type], so applying that would yield the instance:

instance forall {(f :: Type -> Type) (g :: Type -> Type)}.
         (Functor f, Functor g) => Functor (Compose f g)

And now it kind-checks, so we can feed the instance context into the simplifier (part (k)).

My question is: where does this extra unification for deriving Functor, Foldable, or Traversable fall into your algorithm? In part (j) you write instance forall {bs sks as}. ... => drv ty, which seems to suggest that the type variables shouldn't be unified any more after that step, but that's not true in this particular example.

comment:37 Changed 2 years ago by simonpj

there can be more unification after part (i) if you are deriving Functor, Foldable, or Traversable

That is terrible! I had no idea we did this. It seems absurdly ad-hoc.

I can see two ways forward.

  1. Require standalone deriving in such cases. It's not so bad, and is a lot clearer! I'm against inferring too much. Indeed I'd happily weaken our existing inference further. (Acknowledging back-compat issues.)
  1. Do it properly. That is, after simplifying the instance constraints we'll end up withk~Type in these cases, and perhaps others. Instead of rejecting such constraints as too exotic, simply commit to them. That's the "extra unification".

comment:38 in reply to:  37 Changed 2 years ago by RyanGlScott

Replying to simonpj:

It seems absurdly ad-hoc.

I'm not sure what makes this any more ad hoc than anything else we do to derive Functor.

I'd caution against letting the tail wag the dog here—if something in our algorithm rules out a fundamentally important case like deriving Functor for Compose, then I'd interpret that as meaning our algorithm is wrong, not the example.

  1. Require standalone deriving in such cases. It's not so bad, and is a lot clearer! I'm against inferring too much. Indeed I'd happily weaken our existing inference further. (Acknowledging back-compat issues.)

I'm strongly opposed to this. There's no intuitive reason why deriving Functor shouldn't just work in this case, and now we'd have to explain to a mob of pitchfork-wielding Haskell users why their code broke due to GHC not "inferring too much".

  1. Do it properly. That is, after simplifying the instance constraints we'll end up withk~Type in these cases, and perhaps others. Instead of rejecting such constraints as too exotic, simply commit to them. That's the "extra unification".

For obvious reasons, I'd prefer this option to option 1. But I'll admit that I don't understand the proposed fix here. At what point does instance constraint simplification derive a k ~ Type constraint?

comment:39 Changed 2 years ago by goldfire

I see what's Simon's getting at with his (2). Let me try to explain by way of a much simpler example.

Suppose the user has written

f :: _ => a -> a
f True = False
f False = True

GHC rejects. But it doesn't have to do so: it could infer _ := (a ~ Bool), thus giving f the type (a ~ Bool) => a -> a, a perfectly fine type for that definition. Of course, GHC doesn't do this, because it leads to a bad user experience.

It's similar with deriving inference: GHC is free to infer whatever constraints it wants for the instance. It could choose to infer a k ~ Type constraint. Currently, it doesn't because that's too like the a ~ Bool constraint above. So Simon is proposing to unrestrict GHC in this regard.

Sadly, however, this doesn't actually work. Again, I'll use a simpler example to demonstrate:

g :: forall k (a :: k). k ~ Type => a -> a
g x = x

GHC rejects this type signature, saying that a has kind k. This isn't a bug. It was decided en route to TypeInType that GHC wouldn't allow kind-level equality constraints to be used in the same type that they're brought into scope. (Essentially, we don't Pi-quantify constraints.) One reason for this is that ~ is lifted and can be forged. (There are some disorganized notes about all this here.)

The k ~ Type constraint Simon proposes would suffer from the same non-feature. So, even if GHC did infer k ~ Type, we couldn't just stuff this constraint in the inferred theta and declare victory.

So, while Simon's (2) is nice in theory, it wouldn't work until we have more dependent types.

I, too, am against Simon's (1). stock deriving is all ad-hoc. I'm not bothered by this particular piece of ad-hockery. It should be documented, of course, but I think it's OK. I don't think my algorithm should accommodate this, though, precisely because it is indeed ad-hoc.

comment:40 Changed 2 years ago by simonpj

So, while Simon's (2) is nice in theory, it wouldn't work until we have more dependent types.

Yes it will -- I just explained it badly.

In TcDerivInfer.inferConstaints we figure out the context of the derived instance decl. To do so we call TcDerivInfer.simplifyDeriv, which in turn calls TcSimplify.solveWantedsAndDrop. It's the latter that will come up with that k~Type constraint.

Now if that k is a unification variable, solveWantedsAndDrop will go right ahead and unify it. Which, you are saying, is precisely what we want. But, unlike the current ad-hoc setup, that will happen though constraint solving in general, rather than through a magical Functor-specific wim-wam.

So, I say, make those unifiable k's into real unification variables, and let the constraint solver do its thing. Then, when the dust settles, gather up all the free variables and quantify over them, much as we do in any other inferred type. This does mean we can't fix on the quantified variables until after inferConstraints. But it's simple and systematic.

comment:41 Changed 2 years ago by bgamari

What is the conclusion here? Do we want to merge comment:10 to 8.2.2?

comment:42 Changed 2 years ago by simonpj

Personally I think comment:10 is an improvement, but there is clearly more to do. Either way, it won't affect many users, so you could leave it out of 8.2 without any significant impact, I think.

comment:43 Changed 2 years ago by bgamari

Milestone: 8.2.28.4.1
Status: mergenew

Alright, let's punt then.

comment:44 Changed 2 years ago by goldfire

I see we've all come to happy agreement on what to do... but there's been no talk of who will do it. I'm afraid if it comes to my plate, it will have fairly low priority...

comment:45 Changed 2 years ago by RyanGlScott

I would be willing to try this, but implementing this would require knowledge that I'm not currently privy to...

comment:46 Changed 2 years ago by simonpj

Let's have a Skype call and I can reveal the secret knowledge!

comment:47 Changed 2 years ago by RyanGlScott

I made an attempt towards fixing this at https://github.com/RyanGlScott/ghc/tree/rgs/T14331. I didn't get very far.

My first goal was to switch over from the use of the pure unifier to the monadic one, but that alone proves to be quite difficult. The problem is that for some strange reason, using the monadic unifier causes several type variables to be filled in with Any, leading to Core Lint errors and general badness. As one example, if you compile this program:

module Bug where

data Pair a b = Pair a b
  deriving Eq

Using my branch with -dcore-lint on, you'll be greeted with this:

$ ghc/inplace/bin/ghc-stage2 --interactive Bug.hs -dcore-lint
GHCi, version 8.3.20171031: http://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug              ( Bug.hs, interpreted )
*** Core Lint errors : in result of Desugar (after optimization) ***
Bug.hs:4:12: warning:
    [RHS of $fEqPair :: forall a b.
                        (Eq Any, Eq Any) =>
                        Eq (Pair Any Any)]
    The type of this binder doesn't match the type of its RHS: $fEqPair
    Binder's type: forall a b. (Eq Any, Eq Any) => Eq (Pair Any Any)
    Rhs type: forall a b. (Eq b, Eq a) => Eq (Pair a b)
*** Offending Program ***
$c==_a2Cw
  :: forall a b. (Eq b, Eq a) => Pair a b -> Pair a b -> Bool
[LclId]
$c==_a2Cw
  = \ (@ a_a2Cr)
      (@ b_a2Cs)
      ($dEq_a2Ct :: Eq b_a2Cs)
      ($dEq_a2Cu :: Eq a_a2Cr)
      (ds_d2Dz :: Pair a_a2Cr b_a2Cs)
      (ds_d2DA :: Pair a_a2Cr b_a2Cs) ->
      case ds_d2Dz of { Pair a1_a2Cn a2_a2Co ->
      case ds_d2DA of { Pair b1_a2Cp b2_a2Cq ->
      &&
        (== @ a_a2Cr $dEq_a2Cu a1_a2Cn b1_a2Cp)
        (== @ b_a2Cs $dEq_a2Ct a2_a2Co b2_a2Cq)
      }
      }

Rec {
$fEqPair [InlPrag=NOUSERINLINE CONLIKE]
  :: forall a b. (Eq Any, Eq Any) => Eq (Pair Any Any)
[LclIdX[DFunId],
 Unf=DFun: \ (@ a_a2z3[tau:1])
             (@ b_a2z4[tau:1])
             (v_B1 :: Eq b_a2z4[tau:1])
             (v_B2 :: Eq a_a2z3[tau:1]) ->
       C:Eq TYPE: Pair a_a2z3[tau:1] b_a2z4[tau:1]
            $c==_a2Cw @ a_a2z3[tau:1] @ b_a2z4[tau:1] v_B1 v_B2
            $c/=_a2CF @ a_a2z3[tau:1] @ b_a2z4[tau:1] v_B1 v_B2]
$fEqPair
  = \ (@ a_a2Cr)
      (@ b_a2Cs)
      ($dEq_a2Ct :: Eq b_a2Cs)
      ($dEq_a2Cu :: Eq a_a2Cr) ->
      C:Eq
        @ (Pair a_a2Cr b_a2Cs)
        ($c==_a2Cw @ a_a2Cr @ b_a2Cs $dEq_a2Ct $dEq_a2Cu)
        ($c/=_a2CF @ a_a2Cr @ b_a2Cs $dEq_a2Ct $dEq_a2Cu)

$c/=_a2CF [Occ=LoopBreaker]
  :: forall a b. (Eq b, Eq a) => Pair a b -> Pair a b -> Bool
[LclId]
$c/=_a2CF
  = \ (@ a_a2Cr)
      (@ b_a2Cs)
      ($dEq_a2Ct :: Eq b_a2Cs)
      ($dEq_a2Cu :: Eq a_a2Cr) ->
      $dm/=
        @ (Pair a_a2Cr b_a2Cs)
        ($fEqPair @ a_a2Cr @ b_a2Cs $dEq_a2Ct $dEq_a2Cu)
end Rec }

$trModule :: Module
[LclIdX]
$trModule = Module (TrNameS "main"#) (TrNameS "Bug"#)

$krep_a2Dx [InlPrag=NOUSERINLINE[~]] :: KindRep
[LclId]
$krep_a2Dx = $WKindRepVar (I# 1#)

$krep_a2Dv [InlPrag=NOUSERINLINE[~]] :: KindRep
[LclId]
$krep_a2Dv = $WKindRepVar (I# 0#)

$tcPair :: TyCon
[LclIdX]
$tcPair
  = TyCon
      13156152634686180623##
      12550973000996521707##
      $trModule
      (TrNameS "Pair"#)
      0#
      krep$*->*->*

$krep_a2Dy [InlPrag=NOUSERINLINE[~]] :: KindRep
[LclId]
$krep_a2Dy
  = KindRepTyConApp
      $tcPair
      (: @ KindRep $krep_a2Dv (: @ KindRep $krep_a2Dx ([] @ KindRep)))

$krep_a2Dw [InlPrag=NOUSERINLINE[~]] :: KindRep
[LclId]
$krep_a2Dw = KindRepFun $krep_a2Dx $krep_a2Dy

$krep_a2Du [InlPrag=NOUSERINLINE[~]] :: KindRep
[LclId]
$krep_a2Du = KindRepFun $krep_a2Dv $krep_a2Dw

$tc'Pair :: TyCon
[LclIdX]
$tc'Pair
  = TyCon
      13419949030541524809##
      8448108315116356699##
      $trModule
      (TrNameS "'Pair"#)
      2#
      $krep_a2Du

*** End of Offense ***


<no location info>: error: 
Compilation had errors


*** Exception: ExitFailure 1

I've tried various combinations of zonkTcTypes and zonkTcTypeToTypes, but none of them work, so I'm thoroughly stuck here.

comment:48 Changed 2 years ago by goldfire

I'm taking a look at your work, but it would be much more ergonomic to review this in Phab.

Rough comments:

  • Why the newMetaTyVars at the top? That doesn't look right to me.
  • You're trying to swap the tcUnifyTy with a unifyType. Good. But the tcUnifyTy is still there. Is this intentional or an aspect of the fact that this is w.i.p.?
  • Before you call unifyType, you need to have metavariables that unifyType will unify. According to comment:31, these variables should be as specified in step (h) of the algorithm. So perhaps you do need newMetaTyVars, but not over all the tvs, just a subset of them.
  • The second half of step (i) of the algorithm (skolemizing unbound metavariables) might nicely be accomplished by quantifyTyVars. It's a bit unclear to me without thinking more about this whether this function does too much, but its helper function zonkQuantifiedTyVar is definitely what you need to do.

I hope this gets you going again...

comment:49 Changed 2 years ago by RyanGlScott

I posted this to a branch instead of Phab per SPJ's request, since he says he finds that easier to navigate than Phab.

As far as newMetaTyVars goes: yes, I'm aware that I needn't call newMetaTyVars on everything in tvs. As I mentioned, I'm taking this piece-by-piece, and I wanted to get the simple case where the deriving clause mentions no variables working first before I add additional complexity on top (especially since the simple case is proving to be so difficult).

I still need the tcUnifyTy because of this validity check: https://github.com/RyanGlScott/ghc/commit/d8ed9e57ecc60a78321ab10b02f6387759d2c82e#diff-6ce1356ff43cc56932867d6f6b63d7dcR718

I'm quite confused at all the different variants of of zonkWibbleWobble out there. There's zonkTcType and zonkTcTypeToType for starters (whose simultaneous existence still baffles me), and now there's zonkQuantifiedTyVar and zonkTyBndrX‽ How is someone like me who isn't in the loop supposed to be able to discern all of these little idiosyncrasies?

(Sorry, rant over. I frequently get overwhelmed at all of the arcane knowledge one needs to make simple changes to the typechecker.)

Last edited 2 years ago by RyanGlScott (previous) (diff)

comment:50 Changed 2 years ago by goldfire

Most of the arcane knowledge is just knowledge of Haskell. The rest is but a small epsilon... :)

There are basically two families of zonking functions:

  1. The functions defined in TcMType do an intermediate zonk. They squeeze out filled-in metavariables but don't run into trouble (or do anything, really) if they encounter an unfilled metavariable. The most frequently called function from this family is zonkTcType. These functions are needed during type-checking when, say, we are about to look at the free variables of something. Doing that without zonking first might give wrong information.
  1. The functions defined in TcHsSyn (such as zonkTcTypeToType) do a final zonk. If one of these functions encounters a metavariable, that metavariable is zonked to Any (most of the time -- details unimportant at the moment). This zonking happens when desugaring the type-checked program into Core; it also happens when building tycons from user-written type declarations.

The basic idea is that we would like to consider TcType and Type as two separate types; the former lives in the type-checker and the latter lives in Core. zonkTcType both takes and returns a TcType. zonkTcTypeToType takes a TcType and returns a Type.

As for zonkQuantifiedTyVar: that does more than just zonk -- it also skolemizes. (That is, it takes an unfilled metavariable and turns it into a skolem, which is useful when you're about to generalize.) Contrast with zonkTyBndrX (part of the final zonk), which expects a skolem to begin with.

I remember it took years before I finally grokked zonking. And now I can't tell you why it seemed so hard!

comment:51 Changed 2 years ago by goldfire

What do we think of

class Cat k (cat :: k -> k -> *) where
  catId   :: cat a a
  catComp :: cat b c -> cat a b -> cat a c

instance Cat * (->) where
  catId   = id
  catComp = (.)

newtype Fun1 a b = Fun1 (a -> b) deriving (Cat k)

This is currently accepted and in the testsuite as deriving/should_compile/T11732c. I think this should fail, because it requires unifying k with Type. There is useful commentary in #11732.

In my work on #14066, I had to remove this line from the test case, leaving a note pointing to this ticket. Please update the test case when this ticket is finally put to rest.

Last edited 2 years ago by goldfire (previous) (diff)

comment:52 Changed 2 years ago by RyanGlScott

I assume we're treating the k in deriving (Cat k) and the k in deriving (forall k. Cat k) the same? If so, then yes, this program should fail.

comment:53 Changed 2 years ago by Iceland_jack

Intuition: I would expect to have to write deriving (Cat Type).

comment:54 Changed 2 years ago by goldfire

I agree wholeheartedly with comment:52 and comment:53, but this is at odds with what we (the same we!) concluded in #11732. I'm OK with a change of mind here, but I just want to call this out as different than what we thought previously.

comment:55 Changed 2 years ago by RyanGlScott

I'm not sure how this is at odds? The example from #11732 is:

data Proxy k (a :: k) = ProxyCon deriving Generic1

Here, we are unifying a kind variable from the datatype with Type, which is acceptable, instead of a kind variable from the class (as is the case in comment:51), which should be an error. Or am I missing something?

comment:56 Changed 2 years ago by simonpj

Ryan is spot on in comment:55 (i.e. this is different to #11732), and also in comment:52 (i.e. deriving( Cat k ) should fail if we really mean deriving( Cat Type ).

Ryan this is in your patch, indeed right in the area you have in-flight work on.

Last edited 2 years ago by simonpj (previous) (diff)

comment:57 Changed 2 years ago by Iceland_jack

comment:56 is self-referential :-)

comment:58 Changed 2 years ago by goldfire

See comment:14:ticket:11732 and environs for how this is at odds. But it's probably not worth rehashing it all.

comment:59 Changed 2 years ago by Iceland_jack

How about inferring wildcards? Should I open a ticket

newtype Fun1 a b = Fun1 (a -> b) deriving (Cat _)

comment:60 Changed 2 years ago by RyanGlScott

Sorry goldfire, I didn't realize you were referring to comment:14:ticket:11732 in particular when you referenced #11732 (which has a much different program than the original one I copy-pasted in comment:55). Yes, I was originally of the belief that deriving should be allowed to unify whatever it likes, which is why I originally argued so vehemently against the ideas put forth in this ticket. I've since changed my opinion on the matter after reading the discussion here, and believe that the program in comment:14:ticket:11732 should fail.

FWIW, programs like in comment:14:ticket:11732 are quite rare in practice, so I wouldn't anticipate too much breakage from disallowing them. The only comparable example that I can think of which is widely used in practice is when you derive Generic1, since the kind of Generic1 is (k -> Type) -> Constraint, and one frequently unifies that k with Type. Fortunately, almost everyone writes their derived Generic1 instances as

data Foo (a :: Type) = ... deriving Generic1

where the k argument to Generic1 isn't specified, so it's allowed to freely unify with Type. It'd be a problem if folks were writing the above as

data Foo (a :: Type) = ... deriving ((Generic1 :: (k -> Type) -> Constraint)) 

But thankfully, only crazy people like myself have ever attempted this. :)

comment:61 Changed 2 years ago by bgamari

Milestone: 8.4.18.6.1

This ticket won't be resolved in 8.4; remilestoning for 8.6. Do holler if you are affected by this or would otherwise like to work on it.

comment:62 Changed 18 months ago by bgamari

Milestone: 8.6.18.8.1

These won't be addressed in GHC 8.6.

comment:63 Changed 17 months ago by RyanGlScott

Blocking: 15376 added

comment:64 Changed 17 months ago by RyanGlScott

#15376 is a symptom of this.

comment:65 Changed 17 months ago by simonpj

I'm a bit lost as to where we are on this ticket.

comment:66 Changed 17 months ago by RyanGlScott

No one has attempted to implemented comment:31, so there's been no progress on it.

comment:67 Changed 12 months ago by osa1

Milestone: 8.8.18.10.1

Bumping milestones of low-priority tickets.

comment:68 Changed 11 months ago by RyanGlScott

Visible kind application adds another layer of screwball-ery to the mix:

{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeApplications #-}
module Bug where

import Data.Kind

class Cat (cat :: k -> k -> Type)
instance Cat (->)
newtype Fun1 a b = Fun1 (a -> b)
  deriving (Cat @k)
$ ~/Software/ghc/inplace/bin/ghc-stage2 --interactive Bug.hs -ddump-deriv -fprint-explicit-kinds
GHCi, version 8.7.20190105: https://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug              ( Bug.hs, interpreted )

==================== Derived instances ====================
Derived class instances:
  instance Bug.Cat @* Bug.Fun1 where
  

Derived type family instances:


Ok, one module loaded.
Note: See TracTickets for help on using tickets.