Hi!

I must say that I do not really understand this, but I nevertheless doubt that it solves my problem. In your code, you are already starting with the value IsListType whose type you specify as [a]. In this case, there is nothing to find out about the element type; you already know that it is a. My situation is that I have some type l and a value p :: IsListType l. A successful match of p against the pattern IsListType tells me that there is an a with l ~ [a]. However, I cannot refer to this a.

All the best,
Wolfgang

Am Donnerstag, den 10.08.2017, 16:35 -0700 schrieb 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@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.