☣️ Issue dispatching hcom for sigma types

[TOTBWF]

trafficstars

When messing around with some ideas that @cangiuli had regarding records, I came across the following crash:

import prelude
import hlevel

-- Equivalences.
def fiber (A : type) (B : type)  (f : A → B) (b : B) : type := (a : A) × path B {f a} b

def is-equiv (A : type) (B : type) (f : A → B) : type := (b : B) → is-contr {fiber A B f b}

def equiv (A : type) (B : type) : type := (f : A → B) × is-equiv A B f

def equiv/id (A : type) : equiv A A :=
  [ x => x,
    x => [
      [ x , i => x ],
      fib i =>
        let aux : 𝕀 → A := j =>
	  hcom A 1 j {∂ i} {j _ => [
	    | j=1 ∨ i=0 => x
	    | i=1 => {snd fib} j
	    ]
	  }
        in [ aux 0, aux ]
    ]
  ]

#normalize {equiv/id {(x : type) × x}}

This crashes with:

[DEBUG] dispatch_rigid_hcom: lam[clo[lam[<anon>, el/out[ap[ap[var[2], var[1]], var[0]]]] ; [
[ 
] ; [ <let-sym> ]]]]
Core.Semantics.NbeFailed("Invalid arguments to dispatch_rigid_hcom")

I suspect that there's something fishy going on here with hcom_sg... It's worth noting this is fine for say, (x : type) × nat

[TOTBWF]

Here's a more minimal repo:

def test : (x : type) × x :=
  hcom {(x : type) × x} 0 1 ⊥ {j _ =>  [ j=0 => [ nat, 4 ] ] }

[TOTBWF]

After a bit of poking around, it seems that the crash happens when we try to evaluate the cap of the Box by test...

[jonsterling]

could it be caused by #288 ? LOL

[TOTBWF]

Oh that could totally be it!