
#14645: Allow type family in data family return kind -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.4.1-alpha1 Resolution: | Keywords: TypeInType, | TypeFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (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! -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14645#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler