-{-# OPTIONS -XRankNTypes -XMultiParamTypeClasses -XNoMonomorphismRestriction -XTypeOperators -XFlexibleInstances -XFunctionalDependencies #-}
+{-# OPTIONS -XRankNTypes -XMultiParamTypeClasses -XNoMonomorphismRestriction -XTypeOperators -XFlexibleInstances -XFunctionalDependencies -XEmptyDataDecls #-}
-----------------------------------------------------------------------------
-- |
-- Module : GHC.HetMet.Arrow
ga_applyl = ga_swap >>> app
ga_applyr = app
-
-
+-- The uninhabited type
+data Void
+
+-- In Coq we could simply prove that these cases are impossible; in Haskell we need to have some faith.
+voidImpossible :: Void -> a
+voidImpossible = error "this is impossible; you have a bug in your compiler"
+
+instance ArrowChoice a => GArrow a Either Void where
+ ga_first = left
+ ga_second = right
+ ga_uncancell = arr Right
+ ga_uncancelr = arr Left
+ ga_cancell = arr unVoidLeft
+ where
+ unVoidLeft (Left v) = voidImpossible v
+ unVoidRight (Right x) = x
+ ga_cancelr = arr unVoidRight
+ where
+ unVoidRight (Left x) = x
+ unVoidRight (Right v) = voidImpossible v
+ ga_assoc = arr eitherAssoc
+ where
+ eitherAssoc (Left (Left x)) = Left x
+ eitherAssoc (Left (Right y)) = Right (Left y)
+ eitherAssoc (Right z ) = Right (Right z)
+ ga_unassoc = arr eitherUnAssoc
+ where
+ eitherUnAssoc (Left x ) = Left (Left x)
+ eitherUnAssoc (Right (Left y)) = Left (Right y)
+ eitherUnAssoc (Right (Right z)) = Right z
+
+instance ArrowChoice a => GArrowSum a (,) () Void Either where
+ ga_never = arr voidImpossible
+ ga_merge = arr merge
+ where
+ merge (Left x) = x
+ merge (Right x) = x