How to get this type checked?

[refparo]

prim I
prim left
prim right
prim arcoe
struct Path (A : I -> Type) (a : A left) (b : A right) : Type
 | at (i : I) : A i {
   | left => a
   | right => b
 }
def path {A : I -> Type} (p : Pi (i : I) -> A i)
  => new Path A (p left) (p right) { | at i => p i }
def `=` Eq {A : Type} (a b : A) : Type => Path (\ i => A) a b
def idp {A : Type} (a : A) : a = a => path (\ i => a)

bind application tighter =

open data Unit : Set | unit

def foo
  : Path (λ i ⇒ Unit) unit (arcoe (λ i ⇒ (idp Unit).at i) unit right)
  => idp unit

[ice1000]

Simplified repro:

prim I
prim left
prim right
prim arcoe
struct Path (A : I -> Type) (a : A left) (b : A right) : Type
 | at (i : I) : A i {
   | left => a
   | right => b
 }
def path {A : I -> Type} (p : Pi (i : I) -> A i)
  => new Path A (p left) (p right) { | at i => p i }
def `=` Eq {A : Type} (a b : A) : Type => Path (\ i => A) a b
def idp {A : Type} (a : A) : a = a => path (\ i => a)

bind application tighter =

open data Unit : Set | unit

def foo
  : unit = arcoe (idp Unit).at unit right
  => idp unit

[ice1000]

This is a bug. Fixed in d6c7234. Sorry for the late reply.

For apology, here's a good song https://www.youtube.com/watch?v=4bcnO3VQ_fc I was listening to this while fixing the bug