show how quantifiedconstraints can be used for writing highly polymorphic versions of functions like pure

example.hs

{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE RoleAnnotations #-}
{-# LANGUAGE TypeApplications #-}
{-# OPTIONS_GHC -Wall #-}

module MaybeT where

import Control.Monad.Trans
import Data.Coerce
import Data.Proxy
import Unsafe.Coerce

newtype MaybeT m a = MaybeT { unMaybeT :: m (Maybe a) }

-- type role MaybeT representational representational

instance MonadTrans MaybeT where
  lift :: Monad m => m a -> MaybeT m a
  lift ma = MaybeT $ fmap Just ma

instance Functor m => Functor (MaybeT m) where
  fmap :: forall a b. (a -> b) -> MaybeT m a -> MaybeT m b
  fmap a2b (MaybeT ma) = MaybeT go
    where
      go :: m (Maybe b)
      go =
        let _ = ma :: m (Maybe a)
        in fmap inner ma

      inner :: forall anyM. Functor anyM => anyM a -> anyM b
      inner = fmap a2b

-- | This instance (and implementation of pure), requires that @m x@ is
-- representationally equal as long as @x@ is representationally equal.   In
-- practice, this is too restrictive because we may want to use this Applicative
-- instance with something that is not representationally equal (for instance
-- the MyGADT below).
-- instance (forall x y. Coercible x y => Coercible (m x) (m y), Applicative m) => Applicative (MaybeT m) where
--   pure :: a -> MaybeT m a
--   pure a = pure' (Proxy @Maybe) a

instance Applicative m => Applicative (MaybeT m) where
  pure :: a -> MaybeT m a
  pure a = MaybeT $ pure (pure a)

  (<*>) :: forall a b. MaybeT m (a -> b) -> MaybeT m a -> MaybeT m b
  MaybeT ma2b <*> MaybeT ma = MaybeT go
    where
      go :: m (Maybe b)
      go =
        let _ = ma2b :: m (Maybe (a -> b))
            _ = ma :: m (Maybe a)
        in inner <$> ma2b <*> ma

      inner :: forall anyM. Applicative anyM => anyM (a -> b) -> anyM a -> anyM b
      inner = (<*>)

-- | This is a generic version of pure that will work for both EitherT and MaybeT.
pure'
  :: forall a m inner proxy n
   . ( Applicative m
     , Applicative inner
     -- This says that as long as for all x and y that are representationally
     -- equal, we know that (m (inner x)) and (n m y) are representationally
     -- equal.  This is exactly what we need to be able to do the coersion.
     --
     -- However, I think this will NOT work if @m@ is a GADT, since the type-role
     -- of @a@ in @m a@ may not be representational in that case.
     , forall x y. Coercible x y => Coercible (m (inner x)) (n m y)
     )
  => proxy inner
  -> a
  -> n m a
pure' _ a = coerce (pure (pure a) :: m (inner a))

-- | This is similar to 'pure'', but it is using unsafeCoerce, so it is less
-- safe.
pure'' :: forall a n m inner proxy. (Applicative inner, Applicative m) => proxy inner -> a -> n m a
pure'' _ a = unsafeCoerce (pure (pure a) :: m (inner a))

newtype EitherT e m a = EitherT { unEitherT :: m (Either e a) }

data MyGADT a where
  Pure :: a -> MyGADT a
  Intiii :: Int -> MyGADT Int

type role MyGADT nominal

instance Functor MyGADT where
  fmap :: (a -> b) -> MyGADT a -> MyGADT b
  fmap a2b (Pure a) = Pure (a2b a)
  fmap i2b (Intiii i) = Pure (i2b i)

instance Applicative MyGADT where
  pure = Pure

  (<*>) :: MyGADT (a -> b) -> MyGADT a -> MyGADT b
  Pure a2b <*> Pure a = Pure (a2b a)
  Pure i2b <*> Intiii i = Pure (i2b i)

blah :: MaybeT MyGADT String
blah = pure "hello"
-- blah = MaybeT (Pure (Just "hello"))

This will of course only run in GHC-8.6 or greater because it is using QuantifiedConstraints.

This QuantifiedConstraint trick comes from here:
https://ryanglscott.github.io/2018/03/04/how-quantifiedconstraints-can-let-us-put-join-back-in-monad/