Skip to content

Typechecking regression

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.
Trac metadata
Trac field Value
Version 7.0.1
Type Bug
TypeOfFailure OtherFailure
Priority highest
Resolution Unresolved
Component Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information