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

Question

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.

Answer 1

You can't do it with the class as written. See Can I magic up type equality from a functional dependency?. But you can do it with a different class:

class t ~ T s => S s t where
  type T s :: *

You'll need to define T for each instance, but at least that's not hard. And you can provide a default definition of T if there's an appropriate one.