Ashley Yakeley wrote:

If this were allowed, it would effectively allow type-lambda class C a b | a -> b instance C Int Bool instance C Bool Char

newtype T a = MkT (forall b.(C a b) => b) helperIn :: (forall b.(C a b) => b) -> T a helperIn b = MkT b; -- currently won't work helperOut :: T a -> (forall b.(C a b) => b) helperOut (MkT b) = b

And it does work (based on the code shown here previously):

class C a b | a -> b instance C Int Bool instance C Bool Char instance C Char Float instance C Float (Int->()) instance (C a b) => C (a->()) (b->())

newtype T a = T (forall b.(C a b) => b) data T1 a = T1 a (T a) xx b = case (T1 b (T undefined)) of T1 _ (T x) -> x

Ok, modules loaded: Main. *Main> :type xx$(1::Int) Bool *Main> :type xx$ xx$ (1::Int) Char *Main> :type xx$ xx$ xx$ (1::Int) Float *Main> :type xx$ xx$ xx$ xx$ (1::Int) Int -> () *Main> :type xx$ xx$ xx$ xx$ xx$ (1::Int) Bool -> () *Main> :type xx$ xx$ xx$ xx$ xx$ xx$ (1::Int) Char -> () *Main> :type xx$ xx$ xx$ xx$ xx$ xx$ xx$ (1::Int) Float -> () *Main> :type xx$ xx$ xx$ xx$ xx$ xx$ xx$ xx$ (1::Int) (Int -> ()) -> () *Main> :type xx$ xx$ xx$ xx$ xx$ xx$ xx$ xx$ xx$ (1::Int) (Bool -> ()) -> () *Main> :type xx$ xx$ xx$ xx$ xx$ xx$ xx$ xx$ xx$ xx$ (1::Int) (Char -> ()) -> () It seems it does compute.... The principle was to use constraints to force the "evaluation" of the type "lambda". Obtaining the type "lambda" was the thrust behind the exercise with existential and useless types. Perhaps I neglected to mention that point. We can use the Coerce type function (aka class) mentioned in the thread on first-class types to convert from the types computed by 'xx' to values. Incidentally, the class D was already a type function: the function 'meet'.