GADT and typeclass funcional dependencies not working well together

To use GADTs in anger, I keep needing to put them into homogeneous collections (set, list etc.) but to do this the typing parameter needs hiding. Later, when you operate on elements of the list, you need to pattern-match to recover the actual type of the element, and then chain on calls to that. This doesn't seem to work well in practice when the operation to run relies upon a fundep.

data Zero
data Suc a

data ListWithLength a b where
  Nill :: ListWithLength a Zero
  Cons :: a -> ListWithLength a b -> ListWithLength a (Suc b)

class Even a
instance Even Zero
instance (Even e) => Even (Suc (Suc e))


-- have to model this as a class
class (Even b) => DoubleUp a b | a -> b where
  doubleUp :: ListWithLength x a -> ListWithLength x b

instance DoubleUp Zero Zero where
  doubleUp Nill = Nill

instance (DoubleUp e f) => DoubleUp (Suc e) (Suc (Suc f)) where
  doubleUp (Cons x xs) = Cons x (Cons x (doubleUp xs))


-- we want to stick a load of these into a list, so we must wrap them up somehow

data AnyLWL a where
  AnyLWL :: ListWithLength a b -> AnyLWL a


-- now, we would like to apply doubleUp to each element of the list
duAny :: [AnyLWL a] -> [AnyLWL a]
duAny = map duAny_
  where
    duAny_ (AnyLWL n@Nill)       = AnyLWL $ doubleUp n
    duAny_ (AnyLWL c@(Cons _ _)) = AnyLWL $ doubleUp c


$ ghc --make -fglasgow-exts -fallow-undecidable-instances -o listWithLength ListWithLength.hs
[1 of 1] Compiling Main             ( ListWithLength.hs, ListWithLength.o )

ListWithLength.hs:34:21:
    Couldn't match expected type `b' (a rigid variable)
           against inferred type `Zero'
      `b' is bound by the pattern for `AnyLWL'
            at ListWithLength.hs:34:12-24
    In the pattern: Nill
    In the pattern: AnyLWL (n@Nill)
    In the definition of `duAny_':
        duAny_ (AnyLWL (n@Nill)) = AnyLWL $ (doubleUp n)

Trac metadata

Trac field	Value
Version	6.6
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture