ImpredicativeTypes Type Inference Failure with Misleading Error Message

Summary

ImpredicativeTypes can sometimes give misleading error messages where it cannot resolve ambiguity.

Steps to reproduce

{-# LANGUAGE ImpredicativeTypes #-}

import Data.Kind (Type)

type Exis (f :: (a -> Type)) = forall r. (forall x. f x -> r) -> r

exis :: c p -> Exis c
exis x c = c x

newtype Foo a =
  Foo a

tmp :: Exis Foo
tmp = exis (Foo 3)

-- Succeeds
tmp2 :: Exis Foo
tmp2 = (tmp :: (forall x. Foo x -> Exis Foo) -> Exis Foo) exis

-- Fails
tmp2b :: Exis Foo
tmp2b = tmp exis

Trying to compile this code will output:

error:
    * Couldn't match type: forall r1. (forall x1. Foo x1 -> r1) -> r1
                     with: (forall x1. Foo x1 -> r) -> r
      Expected: Foo x -> (forall x1. Foo x1 -> r) -> r
        Actual: Foo x -> Exis Foo
    * In the first argument of `tmp', namely `exis'
      In the expression: tmp exis
      In an equation for `tmp2b': tmp2b = tmp exis
    * Relevant bindings include
        tmp2b :: (forall x. Foo x -> r) -> r
          (bound at HaskellHasASkillIssue.hs:24:1)
   |
24 | tmp2b = tmp exis
   |             ^^^^
Failed, no modules loaded.

Expected behavior

Either correctly inferring the type of r in tmp (and not outputting an error), or giving a better error message. The provided error message seems to imply that the code simply does not typecheck, while it really is a case where GHC cannot resolve the ambiguity.

Environment

• GHC version used: 9.4.4