Opened 3 years ago

Last modified 8 months ago

#11523 new bug

Infinite Loop when mixing UndecidableSuperClasses and the class/instance constraint synonym trick.

Reported by: ekmett Owned by: simonpj
Priority: high Milestone: 8.4.1
Component: Compiler (Type checker) Version: 8.0.1-rc1
Keywords: UndecidableSuperClasses Cc: simonpj, Iceland_jack, aaronvargo
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC rejects valid program Test Case: polykinds/T11523
Blocked By: Blocking:
Related Tickets: #11480 Differential Rev(s):
Wiki Page:

Description

There seems to be a bad interaction between UndecidableSuperClasses and the common trick of using a cyclic definition of a class and instance to make an alias at the constraint level:

class (Foo f, Bar f) => Baz f
instance (Foo f, Bar f) => Baz f

Unfortunately, there are circumstances in which you can't eliminate it, such as

class (p, q) => p & q
instance (p, q) => p & q

There we can't partially apply (,) at the constraint level, but we can talk about (&) :: Constraint -> Constraint -> Constraint and (&) (Eq a) :: Constraint -> Constraint.

This doesn't seem to happen on simpler examples like the above, but once I modify the categories example from #11480 to move the domain and codomain of a functor into class associated types, so that they don't infect every single subclass of functor, we run into a problem. The following stripped down version of the code seems to send the compiler into an infinite loop:

