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:1 Changed 8 months ago by RyanGlScott

Is this the same bug as #14042?

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

Last edited 8 months ago by RyanGlScott (previous) (diff)

comment:2 Changed 7 months ago by simonpj

But there is useful discussion in #14042.

comment:3 Changed 7 months 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 7 months 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 7 months ago by simonpj

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

comment:6 Changed 7 months ago by goldfire

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

comment:7 Changed 2 months ago by RyanGlScott

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 goldfire

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

Why do you think you need step 2? I think the existing code in kcDataDefn will do the right thing here.

comment:10 in reply to:  9 Changed 2 months ago by RyanGlScott

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 goldfire

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.