Crash related to equation compiler(?)

Reported by @kodyvajjha on Zulip. The following code crashes both 3.4.2 and the latest 3.5.0c nightly ("nightly-2019-05-17"):

universe u

open nat

variable {α : Type u}
def vec : Type u → ℕ → Type*
| A 0 := punit
| A (succ k) := A × vec A k

inductive dfin : ℕ → Type
| fz {n} : dfin (n+1)
| fs {n} : dfin n → dfin (n+1)

def kth_projn : Π n, vec α n → dfin n → α
| (_) x dfin.fz := x.fst -- crashes lean
| (succ n) (x,xs) (dfin.fs k) := kth_projn n xs k

Curiously, it does not crash when run in the web editor, instead returns the following error message:

equation compiler failed (use 'set_option trace.eqn_compiler.elim_match true' for additional details)
nested exception message:
cases tactic failed, it is not applicable to the given hypothesis

Reproduce the supplied vec/dfin/kth_projn example on Lean 3.4.2 and nightly-2019-05-17, comparing the crash with the web editor's equation compiler error. Start at the equation compiler and enable the mentioned trace.eqn_compiler.elim_match option for diagnostics. Done means the example no longer crashes and produces a handled result or diagnostic.