GitLab

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 (closed) 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!

Trac metadata

Trac field	Value
Version	7.10.3
Type	Bug
TypeOfFailure	OtherFailure
Priority	highest
Resolution	Unresolved
Component	Compiler (Type checker)
Test case
Differential revisions
BlockedBy
Related
Blocking
CC	simonpj
Operating system
Architecture