[GHC] #1573: GADT and typeclass funcional dependencies not working well together

[GHC]

#1573: GADT and typeclass funcional dependencies not working well together
---------------------------------------+------------------------------------
  Reporter:  matthew.pocock at ncl.ac.uk  |          Owner:       
      Type:  bug                       |         Status:  new  
  Priority:  normal                    |      Milestone:       
 Component:  Compiler                  |        Version:  6.6  
  Severity:  normal                    |       Keywords:       
Difficulty:  Unknown                   |             Os:  Linux
  Testcase:                            |   Architecture:  ia64 
---------------------------------------+------------------------------------
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 at 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 at Nill)
     In the definition of `duAny_':
         duAny_ (AnyLWL (n at Nill)) = AnyLWL $ (doubleUp n)
 }}}

-- 
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/1573>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler