Hello, assume I want to have the following function:
test :: (forall t . (forall a . t a) -> t b) -> b -> b test g x = g (\f y -> y) id x
This should be well-typed if the type constructor t is instantiated as follows: t c = forall d . (c->d) -> d -> d Of course, I don't expect type inference to detect this, so I give explicit annotations:
test :: (forall t . (forall a . t a) -> t b) -> b -> b test g x = (g :: (forall a . (forall d . (a->d) -> d -> d)) -> (forall e . (b->e) -> e -> e)) ((\f y -> y) :: (forall a . (forall d . (a->d) -> d -> d))) (id :: (b -> b)) (x :: b)
GHC 4.08 complains: Couldn't match `forall a d. (a -> d) -> d -> d' against `forall a. t a' Expected type: (forall a d. (a -> d) -> d -> d) -> (b -> e) -> e -> e Inferred type: (forall a. t a) -> t b1 In an expression with a type signature: g :: forall b. (forall a d. (a -> d) -> d -> d) -> forall e. (b -> e) -> e -> e Clearly, giving the annotations was not enough to make the type checker accept the program, since it still tries to perform a higher-order matching. But, how can I make explicit for which type constructor t (namely the one given above) I want to use g (which is polymorphic over t)? I guess, in polymorphic lambda calculus (where types are explicitly abstracted) I should be able to apply a polymorphic g to some concrete type to obtain an instance (does this also work for type constructors?). But, how to do it in Haskell? Note that it doesn't help me to choose another type for "test", because I'm interested in the "free theorem" for exactly the given type of g. Thanks for any hints! Regards, Janis. -- Janis Voigtlaender http://wwwtcs.inf.tu-dresden.de/~voigt/ mailto:voigt@tcs.inf.tu-dresden.de