#14728 closed bug (fixed)
Is (GeneralizedNewtypeDeriving + associated type classes) completely bogus?
Reported by: | RyanGlScott | Owned by: | |
---|---|---|---|
Priority: | normal | Milestone: | 8.4.1 |
Component: | Compiler (Type checker) | Version: | 8.2.2 |
Keywords: | deriving, TypeFamilies | Cc: | Iceland_jack |
Operating System: | Unknown/Multiple | Architecture: | Unknown/Multiple |
Type of failure: | None/Unknown | Test Case: | |
Blocked By: | Blocking: | ||
Related Tickets: | Differential Rev(s): | Phab:D4402 | |
Wiki Page: |
Description
In Phab:D2636, I implemented this ability to use GeneralizedNewtypeDeriving
to derive instances of type classes with associated type families. At the time, I thought the implementation was a no-brainer, but now I'm starting to have second thoughts. To explain what I mean, consider this program:
{-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeInType #-} module Bug where import Data.Functor.Identity import Data.Kind class C (a :: Type) where type T a (x :: a) :: Type instance C () where type T () '() = Bool deriving instance C (Identity a)
Quite to my surprise, this typechecks. Let's consult -ddump-deriv
to figure out what code is being generated:
$ /opt/ghc/8.2.2/bin/ghci Bug.hs -ddump-deriv GHCi, version 8.2.2: http://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.C (Data.Functor.Identity.Identity a) where Derived type family instances: type Bug.T (Data.Functor.Identity.Identity a1_a1M3) x_a1M5 = Bug.T a1_a1M3 x_a1M5
Hm... OK. Since GHC was able to generate this code, surely we should be able to write it ourselves, right?
{-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeInType #-} module Bug where import Data.Functor.Identity import Data.Kind class C (a :: Type) where type T a (x :: a) :: Type instance C () where type T () '() = Bool -- deriving instance C (Identity a) instance C (Identity a) where type T (Identity a) x = T a x
$ /opt/ghc/8.2.2/bin/ghci Bug.hs GHCi, version 8.2.2: http://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/rgscott/.ghci [1 of 1] Compiling Bug ( Bug.hs, interpreted ) Bug.hs:19:31: error: • Occurs check: cannot construct the infinite kind: a ~ Identity a • In the second argument of ‘T’, namely ‘x’ In the type ‘T a x’ In the type instance declaration for ‘T’ | 19 | type T (Identity a) x = T a x | ^
Uh-oh. GHC gets quite angry when we try to type this in ourselves, which isn't a good sign. This raises the question: just what is GHC doing in the previous version of the program? I tried to answer that question by seeing if T (Identity a) x
could ever reduce:
{-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeInType #-} module Bug where import Data.Functor.Identity import Data.Kind class C (a :: Type) where type T a (x :: a) :: Type instance C () where type T () '() = Bool deriving instance C (Identity a) f :: T (Identity ()) ('Identity '()) f = True
And lo and behold, you get:
$ /opt/ghc/8.2.2/bin/ghci Bug.hs GHCi, version 8.2.2: http://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/rgscott/.ghci [1 of 1] Compiling Bug ( Bug.hs, interpreted ) Bug.hs:19:5: error: • Couldn't match type ‘T () ('Identity '())’ with ‘Bool’ Expected type: T (Identity ()) ('Identity '()) Actual type: Bool • In the expression: True In an equation for ‘f’: f = True | 19 | f = True | ^^^^
It appears that T (Identity ()) ('Identity '())
reduced to T () ('Identity '())
. At that point, it becomes stuck. (Perhaps it's for the best that it's the case—if T () ('Identity '())
managed to reduce, who knows what kind of mischief GHC could get itself into.)
But all of this leads me to wonder: is something broken in the implementation of this feature, or is GeneralizedNewtypeDeriving
simply not sound with respect to associated type families? I certainly hope that it's not the latter, as it's quite a useful feature. But at the same time, it's hard to reconcile that usefulness with the strange behavior above.
Change History (16)
comment:1 Changed 20 months ago by
comment:2 Changed 20 months ago by
I can see two ways out of this mess:
- We should kind-check associated type family instances that are generated in derived code. This would have caught these mistakes early (and just seems like a good idea in general). Currently, we simply generate
Type
s directly inTcGenDeriv
, so we have to take it on faith thatTcGenDeriv
is doing the right thing. - Disallow occurrences of the derived class's last type parameter as a kind within an associated type family. I believe the sketchiness witnesses above only happens when this criterion is met, so we could just disallow that wholesale.
One downside is that there would actually be a small class of programs that would be ruled out by this restriction. Namely:
{-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeInType #-} {-# LANGUAGE UndecidableInstances #-} module Bug where import Data.Kind class C (a :: Type) where type T a (x :: a) :: Type newtype Loop = Loop Loop deriving instance C Loop
This currently compiles (and genuinely kind-checks), but would fail to compile if we instituted the aforementioned kind validity check. But this isn't too much of a loss, as actually trying to use the
T
instance forLoop
would, well, infinitely loop. :)
Option (2) sounds much simpler, so I think I'd be inclined to favor that for the time being.
comment:3 follow-up: 4 Changed 20 months ago by
type T (Identity a) x = T a x
is ill-kinded, sure enough. Let's write out the details:
Identity :: Type -> Type 'Identity :: forall (a :: Type). a -> Identity a T :: pi (x :: Type) -> x -> Type type instance forall (a :: Type) (x :: Identity a). T (Identity a) x = T a x
In the last line, the x
has the wrong kind: it has kind Identity a
, where it really should have kind a
. Here's the correct type instance:
type instance forall (a :: Type) (x :: Identity a). T (Identity a) x = T a ('runIdentity x)
where I've used '
to use the term-level runIdentity
function in a type.
I don't think this would be impossible to support. Currently, the deriving
mechanism produces HsSyn. I suppose that makes it easier w.r.t. inferring contexts and such. But suppose we could write the RHS of type instances in Core, and use HsCoreTy
to embed it into HsSyn. Then, runIdentity
is just a cast by the axiom induced by the Identity
newtype.
But it gets more complicated, sadly.
class D a where type S a (x :: Maybe a) deriving instance D (Identity a)
This would need to produce
type instance forall (a :: Type) (x :: Maybe (Identity a)). S (Identity a) x = S a (x |> g) where g :: Maybe (Identity a) ~ Maybe a g = Maybe axIdentity
This example shows us that just using the newtype axiom isn't enough. We need to take the type of x
, find all occurrences of a
in it, and rewrite those to be axIdentity
instead. Happily, GHC already has implemented this operation: it's called Coercion.liftCoSubst
. A detailed explanation of lifting is in the "System FC with Explicit Kind Equalities" paper (among other places, I think). It's useful when you have a coercion between ty1
and ty2
(in our case, the newtype axiom) and you need a coercion between ty3[ty1/a]
and ty3[ty2/a]
-- precisely our scenario.
But it gets even worse.
Suppose now later parameters to the type family depend on x
. These will have to account for the change in x
's type. So we need a coercion relating the old x
to the new, casted x
, which will then be used to cast those later parameters. Happily, I've already worked out the algorithm to deal with this more general case, and I've implemented it in my branch (github.com/goldfirere/ghc, on the wip/rae branch), in TcFlatten.flatten_args
. This branch is not merged due to performance trouble, but the algorithm is correct.
Actually, as I'm writing this all up, I realize that FamInstEnv.normaliseType
is behind the times here. It, too, needs to take all of these challenges into account in order to produce a well-kinded output. I'll post a new bug to this effect.
Is it worth doing all of these here, for GND? Probably not. And I think the idea of "just don't allow this" may be best. However, it's good to know that we could do this if we wanted.
comment:4 Changed 20 months ago by
Replying to goldfire:
Here's the correct type instance:
type instance forall (a :: Type) (x :: Identity a). T (Identity a) x = T a ('runIdentity x)where I've used
'
to use the term-levelrunIdentity
function in a type.
This requires Dependent Haskell, I presume?
I don't think this would be impossible to support. Currently, the
deriving
mechanism produces HsSyn. I suppose that makes it easier w.r.t. inferring contexts and such. But suppose we could write the RHS of type instances in Core, and useHsCoreTy
to embed it into HsSyn. Then,runIdentity
is just a cast by the axiom induced by theIdentity
newtype.
One correction: deriving
only uses HsSyn for derived methods. It does in fact generate Core
for the RHS of type instances. So what you describe might be possible today? (I'm not sure I follow the other details, so it's hard for me to say.)
This would need to produce
type instance forall (a :: Type) (x :: Maybe (Identity a)). S (Identity a) x = S a (x |> g) where g :: Maybe (Identity a) ~ Maybe a g = Maybe axIdentity
axIdentity
? What sorcery is this?
Actually, as I'm writing this all up, I realize that
FamInstEnv.normaliseType
is behind the times here. It, too, needs to take all of these challenges into account in order to produce a well-kinded output. I'll post a new bug to this effect.
Interesting. Is there a program that exhibits this bug (that doesn't leverage this GND business)?
Is it worth doing all of these here, for GND? Probably not. And I think the idea of "just don't allow this" may be best. However, it's good to know that we could do this if we wanted.
Indeed. And we could quite easily change this design in the future, so I'm not too worried about being conservative for now.
comment:5 Changed 20 months ago by
And by "What sorcery is this", I mean: can the user write this incantation themselves? Or are these magicks that are only accessible in Core?
Is there a program that exhibits this bug (that doesn't leverage this GND business)?
This question was answered in #14729.
comment:6 follow-up: 7 Changed 20 months ago by
Good about generating Core for type instances. Then this is all doable today.
axIdentity
is the newtype axiom that comes into being when a user declares a newtype. It can be accessed by coerce
, but is mostly internal magic. Specifically, if you write
newtype N a b c = MkN (some_type)
then we get
axN :: N a b c ~R some_type
as an axiom (type CoAxiom
in GHC).
comment:7 follow-up: 9 Changed 20 months ago by
Replying to goldfire:
Good about generating Core for type instances. Then this is all doable today.
That's great! I can't claim to know where to proceed from here, though—the details of pushing this cast through axioms is still quite fuzzy to me.
Is this blocked (at least partially) on getting your branch merged and/or fixing #14729?
comment:8 Changed 20 months ago by
Cc: | Iceland_jack added |
---|
comment:9 Changed 20 months ago by
After talking to goldfire about this, I can answer my earlier question in comment:7:
Replying to RyanGlScott:
Is this blocked (at least partially) on getting your branch merged and/or fixing #14729?
The short answer is: no.
The long answer is: what goldfire was suggesting in comment:3 was that an intrepid GHC hacker could look at the innards of his GHC fork at https://github.com/goldfirere/ghc and, conceivably, adapt the logic he uses in TcFlatten.flatten_args
to come up with an algorithm that would fix the problem in this ticket. (I had mistakenly though he meant that liftCoSubst
was this algorithm, but in fact, it's only one component of it.)
That being said, the performance of TcFlatten.flatten_args
is apparently pretty bad, so adapting it in its current state might not be the wisest course of action. In light of this, I think I'll hold off on this idea for now and proceed with option (2) in comment:2 as a stopgap solution.
comment:10 Changed 20 months ago by
Differential Rev(s): | → Phab:D4402 |
---|---|
Status: | new → patch |
I've implemented the "stopgap solution" (mentioned in comment:9) in Phab:D4402.
comment:11 Changed 19 months ago by
Milestone: | → 8.4.1 |
---|
comment:12 Changed 19 months ago by
Status: | patch → merge |
---|
comment:14 Changed 19 months ago by
Resolution: | → fixed |
---|---|
Status: | merge → closed |
Merged with 0f78f18129d24f17154ae7dca84937fddd1f8b0c.
comment:15 Changed 18 months ago by
So flatten_args
has been merged into GHC, so in theory, this ticket is unblocked now. However, after looking at flatten_args
, I have no idea how it relates to this idea. What I was expected (after reading the description in comment:3) was some sort of function of type:
Type -> Coercion -> Type
Where in the example in comment:3, the Type
argument would be S (Identity a) x
, the Coercion
argument would be the newtype axiom g :: Identity a ~R# a
, and the result Type
would be S a (x |> g)
. But flatten_args
doesn't look very much like this at all, so I'm plain stumped.
comment:16 Changed 18 months ago by
I completely take back what I said in comment:15 about this being unblocked—that couldn't be further from the truth! In fact, after talking with goldfire and kcsongor about this, we've come to the realization that all of the ideas in comment:3 are completely untenable at present.
The issue is that we're trying to construct the type (x |> g)
, where x
is a type and g
is a coercion. However, in order for this to kind-check, g
must be nominally roled. This is never the case in GND, as we always use newtype axioms, which are by definition representationally roled!
This pretty much makes this idea dead in the water, at least until we figure out a way to have representational casts in kinds (which is likely a ways away).
Sure enough, slightly tweaking the third program can tickle a Core Lint error: