Hello, I am looking for a real world example of a type constructor, that expects another type constructor as an argument in the context of subtyping, e.g., one could define --not Haskell98 data T a b c = F (a b c) a::T (->) Pt Pt a = F id b::T (->) CPt CPt b = F id l = [a,b] Thereby CPt is assumed to be a subtype of Pt. From my expectations l should be typable [T (->) CPt Pt], because of contravariance of (->). Using c::T (Either) Pt Pt and d::T (Either) CPt CPt one would gain [c,d]::T (Either) Pt Pt. I need this "real world" example for the sake of motivation, that variance can be expressed by Haskell kinds, e.g., in a kind system the kind of T could be (a->b->*)->a->b->*. Thereby the "kind variables" a and b can be instantiated by "special kinds" + and -, that represent co- and contravariance, respectively. So one would have T (->)::- -> + -> * and T (Either)::+ -> + -> * and so on... Any ideas are very appreciated. Ciao, Steffen