Opened 10 days ago

Last modified 9 days ago

#14645 new bug

Allow type family in data family return kind

Reported by: goldfire Owned by:
Priority: normal Milestone:
Component: Compiler Version: 8.4.1-alpha1
Keywords: TypeInType, TypeFamilies Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

GHC currently allows

data family DF1 :: k1 -> k2

where it's expected (and checked) that all data instances have a return kind of Type. (Perhaps k2 expands to Type -> Type, for example.)

However, it rejects

type family TF (x :: Type) :: Type
data family DF2 :: x -> TF x

when that's clearly just as sensible as the first definition.

Change History (6)

comment:1 Changed 10 days ago by RyanGlScott

Is this the same bug as #14042?

EDIT: No it isn't, as this concerns data families only.

Last edited 10 days ago by RyanGlScott (previous) (diff)

comment:2 Changed 9 days ago by simonpj

But there is useful discussion in #14042.

comment:3 Changed 9 days ago by simonpj

Let's translate to FC. Here's the example

type family TF (x :: Type) :: Type
data family DF (x :: Type) :: TF x

type instance TF Bool = Type -> Type

data instance DF Bool (a :: Type) = T1 a | T2

The translation to FC might look like this

axiom ax1 :: TF Bool ~ (Type -> Type)

data DFBool a = T1 a | T2   -- An ordinary algebraic data type
  -- T1 :: a -> DFBool a

axiom ax2 :: DFBool ~ DF Bool |> ax1

$WT1 :: forall a. a -> DF Bool a
$WT1 = /\a. \(x::a). T1 x |> ax2 a
  -- ax2 a :: DFBool a ~ ((DF Bool) |> ax1) a

The kind coercion |> ax1 in the kind of axiom ax2 is essential to make axiom ax2 homogeneously kinded; both sides have kind Type -> Type.

Does that look right?

comment:4 Changed 9 days ago by goldfire

Does that look right?

Almost. You need a cast in the type of $WT1:

$WT1 :: forall a. a -> (DF Bool |> ax1) a

Otherwise, yes, I agree.

comment:5 Changed 9 days ago by simonpj

Fine. Then let's do it! (Or does it need a GHC proposal?)

comment:6 Changed 9 days ago by goldfire

I think this passes under the bar of a proposal. :)

Note: See TracTickets for help on using tickets.