What is this Haskell Syntax (type level operators?)

Question

What does '[] or ': signify in Haskell code? Some examples -

Example 1:

data OrderPacket replies where
  NoOrders :: OrderPacket '[]

Example 2:

data Elem :: [a] -> a -> * where
  EZ :: Elem (x ': xs) x

Answer 1

From the Haskell user guide section on Promoted list and tuple lists:

With -XDataKinds, Haskell's list and tuple types are natively promoted to kinds, and enjoy the same convenient syntax at the type level, albeit prefixed with a quote:

data HList :: [*] -> * where
  HNil  :: HList '[]
  HCons :: a -> HList t -> HList (a ': t)

data Tuple :: (*,*) -> * where
  Tuple :: a -> b -> Tuple '(a,b)

foo0 :: HList '[]
foo0 = HNil

foo1 :: HList '[Int]
foo1 = HCons (3::Int) HNil

foo2 :: HList [Int, Bool]
foo2 = ...

(Note: the declaration for HCons also requires -XTypeOperators because of infix type operator (:').) For type-level lists of two or more elements, such as the signature of foo2 above, the quote may be omitted because the meaning is unambiguous. But for lists of one or zero elements (as in foo0 and foo1), the quote is required, because the types [] and [Int] have existing meanings in Haskell.

So basically it is the same syntax prefixed with a single quote but which operates at kind level. Some playup using ghci with the above code:

λ> :t HNil
HNil :: HList '[]
λ> :t HCons
HCons :: a -> HList t -> HList (a : t)
λ> let x = 3 `HCons` HNil
λ> :t x
x :: Num a => HList '[a]
λ> let x = Tuple 3 "spj"
λ> :t x
x :: Num a => Tuple '(a, [Char])