GitLab

I'm quite confident that this is a duplicate of some prior issue (#14860?), but this is different enough from all tickets I skimmed so far. This program is rejected:

{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE KindSignatures #-}

module Lib where

data T a = T a
type family F a

x :: (forall a. T a ~ F a) => F Int
x = T 42

src.hs:10:6: error:
    • Couldn't match type ‘F a’ with ‘T a’
    • In the ambiguity check for ‘x’
      To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
      In the type signature: x :: (forall a. T a ~ F a) => F Int
   |
10 | x :: (forall a. T a ~ F a) => F Int
   |      ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

And I'm unsure why. In my head this should just work.

@matheus23 and I would really like to use it in !2315 (closed) to generalise constraints of the form XRec pass (HsExpr pass) ~ Located (HsExpr pass) (generalise over the syntactic entity HsExpr pass, that is).