id,summary,reporter,owner,description,type,status,priority,milestone,component,version,resolution,keywords,cc,os,architecture,failure,testcase,blockedby,blocking,related,differential,wikipage
11523,Infinite Loop when mixing UndecidableSuperClasses and the class/instance constraint synonym trick.,ekmett,simonpj,"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!",bug,new,high,8.4.1,Compiler (Type checker),8.0.1-rc1,,UndecidableSuperClasses,simonpj Iceland_jack aaronvargo,Unknown/Multiple,Unknown/Multiple,GHC rejects valid program,polykinds/T11523,,,#11480,,