I forgot the subject, sorry for reposting... I'm trying to apply the nested regions (as in Lightweight Monadic Regions by Oleg Kiselyov and Chung-chieh Shan) design pattern, if that's the proper term, in hope to gain a bit more type safety in this little library I'm working on (Streaming Component Combinators, available on Hackage). I guess the problem is that I'm getting too much type safety now, because I can't get the thing to compile. Most of the existing code works, the only exceptions seem to be various higher-order functions. I've reduced the problem to several lines of Literate Haskell code below, can anybody find a solution or confirm there isn't one?

{-# LANGUAGE EmptyDataDecls, Rank2Types #-} {-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, FlexibleInstances, IncoherentInstances #-} module Main where main = undefined

I'll call the main type, originally a monad transformer, simply Region. I'm leaving out the Monad and MonadTransformer instances, because they don't contribute to the problem. The parameter r is the phantom region type.

newtype Region r a = Region a

The Ancestor class is used to denote relationship between two regions where one is nested in another.

data Child r

class Ancestor r r'

instance Ancestor r (Child r) instance Ancestor r1 r2 => Ancestor r1 (Child r2)

Handle is a simple wrapper around a value. It carries information about the region that originates the value.

data Handle r x = Handle x

A typical calculation in the Region monad will take a bunch of Handles inherited from an Ancestor region and do something with them. The Ancestor constraint is there to ensure that the handles are not fake but genuinely inherited.

type SingleHandler x y = forall r1s rs. Ancestor r1s rs => Handle r1s x -> Region rs y type DoubleHandler x y z = forall r1d r2d rd. (Ancestor r1d rd, Ancestor r2d rd) => Handle r1d x -> Handle r2d y -> Region rd z

And now I get to the problem. The following higher-order function doesn't type-check:

mapD :: (SingleHandler x z -> SingleHandler y z) -> DoubleHandler x w z -> DoubleHandler y w z mapD f d = \y w-> f (\x-> d x w) y

I get the same error from GHC 6.8.2 and 6.8.2: Test.lhs:36:28: Could not deduce (Ancestor r2d rs) from the context (Ancestor r1s rs) arising from a use of `d' at Test.lhs:36:28-32 Possible fix: add (Ancestor r2d rs) to the context of the polymorphic type `forall r1s rs. (Ancestor r1s rs) => Handle r1s x -> Region rs z' In the expression: d x w In the first argument of `f', namely `(\ x -> d x w)' In the expression: f (\ x -> d x w) y The same code compiles just fine if all the Ancestor constraints are removed. I don't see any place to add the extra (Ancestor r2d rs) constraint, as GHC recommends. I think it ought to be able to figure things out based on the exisisting constraints, but I may be wrong: perhaps higher-order functions pose a fundamental problem for type-level programming. Can anybody shed any light on this?