Add regression test for #17773

3 files changed, 32 insertions, 0 deletions

diff --git a/testsuite/tests/typecheck/should_fail/T17773.hs b/testsuite/tests/typecheck/should_fail/T17773.hs
new file mode 100644
index 0000000..f1fd17e
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T17773.hs
@@ -0,0 +1,16 @@
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+module Bug where
+
+import Data.Proxy (Proxy(..))
+import Data.Type.Equality ((:~:)(..))
+
+type family (x :: f a) <|> (y :: f a) :: f a
+type family Mzero :: f a
+
+monadPlusMplus :: forall f a (x :: f a) (y :: f a).
+                  Proxy x -> Proxy y
+               -> Mzero x y :~: (x <|> y)
+monadPlusMplus _ _ = _Refl
diff --git a/testsuite/tests/typecheck/should_fail/T17773.stderr b/testsuite/tests/typecheck/should_fail/T17773.stderr
new file mode 100644
index 0000000..5a6989a
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T17773.stderr
@@ -0,0 +1,15 @@
+
+T17773.hs:16:22: error:
+    • Found hole: _Refl :: Mzero x y :~: (x <|> y)
+      Where: ‘x’, ‘f’, ‘k’, ‘a’, ‘y’ are rigid type variables bound by
+               the type signature for:
+                 monadPlusMplus :: forall k (f :: k -> *) (a :: k) (x :: f a)
+                                          (y :: f a).
+                                   Proxy x -> Proxy y -> Mzero x y :~: (x <|> y)
+               at T17773.hs:(13,1)-(15,41)
+      Or perhaps ‘_Refl’ is mis-spelled, or not in scope
+    • In the expression: _Refl
+      In an equation for ‘monadPlusMplus’: monadPlusMplus _ _ = _Refl
+    • Relevant bindings include
+        monadPlusMplus :: Proxy x -> Proxy y -> Mzero x y :~: (x <|> y)
+          (bound at T17773.hs:16:1)
diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T
index f0f290c..156042c 100644
--- a/testsuite/tests/typecheck/should_fail/all.T
+++ b/testsuite/tests/typecheck/should_fail/all.T
@@ -552,3 +552,4 @@ test('T17563', normal, compile_fail, [''])
 test('T16946', normal, compile_fail, [''])
 test('T17566b', normal, compile_fail, [''])
 test('T17566c', normal, compile_fail, [''])
+test('T17773', normal, compile_fail, [''])