Wojciech Nawrocki (Jun 18 2019 at 12:36):
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 (Jun 18 2019 at 12:40):
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.
Last updated: May 18 2021 at 17:44 UTC