#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 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): 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: | 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: | -------------------------------------+------------------------------------- Comment (by Richard Eisenberg ): 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