This is one of the ergonomic reasons I prefer using Lean over Coq when playing around with dependent types:
Quote Tweet
I wish Haskell supported constructors namespaced by type so that we didn't need to add prefixes to constructor names to disambiguate them