Added a regression test, this would trigger a Core Lint error before GHC 9

2 files changed, 39 insertions, 0 deletions

diff --git a/testsuite/tests/impredicative/Dict.hs b/testsuite/tests/impredicative/Dict.hs
new file mode 100644
index 0000000000..0330784a69
--- /dev/null
+++ b/testsuite/tests/impredicative/Dict.hs
@@ -0,0 +1,38 @@
+-- This used to produce Core Lint errors
+
+{-# Language ConstraintKinds       #-}
+{-# Language DataKinds             #-}
+{-# Language FlexibleInstances     #-}
+{-# Language GADTs                 #-}
+{-# Language ImpredicativeTypes    #-}
+{-# Language KindSignatures        #-}
+{-# Language MultiParamTypeClasses #-}
+{-# Language PolyKinds             #-}
+{-# Language QuantifiedConstraints #-}
+{-# Language RankNTypes            #-}
+{-# Language TypeOperators         #-}
+{-# Language UndecidableInstances  #-}
+
+{-# Options_GHC -dcore-lint #-}
+
+module Dict where
+
+import Data.Kind (Type)
+import Data.Maybe (isJust, isNothing)
+import Data.Type.Equality ((:~:))
+
+data LoT k where
+  LoT0   :: LoT Type
+  (:&&:) :: k -> LoT ks -> LoT (k -> ks)
+
+data Dict cls where
+ Dict :: cls => Dict cls
+
+class GTE a b x y (f :: LoT kf -> Type) (g :: LoT kg -> Type) where
+  gTE :: f x -> g y -> Maybe (a :~: b)
+
+class    (forall a b. GTE a b (a :&&: LoT0) (b :&&: LoT0) rep rep) => As f rep
+instance (forall a b. GTE a b (a :&&: LoT0) (b :&&: LoT0) rep rep) => As f rep
+
+ok :: Dict (As f rep) -> Dict (forall a b. GTE a b (a :&&: LoT0) (b :&&: LoT0) rep rep)
+ok Dict = Dict
diff --git a/testsuite/tests/impredicative/all.T b/testsuite/tests/impredicative/all.T
index 2f23210f6b..2bd813de60 100644
--- a/testsuite/tests/impredicative/all.T
+++ b/testsuite/tests/impredicative/all.T
@@ -20,3 +20,4 @@ test('T7026', normal, compile, [''])
 test('T8808', normal, compile, [''])
 test('T17332', normal, compile_fail, [''])
 test('expr-sig', normal, compile, [''])
+test('Dict', normal, compile, [''])