'Occurs check failed' error

Stream: general

[Gihan Marasingha]

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]

@Gihan Marasingha Does exact h₁ work?

[Johan Commelin]

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

[Gihan Marasingha]

@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]

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

[Johan Commelin]

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

[Gihan Marasingha]

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]

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

[Johan Commelin]

Maybe that's the issue why exact is not working

[Johan Commelin]

Ooh, h\3 is telling me the answer

[Gihan Marasingha]

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]

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.