Re: #16356: Unexpected type application in default declaration

#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/2e8f664957dc3763dc4375894b8dc4d046d2e95b/compiler/typecheck/TcTyClsDecls.hs#L1401-1419
 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/2e8f664957dc3763dc4375894b8dc4d046d2e95b/compiler/hsSyn/HsDecls.hs#L1618-1619
 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/2e8f664957dc3763dc4375894b8dc4d046d2e95b/compiler/hsSyn/HsDecls.hs#L1581
 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>