[GHC] #15795: Core lint error with visible kind patterns
#15795: Core lint error with visible kind patterns -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.1 Keywords: | Operating System: Unknown/Multiple TypeApplications | Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- Finally managed to trigger a core lint error with #12045 {{{#!hs {-# Language RankNTypes #-} {-# Language TypeApplications #-} {-# Language DataKinds #-} {-# Language PolyKinds #-} {-# Language TypeOperators #-} {-# Language GADTs #-} {-# Options_GHC -dcore-lint #-} import Data.Kind type Cat ob = ob -> ob -> Type data (×) :: forall (cat1 :: Cat ob1) (cat2 :: Cat ob2). Cat (ob1, ob2) where Prod :: forall ob1 ob2 cat1 cat2 a1 b1 a2 b2 u. cat1 a1 b1 -> cat2 a2 b2 -> (×) @u '(a1, a2) '(b1, b2) }}} log attached from running `ghci -ignore-dot-ghci <file>.hs` -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15795> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#15795: Core lint error with visible kind patterns -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.1 Resolution: | Keywords: | TypeApplications Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by Iceland_jack): * Attachment "log" added. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15795> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#15795: Core lint error with visible kind patterns -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.1 Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by goldfire): * keywords: TypeApplications => TypeInType * cc: mnguyen (removed) Comment: This has nothing to do with visible kind application. This fails the same way: {{{#!hs data (×) :: forall (cat1 :: Cat ob1) (cat2 :: Cat ob2). Cat (ob1, ob2) where Prod :: forall ob1 ob2 cat1 cat2 a1 b1 a2 b2 u. cat1 a1 b1 -> cat2 a2 b2 -> (×) '((a1 :: u), a2) '(b1, b2) }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15795#comment:1> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#15795: Core lint error with visible kind patterns -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.1 Resolution: | Keywords: TypeInType 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 monoidal): Smaller version: {{{ #!haskell {-# Language RankNTypes #-} {-# Language PolyKinds #-} {-# Language GADTs #-} {-# Options_GHC -dcore-lint #-} module DF where import Data.Kind data F :: forall (cat1 :: ob1). ob1 -> Type where Prod :: F (a :: u) }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15795#comment:2> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#15795: Core lint error with unused kind variable in data type return kind -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.1 Resolution: | Keywords: TypeInType 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): Thanks, monoidal! -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15795#comment:3> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#15795: Core lint error with unused kind variable in data type return kind -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.1 Resolution: | Keywords: TypeInType 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): It's worth noting that this Core Lint error only appears to occur when GHC constructs a wrapper for `Prod`. In other words, the following errors: {{{#!hs data F :: forall (cat1 :: ob1). ob1 -> Type where Prod :: forall u (a :: u). F a }}} But this does //not// error: {{{#!hs data F :: forall (cat1 :: ob1). ob1 -> Type where Prod :: F a }}} Since in the latter code, `Prod` won't need a wrapper, and its type will simply be `forall {ob1} {cat1 :: ob1} (a :: ob1). F a`. (Currently, there's no way to write that with GHC's explicit `forall` syntax, so pretty much any attempt to write the type of `Prod` using a `forall` will trigger this error.) -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15795#comment:4> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#15795: Core lint error with unused kind variable in data type return kind -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.1 Resolution: | Keywords: TypeInType 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 another way to trigger (what I believe to be) the same issue: {{{#!hs {-# LANGUAGE DataKinds #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE ScopedTypeVariables #-} module Bug where import Data.Kind type KindOf (a :: k) = k data T :: forall j (a :: j). KindOf a -> Type where MkT :: forall k (b :: k). T b }}} {{{ $ /opt/ghc/8.6.3/bin/ghc Bug.hs -dcore-lint [1 of 1] Compiling Bug ( Bug.hs, Bug.o ) *** Core Lint errors : in result of Tidy Core *** <no location info>: warning: In the type ‘forall (a :: k_aVT[sk:1]) k (b :: k). T b’ @ k_aVT[sk:1] is out of scope *** Offending Program *** $WMkT [InlPrag=INLINE[2]] :: forall (a :: k_aVT[sk:1]) k (b :: k). T b [GblId[DataConWrapper], Caf=NoCafRefs, Unf=Unf{Src=InlineStable, TopLvl=True, Value=True, ConLike=True, WorkFree=True, Expandable=True, Guidance=ALWAYS_IF(arity=0,unsat_ok=True,boring_ok=True) Tmpl= \ (@ (a_aWw :: k_aVT[sk:1])) (@ k_XVV) (@ (b_aVU :: k_XVV)) -> MkT @ k_XVV @ a_aWw @ b_aVU}] $WMkT = \ (@ (a_aWw :: k_aVT[sk:1])) (@ k_XVV) (@ (b_aVU :: k_XVV)) -> MkT @ k_XVV @ a_aWw @ b_aVU <elided> *** End of Offense *** <no location info>: error: Compilation had errors }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15795#comment:5> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#15795: Core lint error with unused kind variable in data type return kind -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.1 Resolution: | Keywords: TypeInType 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 Simon Peyton Jones <simonpj@…>): In [changeset:"71e26a74da5e5e9a61163b87ab4d22de88a2d04a/ghc" 71e26a74/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="71e26a74da5e5e9a61163b87ab4d22de88a2d04a" Make candidateQTvs contain tyvar with zonked kinds candidateQTyVars was failing to return fully-zonked tyvars, and that made things fall over chaotically when we try to sort them into a well-scoped telescope. Result: Trac #15795 So I made candidateQTvs guarantee to have fully-zonked tyvars (i.e. with zonked kinds). That's a bit annoying but not really difficult. }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15795#comment:6> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#15795: Core lint error with unused kind variable in data type return kind -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.1 Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: | tests/polykinds/T15795, T15795a Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * testcase: => tests/polykinds/T15795, T15795a Comment: Great test cases thank you. The cause was that `candidateQTyVars` was returning tyvars with unzonked kinds, and that meant we put the binders in the wrong dependency order. Once that happens, chaos results. The fix is easy, but a bit tiresome. Richard you might want to look. The key point it this (in `TcMType`). {{{ go_tv dv@(DV { dv_kvs = kvs, dv_tvs = tvs }) tv | tv `elemDVarSet` kvs = return dv -- We have met this tyvar aleady | not is_dep , tv `elemDVarSet` tvs = return dv -- We have met this tyvar aleady | otherwise = do { tv_kind <- zonkTcType (tyVarKind tv) -- This zonk is annoying, but it is necessary, both to -- ensure that the collected candidates have zonked kinds -- (Trac #15795) and to make the naughty check -- (which comes next) works correctly ; if intersectsVarSet bound (tyCoVarsOfType tv_kind) }}} Now from the two test cases we get the following results. From comment:5 (immortalised as `polykinds/T15795` we get {{{ TYPE CONSTRUCTORS type synonym KindOf{2} :: forall k. k -> * roles nominal phantom data type T{3} :: forall j (a :: j). KindOf @j a -> * roles nominal nominal phantom DATA CONSTRUCTORS MkT :: forall k (b :: k). T @k @(GHC.Types.Any @k) b }}} From comment:2 (immortalised as `polykinds/T15795a` we get {{{ TYPE CONSTRUCTORS data type F{3} :: forall ob1 (cat1 :: ob1). ob1 -> * roles nominal nominal phantom DATA CONSTRUCTORS Prod :: forall u (a :: u). F @u @(GHC.Types.Any @u) a }}} Note the use of `Any`, which I think is right. Richard/Ryan: just check? Then close. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15795#comment:7> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#15795: Core lint error with unused kind variable in data type return kind -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 8.6.1 Resolution: fixed | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: | tests/polykinds/T15795, T15795a Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by goldfire): * status: new => closed * resolution: => fixed Comment: Checked. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15795#comment:8> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#15795: Core lint error with unused kind variable in data type return kind -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 8.6.1 Resolution: fixed | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: | tests/polykinds/T15795, T15795a Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Richard Eisenberg <rae@…>): In [changeset:"17bd163566153babbf51adaff8397f948ae363ca/ghc" 17bd1635/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="17bd163566153babbf51adaff8397f948ae363ca" Visible kind application Summary: This patch implements visible kind application (GHC Proposal 15/#12045), as well as #15360 and #15362. It also refactors unnamed wildcard handling, and requires that type equations in type families in Template Haskell be written with full type on lhs. PartialTypeSignatures are on and warnings are off automatically with visible kind application, just like in term-level. There are a few remaining issues with this patch, as documented in ticket #16082. Includes a submodule update for Haddock. Test Plan: Tests T12045a/b/c/TH1/TH2, T15362, T15592a Reviewers: simonpj, goldfire, bgamari, alanz, RyanGlScott, Iceland_jack Subscribers: ningning, Iceland_jack, RyanGlScott, int-index, rwbarton, mpickering, carter GHC Trac Issues: `#12045`, `#15362`, `#15592`, `#15788`, `#15793`, `#15795`, `#15797`, `#15799`, `#15801`, `#15807`, `#15816` Differential Revision: https://phabricator.haskell.org/D5229 }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15795#comment:9> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
participants (1)
-
GHC