[Haskell-cafe] How to bring existentially quantified type variables into scope

[Ben Gamari]

On August 10, 2017 7:16:04 PM EDT, Wolfgang Jeltsch <wolfgang-it at jeltsch.info> wrote:
>Hi!
>
>GHC has some support for referring to existentially quantified type
>variables. For example, consider the following definition:
>
>> data SomeList = forall a . SomeList [a]
>
>With the ScopedTypeVariables extension, you can get hold of the
>concrete
>type a used in a SomeList value:
>
>> f :: SomeList -> SomeList
>> f (SomeList [x :: a]) = SomeList xs where
>>
>>     xs :: [a]
>>     xs = [x, x]
>
>However, this approach does not work if there are no fields whose type
>involves the existentially quantified type variable. Consider, for
>example, the following definition:
>
>> data IsListType a where
>>
>>     IsListType :: IsListType [b]
>
>For each type T, we can match a value of type IsListType T against the
>pattern IsListType. If this succeeds, we know that T is a list type,
>but
>we do not have access to the respective element type.
>
>Is there a way to determine existentially quantified type variables
>like
>the b in the above example?
>
>All the best,
>Wolfgang
>_______________________________________________
>Haskell-Cafe mailing list
>To (un)subscribe, modify options or view archives go to:
>http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
>Only members subscribed via the mailman list are allowed to post.

Note that the feature described in #11350 will provide a quite direct way to accomplish this by allowing type applications in pattern matches.