"deriving newtype instance" generates an infinite loop

changed weight to 5

changed the description

I'm afraid that I can't reproduce the issue. Can you post a minimal example (preferably with no external dependencies like esqueleto) that demonstrates the bug?

This loops in the REPL:

:set -XDerivingStrategies 
:set -XFlexibleInstances 
:set -XFunctionalDependencies
:set -XGeneralizedNewtypeDeriving 
:set -XMultiParamTypeClasses 
:set -XStandaloneDeriving
:set -XUndecidableInstances

import Data.Proxy

class C a b | a -> b, b -> a where c :: Proxy a -> Int
instance C Int Int where c _ = 1

newtype X a b = X { unX :: b }
deriving newtype instance C a b => C (X String a) (X String b)

when I evaluate

> c (Proxy :: Proxy (X String Int))

Most likely UndecidableInstances is the culprit here, since I can't derive the instance otherwise, but it seems like it should be possible to derive anyway.

-ddump-deriv shows this:

Derived class instances:
  instance Ghci1.C a b =>
           Ghci1.C
             (Ghci3.X GHC.Base.String a) (Ghci3.X GHC.Base.String b) where
    Ghci1.c
      = GHC.Prim.coerce
          @((Data.Proxy.Proxy (Ghci3.X GHC.Base.String a_a1Ei) :: TYPE GHC.Types.LiftedRep)
            -> GHC.Types.Int)
          @((Data.Proxy.Proxy (Ghci3.X GHC.Base.String a_a1Ei) :: TYPE GHC.Types.LiftedRep)
            -> GHC.Types.Int)
          Ghci1.c ::
          (Data.Proxy.Proxy (Ghci3.X GHC.Base.String a_a1Ei) :: TYPE GHC.Types.LiftedRep)
          -> GHC.Types.Int

which identifies the issue: GHC is not coercing away the newtype, but deriving an identity coercion.

Apologies again if I'm missing something obvious here.

Ah, I misinterpreted your comment—I thought that you were implying that the code was infinitely looping at compile-time, not runtime. My apologies.

The code that deriving newtype instance C a b => C (X String a) (X String b) generates is expected behavior, as it turns out. From the users' guide section on StandaloneDeriving:

The stand-alone syntax is generalised for newtypes in exactly the same way that ordinary deriving clauses are generalised [...]. For example:
newtype Foo a = MkFoo (State Int a)

deriving instance MonadState Int Foo
GHC always treats the //last// parameter of the instance (Foo in this example) as the type whose instance is being derived.

In other words, the generated code will coerce underneath the last type argument, and nothing more. In your example, you have:

class C a b | a -> b, b -> a where
  c :: Proxy a -> Int

newtype X a b = X b
deriving newtype instance C a b => C (X String a) (X String b)

This will coerce from X String b to b, and nothing more. Because the type of c happens to never mention the last type parameter of C, this results in the "identity coercion" behavior you see with -ddump-deriv.

It's a bit strange, but there's a certain consistency to it. After all, deriving newtype instance C a b => C (X String a) (X String b) could mean three different things:

Coerce underneath X String a only.
Coerce underneath X String b only.
Coerce underneath X String a and X String b.

In general, if a multi-parameter type class has //n// type parameters, then there are 2^//n//^ - 1 different potential choices of code to generate. Since deriving clauses only coerce underneath the last type parameter, StandaloneDeriving picks the same convention.

I understand that only the last argument is coerced, but even so, that would require an instance for C (X String a) b, which in this specific case instantiates to C (X String Int) Int, and the functional dependency should (I think) force this to fail via X String Int ~ Int. No?

To be clear, I now understand why this code should fail to compile, because the instance precondition should be C (X String a) b, and not C a b. But I still think it shouldn't loop at runtime.

