Hi Kosyrev, Would refactoring the type like this work for you?
data GADT a where G :: HasDict a => Tag -> a -> GADT a
data Tag = Tag1 | ... | Tagn
withGADTDict :: ... withGADTDict body x = x & case x of G _ _ -> body
Li-yao On 10/15/2017 07:07 PM, Kosyrev Serge wrote:
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..