TypesAndValues.hs

-- This works
--   recoverF_CPS everyP (f (A 1)) B'
-- and so does
--   recoverF_CPS (Proxy :: Proxy ((~) Char)) (\x -> case x of A _ -> 'a'; B -> 'b') (A' 1)
-- But this isn't allowed to type check:
--   recoverF_CPS everyP (f B) B'

-- Also note this law holds:
--   recoverF_CPS everyP recoverF' = id

-- I believe an actual isomorphism is between `F'` and `Either (F a AType) (F a BType)`,
-- which should also provide the type safety the question is asking for
-- (since it shouldn't matter where the `F y x` values come from when `f`
-- is being used).
-- This isomorphism is given by `toEither` and `fromEither`.

{-# LANGUAGE GADTs              #-}
{-# LANGUAGE TypeFamilies       #-}
{-# LANGUAGE DataKinds          #-}
{-# LANGUAGE ConstraintKinds    #-}
{-# LANGUAGE RankNTypes         #-}
{-# LANGUAGE PolyKinds          #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE FlexibleInstances  #-}

import Data.Constraint (Constraint)
import Data.Proxy

recoverF_CPS :: Proxy c -> (c r => (forall x. F y x -> r) -> F' y -> r)
recoverF_CPS Proxy k (A' v) = k (A v)
recoverF_CPS Proxy k B'     = k B

toEither :: F' a -> Either (F a AType) (F a BType)
toEither = withEither id

fromEither :: Either (F a AType) (F a BType) -> F' a
fromEither (Left (A v)) = A' v
fromEither (Right B)    = B'

withEither :: (Either (F a AType) (F a BType) -> r) -> F' a -> r
withEither k (A' v) = k (Left (A v))
withEither k B'     = k (Right B)

data T = AType | BType deriving Show

data F y (x :: T) where
  A :: a -> F a AType
  B :: F a BType

deriving instance Show y => Show (F y x)

type family Valid x y :: Constraint where
  Valid BType ty2 = ty2 ~ AType
  Valid ty1   ty2 = ()

data F' a = A' a | B' deriving Show

recoverF' :: F x t -> F' x
recoverF' (A v) = A' v
recoverF' B     = B'

class Every a
instance Every a

everyP :: Proxy Every
everyP = Proxy

f :: Valid ty1 ty2 => F a ty1 -> F a ty2 -> F a ty1
f (A x) B     = A x
f B     (A _) = B
f (A _) (A x) = A x