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.