LenList.hs

{-# LANGUAGE GADTs #-}
module LenList where

data Zero
data Succ n

data LenList n a where
  Nil :: LenList Zero a
  Cons :: a -> LenList n a -> LenList (Succ n) a

data UnknownLenList a where
  UnknownLenList :: LenList n a -> UnknownLenList a

type Square n a = LenList n (LenList n a)

-- type-checks
sq3 =
  Cons (Cons 'a' . Cons 'b' . Cons 'c' $ Nil) .
  Cons (Cons 'd' . Cons 'e' . Cons 'f' $ Nil) .
  Cons (Cons 'g' . Cons 'h' . Cons 'i' $ Nil) $
  Nil

-- fails to type-check
sq_bad =
  Cons (Cons 'a' . Cons 'b' . Cons 'c' $ Nil) .
  Cons (Cons 'd' . Cons 'e' . Cons 'f' $ Nil) .
  Cons (Cons 'g' . Cons 'h' $ Nil) $
  Nil