Generic Existentials

generics.hs

data Skolem (s :: Nat) = forall a. Skolem a

unsafeUnskolem :: Skolem n -> a
unsafeUnskolem (Skolem a) = unsafeCoerce a


data Error e (m :: * -> *) a
  = Throw e
  | forall x. Catch (m x) (e -> m x) (x -> a)

instance Functor m => Generic (Error e m a) where
  type Rep (Error e m a)
   = D1
      ('MetaData "Error" "TRYAGAIN" "main" 'False)
      (C1
         ('MetaCons "Throw" 'PrefixI 'False)
         (S1
            ('MetaSel
               'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy)
            (Rec0 e))
       :+: C1
             ('MetaCons "Catch" 'PrefixI 'False)
             (S1
                ('MetaSel
                   'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy)
                (Rec0 (m (Skolem 0))
              :*: (S1
                     ('MetaSel
                        'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy)
                     (Rec0 (e -> m (Skolem 0)))
                   :*: S1
                         ('MetaSel
                            'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy)
                         (Rec0 (Skolem 0 -> a))))))
  from (Throw e) = M1 $ L1 $ M1 $ M1 $ K1 $ e
  from (Catch a b c) =
    M1 $ R1 $ M1 $ M1 $ K1 (fmap Skolem a)
                :*: M1 (K1 $ \e -> fmap Skolem $ b e)
                :*: M1 (K1 $ \(Skolem s) -> c $ unsafeCoerce s)
  to (M1 (L1 (M1 (M1 (K1 e))))) = Throw e
  to (M1 (R1 (M1 (M1 (K1 a :*: (M1 (K1 b)) :*: (M1 (K1 c))))))) =
    Catch (fmap unsafeUnskolem a)
          (fmap (fmap unsafeUnskolem) b)
          (c . unsafeUnskolem)