Zulip Chat Archive

Stream: general

Topic: Elaboration of function types

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: Aug 03 2023 at 10:10 UTC