Zulip Chat Archive

Stream: general

Topic: 'Occurs check failed' error


Gihan Marasingha (Jul 16 2020 at 13:17):

Hello! I'm getting an error message I don't understand. Can anyone help me?

I have, in the local context, a hypothesis h₁ : en = M :: (ys ++ ↑"U"), and would like to close the goal ⊢ en = M :: ?m_1. I try rw h₁ and get the error message exact tactic failed, failed to assign eq.mpr (id (eq.rec (eq.refl (en = M :: ?m_1)) h₁)) htarget to metavariable ?m_2 (possible cause: occurs check failed).

Johan Commelin (Jul 16 2020 at 13:18):

@Gihan Marasingha Does exact h₁ work?

Johan Commelin (Jul 16 2020 at 13:18):

If not, do you have other open goals, or is this the only one?

Gihan Marasingha (Jul 16 2020 at 13:21):

@Johan Commelin . Thanks! exact h₁ gives an 'invalid type ascription error'. This is not the only goal. My tactic state, before trying the rw is:

2 goals
st en : miustr,
ys : list miu_atom,
h₂ : st = M :: ys,
h₃ : M :: ys ++ "U" = M :: (ys ++ "U"),
h₁ : en = M :: (ys ++ "U")
 en = M :: ?m_1

st en : miustr,
h₁ : rule1 st en,
h₂ : goodstart st
 list miu_atom

Johan Commelin (Jul 16 2020 at 13:23):

Hmm... confusing. Maybe convert instead of exact can make Lean behave?

Johan Commelin (Jul 16 2020 at 13:23):

Otherwise, exact (ys ++ ↑"U") in the other goal might give more info

Gihan Marasingha (Jul 16 2020 at 13:38):

Thanks. I was mistaken in my previous comment regarding the tactic state. It was different. I've also just changed my code to avoid the coercion. Now the tactic state before the rw is:

---snip---

I haven't used convert before. I'll look into it.

Johan Commelin (Jul 16 2020 at 13:39):

@Gihan Marasingha Actually, I don't know how the parens are in h\1 !

Johan Commelin (Jul 16 2020 at 13:39):

Maybe that's the issue why exact is not working

Johan Commelin (Jul 16 2020 at 13:40):

Ooh, h\3 is telling me the answer

Gihan Marasingha (Jul 16 2020 at 14:13):

Ahh, I'm being an idiot and deleted an extra line in my last message (thus changing the goal). My original tactic state (modulo coercion) was what I have now. In case it helps, when I try exact h₁, I get:

invalid type ascription, term has type
  en = M :: (ys ++ [U])
but is expected to have type
  en = M :: ?m_1

Gihan Marasingha (Jul 16 2020 at 15:38):

OK, it's all fixed now. I had an extra split at the start of my code that caused everything to foul up! Thanks for the help.


Last updated: Dec 20 2023 at 11:08 UTC