
#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