Cursed.hs

{-# LANGUAGE GADTs, DataKinds, ImplicitParams #-}

import Data.Kind
import Control.Monad.Identity

data Union (f :: t -> *) (xs :: [t]) :: * where
  This :: f x -> Union f (x : xs)
  That :: Union f xs -> Union f (x : xs)

type OpenUnion = Union Identity

data Elem :: t -> [t] -> * where
  Here :: Elem x (x : xs)
  There :: Elem x xs -> Elem x (y : xs)

class Member x xs where
  memberProof :: Elem x xs

instance Member x (x : xs) where
  memberProof = Here

instance Member x xs => Member x (y : xs) where
  memberProof = There memberProof

injRaw :: forall (t :: Type)
                 (x :: t)
                 (f :: t -> Type)
                 (xs :: [t])
        . (?prf :: Elem x xs)
       => f x
       -> Union f xs
injRaw x =
  case ?prf of
    Here -> This x
    There prf -> let ?prf = prf
                  in That (injRaw x)

prjRaw :: forall (t :: Type)
                 (x :: t)
                 (f :: t -> Type)
                 (xs :: [t])
        . (?prf :: Elem x xs)
       => Union f xs
       -> Maybe (f x)
prjRaw a =
  case ?prf of
    Here ->
      case a of
        This x -> Just x
        That _ -> Nothing
    There prf ->
      case a of
        This _ -> Nothing
        That x -> let ?prf = prf
                   in prjRaw x

inj :: Member x xs => f x -> Union f xs
inj a =
  let ?prf = memberProof
   in injRaw a

openInj :: Member x xs => x -> OpenUnion xs
openInj = inj . pure

prj :: Member x xs => Union f xs -> Maybe (f x)
prj a =
  let ?prf = memberProof
   in prjRaw a

openPrj :: Member x xs => OpenUnion xs -> Maybe x
openPrj = fmap runIdentity . prj