1 files changed, 38 insertions, 0 deletions
diff --git a/testsuite/tests/indexed-types/should_compile/GADT12.hs b/testsuite/tests/indexed-types/should_compile/GADT12.hs
new file mode 100644
index 0000000000..4eb5124c1d
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/GADT12.hs
@@ -0,0 +1,38 @@
+{-# LANGUAGE TypeFamilies, GADTs, ScopedTypeVariables, KindSignatures #-}
+{-# LANGUAGE EmptyDataDecls #-}
+
+-- Tests whether a type signature can refine a type
+-- See the definition of bug2a
+
+module ShouldCompile where
+
+data Typed
+data Untyped
+
+type family TU a b :: *
+type instance TU Typed b = b
+type instance TU Untyped b = ()
+
+-- A type witness type, use eg. for pattern-matching on types
+data Type a where
+    TypeInt     :: Type Int
+    TypeBool    :: Type Bool
+    TypeString  :: Type String
+    TypeList    :: Type t -> Type [t]
+
+data Expr :: * -> * -> * {- tu a -} where
+    Const :: Type a -> a -> Expr tu (TU tu a)
+    Var2  :: String -> TU tu (Type a) -> Expr tu (TU tu a)
+
+bug1 :: Expr Typed Bool -> ()
+bug1 (Const TypeBool False) = ()
+
+bug2a :: Expr Typed Bool -> ()
+bug2a (Var2 "x" (TypeBool :: Type Bool)) = ()
+
+bug2c :: Expr Typed Bool -> ()
+bug2c (Var2 "x" TypeBool) = ()
+
+bug2b :: Expr Typed (TU Typed Bool) -> ()
+bug2b (Var2 "x" TypeBool) = ()
+