[commit: ghc] ghc-8.4: Add regression test for #14040 (0d40693)

[git at git.haskell.org]

Repository : ssh://git@git.haskell.org/ghc

On branch  : ghc-8.4
Link       : http://ghc.haskell.org/trac/ghc/changeset/0d40693654678e6a8ce8a63d198420c88e11dcff/ghc

>---------------------------------------------------------------

commit 0d40693654678e6a8ce8a63d198420c88e11dcff
Author: Ryan Scott <ryan.gl.scott at gmail.com>
Date:   Tue Dec 12 10:16:39 2017 -0500

    Add regression test for #14040
    
    This adds a regression test for the original program in #14040.
    
    This does not fix #14040 entirely, though, as the program in
    https://ghc.haskell.org/trac/ghc/ticket/14040#comment:2 still
    panics, so there is more work to be done there.
    
    (cherry picked from commit be1ca0e439e9d26107c7d82fe6e78b64ee6320a9)


>---------------------------------------------------------------

0d40693654678e6a8ce8a63d198420c88e11dcff
 .../tests/partial-sigs/should_fail/T14040a.hs      | 34 +++++++++++++++
 .../tests/partial-sigs/should_fail/T14040a.stderr  | 48 ++++++++++++++++++++++
 testsuite/tests/partial-sigs/should_fail/all.T     |  1 +
 3 files changed, 83 insertions(+)

diff --git a/testsuite/tests/partial-sigs/should_fail/T14040a.hs b/testsuite/tests/partial-sigs/should_fail/T14040a.hs
new file mode 100644
index 0000000..382e218
--- /dev/null
+++ b/testsuite/tests/partial-sigs/should_fail/T14040a.hs
@@ -0,0 +1,34 @@
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeInType #-}
+module T14040a where
+
+import Data.Kind
+
+data family Sing (a :: k)
+
+data WeirdList :: Type -> Type where
+  WeirdNil  :: WeirdList a
+  WeirdCons :: a -> WeirdList (WeirdList a) -> WeirdList a
+
+data instance Sing (z :: WeirdList a) where
+  SWeirdNil  :: Sing WeirdNil
+  SWeirdCons :: Sing w -> Sing wws -> Sing (WeirdCons w wws)
+
+elimWeirdList :: forall (a :: Type) (wl :: WeirdList a)
+                        (p :: forall (x :: Type). x -> WeirdList x -> Type).
+                 Sing wl
+              -> (forall (y :: Type). p _ WeirdNil)
+              -> (forall (z :: Type) (x :: z) (xs :: WeirdList (WeirdList z)).
+                    Sing x -> Sing xs -> p _ xs
+                  -> p _ (WeirdCons x xs))
+              -> p _ wl
+elimWeirdList SWeirdNil pWeirdNil _ = pWeirdNil
+elimWeirdList (SWeirdCons (x :: Sing (x :: z))
+                          (xs :: Sing (xs :: WeirdList (WeirdList z))))
+              pWeirdNil pWeirdCons
+  = pWeirdCons @z @x @xs x xs
+      (elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons)
diff --git a/testsuite/tests/partial-sigs/should_fail/T14040a.stderr b/testsuite/tests/partial-sigs/should_fail/T14040a.stderr
new file mode 100644
index 0000000..b4f0e26
--- /dev/null
+++ b/testsuite/tests/partial-sigs/should_fail/T14040a.stderr
@@ -0,0 +1,48 @@
+
+T14040a.hs:21:18: error:
+    • The kind of variable ‘wl1’, namely ‘WeirdList a1’,
+      depends on variable ‘a1’ from an inner scope
+      Perhaps bind ‘wl1’ sometime after binding ‘a1’
+    • In the type signature:
+        elimWeirdList :: forall (a :: Type)
+                                (wl :: WeirdList a)
+                                (p :: forall (x :: Type). x -> WeirdList x -> Type).
+                         Sing wl
+                         -> (forall (y :: Type). p _ WeirdNil)
+                            -> (forall (z :: Type) (x :: z) (xs :: WeirdList (WeirdList z)).
+                                Sing x -> Sing xs -> p _ xs -> p _ (WeirdCons x xs))
+                               -> p _ wl
+
+T14040a.hs:34:8: error:
+    • Cannot apply expression of type ‘Sing wl
+                                       -> (forall y. p x0 w0 'WeirdNil)
+                                       -> (forall z1 (x :: z1) (xs :: WeirdList (WeirdList z1)).
+                                           Sing x
+                                           -> Sing xs
+                                           -> p (WeirdList z1) w1 xs
+                                           -> p z1 w2 ('WeirdCons x xs))
+                                       -> p a w3 wl’
+      to a visible type argument ‘(WeirdList z)’
+    • In the sixth argument of ‘pWeirdCons’, namely
+        ‘(elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons)’
+      In the expression:
+        pWeirdCons
+          @z
+          @x
+          @xs
+          x
+          xs
+          (elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons)
+      In an equation for ‘elimWeirdList’:
+          elimWeirdList
+            (SWeirdCons (x :: Sing (x :: z))
+                        (xs :: Sing (xs :: WeirdList (WeirdList z))))
+            pWeirdNil
+            pWeirdCons
+            = pWeirdCons
+                @z
+                @x
+                @xs
+                x
+                xs
+                (elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons)
diff --git a/testsuite/tests/partial-sigs/should_fail/all.T b/testsuite/tests/partial-sigs/should_fail/all.T
index 36ea6cb..b974ce8 100644
--- a/testsuite/tests/partial-sigs/should_fail/all.T
+++ b/testsuite/tests/partial-sigs/should_fail/all.T
@@ -64,6 +64,7 @@ test('PatBind3', normal, compile_fail, [''])
 test('T12039', normal, compile_fail, [''])
 test('T12634', normal, compile_fail, [''])
 test('T12732', normal, compile_fail, ['-fobject-code -fdefer-typed-holes'])
+test('T14040a', normal, compile_fail, [''])
 test('T14449', normal, compile_fail, [''])
 test('T14479', normal, compile_fail, [''])
 test('T14584', normal, compile, [''])