fix: bug in elab TC for projections

Open digama0 opened this issue 2 years ago • 2 comments

This adapts the code from the inferProjType function and the kernel projection typechecker so that the elaborator correctly reports errors when the projection would be rejected by the kernel. Fixes #2697.

Oct 16 '23 21:10 digama0

This PR fixes part of the issue (it prevents

inductive Foo : Prop where
  | mk (x : Nat) (h : x = x) : Foo

example (h : Foo) := h.2

from working), but it does not fix the example from #2697, and I think a proper fix would require more than just this, so this PR is on hold until I get approval for making some changes that will affect the kernel.

Oct 16 '23 23:10 digama0

💥 Mathlib branch lean-pr-testing-2700 build failed against this PR. (2023-10-17 00:27:53) View Log
💥 Mathlib branch lean-pr-testing-2700 build failed against this PR. (2023-10-22 08:09:51) View Log

Oct 17 '23 00:10 leanprover-community-mathlib4-bot