equiv.hs

prepropEquivInterpreters
    :: forall effs x r1 r2
     . (Eq x, Show x, Inject effs r1, Inject effs r2, Members effs effs)
    => (forall a. Sem r1 a -> IO a)
    -> (forall a. Sem r2 a -> IO a)
    -> (forall r. Members effs r => Gen (Sem r x))
    -> Property
prepropEquivInterpreters int1 int2 mksem = property $ do
  SomeSem sem <- liftGen @effs @x mksem
  pure $ ioProperty $ do
    a1 <- int1 sem
    a2 <- int2 sem
    pure $ a1 === a2

newtype SomeSem effs a = SomeSem
  { getSomeSem :: forall r. (Inject effs r) => Sem r a
  }

liftGen
    :: forall effs a
     . Members effs effs
    => (forall r. Members effs r => Gen (Sem r a))
    -> Gen (SomeSem effs a)
liftGen g = do
  a <- g @effs
  pure $ SomeSem $ inject a

inject :: Inject effs r => Sem effs a -> Sem r a
inject (Sem a) = a $ liftSem . deject . hoist inject

class Inject effs r where
  deject :: Union effs (Sem r) a -> Union r (Sem r) a

instance Inject '[] r where
  deject = absurdU

instance {-# INCOHERENT #-} Inject r r where
  deject = id

instance (Member eff r, Inject effs r) => Inject (eff ': effs) r where
  deject u =
    case decomp u of
      Left  u' -> deject u'
      Right w  -> Union membership w