QuantifiedConstraints don't work with equality constraints on type families
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).