#16356: Unexpected type application in default declaration -------------------------------------+------------------------------------- Reporter: int-index | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.6.3 checker) | Resolution: | Keywords: 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): Upon further thought, I downplayed the amount of effort required to make this work in comment:1. [https://gitlab.haskell.org/ghc/ghc/blob/2e8f664957dc3763dc4375894b8dc4d046d2... This code] in `TcTyClsDecls.tcDefaultAssocDecl` is problematic: {{{#!hs tcDefaultAssocDecl fam_tc [dL->L loc (FamEqn { feqn_tycon = L _ tc_name , feqn_pats = hs_tvs , feqn_rhs = hs_rhs_ty })] | HsQTvs { hsq_ext = HsQTvsRn { hsq_implicit = imp_vars} , hsq_explicit = exp_vars } <- hs_tvs = -- <elided> fam_arity = length (tyConVisibleTyVars fam_tc) -- <elided> -- Arity check ; checkTc (exp_vars `lengthIs` fam_arity) (wrongNumberOfParmsErr fam_arity) }}} Unless the number of `exp_vars` is exactly the number of visible arguments that the type family expects, then `wrongNumberOfParmsErr` will throw an error. Unfortunately, it turns out that `exp_vars` //includes// visible kind arguments! In other words, if you have this: {{{#!hs class FAssocDefaultClass k where type FAssocDefault :: k -> Type type FAssocDefault @k = B @k }}} Then `exp_vars = [k]` and `fam_arity = 0`, which means that GHC will mistakenly reject `FAssocDefault` under the guise that it supplies too many arguments. ----- Why, then, does this problem not occur for ordinary type family equations? It turns out that it's because GHC stores the ASTs for each form of declaration in subtly different ways. [https://gitlab.haskell.org/ghc/ghc/blob/2e8f664957dc3763dc4375894b8dc4d046d2... This] is how GHC represents ordinary type family equations: {{{#!hs type FamInstEqn pass rhs = HsImplicitBndrs pass (FamEqn pass (HsTyPats pass) rhs) }}} And [https://gitlab.haskell.org/ghc/ghc/blob/2e8f664957dc3763dc4375894b8dc4d046d2... this] is how GHC represents associated type family defaults: {{{#!hs type TyFamDefltEqn pass = FamEqn pass (LHsQTyVars pass) (LHsType pass) }}} The important bit here is the second argument to `FamEqn`, which represents the patterns in the type family equation. In `FamInstEqn`s, the patterns are `HsTyPats`, which distinguish between ordinary arguments and visible kind arguments. In `TyFamDefltEqn`, however, the patterns are `LHsQTyVars`. AFAICT, `LHsQTyVars` do not make any sort of distinction between ordinary arguments and visible kind arguments, instead only caring about explicitly vs. implicitly quantified variables. ----- How, then, should we change things to allow VKAs in type family defaults? One option is to try switching out `LHsQTyVars` for `HsTyPats` in `TyFamDefltEqn`. I'm not clear as to why we're using `LHsQTyVars` in the first place, however, so it's possible that there actually is a good reason for its existence here. If so, another alternative would be to somehow augment `LHsQTyVars` with informative about which of its arguments are VKAs or not. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16356#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler