#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/406e43af2f12756c80d583b86326f760f2f5... 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/406e43af2f12756c80d583b86326f760f2f5... 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