Performance mystery w/ unglue

[pi3js2]

Here is a performance mystery seemingly involving unglue. I wonder if I just did something bad?

The mystery is at the bottom. Typechecking the last definitions (commented) takes a very long time (at best -- I haven't seen it finish), and naively this seems surprising. Maybe it makes sense?

import basics;
import bool;

-- Some preliminaries:

Ω (A : U) (a : A) : U := a = a;
Ω² (A : U) (a : A) : U := Ω (Ω A a) refl;

negEquiv : equiv Bool Bool :=
  isoToEquiv Bool Bool negIso;

toPathP (A B : U) (p : A = B)
  (a : A) (b : B) (q : coe 0 1 p a ={_. B} b)
  : a ={i. p i} b :=
  λ i. hcom 1 0
         [ i=0 j. coe j 0 p (coe 0 j p a)
         ; i=1 j. b
         ]
         (coe 1 i p (q i));

-- isPropIsEquiv (copied from new_brunerie_adjusthcom.cctt.opt)
isProp (A : U) : U := (a b : A) → a = b;
isSet (A : U) : U := (a b : A) → isProp (a = b);
lemPropFam (A : U) (P : A → U) (pP : (x : A) → isProp (P x)) (a0 a1 : A)
           (p : a0 = a1) (b0 : P a0) (b1 : P a1) : b0 ={ap P p} b1
  := λ i. pP (p i) (coe 0 i (ap P p) b0) (coe 1 i (ap P p) b1) i;
lemPropFam' (A : I → U) (A-prop : (i : I) → isProp (A i))
  (a0 : A 0) (a1 : A 1) : a0 ={i. A i} a1 :=
  λ i. A-prop i (coe 0 i (i. A i) a0) (coe 1 i (i. A i) a1) i;
isPropIsContr (A : U) : isProp (isContr A)
  := λ c d i.
       (c.2 d.1 i,
        (λ x j.
           hcom 0 1
             [ j=0 _. c.2 d.1 i
             ; j=1 _. x
             ; i=0 i. hcom i 1
                        [ j=0 j. c.2 c.1 j
                        ; j=1 j. c.2 x j
                        ]
                        (c.2 (c.2 x j) i)
             ; i=1 i. hcom i 1
                        [ j=0 j. c.2 d.1 j
                        ; j=1 j. c.2 x j
                        ]
                        (c.2 (d.2 x j) i)
             ]
             (hcom 0 1
                [ j=0 j. c.2 (c.2 d.1 i) j
                ; j=1 j. c.2 x j
                ]
                c.1)));
isPropPi (A : U) (B : A → U) (pr : (x : A) → isProp (B x))
  : isProp ((x : A) → B x)
  := λ f g i x. pr x (f x) (g x) i;
isPropHasContrFibers (A B : U) (f : A → B) : isProp (hasContrFibers A B f)
  := isPropPi B (λ b. isContr (fiber A B f b))
       (λ b. isPropIsContr (fiber A B f b));
isPropIsEquiv (A B : U) (f : A → B) : isProp (isEquiv A B f)
  := λ e1 e2 i.
       hcom 0 1
         [ i=0. isEquivRetractContrFibers A B f e1
         ; i=1. isEquivRetractContrFibers A B f e2
         ]
         (contrFibersToIsEquiv A B f
           (isPropHasContrFibers A B f
             (isEquivToContrFibers A B f e1)
             (isEquivToContrFibers A B f e2)
             i));
-- end isPropIsEquiv copy

equivEq (A B : U) (f g : equiv A B) (h : (x : A) → f.1 x = g.1 x) : f = g :=
  λ i. ((λ x. h x i),
        lemPropFam (A → B) (isEquiv A B)
          (isPropIsEquiv A B)
          f.1 g.1 (λ i x. h x i)
          f.2 g.2 i);



-- Example starts here:

higher inductive S² :=
  baseS²
| surfS² (i j : I)
    [ i=0. baseS²
    ; i=1. baseS²
    ; j=0. baseS²
    ; j=1. baseS²
    ];

recS² (A : U) (x : A) (p : Ω² A x) : S² → A :=
  λ [ baseS². x
    ; surfS² i j. p i j
    ];

higher inductive RP² :=
  baseRP²
| loopRP² (i : I)
    [ i=0. baseRP²
    ; i=1. baseRP²
    ]
| surfRP² (i j : I)
    [ i=0. baseRP²
    ; i=1. loopRP² j
    ; j=0. loopRP² i
    ; j=1. baseRP²
    ];

problem1 : refl ={i. negEq i = Bool} negEq :=
  let f0' : negEquiv ={_. equiv Bool Bool} negEquiv :=
    refl;

  let f2' : negEquiv ={j. equiv (negEq j) Bool} idEquiv Bool :=
    toPathP (equiv Bool Bool) (equiv Bool Bool)
      (λ i. equiv (negEq i) Bool)
      negEquiv (idEquiv Bool)
      (equivEq Bool Bool
         (coe 0 1 (i. equiv (negEq i) Bool) negEquiv)
         (idEquiv Bool)
         (λ [ false. refl; true. refl ]));

  let f3' : idEquiv Bool ={i. equiv (negEq i) Bool} negEquiv :=
    toPathP (equiv Bool Bool) (equiv Bool Bool)
      (λ i. equiv (negEq i) Bool)
      (idEquiv Bool) negEquiv
      (equivEq Bool Bool
         (coe 0 1 (i. equiv (negEq i) Bool) (idEquiv Bool))
         negEquiv
         (λ _. refl));

  λ i j. Glue Bool
           [ i=0. (Bool, f0' j)
           ; i=1. (negEq j, f3' j)
           ; j=0. (negEq i, f2' i)
           ; j=1. (Bool, f0' i)
           ];

doubleCover : RP² → U :=
  λ[ baseRP². Bool
   ; loopRP² i. negEq i
   ; surfRP² i j. problem1 i j
   ];

side : (i j : I) → doubleCover (surfRP² i j) → Bool :=
  λ i j x. unglue x;

surf-if : Bool → Ω² S² baseS² :=
  λ [ false. refl
    ; true. λ i j. surfS² i j
    ];


-- These all normalize to λ _ x. baseS²:

yikes-i0 : (j : I) → doubleCover (surfRP² 0 j) → S² :=
  λ j x. surf-if (side 0 j x) 0 j;

yikes-i1 : (j : I) → doubleCover (surfRP² 1 j) → S² :=
  λ j x. surf-if (side 1 j x) 1 j;

yikes-j0 : (i : I) → doubleCover (surfRP² i 0) → S² :=
  λ i x. surf-if (side i 0 x) i 0;

yikes-j1 : (i : I) → doubleCover (surfRP² i 1) → S² :=
  λ i x. surf-if (side i 1 x) i 1;

-- so far everything checks fine, but uncommenting any one of these
-- makes checking take forever (?)

-- yikes1 : (i j : I) → doubleCover (surfRP² i j) → S² :=
--   λ i j x. surf-if (side i j x) i j;

-- yikes2 : (λ _ _. baseS²) ={i. (λ _. baseS²) ={j. doubleCover (surfRP² i j) → S²} (λ _. baseS²)} (λ _ _. baseS²) :=
--   λ i j x. surf-if (side i j x) i j;

-- yikes3 : (λ j. yikes-i0 j) ={i. yikes-j0 i ={j. doubleCover (surfRP² i j) → S²} yikes-j1 i} (λ j. yikes-i1 j) :=
--   λ i j x. surf-if (side i j x) i j;

[AndrasKovacs]

Yes, just eyeballing this, it is suspicious. I'll try to look at it. Maybe the approximate conversion is not firing enough to shortcut doubleCover (surfRP² i j) =? doubleCover (surfRP² i j).

[pi3js2]

Thanks, glad my eyeballs work :)

Just for context:

I was working on this example to try to run some closed computations.

I got the computations working in Agda now, using a very similar example.

In Agda, checking some things is a bit slow, but especially the closed computations (pi2RP2 -> Z) are slow. So maybe this could be another useful comparison someday.