Translation error when using sets in a forall expression; bad triggers? about dafny HOT 3 CLOSED

My guess is that Dafny simplifies i in {1} to i == 1 as part of its set expression simplification pass, and this creates an invalid trigger. I can think of multiple options

1. Disabling simplification when the set expression it's part of a trigger
2. Simplifying, then warning about the lack of trigger in this expression
3. Simplifying, but only in the body of the quantifier

I don't know how option 3 would affect completeness. I don't like option 1 much.

from dafny.

Sounds like a plausible explanation. If true, then 2 might be the easiest to achieve if we can make the set simplification happen before auto-triggers gets a chance to run.

from dafny.

FWIW, I arrived at this example by simplifying from a larger one, that still used a set literal, but had more than one element in the set. So we'd want to make sure that whatever fix is used captures that case as well.

from dafny.