{-# language KindSignatures #-}
{-# language PolyKinds #-}
{-# language DataKinds #-}
{-# language TypeFamilies #-}
{-# language RankNTypes #-}
{-# language NoImplicitPrelude #-}
{-# language FlexibleContexts #-}
{-# language MultiParamTypeClasses #-}
{-# language GADTs #-}
{-# language ConstraintKinds #-}
{-# language FlexibleInstances #-}
{-# language TypeOperators #-}
{-# language ScopedTypeVariables #-}
{-# language DefaultSignatures #-}
{-# language FunctionalDependencies #-}
{-# language UndecidableSuperClasses #-}
{-# language UndecidableInstances #-}
{-# language TypeInType #-}

import GHC.Types (Constraint, Type)
import qualified Prelude

type Cat i = i -> i -> Type

newtype Y (p :: i -> j -> Type) (a :: j) (b :: i) = Y { getY :: p b a }

class Vacuous (a :: i)
instance Vacuous a

class (Functor p, Dom p ~ Op p, Cod p ~ Nat p (->)) => Category (p :: Cat i) where
  type Op p :: Cat i
  type Op p = Y p
  type Ob p :: i -> Constraint
  type Ob p = Vacuous

class (Category (Dom f), Category (Cod f)) => Functor (f :: i -> j) where
  type Dom f :: Cat i
  type Cod f :: Cat j

class    (Functor f, Dom f ~ p, Cod f ~ q) => Fun (p :: Cat i) (q :: Cat j) (f :: i -> j) | f -> p q
instance (Functor f, Dom f ~ p, Cod f ~ q) => Fun (p :: Cat i) (q :: Cat j) (f :: i -> j)

data Nat (p :: Cat i) (q :: Cat j) (f :: i -> j) (g :: i -> j)

instance (Category p, Category q) => Category (Nat p q) where
  type Ob (Nat p q) = Fun p q

instance (Category p, Category q) => Functor (Nat p q) where
  type Dom (Nat p q) = Y (Nat p q)
  type Cod (Nat p q) = Nat (Nat p q) (->)

instance (Category p, Category q) => Functor (Nat p q f) where
  type Dom (Nat p q f) = Nat p q
  type Cod (Nat p q f) = (->)

instance Category (->) 

instance Functor ((->) e) where
  type Dom ((->) e) = (->)
  type Cod ((->) e) = (->)

instance Functor (->) where
  type Dom (->) = Y (->)
  type Cod (->) = Nat (->) (->)

instance (Category p, Op p ~ Y p) => Category (Y p) where
  type Op (Y p) = p

instance (Category p, Op p ~ Y p) => Functor (Y p a) where
  type Dom (Y p a) = Y p
  type Cod (Y p a) = (->)

instance (Category p, Op p ~ Y p) => Functor (Y p) where
  type Dom (Y p) = p
  type Cod (Y p) = Nat (Y p) (->)

Here I need the circular definition of Fun to talk about the fact that the objects in the category of natural transformations from a category p to a category q are functors with domain p and codomain q, so to give the definition of the class-associated type Ob (Nat p q) I need such a cyclic definition.

I can't leave the domain and codomain of Functor in fundeps, otherwise if I go to define a subclass of Functor I'd have to include the arguments, and I have a lot of those subclasses!

Attachments (1)

Categories.hs (7.0 KB) - added by ekmett 3 years ago.
a test case that is still failing after february 8th patches

Download all attachments as: .zip

Change History (33)

comment:1 Changed 3 years ago by ekmett

(It apparently isn't infinite, the compiler eventually runs out of memory and crashes.)

comment:2 Changed 3 years ago by simonpj

I have a fix for this. Patch coming.

comment:3 Changed 3 years ago by ekmett

Version: 7.10.38.0.1-rc1

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

In 8871737/ghc:

Document and improve superclass expansion

When investigating Trac #11523 I found that superclass
expansion was a little over-aggressive; we were sort of
unrolling each loop twice.

This patch corrects that, and adds explanatory comments.

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

In 43e02d12/ghc:

Fix a nasty superclass expansion bug

This patch fixes Trac #11523.

* The basic problem was that TcRnTypes.superClassesMightHelp was
  returning True of a Derived constraint, and that led to us
  expanding Given superclasses, which produced the same Derived
  constraint again, and so on infinitely.  We really want to do
  this only if there are unsolve /Wanted/ contraints!

* On the way I made TcSMonad.getUnsolvedInerts a bit more
  discriminating about which Derived equalities it returns;
  see Note [Unsolved Derived equalities] in TcSMonad

* Lots of new comments in TcSMonad.

comment:6 Changed 3 years ago by simonpj

Status: newmerge
Test Case: polykinds/T11523

I believe I've fixed this. I'm sorry I missed the RC2 bus.

Simon

comment:7 Changed 3 years ago by ekmett

Thanks! I'll give it a shot.

Changed 3 years ago by ekmett

Attachment: Categories.hs added

a test case that is still failing after february 8th patches

comment:8 Changed 3 years ago by ekmett

Attempting to compile the attachment I just submitted now crashes ghc HEAD with the following rather uninformative error message:

*** Exception: No match in record selector ctev_dest

I haven't cut down the example, yet, however.

comment:9 Changed 3 years ago by simonpj

Ah, that's #11401, which Richard hasn't got to yet. So, progress of a sort.

comment:10 Changed 3 years ago by Iceland_jack

Cc: Iceland_jack added

comment:11 Changed 3 years ago by bgamari

Resolution: fixed
Status: mergeclosed

comment:12 Changed 3 years ago by ekmett

Resolution: fixed
Status: closednew

The example I attached after the february 8th patch still doesn't compile.

The ctev_dest crash was masking a completely different blowup.

That said, it may not be for this issue, but for something else.

comment:13 Changed 3 years ago by ekmett

Adding p ~ Op (Op p)) to the superclass constraints of Category in Categories.hs drastically reduces the size of the unresolved wanteds, but they never seem to go away.

comment:14 Changed 3 years ago by simonpj

The undecideable superclasses thing has the following property:

  • If you have a type error (a wanted that genuinely cannot be solved)
  • and you have an infinite number of superclasses

then the typechecker will take a long time and then complain about too many iterations. (This is not great, but I don't know how to do better, and it's a hard problem.) Which is exactly what happens

T11523b.hs:1:1: error:
    solveWanteds: too many iterations (limit = 4)
      Unsolved: WC {wc_simple =
                      [D] _ :: Functor p_a1EY (CDictCan)
                      [D] _ :: Functor (Nat p_a1EY (->)) (CDictCan)
                      [D] _ :: Functor (Y (Nat p_a1EY (->))) (CDictCan)
                      [D] _ :: Functor (Nat (Nat p_a1EY (->)) (->)) (CDictCan)
... blah

In this case, do you think that there is a finite tower of superclasses? I get

[G] Category p
+-> {add superclasses}
        Functor p
        Dom p ~ Op p
        Cod p ~ Nat p (->)
        Ob (Op p) ~ Ob p

+-> {add superclasse of Functor}
        Category (Dom p)
        Cateogory (Cod p)

and now we merrily go round. Adding p ~ Op (Op p) will help, because Dom p ~ Op p. But we are still going to get Cateogry (Cod p), Category (Cod (Cod p)) and so on. Is that really what you intend?

Last edited 3 years ago by simonpj (previous) (diff)

comment:15 Changed 3 years ago by simonpj

Edward, we are stalled on this ticket, pending input from you.

comment:16 Changed 3 years ago by Iceland_jack

Brought up on #ghc, are there technical reasons why (,) cannot be partially applied with the same meaning as (&)?

comment:17 in reply to:  16 ; Changed 3 years ago by simonpj

Replying to Iceland_jack:

Brought up on #ghc, are there technical reasons why (,) cannot be partially applied with the same meaning as (&)?

I'm lost. What is (&)? How is this connected with this ticket?

comment:18 in reply to:  17 Changed 3 years ago by Iceland_jack

Replying to simonpj:

Replying to Iceland_jack:

Brought up on #ghc, are there technical reasons why (,) cannot be partially applied with the same meaning as (&)?

I'm lost. What is (&)? How is this connected with this ticket?

(&) :: Constraint -> Constraint -> Constraint is defined by

class    (p, q) => p & q
instance (p, q) => p & q

at the beginning of this ticket. This would actually be solved by #11715 (per your comment ticket:11715#comment:14)

  • Allow partial applications like (,) (Eq a) :: Constraint -> Constraint

comment:19 Changed 3 years ago by ekmett

I would have thought that if we're not hitting a fixed point in the attached example, we'd have a similar breakage in the example in the description, because we'd see the same tower of Nat's there, but that stripped down version compiles just fine.

Is this something that only comes up when I use constraints like this somehow?

comment:20 Changed 3 years ago by simonpj

comment:14 explains why there is no fixed point. Did the explanation make sense? Do you think there is a fixed point? The existence or otherwise of a fixpoint should not be related to how you use constraints.

Simon

comment:21 Changed 3 years ago by simonpj

Milestone: 8.0.18.2.1
Priority: highesthigh

I'm going to move this off the 8.0 milestone. I claim it's behaving as advertised, and no one is disputing that claim.

By all means bring it back if you disagree.

Simon

comment:22 Changed 3 years ago by ekmett

I've yet to figure out why the shorter example passes, but the longer, which doesn't seem to change the part that spins forever fails.

No objection to moving this out to 8.2 though.

comment:23 Changed 3 years ago by simonpj

I've yet to figure out why the shorter example passes, but the longer, which doesn't seem to change the part that spins forever fails.

I explain precisely this in comment:14 above. You (implicitly) claim that there is a finite number of superclasses. I claim the contrary. We can't both be right :-).

Maybe there's a bug in the example Categories.h? That's my current belief.

comment:24 Changed 3 years ago by simonpj

See #12131 for another version of this.

comment:25 Changed 2 years ago by bgamari

Owner: set to simonpj

comment:26 Changed 2 years ago by simonpj

Edward says "I can't check particulars right now. I can definitely say I'd like some way to attain an equivalent result, but I accept that it may not be possible with the machinery we have."

comment:27 Changed 2 years ago by bgamari

Milestone: 8.2.18.4.1

Regardless, this certainly won't be addressed for 8.2.

comment:28 in reply to:  14 Changed 8 months ago by aaronvargo

Replying to simonpj:

In this case, do you think that there is a finite tower of superclasses? I get

[G] Category p
+-> {add superclasses}
        Functor p
        Dom p ~ Op p
        Cod p ~ Nat p (->)
        Ob (Op p) ~ Ob p

+-> {add superclasse of Functor}
        Category (Dom p)
        Cateogory (Cod p)

and now we merrily go round. Adding p ~ Op (Op p) will help, because Dom p ~ Op p. But we are still going to get Cateogry (Cod p), Category (Cod (Cod p)) and so on. Is that really what you intend?

What if you take instances into account in considering when to terminate? Then the tower is finite, since Category (Cod p) is a consequence of:

Category p
Cod p ~ Nat p (->)
instance (Category p, Category q) => Category (Nat p q)
instance Category (->)

and so the fact that Category (Cod p) is a superclass provides no new information, and thus there's no need to go any further.

This also suggests a slightly ugly work-around, which indeed seems to work (at least in this case):

-- Functor without Category (Cod f)
class Category (Dom f) => Functor' (f :: i -> j)

-- Functor with Category (Cod f)
class (Functor' f, Category (Cod f)) => Functor f
instance (Functor' f, Category (Cod f)) => Functor f

-- only require Functor', since Category (Cod p) is already implied
class ( Functor' p
      , Dom p ~ Op p
      , Cod p ~ Nat p (->)
      , Ob (Op p) ~ Ob p
      , Op (Op p) ~ p
      ) => Category (p :: Cat i)

Tangentially, there's also really no need for Op p, since it's just equal to Dom p, and so Category can be simplified to:

class ( Functor' p
      , Cod p ~ Nat p (->)
      , Dom (Dom p) ~ p
      , Ob (Dom p) ~ Ob p
      ) => Category (p :: Cat i)

comment:29 Changed 8 months ago by simonpj

What if you take instances into account in considering when to terminate?

That's a very interesting point.

Currently, for each new "Given" (of which the potential superclasses are an example), GHC

  1. Rewrites it with currently available Given equalities, a kind of normalisation step
  2. And then sees if it is syntactically equal to one of the existing Givens.

You are suggesting changing Step 2 to

  1. See if it is completely provable from the existing Givens and top-level instances

That is an intriguing thought. I say "completely" provable from because suppose you had

   instance (C a, D a) => D (T a)
   [G] C a

and you were about to add [G] D (T a). The instance declaration applies, yielding sub-goals (C a, D a). We have (C a), but not D a. So I think we then must abandon the attempt -- even if only one out of hundreds of sub-goals fails -- and add the proposed new Given after all.

I worry a bit about solve order. In the original example, suppose we added [G] Category (Cod p) before we added Category p. If we were going to be solidly robust to solve order, whenever we added a new Given we'd have to check all the existing Givens to see if any of them could be proved from the new one (and the others).

But perhaps we could apply this magic only to the superclass expansion step; for "normal" Givens it's at most an optimisation.

Interesting! I wonder if there are any other compelling examples. Edward??

comment:30 Changed 8 months ago by aaronvargo

Are QuantifiedConstraints another thing to consider here? The proposed magic would properly account for them as well, while the current rules presumably ignore them the same way they ignore top-level instances.

comment:31 Changed 8 months ago by simonpj

I guess so. Can you offer an example?

So far we we have precisely one example needing the magic... more examples would strengthen the case for making a change.

comment:32 Changed 8 months ago by aaronvargo

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