ill-subtype-variance-restriction-faces.rzk

#lang rzk-1

-- PROBE: should be REJECTED (paper rules / dRzk).
--
-- Requirement for `g k`:
--   (x : A [t === 0_2 |-> a, t === 1_2 |-> b]) → A
--     <:  (x : A [t === 0_2 |-> a]) → A
-- By contravariance of Π domains this needs
--   A [t === 0_2 |-> a]  <:  A [t === 0_2 |-> a, t === 1_2 |-> b]
-- which by S-Restr fails: the face t === 1_2 |-> b of the supertype is
-- not covered by the subtype's faces.
--
-- Semantically: g feeds k elements that promise nothing at t === 1_2;
-- k's type entitles it to compute x ≡ b there.
--
-- A checker whose restriction-face coverage check ignores the variance
-- flag checks the converse inclusion (true) and ACCEPTS.

#def restr-wrong-accept
  ( A : U)
  ( a : A)
  ( b : A)
  ( t : 2)
  ( g : ((x : A [t === 0_2 |-> a]) → A) → A)
  ( k : (x : A [t === 0_2 |-> a, t === 1_2 |-> b]) → A)
  : A
  := g k