RequiredTypeArguments doesn't interact with DeepSubsumption
While experimenting with RequiredTypeArguments
in GHC 9.10.1-alpha3, I discovered a surprising quirk that feels like a bug, although I'm not entirely sure. For context, suppose you have this program:
{-# LANGUAGE GHC2024 #-}
{-# LANGUAGE DeepSubsumption #-}
{-# LANGUAGE RequiredTypeArguments #-}
{-# LANGUAGE TypeAbstractions #-}
module Foo where
f1 :: () -> forall a. Eq a => a -> a -> Bool
f1 () @a = (==) @a
f2 :: () -> forall a. Ord a => a -> a -> Bool
f2 = f1
Note that f2
only typechecks due to DeepSubsumption
being enabled.
I decided to see what would happen if I turned the invisible forall a.
s to visible forall ->
s:
g1 :: () -> forall a -> Eq a => a -> a -> Bool
g1 () a = (==) @a
g2 :: () -> forall a -> Ord a => a -> a -> Bool
g2 = g1
Surprisingly, this doesn't typecheck:
$ ghc-9.10.0.20240413 Foo.hs
[1 of 1] Compiling Foo ( Foo.hs, Foo.o )
Foo.hs:17:6: error: [GHC-83865]
• Couldn't match type: Eq a
with: Ord a
Expected: forall a -> Ord a => a -> a -> Bool
Actual: forall a -> Eq a => a -> a -> Bool
• In the expression: g1
In an equation for ‘g2’: g2 = g1
|
17 | g2 = g1
| ^^
I would have expected DeepSubsumption
to allow g2
to typecheck, much in the same way that f2
typechecks. Note that g2 u = g1 u
also does not typecheck.