1 files changed, 19 insertions, 0 deletions
diff --git a/testsuite/tests/indexed-types/should_compile/Refl2.hs b/testsuite/tests/indexed-types/should_compile/Refl2.hs
new file mode 100644
index 0000000000..b6f5d056b5
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/Refl2.hs
@@ -0,0 +1,19 @@
+{-# LANGUAGE TypeFamilies #-}
+
+module Refl2 where
+
+type family T (a :: * -> *) :: * -> *
+
+data U a x = U (T a x)
+
+mkU :: a x -> U a x
+mkU x = U undefined
+
+-- The first definition says "Could not deduce (T a x ~ T a x)", the other two
+-- work fine
+
+foo :: a x -> U a x
+foo x = case mkU x of U t -> id (U t)
+-- foo x = case mkU x of U t -> id ((U :: T a x -> U a x) t)
+-- foo x = case mkU x of U t -> U t
+