Skip to content

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