[Haskell-cafe] Problem when class function doesn't mention all type parameters or...

[Daniil Elovkov]

Hi again
So, I keep trying to implement the dsl, I mentioned yesterday. I ran
into a problem which can be illustrated by the following small
example.

> class Cl s1 a1 s2 a2 where
>    clF :: a1 -> a2

clF doesn't mention s1 and s2, they're used only to restrict types below

> data T s a where
>    C :: (Cl s1 a1 s2 a2) => T s1 a1 -> T s2 a2

> f :: T s a -> a
> f (C t) = let v = f t in clF v

This doesn't typecheck with the error
   Could not deduce (Cl s11 a1 s2 a) from the context (Cl s1 a1 s a)
   arising from use of `clF'

Here T depends on s, while the result of f doesn't. What happens is s gets lost.

I'm not sure if the problem is that stated in the subject, really.
But, I wonder how at all ghc should guess about s parameters.

Maybe if f were T s a -> (s,a) where s were never evaluated...
...but no, this

> f :: T s a -> (s,a)
> f (C t) = let (s,v) = f t in (s,clF v)

also fails to unify those s types.

Can someone sched some light, please?