Core Lint error
{-# 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
.