[GHC] #11523: Infinite Loop when mixing UndecidableSuperClasses and the class/instance constraint synonym trick.

[GHC]

#11523: Infinite Loop when mixing UndecidableSuperClasses and the class/instance
constraint synonym trick.
-------------------------------------+-------------------------------------
        Reporter:  ekmett            |                Owner:  simonpj
            Type:  bug               |               Status:  new
        Priority:  high              |            Milestone:  8.4.1
       Component:  Compiler (Type    |              Version:  8.0.1-rc1
  checker)                           |             Keywords:
      Resolution:                    |  UndecidableSuperClasses
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  GHC rejects       |            Test Case:
  valid program                      |  polykinds/T11523
      Blocked By:                    |             Blocking:
 Related Tickets:  #11480            |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by aaronvargo):

 Replying to [comment:14 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:

 {{{#!hs
 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):

 {{{#!hs
 -- 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:

 {{{#!hs
 class ( Functor' p
       , Cod p ~ Nat p (->)
       , Dom (Dom p) ~ p
       , Ob (Dom p) ~ Ob p
       ) => Category (p :: Cat i)
 }}}

-- 
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11523#comment:28>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler