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?