How to pattern match on an universally quantified free monad?

Question

I'm wondering if I can write a function isPure :: Free f () -> Bool, which tells you if the given free monad equals Pure () or not. This is easy to do for a simple case, but I can't figure it out for a more complex case where there are constraints on the functor f.

import Control.Monad.Free

-- * This one compiles

isPure :: Free Maybe () -> Bool
isPure (Pure ()) = True
isPure _ = False

-- * This one fails to compile with "Ambiguous type variable ‘context0’ arising from a pattern
-- prevents the constraint ‘(Functor context0)’ from being solved."

{-# LANGUAGE RankNTypes #-}
type ComplexFree = forall context. (Functor context) => Free context ()

isPure' :: ComplexFree -> Bool
isPure' (Pure ()) = True
isPure' _ = False

I can see why specifying the exact type of context0 would be necessary in general, but all I want is to look the coarse-grained structure of the free monad (i.e. is it Pure or not Pure). I don't want to pin down the type because my program relies on passing around some constrained universally quantified free monads and I want this to work with any of them. Is there some way to do this? Thanks!

EDITED to change "existentially quantified" -> "universally quantified"

EDIT: since my ComplexFree type might have been too general, here's a version that more exactly mimics what I'm trying to do.

--* This one actually triggers GHC's warning about impredicative polymorphism...
{-# LANGUAGE GADTs #-}

data MyFunctor context next where
  MyFunctor :: Int -> MyFunctor context next -- arguments not important

type RealisticFree context a = Free (MyFunctor context) a

class HasFoo context where
  getFoo :: context -> Foo

class HasBar context where
  getBar :: context -> Bar

type ConstrainedRealisticFree = forall context. (HasFoo context, HasBar context) => RealisticFree context ()

processRealisticFree :: ConstrainedRealisticFree -> IO ()
processRealisticFree crf = case isPure'' crf of
  True -> putStrLn "It's pure!"
  False -> putStrLn "Not pure!"

isPure'' :: ConstrainedRealisticFree -> Bool
isPure'' = undefined -- ???

(For some more context, this free monad is meant to model an interpreter for a simple language, where a "context" is present. You can think of the context as describing a reader monad that the language is evaluated within, so HasFoo context and HasBar context enforce that a Foo and Bar are available. I use universal quantification so that the exact type of the context can vary. My goal is to be able to identify an "empty program" in this free monad interpreter.)

Answer 1

First of all, this is not existential quantification. That would look like this:

data ComplexFree = forall context. (Functor context) => ComplexFree (Free context ())

(a syntax I find rather confusing, so I prefer the GADT form

data ComplexFree where
    ComplexFree :: (Functor context) => Free context () -> ComplexFree 

, which means the same thing)

You have a universally quantified type here, that is, if you have a value of type ComplexFree (the way you have written it), it can turn into a free monad over any functor you choose. So you can just instantiate it at Identity, for example

isPure' :: ComplexFree -> Bool
isPure' m = case m :: Free Identity () of 
                Pure () -> True
                _       -> False

It must be instantiated at some type in order to inspect it, and the error you see is because the compiler couldn't decide which functor to use by itself.

However, instantiating is not necessary for defining isPure'. Ignoring bottoms¹, one of the functors you could instantiate ComplexFree with is Const Void, which means that the recursive case of Free reduces to

f (m a)
  = Const Void (m a)
 ~= Void

that is, it is impossible. By some naturality arguments, we can show that which branch a ComplexFree takes cannot depend on the choice of functor, which means that any fully-defined ComplexFree must be a Pure one. So we can "simplify" to

isPure' :: ComplexFree -> Bool
isPure' _ = True

How boring.

---

However, I suspect you may have made a mistake defining ComplexFree, and you really do want the existential version?

data ComplexFree where
    ComplexFree :: (Functor context) => Free context () -> ComplexFree

In this case, a ComplexFree "carries" the functor with it. It only works for one functor, and it (and only it) knows what functor that is. This problem is better-formed, and implemented just as you would expect

isPure' :: ComplexFree -> Bool
isPure' (ComplexFree (Pure _)) = True
isPure' _ = False

---

¹ Ignoring bottom is a common practice, and usually not problematic. This reduction strictly increases the information content of the program -- that is, whenever the original version gave a defined answer, the new version will give the same answer. But the new one might "fail to go into an infinite loop" and accidentally give an answer instead. In any case, this reduction can be modified to be completely correct, and the resulting isPure' is just as useless.