Opened 3 years ago

Last modified 17 months ago

#12860 new bug

GeneralizedNewtypeDeriving + MultiParamTypeClasses sends typechecker into an infinite loop

Reported by: RyanGlScott Owned by:
Priority: normal Milestone:
Component: Compiler (Type checker) Version: 8.0.1
Keywords: FunDeps, deriving Cc: diatchki, dfeuer
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: Compile-time performance bug Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

This worked in GHC 7.6.3, but ever since GHC 7.8, this code will cause the typechecker to loop infinitely:

{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE MultiParamTypeClasses #-}
module Bug where

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

newtype Foo a = Foo a
  deriving (C b)

Change History (24)

comment:1 Changed 3 years ago by rwbarton

Well before 8.0, it results in a context reduction stack overflow reasonably quickly.

The code is extremely dubious anyways, since the derived instance would have form

instance C b a => C b (Foo a) where ...

But if you could actually satisfy the context C b a, then you would be disallowed from writing the instance C b (Foo a) by the functional dependency. So the derived instance should be useless.

comment:2 Changed 3 years ago by simonpj

Yikes that is really bad. At least we should get a context-stack overflow.

But there is more, as I found when investigating:

  • At the moment if we have
    inert:     [D] a ~ ty
    work item  [D] a ~ ty
    
    we rewrite the work item with the inert to get [D] ty ~ ty and then take a series steps to decompose it. It'd be fast to use unifyDerived for this case.
  • The reason we generate two duplicate Derived constraints is also a bit stupid. Suppose we have [W] C T a, where class C has some fundeps, and a is a skolem of some kind. From this we might generate a derived [D] a ~ ty. This kicks out a derived shadow [D] C T a from the inerts. We rewrite it to [D] C T ty. But then we interact it with the [W] C T a in the inert set, to make another derived [D] a ~ ty. What a waste of effort.

But underlying all this is the question of what should happen here. The problem is:

[W] C a b
--> [D] b ~ Foo beta1    (by fundeps, beta1 fresh unification variable)
--> [D] C a (Foo beta1)  (rewrite)
--> [D] C a beta1        (use instance C a b => C a (Foo b))

and now the cycle repeats. With a hand-written instance decl

instance C a b => C a (Foo b)

you rightly need UndecidableInstances, but it's less clear what to do when trying to guess the instance context; fail in some way I guess.

comment:3 Changed 3 years ago by RyanGlScott

If I understand correctly, GHC sometimes rejects deriving clauses if the inferred context is considered too "exotic", right? Is there a nice way to teach GHC that this case should be marked as exotic?

comment:4 Changed 3 years ago by Simon Peyton Jones <simonpj@…>

In eb55ec2/ghc:

Refactor functional dependencies a bit

* Rename CoAxiom.Eqn = Pair Type to TypeEqn,
  and use it for fundeps

* Use the FunDepEqn for injectivity, which lets us share a bit
  more code, and (more important) brain cells

* When generating fundeps, take the max depth of the two
  constraints.  This aimed at tackling the strange loop in
  Trac #12860, but there is more to come for that.

* Improve pretty-printing with -ddump-tc-trace

comment:5 Changed 3 years ago by Simon Peyton Jones <simonpj@…>

In f8c966c/ghc:

Be a bit more selective about improvement

This patch makes [W] constraints not participate in
improvement.   See Note [Do not do improvement for WOnly]
in TcSMonad.

Removes some senseless work duplication in some cases (notably
Trac #12860); should not change behaviour.

comment:6 Changed 3 years ago by simonpj

Well my efforts thus far have at least succeeded in getting an error message very promptly

T12860.hs:12:13: error:
    • Reduction stack overflow; size = 201
      When simplifying the following type: C y (Foo x)
      Use -freduction-depth=0 to disable this check
      (any upper bound you could choose might fail unpredictably with
       minor updates to GHC, so disabling the check is recommended if
       you're sure that type checking should terminate)
    • When deriving the instance for (C y (Foo x))

comment:7 Changed 3 years ago by simonpj

Maybe it'd be better to somehow get the "context too exotic" message, but that might be no more illuminating than the one above. And it's a bit of a corner case.

So I'm moving this off my stack for now anyway.

Simon

comment:8 Changed 2 years ago by simonpj

Keywords: FunDeps added

comment:9 Changed 2 years ago by RyanGlScott

Keywords: deriving added

comment:10 Changed 2 years ago by dfeuer

Based on rwbarton's comment:1, it seems that GND should probably reject deriving any class whose last parameter is determined by a fundep. Is there something wrong with such a rule?

comment:11 Changed 2 years ago by RyanGlScott

The problem isn't limited to just derived instances. If you try to write out the code that would be derived by hand:

{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE UndecidableInstances #-}
module Bug where

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

newtype Foo a = Foo a

instance C b a => C b (Foo a) where
  c (Foo a) = c a

Then GHC will also "loop" (i.e., it will stack overflow on GHC 8.0.2 or later, and properly loop on GHC 8.0.1):

    • Reduction stack overflow; size = 201
      When simplifying the following type: C a0 (Foo a)
      Use -freduction-depth=0 to disable this check
      (any upper bound you could choose might fail unpredictably with
       minor updates to GHC, so disabling the check is recommended if
       you're sure that type checking should terminate)
    • In the expression: c a
      In an equation for ‘c’: c (Foo a) = c a
      In the instance declaration for ‘C b (Foo a)’
   |
14 |   c (Foo a) = c a
   |               ^^^

So if anything, we should be placing an extra check in the constraint solver, not just GND.

comment:12 Changed 18 months ago by RyanGlScott

Well, maybe. The original program and the program in comment:11 have another key difference. The latter uses UndecidableInstances, so I suppose it's entirely reasonable that we get a stack overflow error on that one. The former program, on the other hand, does not use UndecidableInstances.

Really, we ought to reject the former program outright with an error message similar to the one that we get if we leave off UndecidableInstances from the latter program:

{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE MultiParamTypeClasses #-}
module Bug where

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

newtype Foo a = Foo a

instance C b a => C b (Foo a) where
  c (Foo a) = c a
Bug.hs:12:10: error:
    • Illegal instance declaration for ‘C b (Foo a)’
        The coverage condition fails in class ‘C’
          for functional dependency: ‘a -> b’
        Reason: lhs type ‘b’ does not determine rhs type ‘Foo a’
        Un-determined variable: a
        Using UndecidableInstances might help
    • In the instance declaration for ‘C b (Foo a)’
   |
12 | instance C b a => C b (Foo a) where
   |          ^^^^^^^^^^^^^^^^^^^^

If we did this, then I would consider this issue resolved.

This coverage condition check is performed in checkValidInstance. Curiously, we don't call checkValidInstance on derived instances at the comment. There are relevant comments here:

                -- checkValidInstance tyvars theta clas inst_tys
                -- Not necessary; see Note [Exotic derived instance contexts]

           ; traceTc "TcDeriv" (ppr deriv_rhs $$ ppr theta)
                -- Claim: the result instance declaration is guaranteed valid
                -- Hence no need to call:
                --   checkValidInstance tyvars theta clas inst_tys

As this ticket shows, this isn't quite right. So perhaps we need to carve out the bit that checks the coverage condition and just check that.

comment:13 Changed 17 months ago by simonpj

So perhaps we need to carve out the bit that checks the coverage condition and just check that.

Or just call checkValidInstance with a Note explaining why you might think it's not necessary (the exotic-derived Note), and the example from this ticket explaining why it actually is.

comment:14 Changed 17 months ago by RyanGlScott

Another thing I'm unclear on is: should we be calling checkValidInstance after every iteration of simplifyDeriv? Or should we only do it once, after the final inferred context has been found?

comment:15 Changed 17 months ago by simonpj

Just at the end I think.

comment:16 Changed 17 months ago by RyanGlScott

Hm. I tried to use checkValidInstance, but there's a big problem: its type signature is not very amenable to being put into simplifyInstanceContexts. It is currently:

checkValidInstance :: UserTypeCtxt -> LHsSigType GhcRn -> Type
                   -> TcM ([TyVar], ThetaType, Class, [Type])

There are two awkward things about this:

  1. It expects an LHsSigType GhcRn argument, but this isn't available in simplifyInstanceContexts. (However, checkValidInstance only uses this to get a SrcSpan, so perhaps this can be changed to just be a SrcSpan argument.)
  2. A more awkward sticking point is that checkValidInstance expects a Type as an argument. This is because it then proceeds to split it with tcSplitSigmaTy (and returns the resulting tyvars and theta). However, in simplifyInstanceContexts, our instance type is already "pre-split" (that is, we already have the tyvars, theta, class, and class argument types lying around).

What's worse, I can't just change the Type argument and replace it with the constituent [TyVar], ThetaType, etc., since checkValidInstance passes that Type wholesale to checkAmbiguity. So I don't know what to do here.

comment:17 Changed 17 months ago by simonpj

Its a bit crude, but you could readily make the type to pass to checkValidInstance by saying mkSigmaTy tyvars theta the_pred.

comment:18 Changed 17 months ago by RyanGlScott

I've hit another snag, related to comment:15. I tried putting the call to checkValidInstance after simplifyDeriv has finished iterating, but that doesn't work for the original program in this ticket. Why? Because during the second iteration of simplifyDeriv, we pass the context C b a (the result of the first iteration of simplifyDeriv) to solveWantedsAndDrop. But that leads to the infinite loop described in comment:2, so it's already too late by that point.

Naturally, I thought to instead try calling checkValidInstance after every iteration of simplifyDeriv. This does fix the original program, but it causes the test case T4809 to fail instead. The reason is because of this derived instance:

newtype XMLGenT m a = XMLGenT (m a)
  deriving (MonadRWS r w s)

After the first iteration of simplifyDeriv, it produces the context Monoid w. We then pass the following instance to checkValidInstance:

instance Monoid w => MonadRWS r w s (XMLGenT m)

But this doesn't satisfy the coverage condition for MonadRWS's fundeps! (We need m -> r, m -> w, and m -> s.) The final context for this instance, (MonadReader r m, MonadWriter w m, MonadState s m), does satisfy the coverage condition, but we don't get this until after a later iteration of simplifyDeriv.

To sum it up: I can't call checkValidInstance at the end, since an intermediate context might throw the simplifier into a loop, but I can't call checkValidInstance in the middle either, since an intermediate context might not satisfy the coverage condition. I don't know how to proceed from here.

Last edited 17 months ago by RyanGlScott (previous) (diff)

comment:19 Changed 17 months ago by simonpj

Maybe you want dis-aggregate checkValidInstance.

  • I think you need checkInstTermination on every iteration. Probably even if UndecidableInstances is on; I'm not sure that automatic deriving should ever generate a non-provably-terminating instance.
  • Then you can call checkValidInstance itself right at the end -- that will check the coverage conditions.

comment:20 Changed 17 months ago by RyanGlScott

I'm afraid that won't work either. checkInstTermination only checks the Paterson termination conditions, not the fundep coverage conditions (which are checked separately in checkInstCoverage).

Indeed, I just tried calling checkInstTermination after every iteration of simplifyDeriv, but the original program still loops even with that, since C b a passes the Paterson termination conditions.

comment:21 Changed 17 months ago by simonpj

Well I'm not sure what to do.

1 You don't want 'deriving' to loop 2 If the fundep coverage condition isn't satisfied, instance resolution can go into a loop, 3 But comment:18 says that you want 'deriving' to work when fundep coverage doesn't hold.

Perhaps (2) is over-conservative, somehow? Presumably there is something special about (3) that makes it terminate, despite (2) not holding. If you can identify what that is, you can make that into a new (more expressive) fundep coverage condition.

Iavor is the fundep expert.

comment:22 Changed 17 months ago by RyanGlScott

Cc: diatchki added

Indeed, I suspect we need a more permissive check than checkInstCoverage which would reject C b a but not Monoid w in the XMLGenT example. Alas, I have no idea what that check would be.

comment:23 Changed 17 months ago by dfeuer

Ryan mentions

newtype XMLGenT m a = XMLGenT (m a) deriving (MonadRWS r w s)`

I suspect what we want to do is collect the fundeps from the superclass constraints of MonadRWS before doing anything much else. I have the feeling (maybe wrong?) that we can get these more safely than we can fundeps of instance constraints. These should (at least in this case) be sufficient to satisfy the coverage condition.

comment:24 Changed 17 months ago by dfeuer

Cc: dfeuer added
Note: See TracTickets for help on using tickets.