Opened 8 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 (11)

### comment:3 Changed 7 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 7 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.

### comment:7 Changed 2 months ago by

I tried giving this a go, but quickly became stuck. I'll dump my progress here in case anyone finds it useful.

- The first step is revising a validity check to allow type families to appear in data family return kinds. You'll need a predicate which checks if a type is a type family application:

-- | Returns @'Just' (fam_tc, args)@ if the argument 'Type' is a type family -- constructor @fam_tc@ applied to some arguments @args@. Otherwise, returns -- @Nothing@. tcGetTyFamTyConApp_maybe :: Type -> Maybe (TyCon, [Type]) tcGetTyFamTyConApp_maybe ty | Just ty' <- tcView ty = tcGetTyFamTyConApp_maybe ty' tcGetTyFamTyConApp_maybe (TyConApp fam_tc args) | isTypeFamilyTyCon fam_tc = Just (fam_tc, args) tcGetTyFamTyConApp_maybe _ = Nothing

Then you'll need to change

`tcFamDecl1`

to use this:

; checkTc (tcIsStarKind final_res_kind - || isJust (tcGetCastedTyVar_maybe final_res_kind)) + || isJust (tcGetCastedTyVar_maybe final_res_kind) + || isJust (tcGetTyFamTyConApp_maybe final_res_kind)) (badKindSig False res_kind)

- The next step is to figure out where to grab the type family instance axiom from when typechecking data family instances (in
`tcDataFamInstDecl`

).

My first inclination was to change

`tcDataKindSig`

to return a`CoAxiom`

resulting from the return kind signature. However, this doesn't always work. For instance, in the example from comment:3, the return kind of the`DF Bool (a :: Type)`

instance is simply`Type`

by the type you get to`tcDataKindSig`

(instead of something like`TF Bool`

), which makes it essentially impossible to grab a type family axiom from.

This makes me suspect that we need to grab this type family axiom earlier, perhaps when typechecking the type family patterns (in

`tcFamTyPats`

). At this point, I became lost.

### comment:8 Changed 2 months ago by

For step one, I wonder if it would be better to look for return kinds that are not *apart* from `TYPE r`

. Perhaps this would do it:

-- | Returns whether the two types are apart. Assumes that -- both types have the same kind. apart :: Type -> Type -> Bool apart ty1 ty2 | SurelyApart <- tcUnifyTysFG (const BindMe) [ty1] [ty2] = True | otherwise = False

(I'm surprised that function doesn't already exist.)

Then, use that to check the return kind against `TYPE r`

(where `r`

can really be any tyvar). This should subsume the current check.

### comment:9 follow-up: 10 Changed 2 months ago by

Why do you think you need step 2? I think the existing code in `kcDataDefn`

will do the right thing here.

### comment:10 Changed 2 months ago by

Replying to goldfire:

Why do you think you need step 2? I think the existing code in

`kcDataDefn`

will do the right thing here.

I'm not sure that I understand this comment. You're suggesting that GHC will do all of the steps outlined in comment:3 with only step 1? Experimental evidence suggests that this is not true, as trying an implementation with only step 1 panics when given the program in comment:3.

### comment:11 Changed 2 months ago by

OK. I was hopelessly optimistic.

The problem is that, currently, type family axioms never have casts in quite the spot that `ax2`

of comment:3 has one in. So we'd need to make a place for that cast, and I don't see an easy way to do that, because the axiom LHS might be something like `((DF ty1 ty2) |> co) ty3 ty4`

. Maybe we need to have axioms just take an LHS type instead of a bunch of patterns. But then we'll run into trouble with matching.

I *think* we'd have to overhaul `CoAxBranch`

and `FamInst`

to make this work. I don't actually think it would be all that hard, but a good deal of plumbing would have to move, as we're currently assuming that every axiom LHS looks like `F tys`

.

Once the plumbing has been rearranged, then the `kind_checker`

in tcFamTyPats` would have to return some more exotic structure that takes the applied tycon and transforms it to the correct axiom LHS. This should probably be something of type `

TcType -> TcType`. (To be clear, I'm proposing that the 5th argument to `

tcFamTyPats` have type `

TcKind -> TcM (TcType -> TcType, TcKind)`.) Currently, the `

kind_checker` returns extra type patterns; these are always appended to existing patterns. The new form would simply be applied to the family tycon applied to the existing patterns.

Then, in `kcDataDefn`

, you would build the right transformation from the `co`

returned by `checkExpectedKindX`

-- right now, this `co`

is ignored.

Definitely hairier than I thought!

**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.