Elaboration of function types

Stream: general

[Wojciech Nawrocki]

Is this behaviour of the elaborator expected/necessary or could it be improved so that the last two cases are also inferrable?

#check ((λ n: ℕ, n): _) -- good
#check ((λ n: ℕ, n): (_ → ℕ)) -- good
#check ((λ n: ℕ, n): (ℕ → _)) -- failed, sort expected ?m_1[a]
#check ((λ n: ℕ, n): (_ → _)) -- failed, sort expected ?m_1[a]

[Mario Carneiro]

arguably this shouldn't happen with the arrow, which is supposed to be nondependent, but the parser turns the later two into \forall _x:nat, _ which produces a metavariable _x : nat |- ?m_1 and then the typing forces it to unify ?m_1[n] =?= nat, and it doesn't like these sorts of unification problems so it delays, hoping that ?m_1 will be solved directly.