id	summary	reporter	owner	description	type	status	priority	milestone	component	version	resolution	keywords	cc	os	architecture	failure	difficulty	testcase	blockedby	blocking	related
4950	Typechecking regression	igloo		"Reduced from `data-category-0.3.1.1`, this module:
{{{
{-# LANGUAGE FlexibleContexts, FlexibleInstances, GADTs,
             MultiParamTypeClasses, RankNTypes, ScopedTypeVariables,
             TypeOperators, TypeFamilies, TypeSynonymInstances,
             UndecidableInstances #-}

module Data.Category.Limit (limitUniv') where

import Prelude hiding ((.), Functor, product)

infixl 9 !
infixr 9 %
infixr 9 :%
infixr 8 .

data Diag :: (* -> * -> *) -> (* -> * -> *) -> *

type instance Dom (Diag j (~>)) = (~>)
type instance Cod (Diag j (~>)) = Nat j (~>)
type instance Diag j (~>) :% a = Const j (~>) a

type DiagF f = Diag (Dom f) (Cod f)
type Cone   f n = Nat (Dom f) (Cod f) (ConstF f n) f

coneVertex :: Cone f n -> Obj (Cod f) n
coneVertex = undefined

type family LimitFam j (~>) f :: *
type Limit f = LimitFam (Dom f) (Cod f) f
type LimitUniversal f = TerminalUniversal f (DiagF f) (Limit f)

limitUniversal :: (Cod f ~ (~>))
               => Cone f (Limit f)
               -> (forall n. Cone f n -> n ~> Limit f)
               -> LimitUniversal f
limitUniversal = undefined

limit :: LimitUniversal f -> Cone f (Limit f)
limit = undefined

class (Category j, Category (~>)) => HasLimits j (~>) where
  limitUniv :: Obj (Nat j (~>)) f -> LimitUniversal f

type family BinaryProduct ((~>) :: * -> * -> *) x y :: *

class Category (~>) => HasBinaryProducts (~>) where
  proj2 :: Obj (~>) x -> Obj (~>) y -> BinaryProduct (~>) x y ~> y

limitUniv' :: forall f n (~>) .
              (Functor f,
               Dom f ~ Discrete (S n),
               Cod f ~ (~>),
               HasLimits (Discrete n) (~>),
               HasBinaryProducts (~>))
           => f -> LimitUniversal f
limitUniv' f = limitUniversal (Nat undefined f (\z -> unCom $ h z)) undefined
    where x = f % Z
          y = coneVertex limNext
          limNext = limit luNext
          luNext = limitUniv (natId (Next f))
          h :: Obj (Discrete (S n)) z
            -> Com (ConstF f (LimitFam (Discrete (S n)) (~>) f)) f z
          h Z     = undefined
          h (S n) = Com $ limNext ! n . proj2 x y

data Z
data S n

data Discrete :: * -> * -> * -> * where
  Z :: Discrete (S n) Z Z
  S :: Discrete n a a -> Discrete (S n) (S a) (S a)

instance Category (Discrete Z) where
  src = undefined
  tgt = undefined
  (.) = undefined

instance Category (Discrete n) => Category (Discrete (S n)) where
  src = undefined
  tgt = undefined
  (.) = undefined

type family PredDiscrete (c :: * -> * -> *) :: * -> * -> *
type instance PredDiscrete (Discrete (S n)) = Discrete n

data Next :: * -> * where
  Next :: (Functor f, Dom f ~ Discrete (S n)) => f -> Next f

type instance Dom (Next f) = PredDiscrete (Dom f)
type instance Cod (Next f) = Cod f
type instance Next f :% a = f :% S a

instance (Functor f, Category (PredDiscrete (Dom f))) => Functor (Next f) where
  Next f % Z     = f % S Z
  Next f % (S a) = f % S (S a)

data Nat :: (* -> * -> *) -> (* -> * -> *) -> * -> * -> * where
  Nat :: (Functor f, Functor g, c ~ Dom f, c ~ Dom g, d ~ Cod f, d ~ Cod g)
    => f -> g -> (forall z. Obj c z -> Component f g z) -> Nat c d f g

type Component f g z = Cod f (f :% z) (g :% z)

newtype Com f g z = Com { unCom :: Component f g z }

(!) :: (Category c, Category d) => Nat c d f g -> c a b -> d (f :% a) (g :% b)
(!) = undefined

natId :: Functor f => f -> Nat (Dom f) (Cod f) f f
natId = undefined

instance (Category c, Category d) => Category (Nat c d) where
  src = undefined
  tgt = undefined
  (.) = undefined

type family Dom ftag :: * -> * -> *
type family Cod ftag :: * -> * -> *

class (Category (Dom ftag), Category (Cod ftag)) => Functor ftag where
  (%)  :: ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)

type family ftag :% a :: *

data Const (c1 :: * -> * -> *) (c2 :: * -> * -> *) x

type instance Dom (Const c1 c2 x) = c1
type instance Cod (Const c1 c2 x) = c2
type instance Const c1 c2 x :% a = x

instance (Category c1, Category c2) => Functor (Const c1 c2 x) where
  (%) = undefined

type ConstF f = Const (Dom f) (Cod f)

data TerminalUniversal x u a

type Obj (~>) a = a ~> a

class Category (~>) where
  src :: a ~> b -> Obj (~>) a
  tgt :: a ~> b -> Obj (~>) b
  (.) :: b ~> c -> a ~> b -> a ~> c
}}}
is accepted by 7.0.1, but with the 7.0 branch:
{{{
[1 of 1] Compiling Data.Category.Limit ( Data/Category/Limit.hs, interpreted )

Data/Category/Limit.hs:64:21:
    Could not deduce (LimitFam (Discrete (S n1)) (Cod f) f
                        ~
                      BinaryProduct
                        (Cod f) (f :% Z) (LimitFam (Discrete n) (Cod f) (Next f)))
    from the context (Functor f,
                      Dom f ~ Discrete (S n),
                      Cod f ~ (~>),
                      HasLimits (Discrete n) (~>),
                      HasBinaryProducts (~>))
      bound by the type signature for
                 limitUniv' :: (Functor f,
                                Dom f ~ Discrete (S n),
                                Cod f ~ (~>),
                                HasLimits (Discrete n) (~>),
                                HasBinaryProducts (~>)) =>
                               f -> LimitUniversal f
      at Data/Category/Limit.hs:(56,1)-(64,49)
    or from (S n ~ S n1, z ~ S a, z ~ S a)
      bound by a pattern with constructor
                 S :: forall n a. Discrete n a a -> Discrete (S n) (S a) (S a),
               in an equation for `h'
      at Data/Category/Limit.hs:64:14-16
    Expected type: ConstF f (LimitFam (Discrete (S n)) (~>) f)
      Actual type: Const
                     (Discrete (S n1))
                     (Cod f)
                     (BinaryProduct
                        (Cod f) (f :% Z) (LimitFam (Discrete n) (Cod f) (Next f)))
    Expected type: Com
                     (ConstF f (LimitFam (Discrete (S n)) (~>) f)) f z
      Actual type: Com
                     (Const
                        (Discrete (S n1))
                        (Cod f)
                        (BinaryProduct
                           (Cod f) (f :% Z) (LimitFam (Discrete n) (Cod f) (Next f))))
                     f
                     z
    In the expression: Com $ limNext ! n . proj2 x y
    In an equation for `h': h (S n) = Com $ limNext ! n . proj2 x y

Data/Category/Limit.hs:64:27:
    Could not deduce (LimitFam (Discrete n1) (Cod f) (Next f)
                        ~
                      LimitFam (Discrete n) (Cod f) (Next f))
    from the context (Functor f,
                      Dom f ~ Discrete (S n),
                      Cod f ~ (~>),
                      HasLimits (Discrete n) (~>),
                      HasBinaryProducts (~>))
      bound by the type signature for
                 limitUniv' :: (Functor f,
                                Dom f ~ Discrete (S n),
                                Cod f ~ (~>),
                                HasLimits (Discrete n) (~>),
                                HasBinaryProducts (~>)) =>
                               f -> LimitUniversal f
      at Data/Category/Limit.hs:(56,1)-(64,49)
    or from (S n ~ S n1, z ~ S a, z ~ S a)
      bound by a pattern with constructor
                 S :: forall n a. Discrete n a a -> Discrete (S n) (S a) (S a),
               in an equation for `h'
      at Data/Category/Limit.hs:64:14-16
    NB: `LimitFam' is a type function, and may not be injective
    Expected type: LimitFam (Discrete n) (Cod f) (Next f)
      Actual type: ConstF (Next f) (Limit (Next f)) :% a
    Expected type: Cod
                     f (LimitFam (Discrete n) (Cod f) (Next f)) (f :% S a)
      Actual type: Cod
                     f (ConstF (Next f) (Limit (Next f)) :% a) (Next f :% a)
    In the first argument of `(.)', namely `limNext ! n'
    In the second argument of `($)', namely `limNext ! n . proj2 x y'
Failed, modules loaded: none.
}}}
"	bug	closed	highest	7.0.2	Compiler (Type checker)	7.0.1	duplicate		sjoerd@…	Unknown/Multiple	Unknown/Multiple	None/Unknown