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

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.