content: {-# LANGUAGE MultiParamTypeClasses #-}
  {-# LANGUAGE KindSignatures #-}
  {-# LANGUAGE FunctionalDependencies #-}
  {-# LANGUAGE FlexibleInstances #-}
  {-# LANGUAGE DataKinds #-}
  {-# LANGUAGE NoImplicitPrelude #-}
  {-# LANGUAGE TypeApplications #-}
  {-# LANGUAGE UnicodeSyntax #-}
  {-# LANGUAGE LinearTypes #-}
  module Foo where
  
  data Either a b = Left a | Right b
  
  either :: (a -> c) -> (b -> c) -> Either a b -> c
  either f g (Left a) = f a
  either f g (Right b) = g b
  
  class Iden p where
    iden :: p a a
  
  instance Iden (->) where
    iden x = x
  
  class Cat p where
    comp :: p b c -> p a b -> p a c
  
  instance Cat (->) where
    comp f g = \x -> f (g x)
  
  class ArrowChoice a where
      (+++) :: a b c -> a b' c' -> a (Either b b') (Either c c')
      (|||) :: a b d -> a c d -> a (Either b c) d
  
  instance ArrowChoice (->) where
  --    This doesn't work as |p| is inferred to be |-o| because of |Left|.
  --    Then GHC complains that |f| is not the same type before it realises
  --    that the overall type must be (->)
  --    f +++ g = (Left `comp` f) ||| (Right `comp` g)
      f +++ g = (comp @(->) Left f) ||| (comp @(->) Right g)
      (|||) = either
  
  
  -- This shouldn't work
  foo :: a ⊸ a
  foo = iden
  