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 .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.

Am Donnerstag, den 10.08.2017, 19:39 -0400 schrieb Ben Gamari:

On August 10, 2017 7:16:04 PM EDT, Wolfgang Jeltsch wrote:

...

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?

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

Yes, this feature seems to provide what I need. In my particular use case, it allows for pretty clear code. Is there also a solution that does not involve using this (unimplemented) feature? All the best, Wolfgang

How about this: {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE GADTs #-} import Data.Proxy data IsListType a where IsListType :: IsListType [b] type family Elem a where Elem [a] = a elemType :: forall a b . Elem a ~ b => IsListType a -> Proxy b elemType _ = Proxy :: Proxy (Elem a) On Thu, Aug 10, 2017 at 5:29 PM Alexis King wrote:

...

On Aug 10, 2017, at 5:08 PM, Wolfgang Jeltsch wrote:

Is there also a solution that does not involve using this (unimplemented) feature?

I get the feeling there is a better way to do this, but I found something of a hack that I think does what you want. Using Data.Type.Equality, you can match on Refl to bring the `b` into scope.

import Data.Type.Equality

f :: forall a. IsListType a -> () f IsListType = case Refl of (Refl :: (a :~: [b])) -> ()

This is sort of silly, though.

Alexis

_______________________________________________ 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.