Opened 2 years ago
Last modified 13 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
comment:2 follow-up: 3 Changed 2 years ago by
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.)
comment:3 Changed 2 years ago by
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 forall
s 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
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
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 follow-up: 7 Changed 2 years ago by
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 Changed 2 years ago by
Replying to goldfire:
But I see
instance C (a :: k) D
as fully equivalent toinstance 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 forall
s 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 follow-up: 9 Changed 2 years ago by
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 Changed 2 years ago by
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:11 Changed 2 years ago by
Milestone: | → 8.2.2 |
---|---|
Status: | new → merge |
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
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
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. But the first thing is to decide what we want.
comment:14 Changed 2 years ago by
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 forall
s 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>
).
comment:15 Changed 2 years ago by
For what it's worth, I agree with Ryan in what GHC should do here.
comment:16 Changed 2 years ago by
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.
comment:17 Changed 2 years ago by
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
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
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 follow-up: 21 Changed 2 years ago by
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 Changed 2 years ago by
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 C2do I mean
instance C2 {k -> Type} Dor
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
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
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
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?
comment:25 Changed 2 years ago by
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
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
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
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?
comment:29 follow-up: 30 Changed 2 years ago by
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 Changed 2 years ago by
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
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:
- The variables introduces in the
data
declaration head scope over thederiving
clause. (Throughout this comment,newtype
is treated identically todata
.) This is true even for GADT-syntax declarations where any variables in the head typically have no scope.
- Any type variables mentioned in a
deriving
clause but not already in scope are brought into scope locally in thatderiving
clause. Independent comma-separated clauses are separate and quantify separately.
- The user may write an explicit
forall
in aderiving
clause scoped over only one clause. If the user writes aforall
, it must bind every type variable not brought into scope by thedata
declaration. Thisforall
is understood as a scoping construct, not quite as a full-bloodedforall
, which normally requires its body to have kindTYPE r
for somer
.
- Process a
data
declaration on its own, without further regard to anyderiving
clauses.
- For each
deriving
clause:- Let the kind of the head of the clause (the part without the
forall
) beki
and the set of variables locally quantified bebs
. Let the head of the clause bedrv
. - Instantiate
ki
with fresh unification variables for any kind variables inki
. (This is vanilla instantiation for an applied type.) - Unify
ki
withkappa -> Constraint
, getting a substitution forkappa
; let the result of this substitution beki2
. (Issue an error if unification fails.) - It is required that
ki2
have the form... -> Type
orkappa2
for some unification variablekappa2
. Ifki2
iskappa2
, then choosekappa2 := Type
. Now, we have something of the form... -> Type
. Let the number of arguments in the...
ben
. - Let the set of variables mentioned in the
deriving
clause but not locally scoped (that is, they are also mentioned in thedata
declaration head) beas
. - It is an error if any variable in
as
is mentioned in any of the lastn
arguments in thedata
declaration head. Data family instances need even more checks. - Drop the last
n
arguments (whether visible or invisible) to the datatype. Call the resultty
. - Replace any type variables in
ty
but not mentioned in thederiving
clause with fresh unification variables. - Unify the kind of
ty
withki2
, issuing an error if unification fails. Zonkty
, replacing any unfilled unification variable with fresh skolems. Call the set of these skolemssks
. - 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. - Solve for the unknown context
...
and insert that into the declaration. - Declare victory.
- Let the kind of the head of the clause (the part without the
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.
comment:32 follow-up: 33 Changed 2 years ago by
Thanks Richard, this looks wonderful. I have some questions/comments about your algorithm:
- What happens if the user writes an explicit
forall
in aderiving
clause but leaves out a variable, such as indata Foo a = ... deriving (forall b. C b c)
?
Also, in what sense is this not a "full-blooded
forall
"?
- c. I'm not sure I understand this business about
kappa2
(or why you'd choosekappa2 := Type
). Can you give an example of where this would arise?
- e. Some more validity checks that would need to be performed for data family instances are documented here.
- 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 haveclass C k (a :: k)
) since thek
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 thek
indata D = D deriving (C k)
also get skolemized?
comment:33 follow-up: 34 Changed 2 years ago by
I've clarified point 3, above.
Replying to RyanGlScott:
- c. I'm not sure I understand this business about
kappa2
(or why you'd choosekappa2 := 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.
- e. Some more validity checks that would need to be performed for data family instances are documented here.
I've updated my algorithm. Thanks.
- 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 thek
indata 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 Changed 2 years ago by
Replying to goldfire:
class C a data D a = D deriving CWe see that
C :: forall k. k -> Constraint
. So we haveki
=forall k. k -> Constraint
. We then instantiate (note new step, above) to getki
=kappa3 -> Constraint
, wherekappa3
is a fresh unification variable. Unifying withkappa -> Constraint
simply setskappa := kappa3
. So,ki2
is really justkappa3
. 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
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
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 follow-up: 38 Changed 2 years ago by
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.
- 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.)
- Do it properly. That is, after simplifying the instance constraints we'll end up with
k~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 Changed 2 years ago by
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.
- 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".
- Do it properly. That is, after simplifying the instance constraints we'll end up with
k~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
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
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
What is the conclusion here? Do we want to merge comment:10 to 8.2.2?
comment:42 Changed 2 years ago by
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
Milestone: | 8.2.2 → 8.4.1 |
---|---|
Status: | merge → new |
Alright, let's punt then.
comment:44 Changed 2 years ago by
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
I would be willing to try this, but implementing this would require knowledge that I'm not currently privy to...
comment:47 Changed 2 years ago by
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
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 aunifyType
. Good. But thetcUnifyTy
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 thatunifyType
will unify. According to comment:31, these variables should be as specified in step (h) of the algorithm. So perhaps you do neednewMetaTyVars
, 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 functionzonkQuantifiedTyVar
is definitely what you need to do.
I hope this gets you going again...
comment:49 Changed 2 years ago by
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.)
comment:50 Changed 2 years ago by
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:
- 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 iszonkTcType
. 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.
- The functions defined in
TcHsSyn
(such aszonkTcTypeToType
) do a final zonk. If one of these functions encounters a metavariable, that metavariable is zonked toAny
(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
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.
comment:52 Changed 2 years ago by
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:54 Changed 2 years ago by
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
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
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.
comment:58 Changed 2 years ago by
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
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
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
Milestone: | 8.4.1 → 8.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:63 Changed 18 months ago by
Blocking: | 15376 added |
---|
comment:66 Changed 18 months ago by
No one has attempted to implemented comment:31, so there's been no progress on it.
comment:67 Changed 13 months ago by
Milestone: | 8.8.1 → 8.10.1 |
---|
Bumping milestones of low-priority tickets.
comment:68 Changed 13 months ago by
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.
I spoke too soon about that second program (with data families) working. It turns out that it's rejected on GHC HEAD: