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