1 files changed, 43 insertions, 0 deletions
diff --git a/testsuite/tests/typecheck/should_fail/T17139.hs b/testsuite/tests/typecheck/should_fail/T17139.hs
index b4025588dd..4869e9559d 100644
--- a/testsuite/tests/typecheck/should_fail/T17139.hs
+++ b/testsuite/tests/typecheck/should_fail/T17139.hs
@@ -13,3 +13,46 @@ type family TypeFam f fun where
 
 lift :: (a -> b) -> TypeFam f (a -> b)
 lift f = \x -> _ (f <*> x)
+
+
+{-
+x              :: alpha
+body of lambda :: beta
+
+[W] TypeFam f (a->b) ~ (alpha -> beta)
+-->
+[W] (f a -> TypeFam f b) ~ (alpha -> beta)
+-->
+ alpha := f a
+ beta  := TypeFam f b
+
+(<*>) :: Applicative g => g (p -> q) -> g p -> g q
+
+f <*> x
+
+arg1
+  (a->b) ~ g0 (p0->q0)
+  g0 := ((->) a)
+  (p0 -> q0) ~ b   <---------
+arg2
+  alpha ~ g0 p0
+  g0 ~ f          <----------
+  p0 := a
+res
+  g0 q0
+
+Finish with
+ [W] f ~ (->) a
+ [W] b ~ (a -> q0)
+ --> rewrite b
+ [W] (a -> q0) ~ a -> (
+
+_ :: g0 q0 -> beta
+  :: (a -> q0) -> TypeFam f b
+  :: (a -> q0) -> TypeFam ((->) a) (a -> q0)
+  :: (a -> q0) -> (a->a) -> TypeFam (-> a) q0
+
+BUT we would get different error messages if we did
+   g0 := f
+and then encountered [W] g0 ~ ((->) a)
+-}
+\ No newline at end of file