Skip to content

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
Edited by Ziyang Liu
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information