Deep Pure Fun

Pure.hs

{-# LANGUAGE TypeApplications, DataKinds, KindSignatures, TypeFamilies, MultiParamTypeClasses, FunctionalDependencies, UndecidableInstances #-}

module Main where

import Data.Functor.Compose
import Data.Functor.Identity
import Data.Coerce

data Nat = Zero | Succ Nat

type family WrapCompose (x :: *) where
  WrapCompose (f x) = Compose f (WrapCompose x)
  WrapCompose x = Identity

class Pure f (n :: Nat) | f -> n where
  deepPure :: a -> f a

instance Pure Identity Zero where
  deepPure = Identity

instance (Applicative f, Pure g n) => Pure (Compose f g) (Succ n) where
  deepPure = Compose . pure . deepPure

veryPure :: forall a b n. (Coercible b (WrapCompose b a), Pure (WrapCompose b) n)
  => a -> b
veryPure x = coerce $ deepPure @(WrapCompose b) x


main :: IO (Maybe Bool)
main = veryPure ()