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

[Kai Zhang]

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 <lexi.lambda at gmail.com> wrote:

> > On Aug 10, 2017, at 5:08 PM, Wolfgang Jeltsch
> > <wolfgang-it at jeltsch.info> 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.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20170811/24e5057a/attachment.html>