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 |