Allow scoped type variables refer to types

This patch implements GHC proposal 29:
(sorry, URL is too long for the commit message linter)
and fixess #15050.

The change is simple: Just use a different meta variable form.

Test suite and documentation updated.

Differential Revision: https://phabricator.haskell.org/D4980

4 files changed, 1 insertions, 50 deletions

diff --git a/testsuite/tests/indexed-types/should_fail/T7786.hs b/testsuite/tests/indexed-types/should_compile/T7786.hs
index 33a74f233f..33a74f233f 100644
--- a/testsuite/tests/indexed-types/should_fail/T7786.hs
+++ b/testsuite/tests/indexed-types/should_compile/T7786.hs
diff --git a/testsuite/tests/indexed-types/should_compile/all.T b/testsuite/tests/indexed-types/should_compile/all.T
index 035c85d179..11b7bcbc16 100644
--- a/testsuite/tests/indexed-types/should_compile/all.T
+++ b/testsuite/tests/indexed-types/should_compile/all.T
@@ -280,6 +280,7 @@ test('T14237', normal, compile, [''])
 test('T14554', normal, compile, [''])
 test('T14680', normal, compile, [''])
 test('T15057', normal, compile, [''])
+test('T7786', normal, compile, [''])
 test('T15144', normal, compile, [''])
 test('T15122', normal, compile, [''])
 test('T13777', normal, compile, [''])
@@ -289,4 +290,3 @@ test('T15322', normal, compile, [''])
 test('T15322a', normal, compile_fail, [''])
 test('T15142', normal, compile, [''])
 test('T15352', normal, compile, [''])
-
diff --git a/testsuite/tests/indexed-types/should_fail/T7786.stderr b/testsuite/tests/indexed-types/should_fail/T7786.stderr
deleted file mode 100644
index a82a1ca2f7..0000000000
--- a/testsuite/tests/indexed-types/should_fail/T7786.stderr
+++ /dev/null
@@ -1,48 +0,0 @@
-
-T7786.hs:96:41: error:
-    • Couldn't match type ‘xxx’
-                     with ‘Intersect (BuriedUnder sub k 'Empty) inv’
-      Expected type: Maybe (Sing xxx)
-        Actual type: Maybe
-                       (Sing (Intersect (BuriedUnder sub k 'Empty) inv))
-    • In a stmt of a 'do' block: Nil :: Sing xxx <- foogle db k sub
-      In the expression:
-        do Nil :: Sing xxx <- foogle db k sub
-           return $ Sub db k sub
-      In an equation for ‘addSub’:
-          addSub db k sub
-            = do Nil :: Sing xxx <- foogle db k sub
-                 return $ Sub db k sub
-    • Relevant bindings include
-        sub :: Database sub (bound at T7786.hs:96:13)
-        k :: Sing k (bound at T7786.hs:96:11)
-        db :: Database inv (bound at T7786.hs:96:8)
-        addSub :: Database inv
-                  -> Sing k
-                  -> Database sub
-                  -> Maybe (Database (BuriedUnder sub k inv))
-          (bound at T7786.hs:96:1)
-
-T7786.hs:97:31: error:
-    • Could not deduce: Intersect (BuriedUnder sub k 'Empty) inv
-                        ~ 'Empty
-        arising from a use of ‘Sub’
-      from the context: xxx ~ 'Empty
-        bound by a pattern with constructor: Nil :: forall a. Sing 'Empty,
-                 in a pattern binding in
-                      a 'do' block
-        at T7786.hs:96:22-24
-    • In the second argument of ‘($)’, namely ‘Sub db k sub’
-      In a stmt of a 'do' block: return $ Sub db k sub
-      In the expression:
-        do Nil :: Sing xxx <- foogle db k sub
-           return $ Sub db k sub
-    • Relevant bindings include
-        sub :: Database sub (bound at T7786.hs:96:13)
-        k :: Sing k (bound at T7786.hs:96:11)
-        db :: Database inv (bound at T7786.hs:96:8)
-        addSub :: Database inv
-                  -> Sing k
-                  -> Database sub
-                  -> Maybe (Database (BuriedUnder sub k inv))
-          (bound at T7786.hs:96:1)
diff --git a/testsuite/tests/indexed-types/should_fail/all.T b/testsuite/tests/indexed-types/should_fail/all.T
index b8775554c9..11e9d0a65d 100644
--- a/testsuite/tests/indexed-types/should_fail/all.T
+++ b/testsuite/tests/indexed-types/should_fail/all.T
@@ -87,7 +87,6 @@ test('T7536', normal, compile_fail, [''])
 
 test('T7729', normal, compile_fail, [''])
 test('T7729a', normal, compile_fail, [''])
-test('T7786', normal, compile_fail, [''])
 
 test('NoGood', normal, compile_fail, [''])
 test('T7967', normal, compile_fail, [''])