calc ZMOD bug

Stream: general

[Kevin Buzzard]

Preparing some number theory for my course, and experimenting to try and figure out which of the four ways n \| b - c, b \== c [ZMOD n], b % n = c % n and (b : zmod n) = c is most convenient to use in practice when b,c are integers and n is a natural (often coerced to an integer). I ran into the below though: is this a bug in calc?

import data.int.modeq

-- typechecks
example (m : ℤ) : 4 * m + 3 ≡ 7 [ZMOD 4] :=
calc
4 * m + 3 ≡ 3         [ZMOD 4] : sorry
...       ≡ 7         [ZMOD 4] : sorry

-- fails to typecheck
-- goal at first sorry is `4 * m + 3 ≡ 3 [ZMOD ?m_1]`
example (m : ℤ) : 4 * m + 3 ≡ 7 [ZMOD 4] :=
calc
4 * m + 3 ≡ 3         [ZMOD 4] : by { sorry } -- tactic failed, result contains meta-variables
...       ≡ 7         [ZMOD 4] : by { sorry }

-- typechecks
example (m : ℤ) : 4 * m + 3 ≡ 7 [ZMOD 4] :=
calc
4 * m + 3 ≡ 3         [ZMOD 4] : by { show _ ≡ _ [ZMOD 4], sorry }
...       ≡ 7         [ZMOD 4] : by { sorry }

-- typechecks, but change either `: sorry` to `: by sorry`
-- and it fails
example (m n : ℤ) : 4 * m + 3 ≡ 8 * n + 7 [ZMOD 4] :=
calc
4 * m + 3 ≡ 3         [ZMOD 4] : sorry
...       ≡ 7         [ZMOD 4] : by sorry
...       ≡ 8 * n + 7 [ZMOD 4] : sorry