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](1382e9fbc4/src/lake/Lake/Load/Main.lean (L196C49-L196C63)),
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.
e5e5a4d2e0