Opened 7 months ago

Last modified 7 months ago

#16255 merge bug

Visible kind application defeats type family with higher-rank result kind

Reported by: RyanGlScott Owned by:
Priority: normal Milestone: 8.8.1
Component: Compiler (Type checker) Version: 8.7
Keywords: TypeApplications, TypeFamilies Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC accepts invalid program Test Case: typecheck/should_fail/T16255
Blocked By: Blocking:
Related Tickets: #15740 Differential Rev(s): https://gitlab.haskell.org/ghc/ghc/merge_requests/260
Wiki Page:

Description

After #15740, GHC now (correctly) rejects this program:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
module Bug where

import Data.Kind

data SBool :: Bool -> Type
type family F :: forall k. k -> Type where
  F = SBool
$ ~/Software/ghc5/inplace/bin/ghc-stage2 --interactive Bug.hs
GHCi, version 8.7.20190115: https://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug              ( Bug.hs, interpreted )

Bug.hs:12:7: error:
    • Expected kind ‘forall k. k -> *’,
        but ‘SBool’ has kind ‘Bool -> *’
    • In the type ‘SBool’
      In the type family declaration for ‘F’
   |
12 |   F = SBool
   |       ^^^^^

However, there's a very simple way to circumvent this: add a visible kind application to F's equation.

type family F :: forall k. k -> Type where
  F @Bool = SBool

If I understand things correctly, GHC shouldn't allow this.

Change History (7)

comment:1 Changed 7 months ago by goldfire

You understand things correctly. The arity checker probably only looks at the visible arity, which is correct, and the kind, which is also correct. Of course, that's clearly not the whole story.

comment:2 Changed 7 months ago by RyanGlScott

Your hunch is correct, since the current implementation of the arity checker ignores invisible arguments entirely:

          -- this check reports an arity error instead of a kind error; easier for user
       ; let vis_pats = numVisibleArgs hs_pats
       ; checkTc (vis_pats == vis_arity) $
                  wrongNumberOfParmsErr vis_arity

...
  where
    vis_arity = length (tyConVisibleTyVars tc_fam_tc)

I wonder if fixing this check is as simple as adding another checkTc for the number of specified arguments? Something like:

  ; let invis_pats = length hs_pats - vis_pats
  ; checkTc (invis_pats <= specified_arity) $ error "You done goofed"

...
  where
    specified_arity = length [ tv | Bndr tv vis <- tyConBinders tc
                                  , tyConBndrVisArgFlag vis == Specified ]

I can only think of one place where this sort of thing could go wrong. If you instantiate a specified argument with forall a. a, then you could theoretically do something like this:

type family F :: k where        -- One specified binder...
  F @(forall a. a) @Bool = True -- ...but two specified arguments!

That being said, GHC currently doesn't allow type family definitions like this one:

    • Illegal polymorphic type: forall a. a
    • In the equations for closed type family ‘F’
      In the type family declaration for ‘F’

So perhaps this isn't an issue in practice.

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

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.

comment:4 in reply to:  3 Changed 7 months ago by RyanGlScott

Replying to goldfire:

This should probably be done in the validity checker.

How would that possibly work? By the time we're in the validity checker, all we have are CoAxBranches, which don't distinguish between required and specified arguments.

comment:5 Changed 7 months ago by RyanGlScott

Ah, I just realized the answer to my own question: this information is (indirectly) stored in the tyConBinders of the type family tycon. We'd have to do a little bit of reverse engineering to recover which type patterns had which visibility, but it should be possible (I think).

Another challenge is figuring out a good SrcSpan to use in the error message, which we don't have any location info in TcValidity. Maybe we'll just have to settle for the SrcSpan of the entire type family equation?

comment:6 Changed 7 months ago by RyanGlScott

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

comment:7 Changed 7 months ago by RyanGlScott

Status: patchmerge
Test Case: typecheck/should_fail/T16255
Note: See TracTickets for help on using tickets.