[GHC] #14162: Core Lint error
#14162: Core Lint error -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Keywords: TypeInType | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- {{{#!hs {-# Options_GHC -dcore-lint #-} {-# Language TypeOperators, KindSignatures, DataKinds, PolyKinds, TypeFamilies, GADTs, TypeInType #-} import Data.Kind data family Sing (a :: k) data SubList :: [a] -> [a] -> Type where SubNil :: SubList '[] '[] Keep :: SubList xs ys -> SubList (x ': xs) (x ': ys) Drop :: SubList xs ys -> SubList xs (x ': ys) data instance Sing (x :: SubList ys xs) where SSubNil :: Sing SubNil SKeep :: Sing x -> Sing (Keep x) SDrop :: Sing x -> Sing (Drop x) }}} running it gives a massive core lint error, attached as a `lint.log`. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14162> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14162: Core Lint error -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.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 Iceland_jack): * Attachment "lint.log" added. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14162> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14162: Core Lint error -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.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 Iceland_jack): From trying to compile Richard's [https://github.com/goldfirere/effects/blob/master/Effects.hs Effects.hs] with `-dcore-lint`. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14162#comment:1> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14162: Core Lint error -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.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: | -------------------------------------+------------------------------------- Description changed by Iceland_jack: Old description:
{{{#!hs {-# Options_GHC -dcore-lint #-}
{-# Language TypeOperators, KindSignatures, DataKinds, PolyKinds, TypeFamilies, GADTs, TypeInType #-}
import Data.Kind
data family Sing (a :: k)
data SubList :: [a] -> [a] -> Type where SubNil :: SubList '[] '[] Keep :: SubList xs ys -> SubList (x ': xs) (x ': ys) Drop :: SubList xs ys -> SubList xs (x ': ys)
data instance Sing (x :: SubList ys xs) where SSubNil :: Sing SubNil SKeep :: Sing x -> Sing (Keep x) SDrop :: Sing x -> Sing (Drop x) }}}
running it gives a massive core lint error, attached as a `lint.log`.
New description: {{{#!hs {-# Options_GHC -dcore-lint #-} {-# Language TypeOperators, KindSignatures, DataKinds, PolyKinds, TypeFamilies, GADTs, TypeInType #-} import Data.Kind data family Sing (a :: k) data SubList :: [a] -> [a] -> Type where SubNil :: SubList '[] '[] Keep :: SubList xs ys -> SubList (x ': xs) (x ': ys) Drop :: SubList xs ys -> SubList xs (x ': ys) data instance Sing (x :: SubList ys xs) where SSubNil :: Sing SubNil SKeep :: Sing x -> Sing (Keep x) SDrop :: Sing x -> Sing (Drop x) }}} running it gives a massive core lint error, attached as `lint.log`. -- -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14162#comment:2> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14162: Core Lint error -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.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 simonpj): Here's a simpler version {{{ {-# Language TypeOperators, KindSignatures, DataKinds, PolyKinds, TypeFamilies, GADTs, TypeInType #-} module T14162 where import Data.Kind data SubList :: Maybe a -> Type where SubNil :: SubList 'Nothing data family Sing (a :: k) data instance Sing (x :: SubList ys) where SSubNil :: Sing SubNil }}} There's an ASSERT error in `substTy` too, if you compile with a -DDEBUG compiler -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14162#comment:3> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14162: Core Lint error -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.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 simonpj): But the actual error is somewhere in the unfolding wrapper for `SSubNil`, which is injected by `CorePrep` and looks like this {{{ SSubNil :: forall a (ys :: Maybe a) (x :: SubList a ys). ((ys :: Maybe a) ~# ('Nothing a :: Maybe a), (x :: SubList a ys) ~# ('SubNil a :: SubList a ('Nothing a))) => R:SingSubListx a ys x [GblId[DataCon], Arity=2, Caf=NoCafRefs, Str=<L,U><L,U>m, Unf=OtherCon []] SSubNil = \ (@ a_aSK) (@ (ys_aRV :: Maybe a_aSK)) (@ (x_aRW :: SubList a_aSK ys_aRV)) (eta_B2 :: (ys_aRV :: Maybe a_aSK) ~# ('Nothing a_aSK :: Maybe a_aSK)) (eta_B1 :: (x_aRW :: SubList a_aSK ys_aRV) ~# ('SubNil a_aSK :: SubList a_aSK ('Nothing a_aSK))) -> SSubNil @ a_aSK @ ys_aRV @ x_aRW @~ (eta_B2 :: (ys_aRV :: Maybe a_aSK) ~# ('Nothing a_aSK :: Maybe a_aSK)) @~ (eta_B1 :: (x_aRW :: SubList a_aSK ys_aRV) ~# ('SubNil a_aSK :: SubList a_aSK ('Nothing a_aSK))) }}} Lint says {{{ *** Core Lint errors : in result of CorePrep *** <no location info>: warning: In the type ‘forall a (ys :: Maybe a) (x :: SubList a ys). ((ys :: Maybe a) ~# ('Nothing a :: Maybe a), (x :: SubList a ys) ~# ('SubNil a :: SubList a ('Nothing a))) => R:SingSubListx a ys x’ Kind application error in type ‘SubList a_aSK ys_aRV’ Function kind = forall {a}. Maybe a -> * Arg kinds = [(a_aSK, *), (ys_aRV, Maybe a_aSv)] }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14162#comment:4> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14162: Core Lint error -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.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:"3a27e34f7a59a30f91fad9dd2ca194acdb1bcb1a/ghc" 3a27e34/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="3a27e34f7a59a30f91fad9dd2ca194acdb1bcb1a" Fix subtle bug in TcTyClsDecls.mkGADTVars This bug was revealed by Trac #14162. In a GADT-style data-family instance we ended up a data constructor whose type mentioned an out-of-scope variable. (This variable was in the kind of a variable in the kind of a variable.) Only Lint complained about this (actually only when the data constructor was injected into the bindings by CorePrep). So it doesn't matter much -- but it's a solid bug and might bite us some day. It took me quite a while to unravel because the test case was itself quite tricky. But the fix is easy; just add a missing binding to the substitution we are building up. It's in the regrettably-subtle mkGADTVars function. }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14162#comment:5> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14162: Core Lint error -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: merge Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: indexed- | types/should_compile/T14162 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * status: new => merge * testcase: => indexed-types/should_compile/T14162 Comment: I believe this fix is also on Richards `wip/rae` branch. Worth merging to 8.2 I think, because it's a simple, local change. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14162#comment:6> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14162: Core Lint error -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: merge Priority: normal | Milestone: 8.2.2 Component: Compiler | Version: 8.2.1 Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: indexed- | types/should_compile/T14162 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * milestone: => 8.2.2 -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14162#comment:7> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14162: Core Lint error -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: 8.2.2 Component: Compiler | Version: 8.2.1 Resolution: fixed | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: indexed- | types/should_compile/T14162 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by bgamari): * status: merge => closed * resolution: => fixed Comment: Merged to `ghc-8.2` as 8fda8aded0d2194bddbaaed43256d0e3d0632fe2. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14162#comment:8> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
participants (1)
-
GHC