Regression with type families in quantified constraints breaking inference
Summary
Given something like f :: forall a. ((forall b. C) => a) -> A
where C
's context mentions a type family,
f x
where x
's type isn't forall a. a
fails without a type application. f undefined
does OTOH still work.
This works for me in 9.0.2, but not since at least 9.2.3.
Steps to reproduce
import Data.Kind (Type, Constraint)
type family C :: Type
class (C ~ ()) => D where
f :: forall a. ((forall b. D) => a) -> ()
f _ = ()
x :: ()
x = f ()
Error:
Test.hs:19:7: error:
• Couldn't match expected type ‘a0’ with actual type ‘()’
• ‘a0’ is untouchable
inside the constraints: forall b. D
bound by a type expected by the context:
(forall b. D) => a0
at Test.hs:19:7-8
• In the first argument of ‘f’, namely ‘()’
In the expression: f ()
In an equation for ‘x’: x = f ()
|
19 | x = f ()
Expected behavior
This should work. The type of a
is obviously ()
.
Environment
- GHC version used: 9.2.4