chore: fix the MonadStore type classes, with semiOutParam

[JovanGerb]

The type class MonadStore1 and friends have an outParam, which should not be an outParam, because there are multiple possible values for this parameter. At this function fetchOrCreate, there are multiple stacked StateT monad transformers that each give a different instance to MonadStore1. It is an implementation detail of type class synthesis which instance is found. This particular type class synthesis fails when the unused instance Lake.instMonadStore1OfMonadDStoreOfFamilyOut is set to a lower priority, because then the synthesis order happens to go differently, so the wrong instance is found.

Replacing the outParam with a semiOutParam solves this issue. Thus, we make a new type class MonadStore1Of, which is the same, but with a semiOutParam. This follows the design of MonadState and MonadStateOf.

However, then it turns out that the instance cannot anymore be synthesised.

There are two instances for MonadStore1:

instance [MonadDStore κ β m] : MonadStore1 k (β k) m
instance [MonadDStore κ β m] [FamilyOut β k α] : MonadStore1 k α m 

The first one is problematic during unification, especially when β should be instantiated as a constant function. We make the second one sufficient by adding an instance for the general type family:

/-- The general type family -/
instance (priority := low) : FamilyDef Fam a (Fam a) where
  family_key_eq_type := rfl

So then we can get rid of the first instance.

[leanprover-community-mathlib4-bot]

Mathlib CI status (docs):

• 🟡 Mathlib branch lean-pr-testing-4205 build against this PR was cancelled. (2024-05-17 21:10:59) View Log
• 🟡 Mathlib branch lean-pr-testing-4205 build against this PR was cancelled. (2024-05-17 21:30:50) View Log
• 🟡 Mathlib branch lean-pr-testing-4205 build against this PR was cancelled. (2024-05-17 22:36:41) View Log
• 🟡 Mathlib branch lean-pr-testing-4205 build against this PR was cancelled. (2024-05-17 22:54:59) View Log
• ✅ Mathlib branch lean-pr-testing-4205 has successfully built against this PR. (2024-05-18 00:05:35) View Log
• ✅ Mathlib branch lean-pr-testing-4205 has successfully built against this PR. (2024-05-18 23:42:38) View Log
• ✅ Mathlib branch lean-pr-testing-4205 has successfully built against this PR. (2024-05-19 22:54:27) View Log
• ✅ Mathlib branch lean-pr-testing-4205 has successfully built against this PR. (2024-05-22 01:09:04) View Log
• ✅ Mathlib branch lean-pr-testing-4205 has successfully built against this PR. (2024-05-22 21:23:51) View Log

[JovanGerb]

awaiting-review

[tydeu]

Thanks for your work on this! ❤️ The MonadStore(1)/MonadStore(1)Of split looks great! However, I still have some outstanding questions on the design of the instances, along with a few minor organizational notes.

[tydeu]

Okay, everything looks good to me! Thank you for the time you spent on this PR and explaining the situation to me! ❤️