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 ~> cis 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 |