TCB Dependent Match

Stream: new members

[Marcus Rossel]

I heard someone say today that the fact that Lean can perform dependent pattern matching "by itself" (without needing to provide the type level information as e.g. in Coq) comes at the cost of a larger trusted code base.
I couldn't follow as to why this would be the case, as I thought Lean just elaborates everything to its Expr type and then passes that to the kernel - so I wouldn't see how the kernel would have to distinguish between dependent vs nondependent matches.
What's the right answer here?

[Sky Wilshaw]

I don't think the kernel cares whether matches are dependent or not - they get compiled down into recursor applications anyway, which are handled here. The lack of match expressions in the kernel can be seen from lean's list of expression types.

[Mario Carneiro]

yes, this argument sounds like either nonsense or a miscommunication

[Mario Carneiro]

I don't even know what it means to say that "lean doesn't need to provide type level information as e.g. in Coq", lean has types for everything it just has to elaborate them using type inference

[Sky Wilshaw]

We're allowed to omit some type information because Lean's elaborator is strong.

[Reid Barton]

If anything it seems like the reverse is true, because the Lean kernel only sees recursor applications