Strange type equality solving failures with ImpredicativeTypes
Steps to reproduce
(I realize ImpredicativeTypes aren't really a feature at the moment, but reporting anyway since Simon wrote last week that tickets about it are still useful.)
:set -XImpredicativeTypes -XConstraintKinds -XGADTs -XAllowAmbiguousTypes
-- This typechecks
() :: ((Show a => Num a => Int) ~ ((Show a, Num a) => Int)) => ()
-- -> replace `Num a` with `(Eq a, Ord a)`
-- This doesn't typecheck
-- Couldn't match type ‘Ord a0 => Int’ with ‘Int’
() :: ((Show a => (Eq a, Ord a) => Int) ~ ((Show a, (Eq a, Ord a)) => Int)) => ()
type A a = (Eq a, Ord a)
-- This typechecks
() :: (Eq a, Ord a) ~ A a => ()
-- This doesn't typecheck
-- Couldn't match type ‘()’ with ‘Ord a0 -> ()’
() :: (A a => ()) ~ ((Eq a, Ord a) => ()) => ()
-- -> replace `Num a` with `A a` instead
-- This typechecks
() :: ((Show a => A a => Int) ~ ((Show a, A a) => Int)) => ()
-- Let's make a type synonym out of the entire constraint
type C c a = ((Show a => c => Int) ~ ((Show a, c) => Int))
-- Now all of these typecheck:
() :: C (Num a) a => ()
() :: C (Eq a, Ord a) a => ()
() :: C (A a) a => ()
-- This doesn't typecheck
() :: ((() => () => Int) ~ (((), ()) => Int)) => ()
-- Let's turn this constraint into a different type synonym
type B a b = ((a => b => Int) ~ ((a, b) => Int))
-- These both typecheck now:
() :: B (Show a) (Num a) => ()
() :: B () () => ()
This seems awfully inconsistent.
Expected behavior
All of these examples should typecheck.
Environment
- GHC version used: HEAD (8.9.0.20191012)