[Haskell-cafe] understanding typeable

[Anatoly Yakovenko]

So I am getting a little further, but i am seeing this bizarre behaviour:

I wrote a function that will fold over parameters and push them into a
constructor if it can
given this type:

   data Foo = FooC Int
            | BarC Int
            deriving (Data, Typeable, Show)

i can do this:

   > let a::Maybe Foo = foldFunc (Just FooC) (params $ BarC 1)
   Loading package syb ... linking ... done.
   > a
   Just (FooC 1)

here is the implementation

   data Child = forall a. (Typeable a, Data a) => Child a

   params::(Data a) => a -> [Child]
   params = gmapQ Child

   --foldFunc :: (Typeable x, Data y) => (Maybe x) -> [Child] -> Maybe y
   --foldFunc :: forall y1 y.  (Typeable y1, Data y) => Maybe y1 ->
[Child] -> Maybe y
   foldFunc (Just ff) (ch:[]) = applyCtor ff ch
   foldFunc (Just ff) (ch:tt) = foldFunc (applyFunc ff ch) tt
   foldFunc Nothing _ = Nothing
   foldFunc (Just ff) [] = castObj ff
      where
         castObj::(Typeable y, Data x) => y -> (Maybe x)
         castObj = cast

   applyCtor :: (Typeable x, Data y) => x -> Child -> Maybe y
   applyCtor ff (Child ch) = do
      func <- castFunc ff
      return $ func ch
      where
         castFunc::(Typeable y, Data x, Data z) => y -> (Maybe (x -> z))
         castFunc = cast

   applyFunc :: (Typeable x, Typeable y) => x -> Child -> Maybe y
   applyFunc ff (Child ch) = do
      func <- castFunc ff
      return $ func ch
      where
         castFunc::(Typeable y, Data x, Typeable z) => y -> (Maybe (x -> z))
         castFunc = cast

now this is the weird part:

--foldFunc :: (Typeable x, Data y) => (Maybe x) -> [Child] -> Maybe y
--foldFunc :: forall y1 y.  (Typeable y1, Data y) => Maybe y1 ->
[Child] -> Maybe y

if i uncomment either one of those, (shouldn't they be equivalent?), i
get an error, the first one gives me

   ParseG.hs:44:39:
       Ambiguous type variable `x' in the constraint:
         `Typeable x'
           arising from a use of `applyFunc' at ParseG.hs:44:39-53
       Probable fix: add a type signature that fixes these type variable(s)
   Failed, modules loaded: none.

the second one gives me:

   ParseG.hs:46:24:
       Could not deduce (Data y1) from the context (Typeable y1, Data y)
         arising from a use of `castObj' at ParseG.hs:46:24-33
       Possible fix:
         add (Data y1) to the context of the type signature for `foldFunc'
       In the expression: castObj ff
       In the definition of `foldFunc':
           foldFunc (Just ff) []
                      = castObj ff
                      where
                          castObj :: (Typeable y, Data x) => y -> (Maybe x)
                          castObj = cast

   ParseG.hs:46:32:
       Couldn't match expected type `y' against inferred type `y1'
         `y' is a rigid type variable bound by
             the type signature for `foldFunc' at ParseG.hs:42:22
         `y1' is a rigid type variable bound by
              the type signature for `foldFunc' at ParseG.hs:42:19
       In the first argument of `castObj', namely `ff'
       In the expression: castObj ff
       In the definition of `foldFunc':
           foldFunc (Just ff) []
                      = castObj ff
                      where
                          castObj :: (Typeable y, Data x) => y -> (Maybe x)
                          castObj = cast
   Failed, modules loaded: none.

So they are not equivalent, so why is that so, and why is this the
type signature of the function if i dont give one:

   > :t foldFunc
   foldFunc :: forall y1 y.
               (Typeable y1, Data y) =>
               Maybe y1 -> [Child] -> Maybe y