happy-subtype-variance-tope-family.rzk

#lang rzk-1

-- PROBE: should be ACCEPTED (paper rules / dRzk).
--
-- Requirement for `g h`:
--   (φ : (t : 2 | TOP) → TOPE) → A  <:  (φ : (t : 2 | t === 0_2) → TOPE) → A
-- By contravariance of Π domains this needs
--   (t : 2 | t === 0_2) → TOPE  <:  (t : 2 | TOP) → TOPE
-- which by S-TopeFam (covariant domains) needs  t === 0_2 ⊢ TOP  — TRUE.
--
-- Semantically: g passes h tope families bounded by t === 0_2; h accepts
-- any tope family whatsoever (bound TOP), so this is safe.
--
-- A checker whose S-TopeFam check ignores the variance flag checks
-- TOP ⊢ t === 0_2 (false) and REJECTS.

#def tope-fam-wrong-reject
  ( A : U)
  ( g : ((φ : (t : 2 | t === 0_2) → TOPE) → A) → A)
  ( h : (φ : (t : 2 | TOP) → TOPE) → A)
  : A
  := g h