[Haskell-cafe] heterogeneous container smart constructor question

[Zoran Bošnjak]

Dear haskellers,
I am trying to add some type safety to the program in the following situation:

There are some distinct 'Item t' types which come in groups. That is: 'EList' container can contain either:
- items 0,1
- items 0,1,2,3
- items 0,1,2,3,4,5,6

All other combinations (like items 0,1,2) are invalid and shall be rejected by compiler. 
The 'EList' implementation (see below) seems to have this property.

In addition, I would like to define a smart constructor (mkEList), to simplify EList construction from some linear (no groups) IList type. In other words, mkEList shall slice IList to proper groups. I am aware that I need to use a type class / type families for this. I have tried several approaches, but ghc was not happy with any.

What is the correct implementation of mkEList?

Here is a sample code and the intended usage:

-- (sample build-test.hs)
import GHC.TypeLits

data Item (t :: Nat) = Item

-- List/group of items
data IList (ts :: [Nat]) where
    INil  :: IList '[]
    ICons :: Item t -> IList ts -> IList (t ': ts)

nil :: IList '[]
nil = INil

infixr 5 &:
(&:) :: Item t -> IList ts -> IList (t : ts)
(&:) = ICons

-- Extended list of groups
data EList (ts :: [Nat]) (tss :: [[Nat]]) where
    EList :: IList ts1 -> Maybe (EList ts2 tss) -> EList ts1 (ts2 ': tss)

instance Eq (EList ts tss)

-- Manual test

type T1 = '[0, 1]
type T2 = '[ '[2, 3], '[4, 5, 6], '[] ]

test1 :: EList T1 T2
test1 = EList (Item @0 &: Item @1 &: nil) Nothing

test2 :: EList T1 T2
test2 = EList (Item @0 &: Item @1 &: nil)
    (Just (EList (Item @2 &: Item @3 &: nil) Nothing))

test3 :: EList T1 T2
test3 = EList (Item @0 &: Item @1 &: nil)
    (Just (EList (Item @2 &: Item @3 &: nil)
        (Just (EList (Item @4 &: Item @5 &: Item @6 &: nil) Nothing))))

-- Intended usage

-- | Helper function or class method :: IList ? -> EList ? ?
mkEList :: a
mkEList = undefined

el1 :: EList T1 T2
el1 = mkEList
    ( Item @0 
   &: Item @1 
   &: nil) 

el2 :: EList T1 T2
el2 = mkEList
    ( Item @0 
   &: Item @1 
   &: Item @2 
   &: Item @3
   &: nil)

el3 :: EList T1 T2
el3 = mkEList
    ( Item @0 
   &: Item @1 
   &: Item @2 
   &: Item @3
   &: Item @4 
   &: Item @5 
   &: Item @6
   &: nil)

check :: Bool -- expecting True
check = and [el1 == test1, el2 == test2, el3 == test3]
-- (end of sample)

regards,
Zoran