Exceptions (with Tom's stuff)

Exceptions.hs

{-# LANGUAGE DataKinds              #-}
{-# LANGUAGE FlexibleContexts       #-}
{-# LANGUAGE FlexibleInstances      #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GADTs                  #-}
{-# LANGUAGE InstanceSigs           #-}
{-# LANGUAGE KindSignatures         #-}
{-# LANGUAGE RankNTypes             #-}
{-# LANGUAGE ScopedTypeVariables    #-}
{-# LANGUAGE TypeApplications       #-}
{-# LANGUAGE TypeOperators          #-}
{-# LANGUAGE UndecidableInstances   #-}

module Exceptions where

import Data.Kind (Type)
import Data.Proxy

-- Tom's stuff https://gist.github.com/i-am-tom/e678a0e60ae7a161e26254d1704e6327

data Variant (xs :: [Type]) where
  Here :: x -> Variant (x ': xs)
  There :: Variant xs -> Variant (y ': xs)


class (xs :: [Type]) `CouldBe` (x :: Type) where
  throw :: x -> Variant xs

instance (x ': xs) `CouldBe` x where
  throw = Here

instance {-# OVERLAPPABLE #-} xs `CouldBe` x
    => (y ': xs) `CouldBe` x where
  throw = There . throw


class Drop x xs ys | x xs -> ys, x ys -> xs where
  catch :: Variant xs -> Either x (Variant ys)

instance Drop x (x ': xs) xs where
  catch (Here  x ) = Left x
  catch (There xs) = Right xs

instance {-# INCOHERENT #-} (y ~ z, Drop x xs ys)
    => Drop x (y ': xs) (z ': ys) where
  catch (There xs) = fmap There (catch xs)


f :: (e `CouldBe` String, e `CouldBe` Bool) => Variant e
f = throw True

g :: e `CouldBe` Bool => Either String (Variant e)
g = catch @String f

--

data Foo = Foo Int Bool String deriving (Eq, Show)

data InvalidInt = InvalidInt deriving (Eq, Show)
data InvalidBool = InvalidBool deriving (Eq, Show)
data InvalidString = InvalidString deriving (Eq, Show)

constructFoo
  :: ( e `CouldBe` InvalidInt
     , e `CouldBe` InvalidBool
     , e `CouldBe` InvalidString
     )
  => Int -> Bool -> String
  -> Either (Variant e) Foo
constructFoo i b s
  =   Foo
  <$> (if i > 0 then Right i else Left $ throw InvalidInt)
  <*> (if b then Right b else Left $ throw InvalidBool)
  <*> (if s /= "" then Right s else Left $ throw InvalidString)

catchInt
  :: ( e `CouldBe` InvalidBool
     , e `CouldBe` InvalidString
     )
  => Int -> Bool -> String
  -> Either InvalidInt (Variant e)
catchInt i b s
  = case constructFoo i b s of
      Left e -> catch @InvalidInt e
      Right _ -> undefined

catchErrors
  :: Int -> Bool -> String
  -> Foo
catchErrors i b s
  = case constructFoo i b s of
      Left e -> case catch @InvalidInt e of
        Left ii -> error "invalid int"
        Right e' -> case catch @InvalidBool e' of
          Left ib -> error "invalid bool"
          Right e'' -> case catch @InvalidString e'' of
            Left is -> error "invalid string"
            Right _ -> error "CAN'T BE"
      Right f -> f

data Error where
  Error :: forall e. Show e => e -> Error

instance Show Error where
  show (Error e) = "Error: " ++ show e

catchErrors'
  -- :: Int -> Bool -> String
  -- -> Either Error Foo
  :: Either (Variant '[InvalidInt, InvalidBool, InvalidString]) a
  -> Either (Either Error (Variant '[])) a
catchErrors' comput
  = case comput of
  -- = case constructFoo i b s of
      Left e -> case catch @InvalidInt e of
        Left ii -> Left $ Left (Error InvalidInt)
        Right e' -> case catch @InvalidBool e' of
          Left ib -> Left $ Left (Error InvalidBool)
          Right e'' -> case catch @InvalidString e'' of
            Left is -> Left $ Left (Error InvalidString)
            Right e''' -> Left $ Right e'''
      Right f -> Right f

catchErrors''
  :: Either (Variant '[InvalidInt, InvalidBool, InvalidString]) a
  -> Either Error a
catchErrors'' (Right a) = Right a
catchErrors'' (Left e)
  = case e of
      Here ii                 -> Left $ Error ii
      There (Here ib)         -> Left $ Error ib
      There (There (Here is)) -> Left $ Error is


handleError
  :: Either Error Foo
  -> (forall e. Show e => e -> String)
  -> Either String Foo
handleError (Left (Error e)) f = Left (f e)
handleError (Right foo)      _ = Right foo

main :: IO ()
main = undefined