[ You can consult this new issue online at [bugit#4](http://faina.iro.umontreal.ca/bugit.cgi?rep=typer&issue=f6e38e6eb5dba869a540...). ] ## Author: Stefan Monnier <monnier@iro.umontreal.ca> ## Date: Wed Aug 31 20:55:51 2016 -0400 As the title say: f = lambda (x : Type) ≡> x; will happily be accepted by the elaboration phase, and then crash at run-time.