Consider this: type Super = forall a. [a] type Sub = forall b. b cast0 :: Sub -> Super cast0 s = s cast1a :: forall p. (Super -> p) -> (Sub -> p) cast1a sp x = sp x cast1b :: forall p. (Super -> p) -> (Sub -> p) cast1b sp = sp This compiles except for cast1b (ghc -c -fglasgow-exts): Occurs check: cannot construct the infinite type: a = [a] When generalising the type(s) for `cast1b' I get a similar result when I try a different Super and Sub: type Super = (?x :: Bool) => Int type Sub = Int Couldn't match expected type `Sub' against inferred type `Super' When matching `(?x::Bool) => Int' and `Int' Expected type: Sub -> p Inferred type: Super -> p In the expression: sp In either case, if cast1a compiles, shouldn't cast1b compile? -- Ashley Yakeley