What is '[] and ': in Haskell?

DataKinds allows one to use term-level constructors at the type level.

After

data T = A | B | C

one can write types indexed by a value of T

data U (t :: T) = ...
foo :: U A -> U B -> ...

Here, however, A and B are used as types, not as values. Hence, they have to be "promoted" using a quote:

data U (t :: T) = ...
foo :: U 'A -> U 'B -> ...

The same happens with the familiar list syntax. '[] is an empty list, promoted at the type level. '[a,b,c] is the same as a ': b ': c ': '[], a list promoted at the type level.

type           :: kind
'[]            :: [k]   -- polykinded! works for any kind k
'[ 'A, 'B, 'C] :: [T]   -- mind the spaces, we do not want the char '['
'A ': '[]      :: [T]
'[ Int, Bool ] :: [*]   -- a list of types
'[ Int ]       :: [*]   -- a list of types with only one element
[Int]          :: *     -- a type "list of Int"

Note the last two cases, where the quote disambiguates the syntax.