#15788: Core Lint error, from visible kind applications -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.1 Resolution: | Keywords: #12045 Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Description changed by Iceland_jack: Old description:

{{{#!hs {-# Language RankNTypes #-} {-# Language GADTs #-} {-# Language TypeApplications #-} {-# Language PolyKinds #-}

{-# Options_GHC -dcore-lint #-}

import Data.Kind

data A :: forall k. Type where MkA :: A @k }}}

this cute bug crashes under the [https://phabricator.haskell.org/D5229 visible kind application] diff, produces:

{{{ $ ghci -ignore-dot-ghci 545_bug.hs GHCi, version 8.7.20181017: http://www.haskell.org/ghc/ :? for help [1 of 1] Compiling Main ( 545_bug.hs, interpreted ) *** Core Lint errors : in result of Tidy Core *** <no location info>: warning: In the type ‘forall (k :: k_a1xN[sk:1]) k. A’ @ k_a1xN[sk:1] is out of scope *** Offending Program *** $WMkA [InlPrag=INLINE[2]] :: forall (k :: k_a1xN[sk:1]) k. A [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= \ (@ (k_a1y5 :: k_a1xN[sk:1])) (@ k_X1xP) -> MkA @ k_X1xP @ k_a1y5}] $WMkA = \ (@ (k_a1y5 :: k_a1xN[sk:1])) (@ k_X1xP) -> MkA @ k_X1xP @ k_a1y5

$trModule1_r1zb :: Addr# [GblId, Caf=NoCafRefs, Unf=OtherCon []] $trModule1_r1zb = "main"#

$trModule2_r1zu :: TrName [GblId, Caf=NoCafRefs, Unf=OtherCon []] $trModule2_r1zu = TrNameS $trModule1_r1zb

$trModule3_r1zv :: Addr# [GblId, Caf=NoCafRefs, Unf=OtherCon []] $trModule3_r1zv = "Main"#

$trModule4_r1zw :: TrName [GblId, Caf=NoCafRefs, Unf=OtherCon []] $trModule4_r1zw = TrNameS $trModule3_r1zv

$trModule :: Module [GblId, Caf=NoCafRefs, Unf=OtherCon []] $trModule = Module $trModule2_r1zu $trModule4_r1zw

$krep_r1zx :: KindRep [GblId, Caf=NoCafRefs, Unf=OtherCon []] $krep_r1zx = KindRepVar 1#

$krep1_r1zy :: KindRep [GblId, Caf=NoCafRefs, Unf=OtherCon []] $krep1_r1zy = KindRepVar 0#

$tcA1_r1zz :: Addr# [GblId, Caf=NoCafRefs, Unf=OtherCon []] $tcA1_r1zz = "A"#

$tcA2_r1zA :: TrName [GblId, Caf=NoCafRefs, Unf=OtherCon []] $tcA2_r1zA = TrNameS $tcA1_r1zz

$tcA :: TyCon [GblId, Unf=OtherCon []] $tcA = TyCon 16201120719427956884## 13080046616073797921## $trModule $tcA2_r1zA 2# krep$*

$krep2_r1zB :: [KindRep] [GblId, Caf=NoCafRefs, Unf=OtherCon []] $krep2_r1zB = : @ KindRep $krep1_r1zy ([] @ KindRep)

$krep3_r1zC :: [KindRep] [GblId, Caf=NoCafRefs, Unf=OtherCon []] $krep3_r1zC = : @ KindRep $krep_r1zx $krep2_r1zB

$krep4_r1zD :: KindRep [GblId, Unf=OtherCon []] $krep4_r1zD = KindRepTyConApp $tcA $krep3_r1zC

$tc'MkA1_r1zE :: Addr# [GblId, Caf=NoCafRefs, Unf=OtherCon []] $tc'MkA1_r1zE = "'MkA"#

$tc'MkA2_r1zF :: TrName [GblId, Caf=NoCafRefs, Unf=OtherCon []] $tc'MkA2_r1zF = TrNameS $tc'MkA1_r1zE

$tc'MkA :: TyCon [GblId, Unf=OtherCon []] $tc'MkA = TyCon 1695572187443655535## 16213897990811765752## $trModule $tc'MkA2_r1zF 2# $krep4_r1zD

*** End of Offense ***

<no location info>: error: Compilation had errors

*** Exception: ExitFailure 1 }}}

New description: {{{#!hs {-# Language RankNTypes #-} {-# Language GADTs #-} {-# Language TypeApplications #-} {-# Language PolyKinds #-} {-# Options_GHC -dcore-lint #-} import Data.Kind data A :: forall k. Type where MkA :: A @k }}} this cute bug crashes under the [https://phabricator.haskell.org/D5229 visible kind application] diff, produces: {{{ $ ghci -ignore-dot-ghci 545_bug.hs GHCi, version 8.7.20181017: http://www.haskell.org/ghc/ :? for help [1 of 1] Compiling Main ( 545_bug.hs, interpreted ) *** Core Lint errors : in result of Tidy Core *** <no location info>: warning: In the type ‘forall (k :: k_a1xN[sk:1]) k. A’ @ k_a1xN[sk:1] is out of scope *** Offending Program *** $WMkA [InlPrag=INLINE[2]] :: forall (k :: k_a1xN[sk:1]) k. A [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= \ (@ (k_a1y5 :: k_a1xN[sk:1])) (@ k_X1xP) -> MkA @ k_X1xP @ k_a1y5}] $WMkA = \ (@ (k_a1y5 :: k_a1xN[sk:1])) (@ k_X1xP) -> MkA @ k_X1xP @ k_a1y5 $trModule1_r1zb :: Addr# [GblId, Caf=NoCafRefs, Unf=OtherCon []] $trModule1_r1zb = "main"# $trModule2_r1zu :: TrName [GblId, Caf=NoCafRefs, Unf=OtherCon []] $trModule2_r1zu = TrNameS $trModule1_r1zb $trModule3_r1zv :: Addr# [GblId, Caf=NoCafRefs, Unf=OtherCon []] $trModule3_r1zv = "Main"# $trModule4_r1zw :: TrName [GblId, Caf=NoCafRefs, Unf=OtherCon []] $trModule4_r1zw = TrNameS $trModule3_r1zv $trModule :: Module [GblId, Caf=NoCafRefs, Unf=OtherCon []] $trModule = Module $trModule2_r1zu $trModule4_r1zw $krep_r1zx :: KindRep [GblId, Caf=NoCafRefs, Unf=OtherCon []] $krep_r1zx = KindRepVar 1# $krep1_r1zy :: KindRep [GblId, Caf=NoCafRefs, Unf=OtherCon []] $krep1_r1zy = KindRepVar 0# $tcA1_r1zz :: Addr# [GblId, Caf=NoCafRefs, Unf=OtherCon []] $tcA1_r1zz = "A"# $tcA2_r1zA :: TrName [GblId, Caf=NoCafRefs, Unf=OtherCon []] $tcA2_r1zA = TrNameS $tcA1_r1zz $tcA :: TyCon [GblId, Unf=OtherCon []] $tcA = TyCon 16201120719427956884## 13080046616073797921## $trModule $tcA2_r1zA 2# krep$* $krep2_r1zB :: [KindRep] [GblId, Caf=NoCafRefs, Unf=OtherCon []] $krep2_r1zB = : @ KindRep $krep1_r1zy ([] @ KindRep) $krep3_r1zC :: [KindRep] [GblId, Caf=NoCafRefs, Unf=OtherCon []] $krep3_r1zC = : @ KindRep $krep_r1zx $krep2_r1zB $krep4_r1zD :: KindRep [GblId, Unf=OtherCon []] $krep4_r1zD = KindRepTyConApp $tcA $krep3_r1zC $tc'MkA1_r1zE :: Addr# [GblId, Caf=NoCafRefs, Unf=OtherCon []] $tc'MkA1_r1zE = "'MkA"# $tc'MkA2_r1zF :: TrName [GblId, Caf=NoCafRefs, Unf=OtherCon []] $tc'MkA2_r1zF = TrNameS $tc'MkA1_r1zE $tc'MkA :: TyCon [GblId, Unf=OtherCon []] $tc'MkA = TyCon 1695572187443655535## 16213897990811765752## $trModule $tc'MkA2_r1zF 2# $krep4_r1zD *** End of Offense *** <no location info>: error: Compilation had errors *** Exception: ExitFailure 1 }}} Another example that fails {{{#!hs data Kl_kind :: forall (m :: k -> Type). Type where Kl :: k -> Kl_kind @(m :: k -> Type) }}} -- -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15788#comment:2> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

#15788: Core Lint error, from visible kind applications -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.1 Resolution: | Keywords: #12045 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 goldfire): #15743 is solved now. When the kind applications patch is rebased, I expect this will be fixed. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15788#comment:4> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

#15788: Core Lint error, from visible kind applications -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: 8.8.1 Component: Compiler | Version: 8.6.1 Resolution: fixed | Keywords: #12045 Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: | typecheck/should_compile/T15788 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D5229 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/15788#comment:6> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler