Bad error message around lack of impredicativity
(Broken out from #12557 (closed).)
foo :: ((forall a. f a) -> f r) -> f r foo g = undefined x = \g -> foo g
Compiling this code produces
Scratch.hs:24:15: error: • Couldn't match expected type ‘(forall (a :: k). f a) -> f r’ with actual type ‘t’ ‘t’ is a rigid type variable bound by the inferred type of x :: t -> f r at Scratch.hs:24:1-15 • In the first argument of ‘foo’, namely ‘g’ In the expression: foo g In the expression: \ g -> foo g • Relevant bindings include g :: t (bound at Scratch.hs:24:6) x :: t -> f r (bound at Scratch.hs:24:1)
The code should be rejected. But, really, the problem is that the type of a lambda-bound variable can't be a polytype (unless the type is obvious at the binding site). We should improve this error message.