Calling a function within a pattern synonym

Question

I'm implementing some functionality on top of a zipper where the hole type is existentially quantified, i.e. I have something like this:

data Zipper (c :: Type -> Constraint) ... =
  forall hole. (c hole, ...) =>
    Zipper hole ...

where dots denote implementation details which I think are unrelated to my question. Consider now some data type:

data Tree = Fork Tree Tree | Leaf Int

What I would like to have is an ability to inspect my position in the tree. In case of simple recursion the standard way to achieve this is pattern matching:

case hole of
  Fork _ _ -> doSomething
  Leaf _   -> doSomethingElse

However, the type of hole is existentially quantified, so simple pattern matching won't do. The idea I had is to use a type class

class WhereAmI p a where
    position :: a -> p a

data Position :: Type -> Type where
    C_Leaf :: Position Tree
    C_Fork :: Position Tree
    -- possibly more constructors if we're traversing
    -- multiple data structures

Then I can do stuff like

f :: Zipper (WhereAmI Position) Tree -> Int
f (Zipper hole _) = case position hole of
  C_Leaf -> let (Leaf x) = hole in x
  otherwise -> ...

What I would like, however, is to replace C_Leaf with something like at @"Leaf" (i.e. use the original constructor names) using some magic like this

class WhereAmI' p (a :: Symbol) where
  position' :: Proxy a -> p

instance WhereAmI' (Position Tree) "Leaf" where
  position' _ = C_Leaf

instance WhereAmI' (Position Tree) "Fork" where
  position' _ = C_Fork

at :: forall a p. WhereAmI' p a => p
at = position (Proxy :: Proxy a)

This even works except that I can't use at as a pattern and I if I try to make it a pattern, GHC complains about a parse error in pattern...

Is there some clever way to achieve what I'm trying to describe here?

Answer 1

As far as I can tell, this isn't really possible. There's no way to return a pattern from a function for use in a match, and because of the way GADTs are refined (I think), it doesn't appear to be possible to do anything more complex than just a direct pattern match. For example, one of my failed attempts:

instance Eq (Position a) where
  C_Leaf == C_Leaf = True
  C_Fork == C_Fork = True
  _ == _ = False

pattern At x = ((\y -> at x == y) -> True)

This should allow you to write case position hole of At @"Leaf" -> ..., but it doesn't typecheck, presumably because of the type refinement process. To clarify:

C_Leaf -> ...                -- This works
((== C_Leaf) -> True) -> ... -- This doesn't work
y | y == C_Leaf -> ...       -- This doesn't work

The error I get for the latter two is Couldn't match expected type ‘Tree’ with actual type ‘hole’. I don't actually know for sure why this happens, but my current theory is that the expression is too complex for the type refinement to "take" properly: as far as the compiler is concerned, there's no reason to expect == to always return False when hole is the wrong type (even though we know that never happens). So it's not allowed.

---

I have to wonder, why do you believe using at @"Leaf" would be preferable to using C_Leaf? It's not as if you're really "using the original constructor names" in one version any more than in the other: they both use the original names, with some extra characters tacked on. I suppose in the former case you could allow passing in an arbitrary constructor symbol to match against, but that kind of thing appears to be disallowed in general, so you couldn't do that anyway. From what I can tell, you don't actually gain anything with the symbol approach.

Honestly, if your hole type is going to be restricted to the constructors supported by Position anyway, I don't really see the point in making it existential to begin with. It would be much more simple to create a sum type of all the types the zipper might contain, and pass that as a type parameter. But I don't know your use case very well, so I might be wrong.

---

If you really want to, I suppose you could probably use Template Haskell to do what you're going for. That would allow for something like:

$(at "Leaf") -> ...

Assuming you wrote the appropriate TH function, this would just be converted to C_Leaf -> ... at compile time, which would compile without issue.