Function bad_forall_sort_bad

crates/kernel/src/tutorial/basic.rs:476–547

()

  /// The innermost domain `bvar0` refers to a variable of type Prop, not a Sort.
  #[test]
  fn bad_forall_sort_bad() {
    let mut env = KEnv::<Meta>::new();
    // id : {α : Sort u} → α → α, simplified as Type → Type → Type... no.
    // id.{2} : Sort 2 → Sort 2 := fun x => x
    // id.{2} (Sort 1) (Sort 0) = Sort 0 = Prop
    // Let's use: id_univ2 : Sort 2 → Sort 2 := fun x => x
    let (id2_id, id2_c) = mk_defn(
      "id2",
      0,
      vec![],
      pi(sort(usucc(usucc(uzero()))), sort(usucc(usucc(uzero())))), // Sort 2 → Sort 2
      nlam("x", sort(usucc(usucc(uzero()))), var(0)),
      ReducibilityHints::Abbrev,
    );
    env.insert(id2_id, id2_c);

    // forallSortBad : Prop := ∀ (_ : id2 (Sort 1) applied to Sort 0... )
    // Actually simpler: the domain is (id2 Prop) which reduces to Prop.
    // Then the next domain is bvar(0) which is a Prop value, NOT a Sort.
    //
    // value = ∀ (_ : id2 Prop), ∀ (_ : bvar0), bvar1
    // After WHNF of `id2 Prop` → Prop. Then domain 2 is bvar0 : Prop (not a Sort).
    // Wait, id2 : Sort 2 → Sort 2. Prop = Sort 0 : Sort 1, not Sort 2.
    // So id2 Prop would fail (Prop : Sort 1, not Sort 2).
    //
    // Let's use a simpler approach: id at level 1.
    // id1 : Sort 1 → Sort 1 := fun x => x
    // id1 Prop = Prop (since Prop : Sort 1)
    let (id1_id, id1_c) = mk_defn(
      "id1",
      0,
      vec![],
      pi(sort(usucc(uzero())), sort(usucc(uzero()))), // Sort 1 → Sort 1
      nlam("x", sort(usucc(uzero())), var(0)),
      ReducibilityHints::Abbrev,
    );
    env.insert(id1_id, id1_c);

    // value = ∀ (_ : id1 Prop), ∀ (_ : bvar0), bvar1
    // id1 Prop reduces to Prop (a Sort). First forall OK.
    // Second forall: domain = bvar0 (the variable of type Prop). Not a Sort!
    let id1_prop = app(cnst("id1", &[]), sort0());
    // ∀ (_ : id1 Prop), ∀ (_ : bvar0), ∀ (_ : bvar0), bvar1
    // depth 1: _1 : Prop (from id1 Prop)
    // depth 2: _2 : _1 (var(0) at depth 1 = _1, a Prop variable). _2 has type _1 : Prop.
    // depth 3: domain = bvar0 = _2 (var(0) at depth 2). _2 has type _1 (Prop value).
    //   infer(_2) = _1. ensure_sort(_1) must fail: _1 is a Prop variable, not a Sort.
    let value = npi(
      "_",
      id1_prop, // ∀ _1 : id1 Prop, ...
      npi(
        "_",
        var(0), // ∀ _2 : _1, ... (_1 : Prop, so _2 has a Prop-typed type)
        npi(
          "_",
          var(0), // ∀ _3 : _2, ... — _2's type is _1 (a Prop var, NOT Sort)
          var(1),
        ),