Hi cafe, I'm playing around with GADTs and was hoping they would let me have my cake and eat it too. I am trying to use GADTs to tag a type with some extra information. This information is very useful in a few cases, but the more common case is that I just have a list of items without the tags. Ideally I'll be able to recover the tags from the common case via pattern matching. What I have right now is: {-# LANGUAGE GADTs, ExistentialQuantification, EmptyDataDecls, RankNTypes, LiberalTypeSynonyms #-} data Tag1 data Tag2 data T tag where T1 :: Int -> T Tag1 T2 :: Double -> T Tag2 f1 :: [T t] -> Int f1 = foldr worker 0 where worker (T1 i) a = i+a worker _ a = a f2 :: [T Tag1] -> Int f2 = foldr worker 0 where worker :: T Tag1 -> Int -> Int worker (T1 i) a = a + i In f2 I can work with just values with one tag, but f1 is also important to me (working with the untagged values). f1 type checks but I do not know how to make a list [T t]. If I try the naive thing in ghci, it understandably tells me:

let l = [T1 5, T2 6.0]

<interactive>:6:16: Couldn't match type `Tag2' with `Tag1' Expected type: T Tag1 Actual type: T Tag2 In the return type of a call of `T2' In the expression: T2 6.0 In the expression: [T1 5, T2 6.0] Fair enough. Is there any magical way to make this possible? I am hoping to avoid making a separate existential wrapper around my type. I know that approach works, but that would make the more common case much less convenient. I also remember trying to use a type synonym with -XLiberalTypeSynonyms: type SimpleT = forall tag . T tag I managed to basically get that working with another variant of my list processing function, but it required -XImpredicativeTypes, which apparently did very unfortunate things to type inference. Thanks