Union types (with explicit upcast) in Haskell

Main.hs

-- Example usage
module Main where

import Union


unionValue1 :: Union (String, (Double, ((Int, Int), ())))
unionValue1 = mkUnion "Foo"

unionValue2 :: Union (String, (Double, ((Int, Int), ())))
unionValue2 = upcast (mkUnion 1.5)

unionValue3 :: Union (String, (Double, ((Int, Int), ())))
unionValue3 = upcast (upcast (mkUnion (4,5)))


showFirst :: Union (String, (Double, ((Int, Int), ()))) -> String
showFirst union = case typeCase union of
    Left string -> string
    Right union' -> case typeCase union' of
      Left double -> show double
      Right union'' -> case finalCase union'' of
        (x,y) -> show x

-- |
-- >>> main
-- 4
main :: IO ()
main = do print (showFirst unionValue1)
          print (showFirst unionValue2)
          print (showFirst unionValue3)

Union.hs

{-# LANGUAGE ExistentialQuantification #-}
module Union (Union, mkUnion, upcast, typeCase, finalCase) where

import Data.Typeable


data Union u = forall a. Typeable a => PrivateUnion a

mkUnion :: Typeable a => a -> Union (a, u)
mkUnion x = PrivateUnion x

upcast :: Typeable a => Union u -> Union (a, u)
upcast (PrivateUnion x) = PrivateUnion x

typeCase :: Typeable a => Union (a, u) -> Either a (Union u)
typeCase (PrivateUnion x) = case cast x of
    Just y  -> Left y
    Nothing -> Right (PrivateUnion x)

finalCase :: Typeable a => Union (a, ()) -> a
finalCase union = case typeCase union of
    Left x -> x
    Right y -> y `seq` error msg
      where
        msg = "never happens, as a Union () cannot be constructed."

This gist is in reply to this reddit comment about how Typeable is a bit like instanceof in other languages, in a thread where I said that in a language with instanceof, it would be perfectly fine to have union types in which the summands could be distinguished.

I meant that if a language had union types and the language had instanceof, then the summands of the union type would be distinguishable, as opposed to typical union types in which the only available operations on Union a b are operations which work on both a and b.

So I wondered: could something like union types be implemented in Haskell? My implementation shows that the answer is "kind of, but they're not as convenient". In a language with builtin support for union types, there would be a subtyping relationship between a and Union a b, meaning an a would be implicitly upcasted to a Union a b when passed to a function which expects that. Since Haskell doesn't support subtyping (except for the fancy constraint subtyping which lens uses), my implementation of union types requires explicit upcasting.

Note that in order to complete the implementation, we would need many more explicit coercions to convert between Union a b and Union b a, between Union a a and a, etc. Such operations will become much easier to implement once I finally finish Category Syntax.