#14728: Is (GeneralizedNewtypeDeriving + associated type classes) completely bogus? -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.2.2 checker) | Keywords: deriving, Resolution: | TypeFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): `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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14728#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler