#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

#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): From a quick glance, I would guess that the only reason for `check_syn_tc_app` calling `check_type` instead of `check_arg_type` is due to `LiberalTypeSynonyms`. For instance, consider this (where `T` is a type synonym) {{{ λ> :set -XLiberalTypeSynonyms -XRankNTypes λ> type T a = a λ> :k T (forall a. a) }}} If you check `T`'s argument with `check_type` (as `check_syn_tc_app` does currently), then this will be accepted. If you check it with `check_arg_type`, however, it will be rejected: {{{ Illegal polymorphic type: forall a. a GHC doesn't yet support impredicative polymorphism }}} The difference amounts to whether you set `ve_rank` to `synArgMonoType` (as `check_syn_tc_app` does before invoking `check_type`) or `tyConArgMonoType` (as `check_arg_type` does). Perhaps we can tweak `check_arg_type` so that it knows when to use `synArgMonoType`—it might be as simple as passing an extra `Bool` argument to `check_arg_type` indicating whether this is the argument to a type synonym or not. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16287#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#16287: :kind accepts bogus type -------------------------------------+------------------------------------- Reporter: simonpj | Owner: (none) Type: bug | Status: merge Priority: normal | Milestone: 8.8.1 Component: Compiler | Version: 8.6.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: | ghci/should_fail/T16287 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | https://gitlab.haskell.org/ghc/ghc/merge_requests/293 -------------------------------------+------------------------------------- Changes (by RyanGlScott): * testcase: => ghci/should_fail/T16287 * status: patch => merge * milestone: => 8.8.1 Comment: Landed in [https://gitlab.haskell.org/ghc/ghc/commit/c07e7ecbdfc05429fb6ce84c547c0365d2... c07e7ecb]. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16287#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler