[GHC] #16255: Visible kind application defeats type family with higher-rank result kind

[GHC]

#16255: Visible kind application defeats type family with higher-rank result kind
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  8.7
  checker)                           |             Keywords:
      Resolution:                    |  TypeApplications, TypeFamilies
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  GHC accepts       |  Unknown/Multiple
  invalid program                    |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:  #15740            |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by RyanGlScott):

 Your hunch is correct, since
 [https://gitlab.haskell.org/ghc/ghc/blob/7cdcd3e12a5c3a337e36fa80c64bd72e5ef79b24/compiler/typecheck/TcTyClsDecls.hs#L1736-1739
 the current implementation] of the arity checker ignores invisible
 arguments entirely:

 {{{#!hs
           -- this check reports an arity error instead of a kind error;
 easier for user
        ; let vis_pats = numVisibleArgs hs_pats
        ; checkTc (vis_pats == vis_arity) $
                   wrongNumberOfParmsErr vis_arity

 ...
   where
     vis_arity = length (tyConVisibleTyVars tc_fam_tc)
 }}}

 I wonder if fixing this check is as simple as adding another `checkTc` for
 the number of specified arguments? Something like:

 {{{#!hs
   ; let invis_pats = length hs_pats - vis_pats
   ; checkTc (invis_pats <= specified_arity) $ error "You done goofed"

 ...
   where
     specified_arity = length [ tv | Bndr tv vis <- tyConBinders tc
                                   , tyConBndrVisArgFlag vis == Specified ]
 }}}

 I can only think of one place where this sort of thing could go wrong. If
 you instantiate a specified argument with `forall a. a`, then you could
 theoretically do something like this:

 {{{#!hs
 type family F :: k where        -- One specified binder...
   F @(forall a. a) @Bool = True -- ...but two specified arguments!
 }}}

 That being said, GHC currently doesn't allow type family definitions like
 this one:

 {{{
     • Illegal polymorphic type: forall a. a
     • In the equations for closed type family ‘F’
       In the type family declaration for ‘F’
 }}}

 So perhaps this isn't an issue in practice.

-- 
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/16255#comment:2>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler