Skip to content

data families shouldn't be required to have return kind *, data instances should

I'd like to be able to define

{-# language PolyKinds, KindSignatures, GADTs, TypeFamilies #-}
data family Fix :: (k -> *) -> k
newtype instance Fix f = In { out :: f (Fix f) }

But currently this is disallowed:

Fix.hs:2:1: error:
    • Kind signature on data type declaration has non-* return kind
        (k -> *) -> k
    • In the data family declaration for ‘Fix’

Ultimately I think the issue here is that data instances should be required to end in kind *, not the families, but this generalization didn't mean anything until we had PolyKinds.

As an example of a usecase, with the above, I could define a bifunctor fixed point such as

newtype instance Fix f a = In2 { out2 :: f (Fix f a) a }
Trac metadata
Trac field Value
Version 8.0.1
Type FeatureRequest
TypeOfFailure OtherFailure
Priority normal
Resolution Unresolved
Component Compiler (Type checker)
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