Fix #19044 by tweaking unification in inst lookup

See Note [Infinitary substitution in lookup] in GHC.Core.InstEnv
and Note [Unification result] in GHC.Core.Unify.

Test case: typecheck/should_compile/T190{44,52}

Close #19044
Close #19052

3 files changed, 36 insertions, 0 deletions

diff --git a/testsuite/tests/typecheck/should_compile/T19044.hs b/testsuite/tests/typecheck/should_compile/T19044.hs
new file mode 100644
index 0000000000..ced7658582
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T19044.hs
@@ -0,0 +1,20 @@
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+module T19044 where
+
+class C a b where
+  m :: a -> b
+
+instance C a a where
+  m = id
+
+instance C a (Maybe a) where
+  m _ = Nothing
+
+f :: a -> Maybe a
+f = g
+  where
+    g x = h (m x) x
+
+h :: Maybe a -> a -> Maybe a
+h = const
diff --git a/testsuite/tests/typecheck/should_compile/T19052.hs b/testsuite/tests/typecheck/should_compile/T19052.hs
new file mode 100644
index 0000000000..4904d20b40
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T19052.hs
@@ -0,0 +1,14 @@
+{-# LANGUAGE AllowAmbiguousTypes, DataKinds, FlexibleInstances, KindSignatures, MultiParamTypeClasses, ScopedTypeVariables, TypeApplications, TypeFamilies, TypeOperators, UndecidableInstances #-}
+module Overlap where
+
+import Data.Kind (Type)
+
+class Sub (xs :: [Type]) (ys :: [Type]) where
+  subIndex :: Int
+instance {-# OVERLAPPING #-} Sub xs xs where
+  subIndex = 0
+instance (ys ~ (y ': ys'), Sub xs ys') => Sub xs ys where
+  subIndex = subIndex @xs @ys' + 1
+
+subIndex1 :: forall (x :: Type) (xs :: [Type]). Int
+subIndex1 = subIndex @xs @(x ': xs)
diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T
index f76741a447..3fc36839d8 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -734,6 +734,8 @@ test('T17186', normal, compile, [''])
 test('CbvOverlap', normal, compile, [''])
 test('InstanceGivenOverlap', normal, compile, [''])
 test('InstanceGivenOverlap2', normal, compile, [''])
+test('T19044', normal, compile, [''])
+test('T19052', normal, compile, [''])
 test('LocalGivenEqs', normal, compile, [''])
 test('LocalGivenEqs2', normal, compile, [''])
 test('T18891', normal, compile, [''])