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