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

1 Feb 2016

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

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

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

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

--
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11523
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler