Opened 7 months ago

Last modified 6 months ago

#16287 merge bug

:kind accepts bogus type

Reported by: simonpj Owned by:
Priority: normal Milestone: 8.8.1
Component: Compiler Version: 8.6.3
Keywords: Cc:
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): https://gitlab.haskell.org/ghc/ghc/merge_requests/293
Wiki Page:

Description

Consider this (current HEAD)

ghci> type family F :: k
ghci> data T :: (forall k. k) -> Type
ghci> :kind T F
T F :: *

This is bogus. F has arity 1, and cannot appear unsaturated.

Change History (6)

comment:1 Changed 7 months ago 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, here's why:

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, this is all that check_syn_tc_app does to ensure that unsaturated arguments are rejected:

    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.

comment:2 Changed 7 months ago by simonpj

Perhaps we should just use this logic in check_arg_type as well?

Yes, that looks plausible. Moreover, check_arg_type is called from check_syn_tc_app, so maybe we can only do it in check_arg_type?

(But there is one patch from check_syn_tc_app direct to check_type, bypassing check_arg_type for reasons that are not clear to me. If it could go to check_arg_type we'd be golden.

comment:3 Changed 7 months ago 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.

comment:4 Changed 7 months ago by RyanGlScott

Differential Rev(s): https://gitlab.haskell.org/ghc/ghc/merge_requests/293
Status: newpatch

comment:5 Changed 7 months ago by RyanGlScott

Milestone: 8.8.1
Status: patchmerge
Test Case: ghci/should_fail/T16287

Landed in c07e7ecb.

comment:6 Changed 6 months ago by Marge Bot <ben+marge-bot@…>

In c07e7ec/ghc:

Fix #16287 by checking for more unsaturated synonym arguments

Trac #16287 shows that we were checking for unsaturated type synonym
arguments (in `:kind`) when the argument was to a type synonym, but
_not_ when the argument was to some other form of type constructor,
such as a data type. The solution is to use the machinery that
rejects unsaturated type synonym arguments (previously confined to
`check_syn_tc_app`) to `check_arg_type`, which checks these other
forms of arguments. While I was in town, I cleaned up
`check_syn_tc_app` a bit to only invoke `check_arg_type` so as to
minimize the number of different code paths that that function could
go down.
Note: See TracTickets for help on using tickets.