Opened 2 months ago

Last modified 2 months 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:3 Changed 2 months ago by

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 2 months ago by

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.

**Note:**See TracTickets for help on using tickets.

Is this the same bug as #14042?

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