Opened 20 months ago

Closed 19 months ago

Last modified 18 months ago

#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 RyanGlScott

Sure enough, slightly tweaking the third program can tickle a Core Lint error:

{-# 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 = undefined
$ /opt/ghc/8.2.2/bin/ghc Bug.hs -dcore-lint
[1 of 1] Compiling Bug              ( Bug.hs, Bug.o )
*** Core Lint errors : in result of Desugar (after optimization) ***
<no location info>: warning:
    In the expression: undefined
                         @ 'LiftedRep @ (T () ('Identity '())) $dIP_a2e7
    Kind application error in type ‘T () ('Identity '())’
      Function kind = forall a -> a -> *
      Arg kinds = [((), *), ('Identity '(), Identity ())]
Bug.hs:19:1: warning:
    [RHS of f :: T (Identity ()) ('Identity '())]
    @ a2_a1bw is out of scope
*** Offending Program ***
$fC() [InlPrag=CONLIKE] :: C ()
[LclIdX[DFunId], Unf=DFun: \ -> C:C TYPE: ()]
$fC() = C:C @ ()

$fCIdentity [InlPrag=CONLIKE] :: forall a. C (Identity a)
[LclIdX[DFunId], Unf=DFun: \ (@ a_aWB) -> C:C TYPE: Identity a_aWB]
$fCIdentity = \ (@ a_a2ea) -> C:C @ (Identity a_a2ea)

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

$krep_a2pm [InlPrag=[~]] :: KindRep
[LclId]
$krep_a2pm = KindRepTyConApp $tcConstraint ([] @ KindRep)

$krep_a2pl [InlPrag=[~]] :: KindRep
[LclId]
$krep_a2pl = KindRepFun krep$* $krep_a2pm

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

$tcC :: TyCon
[LclIdX]
$tcC
  = TyCon
      12754692886077552850##
      18375870125396612007##
      $trModule
      (TrNameS "C"#)
      0#
      $krep_a2pl

$krep_a2pn [InlPrag=[~]] :: KindRep
[LclId]
$krep_a2pn
  = KindRepTyConApp $tcC (: @ KindRep $krep_a2po ([] @ KindRep))

$tc'C:C :: TyCon
[LclIdX]
$tc'C:C
  = TyCon
      302756782745842909##
      14248103394115774781##
      $trModule
      (TrNameS "'C:C"#)
      1#
      $krep_a2pn

$dIP_a2e7 :: HasCallStack
[LclId]
$dIP_a2e7
  = (pushCallStack
       (unpackCString# "undefined"#,
        SrcLoc
          (unpackCString# "main"#)
          (unpackCString# "Bug"#)
          (unpackCString# "Bug.hs"#)
          (I# 19#)
          (I# 5#)
          (I# 19#)
          (I# 14#))
       ((emptyCallStack
         `cast` (Sym (N:IP[0] <"callStack">_N <CallStack>_N)
                 :: (CallStack :: *) ~R# ((?callStack::CallStack) :: Constraint)))
        `cast` (N:IP[0] <"callStack">_N <CallStack>_N
                :: ((?callStack::CallStack) :: Constraint) ~R# (CallStack :: *))))
    `cast` (Sym (N:IP[0] <"callStack">_N <CallStack>_N)
            :: (CallStack :: *) ~R# ((?callStack::CallStack) :: Constraint))

f :: T (Identity ()) ('Identity '())
[LclIdX]
f = (undefined @ 'LiftedRep @ (T () ('Identity '())) $dIP_a2e7)
    `cast` (Sub
              (Sym (R:TIdentityx[0] <()>_N <a2_a1bw>_N <'Identity '()>_N))
            :: (T () ('Identity '()) :: *)
               ~R#
               (T (Identity ()) ('Identity '()) :: *))

*** End of Offense ***


<no location info>: error: 
Compilation had errors

comment:2 Changed 20 months ago by RyanGlScott

I can see two ways out of this mess:

  1. 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 Types directly in TcGenDeriv, so we have to take it on faith that TcGenDeriv is doing the right thing.
  2. 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 for Loop 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 Changed 20 months ago 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.

comment:4 in reply to:  3 Changed 20 months ago by RyanGlScott

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-level runIdentity 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 use HsCoreTy to embed it into HsSyn. Then, runIdentity is just a cast by the axiom induced by the Identity 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 RyanGlScott

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 Changed 20 months ago by goldfire

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 in reply to:  6 ; Changed 20 months ago by RyanGlScott

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 Iceland_jack

Cc: Iceland_jack added

comment:9 in reply to:  7 Changed 20 months ago by RyanGlScott

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 RyanGlScott

Differential Rev(s): Phab:D4402
Status: newpatch

I've implemented the "stopgap solution" (mentioned in comment:9) in Phab:D4402.

comment:11 Changed 19 months ago by bgamari

Milestone: 8.4.1

comment:12 Changed 19 months ago by bgamari

Status: patchmerge

comment:13 Changed 19 months ago by Ben Gamari <ben@…>

In 1ede46d4/ghc:

Implement stopgap solution for #14728

It turns out that one can produce ill-formed Core by
combining `GeneralizedNewtypeDeriving`, `TypeInType`, and
`TypeFamilies`, as demonstrated in #14728. The root of the problem
is allowing the last parameter of a class to appear in a //kind// of
an associated type family, as our current approach to deriving
associated type family instances simply doesn't work well for that
situation.

Although it might be possible to properly implement this feature
today (see https://ghc.haskell.org/trac/ghc/ticket/14728#comment:3
for a sketch of how this might work), there does not currently exist
a performant implementation of the algorithm needed to accomplish
this. Until such an implementation surfaces, we will make this corner
case of `GeneralizedNewtypeDeriving` an error.

Test Plan: make test TEST="T14728a T14728b"

Reviewers: bgamari

Reviewed By: bgamari

Subscribers: rwbarton, thomie, carter

GHC Trac Issues: #14728

Differential Revision: https://phabricator.haskell.org/D4402

comment:14 Changed 19 months ago by bgamari

Resolution: fixed
Status: mergeclosed

comment:15 Changed 18 months ago by RyanGlScott

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 RyanGlScott

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).

Note: See TracTickets for help on using tickets.