IE

[ice1000]

def overlap ++-assoc (xs : Vec A n) (ys : Vec A m) (zs : Vec A o)
  : Path (\i => Vec A (+-assoc i)) ((xs ++ ys) ++ zs) (xs ++ (ys ++ zs))
| vnil, ys, zs => idp
| xs, vnil, zs => idp
| xs, ys, vnil => idp
| x :> xs, ys, zs => pmapd (\i => x :>) (++-assoc xs ys zs)

Internal Exception

[HoshinoTented]

Smaller code:

open data Unit | unit
open data Nat | O | S Nat
open data SomeDT Nat
| m => someDT
def how' {m : Nat} (a : Nat) (b : SomeDT m) : Nat => 0
def what {A : Nat -> Type} (B : Fn (n : Nat) -> A n -> Nat) : Unit => unit
def boom => what (fn n => fn m => how' 0 m)

[ice1000]

Smaller code:

open data Unit | unit
open data Nat | O | S Nat
open data SomeDT Nat
| m => someDT
def how' {m : Nat} (a : Nat) (b : SomeDT m) : Nat => 0
def what {A : Nat -> Type} (B : Fn (n : Nat) -> A n -> Nat) : Unit => unit
def boom => what (fn n => fn m => how' 0 m)

This is fixed in the locally nameless version of Aya