Opened 4 months ago

Closed 3 months ago

#13988 closed bug (fixed)

GADT constructor with kind equality constraint quantifies unused existential type variables

Reported by: RyanGlScott Owned by:
Priority: normal Milestone: 8.4.1
Component: Compiler (Type checker) Version: 8.0.1
Keywords: TypeInType Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: Incorrect result at runtime Test Case: ghci/scripts/T13988
Blocked By: Blocking: #14131
Related Tickets: Differential Rev(s): Phab:D3902
Wiki Page:

Description

Reproducible with GHC 8.0.1., 8.0.2, 8.2.1, or HEAD (but I'll use GHC 8.2.1 to show the results of :type +v):

$ /opt/ghc/8.2.1/bin/ghci
GHCi, version 8.2.0.20170704: http://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
λ> :set -XTypeInType -XGADTs -fprint-explicit-foralls 
λ> import Data.Kind
λ> data Foo (a :: k) where MkFoo :: (k ~ Type) => Foo (a :: k)
λ> :type +v MkFoo
MkFoo :: forall k1 (a :: k1) k2 (k3 :: k2). k1 ~ * => Foo a

Note that MkFoo quantifies two extra existential type variables, k2 and k3 which are completely unused!

Note that this does not occur if the MkFoo constructor uses an explicit forall:

λ> :set -XScopedTypeVariables 
λ> data Foo (a :: k) where MkFoo :: forall k (a :: k). (k ~ Type) => Foo (a :: k)
λ> :type +v MkFoo
MkFoo :: forall k (a :: k). k ~ * => Foo a

Change History (8)

comment:1 Changed 3 months ago by RyanGlScott

Differential Rev(s): Phab:D3872
Status: newpatch

I ended up needing to fix this as a part of an unrelated patch, Phab:D3872. (Note that I borrowed the solution for this particular issue from Richard, so the credit should go to him.)

comment:2 Changed 3 months ago by RyanGlScott

Differential Rev(s): Phab:D3872
Status: patchnew

...but Phab:D3872 is in limbo for the time being, so I'll set the resolution back to "new" again.

comment:3 Changed 3 months ago by RyanGlScott

Differential Rev(s): Phab:D3872
Status: newpatch

...and now Phab:D3872 is back! Re-setting the Differential revision.

comment:4 Changed 3 months ago by RyanGlScott

Blocking: 14131 added
Differential Rev(s): Phab:D3872Phab:D3902

I decided to split this off into its own Diff, since it's a somewhat hefty patch by itself.

comment:5 Changed 3 months ago by Ben Gamari <ben@…>

In b9ac9e0/ghc:

Fix egregious duplication of vars in RnTypes

`RnTypes` contains a fairly intricate algorithm to extract
the kind and type variables of an HsType. This algorithm carefully
maintains the separation between type variables and kind variables
so that the difference between `-XPolyKinds` and `-XTypeInType` can
be respected.

But after doing all this, `rmDupsInRdrTyVars` stupidly just
concatenated the lists of type and kind variables at the end. If a
variable were used as both a type and a kind, the algorithm would
produce *both*! This led to all kinds of problems, including #13988.

This is mostly Richard Eisenberg's patch. The only original
contribution I made was adapting call sites of `rnImplicitBndrs` to
work with the new definition of `rmDupsInRdrTyVars`. That is,
`rnImplicitBndrs` checks for variables that are illegally used in
both type and kind positions without using `-XTypeInType`, but in
order to check this, one cannot have filtered duplicate variables out
before passing them to `rnImplicitBndrs`. To accommodate for this, I
needed to concoct variations on the existing `extract-` functions in
`RnTypes` which do not remove duplicates, and use those near
`rnImplicitBndrs` call sites.

test case: ghci/scripts/T13988

Test Plan: make test TEST=T13988

Reviewers: goldfire, simonpj, austin, bgamari

Reviewed By: goldfire, simonpj

Subscribers: rwbarton, thomie

GHC Trac Issues: #13988

Differential Revision: https://phabricator.haskell.org/D3902

comment:6 Changed 3 months ago by bgamari

Can this be considered resolved?

comment:7 Changed 3 months ago by simonpj

Test Case: ghci/scripts/T13988

comment:8 in reply to:  6 Changed 3 months ago by RyanGlScott

Milestone: 8.4.1
Resolution: fixed
Status: patchclosed

Replying to bgamari:

Can this be considered resolved?

Indeed it can.

Note: See TracTickets for help on using tickets.