Why can't I use record selectors with an existentially quantified type?

Question

When using Existential types, we have to use a pattern-matching syntax for extracting the foralled value. We can't use the ordinary record selectors as functions. GHC reports an error and suggest using pattern-matching with this definition of yALL:

{-# LANGUAGE ExistentialQuantification #-}  data ALL = forall a. Show a => ALL { theA :: a } -- data ok  xALL :: ALL -> String xALL (ALL a) = show a -- pattern matching ok  -- ABOVE: heaven -- BELOW: hell  yALL :: ALL -> String yALL all = show $ theA all -- record selector failed 

---

forall.hs:11:19:     Cannot use record selector `theA' as a function due to escaped type variables     Probable fix: use pattern-matching syntax instead     In the second argument of `($)', namely `theA all'     In the expression: show $ theA all     In an equation for `yALL': yALL all = show $ theA all 

Some of my data take more than 5 elements. It's hard to maintain the code if I use pattern-matching:

func1 (BigData _ _ _ _ elemx _ _) = func2 elemx 

Is there a good method to make code like that maintainable or to wrap it up so that I can use some kind of selectors?

Answer 1

Existential types work in a more elaborate manner than regular types. GHC is (rightly) forbidding you from using theA as a function. But imagine there was no such prohibition. What type would that function have? It would have to be something like this:

-- Not a real type signature! theA :: ALL -> t  -- for a fresh type t on each use of theA; t is an instance of Show 

To put it very crudely, forall makes GHC "forget" the type of the constructor's arguments; all that the type system knows is that this type is an instance of Show. So when you try to extract the value of the constructor's argument, there is no way to recover the original type.

What GHC does, behind the scenes, is what the comment to the fake type signature above says—each time you pattern match against the ALL constructor, the variable bound to the constructor's value is assigned a unique type that's guaranteed to be different from every other type. Take for example this code:

case ALL "foo" of     ALL x -> show x 

The variable x gets a unique type that is distinct from every other type in the program and cannot be matched with any type variable. These unique types are not allowed to escape to the top level—which is the reason why theA cannot be used as a function.