non-commutative.hs

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeApplications #-}
module Test where

newtype Value a = Value a

class MaybeHasValue x where
  maybeValue :: Maybe (Value x)

data Void

instance MaybeHasValue Void where
  maybeValue = Nothing

instance MaybeHasValue () where
  maybeValue = Just (Value ())

foo :: forall a . MaybeHasValue a => Maybe (Value a)
foo = maybeValue

bar :: (forall a . MaybeHasValue a => Value a) -> Void
bar f = case f of
  Value x -> x

baz :: (forall a . MaybeHasValue a => Maybe (Value a)) -> Maybe Void
baz f = case f @() of
  Just v -> Just $ bar v
  Nothing -> Nothing