Inconsistency in reporting skolem escapes
This program:
{-# LANGUAGE ExistentialQuantification #-}
module Foo where
data A = forall a. A a
f (A x) = Just x
leads to a sensible skolem escape error:
• Couldn't match expected type ‘p’ with actual type ‘Maybe a’
because type variable ‘a’ would escape its scope
This (rigid, skolem) type variable is bound by
a pattern with constructor: A :: forall a. a -> A,
in an equation for ‘f’
...
But if f
is changed to
f (A x) = x
then the error message becomes
• Couldn't match expected type ‘p’ with actual type ‘a’
‘a’ is a rigid type variable bound by
a pattern with constructor: A :: forall a. a -> A,
in an equation for ‘f’
at Foo.hs:7:4-6
‘p’ is a rigid type variable bound by
the inferred type of f :: A -> p
...
Apparently, in the second case the inferred type of f
is forall p. A -> p
, hence p
is rigid; while in the first case p
is a unification variable that unifies with Maybe a
.
The second error message is a bit confusing since it is not clear why f
is inferred to have type forall p. A -> p
. Is it possible to make it report skolem escape as well?
Environment
- GHC version used: 8.10.2