happy-data-large-warning.rzk

#lang rzk-1

-- Exercise standalone diagnostics independently of the safe-mode bundle.
#set-option "rstt-safe" = "off"

-- A constructor field storing a universe makes the type large: under
-- type-in-type this is a paradox amplifier, so the declaration is accepted
-- with a warning (and will be rejected under safe mode).
#data large := box (X : U)

-- a small declaration alongside stays warning-free
#data unit-like := point