[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 goldfire):

 I have no idea what that `F` would mean if it were allowed. Thankfully,
 it's not.

 I don't think it's as simple as that arity check, though. Witness

 {{{#!hs
 type family F (x :: j) :: forall k. Either j k where
   F 5 @Symbol = Left 4
 }}}

 That looks well-kinded to me, it has the right visible arity, and it has
 the right specified arity, but it's still wrong.

 To get this right, I think we have to look not at the overall specified
 arity, but the specified arity ''after the last visible argument''. If we
 get that right, I think we've gotten this aspect right. (Note that a
 problem before the last visible argument must necessarily be a kind error,
 not an arity error.) That's a bit gross, but I think it will work.

 This should probably be done in the validity checker. The spot you've
 edited above is in the kind-checker. The only reason the visible arity
 check is done there is because it gives a nicer error message. These
 checks morally ought to be later.

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