[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

GHC

GHC

GHC

GHC

GHC

GHC

GHC

GHC

GHC

GHC

GHC

GHC

GHC

GHC

GHC

GHC

GHC

GHC

GHC

GHC

GHC

GHC

GHC

GHC

GHC

GHC

GHC

GHC

GHC

GHC

GHC

GHC

GHC

GHC

tags

participants (1)