#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 RyanGlScott): Is this the same bug as #14042? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14645#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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 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? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14645#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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 simonpj): Fine. Then let's do it! (Or does it need a GHC proposal?) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14645#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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 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: {{{#!hs -- | 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: {{{#!diff ; 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14645#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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): Why do you think you need step 2? I think the existing code in `kcDataDefn` will do the right thing here. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14645#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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