How can a functional type dependence be used to derive equality of type parameters?

Viewed 79

Consider the following code:

{-# LANGUAGE RankNTypes, MultiParamTypeClasses, FunctionalDependencies #-}

data St t = St
    {       use_t :: t
    }

class S s t | s -> t
    where   -- Nothing really

newtype P s = P
    {       unP :: forall b t. (S s t) =>
                    St t
            ->      (St t -> b)     -- pok
            ->      b
    }

f :: (S s t) => t -> P s
f t = P $ \s pok -> pok s { use_t = t }

The code looks contrived, but the idea is that the class S is used to express that the type parameter t is determined by the type parameter s, so I don't have to add t as a type parameter to the type P.

The above code however in short gives the following error Could not deduce (t1 ~ t) from the context (S s t) or from (S s t1). This error message suggests that the compiler wants to use either one or the other of these contexts, whereas I would have hoped it would use both and conclude t1 ~ t from them.

I would appreciate any suggestions to get this working without adding t as a type parameter to type P.

2 Answers
Related