<html><head></head><body><div>Hi!</div><div><br></div><div>I think this is too complicated. I am developing a library and this access to existentially quantified type variables is something that cannot be part of the library, but must be done by users using the library. So it should be doable in an easy-to-understand and lightweight way.</div><div><br></div><div>All the best,</div><div>Wolfgang</div><div><br></div><div>Am Freitag, den 11.08.2017, 07:04 +0000 schrieb Kai Zhang:</div><blockquote type="cite"><div dir="ltr">How about this:<div><br></div><div><div>{-# LANGUAGE TypeFamilies #-}</div><div>{-# LANGUAGE ScopedTypeVariables #-}</div><div>{-# LANGUAGE GADTs #-}</div><div><br></div><div>import Data.Proxy</div><div><br></div><div>data IsListType a where</div><div> IsListType :: IsListType [b]</div><div><br></div><div>type family Elem a where</div><div> Elem [a] = a</div><div><br></div><div>elemType :: forall a b . Elem a ~ b => IsListType a -> Proxy b</div><div>elemType _ = Proxy :: Proxy (Elem a)</div></div></div><br><div class="gmail_quote"><div dir="ltr">On Thu, Aug 10, 2017 at 5:29 PM Alexis King <<a href="mailto:lexi.lambda@gmail.com">lexi.lambda@gmail.com</a>> wrote:<br></div><blockquote type="cite">> On Aug 10, 2017, at 5:08 PM, Wolfgang Jeltsch<br>
> <<a href="mailto:wolfgang-it@jeltsch.info" target="_blank">wolfgang-it@jeltsch.info</a>> wrote:<br>
><br>
> Is there also a solution that does not involve using this<br>
> (unimplemented) feature?<br>
<br>
I get the feeling there is a better way to do this, but I found<br>
something of a hack that I think does what you want. Using<br>
Data.Type.Equality, you can match on Refl to bring the `b` into scope.<br>
<br>
import Data.Type.Equality<br>
<br>
f :: forall a. IsListType a -> ()<br>
f IsListType = case Refl of<br>
(Refl :: (a :~: [b])) -> ()<br>
<br>
This is sort of silly, though.<br>
<br>
Alexis<br>
<br>
_______________________________________________<br>
Haskell-Cafe mailing list<br>
To (un)subscribe, modify options or view archives go to:<br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe</a><br>
Only members subscribed via the mailman list are allowed to post.<br></blockquote></div>
</blockquote></body></html>