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,873
    • Issues 4,873
    • List
    • Boards
    • Service Desk
    • Milestones
    • Iterations
  • Merge requests 457
    • Merge requests 457
  • 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
  • #4950
Closed
Open
Created Feb 09, 2011 by Ian Lynagh <igloo@earth.li>@trac-igloo

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
Assignee
Assign to
Time tracking