Region76.hs

{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE OverlappingInstances  #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE UndecidableInstances #-}
module Region76 where

newtype Foo s a = Foo a

foo :: forall s s' a. (Show a, Protect s s') => Foo s a -> IO (Foo s' a)
foo (Foo a) = do
  check (Proxy2 :: Proxy2 s s') (print a)
  return (Foo a)

data Proxy2 a b = Proxy2
data Proxy1 a   = Proxy1

-- Type class which select whether perform action or do not
class Protect a b where
  check :: Monad m => p a b -> m () -> m ()

-- We use helper type class to select correct instance
instance (TypeEq a b eq, ProtectCase eq a b) => Protect a b where
  check p = checkCase (Proxy1 :: Proxy1 eq) p

-- Helper type class here we dispatch on eq type var. Unfortunate
-- feature of fundeps is that we need to introduce extra type class
-- for dispatch on type
class ProtectCase eq a b where
  checkCase :: Monad m => p eq -> q a b -> m () -> m ()

instance ProtectCase True a b where
  checkCase _ _ _ = return ()
instance ProtectCase False a b where
  checkCase _ _ = id


-- Type equality using functional dependencies
class  TypeEq (a :: α) (b :: α) (eq :: Bool) | a b -> eq
instance               TypeEq a a True
instance eq ~ False => TypeEq a b eq

Region78.hs

{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
module Region78 where

import Data.Typeable
import Data.Type.Equality

newtype Foo s a = Foo a

foo :: forall s s' a. (Show a, Action (s == s')) => Foo s a -> IO (Foo s' a)
foo (Foo a) = do
  check (Proxy :: Proxy s) (Proxy :: Proxy s') (print a)
  return (Foo a)



check :: forall m p a b. (Action (a == b), Monad m) => p a -> p b -> m () -> m ()
check _ _ = action (Proxy :: Proxy (a == b))


class Action (eq :: Bool) where
  action :: Monad m => p eq -> m () -> m ()

instance Action True  where action _ _= return ()
instance Action False where action _  = id