:kind! fails to expand type synonyms
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.
Edited by Simon Peyton Jones