#4950: Typechecking regression
----------------------------------------+-----------------------------------
Reporter: igloo | Owner:
Type: bug | Status: new
Priority: highest | Milestone: 7.0.2
Component: Compiler (Type checker) | Version: 7.0.1
Keywords: | Testcase:
Blockedby: | Difficulty:
Os: Unknown/Multiple | Blocking:
Architecture: Unknown/Multiple | Failure: None/Unknown
----------------------------------------+-----------------------------------
Comment(by simonpj):
This is a truly mind-boggling file. I have spent over an whole hour
simply typ-checking the program manually. It's jolly hard!
Below is my version of the code, heavily annotated with type signatures.
I've simplified it a bit, but it gives essentially the exact same error
message.
And the message looks right to me:
{{{
Could not deduce (BinaryProduct
(Cod f) (f :% Z) (LimitFam (Discrete n1) (Cod f)
(Next f))
~
LimitFam (Discrete (S n)) (Cod f) f)
}}}
Why should those two these two types be equal? Both `BinaryProduct` and
`LimitFam` are families, but neither have any equations.
'''AAARGH!''' I've just recompiled the original package source with a
version of GHC that has #4935 fixed, and it compiles `Data.Category.Limit`
just fine. So the real bug is in the cut-down version! (Both 7.0.1 and
HEAD break on `Data.Category.Adjunction`, with a skolem-escape error, but
that is a separate regression, which I'll open a separate ticket for.)
So I'm just going to close this ticket.
{{{
{-# LANGUAGE FlexibleContexts, FlexibleInstances, GADTs,
MultiParamTypeClasses, RankNTypes, ScopedTypeVariables,
TypeOperators, TypeFamilies, TypeSynonymInstances,
UndecidableInstances, EmptyDataDecls #-}
module T4950 (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 g => HasBinaryProducts g where
proj2 :: g x x -> g y y -> g (BinaryProduct g x y) y
limitUniv' :: forall f n .
(Functor f,
Dom f ~ Discrete (S n),
HasLimits (Discrete n) (Cod f),
HasBinaryProducts (Cod f))
=> f -> LimitUniversal f
limitUniv' f = limitUniversal (Nat undefined f (\z -> h z)) undefined
where
x :: Cod f (f :% Z) (f :% Z)
x = f % Z
y :: Cod (Next f) (Limit (Next f)) (Limit (Next f))
y = coneVertex limNext
limNext :: Nat (Dom (Next f))
(Cod (Next f))
(Const (Dom (Next f)) (Cod (Next f)) (Limit (Next
f)))
(Next f)
limNext = limit luNext
luNext :: LimitUniversal (Next f)
luNext = limitUniv nid
nid :: Nat (Dom (Next f)) (Cod (Next f)) (Next f) (Next f)
nid = natId nf
nf :: Next f
nf = Next f
-- h :: Discrete (S n) z z
-- -> Component (ConstF f (LimitFam (Discrete (S n)) (~>) f)) f
z
-- h :: Discrete (S n) z z
-- -> Cod (ConstF f (LimitFam (Discrete (S n)) (~>) f))
-- (ConstF f (LimitFam (Discrete (S n)) (~>) f) :% z)
-- (f :% z)
-- h :: Discrete (S n) z z
-- -> Cod (Const (Dom f) (Cod f) (LimitFam (Discrete (S n))
(~>) f))
-- (Const (Dom f) (Cod f) (LimitFam (Discrete (S n))
(~>) f)
-- :% z)
-- (f :% z)
-- h :: Discrete (S n) z z
-- -> Cod f
-- (Const (Dom f) (Cod f) (LimitFam (Discrete (S n))
(Cod f) f)
-- :% z)
-- (f :% z)
h :: Discrete (S n) z z
-> Cod f
(LimitFam (Discrete (S n)) (Cod f) f)
(f :% z)
h (S (n::Discrete n a a)) = undefined . p2
where
p2 :: Cod f (BinaryProduct (Cod f) (f :% Z) (Limit
(Next f)))
(Limit (Next f))
-- NB: needs (Cod f ~ Cod (Next f))
-- But that holds!
p2 = proj2 x y
-- (.) :: forall (~>). Category (~>) => (b ~> c) -> (a ~> b) -> (a ~> c)
-- (~>) instantiated to (Cod f)
-- (.) :: Cod f b c -> Cod f a b -> Cod f a c
-- a := (BinaryProduct (Cod f) (f :% Z) (Limit (Next f)))
-- = (BinaryProduct (Cod f) (f :% Z) (LimitFam (Dom (Next f)) (Cod
(Next f)) (Next f)))
-- = (BinaryProduct (Cod f) (f :% Z) (LimitFam (PredDiscrete (Dom f))
(Cod f) (Next f)))
-- Since Dom f ~ Discrete (S n)
-- = (BinaryProduct (Cod f) (f :% Z) (LimitFam (PredDiscrete (Discrete
(S n))) (Cod f) (Next f)))
-- = (BinaryProduct (Cod f) (f :% Z) (LimitFam (Discrete n) (Cod f)
(Next f)))
-- Result of (.) call: Need a ~ (LimitFam (Discrete (S n)) (~>) f)
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
}}}
Message is
{{{
T4950.hs:102:51:
Could not deduce (BinaryProduct
(Cod f) (f :% Z) (LimitFam (Discrete n1) (Cod f)
(Next f))
~
LimitFam (Discrete (S n)) (Cod f) f)
from the context (Functor f,
Dom f ~ Discrete (S n),
HasLimits (Discrete n) (Cod f),
HasBinaryProducts (Cod f))
bound by the type signature for
limitUniv' :: (Functor f,
Dom f ~ Discrete (S n),
HasLimits (Discrete n) (Cod f),
HasBinaryProducts (Cod f)) =>
f -> LimitUniversal f
at T4950.hs:(54,1)-(108,35)
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 T4950.hs:102:14-34
Expected type: Cod
f
(LimitFam (Discrete (S n)) (Cod f) f)
(LimitFam (Discrete n1) (Cod f) (Next f))
Actual type: Cod
f
(BinaryProduct (Cod f) (f :% Z) (Limit (Next f)))
(Limit (Next f))
In the second argument of `(.)', namely `p2'
In the expression: undefined . p2
In an equation for `h':
h (S (n :: Discrete n a a))
= undefined . p2
where
p2 ::
Cod f (BinaryProduct (Cod f) (f :% Z) (Limit (Next f)))
(Limit (Next f))
p2 = proj2 x y
}}}
--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/4950#comment:2>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
_______________________________________________
Glasgow-haskell-bugs mailing list
Glasgow-haskell-bugs@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
