[GHC] #13988: GADT constructor with kind equality constraint quantifies unused existential type variables
#13988: GADT constructor with kind equality constraint quantifies unused existential type variables -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 (Type checker) | Keywords: TypeInType | Operating System: Unknown/Multiple Architecture: | Type of failure: Incorrect result Unknown/Multiple | at runtime Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- 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 }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/13988> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#13988: GADT constructor with kind equality constraint quantifies unused existential type variables -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: patch Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: Type of failure: Incorrect result | Unknown/Multiple at runtime | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D3872 Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * status: new => patch * differential: => Phab:D3872 Comment: 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.) -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/13988#comment:1> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#13988: GADT constructor with kind equality constraint quantifies unused existential type variables -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: Type of failure: Incorrect result | Unknown/Multiple at runtime | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * status: patch => new * differential: Phab:D3872 => Comment: ...but Phab:D3872 is in limbo for the time being, so I'll set the resolution back to "new" again. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/13988#comment:2> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#13988: GADT constructor with kind equality constraint quantifies unused existential type variables -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: patch Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: Type of failure: Incorrect result | Unknown/Multiple at runtime | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D3872 Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * status: new => patch * differential: => Phab:D3872 Comment: ...and now Phab:D3872 is back! Re-setting the Differential revision. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/13988#comment:3> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#13988: GADT constructor with kind equality constraint quantifies unused existential type variables -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: patch Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: Type of failure: Incorrect result | Unknown/Multiple at runtime | Test Case: Blocked By: | Blocking: 14131 Related Tickets: | Differential Rev(s): Phab:D3902 Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * differential: Phab:D3872 => Phab:D3902 * blocking: => 14131 Comment: I decided to split this off into its own Diff, since it's a somewhat hefty patch by itself. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/13988#comment:4> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#13988: GADT constructor with kind equality constraint quantifies unused existential type variables -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: patch Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: Type of failure: Incorrect result | Unknown/Multiple at runtime | Test Case: Blocked By: | Blocking: 14131 Related Tickets: | Differential Rev(s): Phab:D3902 Wiki Page: | -------------------------------------+------------------------------------- Comment (by Ben Gamari <ben@…>): In [changeset:"b9ac9e05b29c58efc93b78bf7fca43d61ead50c7/ghc" b9ac9e0/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="b9ac9e05b29c58efc93b78bf7fca43d61ead50c7" 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 }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/13988#comment:5> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#13988: GADT constructor with kind equality constraint quantifies unused existential type variables -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: patch Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: Type of failure: Incorrect result | Unknown/Multiple at runtime | Test Case: Blocked By: | Blocking: 14131 Related Tickets: | Differential Rev(s): Phab:D3902 Wiki Page: | -------------------------------------+------------------------------------- Comment (by bgamari): Can this be considered resolved? -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/13988#comment:6> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#13988: GADT constructor with kind equality constraint quantifies unused existential type variables -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: patch Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: Incorrect result | Test Case: at runtime | ghci/scripts/T13988 Blocked By: | Blocking: 14131 Related Tickets: | Differential Rev(s): Phab:D3902 Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * testcase: => ghci/scripts/T13988 -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/13988#comment:7> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#13988: GADT constructor with kind equality constraint quantifies unused existential type variables -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: 8.4.1 Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: fixed | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: Incorrect result | Test Case: at runtime | ghci/scripts/T13988 Blocked By: | Blocking: 14131 Related Tickets: | Differential Rev(s): Phab:D3902 Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * status: patch => closed * resolution: => fixed * milestone: => 8.4.1 Comment: Replying to [comment:6 bgamari]:
Can this be considered resolved?
Indeed it can. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/13988#comment:8> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
participants (1)
-
GHC