Free lunch with GADTs

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