[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=
#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
#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