Hi! I find it extremely difficult to describe my problem, so here goes nothing:

I have a bunch of assertions on the type of a function. These assertions rely on a type variable that is not used for any parameter of the function, but is only used for internal bindings. Whenever I use this function it does not compile because, of course, the compiler has no information from which to guess what type to bind my type variable. Here is the code:

{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, FlexibleInstances,
  UndecidableInstances, FlexibleContexts, EmptyDataDecls, ScopedTypeVariables,
  TypeOperators, TypeSynonymInstances #-}

class C a a'  where convert :: a -> a'
class F a b   where apply :: a -> b
class S s a   where select :: s -> a

data CInt = CInt Int

instance S (Int,String) Int where select (i,_) = i
instance F Int CInt where apply = CInt

f :: forall s a b . (S s a, F a b) => s -> b
f s = 
  let v = select s :: a
      y = apply v :: b
  in y

x :: Int
x = f (10,"Pippo")

And here is the generated error:

FunctorsProblems.hs:21:4:
    No instances for (F a Int, S (t, [Char]) a)
      arising from a use of `f' at FunctorsProblems.hs:21:4-17
    Possible fix:
      add an instance declaration for (F a Int, S (t, [Char]) a)
    In the expression: f (10, "Pippo")
    In the definition of `x': x = f (10, "Pippo")
Failed, modules loaded: none.
Prelude>