type checker loop in pushCoe #38

New Issue

Closed

opened 2023-12-20 16:03:25 -05:00 by rhi · 2 comments

rhi commented

2023-12-20 16:03:25 -05:00

Owner

def revive0 : 0.(A : ★) → 0.[0.A] → [0.A] =
  λ A s ⇒ [case s return A of { [s] ⇒ s }]

def0 boxω-inj : (A : ★) → (x y : A) → [x] ≡ [y] : [ω.A] → x ≡ y : A =
  λ A x y xy ⇒ δ 𝑖 ⇒ case xy @𝑖 return A of { [x] ⇒ x }

def0 Irr1 : (A : ★) → (A → ★) → ★ =
  λ A P ⇒ (x : A) → (p q : P x) → p ≡ q : P x

def0 Sub : (A : ★) → (P : A → ★) → ★ =
  λ A P ⇒ (x : A) × [0. P x]

def0 SubDup : (A : ★) → (P : A → ★) → Sub A P → ★ =
  λ A P s ⇒ (x! : [ω.A]) × [0. x! ≡ [fst s] : [ω.A]]

def0 Dup : (A : ★) → A → ★ =
  λ A x ⇒ (x! : [ω.A]) × [0. x! ≡ [x] : [ω.A]]


-- type checker loop?????????????????? :(
def subdup-to-dup :
    0.(A : ★) → 0.(P : A → ★) → 0.(Irr1 A P) →
    0.(s : Sub A P) → SubDup A P s → Dup (Sub A P) s =
  λ A P pirr s sd ⇒
    case sd return Dup (Sub A P) s of { (sω, ss0) ⇒
      case sω
      return sω' ⇒ 0.(sω' ≡ [fst s] : [ω.A]) → Dup (Sub A P) s
      of { [s!] ⇒ λ ss' ⇒
        let ω.p  : [0.P (fst s)] = revive0 (P (fst s)) (snd s);
            0.ss : s! ≡ fst s : A = boxω-inj A s! (fst s) ss';
            0.pp : [0.P s!] ≡ [0.P (fst s)] : ★ = (δ 𝑖 ⇒ [0.P (ss @𝑖)]) in
        ([(s!, coe (𝑖 ⇒ pp @𝑖) @1 @0 p)],
         [δ 𝑗 ⇒ [(ss @𝑗, coe (𝑖 ⇒ pp @𝑖) @1 @𝑗 p)]]) -- ⇐ maybe here?
      } (δ _ ⇒ sω)
    }

-- not here tho
def coe2 : 0.(A B : ★) → 0.(AB : A ≡ B : ★) → (x : A) →
           (x' : B) × [0. Eq (𝑖 ⇒ AB @𝑖) x x'] =
  λ A B AB x ⇒ (coe (𝑖 ⇒ AB @𝑖) x, [δ 𝑗 ⇒ coe (𝑖 ⇒ AB @𝑖) @0 @𝑗 x])

hælp

``` def revive0 : 0.(A : ★) → 0.[0.A] → [0.A] = λ A s ⇒ [case s return A of { [s] ⇒ s }] def0 boxω-inj : (A : ★) → (x y : A) → [x] ≡ [y] : [ω.A] → x ≡ y : A = λ A x y xy ⇒ δ 𝑖 ⇒ case xy @𝑖 return A of { [x] ⇒ x } def0 Irr1 : (A : ★) → (A → ★) → ★ = λ A P ⇒ (x : A) → (p q : P x) → p ≡ q : P x def0 Sub : (A : ★) → (P : A → ★) → ★ = λ A P ⇒ (x : A) × [0. P x] def0 SubDup : (A : ★) → (P : A → ★) → Sub A P → ★ = λ A P s ⇒ (x! : [ω.A]) × [0. x! ≡ [fst s] : [ω.A]] def0 Dup : (A : ★) → A → ★ = λ A x ⇒ (x! : [ω.A]) × [0. x! ≡ [x] : [ω.A]] -- type checker loop?????????????????? :( def subdup-to-dup : 0.(A : ★) → 0.(P : A → ★) → 0.(Irr1 A P) → 0.(s : Sub A P) → SubDup A P s → Dup (Sub A P) s = λ A P pirr s sd ⇒ case sd return Dup (Sub A P) s of { (sω, ss0) ⇒ case sω return sω' ⇒ 0.(sω' ≡ [fst s] : [ω.A]) → Dup (Sub A P) s of { [s!] ⇒ λ ss' ⇒ let ω.p : [0.P (fst s)] = revive0 (P (fst s)) (snd s); 0.ss : s! ≡ fst s : A = boxω-inj A s! (fst s) ss'; 0.pp : [0.P s!] ≡ [0.P (fst s)] : ★ = (δ 𝑖 ⇒ [0.P (ss @𝑖)]) in ([(s!, coe (𝑖 ⇒ pp @𝑖) @1 @0 p)], [δ 𝑗 ⇒ [(ss @𝑗, coe (𝑖 ⇒ pp @𝑖) @1 @𝑗 p)]]) -- ⇐ maybe here? } (δ _ ⇒ sω) } -- not here tho def coe2 : 0.(A B : ★) → 0.(AB : A ≡ B : ★) → (x : A) → (x' : B) × [0. Eq (𝑖 ⇒ AB @𝑖) x x'] = λ A B AB x ⇒ (coe (𝑖 ⇒ AB @𝑖) x, [δ 𝑗 ⇒ coe (𝑖 ⇒ AB @𝑖) @0 @𝑗 x]) ``` hælp

rhi added the

bug

label 2023-12-20 16:03:25 -05:00

rhi commented

2024-01-30 15:39:38 -05:00

Author

Owner

i found it

it's the η expansion for boxes, in Q.Whnf.Coercion.pushCoe

in the function η expansions, you have something like

(coe (𝑖 ⇒ π.(x : A) → B) @p @q s)
  ⇝
(λ y ⇒ (coe (𝑖 ⇒ π.(x : A) → B) @p @q s) y) ∷ (π.(x : A) → B)‹q/𝑖›
 ‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾

where the underlined thing is in whnf. for boxes it keeps "η-expanding" the head forever

**i found it** it's the η expansion for boxes, in `Q.Whnf.Coercion.pushCoe` in the function η expansions, you have something like ``` (coe (𝑖 ⇒ π.(x : A) → B) @p @q s) ⇝ (λ y ⇒ (coe (𝑖 ⇒ π.(x : A) → B) @p @q s) y) ∷ (π.(x : A) → B)‹q/𝑖› ‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾ ``` where the underlined thing is in whnf. for boxes it keeps "η-expanding" the head forever

rhi referenced this issue from a commit

2024-02-10 04:07:36 -05:00

fix typechecker loop when coercing boxes

rhi closed this issue

2024-02-10 04:07:36 -05:00

rhi changed title from ~~type checker loop~~ to type checker loop in pushCoe

2024-02-13 19:45:00 -05:00

rhi commented

2024-02-13 19:45:24 -05:00

Author

Owner

actually no the Π/Eq rules have the same problem after all lol