[GHC] #16287: :kind accepts bogus type

[GHC]

#16287: :kind accepts bogus type
-------------------------------------+-------------------------------------
        Reporter:  simonpj           |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  8.6.3
      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):

 Here's an even simpler example:

 {{{
 λ> data T :: (Type -> Type) -> Type
 λ> type F a = a
 λ> :k T F
 T F :: *
 }}}

 I'm very surprised that `TcValidity` doesn't catch this. Now that I look
 closer,
 [https://gitlab.haskell.org/ghc/ghc/blob/406e43af2f12756c80d583b86326f760f2f584cc/compiler/typecheck/TcValidity.hs#L604-608
 here's why]:

 {{{#!hs
 check_type ve ty@(TyConApp tc tys)
   | isTypeSynonymTyCon tc || isTypeFamilyTyCon tc
   = check_syn_tc_app ve ty tc tys
   | isUnboxedTupleTyCon tc = check_ubx_tuple ve ty tys
   | otherwise              = mapM_ (check_arg_type ve) tys
 }}}

 If `T` were a type synonym, then we'd call `check_syn_tc_app`, which would
 reject the unsaturated `F` argument. But since `T` isn't a type synonym,
 we instead go down a different code path (`check_arg_type`), which doesn't
 catch this.

 FWIW,
 [https://gitlab.haskell.org/ghc/ghc/blob/406e43af2f12756c80d583b86326f760f2f584cc/compiler/typecheck/TcValidity.hs#L716-723
 this] is all that `check_syn_tc_app` does to ensure that unsaturated
 arguments are rejected:

 {{{#!hs
     arg_ctxt :: UserTypeCtxt
     arg_ctxt
       | GhciCtxt _ <- ctxt = GhciCtxt False
           -- When checking an argument, set the field of GhciCtxt to False
 to
           -- indicate that we are no longer in an outermost position (and
 thus
           -- unsaturated synonyms are no longer allowed).
           -- See Note [Unsaturated type synonyms in GHCi]
       | otherwise          = ctxt
 }}}

 Perhaps we should just use this logic in `check_arg_type` as well? I think
 that would catch the program in this ticket without too much fuss.

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