Skip to content

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.

Edited by Icelandjack
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information