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

[Michael Burge]

Could something like this work for you? Here, a ~ b and you have access to
b:

case (IsListType :: IsListType [a], Proxy :: Proxy a) of
    (_, proxy :: Proxy b) -> asProxyTypeOf undefined proxy :: b

On Thu, Aug 10, 2017 at 4:16 PM, 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.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20170810/76582eca/attachment.html>