instance declaration rfl error

Stream: lean4

[Shreyas Srinivas]

When declaring an instance of a complete lattice for a type I started by sorrying out all fields. However I get the usual rfl error :

The rfl tactic failed. Possible reasons:
- The goal is not a reflexive relation (neither `=` nor a relation with a @[refl] lemma).
- The arguments of the relation are not equal.
Try using the reflexivity lemma for your relation explicitly, e.g. `exact Eq.refl _` or
`exact HEq.rfl` etc.

[Shreyas Srinivas]

This makes no sense to me since I haven't even applied rfl

[Shreyas Srinivas]

I don't have a good #mwe yet since I don't know where the error is coming from

[Matthew Ballard]

Autoparams are being filled somewhere by rfl most likely

[Matthew Ballard]

If you use the code action for the maximal skeleton, you should be able to track it down

[Shreyas Srinivas]

how do I trigger this code action?

[Matthew Ballard]

instance x : MyClass := _ I think

[Matthew Ballard]

The :light_bulb: should pop over the hole

[Shreyas Srinivas]

okay so I need to use the := instead of where clause to trigger it

[Shreyas Srinivas]

I didn't get it when I tried with where

[Shreyas Srinivas]

While I trace down the issue, I am wondering if the code action could be made to work with where

[Shreyas Srinivas]

It just looks neater to my haskell brain

[Matthew Ballard]

That is reasonable request though you might want where? or something maybe.

[Shreyas Srinivas]

So this was a case of accidentally putting \subset where I really wanted \ssubset. But I was able to use inferInstance and make the whole issue go away