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@gmail.com> wrote:

> On Aug 10, 2017, at 5:08 PM, Wolfgang Jeltsch
> <wolfgang-it@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.