Replying to [ticket:16322#comment:168726 paf31]:

I understand that only the last argument is coerced, but even so, that would require an instance for C (X String a) b, which in this specific case instantiates to C (X String Int) Int, and the functional dependency should (I think) force this to fail via X String Int ~ Int. No?

If you had written instance C (X String a) b => C (X String a) (X String b), then that would be the case. But you didn't—you specifically wrote instance C a b => C (X String a) (X String b), which has no functional dependency issues.

But I still think it shouldn't loop at runtime.

For the same reasons I explained in ticket:16322#comment:168724, the code that gets generated is c = coerce c, where the two occurrences of c have the same type, i.e., an infinite loop.

I understand that GHC is inserting an identity coercion which leads to a loop, but what I don't understand is why it thinks that instance is a valid choice to defer to in the first place. If it's deferring to C (X String a) (X String b), then no newtype was ever unwrapped.

I'll break down my understanding step-by-step based on what you've said above, and please let me know where I go wrong:

I require C (X String a) (X String b) given C a b
deriving newtype uses the newtype only in the last type argument, so GHC reduces this to looking for an instance of C (X String a) b.
The only instances that could ever possibly be applicable (even just based on the class) are C Int Int, C a b (in scope locally) and C (X String a) (X String b) itself (the recursive instance which is apparently chosen) but each leads to a contradiction (note that the functional dependency means I can infer the first type argument from the second):

C Int Int fails via Int ~ X String a.
C a b forces X String a ~ a
C (X String a) (X String b) forces X String b ~ b.

Step 2 isn't quite accurate. In general, saying "GHC reduces to looking for an instance of ..." is a decent intuition for how GeneralizedNewtypeDeriving works, but it breaks down in the particular case of C. Given the standalone deriving declaration you've written, GHC will first generate this code:

instance C a b => C (X String a) (X String b) where
  c :: Proxy (X String a) -> Int
  c = coerce @(Proxy (X String a) -> Int) @(Proxy (X String a) -> Int) c

At this point, GHC will typecheck this code. GHC has no issues with this code—the only class constraint that needs to be satisfies in order to typecheck is C (X String a) (X String b), but since that's exactly the instance we're defining, this works. Moreover, that's why c loops at runtime, since we're recursively invoking c from the same instance without end. (Note that the C a b => constraint is never really used at runtime—the only purpose it serves is to satisfy the functional dependency coverage condition.)

All of this weirdness is ultimately due to the fact that the type of c never mentions b anywhere. If c's type were Proxy b -> Int, then the generated code would instead be:

instance C a b => C (X String a) (X String b) where
  c :: Proxy (X String b) -> Int
  c = coerce @(Proxy b -> Int) @(Proxy (X String b) -> Int) c

In order to typecheck this, GHC would need actually need to satisfy a C a b constraint. In that scenario, it would be fair to summarize the whole thing as "reducing to looking for an instance of C a b". But in the program you've presented, you have an atypical corner case where the method's type does not mention the last type parameter of the class, so the usual intuition doesn't apply.

I see, thank you. My understanding of GeneralizedNewtypeDeriving in the presence of MPTCs was faulty then.

If it makes you feel any better, the code you were trying to write will be rejected with an error message in GHC 8.8 due to a slight tweak in the code generation strategy for GeneralizedNewtypeDeriving (notice the extra visible type applications):

λ> deriving instance C a b => C (X String a) (X String b)

==================== Derived instances ====================
Derived class instances:
  instance Ghci1.C a b =>
           Ghci1.C
             (Ghci2.X GHC.Base.String a) (Ghci2.X GHC.Base.String b) where
    Ghci1.c
      = GHC.Prim.coerce
          @(Data.Proxy.Proxy (Ghci2.X GHC.Base.String a_a1I3)
            -> GHC.Types.Int)
          @(Data.Proxy.Proxy (Ghci2.X GHC.Base.String a_a1I3)
            -> GHC.Types.Int)
          (Ghci1.c @(Ghci2.X GHC.Base.String a_a1I3) @b_a1I4) ::
          Data.Proxy.Proxy (Ghci2.X GHC.Base.String a_a1I3) -> GHC.Types.Int
  

Derived type family instances:



<interactive>:13:1: error:
    • Occurs check: cannot construct the infinite type: b ~ X String b
        arising from a functional dependency between constraints:
          ‘C a b’ arising from a use of ‘c’ at <interactive>:13:1-54
          ‘C a b1’
            arising from the instance declaration at <interactive>:13:1-54
    • In the third argument of ‘GHC.Prim.coerce’, namely
        ‘(c @(X String a) @b)’
      In the expression:
          GHC.Prim.coerce
            @(Proxy (X String a) -> Int)
            @(Proxy (X String a) -> Int)
            (c @(X String a) @b) ::
            Proxy (X String a) -> Int
      In an equation for ‘c’:
          c = GHC.Prim.coerce
                @(Proxy (X String a) -> Int)
                @(Proxy (X String a) -> Int)
                (c @(X String a) @b) ::
                Proxy (X String a) -> Int
      When typechecking the code for ‘c’
        in a derived instance for ‘C (X String a) (X String b)’:
        To see the code I am typechecking, use -ddump-deriv

<interactive>:13:1: error:
    • Occurs check: cannot construct the infinite type: a ~ X String a
        arising from a functional dependency between constraints:
          ‘C (X String a) b1’
            arising from a use of ‘c’ at <interactive>:13:1-54
          ‘C a b1’
            arising from the instance declaration at <interactive>:13:1-54
    • In the third argument of ‘GHC.Prim.coerce’, namely
        ‘(c @(X String a) @b)’
      In the expression:
          GHC.Prim.coerce
            @(Proxy (X String a) -> Int)
            @(Proxy (X String a) -> Int)
            (c @(X String a) @b) ::
            Proxy (X String a) -> Int
      In an equation for ‘c’:
          c = GHC.Prim.coerce
                @(Proxy (X String a) -> Int)
                @(Proxy (X String a) -> Int)
                (c @(X String a) @b) ::
                Proxy (X String a) -> Int
      When typechecking the code for ‘c’
        in a derived instance for ‘C (X String a) (X String b)’:
        To see the code I am typechecking, use -ddump-deriv
    • Relevant bindings include
        c :: Proxy (X String a) -> Int (bound at <interactive>:13:1)

If this discussion answers your question, can this issue be closed?

Perfect! Yes, please do close this.

closed

Trac metadata

Trac field	Value
Resolution	Unresolved → ResolvedInvalid

added Pnormal label

"deriving newtype instance" generates an infinite loop

Child items 0

Activity