GitLab

Let me know if this is expected behaviour, I want to return the object type of a category Cat ob which is what I use as a shorthand for ob -> ob -> Type.

I want to be able to write Object (->) and get out Type, when written as a type synonym the call to Object (->) gets stuck:

{-# Language ConstraintKinds          #-}
{-# Language DataKinds                #-}
{-# Language GADTs                    #-}
{-# Language PolyKinds                #-}
{-# Language RankNTypes               #-}
{-# Language StandaloneKindSignatures #-}
{-# Language TypeFamilies             #-}
{-# Language TypeOperators            #-}

import Data.Kind

type Cat :: Type -> Type
type Cat ob = ob -> ob -> Type

type Dict :: Constraint -> Type
data Dict cls where
 Dict :: cls => Dict cls

type    (:-) :: Cat Constraint
newtype cls1 :- cls2 where
 Sub :: (cls1 => Dict cls2) -> (cls1 :- cls2)

-- > :k! Object ((->) :: Cat Type)
-- = Object (->)
--
-- > import Data.Type.Equality
-- > :k! Object (:~:)
-- = Object (:~:)
--
-- > :k! Object Op
-- = Object Op
--
-- > :k! Object (:-)
-- = Object (:-)
type Object :: Cat ob -> Type
type Object (cat :: ob -> ob -> Type) = ob

It works with a type family, what is the difference here?

-- > :k! Object (->)
-- = *
--
-- > :k! forall ob. Object ((:~:) :: Cat ob)
-- = ob
--
-- > :k! Object Op
-- = *
--
-- > :k! Object (:-)
-- = Constraint
type
  Object :: Cat ob -> Type
type family
  Object cat where
  Object @ob cat = ob

Tested with GHC 9.0.0.20200925.