Improvements to `magicDict`
Motivation
We'd like to clean up and generalize the machinery related to magicDict
. The idea for that started on #16586 (closed), have a look there for context.
Proposal
The idea is due to @simonpj from #16586 (closed):
Actually I think we can simplify magicDict yet more:
magicDict :: (dt => r) -> st -> r
where
dt
should be a single-method type class whose payload isst
; so that there is a (representational) cast from st todt
.
st
should be instantiated with only a singleton type. This is to avoid the possiblity of having many value of typedt
in scope, but with different and incoherent valuesNow the rewrite rule is
magicDict @dt @st @r k sv ===> k (sv |> co)
where
co
is a newtype coercion that converts typest
to constraintdt
. This coercion should always be possible (by point (1) above); if not, the rule does not fire. No Wrap needed, at all, I think! But invocations ofmagicDict
would need a type application to instantiatedt
.