Haskell: QuantifiedConstraints

Main.hs

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE MagicHash #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UnliftedNewtypes #-}
{-# LANGUAGE NoStarIsType #-}
{-# OPTIONS_GHC -Werror #-}
{-# OPTIONS_GHC -Wincomplete-patterns #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}

module Main where


type Cofree :: (Type -> Type) -> Type -> Type
data Cofree f a = a :< (f (Cofree f a))

instance (Show1 f) => Show1 (Cofree f) where
  liftShowsPrec sp sl = go
    where
      goList = liftShowList sp sl
      go d (a :< as) = showParen (d > 5) $
        sp 6 a . showString " :< " . liftShowsPrec go goList 5 as

instance (Show a, Show1 f) => Show (Cofree f a) where
  showsPrec = showsPrec1

-- instance (Eq a, Eq1 f) => Eq (Cofree f a) where
--   a1 :< k1 == a2 :< k2 =
--     a1 == a2 && k1 `eq1` k2

-- instance (Eq a, Eq (f (Cofree f a))) => Eq (Cofree f a) where
--   a1 :< k1 == a2 :< k2 =
--     a1 == a2 && k1 == k2

instance (Eq a, forall x. Eq x => Eq (f x)) => Eq (Cofree f a) where
  a1 :< k1 == a2 :< k2 =
    a1 == a2 && k1 == k2

type NonEmpty a = Cofree Maybe a

nonEmptyList :: NonEmpty Int
nonEmptyList = 0 :< Just (1 :< Just (2 :< Nothing))

nonEmptyList2 :: NonEmpty Int
nonEmptyList2 = 0 :< Just (3 :< Just (2 :< Nothing))

type MonadTrans :: Type
type MonadTrans = (Type -> Type) -> Type -> Type

-- type Trans :: MonadTrans -> Constraint
-- class Trans t where
--   lift :: Monad m => m a -> (t m) a

type (*) :: MonadTrans -> MonadTrans -> MonadTrans
newtype (t1 * t2) m a = C { runC :: t1 (t2 m) a }
  deriving newtype (Functor, Applicative, Monad)

{-
-- app/Main.hs:119:14-17: error: …
--     • Could not deduce (Monad (t2 m)) arising from a use of ‘lift’
--       from the context: (Trans t1, Trans t2)
--         bound by the instance declaration
--         at /home/arnau/projects/haskell/scratch/app/Main.hs:118:10-48
--       or from: Monad m
--         bound by the type signature for:
--                    lift :: forall (m :: * -> *) a. Monad m => m a -> (*) t1 t2 m a
--         at /home/arnau/projects/haskell/scratch/app/Main.hs:119:3-6
--     • In the first argument of ‘(.)’, namely ‘lift’
--       In the second argument of ‘(.)’, namely ‘lift . lift’
--       In the expression: C . lift . lift
--     |
-- Compilation failed.
instance (Trans t1, Trans t2) => Trans (t1 * t2) where
  lift = C . lift . lift
-}

class (forall m. Monad m => Monad (t m)) => Trans t where
  lift :: Monad m => m a -> (t m) a

instance (Trans t1, Trans t2) => Trans (t1 * t2) where
  lift = C . lift . lift