ill-data-negative.rzk

#lang rzk-1

-- The declared type occurs in a domain: not strictly positive.
#data bad := c (f : bad → bad)