foo-not-bar.hs

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances #-}
module Test where

foo :: forall f b . (forall a . Maybe (f a)) -> ((forall a . f a) -> b) -> b -> b
foo x yesCont noCont = case x @() of
  Just _ -> yesCont v'
    where
      v' :: forall a . f a
      v' = case x @a of
        Just x' -> x'
        Nothing -> error "where's my free lunch?"
  Nothing -> noCont

class (Applicative f) => BarConstraint f a where
  maybeA :: Maybe (f a)

data Void

instance (Applicative f) => BarConstraint f Void where
  maybeA = Nothing

instance (Applicative f) => BarConstraint f () where
  maybeA = Just (pure ())

bar :: forall f b . Applicative f => (forall a . BarConstraint f a => Maybe (f a)) -> ((forall a . BarConstraint f a => f a) -> b) -> b ->b
bar x yesCont noCont = case x @() of
  Just _ -> yesCont v'
    where
      v' :: forall a . BarConstraint f a => f a
      v' = case x @a of
        Just v -> v
        Nothing -> error "wait, this isn't impossible..."
  Nothing -> noCont