Skip to content

prefix type-level cons can't be parsed

Whereas other type operators (whether used as type families or used as data constructors) can be safely used in a prefix form, only the type-level cons of the built-in list kind can't be used in a prefix form.

It really is a problem because we don't have any means to express the type-level cons itself in source code. This for example prevents us from writing a generic type-level foldr that takes the built-in list and other similar data types alike.

In a ghci:

> :set -XDataKinds -XTypeOperators
> data Listy a = a ::: Listy a | Nily
> :kind! (:::)
(:::) :: k -> Listy k -> Listy k
= forall (k :: BOX). (':::)
> :kind! (:)

<interactive>:1:2: parse error on input :
Edited by Yusuke Matsushita
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information