fastsum
fastsum copied to clipboard
Is :> too rigid?
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)