[GHC] #14162: Core Lint error

[GHC]

#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