[Haskell-cafe] Exposing a GADT-provided dictionary

[Kosyrev Serge]

Good day, cafe!

I found a way to expose a GADT-provided dictionary, but I don't quite
like it:

> {-# LANGUAGE GADTs, RankNTypes #-}
>
> import Data.Function ((&))
>
> class HasDict a where
>
> data GADT a where
>   G1 :: HasDict a => a -> GADT a
>   -- ...
>   Gn :: HasDict a => a -> GADT a
>
> -- | Execute @body with the dictionary for HasDict extracted from the
> --   GADT.
> withGADTDict ::
>   (forall b. (b ~ a, HasDict b) => GADT b -> c) -> GADT a -> c
> withGADTDict body x = x & case x of
>   G1      _ -> body
>   -- ...
>   Gn      _ -> body

The problem is in withGADTDict's proportionality to the number of GADT's
clauses, as it is somewhat anti-modular.

Is that the only light-weight option?  I can imagine there is a way to
leverage generic programming, but that's a bit heavy..

-- 
с уважениeм / respectfully,
Kosyrev Serge

PGP Key ID: 3F62F118E38BED6D
--
“Most deadly errors arise from obsolete assumptions.”
  -- Frank Herbert, Children of Dune