Skip to content

GitLab

  • Menu
Projects Groups Snippets
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
  • Sign in / Register
  • GHC GHC
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
    • Locked Files
  • Issues 4,968
    • Issues 4,968
    • List
    • Boards
    • Service Desk
    • Milestones
    • Iterations
  • Merge requests 474
    • Merge requests 474
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Schedules
    • Test Cases
  • Deployments
    • Deployments
    • Releases
  • Analytics
    • Analytics
    • Value stream
    • CI/CD
    • Code review
    • Insights
    • Issue
    • Repository
  • Wiki
    • Wiki
  • Snippets
    • Snippets
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Glasgow Haskell Compiler
  • GHCGHC
  • Issues
  • #11523
Closed
Open
Created Feb 01, 2016 by Edward Kmett@ekmett

Infinite Loop when mixing UndecidableSuperClasses and the class/instance constraint synonym trick.

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
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking