Is :> too rigid?

[jwiegley]

I'm trying to figure out how to get the following to work:

stronger :: f :< r => Sum r v -> a
stronger = undefined

weaker :: f :< r => Sum (e ': r) v -> a
weaker = stronger

I would think that f :> r entails the constraint f :> any ': r, but this does not seem to be the case. Intuitively I would see the entailment as just a Succ on the former witness. Instead, the error I get is:

• Could not deduce (KnownNat (ElemIndex f0 (e : r)))
    arising from a use of ‘stronger’
  from the context: f :< r
    bound by the type signature for:
               weaker :: forall (f :: * -> *) (r :: [* -> *]) (e :: * -> *) v.
                         (f :< r) =>
                         Sum (e : r) v -> f v
    at /Users/johnw/src/trade-journal/src/Journal/SumLens.hs:74:1-41
  The type variable ‘f0’ is ambiguous
  Relevant bindings include
    weaker :: Sum (e : r) v -> f v
      (bound at /Users/johnw/src/trade-journal/src/Journal/SumLens.hs:75:1)