Implement pruning to fix this example by Hoshino

[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)

Originally posted by @HoshinoTented in #768