Binding type variables that only occur in assertions

Question

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>

Answer 1

You are trying to intersect some set of instances of classes and for compiler there is no way to say that this intersection will be empty or single entry.
You want to force compiler to choose the right type for you without knowing which problems (information loss or complexity of calculations) that decision can bring in your program. If you want to do that you should give a hint to compiler what is the best type "a" for specific pair "s" and "b" (with us of that FunctionalDependencies you specified).

class E x a | x -> a
instance (S s Int, F Int CInt) => E (s, CInt) Int
f :: forall s a b . (E (s,b) a) => s -> b

Probably there is the way to specify order of preferred types of "a" for pair of "s" and "b" with further deduce of best "a" (i.e. use of type-level or something like that to attach that information).