From 8e15e3d370e9c253ae0dbb330e25b72cb00cdb76 Mon Sep 17 00:00:00 2001
From: Richard Eisenberg <rae@cs.brynmawr.edu>
Date: Thu, 1 Jun 2017 17:27:14 -0400
Subject: Improve error messages around kind mismatches.

Previously, when canonicalizing (or unifying, in uType) a
heterogeneous equality, we emitted a kind equality and used the
resulting coercion to cast one side of the heterogeneous equality.

While sound, this led to terrible error messages. (See the bugs
listed below.) The problem is that using the coercion built from
the emitted kind equality is a bit like a wanted rewriting a wanted.
The solution is to keep heterogeneous equalities as irreducible.

See Note [Equalities with incompatible kinds] in TcCanonical.

This commit also removes a highly suspicious switch to FM_SubstOnly
when flattening in the kinds of a type variable. I have no idea
why this was there, other than as a holdover from pre-TypeInType.
I've not left a Note because there is simply no reason I can conceive
of that the FM_SubstOnly should be there.

One challenge with this patch is that the emitted derived equalities
might get emitted several times: when a heterogeneous equality is
in an implication and then gets floated out from the implication,
the Derived is present both in and out of the implication. This
causes a duplicate error message. (Test case:
typecheck/should_fail/T7368) Solution: track the provenance of
Derived constraints and refuse to float out a constraint that has
an insoluble Derived.

Lastly, this labels one test (dependent/should_fail/RAE_T32a)
as expect_broken, because the problem is really #12919. The
different handling of constraints in this patch exposes the error.

This fixes bugs #11198, #12373, #13530, and #13610.

test cases:
typecheck/should_fail/{T8262,T8603,tcail122,T12373,T13530,T13610}
---
 testsuite/tests/dependent/should_fail/T11471.hs     |  2 +-
 testsuite/tests/dependent/should_fail/T11471.stderr | 11 +++++++----
 testsuite/tests/dependent/should_fail/all.T         |  2 +-
 3 files changed, 9 insertions(+), 6 deletions(-)

(limited to 'testsuite/tests/dependent')

diff --git a/testsuite/tests/dependent/should_fail/T11471.hs b/testsuite/tests/dependent/should_fail/T11471.hs
index 19025db22b..ae09ae07bb 100644
--- a/testsuite/tests/dependent/should_fail/T11471.hs
+++ b/testsuite/tests/dependent/should_fail/T11471.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE MagicHash, PolyKinds, TypeFamilies #-}
+{-# LANGUAGE MagicHash, PolyKinds, TypeFamilies, AllowAmbiguousTypes #-}
 
 module T11471 where
 
diff --git a/testsuite/tests/dependent/should_fail/T11471.stderr b/testsuite/tests/dependent/should_fail/T11471.stderr
index 80c5fc606c..640ae6c754 100644
--- a/testsuite/tests/dependent/should_fail/T11471.stderr
+++ b/testsuite/tests/dependent/should_fail/T11471.stderr
@@ -1,19 +1,22 @@
 
 T11471.hs:15:10: error:
     • Couldn't match a lifted type with an unlifted type
-      Expected type: Proxy Int#
+      When matching types
+        a :: *
+        Int# :: TYPE 'IntRep
+      Expected type: Proxy a
         Actual type: Proxy Int#
-      Use -fprint-explicit-kinds to see the kind arguments
     • In the first argument of ‘f’, namely ‘(undefined :: Proxy Int#)’
       In the expression: f (undefined :: Proxy Int#) 3#
       In an equation for ‘bad’: bad = f (undefined :: Proxy Int#) 3#
+    • Relevant bindings include bad :: F a (bound at T11471.hs:15:1)
 
 T11471.hs:15:35: error:
     • Couldn't match a lifted type with an unlifted type
       When matching types
-        F Int# :: *
+        F a :: *
         Int# :: TYPE 'IntRep
     • In the second argument of ‘f’, namely ‘3#’
       In the expression: f (undefined :: Proxy Int#) 3#
       In an equation for ‘bad’: bad = f (undefined :: Proxy Int#) 3#
-    • Relevant bindings include bad :: F Int# (bound at T11471.hs:15:1)
+    • Relevant bindings include bad :: F a (bound at T11471.hs:15:1)
diff --git a/testsuite/tests/dependent/should_fail/all.T b/testsuite/tests/dependent/should_fail/all.T
index c648f9ed1d..af3efc6716 100644
--- a/testsuite/tests/dependent/should_fail/all.T
+++ b/testsuite/tests/dependent/should_fail/all.T
@@ -1,5 +1,5 @@
 test('DepFail1', normal, compile_fail, [''])
-test('RAE_T32a', normal, compile_fail, [''])
+test('RAE_T32a', expect_broken(12919), compile_fail, [''])
 test('TypeSkolEscape', normal, compile_fail, [''])
 test('BadTelescope', normal, compile_fail, [''])
 test('BadTelescope2', normal, compile_fail, [''])
-- 
cgit v1.2.1


From 1696dbf4ad0fda4d7c5b4afe1911cab51d7dd0b0 Mon Sep 17 00:00:00 2001
From: Richard Eisenberg <rae@cs.brynmawr.edu>
Date: Tue, 18 Jul 2017 19:44:17 -0400
Subject: Fix #12176 by being a bit more careful instantiating.

Previously, looking up a TyCon that said "no" to mightBeUnsaturated
would then instantiate all of its invisible binders. But this is
wrong for vanilla type synonyms, whose RHS kind might legitimately
start with invisible binders. So a little more care is taken now,
only to instantiate those invisible binders that need to be (so that
the TyCon isn't unsaturated).
---
 testsuite/tests/dependent/should_compile/T12176.hs | 18 ++++++++++++++++++
 testsuite/tests/dependent/should_compile/all.T     |  1 +
 2 files changed, 19 insertions(+)
 create mode 100644 testsuite/tests/dependent/should_compile/T12176.hs

(limited to 'testsuite/tests/dependent')

diff --git a/testsuite/tests/dependent/should_compile/T12176.hs b/testsuite/tests/dependent/should_compile/T12176.hs
new file mode 100644
index 0000000000..0e340068a7
--- /dev/null
+++ b/testsuite/tests/dependent/should_compile/T12176.hs
@@ -0,0 +1,18 @@
+{-# LANGUAGE RankNTypes, TypeInType, GADTs, TypeFamilies #-}
+
+module T12176 where
+
+import Data.Kind
+
+data Proxy :: forall k. k -> Type where
+  MkProxy :: forall k (a :: k). Proxy a
+
+data X where
+  MkX :: forall (k :: Type) (a :: k). Proxy a -> X
+
+type Expr = (MkX :: forall (a :: Bool). Proxy a -> X)
+
+type family Foo (x :: forall (a :: k). Proxy a -> X) where
+  Foo (MkX :: forall (a :: k). Proxy a -> X) = (MkProxy :: Proxy k)
+
+type Bug = Foo Expr  -- this failed with #12176
diff --git a/testsuite/tests/dependent/should_compile/all.T b/testsuite/tests/dependent/should_compile/all.T
index 8a9b221a4e..b854f1d9e7 100644
--- a/testsuite/tests/dependent/should_compile/all.T
+++ b/testsuite/tests/dependent/should_compile/all.T
@@ -24,3 +24,4 @@ test('T11719', normal, compile, [''])
 test('T11966', normal, compile, [''])
 test('T12442', normal, compile, [''])
 test('T13538', normal, compile, [''])
+test('T12176', normal, compile, [''])
-- 
cgit v1.2.1


From 424ecadbb3d06f4d4e0813de670369893e1da2a9 Mon Sep 17 00:00:00 2001
From: Ryan Scott <ryan.gl.scott@gmail.com>
Date: Fri, 28 Jul 2017 11:47:38 -0400
Subject: Add regression tests for #13601, #13780, #13877

Summary:
Some recent commits happened to fix other issues:

* c2417b87ff59c92fbfa8eceeff2a0d6152b11a47 fixed #13601 and #13780
* 8e15e3d370e9c253ae0dbb330e25b72cb00cdb76 fixed the original program in #13877

Let's add regression tests for each of these to ensure they stay fixed.

Test Plan: make test TEST="T13601 T13780a T13780c T13877"

Reviewers: goldfire, bgamari, austin

Reviewed By: bgamari

Subscribers: rwbarton, thomie

GHC Trac Issues: #13601, #13780, #13877

Differential Revision: https://phabricator.haskell.org/D3794
---
 testsuite/tests/dependent/should_fail/T13601.hs    | 47 ++++++++++++++++++++++
 .../tests/dependent/should_fail/T13601.stderr      |  6 +++
 testsuite/tests/dependent/should_fail/T13780a.hs   |  9 +++++
 .../tests/dependent/should_fail/T13780a.stderr     |  6 +++
 testsuite/tests/dependent/should_fail/T13780b.hs   | 10 +++++
 testsuite/tests/dependent/should_fail/T13780c.hs   | 12 ++++++
 .../tests/dependent/should_fail/T13780c.stderr     | 12 ++++++
 testsuite/tests/dependent/should_fail/all.T        |  4 ++
 8 files changed, 106 insertions(+)
 create mode 100644 testsuite/tests/dependent/should_fail/T13601.hs
 create mode 100644 testsuite/tests/dependent/should_fail/T13601.stderr
 create mode 100644 testsuite/tests/dependent/should_fail/T13780a.hs
 create mode 100644 testsuite/tests/dependent/should_fail/T13780a.stderr
 create mode 100644 testsuite/tests/dependent/should_fail/T13780b.hs
 create mode 100644 testsuite/tests/dependent/should_fail/T13780c.hs
 create mode 100644 testsuite/tests/dependent/should_fail/T13780c.stderr

(limited to 'testsuite/tests/dependent')

diff --git a/testsuite/tests/dependent/should_fail/T13601.hs b/testsuite/tests/dependent/should_fail/T13601.hs
new file mode 100644
index 0000000000..5e98c7a657
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T13601.hs
@@ -0,0 +1,47 @@
+{-# LANGUAGE TypeFamilies, DataKinds, TypeInType #-}
+
+import GHC.Exts
+import Prelude (Bool(True,False),Integer,Ordering,undefined)
+import qualified Prelude
+import Data.Kind
+
+--------------------
+-- class hierarchy
+
+type family
+  Rep (rep :: RuntimeRep) :: RuntimeRep where
+  -- Rep IntRep         = IntRep
+  -- Rep DoubleRep      = IntRep
+  -- Rep PtrRepUnlifted = IntRep
+  -- Rep PtrRepLifted   = PtrRepLifted
+
+class Boolean (Logic a) => Eq (a :: TYPE rep) where
+  type Logic (a :: TYPE rep) :: TYPE (Rep rep)
+  (==) :: a -> a -> Logic a
+
+class Eq a => POrd (a :: TYPE rep) where
+  inf :: a -> a -> a
+
+class POrd a => MinBound (a :: TYPE rep) where
+  minBound :: () -> a
+
+class POrd a => Lattice (a :: TYPE rep) where
+  sup :: a -> a -> a
+
+class (Lattice a, MinBound a) => Bounded (a :: TYPE rep) where
+  maxBound :: () -> a
+
+class Bounded a => Complemented (a :: TYPE rep) where
+  not :: a -> a
+
+class Bounded a => Heyting (a :: TYPE rep) where
+  infixr 3 ==>
+  (==>) :: a -> a -> a
+
+class (Complemented a, Heyting a) => Boolean a
+
+(||) :: Boolean a => a -> a -> a
+(||) = sup
+
+(&&) :: Boolean a => a -> a -> a
+(&&) = inf
diff --git a/testsuite/tests/dependent/should_fail/T13601.stderr b/testsuite/tests/dependent/should_fail/T13601.stderr
new file mode 100644
index 0000000000..c1c9803e5a
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T13601.stderr
@@ -0,0 +1,6 @@
+
+T13601.hs:18:16: error:
+    • Expected kind ‘TYPE (Rep 'LiftedRep)’,
+        but ‘Logic a’ has kind ‘TYPE (Rep rep)’
+    • In the first argument of ‘Boolean’, namely ‘(Logic a)’
+      In the class declaration for ‘Eq’
diff --git a/testsuite/tests/dependent/should_fail/T13780a.hs b/testsuite/tests/dependent/should_fail/T13780a.hs
new file mode 100644
index 0000000000..1f7c95c40a
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T13780a.hs
@@ -0,0 +1,9 @@
+{-# LANGUAGE ExistentialQuantification #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeInType #-}
+module T13780a where
+
+data family Sing (a :: k)
+
+data Foo a = a ~ Bool => MkFoo
+data instance Sing (z :: Foo a) = (z ~ MkFoo) => SMkFoo
diff --git a/testsuite/tests/dependent/should_fail/T13780a.stderr b/testsuite/tests/dependent/should_fail/T13780a.stderr
new file mode 100644
index 0000000000..3b113bd89e
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T13780a.stderr
@@ -0,0 +1,6 @@
+
+T13780a.hs:9:40: error:
+    • Expected kind ‘Foo a’, but ‘MkFoo’ has kind ‘Foo Bool’
+    • In the second argument of ‘(~)’, namely ‘MkFoo’
+      In the definition of data constructor ‘SMkFoo’
+      In the data instance declaration for ‘Sing’
diff --git a/testsuite/tests/dependent/should_fail/T13780b.hs b/testsuite/tests/dependent/should_fail/T13780b.hs
new file mode 100644
index 0000000000..238e7a1af9
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T13780b.hs
@@ -0,0 +1,10 @@
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeInType #-}
+module T13780b where
+
+data family Sing (a :: k)
+
+data instance Sing (z :: Bool) =
+    z ~ False => SFalse
+  | z ~ True  => STrue
diff --git a/testsuite/tests/dependent/should_fail/T13780c.hs b/testsuite/tests/dependent/should_fail/T13780c.hs
new file mode 100644
index 0000000000..eee6436237
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T13780c.hs
@@ -0,0 +1,12 @@
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeInType #-}
+module T13780c where
+
+import Data.Kind
+import T13780b
+
+type family ElimBool (p :: Bool -> Type) (b :: Bool) (s :: Sing b)
+                     (pFalse :: p False) (pTrue :: p True) :: p b where
+  ElimBool _ _ SFalse pFalse _ = pFalse
+  ElimBool _ _ STrue  _ pTrue  = pTrue
diff --git a/testsuite/tests/dependent/should_fail/T13780c.stderr b/testsuite/tests/dependent/should_fail/T13780c.stderr
new file mode 100644
index 0000000000..f91d7a3236
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T13780c.stderr
@@ -0,0 +1,12 @@
+[1 of 2] Compiling T13780b          ( T13780b.hs, T13780b.o )
+[2 of 2] Compiling T13780c          ( T13780c.hs, T13780c.o )
+
+T13780c.hs:11:16: error:
+    • Expected kind ‘Sing _’, but ‘SFalse’ has kind ‘Sing 'False’
+    • In the third argument of ‘ElimBool’, namely ‘SFalse’
+      In the type family declaration for ‘ElimBool’
+
+T13780c.hs:12:16: error:
+    • Expected kind ‘Sing _1’, but ‘STrue’ has kind ‘Sing 'True’
+    • In the third argument of ‘ElimBool’, namely ‘STrue’
+      In the type family declaration for ‘ElimBool’
diff --git a/testsuite/tests/dependent/should_fail/all.T b/testsuite/tests/dependent/should_fail/all.T
index af3efc6716..4eb426419d 100644
--- a/testsuite/tests/dependent/should_fail/all.T
+++ b/testsuite/tests/dependent/should_fail/all.T
@@ -17,3 +17,7 @@ test('T11471', normal, compile_fail, [''])
 test('T12174', normal, compile_fail, [''])
 test('T12081', normal, compile_fail, [''])
 test('T13135', normal, compile_fail, [''])
+test('T13601', normal, compile_fail, [''])
+test('T13780a', normal, compile_fail, [''])
+test('T13780c', [extra_files(['T13780b.hs'])],
+                multimod_compile_fail, ['T13780c', ''])
-- 
cgit v1.2.1


From 969928602aa7b23bcaffe0dbfa885ffce87cea02 Mon Sep 17 00:00:00 2001
From: Gabor Greif <ggreif@gmail.com>
Date: Fri, 28 Jul 2017 20:36:59 +0200
Subject: Typofixes [ci skip]

---
 testsuite/tests/dependent/should_fail/T13135.hs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'testsuite/tests/dependent')

diff --git a/testsuite/tests/dependent/should_fail/T13135.hs b/testsuite/tests/dependent/should_fail/T13135.hs
index c39b3f5842..772ac78bfa 100644
--- a/testsuite/tests/dependent/should_fail/T13135.hs
+++ b/testsuite/tests/dependent/should_fail/T13135.hs
@@ -62,7 +62,7 @@ arrLen = smartSym sym where
 
 
 
-{- The original bug was a familure to subsitute
+{- The original bug was a failure to substitute
    properly during type-function improvement.
 
 --------------------------------------
-- 
cgit v1.2.1


From 3b686879dd60250e084852c620864d7651f1a771 Mon Sep 17 00:00:00 2001
From: Richard Eisenberg <rae@cs.brynmawr.edu>
Date: Tue, 8 Aug 2017 18:20:42 -0400
Subject: Test #14038 in dependent/should_compile/T14038

---
 testsuite/tests/dependent/should_compile/T14038.hs | 75 ++++++++++++++++++++++
 testsuite/tests/dependent/should_compile/all.T     |  1 +
 2 files changed, 76 insertions(+)
 create mode 100644 testsuite/tests/dependent/should_compile/T14038.hs

(limited to 'testsuite/tests/dependent')

diff --git a/testsuite/tests/dependent/should_compile/T14038.hs b/testsuite/tests/dependent/should_compile/T14038.hs
new file mode 100644
index 0000000000..839220a0ce
--- /dev/null
+++ b/testsuite/tests/dependent/should_compile/T14038.hs
@@ -0,0 +1,75 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE ExistentialQuantification #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE TypeOperators #-}
+module T14038 where
+
+import Data.Kind (Type)
+
+data family Sing (a :: k)
+data instance Sing (z :: [a]) where
+  SNil  :: Sing '[]
+  SCons :: Sing x -> Sing xs -> Sing (x:xs)
+
+data TyFun :: Type -> Type -> Type
+type a ~> b = TyFun a b -> Type
+infixr 0 ~>
+
+type family Apply (f :: k1 ~> k2) (x :: k1) :: k2
+type a @@ b = Apply a b
+infixl 9 @@
+
+data FunArrow = (:->) -- ^ '(->)'
+              | (:~>) -- ^ '(~>)'
+
+class FunType (arr :: FunArrow) where
+  type Fun (k1 :: Type) arr (k2 :: Type) :: Type
+
+class FunType arr => AppType (arr :: FunArrow) where
+  type App k1 arr k2 (f :: Fun k1 arr k2) (x :: k1) :: k2
+
+type FunApp arr = (FunType arr, AppType arr)
+
+instance FunType (:->) where
+  type Fun k1 (:->) k2 = k1 -> k2
+
+instance AppType (:->) where
+  type App k1 (:->) k2 (f :: k1 -> k2) x = f x
+
+instance FunType (:~>) where
+  type Fun k1 (:~>) k2 = k1 ~> k2
+
+instance AppType (:~>) where
+  type App k1 (:~>) k2 (f :: k1 ~> k2) x = f @@ x
+
+infixr 0 -?>
+type (-?>) (k1 :: Type) (k2 :: Type) (arr :: FunArrow) = Fun k1 arr k2
+
+elimList :: forall (a :: Type) (p :: [a] -> Type) (l :: [a]).
+            Sing l
+         -> p '[]
+         -> (forall (x :: a) (xs :: [a]). Sing x -> Sing xs -> p xs -> p (x:xs))
+         -> p l
+elimList = elimListPoly @(:->)
+
+elimListTyFun :: forall (a :: Type) (p :: [a] ~> Type) (l :: [a]).
+                 Sing l
+              -> p @@ '[]
+              -> (forall (x :: a) (xs :: [a]). Sing x -> Sing xs -> p @@ xs -> p @@ (x:xs))
+              -> p @@ l
+elimListTyFun = elimListPoly @(:~>) @_ @p
+
+elimListPoly :: forall (arr :: FunArrow) (a :: Type) (p :: ([a] -?> Type) arr) (l :: [a]).
+                FunApp arr
+             => Sing l
+             -> App [a] arr Type p '[]
+             -> (forall (x :: a) (xs :: [a]). Sing x -> Sing xs -> App [a] arr Type p xs -> App [a] arr Type p (x:xs))
+             -> App [a] arr Type p l
+elimListPoly SNil                      pNil _     = pNil
+elimListPoly (SCons x (xs :: Sing xs)) pNil pCons = pCons x xs (elimListPoly @arr @a @p @xs xs pNil pCons)
diff --git a/testsuite/tests/dependent/should_compile/all.T b/testsuite/tests/dependent/should_compile/all.T
index b854f1d9e7..a13589280c 100644
--- a/testsuite/tests/dependent/should_compile/all.T
+++ b/testsuite/tests/dependent/should_compile/all.T
@@ -25,3 +25,4 @@ test('T11966', normal, compile, [''])
 test('T12442', normal, compile, [''])
 test('T13538', normal, compile, [''])
 test('T12176', normal, compile, [''])
+test('T14038', expect_broken(14038), compile, [''])
-- 
cgit v1.2.1


From c813d8c9776b2c57ec90ab29e1cc0b687fbb9c34 Mon Sep 17 00:00:00 2001
From: Richard Eisenberg <rae@cs.brynmawr.edu>
Date: Tue, 15 Aug 2017 14:52:53 -0400
Subject: Regression test for #12742

Location: dependent/should_compile/T12742
---
 testsuite/tests/dependent/should_compile/T12742.hs | 11 +++++++++++
 testsuite/tests/dependent/should_compile/all.T     |  1 +
 2 files changed, 12 insertions(+)
 create mode 100644 testsuite/tests/dependent/should_compile/T12742.hs

(limited to 'testsuite/tests/dependent')

diff --git a/testsuite/tests/dependent/should_compile/T12742.hs b/testsuite/tests/dependent/should_compile/T12742.hs
new file mode 100644
index 0000000000..baa3e2c071
--- /dev/null
+++ b/testsuite/tests/dependent/should_compile/T12742.hs
@@ -0,0 +1,11 @@
+{-# LANGUAGE TypeInType, RankNTypes, TypeFamilies #-}
+
+module T12742 where
+
+import Data.Kind
+
+type family F :: forall k2. (k1, k2)
+
+data T :: (forall k2. (Bool, k2)) -> Type
+
+type S = T F
diff --git a/testsuite/tests/dependent/should_compile/all.T b/testsuite/tests/dependent/should_compile/all.T
index a13589280c..774cdce625 100644
--- a/testsuite/tests/dependent/should_compile/all.T
+++ b/testsuite/tests/dependent/should_compile/all.T
@@ -26,3 +26,4 @@ test('T12442', normal, compile, [''])
 test('T13538', normal, compile, [''])
 test('T12176', normal, compile, [''])
 test('T14038', expect_broken(14038), compile, [''])
+test('T12742', normal, compile, [''])
-- 
cgit v1.2.1


From e5beb6ecac1497972fd538fd9a60c75e9279d68f Mon Sep 17 00:00:00 2001
From: Richard Eisenberg <rae@cs.brynmawr.edu>
Date: Wed, 16 Aug 2017 10:43:41 -0400
Subject: Make rejigConRes do kind substitutions

This was a lurking bug discovered on the hunt for #13910, but
it doesn't fix that bug. The old version of rejigConRes was
just wrong, forgetting to propagate a kind-change.
---
 testsuite/tests/dependent/should_compile/T13910.hs | 147 +++++++++++++++++++++
 testsuite/tests/dependent/should_compile/all.T     |   1 +
 2 files changed, 148 insertions(+)
 create mode 100644 testsuite/tests/dependent/should_compile/T13910.hs

(limited to 'testsuite/tests/dependent')

diff --git a/testsuite/tests/dependent/should_compile/T13910.hs b/testsuite/tests/dependent/should_compile/T13910.hs
new file mode 100644
index 0000000000..82d47e45bc
--- /dev/null
+++ b/testsuite/tests/dependent/should_compile/T13910.hs
@@ -0,0 +1,147 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE Trustworthy #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeFamilyDependencies #-}
+{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE TypeOperators #-}
+module T13910 where
+
+import Data.Kind
+import Data.Type.Equality
+
+data family Sing (a :: k)
+
+class SingKind k where
+  type Demote k = (r :: *) | r -> k
+  fromSing :: Sing (a :: k) -> Demote k
+  toSing   :: Demote k -> SomeSing k
+
+data SomeSing k where
+  SomeSing :: Sing (a :: k) -> SomeSing k
+
+withSomeSing :: forall k r
+              . SingKind k
+             => Demote k
+             -> (forall (a :: k). Sing a -> r)
+             -> r
+withSomeSing x f =
+  case toSing x of
+    SomeSing x' -> f x'
+
+data TyFun :: * -> * -> *
+type a ~> b = TyFun a b -> *
+infixr 0 ~>
+
+type family Apply (f :: k1 ~> k2) (x :: k1) :: k2
+type a @@ b = Apply a b
+infixl 9 @@
+
+data FunArrow = (:->) | (:~>)
+
+class FunType (arr :: FunArrow) where
+  type Fun (k1 :: Type) arr (k2 :: Type) :: Type
+
+class FunType arr => AppType (arr :: FunArrow) where
+  type App k1 arr k2 (f :: Fun k1 arr k2) (x :: k1) :: k2
+
+type FunApp arr = (FunType arr, AppType arr)
+
+instance FunType (:->) where
+  type Fun k1 (:->) k2 = k1 -> k2
+
+$(return []) -- This is only necessary for GHC 8.0 -- GHC 8.2 is smarter
+
+instance AppType (:->) where
+  type App k1 (:->) k2 (f :: k1 -> k2) x = f x
+
+instance FunType (:~>) where
+  type Fun k1 (:~>) k2 = k1 ~> k2
+
+$(return [])
+
+instance AppType (:~>) where
+  type App k1 (:~>) k2 (f :: k1 ~> k2) x = f @@ x
+
+infixr 0 -?>
+type (-?>) (k1 :: Type) (k2 :: Type) (arr :: FunArrow) = Fun k1 arr k2
+
+data instance Sing (z :: a :~: b) where
+  SRefl :: Sing Refl
+
+instance SingKind (a :~: b) where
+  type Demote (a :~: b) = a :~: b
+  fromSing SRefl = Refl
+  toSing Refl = SomeSing SRefl
+
+(~>:~:) :: forall (k :: Type) (a :: k) (b :: k) (r :: a :~: b) (p :: forall (y :: k). a :~: y ~> Type).
+           Sing r
+        -> p @@ Refl
+        -> p @@ r
+(~>:~:) SRefl pRefl = pRefl
+
+type WhyReplacePoly (arr :: FunArrow) (from :: t) (p :: (t -?> Type) arr)
+                    (y :: t) (e :: from :~: y) = App t arr Type p y
+data WhyReplacePolySym (arr :: FunArrow) (from :: t) (p :: (t -?> Type) arr)
+  :: forall (y :: t). from :~: y ~> Type
+type instance Apply (WhyReplacePolySym arr from p :: from :~: y ~> Type) x
+  = WhyReplacePoly arr from p y x
+
+replace :: forall (t :: Type) (from :: t) (to :: t) (p :: t -> Type).
+           p from
+        -> from :~: to
+        -> p to
+replace = replacePoly @(:->)
+
+replaceTyFun :: forall (t :: Type) (from :: t) (to :: t) (p :: t ~> Type).
+                p @@ from
+             -> from :~: to
+             -> p @@ to
+replaceTyFun = replacePoly @(:~>) @_ @_ @_ @p
+
+replacePoly :: forall (arr :: FunArrow) (t :: Type) (from :: t) (to :: t)
+                      (p :: (t -?> Type) arr).
+               FunApp arr
+            => App t arr Type p from
+            -> from :~: to
+            -> App t arr Type p to
+replacePoly from eq =
+  withSomeSing eq $ \(singEq :: Sing r) ->
+    (~>:~:) @t @from @to @r @(WhyReplacePolySym arr from p) singEq from
+
+type WhyLeibnizPoly (arr :: FunArrow) (f :: (t -?> Type) arr) (a :: t) (z :: t)
+  = App t arr Type f a -> App t arr Type f z
+data WhyLeibnizPolySym (arr :: FunArrow) (f :: (t -?> Type) arr) (a :: t)
+  :: t ~> Type
+type instance Apply (WhyLeibnizPolySym arr f a) z = WhyLeibnizPoly arr f a z
+
+leibnizPoly :: forall (arr :: FunArrow) (t :: Type) (f :: (t -?> Type) arr)
+                      (a :: t) (b :: t).
+               FunApp arr
+            => a :~: b
+            -> App t arr Type f a
+            -> App t arr Type f b
+leibnizPoly = replaceTyFun @t @a @b @(WhyLeibnizPolySym arr f a) id
+
+leibniz :: forall (t :: Type) (f :: t -> Type) (a :: t) (b :: t).
+           a :~: b
+        -> f a
+        -> f b
+leibniz = replaceTyFun @t @a @b @(WhyLeibnizPolySym (:->) f a) id
+-- The line above is what you get if you inline the definition of leibnizPoly.
+-- It causes a panic, however.
+--
+-- An equivalent implementation is commented out below, which does *not*
+-- cause GHC to panic.
+--
+-- leibniz = leibnizPoly @(:->)
+
+leibnizTyFun :: forall (t :: Type) (f :: t ~> Type) (a :: t) (b :: t).
+                a :~: b
+             -> f @@ a
+             -> f @@ b
+leibnizTyFun = leibnizPoly @(:~>) @_ @f
diff --git a/testsuite/tests/dependent/should_compile/all.T b/testsuite/tests/dependent/should_compile/all.T
index 774cdce625..bb21df7db1 100644
--- a/testsuite/tests/dependent/should_compile/all.T
+++ b/testsuite/tests/dependent/should_compile/all.T
@@ -27,3 +27,4 @@ test('T13538', normal, compile, [''])
 test('T12176', normal, compile, [''])
 test('T14038', expect_broken(14038), compile, [''])
 test('T12742', normal, compile, [''])
+test('T13910', expect_broken(13910), compile, [''])
-- 
cgit v1.2.1


From 86e1db7d6850144d6e86dfb33eb0819205f6904c Mon Sep 17 00:00:00 2001
From: Richard Eisenberg <rae@cs.brynmawr.edu>
Date: Wed, 16 Aug 2017 11:49:49 -0400
Subject: Test #13938, with expect_broken

test case: dependent/should_compile/T13938
---
 testsuite/tests/dependent/should_compile/T13938.hs | 80 ++++++++++++++++++++++
 testsuite/tests/dependent/should_compile/all.T     |  1 +
 2 files changed, 81 insertions(+)
 create mode 100644 testsuite/tests/dependent/should_compile/T13938.hs

(limited to 'testsuite/tests/dependent')

diff --git a/testsuite/tests/dependent/should_compile/T13938.hs b/testsuite/tests/dependent/should_compile/T13938.hs
new file mode 100644
index 0000000000..3ba9e273e4
--- /dev/null
+++ b/testsuite/tests/dependent/should_compile/T13938.hs
@@ -0,0 +1,80 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE ExistentialQuantification #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE TypeOperators #-}
+module T13938 where
+
+import Data.Kind (Type)
+
+data family Sing (a :: k)
+data instance Sing (z :: [a]) where
+  SNil  :: Sing '[]
+  SCons :: Sing x -> Sing xs -> Sing (x:xs)
+
+data TyFun :: Type -> Type -> Type
+type a ~> b = TyFun a b -> Type
+infixr 0 ~>
+
+type family Apply (f :: k1 ~> k2) (x :: k1) :: k2
+type a @@ b = Apply a b
+infixl 9 @@
+
+data FunArrow = (:->) -- ^ '(->)'
+              | (:~>) -- ^ '(~>)'
+
+class FunType (arr :: FunArrow) where
+  type Fun (k1 :: Type) arr (k2 :: Type) :: Type
+
+class FunType arr => AppType (arr :: FunArrow) where
+  type App k1 arr k2 (f :: Fun k1 arr k2) (x :: k1) :: k2
+
+type FunApp arr = (FunType arr, AppType arr)
+
+instance FunType (:->) where
+  type Fun k1 (:->) k2 = k1 -> k2
+
+$(return []) -- This is only necessary for GHC 8.0 -- GHC 8.2 is smarter
+
+instance AppType (:->) where
+  type App k1 (:->) k2 (f :: k1 -> k2) x = f x
+
+instance FunType (:~>) where
+  type Fun k1 (:~>) k2 = k1 ~> k2
+
+$(return [])
+
+instance AppType (:~>) where
+  type App k1 (:~>) k2 (f :: k1 ~> k2) x = f @@ x
+
+infixr 0 -?>
+type (-?>) (k1 :: Type) (k2 :: Type) (arr :: FunArrow) = Fun k1 arr k2
+
+elimList :: forall (a :: Type) (p :: [a] -> Type) (l :: [a]).
+            Sing l
+         -> p '[]
+         -> (forall (x :: a) (xs :: [a]). Sing x -> Sing xs -> p xs -> p (x:xs))
+         -> p l
+elimList = elimListPoly @(:->)
+
+elimListTyFun :: forall (a :: Type) (p :: [a] ~> Type) (l :: [a]).
+                 Sing l
+              -> p @@ '[]
+              -> (forall (x :: a) (xs :: [a]). Sing x -> Sing xs -> p @@ xs -> p @@ (x:xs))
+              -> p @@ l
+elimListTyFun = elimListPoly @(:~>) @_ @p
+
+elimListPoly :: forall (arr :: FunArrow) (a :: Type) (p :: ([a] -?> Type) arr) (l :: [a]).
+                FunApp arr
+             => Sing l
+             -> App [a] arr Type p '[]
+             -> (forall (x :: a) (xs :: [a]). Sing x -> Sing xs -> App [a] arr Type p xs -> App [a] arr Type p (x:xs))
+             -> App [a] arr Type p l
+elimListPoly SNil                      pNil _     = pNil
+elimListPoly (SCons x (xs :: Sing xs)) pNil pCons = pCons x xs (elimListPoly @arr @a @p @xs xs pNil pCons)
diff --git a/testsuite/tests/dependent/should_compile/all.T b/testsuite/tests/dependent/should_compile/all.T
index bb21df7db1..684602cc94 100644
--- a/testsuite/tests/dependent/should_compile/all.T
+++ b/testsuite/tests/dependent/should_compile/all.T
@@ -28,3 +28,4 @@ test('T12176', normal, compile, [''])
 test('T14038', expect_broken(14038), compile, [''])
 test('T12742', normal, compile, [''])
 test('T13910', expect_broken(13910), compile, [''])
+test('T13938', expect_broken(13938), compile, [''])
-- 
cgit v1.2.1


From 7aa000b625c677534c87da43de31c27a2b969183 Mon Sep 17 00:00:00 2001
From: Richard Eisenberg <rae@cs.brynmawr.edu>
Date: Tue, 15 Aug 2017 17:22:50 -0400
Subject: Fix #13391 by checking for kind-GADTs

The check is a bit gnarly, but I couldn't think of a better way.
See the new code in TcTyClsDecls.

test case: polykinds/T13391
---
 testsuite/tests/dependent/should_compile/Dep2.hs               | 2 +-
 testsuite/tests/dependent/should_compile/KindEqualities.hs     | 6 ++++--
 testsuite/tests/dependent/should_compile/KindEqualities.stderr | 2 +-
 3 files changed, 6 insertions(+), 4 deletions(-)

(limited to 'testsuite/tests/dependent')

diff --git a/testsuite/tests/dependent/should_compile/Dep2.hs b/testsuite/tests/dependent/should_compile/Dep2.hs
index 34be3cffc6..df1cb51e08 100644
--- a/testsuite/tests/dependent/should_compile/Dep2.hs
+++ b/testsuite/tests/dependent/should_compile/Dep2.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE PolyKinds, GADTs #-}
+{-# LANGUAGE TypeInType, GADTs #-}
 
 module Dep2 where
 
diff --git a/testsuite/tests/dependent/should_compile/KindEqualities.hs b/testsuite/tests/dependent/should_compile/KindEqualities.hs
index 1f2e82c302..4cba8281ca 100644
--- a/testsuite/tests/dependent/should_compile/KindEqualities.hs
+++ b/testsuite/tests/dependent/should_compile/KindEqualities.hs
@@ -1,8 +1,10 @@
-{-# LANGUAGE PolyKinds, GADTs, ExplicitForAll #-}
+{-# LANGUAGE TypeInType, GADTs, ExplicitForAll #-}
 {-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
 
 module KindEqualities where
 
+import Data.Kind
+
 data TyRep1 :: * -> * where
   TyInt1 :: TyRep1 Int
   TyBool1 :: TyRep1 Bool
@@ -13,7 +15,7 @@ zero1 TyBool1 = False
 
 data Proxy (a :: k) = P
 
-data TyRep :: k -> * where
+data TyRep :: forall k. k -> * where
   TyInt :: TyRep Int
   TyBool :: TyRep Bool
   TyMaybe :: TyRep Maybe
diff --git a/testsuite/tests/dependent/should_compile/KindEqualities.stderr b/testsuite/tests/dependent/should_compile/KindEqualities.stderr
index af429d106b..ad9562eae8 100644
--- a/testsuite/tests/dependent/should_compile/KindEqualities.stderr
+++ b/testsuite/tests/dependent/should_compile/KindEqualities.stderr
@@ -1,5 +1,5 @@
 
-KindEqualities.hs:23:1: warning: [-Wincomplete-patterns (in -Wextra)]
+KindEqualities.hs:25:1: warning: [-Wincomplete-patterns (in -Wextra)]
     Pattern match(es) are non-exhaustive
     In an equation for ‘zero’:
         Patterns not matched: (TyApp (TyApp _ _) _)
-- 
cgit v1.2.1


From e3dbb44f53b2f9403d20d84e27f187062755a089 Mon Sep 17 00:00:00 2001
From: Richard Eisenberg <rae@cs.brynmawr.edu>
Date: Thu, 3 Aug 2017 15:18:39 -0400
Subject: Fix #12919 by making the flattener homegeneous.

This changes a key invariant of the flattener. Previously,
flattening a type meant flattening its kind as well. But now,
flattening is always homogeneous -- that is, the kind of the
flattened type is the same as the kind of the input type.
This is achieved by various wizardry in the TcFlatten.flatten_many
function, as described in Note [flatten_many].

There are several knock-on effects, including some refactoring
in the canonicalizer to take proper advantage of the flattener's
changed behavior. In particular, the tyvar case of can_eq_nc' no
longer needs to take casts into account.

Another effect is that flattening a tyconapp might change it
into a casted tyconapp. This might happen if the result kind
of the tycon contains a variable, and that variable changes
during flattening. Because the flattener is homogeneous, it tacks
on a cast to keep the tyconapp kind the same. However, this
is problematic when flattening CFunEqCans, which need to have
an uncasted tyconapp on the LHS and must remain homogeneous.
The solution is a more involved canCFunEqCan, described in
Note [canCFunEqCan].

This patch fixes #13643 (as tested in typecheck/should_compile/T13643)
and the panic in typecheck/should_compile/T13822 (as reported in #14024).
Actually, there were two bugs in T13822: the first was just some
incorrect logic in tryFill (part of the unflattener) -- also fixed
in this patch -- and the other was the main bug fixed in this ticket.

The changes in this patch exposed a long-standing flaw in OptCoercion,
in that breaking apart an AppCo sometimes has unexpected effects on
kinds. See new Note [EtaAppCo] in OptCoercion, which explains the
problem and fix.

Also here is a reversion of the major change in
09bf135ace55ce2572bf4168124d631e386c64bb, affecting ctEvCoercion.
It turns out that making the flattener homogeneous changes the
invariants on the algorithm, making the change in that patch
no longer necessary.

This patch also fixes:
  #14038 (dependent/should_compile/T14038)
  #13910 (dependent/should_compile/T13910)
  #13938 (dependent/should_compile/T13938)
  #14441 (typecheck/should_compile/T14441)
  #14556 (dependent/should_compile/T14556)
  #14720 (dependent/should_compile/T14720)
  #14749 (typecheck/should_compile/T14749)

Sadly, this patch negatively affects performance of type-family-
heavy code. The following patch fixes these performance degradations.
However, the performance fixes are somewhat invasive and so I've
kept them as a separate patch, labeling this one as [skip ci] so
that validation doesn't fail on the performance cases.
---
 testsuite/tests/dependent/should_compile/T14556.hs | 38 +++++++++++++++++++
 testsuite/tests/dependent/should_compile/T14720.hs | 44 ++++++++++++++++++++++
 testsuite/tests/dependent/should_compile/all.T     |  8 ++--
 .../tests/dependent/should_fail/RAE_T32a.stderr    | 25 ++++++------
 testsuite/tests/dependent/should_fail/all.T        |  2 +-
 5 files changed, 100 insertions(+), 17 deletions(-)
 create mode 100644 testsuite/tests/dependent/should_compile/T14556.hs
 create mode 100644 testsuite/tests/dependent/should_compile/T14720.hs

(limited to 'testsuite/tests/dependent')

diff --git a/testsuite/tests/dependent/should_compile/T14556.hs b/testsuite/tests/dependent/should_compile/T14556.hs
new file mode 100644
index 0000000000..eebbdca888
--- /dev/null
+++ b/testsuite/tests/dependent/should_compile/T14556.hs
@@ -0,0 +1,38 @@
+{-# Language UndecidableInstances, DataKinds, TypeOperators, KindSignatures, PolyKinds, TypeInType, TypeFamilies, GADTs, LambdaCase, ScopedTypeVariables #-}
+
+module T14556 where
+
+import Data.Kind
+import Data.Proxy
+
+data Fn a b where
+  IdSym :: Fn Type Type
+
+type family
+  (@@) (f::Fn k k') (a::k)::k' where
+  IdSym @@ a = a
+
+data KIND = X | FNARR KIND KIND
+
+data TY :: KIND -> Type where
+  ID    :: TY (FNARR X X)
+  FNAPP :: TY (FNARR k k') -> TY k -> TY k'
+
+data TyRep (kind::KIND) :: TY kind -> Type where
+  TID    :: TyRep (FNARR X X)  ID
+  TFnApp :: TyRep (FNARR k k') f
+         -> TyRep k            a
+         -> TyRep k'           (FNAPP f a)
+
+type family
+  IK (kind::KIND) :: Type where
+  IK X            = Type
+  IK (FNARR k k') = Fn (IK k) (IK k')
+
+type family
+  IT (ty::TY kind) :: IK kind where
+  IT ID          = IdSym
+  IT (FNAPP f x) = IT f @@ IT x
+
+zero :: TyRep X a -> IT a
+zero = undefined
diff --git a/testsuite/tests/dependent/should_compile/T14720.hs b/testsuite/tests/dependent/should_compile/T14720.hs
new file mode 100644
index 0000000000..c26a184689
--- /dev/null
+++ b/testsuite/tests/dependent/should_compile/T14720.hs
@@ -0,0 +1,44 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE DefaultSignatures #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE TypeOperators #-}
+module T14720 where
+
+import Data.Kind (Type)
+import Data.Type.Equality ((:~:)(..), sym, trans)
+import Data.Void
+
+data family Sing (z :: k)
+
+class Generic (a :: Type) where
+    type Rep a :: Type
+    from :: a -> Rep a
+    to :: Rep a -> a
+
+class PGeneric (a :: Type) where
+  type PFrom (x :: a)     :: Rep a
+  type PTo   (x :: Rep a) :: a
+
+class SGeneric k where
+  sFrom :: forall (a :: k).     Sing a -> Sing (PFrom a)
+  sTo   :: forall (a :: Rep k). Sing a -> Sing (PTo a :: k)
+
+class (PGeneric k, SGeneric k) => VGeneric k where
+  sTof  :: forall (a :: k).     Sing a -> PTo (PFrom a) :~: a
+  sFot  :: forall (a :: Rep k). Sing a -> PFrom (PTo a :: k) :~: a
+
+data Decision a = Proved a
+                | Disproved (a -> Void)
+
+class SDecide k where
+  (%~) :: forall (a :: k) (b :: k). Sing a -> Sing b -> Decision (a :~: b)
+  default (%~) :: forall (a :: k) (b :: k). (VGeneric k, SDecide (Rep k))
+               => Sing a -> Sing b -> Decision (a :~: b)
+  s1 %~ s2 = case sFrom s1 %~ sFrom s2 of
+    Proved (Refl :: PFrom a :~: PFrom b) ->
+      case (sTof s1, sTof s2) of
+          (Refl, Refl) -> Proved Refl
+    Disproved contra -> Disproved (\Refl -> contra Refl)
diff --git a/testsuite/tests/dependent/should_compile/all.T b/testsuite/tests/dependent/should_compile/all.T
index 684602cc94..ab7ab3c8df 100644
--- a/testsuite/tests/dependent/should_compile/all.T
+++ b/testsuite/tests/dependent/should_compile/all.T
@@ -25,7 +25,9 @@ test('T11966', normal, compile, [''])
 test('T12442', normal, compile, [''])
 test('T13538', normal, compile, [''])
 test('T12176', normal, compile, [''])
-test('T14038', expect_broken(14038), compile, [''])
+test('T14038', normal, compile, [''])
 test('T12742', normal, compile, [''])
-test('T13910', expect_broken(13910), compile, [''])
-test('T13938', expect_broken(13938), compile, [''])
+test('T13910', normal, compile, [''])
+test('T13938', normal, compile, [''])
+test('T14556', normal, compile, [''])
+test('T14720', normal, compile, [''])
diff --git a/testsuite/tests/dependent/should_fail/RAE_T32a.stderr b/testsuite/tests/dependent/should_fail/RAE_T32a.stderr
index cb94dd2854..046a1e1aa4 100644
--- a/testsuite/tests/dependent/should_fail/RAE_T32a.stderr
+++ b/testsuite/tests/dependent/should_fail/RAE_T32a.stderr
@@ -1,19 +1,18 @@
 
 RAE_T32a.hs:28:1: error:
-    Too many parameters to Sing:
-      x is unexpected;
-      expected only two parameters
-    In the data instance declaration for ‘Sing’
+    • Expected kind ‘k0 -> *’,
+        but ‘Sing Sigma (Sigma p r)’ has kind ‘*’
+    • In the data instance declaration for ‘Sing’
 
 RAE_T32a.hs:28:20: error:
-    Expecting two more arguments to ‘Sigma’
-    Expected a type, but
-    ‘Sigma’ has kind
-    ‘forall p -> TyPi p (MkStar p) -> *’
-    In the first argument of ‘Sing’, namely ‘Sigma’
-    In the data instance declaration for ‘Sing’
+    • Expecting two more arguments to ‘Sigma’
+      Expected a type, but
+      ‘Sigma’ has kind
+      ‘forall p -> TyPi p (MkStar p) -> *’
+    • In the first argument of ‘Sing’, namely ‘Sigma’
+      In the data instance declaration for ‘Sing’
 
 RAE_T32a.hs:28:27: error:
-    Expected kind ‘Sigma’, but ‘Sigma p r’ has kind ‘*’
-    In the second argument of ‘Sing’, namely ‘(Sigma p r)’
-    In the data instance declaration for ‘Sing’
+    • Expected kind ‘Sigma’, but ‘Sigma p r’ has kind ‘*’
+    • In the second argument of ‘Sing’, namely ‘(Sigma p r)’
+      In the data instance declaration for ‘Sing’
diff --git a/testsuite/tests/dependent/should_fail/all.T b/testsuite/tests/dependent/should_fail/all.T
index 4eb426419d..e28b2df5cd 100644
--- a/testsuite/tests/dependent/should_fail/all.T
+++ b/testsuite/tests/dependent/should_fail/all.T
@@ -1,5 +1,5 @@
 test('DepFail1', normal, compile_fail, [''])
-test('RAE_T32a', expect_broken(12919), compile_fail, [''])
+test('RAE_T32a', normal, compile_fail, [''])
 test('TypeSkolEscape', normal, compile_fail, [''])
 test('BadTelescope', normal, compile_fail, [''])
 test('BadTelescope2', normal, compile_fail, [''])
-- 
cgit v1.2.1


From 3ebf05f5410a3e89d4dc6d451aea5020706fa5b0 Mon Sep 17 00:00:00 2001
From: Ryan Scott <ryan.gl.scott@gmail.com>
Date: Tue, 27 Mar 2018 08:52:15 -0400
Subject: Fix the test for #13938

Only half of the test files were checked in for T13938.
This commit adds the missing half.
---
 testsuite/tests/dependent/should_compile/Makefile  |  5 ++
 testsuite/tests/dependent/should_compile/T13938.hs | 82 ++++------------------
 .../tests/dependent/should_compile/T13938a.hs      | 80 +++++++++++++++++++++
 testsuite/tests/dependent/should_compile/all.T     |  3 +-
 4 files changed, 102 insertions(+), 68 deletions(-)
 create mode 100644 testsuite/tests/dependent/should_compile/T13938a.hs

(limited to 'testsuite/tests/dependent')

diff --git a/testsuite/tests/dependent/should_compile/Makefile b/testsuite/tests/dependent/should_compile/Makefile
index 9101fbd40a..0f855180c0 100644
--- a/testsuite/tests/dependent/should_compile/Makefile
+++ b/testsuite/tests/dependent/should_compile/Makefile
@@ -1,3 +1,8 @@
 TOP=../../..
 include $(TOP)/mk/boilerplate.mk
 include $(TOP)/mk/test.mk
+
+T13938:
+	$(RM) T13938a.hi T13938a.o T13938.hi T13938.o
+	'$(TEST_HC)' $(TEST_HC_OPTS) -O -c T13938a.hs
+	'$(TEST_HC)' $(TEST_HC_OPTS) -O -c T13938.hs
diff --git a/testsuite/tests/dependent/should_compile/T13938.hs b/testsuite/tests/dependent/should_compile/T13938.hs
index 3ba9e273e4..dd4f3d6c7c 100644
--- a/testsuite/tests/dependent/should_compile/T13938.hs
+++ b/testsuite/tests/dependent/should_compile/T13938.hs
@@ -1,80 +1,28 @@
 {-# LANGUAGE AllowAmbiguousTypes #-}
-{-# LANGUAGE ConstraintKinds #-}
-{-# LANGUAGE ExistentialQuantification #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE TemplateHaskell #-}
 {-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeInType #-}
 {-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
 module T13938 where
 
-import Data.Kind (Type)
+import T13938a
+import Data.Kind
+import Data.Type.Equality
+import GHC.TypeLits
 
-data family Sing (a :: k)
-data instance Sing (z :: [a]) where
-  SNil  :: Sing '[]
-  SCons :: Sing x -> Sing xs -> Sing (x:xs)
+type family Length (l :: [a]) :: Nat where {}
+type family Map (f :: a ~> b) (l :: [a]) :: [b] where {}
 
-data TyFun :: Type -> Type -> Type
-type a ~> b = TyFun a b -> Type
-infixr 0 ~>
+type WhyMapPreservesLength (f :: x ~> y) (l :: [x])
+  = Length l :~: Length (Map f l)
+data WhyMapPreservesLengthSym1 (f :: x ~> y) :: [x] ~> Type
+type instance Apply (WhyMapPreservesLengthSym1 f) l = WhyMapPreservesLength f l
 
-type family Apply (f :: k1 ~> k2) (x :: k1) :: k2
-type a @@ b = Apply a b
-infixl 9 @@
-
-data FunArrow = (:->) -- ^ '(->)'
-              | (:~>) -- ^ '(~>)'
-
-class FunType (arr :: FunArrow) where
-  type Fun (k1 :: Type) arr (k2 :: Type) :: Type
-
-class FunType arr => AppType (arr :: FunArrow) where
-  type App k1 arr k2 (f :: Fun k1 arr k2) (x :: k1) :: k2
-
-type FunApp arr = (FunType arr, AppType arr)
-
-instance FunType (:->) where
-  type Fun k1 (:->) k2 = k1 -> k2
-
-$(return []) -- This is only necessary for GHC 8.0 -- GHC 8.2 is smarter
-
-instance AppType (:->) where
-  type App k1 (:->) k2 (f :: k1 -> k2) x = f x
-
-instance FunType (:~>) where
-  type Fun k1 (:~>) k2 = k1 ~> k2
-
-$(return [])
-
-instance AppType (:~>) where
-  type App k1 (:~>) k2 (f :: k1 ~> k2) x = f @@ x
-
-infixr 0 -?>
-type (-?>) (k1 :: Type) (k2 :: Type) (arr :: FunArrow) = Fun k1 arr k2
-
-elimList :: forall (a :: Type) (p :: [a] -> Type) (l :: [a]).
-            Sing l
-         -> p '[]
-         -> (forall (x :: a) (xs :: [a]). Sing x -> Sing xs -> p xs -> p (x:xs))
-         -> p l
-elimList = elimListPoly @(:->)
-
-elimListTyFun :: forall (a :: Type) (p :: [a] ~> Type) (l :: [a]).
-                 Sing l
-              -> p @@ '[]
-              -> (forall (x :: a) (xs :: [a]). Sing x -> Sing xs -> p @@ xs -> p @@ (x:xs))
-              -> p @@ l
-elimListTyFun = elimListPoly @(:~>) @_ @p
-
-elimListPoly :: forall (arr :: FunArrow) (a :: Type) (p :: ([a] -?> Type) arr) (l :: [a]).
-                FunApp arr
-             => Sing l
-             -> App [a] arr Type p '[]
-             -> (forall (x :: a) (xs :: [a]). Sing x -> Sing xs -> App [a] arr Type p xs -> App [a] arr Type p (x:xs))
-             -> App [a] arr Type p l
-elimListPoly SNil                      pNil _     = pNil
-elimListPoly (SCons x (xs :: Sing xs)) pNil pCons = pCons x xs (elimListPoly @arr @a @p @xs xs pNil pCons)
+mapPreservesLength :: forall (x :: Type) (y :: Type) (f :: x ~> y) (l :: [x]).
+                      Length l :~: Length (Map f l)
+mapPreservesLength
+  = elimListTyFun @x @(WhyMapPreservesLengthSym1 f) @l undefined undefined undefined
diff --git a/testsuite/tests/dependent/should_compile/T13938a.hs b/testsuite/tests/dependent/should_compile/T13938a.hs
new file mode 100644
index 0000000000..3a09292922
--- /dev/null
+++ b/testsuite/tests/dependent/should_compile/T13938a.hs
@@ -0,0 +1,80 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE ExistentialQuantification #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE TypeOperators #-}
+module T13938a where
+
+import Data.Kind (Type)
+
+data family Sing (a :: k)
+data instance Sing (z :: [a]) where
+  SNil  :: Sing '[]
+  SCons :: Sing x -> Sing xs -> Sing (x:xs)
+
+data TyFun :: Type -> Type -> Type
+type a ~> b = TyFun a b -> Type
+infixr 0 ~>
+
+type family Apply (f :: k1 ~> k2) (x :: k1) :: k2
+type a @@ b = Apply a b
+infixl 9 @@
+
+data FunArrow = (:->) -- ^ '(->)'
+              | (:~>) -- ^ '(~>)'
+
+class FunType (arr :: FunArrow) where
+  type Fun (k1 :: Type) arr (k2 :: Type) :: Type
+
+class FunType arr => AppType (arr :: FunArrow) where
+  type App k1 arr k2 (f :: Fun k1 arr k2) (x :: k1) :: k2
+
+type FunApp arr = (FunType arr, AppType arr)
+
+instance FunType (:->) where
+  type Fun k1 (:->) k2 = k1 -> k2
+
+$(return []) -- This is only necessary for GHC 8.0 -- GHC 8.2 is smarter
+
+instance AppType (:->) where
+  type App k1 (:->) k2 (f :: k1 -> k2) x = f x
+
+instance FunType (:~>) where
+  type Fun k1 (:~>) k2 = k1 ~> k2
+
+$(return [])
+
+instance AppType (:~>) where
+  type App k1 (:~>) k2 (f :: k1 ~> k2) x = f @@ x
+
+infixr 0 -?>
+type (-?>) (k1 :: Type) (k2 :: Type) (arr :: FunArrow) = Fun k1 arr k2
+
+elimList :: forall (a :: Type) (p :: [a] -> Type) (l :: [a]).
+            Sing l
+         -> p '[]
+         -> (forall (x :: a) (xs :: [a]). Sing x -> Sing xs -> p xs -> p (x:xs))
+         -> p l
+elimList = elimListPoly @(:->)
+
+elimListTyFun :: forall (a :: Type) (p :: [a] ~> Type) (l :: [a]).
+                 Sing l
+              -> p @@ '[]
+              -> (forall (x :: a) (xs :: [a]). Sing x -> Sing xs -> p @@ xs -> p @@ (x:xs))
+              -> p @@ l
+elimListTyFun = elimListPoly @(:~>) @_ @p
+
+elimListPoly :: forall (arr :: FunArrow) (a :: Type) (p :: ([a] -?> Type) arr) (l :: [a]).
+                FunApp arr
+             => Sing l
+             -> App [a] arr Type p '[]
+             -> (forall (x :: a) (xs :: [a]). Sing x -> Sing xs -> App [a] arr Type p xs -> App [a] arr Type p (x:xs))
+             -> App [a] arr Type p l
+elimListPoly SNil                      pNil _     = pNil
+elimListPoly (SCons x (xs :: Sing xs)) pNil pCons = pCons x xs (elimListPoly @arr @a @p @xs xs pNil pCons)
diff --git a/testsuite/tests/dependent/should_compile/all.T b/testsuite/tests/dependent/should_compile/all.T
index ab7ab3c8df..da25b22799 100644
--- a/testsuite/tests/dependent/should_compile/all.T
+++ b/testsuite/tests/dependent/should_compile/all.T
@@ -28,6 +28,7 @@ test('T12176', normal, compile, [''])
 test('T14038', normal, compile, [''])
 test('T12742', normal, compile, [''])
 test('T13910', normal, compile, [''])
-test('T13938', normal, compile, [''])
+test('T13938', [extra_files(['T13938a.hs'])], run_command,
+     ['$MAKE -s --no-print-directory T13938'])
 test('T14556', normal, compile, [''])
 test('T14720', normal, compile, [''])
-- 
cgit v1.2.1


From faec8d358985e5d0bf363bd96f23fe76c9e281f7 Mon Sep 17 00:00:00 2001
From: Richard Eisenberg <rae@cs.brynmawr.edu>
Date: Mon, 4 Sep 2017 22:27:17 +0100
Subject: Track type variable scope more carefully.

The main job of this commit is to track more accurately the scope
of tyvars introduced by user-written foralls. For example, it would
be to have something like this:

  forall a. Int -> (forall k (b :: k). Proxy '[a, b]) -> Bool

In that type, a's kind must be k, but k isn't in scope. We had a
terrible way of doing this before (not worth repeating or describing
here, but see the old tcImplicitTKBndrs and friends), but now
we have a principled approach: make an Implication when kind-checking
a forall. Doing so then hooks into the existing machinery for
preventing skolem-escape, performing floating, etc. This also means
that we bump the TcLevel whenever going into a forall.

The new behavior is done in TcHsType.scopeTyVars, but see also
TcHsType.tc{Im,Ex}plicitTKBndrs, which have undergone significant
rewriting. There are several Notes near there to guide you. Of
particular interest there is that Implication constraints can now
have skolems that are out of order; this situation is reported in
TcErrors.

A major consequence of this is a slightly tweaked process for type-
checking type declarations. The new Note [Use SigTvs in kind-checking
pass] in TcTyClsDecls lays it out.

The error message for dependent/should_fail/TypeSkolEscape has become
noticeably worse. However, this is because the code in TcErrors goes to
some length to preserve pre-8.0 error messages for kind errors. It's time
to rip off that plaster and get rid of much of the kind-error-specific
error messages. I tried this, and doing so led to a lovely error message
for TypeSkolEscape. So: I'm accepting the error message quality regression
for now, but will open up a new ticket to fix it, along with a larger
error-message improvement I've been pondering. This applies also to
dependent/should_fail/{BadTelescope2,T14066,T14066e}, polykinds/T11142.

Other minor changes:
 - isUnliftedTypeKind didn't look for tuples and sums. It does now.

 - check_type used check_arg_type on both sides of an AppTy. But the left
   side of an AppTy isn't an arg, and this was causing a bad error message.
   I've changed it to use check_type on the left-hand side.

 - Some refactoring around when we print (TYPE blah) in error messages.
   The changes decrease the times when we do so, to good effect.
   Of course, this is still all controlled by
   -fprint-explicit-runtime-reps

Fixes #14066 #14749

Test cases: dependent/should_compile/{T14066a,T14749},
            dependent/should_fail/T14066{,c,d,e,f,g,h}
---
 .../dependent/should_compile/InferDependency.hs    |  6 ++
 testsuite/tests/dependent/should_compile/T11635.hs |  2 +-
 .../tests/dependent/should_compile/T14066a.hs      | 82 ++++++++++++++++++++++
 .../tests/dependent/should_compile/T14066a.stderr  |  5 ++
 testsuite/tests/dependent/should_compile/T14749.hs | 27 +++++++
 testsuite/tests/dependent/should_compile/all.T     |  2 +
 .../dependent/should_fail/BadTelescope.stderr      |  5 +-
 .../dependent/should_fail/BadTelescope2.stderr     | 13 ++--
 .../dependent/should_fail/BadTelescope3.stderr     |  2 +-
 .../dependent/should_fail/BadTelescope4.stderr     |  4 +-
 .../dependent/should_fail/InferDependency.stderr   | 10 +--
 .../tests/dependent/should_fail/T13601.stderr      |  3 +-
 .../tests/dependent/should_fail/T13780c.stderr     |  2 +-
 testsuite/tests/dependent/should_fail/T14066.hs    | 17 +++++
 .../tests/dependent/should_fail/T14066.stderr      | 11 +++
 testsuite/tests/dependent/should_fail/T14066c.hs   |  9 +++
 .../tests/dependent/should_fail/T14066c.stderr     |  6 ++
 testsuite/tests/dependent/should_fail/T14066d.hs   | 17 +++++
 .../tests/dependent/should_fail/T14066d.stderr     | 21 ++++++
 testsuite/tests/dependent/should_fail/T14066e.hs   | 13 ++++
 .../tests/dependent/should_fail/T14066e.stderr     | 11 +++
 testsuite/tests/dependent/should_fail/T14066f.hs   |  8 +++
 .../tests/dependent/should_fail/T14066f.stderr     |  6 ++
 testsuite/tests/dependent/should_fail/T14066g.hs   |  9 +++
 .../tests/dependent/should_fail/T14066g.stderr     |  7 ++
 testsuite/tests/dependent/should_fail/T14066h.hs   | 11 +++
 .../tests/dependent/should_fail/T14066h.stderr     | 16 +++++
 .../tests/dependent/should_fail/TypeSkolEscape.hs  |  1 +
 .../dependent/should_fail/TypeSkolEscape.stderr    | 10 ++-
 testsuite/tests/dependent/should_fail/all.T        | 11 ++-
 30 files changed, 316 insertions(+), 31 deletions(-)
 create mode 100644 testsuite/tests/dependent/should_compile/InferDependency.hs
 create mode 100644 testsuite/tests/dependent/should_compile/T14066a.hs
 create mode 100644 testsuite/tests/dependent/should_compile/T14066a.stderr
 create mode 100644 testsuite/tests/dependent/should_compile/T14749.hs
 create mode 100644 testsuite/tests/dependent/should_fail/T14066.hs
 create mode 100644 testsuite/tests/dependent/should_fail/T14066.stderr
 create mode 100644 testsuite/tests/dependent/should_fail/T14066c.hs
 create mode 100644 testsuite/tests/dependent/should_fail/T14066c.stderr
 create mode 100644 testsuite/tests/dependent/should_fail/T14066d.hs
 create mode 100644 testsuite/tests/dependent/should_fail/T14066d.stderr
 create mode 100644 testsuite/tests/dependent/should_fail/T14066e.hs
 create mode 100644 testsuite/tests/dependent/should_fail/T14066e.stderr
 create mode 100644 testsuite/tests/dependent/should_fail/T14066f.hs
 create mode 100644 testsuite/tests/dependent/should_fail/T14066f.stderr
 create mode 100644 testsuite/tests/dependent/should_fail/T14066g.hs
 create mode 100644 testsuite/tests/dependent/should_fail/T14066g.stderr
 create mode 100644 testsuite/tests/dependent/should_fail/T14066h.hs
 create mode 100644 testsuite/tests/dependent/should_fail/T14066h.stderr

(limited to 'testsuite/tests/dependent')

diff --git a/testsuite/tests/dependent/should_compile/InferDependency.hs b/testsuite/tests/dependent/should_compile/InferDependency.hs
new file mode 100644
index 0000000000..47957d47d6
--- /dev/null
+++ b/testsuite/tests/dependent/should_compile/InferDependency.hs
@@ -0,0 +1,6 @@
+{-# LANGUAGE TypeInType #-}
+
+module InferDependency where
+
+data Proxy k (a :: k)
+data Proxy2 k a = P (Proxy k a)
diff --git a/testsuite/tests/dependent/should_compile/T11635.hs b/testsuite/tests/dependent/should_compile/T11635.hs
index 1cbdbafb90..2292def966 100644
--- a/testsuite/tests/dependent/should_compile/T11635.hs
+++ b/testsuite/tests/dependent/should_compile/T11635.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE TypeInType, KindSignatures, ExplicitForAll #-}
+{-# LANGUAGE TypeInType, KindSignatures, ExplicitForAll, RankNTypes #-}
 
 module T11635 where
 
diff --git a/testsuite/tests/dependent/should_compile/T14066a.hs b/testsuite/tests/dependent/should_compile/T14066a.hs
new file mode 100644
index 0000000000..e1a6255520
--- /dev/null
+++ b/testsuite/tests/dependent/should_compile/T14066a.hs
@@ -0,0 +1,82 @@
+{-# LANGUAGE TypeFamilies, TypeInType, ExplicitForAll, GADTs,
+             UndecidableInstances, RankNTypes, ScopedTypeVariables #-}
+
+module T14066a where
+
+import Data.Proxy
+import Data.Kind
+import Data.Type.Bool
+
+
+type family Bar x y where
+  Bar (x :: a) (y :: b) = Int
+  Bar (x :: c) (y :: d) = Bool   -- a,b,c,d should be SigTvs and unify appropriately
+
+
+  -- the two k's, even though they have different scopes, should unify in the
+  -- kind-check and then work in the type-check because Prox3 has been generalized
+
+data Prox3 a where
+  MkProx3a :: Prox3 (a :: k1)
+  MkProx3b :: Prox3 (a :: k2)
+
+  -- This probably should be rejected, as it's polymorphic recursion without a CUSK.
+  -- But GHC accepts it because the polymorphic occurrence is at a type variable.
+data T0 a = forall k (b :: k). MkT0 (T0 b) Int
+
+  -- k and j should unify
+type family G x a where
+  G Int (b :: k) = Int
+  G Bool (c :: j) = Bool
+
+-- this last example just checks that GADT pattern-matching on kinds still works.
+-- nothing new here.
+data T (a :: k) where
+  MkT :: T (a :: Type -> Type)
+
+data S (a :: Type -> Type) where
+  MkS :: S a
+
+f :: forall k (a :: k). Proxy a -> T a -> ()
+f _ MkT = let y :: S a
+              y = MkS
+          in ()
+
+-- This is questionable. Should we use the RHS to determine dependency? It works
+-- now, but if it stops working in the future, that's not a deal-breaker.
+type P k a = Proxy (a :: k)
+
+
+-- This is a challenge. It should be accepted, but only because c's kind is learned
+-- to be Proxy True, allowing b to be assigned kind `a`. If we don't know c's kind,
+-- then GHC would need to be convinced that If (c's kind) b d always has kind `a`.
+-- Naively, we don't know about c's kind early enough.
+
+data SameKind :: forall k. k -> k -> Type
+type family IfK (e :: Proxy (j :: Bool)) (f :: m) (g :: n) :: If j m n where
+   IfK (_ :: Proxy True)  f _ = f
+   IfK (_ :: Proxy False) _ g = g
+x :: forall c. (forall a b (d :: a). SameKind (IfK c b d) d) -> (Proxy (c :: Proxy True))
+x _ = Proxy
+
+
+f2 :: forall b. b -> Proxy Maybe
+f2 x = fstOf3 y :: Proxy Maybe
+  where
+    y :: (Proxy a, Proxy c, b)
+    y = (Proxy, Proxy, x)
+
+fstOf3 (x, _, _) = x
+
+f3 :: forall b. b -> Proxy Maybe
+f3 x = fst y :: Proxy Maybe
+  where
+    y :: (Proxy a, b)
+    y = (Proxy, x)
+
+-- cf. dependent/should_fail/T14066h. Here, y's type does *not* capture any variables,
+-- so it is generalized, even with MonoLocalBinds.
+f4 x = (fst y :: Proxy Int, fst y :: Proxy Maybe)
+  where
+    y :: (Proxy a, Int)
+    y = (Proxy, x)
diff --git a/testsuite/tests/dependent/should_compile/T14066a.stderr b/testsuite/tests/dependent/should_compile/T14066a.stderr
new file mode 100644
index 0000000000..906695f3f7
--- /dev/null
+++ b/testsuite/tests/dependent/should_compile/T14066a.stderr
@@ -0,0 +1,5 @@
+
+T14066a.hs:13:3: warning:
+    Type family instance equation is overlapped:
+      forall c d (x :: c) (y :: d).
+        Bar x y = Bool -- Defined at T14066a.hs:13:3
diff --git a/testsuite/tests/dependent/should_compile/T14749.hs b/testsuite/tests/dependent/should_compile/T14749.hs
new file mode 100644
index 0000000000..79bcce66ff
--- /dev/null
+++ b/testsuite/tests/dependent/should_compile/T14749.hs
@@ -0,0 +1,27 @@
+{-# LANGUAGE GADTs, TypeOperators, DataKinds, TypeFamilies, TypeInType #-}
+
+module T14749 where
+
+import Data.Kind
+
+data KIND = STAR | KIND :> KIND
+
+data Ty :: KIND -> Type where
+  TMaybe :: Ty (STAR :> STAR)
+  TApp   :: Ty (a :> b) -> (Ty a -> Ty b)
+
+type family IK (k :: KIND) = (res :: Type) where
+  IK STAR   = Type
+  IK (a:>b) = IK a -> IK b
+
+type family I (t :: Ty k) = (res :: IK k)  where
+  I TMaybe     = Maybe
+  I (TApp f a) = (I f) (I a)
+
+data TyRep (k :: KIND) (t :: Ty k) where
+  TyMaybe :: TyRep (STAR:>STAR) TMaybe
+  TyApp   :: TyRep (a:>b) f -> TyRep a x -> TyRep b (TApp f x)
+
+zero :: TyRep STAR a -> I a
+zero x = case x of
+            TyApp TyMaybe _ -> Nothing
diff --git a/testsuite/tests/dependent/should_compile/all.T b/testsuite/tests/dependent/should_compile/all.T
index da25b22799..070e1203f8 100644
--- a/testsuite/tests/dependent/should_compile/all.T
+++ b/testsuite/tests/dependent/should_compile/all.T
@@ -32,3 +32,5 @@ test('T13938', [extra_files(['T13938a.hs'])], run_command,
      ['$MAKE -s --no-print-directory T13938'])
 test('T14556', normal, compile, [''])
 test('T14720', normal, compile, [''])
+test('T14066a', normal, compile, [''])
+test('T14749', normal, compile, [''])
diff --git a/testsuite/tests/dependent/should_fail/BadTelescope.stderr b/testsuite/tests/dependent/should_fail/BadTelescope.stderr
index 2fbc35a9ba..5fa8efd502 100644
--- a/testsuite/tests/dependent/should_fail/BadTelescope.stderr
+++ b/testsuite/tests/dependent/should_fail/BadTelescope.stderr
@@ -1,9 +1,6 @@
 
 BadTelescope.hs:9:1: error:
-    • These kind and type variables: (a :: k)
-                                     k
-                                     (b :: k)
-                                     (c :: SameKind a b)
+    • These kind and type variables: a k (b :: k) (c :: SameKind a b)
       are out of dependency order. Perhaps try this ordering:
         k (a :: k) (b :: k) (c :: SameKind a b)
     • In the data type declaration for ‘X’
diff --git a/testsuite/tests/dependent/should_fail/BadTelescope2.stderr b/testsuite/tests/dependent/should_fail/BadTelescope2.stderr
index 2a9dc76310..55a484910c 100644
--- a/testsuite/tests/dependent/should_fail/BadTelescope2.stderr
+++ b/testsuite/tests/dependent/should_fail/BadTelescope2.stderr
@@ -3,14 +3,11 @@ BadTelescope2.hs:10:8: error:
     • These kind and type variables: a k (b :: k)
       are out of dependency order. Perhaps try this ordering:
         k (a :: k) (b :: k)
-    • In the type signature:
-        foo :: forall a k (b :: k). SameKind a b
+    • In the type signature: foo :: forall a k (b :: k). SameKind a b
 
-BadTelescope2.hs:13:8: error:
-    • The kind of variable ‘b’, namely ‘Proxy a’,
-      depends on variable ‘a’ from an inner scope
-      Perhaps bind ‘b’ sometime after binding ‘a’
-      NB: Implicitly-bound variables always come before other ones.
-    • In the type signature:
+BadTelescope2.hs:13:70: error:
+    • Expected kind ‘k0’, but ‘d’ has kind ‘Proxy a’
+    • In the second argument of ‘SameKind’, namely ‘d’
+      In the type signature:
         bar :: forall a (c :: Proxy b) (d :: Proxy a).
                Proxy c -> SameKind b d
diff --git a/testsuite/tests/dependent/should_fail/BadTelescope3.stderr b/testsuite/tests/dependent/should_fail/BadTelescope3.stderr
index 4ea7458bb2..1137f28c4d 100644
--- a/testsuite/tests/dependent/should_fail/BadTelescope3.stderr
+++ b/testsuite/tests/dependent/should_fail/BadTelescope3.stderr
@@ -1,6 +1,6 @@
 
 BadTelescope3.hs:9:1: error:
-    • These kind and type variables: (a :: k) k (b :: k)
+    • These kind and type variables: a k (b :: k)
       are out of dependency order. Perhaps try this ordering:
         k (a :: k) (b :: k)
     • In the type synonym declaration for ‘S’
diff --git a/testsuite/tests/dependent/should_fail/BadTelescope4.stderr b/testsuite/tests/dependent/should_fail/BadTelescope4.stderr
index 2394f896ad..f7c281e983 100644
--- a/testsuite/tests/dependent/should_fail/BadTelescope4.stderr
+++ b/testsuite/tests/dependent/should_fail/BadTelescope4.stderr
@@ -1,6 +1,6 @@
 
 BadTelescope4.hs:9:1: error:
-    • These kind and type variables: (a :: k)
+    • These kind and type variables: a
                                      (c :: Proxy b)
                                      (d :: Proxy a)
                                      (x :: SameKind b d)
@@ -11,5 +11,5 @@ BadTelescope4.hs:9:1: error:
         (c :: Proxy b)
         (d :: Proxy a)
         (x :: SameKind b d)
-      NB: Implicitly declared kind variables are put first.
+      NB: Implicitly declared variables come before others.
     • In the data type declaration for ‘Bad’
diff --git a/testsuite/tests/dependent/should_fail/InferDependency.stderr b/testsuite/tests/dependent/should_fail/InferDependency.stderr
index 7fa900a889..cc852ee58c 100644
--- a/testsuite/tests/dependent/should_fail/InferDependency.stderr
+++ b/testsuite/tests/dependent/should_fail/InferDependency.stderr
@@ -1,8 +1,10 @@
 
-InferDependency.hs:6:1: error:
-    • Invalid declaration for ‘Proxy2’; you must explicitly
-      declare which variables are dependent on which others.
-      Inferred variable kinds:
+InferDependency.hs:6:13: error:
+    • Type constructor argument ‘k’ is used dependently.
+      Any dependent arguments must be obviously so, not inferred
+      by the type-checker.
+      Inferred argument kinds:
         k :: *
         a :: k
+      Suggestion: use ‘k’ in a kind to make the dependency clearer.
     • In the data type declaration for ‘Proxy2’
diff --git a/testsuite/tests/dependent/should_fail/T13601.stderr b/testsuite/tests/dependent/should_fail/T13601.stderr
index c1c9803e5a..bc2877c3e6 100644
--- a/testsuite/tests/dependent/should_fail/T13601.stderr
+++ b/testsuite/tests/dependent/should_fail/T13601.stderr
@@ -1,6 +1,5 @@
 
 T13601.hs:18:16: error:
-    • Expected kind ‘TYPE (Rep 'LiftedRep)’,
-        but ‘Logic a’ has kind ‘TYPE (Rep rep)’
+    • Expected a type, but ‘Logic a’ has kind ‘TYPE (Rep rep)’
     • In the first argument of ‘Boolean’, namely ‘(Logic a)’
       In the class declaration for ‘Eq’
diff --git a/testsuite/tests/dependent/should_fail/T13780c.stderr b/testsuite/tests/dependent/should_fail/T13780c.stderr
index f91d7a3236..065c700dfc 100644
--- a/testsuite/tests/dependent/should_fail/T13780c.stderr
+++ b/testsuite/tests/dependent/should_fail/T13780c.stderr
@@ -2,7 +2,7 @@
 [2 of 2] Compiling T13780c          ( T13780c.hs, T13780c.o )
 
 T13780c.hs:11:16: error:
-    • Expected kind ‘Sing _’, but ‘SFalse’ has kind ‘Sing 'False’
+    • Expected kind ‘Sing _1’, but ‘SFalse’ has kind ‘Sing 'False’
     • In the third argument of ‘ElimBool’, namely ‘SFalse’
       In the type family declaration for ‘ElimBool’
 
diff --git a/testsuite/tests/dependent/should_fail/T14066.hs b/testsuite/tests/dependent/should_fail/T14066.hs
new file mode 100644
index 0000000000..58396df591
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T14066.hs
@@ -0,0 +1,17 @@
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE KindSignatures #-}
+
+module T14066 where
+
+import Data.Kind ( Type )
+import Data.Type.Equality
+import Data.Proxy
+import GHC.Exts
+
+data SameKind :: k -> k -> Type
+
+f (x :: Proxy a) = let g :: forall k (b :: k). SameKind a b
+                       g = undefined
+                   in ()
diff --git a/testsuite/tests/dependent/should_fail/T14066.stderr b/testsuite/tests/dependent/should_fail/T14066.stderr
new file mode 100644
index 0000000000..cd0142f5c1
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T14066.stderr
@@ -0,0 +1,11 @@
+
+T14066.hs:15:59: error:
+    • Expected kind ‘k0’, but ‘b’ has kind ‘k’
+    • In the second argument of ‘SameKind’, namely ‘b’
+      In the type signature: g :: forall k (b :: k). SameKind a b
+      In the expression:
+        let
+          g :: forall k (b :: k). SameKind a b
+          g = undefined
+        in ()
+    • Relevant bindings include x :: Proxy a (bound at T14066.hs:15:4)
diff --git a/testsuite/tests/dependent/should_fail/T14066c.hs b/testsuite/tests/dependent/should_fail/T14066c.hs
new file mode 100644
index 0000000000..b4597d2cec
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T14066c.hs
@@ -0,0 +1,9 @@
+{-# LANGUAGE TypeFamilies, TypeInType, UndecidableInstances #-}
+
+module T14066c where
+
+type family H a b where
+  H a b = H b a
+
+type X = H True Nothing  -- this should fail to kind-check.
+                         -- if it's accepted, then we've inferred polymorphic recursion for H
diff --git a/testsuite/tests/dependent/should_fail/T14066c.stderr b/testsuite/tests/dependent/should_fail/T14066c.stderr
new file mode 100644
index 0000000000..dc5ba30a4f
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T14066c.stderr
@@ -0,0 +1,6 @@
+
+T14066c.hs:8:17: error:
+    • Expected kind ‘Bool’, but ‘Nothing’ has kind ‘Maybe a0’
+    • In the second argument of ‘H’, namely ‘Nothing’
+      In the type ‘H True Nothing’
+      In the type declaration for ‘X’
diff --git a/testsuite/tests/dependent/should_fail/T14066d.hs b/testsuite/tests/dependent/should_fail/T14066d.hs
new file mode 100644
index 0000000000..ea47644688
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T14066d.hs
@@ -0,0 +1,17 @@
+{-# LANGUAGE RankNTypes, ScopedTypeVariables, TypeInType #-}
+
+module T14066d where
+
+import Data.Proxy
+
+g :: (forall c b (a :: c). (Proxy a, Proxy c, b)) -> ()
+g _ = ()
+
+f :: forall b. b -> (Proxy Maybe, ())
+f x = (fstOf3 y :: Proxy Maybe, g y)
+  where
+    y :: (Proxy a, Proxy c, b)  -- this should NOT generalize over b
+                                -- meaning the call to g is ill-typed
+    y = (Proxy, Proxy, x)
+
+fstOf3 (x, _, _) = x
diff --git a/testsuite/tests/dependent/should_fail/T14066d.stderr b/testsuite/tests/dependent/should_fail/T14066d.stderr
new file mode 100644
index 0000000000..3a8b90edce
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T14066d.stderr
@@ -0,0 +1,21 @@
+
+T14066d.hs:11:35: error:
+    • Couldn't match type ‘b’ with ‘b1’
+      ‘b’ is a rigid type variable bound by
+        the type signature for:
+          f :: forall b. b -> (Proxy Maybe, ())
+        at T14066d.hs:10:1-37
+      ‘b1’ is a rigid type variable bound by
+        a type expected by the context:
+          forall c b1 (a :: c). (Proxy a, Proxy c, b1)
+        at T14066d.hs:11:33-35
+      Expected type: (Proxy a, Proxy c, b1)
+        Actual type: (Proxy a, Proxy c, b)
+    • In the first argument of ‘g’, namely ‘y’
+      In the expression: g y
+      In the expression: (fstOf3 y :: Proxy Maybe, g y)
+    • Relevant bindings include
+        y :: forall k1 k2 (a :: k2) (c :: k1). (Proxy a, Proxy c, b)
+          (bound at T14066d.hs:15:5)
+        x :: b (bound at T14066d.hs:11:3)
+        f :: b -> (Proxy Maybe, ()) (bound at T14066d.hs:11:1)
diff --git a/testsuite/tests/dependent/should_fail/T14066e.hs b/testsuite/tests/dependent/should_fail/T14066e.hs
new file mode 100644
index 0000000000..9b799e542c
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T14066e.hs
@@ -0,0 +1,13 @@
+{-# LANGUAGE MonoLocalBinds, TypeInType, ScopedTypeVariables #-}
+
+module T14066e where
+
+import Data.Proxy
+
+-- this should fail because the dependency between b and c can't be
+-- determined in the type signature
+h :: forall a. a -> ()
+h x = ()
+  where
+    j :: forall c b. Proxy a -> Proxy b -> Proxy c -> Proxy b
+    j _ (p1 :: Proxy b') (p2 :: Proxy c') = (p1 :: Proxy (b' :: c'))
diff --git a/testsuite/tests/dependent/should_fail/T14066e.stderr b/testsuite/tests/dependent/should_fail/T14066e.stderr
new file mode 100644
index 0000000000..504ca5a80e
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T14066e.stderr
@@ -0,0 +1,11 @@
+
+T14066e.hs:13:59: error:
+    • Expected kind ‘c’, but ‘b'’ has kind ‘k0’
+    • In the first argument of ‘Proxy’, namely ‘(b' :: c')’
+      In an expression type signature: Proxy (b' :: c')
+      In the expression: (p1 :: Proxy (b' :: c'))
+    • Relevant bindings include
+        p2 :: Proxy c (bound at T14066e.hs:13:27)
+        p1 :: Proxy b (bound at T14066e.hs:13:10)
+        j :: Proxy a -> Proxy b -> Proxy c -> Proxy b
+          (bound at T14066e.hs:13:5)
diff --git a/testsuite/tests/dependent/should_fail/T14066f.hs b/testsuite/tests/dependent/should_fail/T14066f.hs
new file mode 100644
index 0000000000..ccb7ceac0e
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T14066f.hs
@@ -0,0 +1,8 @@
+{-# LANGUAGE TypeInType #-}
+
+module T14066f where
+
+import Data.Proxy
+
+-- a can't come before k.
+type P a k = Proxy (a :: k)
diff --git a/testsuite/tests/dependent/should_fail/T14066f.stderr b/testsuite/tests/dependent/should_fail/T14066f.stderr
new file mode 100644
index 0000000000..44c4ed293c
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T14066f.stderr
@@ -0,0 +1,6 @@
+
+T14066f.hs:8:1: error:
+    • These kind and type variables: a k
+      are out of dependency order. Perhaps try this ordering:
+        k (a :: k)
+    • In the type synonym declaration for ‘P’
diff --git a/testsuite/tests/dependent/should_fail/T14066g.hs b/testsuite/tests/dependent/should_fail/T14066g.hs
new file mode 100644
index 0000000000..df0e03b173
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T14066g.hs
@@ -0,0 +1,9 @@
+{-# LANGUAGE TypeInType #-}
+
+module T14066g where
+
+import Data.Kind
+
+data SameKind :: k -> k -> Type
+
+data Q a (b :: a) (d :: SameKind c b)
diff --git a/testsuite/tests/dependent/should_fail/T14066g.stderr b/testsuite/tests/dependent/should_fail/T14066g.stderr
new file mode 100644
index 0000000000..22ca786343
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T14066g.stderr
@@ -0,0 +1,7 @@
+
+T14066g.hs:9:1: error:
+    • These kind and type variables: a (b :: a) (d :: SameKind c b)
+      are out of dependency order. Perhaps try this ordering:
+        a (c :: a) (b :: a) (d :: SameKind c b)
+      NB: Implicitly declared variables come before others.
+    • In the data type declaration for ‘Q’
diff --git a/testsuite/tests/dependent/should_fail/T14066h.hs b/testsuite/tests/dependent/should_fail/T14066h.hs
new file mode 100644
index 0000000000..7e7ecd31c9
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T14066h.hs
@@ -0,0 +1,11 @@
+{-# LANGUAGE ScopedTypeVariables, TypeInType, MonoLocalBinds #-}
+
+module T14066h where
+
+import Data.Proxy
+
+f :: forall b. b -> (Proxy Int, Proxy Maybe)
+f x = (fst y :: Proxy Int, fst y :: Proxy Maybe)
+  where
+    y :: (Proxy a, b)  -- MonoLocalBinds means this won't generalize over the kind of a
+    y = (Proxy, x)
diff --git a/testsuite/tests/dependent/should_fail/T14066h.stderr b/testsuite/tests/dependent/should_fail/T14066h.stderr
new file mode 100644
index 0000000000..bfd33693b6
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T14066h.stderr
@@ -0,0 +1,16 @@
+
+T14066h.hs:8:28: error:
+    • Couldn't match kind ‘* -> *’ with ‘*’
+      When matching types
+        a0 :: *
+        Maybe :: * -> *
+      Expected type: Proxy Maybe
+        Actual type: Proxy a0
+    • In the expression: fst y :: Proxy Maybe
+      In the expression: (fst y :: Proxy Int, fst y :: Proxy Maybe)
+      In an equation for ‘f’:
+          f x
+            = (fst y :: Proxy Int, fst y :: Proxy Maybe)
+            where
+                y :: (Proxy a, b)
+                y = (Proxy, x)
diff --git a/testsuite/tests/dependent/should_fail/TypeSkolEscape.hs b/testsuite/tests/dependent/should_fail/TypeSkolEscape.hs
index bbec037487..02b7737499 100644
--- a/testsuite/tests/dependent/should_fail/TypeSkolEscape.hs
+++ b/testsuite/tests/dependent/should_fail/TypeSkolEscape.hs
@@ -1,4 +1,5 @@
 {-# LANGUAGE RankNTypes, PolyKinds, TypeInType #-}
+-- NB: -fprint-explicit-runtime-reps enabled in all.T
 
 module TypeSkolEscape where
 
diff --git a/testsuite/tests/dependent/should_fail/TypeSkolEscape.stderr b/testsuite/tests/dependent/should_fail/TypeSkolEscape.stderr
index 88539858cf..e2ef266914 100644
--- a/testsuite/tests/dependent/should_fail/TypeSkolEscape.stderr
+++ b/testsuite/tests/dependent/should_fail/TypeSkolEscape.stderr
@@ -1,7 +1,5 @@
 
-TypeSkolEscape.hs:8:1: error:
-    • Quantified type's kind mentions quantified type variable
-      (skolem escape)
-           type: forall (a1 :: TYPE v1). a1
-        of kind: TYPE v
-    • In the type synonym declaration for ‘Bad’
+TypeSkolEscape.hs:9:52: error:
+    • Expected kind ‘k0’, but ‘a’ has kind ‘TYPE v’
+    • In the type ‘forall (v :: RuntimeRep) (a :: TYPE v). a’
+      In the type declaration for ‘Bad’
diff --git a/testsuite/tests/dependent/should_fail/all.T b/testsuite/tests/dependent/should_fail/all.T
index e28b2df5cd..7273445548 100644
--- a/testsuite/tests/dependent/should_fail/all.T
+++ b/testsuite/tests/dependent/should_fail/all.T
@@ -1,6 +1,6 @@
 test('DepFail1', normal, compile_fail, [''])
 test('RAE_T32a', normal, compile_fail, [''])
-test('TypeSkolEscape', normal, compile_fail, [''])
+test('TypeSkolEscape', normal, compile_fail, ['-fprint-explicit-runtime-reps'])
 test('BadTelescope', normal, compile_fail, [''])
 test('BadTelescope2', normal, compile_fail, [''])
 test('BadTelescope3', normal, compile_fail, [''])
@@ -10,7 +10,6 @@ test('BadTelescope4', normal, compile_fail, [''])
 test('RenamingStar', normal, compile_fail, [''])
 test('T11407', normal, compile_fail, [''])
 test('T11334b', normal, compile_fail, [''])
-test('InferDependency', normal, compile_fail, [''])
 test('KindLevelsB', normal, compile_fail, [''])
 test('T11473', normal, compile_fail, [''])
 test('T11471', normal, compile_fail, [''])
@@ -21,3 +20,11 @@ test('T13601', normal, compile_fail, [''])
 test('T13780a', normal, compile_fail, [''])
 test('T13780c', [extra_files(['T13780b.hs'])],
                 multimod_compile_fail, ['T13780c', ''])
+test('T14066', normal, compile_fail, [''])
+test('T14066c', normal, compile_fail, [''])
+test('T14066d', normal, compile_fail, [''])
+test('T14066e', normal, compile_fail, [''])
+test('T14066f', normal, compile_fail, [''])
+test('T14066g', normal, compile_fail, [''])
+test('T14066h', normal, compile_fail, [''])
+test('InferDependency', normal, compile_fail, [''])
-- 
cgit v1.2.1


From d8d4266bf73790f65b223ec16f645763eaed8be3 Mon Sep 17 00:00:00 2001
From: Richard Eisenberg <rae@cs.brynmawr.edu>
Date: Mon, 2 Apr 2018 15:32:04 -0400
Subject: Fix #14991.

It turns out that solveEqualities really does need to use simpl_top.
I thought that solveWanteds would be enough, and no existing test
case showed up the different. #14991 shows that we need simpl_top.
Easy enough to fix.

test case: dependent/should_compile/T14991
---
 testsuite/tests/dependent/should_compile/T14991.hs | 34 ++++++++++++++++++++++
 testsuite/tests/dependent/should_compile/all.T     |  1 +
 2 files changed, 35 insertions(+)
 create mode 100644 testsuite/tests/dependent/should_compile/T14991.hs

(limited to 'testsuite/tests/dependent')

diff --git a/testsuite/tests/dependent/should_compile/T14991.hs b/testsuite/tests/dependent/should_compile/T14991.hs
new file mode 100644
index 0000000000..f435c37690
--- /dev/null
+++ b/testsuite/tests/dependent/should_compile/T14991.hs
@@ -0,0 +1,34 @@
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+module T14991 where
+
+import Data.Kind
+
+type family Promote (k :: Type) :: Type
+type family PromoteX (a :: k) :: Promote k
+
+type family Demote (k :: Type) :: Type
+type family DemoteX (a :: k) :: Demote k
+
+-----
+-- Type
+-----
+
+type instance Demote Type = Type
+type instance Promote Type = Type
+
+type instance DemoteX (a :: Type) = Demote a
+type instance PromoteX (a :: Type) = Promote a
+
+-----
+-- Arrows
+-----
+
+data TyFun :: Type -> Type -> Type
+type a ~> b = TyFun a b -> Type
+infixr 0 ~>
+
+type instance Demote  (a ~> b) = DemoteX  a -> DemoteX  b
+type instance Promote (a -> b) = PromoteX a ~> PromoteX b
diff --git a/testsuite/tests/dependent/should_compile/all.T b/testsuite/tests/dependent/should_compile/all.T
index 070e1203f8..701e187b36 100644
--- a/testsuite/tests/dependent/should_compile/all.T
+++ b/testsuite/tests/dependent/should_compile/all.T
@@ -34,3 +34,4 @@ test('T14556', normal, compile, [''])
 test('T14720', normal, compile, [''])
 test('T14066a', normal, compile, [''])
 test('T14749', normal, compile, [''])
+test('T14991', normal, compile, [''])
-- 
cgit v1.2.1


From 718a018128a0ba2ae20001c10bc8ca4d929a1d33 Mon Sep 17 00:00:00 2001
From: Ryan Scott <ryan.gl.scott@gmail.com>
Date: Sat, 7 Apr 2018 07:30:42 -0400
Subject: Fix #14238 by always pretty-printing visible tyvars
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Summary:
Before, GHC would never print visible tyvars in the absence
of `-fprint-explicit-foralls`, which led to `:kind` displaying
incorrect kinds in GHCi. The fix is simple—simply check beforehand
if any of the type variable binders are required when deciding when
to pretty-print them.

Test Plan: make test TEST=T14238

Reviewers: simonpj, goldfire, bgamari

Subscribers: thomie, carter

GHC Trac Issues: #14238

Differential Revision: https://phabricator.haskell.org/D4564
---
 testsuite/tests/dependent/ghci/T14238.script | 4 ++++
 testsuite/tests/dependent/ghci/T14238.stdout | 1 +
 testsuite/tests/dependent/ghci/all.T         | 1 +
 3 files changed, 6 insertions(+)
 create mode 100644 testsuite/tests/dependent/ghci/T14238.script
 create mode 100644 testsuite/tests/dependent/ghci/T14238.stdout

(limited to 'testsuite/tests/dependent')

diff --git a/testsuite/tests/dependent/ghci/T14238.script b/testsuite/tests/dependent/ghci/T14238.script
new file mode 100644
index 0000000000..7c27123e00
--- /dev/null
+++ b/testsuite/tests/dependent/ghci/T14238.script
@@ -0,0 +1,4 @@
+:set -XTypeInType
+:m + Data.Kind
+data Foo (k :: Type) :: k -> Type
+:kind Foo
diff --git a/testsuite/tests/dependent/ghci/T14238.stdout b/testsuite/tests/dependent/ghci/T14238.stdout
new file mode 100644
index 0000000000..fddbc0de54
--- /dev/null
+++ b/testsuite/tests/dependent/ghci/T14238.stdout
@@ -0,0 +1 @@
+Foo :: forall k -> k -> *
diff --git a/testsuite/tests/dependent/ghci/all.T b/testsuite/tests/dependent/ghci/all.T
index 956272fa55..bd819c28bc 100644
--- a/testsuite/tests/dependent/ghci/all.T
+++ b/testsuite/tests/dependent/ghci/all.T
@@ -2,3 +2,4 @@ test('T11549',
      [ expect_broken( 11787 ),
        expect_broken( 11786 ) ],
      ghci_script, ['T11549.script'])
+test('T14238', normal, ghci_script, ['T14238.script'])
-- 
cgit v1.2.1


From d9d801516dccab88b8083d34b465ee9ca8deb92f Mon Sep 17 00:00:00 2001
From: Alp Mestanogullari <alp@well-typed.com>
Date: Thu, 19 Apr 2018 12:40:21 -0400
Subject: testsuite: Fix `./validate --slow`

This fixes all unexpected passes and unexpected failures from a
`./validate --slow` run I did last week. I commented on many
tickets and created a few more as I was going through the failing
tests. A summary of the entire process is available at:

  https://gist.github.com/alpmestan/c371840968f086c8dc5b56af8325f0a9

This is part of an attempt to have `./validate --slow` pass,
tracked in #14890. Another patch will be necessary for the unexpected
stats failures.

Test Plan: ./validate --slow (not green yet)

Reviewers: bgamari, simonmar

Subscribers: thomie, carter

Differential Revision: https://phabricator.haskell.org/D4546
---
 testsuite/tests/dependent/should_compile/all.T | 5 +----
 1 file changed, 1 insertion(+), 4 deletions(-)

(limited to 'testsuite/tests/dependent')

diff --git a/testsuite/tests/dependent/should_compile/all.T b/testsuite/tests/dependent/should_compile/all.T
index 701e187b36..5874d2e936 100644
--- a/testsuite/tests/dependent/should_compile/all.T
+++ b/testsuite/tests/dependent/should_compile/all.T
@@ -10,10 +10,7 @@ test('RaeBlogPost', normal, compile, [''])
 test('mkGADTVars', normal, compile, [''])
 test('TypeLevelVec',normal,compile, [''])
 test('T9632', normal, compile, [''])
-# Simon says in #11330: The "simplifier ticks exhausted" error is expected;
-# see Section 7 of the paper:
-# http://research.microsoft.com/en-us/um/people/simonpj/papers/haskell-dynamic/
-test('dynamic-paper', expect_fail_for(['optasm', 'optllvm']), compile, [''])
+test('dynamic-paper', normal, compile, ['']) # see #11330
 test('T11311', normal, compile, [''])
 test('T11405', normal, compile, [''])
 test('T11241', normal, compile, [''])
-- 
cgit v1.2.1


From ca3d3039386b145ae2835ca563b4c5a3497c25c9 Mon Sep 17 00:00:00 2001
From: Alp Mestanogullari <alp@well-typed.com>
Date: Sun, 13 May 2018 18:38:18 -0400
Subject: Fix another batch of `./validate --slow` failures

A rather detailed summary can be found at:

    https://gist.github.com/alpmestan/be82b47bb88b7dc9ff84105af9b1bb82

This doesn't fix all expectation mismatches yet, but we're down to about
20 mismatches with my previous patch and this one, as opposed to ~150
when I got started.

Test Plan: ./validate --slow

Reviewers: bgamari, erikd, simonmar

Reviewed By: simonmar

Subscribers: thomie, carter

GHC Trac Issues: #14890

Differential Revision: https://phabricator.haskell.org/D4636
---
 testsuite/tests/dependent/should_compile/all.T | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

(limited to 'testsuite/tests/dependent')

diff --git a/testsuite/tests/dependent/should_compile/all.T b/testsuite/tests/dependent/should_compile/all.T
index 5874d2e936..65853169bd 100644
--- a/testsuite/tests/dependent/should_compile/all.T
+++ b/testsuite/tests/dependent/should_compile/all.T
@@ -10,7 +10,14 @@ test('RaeBlogPost', normal, compile, [''])
 test('mkGADTVars', normal, compile, [''])
 test('TypeLevelVec',normal,compile, [''])
 test('T9632', normal, compile, [''])
-test('dynamic-paper', normal, compile, ['']) # see #11330
+# The dynamic-paper test fails in the profasm way if we don't increase
+# the simplifier tick limit. If we do, we run out of stack
+# space. If we increase the stack size enough with -K,
+# we run out of simplifier ticks again. This is
+# discussed in #11330.
+test('dynamic-paper',
+     expect_broken_for(11330, ['profasm']),
+     compile, [''])
 test('T11311', normal, compile, [''])
 test('T11405', normal, compile, [''])
 test('T11241', normal, compile, [''])
-- 
cgit v1.2.1


From 2bbdd00c6d70bdc31ff78e2a42b26159c8717856 Mon Sep 17 00:00:00 2001
From: Simon Peyton Jones <simonpj@microsoft.com>
Date: Fri, 18 May 2018 08:43:11 +0100
Subject: Orient TyVar/TyVar equalities with deepest on the left

Trac #15009 showed that, for Given TyVar/TyVar equalities, we really
want to orient them with the deepest-bound skolem on the left. As it
happens, we also want to do the same for Wanteds, but for a different
reason (more likely to be touchable).  Either way, deepest wins:
see TcUnify Note [Deeper level on the left].

This observation led me to some significant changes:

* A SkolemTv already had a TcLevel, but the level wasn't really being
  used.   Now it is!

* I updated added invariant (SkolInf) to TcType
  Note [TcLevel and untouchable type variables], documenting that
  the level number of all the ic_skols should be the same as the
  ic_tclvl of the implication

* FlatSkolTvs and FlatMetaTvs previously had a dummy level-number of
  zero, which messed the scheme up.   Now they get a level number the
  same way as all other TcTyVars, instead of being a special case.

* To make sure that FlatSkolTvs and FlatMetaTvs are untouchable (which
  was previously done via their magic zero level) isTouchableMetaTyVar
  just tests for those two cases.

* TcUnify.swapOverTyVars is the crucial orientation function; see the
  new Note [TyVar/TyVar orientation].  I completely rewrote this function,
  and it's now much much easier to understand.

I ended up doing some related refactoring, of course

* I noticed that tcImplicitTKBndrsX and tcExplicitTKBndrsX were doing
  a lot of useless work in the case where there are no skolems; I
  added a fast-patch

* Elminate the un-used tcExplicitTKBndrsSig; and thereby get rid of
  the higher-order parameter to tcExpliciTKBndrsX.

* Replace TcHsType.emitTvImplication with TcUnify.checkTvConstraints,
  by analogy with TcUnify.checkConstraints.

* Inline TcUnify.buildImplication into its only call-site in
  TcUnify.checkConstraints

* TcS.buildImplication becomes TcS.CheckConstraintsTcS, with a
  simpler API

* Now that we have NoEvBindsVar we have no need of termEvidenceAllowed;
  nuke the latter, adding Note [No evidence bindings] to TcEvidence.
---
 testsuite/tests/dependent/should_fail/T14066d.stderr | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'testsuite/tests/dependent')

diff --git a/testsuite/tests/dependent/should_fail/T14066d.stderr b/testsuite/tests/dependent/should_fail/T14066d.stderr
index 3a8b90edce..3f5eb9825a 100644
--- a/testsuite/tests/dependent/should_fail/T14066d.stderr
+++ b/testsuite/tests/dependent/should_fail/T14066d.stderr
@@ -1,14 +1,14 @@
 
 T14066d.hs:11:35: error:
-    • Couldn't match type ‘b’ with ‘b1’
-      ‘b’ is a rigid type variable bound by
-        the type signature for:
-          f :: forall b. b -> (Proxy Maybe, ())
-        at T14066d.hs:10:1-37
+    • Couldn't match type ‘b1’ with ‘b’
       ‘b1’ is a rigid type variable bound by
         a type expected by the context:
           forall c b1 (a :: c). (Proxy a, Proxy c, b1)
         at T14066d.hs:11:33-35
+      ‘b’ is a rigid type variable bound by
+        the type signature for:
+          f :: forall b. b -> (Proxy Maybe, ())
+        at T14066d.hs:10:1-37
       Expected type: (Proxy a, Proxy c, b1)
         Actual type: (Proxy a, Proxy c, b)
     • In the first argument of ‘g’, namely ‘y’
-- 
cgit v1.2.1


From c4219d9f7d122a106fc8fb1e5cd9a62dadadf76c Mon Sep 17 00:00:00 2001
From: Alp Mestanogullari <alp@well-typed.com>
Date: Sat, 19 May 2018 14:00:21 -0400
Subject: Another batch of './validation --slow' tweaks

This finally gets us to a green ./validate --slow on linux for a ghc
checkout from the beginning of this week, see

  https://circleci.com/gh/ghc/ghc/4739

This is hopefully the final (or second to final) patch to
address #14890.

Test Plan: ./validate --slow

Reviewers: bgamari, hvr, simonmar

Reviewed By: bgamari

Subscribers: rwbarton, thomie, carter

GHC Trac Issues: #14890

Differential Revision: https://phabricator.haskell.org/D4712
---
 testsuite/tests/dependent/should_compile/all.T | 11 ++++++++++-
 1 file changed, 10 insertions(+), 1 deletion(-)

(limited to 'testsuite/tests/dependent')

diff --git a/testsuite/tests/dependent/should_compile/all.T b/testsuite/tests/dependent/should_compile/all.T
index 65853169bd..66221840bb 100644
--- a/testsuite/tests/dependent/should_compile/all.T
+++ b/testsuite/tests/dependent/should_compile/all.T
@@ -31,7 +31,16 @@ test('T13538', normal, compile, [''])
 test('T12176', normal, compile, [''])
 test('T14038', normal, compile, [''])
 test('T12742', normal, compile, [''])
-test('T13910', normal, compile, [''])
+# we omit profasm because it doesn't bring much to the table but
+# introduces its share of complexity, as the test as it is fails with
+# profasm:
+# T13910.hs:6:5: fatal:
+#     Cannot load -prof objects when GHC is built with -dynamic
+#     To fix this, either:
+#       (1) Use -fexternal-interpreter, or
+#       (2) Build the program twice: once with -dynamic, and then
+#           with -prof using -osuf to set a different object file suffix.
+test('T13910', omit_ways(['profasm']), compile, [''])
 test('T13938', [extra_files(['T13938a.hs'])], run_command,
      ['$MAKE -s --no-print-directory T13938'])
 test('T14556', normal, compile, [''])
-- 
cgit v1.2.1


From c16382d57ed9bf51089a14f079404ff8b4ce6eb2 Mon Sep 17 00:00:00 2001
From: Simon Peyton Jones <simonpj@microsoft.com>
Date: Thu, 7 Jun 2018 11:03:21 +0100
Subject: Remove ad-hoc special case in occAnal

Back in 1999 I put this ad-hoc code in the Case-handling
code for occAnal:

  occAnal env (Case scrut bndr ty alts)
   = ...
        -- Note [Case binder usage]
        -- ~~~~~~~~~~~~~~~~~~~~~~~~
        -- The case binder gets a usage of either "many" or "dead", never "one".
        -- Reason: we like to inline single occurrences, to eliminate a binding,
        -- but inlining a case binder *doesn't* eliminate a binding.
        -- We *don't* want to transform
        --      case x of w { (p,q) -> f w }
        -- into
        --      case x of w { (p,q) -> f (p,q) }
    tag_case_bndr usage bndr
      = (usage', setIdOccInfo bndr final_occ_info)
      where
        occ_info       = lookupDetails usage bndr
        usage'         = usage `delDetails` bndr
        final_occ_info = case occ_info of IAmDead -> IAmDead
                                          _       -> noOccInfo

But the comment looks wrong -- the bad inlining will not happen -- and
I think it relates to some long-ago version of the simplifier.

So I simply removed the special case, which gives more accurate
occurrence-info to the case binder.  Interestingly I got a slight
improvement in nofib binary sizes.

--------------------------------------------------------------------------------
        Program           Size    Allocs   Runtime   Elapsed  TotalMem
--------------------------------------------------------------------------------
      cacheprof          -0.1%     +0.2%     -0.7%     -1.2%     +8.6%
--------------------------------------------------------------------------------
            Min          -0.2%      0.0%    -14.5%    -30.5%      0.0%
            Max          -0.1%     +0.2%    +10.0%    +10.0%    +25.0%
 Geometric Mean          -0.2%     +0.0%     -1.9%     -5.4%     +0.3%

I have no idea if the improvement in runtime is real.  I did look at the
tiny increase in allocation for cacheprof and concluded that it was
unimportant (I forget the details).

Also the more accurate occ-info for the case binder meant that some
inlining happens in one pass that previously took successive passes
for the test dependent/should_compile/dynamic-paper (which has a
known Russel-paradox infinite loop in the simplifier).

In short, a small win: less ad-hoc complexity and slightly smaller
binaries.
---
 testsuite/tests/dependent/should_compile/all.T                | 2 +-
 testsuite/tests/dependent/should_compile/dynamic-paper.stderr | 1 +
 2 files changed, 2 insertions(+), 1 deletion(-)
 create mode 100644 testsuite/tests/dependent/should_compile/dynamic-paper.stderr

(limited to 'testsuite/tests/dependent')

diff --git a/testsuite/tests/dependent/should_compile/all.T b/testsuite/tests/dependent/should_compile/all.T
index 66221840bb..e153cafe41 100644
--- a/testsuite/tests/dependent/should_compile/all.T
+++ b/testsuite/tests/dependent/should_compile/all.T
@@ -17,7 +17,7 @@ test('T9632', normal, compile, [''])
 # discussed in #11330.
 test('dynamic-paper',
      expect_broken_for(11330, ['profasm']),
-     compile, [''])
+     compile_fail, [''])
 test('T11311', normal, compile, [''])
 test('T11405', normal, compile, [''])
 test('T11241', normal, compile, [''])
diff --git a/testsuite/tests/dependent/should_compile/dynamic-paper.stderr b/testsuite/tests/dependent/should_compile/dynamic-paper.stderr
new file mode 100644
index 0000000000..0519ecba6e
--- /dev/null
+++ b/testsuite/tests/dependent/should_compile/dynamic-paper.stderr
@@ -0,0 +1 @@
+ 
\ No newline at end of file
-- 
cgit v1.2.1


From 1508600cb2dd6b57d27742411489b8c46b78b53f Mon Sep 17 00:00:00 2001
From: Ben Gamari <ben@smart-cactus.org>
Date: Thu, 7 Jun 2018 22:05:51 +0000
Subject: testsuite: Fix dynamic-paper stderr file

The stderr file was empty, yet GHC fails with an error.
---
 .../tests/dependent/should_compile/dynamic-paper.stderr  | 16 +++++++++++++++-
 1 file changed, 15 insertions(+), 1 deletion(-)

(limited to 'testsuite/tests/dependent')

diff --git a/testsuite/tests/dependent/should_compile/dynamic-paper.stderr b/testsuite/tests/dependent/should_compile/dynamic-paper.stderr
index 0519ecba6e..3ba4db2219 100644
--- a/testsuite/tests/dependent/should_compile/dynamic-paper.stderr
+++ b/testsuite/tests/dependent/should_compile/dynamic-paper.stderr
@@ -1 +1,15 @@
- 
\ No newline at end of file
+Simplifier ticks exhausted
+  When trying UnfoldingDone delta1
+  To increase the limit, use -fsimpl-tick-factor=N (default 100).
+   
+  If you need to increase the limit substantially, please file a
+  bug report and indicate the factor you needed.
+   
+  If GHC was unable to complete compilation even with a very large factor
+  (a thousand or more), please consult the "Known bugs or infelicities"
+  section in the Users Guide before filing a report. There are a
+  few situations unlikely to occur in practical programs for which
+  simplifier non-termination has been judged acceptable.
+   
+  To see detailed counts use -ddump-simpl-stats
+  Total ticks: 140004
-- 
cgit v1.2.1


From 40db277f1dedd4df7e75cc0eb35aa7e1e1ded02a Mon Sep 17 00:00:00 2001
From: "HE, Tao" <sighingnow@gmail.com>
Date: Thu, 7 Jun 2018 20:43:55 -0400
Subject: Fix `print-explicit-runtime-reps` (#11786).

By fixing splitting of IfaceTypes in splitIfaceSigmaTy.

Test Plan: make test TEST="T11549 T11376 T11786"

Reviewers: goldfire, bgamari

Subscribers: rwbarton, thomie, carter

GHC Trac Issues: #11786, #11376

Differential Revision: https://phabricator.haskell.org/D4733
---
 testsuite/tests/dependent/ghci/T11549.script |  4 ++++
 testsuite/tests/dependent/ghci/T11549.stdout | 17 +++++++++++++----
 testsuite/tests/dependent/ghci/T11786.script | 11 +++++++++++
 testsuite/tests/dependent/ghci/T11786.stdout | 15 +++++++++++++++
 testsuite/tests/dependent/ghci/all.T         |  6 ++----
 5 files changed, 45 insertions(+), 8 deletions(-)
 create mode 100644 testsuite/tests/dependent/ghci/T11786.script
 create mode 100644 testsuite/tests/dependent/ghci/T11786.stdout

(limited to 'testsuite/tests/dependent')

diff --git a/testsuite/tests/dependent/ghci/T11549.script b/testsuite/tests/dependent/ghci/T11549.script
index bb35589671..d8a0e97a61 100644
--- a/testsuite/tests/dependent/ghci/T11549.script
+++ b/testsuite/tests/dependent/ghci/T11549.script
@@ -3,12 +3,16 @@ import GHC.Exts
 
 putStrLn "-fno-print-explicit-runtime-reps"
 :set -fno-print-explicit-runtime-reps
+:type ($)
 :info ($)
 :kind TYPE
+:type error
 :info error
 
 putStrLn "\n-fprint-explicit-runtime-reps"
 :set -fprint-explicit-runtime-reps
+:type ($)
 :info ($)
 :kind TYPE
+:type error
 :info error
diff --git a/testsuite/tests/dependent/ghci/T11549.stdout b/testsuite/tests/dependent/ghci/T11549.stdout
index c8449ba09f..5e23c0da99 100644
--- a/testsuite/tests/dependent/ghci/T11549.stdout
+++ b/testsuite/tests/dependent/ghci/T11549.stdout
@@ -1,12 +1,21 @@
 -fno-print-explicit-runtime-reps
 ($) :: (a -> b) -> a -> b
+($) :: (a -> b) -> a -> b 	-- Defined in ‘GHC.Base’
+infixr 0 $
 TYPE :: RuntimeRep -> *
+error :: [Char] -> a
 error :: GHC.Stack.Types.HasCallStack => [Char] -> a
+  	-- Defined in ‘GHC.Err’
 
 -fprint-explicit-runtime-reps
+($) :: (a -> b) -> a -> b
 ($) :: forall (r :: RuntimeRep) a (b :: TYPE r). (a -> b) -> a -> b
+  	-- Defined in ‘GHC.Base’
+infixr 0 $
 TYPE :: RuntimeRep -> *
-error
-  :: forall (r :: RuntimeRep) (a :: TYPE r).
-     GHC.Stack.Types.HasCallStack =>
-     [Char] -> a
+error :: [Char] -> a
+error ::
+  forall (r :: RuntimeRep) (a :: TYPE r).
+  GHC.Stack.Types.HasCallStack =>
+  [Char] -> a
+  	-- Defined in ‘GHC.Err’
diff --git a/testsuite/tests/dependent/ghci/T11786.script b/testsuite/tests/dependent/ghci/T11786.script
new file mode 100644
index 0000000000..61e3141843
--- /dev/null
+++ b/testsuite/tests/dependent/ghci/T11786.script
@@ -0,0 +1,11 @@
+:set -fno-print-explicit-runtime-reps
+:t ($)
+:t (($))
+:t +v ($)
+:i ($)
+
+:set -fprint-explicit-runtime-reps
+:t ($)
+:t (($))
+:t +v ($)
+:i ($)
diff --git a/testsuite/tests/dependent/ghci/T11786.stdout b/testsuite/tests/dependent/ghci/T11786.stdout
new file mode 100644
index 0000000000..93616ed750
--- /dev/null
+++ b/testsuite/tests/dependent/ghci/T11786.stdout
@@ -0,0 +1,15 @@
+($) :: (a -> b) -> a -> b
+(($)) :: (a -> b) -> a -> b
+($) :: (a -> b) -> a -> b
+($) :: (a -> b) -> a -> b 	-- Defined in ‘GHC.Base’
+infixr 0 $
+($) :: (a -> b) -> a -> b
+(($)) :: (a -> b) -> a -> b
+($)
+  :: forall (r :: GHC.Types.RuntimeRep) a (b :: TYPE r).
+     (a -> b) -> a -> b
+($) ::
+  forall (r :: GHC.Types.RuntimeRep) a (b :: TYPE r).
+  (a -> b) -> a -> b
+  	-- Defined in ‘GHC.Base’
+infixr 0 $
diff --git a/testsuite/tests/dependent/ghci/all.T b/testsuite/tests/dependent/ghci/all.T
index bd819c28bc..89ebab0e44 100644
--- a/testsuite/tests/dependent/ghci/all.T
+++ b/testsuite/tests/dependent/ghci/all.T
@@ -1,5 +1,3 @@
-test('T11549',
-     [ expect_broken( 11787 ),
-       expect_broken( 11786 ) ],
-     ghci_script, ['T11549.script'])
+test('T11549', normal, ghci_script, ['T11549.script'])
+test('T11786', normal, ghci_script, ['T11786.script'])
 test('T14238', normal, ghci_script, ['T14238.script'])
-- 
cgit v1.2.1


From d650729f9a0f3b6aa5e6ef2d5fba337f6f70fa60 Mon Sep 17 00:00:00 2001
From: Vladislav Zavialov <vlad.z.4096@gmail.com>
Date: Thu, 14 Jun 2018 15:02:36 -0400
Subject: Embrace -XTypeInType, add -XStarIsType

Summary:
Implement the "Embrace Type :: Type" GHC proposal,
.../ghc-proposals/blob/master/proposals/0020-no-type-in-type.rst

GHC 8.0 included a major change to GHC's type system: the Type :: Type
axiom. Though casual users were protected from this by hiding its
features behind the -XTypeInType extension, all programs written in GHC
8+ have the axiom behind the scenes. In order to preserve backward
compatibility, various legacy features were left unchanged. For example,
with -XDataKinds but not -XTypeInType, GADTs could not be used in types.
Now these restrictions are lifted and -XTypeInType becomes a redundant
flag that will be eventually deprecated.

* Incorporate the features currently in -XTypeInType into the
  -XPolyKinds and -XDataKinds extensions.
* Introduce a new extension -XStarIsType to control how to parse * in
  code and whether to print it in error messages.

Test Plan: Validate

Reviewers: goldfire, hvr, bgamari, alanz, simonpj

Reviewed By: goldfire, simonpj

Subscribers: rwbarton, thomie, mpickering, carter

GHC Trac Issues: #15195

Differential Revision: https://phabricator.haskell.org/D4748
---
 testsuite/tests/dependent/ghci/T11549.script       |  2 +-
 testsuite/tests/dependent/ghci/T14238.stdout       |  2 +-
 testsuite/tests/dependent/should_compile/Dep1.hs   |  2 +-
 testsuite/tests/dependent/should_compile/Dep2.hs   |  2 +-
 testsuite/tests/dependent/should_compile/Dep3.hs   |  2 +-
 .../tests/dependent/should_compile/DkNameRes.hs    |  9 +++++++
 .../dependent/should_compile/InferDependency.hs    |  6 -----
 .../dependent/should_compile/KindEqualities.hs     |  2 +-
 .../dependent/should_compile/KindEqualities2.hs    |  3 +--
 .../tests/dependent/should_compile/KindLevels.hs   |  2 +-
 .../tests/dependent/should_compile/RAE_T32b.hs     | 24 +++++++++++--------
 testsuite/tests/dependent/should_compile/Rae31.hs  | 23 ++++++++++--------
 .../tests/dependent/should_compile/RaeBlogPost.hs  | 27 ++++++++++-----------
 .../tests/dependent/should_compile/RaeJobTalk.hs   |  2 +-
 testsuite/tests/dependent/should_compile/T11405.hs |  2 +-
 testsuite/tests/dependent/should_compile/T11635.hs |  2 +-
 testsuite/tests/dependent/should_compile/T11711.hs |  1 -
 testsuite/tests/dependent/should_compile/T11719.hs |  6 ++---
 testsuite/tests/dependent/should_compile/T11966.hs |  1 -
 testsuite/tests/dependent/should_compile/T12176.hs |  2 +-
 testsuite/tests/dependent/should_compile/T12442.hs |  4 ++--
 testsuite/tests/dependent/should_compile/T12742.hs |  2 +-
 testsuite/tests/dependent/should_compile/T13910.hs |  9 +++----
 testsuite/tests/dependent/should_compile/T13938.hs |  3 ++-
 .../tests/dependent/should_compile/T13938a.hs      |  3 ++-
 testsuite/tests/dependent/should_compile/T14038.hs |  3 ++-
 .../tests/dependent/should_compile/T14066a.hs      |  2 +-
 testsuite/tests/dependent/should_compile/T14556.hs |  3 ++-
 testsuite/tests/dependent/should_compile/T14720.hs |  3 ++-
 testsuite/tests/dependent/should_compile/T14749.hs |  2 +-
 testsuite/tests/dependent/should_compile/T14991.hs |  3 ++-
 testsuite/tests/dependent/should_compile/T9632.hs  |  2 +-
 .../tests/dependent/should_compile/TypeLevelVec.hs |  2 +-
 testsuite/tests/dependent/should_compile/all.T     |  1 +
 .../dependent/should_compile/dynamic-paper.hs      | 27 ++++++++++++---------
 .../tests/dependent/should_compile/mkGADTVars.hs   |  2 +-
 .../tests/dependent/should_fail/BadTelescope.hs    |  2 +-
 .../tests/dependent/should_fail/BadTelescope2.hs   |  2 +-
 .../tests/dependent/should_fail/BadTelescope3.hs   |  2 +-
 .../tests/dependent/should_fail/BadTelescope4.hs   |  2 +-
 testsuite/tests/dependent/should_fail/DepFail1.hs  |  2 +-
 .../tests/dependent/should_fail/InferDependency.hs |  2 +-
 .../tests/dependent/should_fail/KindLevelsB.hs     |  9 -------
 .../tests/dependent/should_fail/KindLevelsB.stderr |  5 ----
 .../tests/dependent/should_fail/PromotedClass.hs   |  2 +-
 testsuite/tests/dependent/should_fail/RAE_T32a.hs  | 28 ++++++++++++----------
 .../tests/dependent/should_fail/RAE_T32a.stderr    |  6 ++---
 .../tests/dependent/should_fail/RenamingStar.hs    |  2 +-
 .../dependent/should_fail/RenamingStar.stderr      | 10 ++------
 testsuite/tests/dependent/should_fail/SelfDep.hs   |  2 ++
 .../tests/dependent/should_fail/SelfDep.stderr     |  8 +++----
 testsuite/tests/dependent/should_fail/T11407.hs    |  2 +-
 testsuite/tests/dependent/should_fail/T11473.hs    |  2 +-
 testsuite/tests/dependent/should_fail/T12081.hs    |  2 +-
 testsuite/tests/dependent/should_fail/T12174.hs    |  2 +-
 testsuite/tests/dependent/should_fail/T13135.hs    |  4 ++--
 testsuite/tests/dependent/should_fail/T13601.hs    |  2 +-
 testsuite/tests/dependent/should_fail/T13780a.hs   |  2 +-
 testsuite/tests/dependent/should_fail/T13780b.hs   |  3 ++-
 testsuite/tests/dependent/should_fail/T13780c.hs   |  2 +-
 .../tests/dependent/should_fail/T13780c.stderr     |  6 +++--
 testsuite/tests/dependent/should_fail/T14066.hs    |  4 ++--
 testsuite/tests/dependent/should_fail/T14066c.hs   |  2 +-
 testsuite/tests/dependent/should_fail/T14066d.hs   |  2 +-
 testsuite/tests/dependent/should_fail/T14066e.hs   |  2 +-
 testsuite/tests/dependent/should_fail/T14066f.hs   |  2 +-
 testsuite/tests/dependent/should_fail/T14066g.hs   |  2 +-
 testsuite/tests/dependent/should_fail/T14066h.hs   |  2 +-
 testsuite/tests/dependent/should_fail/T15245.hs    | 10 ++++++++
 .../tests/dependent/should_fail/T15245.stderr      |  7 ++++++
 .../tests/dependent/should_fail/TypeSkolEscape.hs  |  2 +-
 testsuite/tests/dependent/should_fail/all.T        |  2 +-
 testsuite/tests/dependent/should_run/T11964a.hs    |  2 +-
 73 files changed, 183 insertions(+), 160 deletions(-)
 create mode 100644 testsuite/tests/dependent/should_compile/DkNameRes.hs
 delete mode 100644 testsuite/tests/dependent/should_compile/InferDependency.hs
 delete mode 100644 testsuite/tests/dependent/should_fail/KindLevelsB.hs
 delete mode 100644 testsuite/tests/dependent/should_fail/KindLevelsB.stderr
 create mode 100644 testsuite/tests/dependent/should_fail/T15245.hs
 create mode 100644 testsuite/tests/dependent/should_fail/T15245.stderr

(limited to 'testsuite/tests/dependent')

diff --git a/testsuite/tests/dependent/ghci/T11549.script b/testsuite/tests/dependent/ghci/T11549.script
index d8a0e97a61..3e0811f921 100644
--- a/testsuite/tests/dependent/ghci/T11549.script
+++ b/testsuite/tests/dependent/ghci/T11549.script
@@ -1,4 +1,4 @@
-:set -XTypeInType
+:set -XPolyKinds
 import GHC.Exts
 
 putStrLn "-fno-print-explicit-runtime-reps"
diff --git a/testsuite/tests/dependent/ghci/T14238.stdout b/testsuite/tests/dependent/ghci/T14238.stdout
index fddbc0de54..729f821af7 100644
--- a/testsuite/tests/dependent/ghci/T14238.stdout
+++ b/testsuite/tests/dependent/ghci/T14238.stdout
@@ -1 +1 @@
-Foo :: forall k -> k -> *
+Foo :: forall k -> k -> Type
diff --git a/testsuite/tests/dependent/should_compile/Dep1.hs b/testsuite/tests/dependent/should_compile/Dep1.hs
index 6f8fe0720d..086d759bbe 100644
--- a/testsuite/tests/dependent/should_compile/Dep1.hs
+++ b/testsuite/tests/dependent/should_compile/Dep1.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE DataKinds, PolyKinds #-}
 
 module Dep1 where
 
diff --git a/testsuite/tests/dependent/should_compile/Dep2.hs b/testsuite/tests/dependent/should_compile/Dep2.hs
index df1cb51e08..34be3cffc6 100644
--- a/testsuite/tests/dependent/should_compile/Dep2.hs
+++ b/testsuite/tests/dependent/should_compile/Dep2.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE TypeInType, GADTs #-}
+{-# LANGUAGE PolyKinds, GADTs #-}
 
 module Dep2 where
 
diff --git a/testsuite/tests/dependent/should_compile/Dep3.hs b/testsuite/tests/dependent/should_compile/Dep3.hs
index cba5043a08..db10d2a8c6 100644
--- a/testsuite/tests/dependent/should_compile/Dep3.hs
+++ b/testsuite/tests/dependent/should_compile/Dep3.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE TypeFamilies, TypeInType, GADTs #-}
+{-# LANGUAGE TypeFamilies, DataKinds, PolyKinds, GADTs #-}
 
 module Dep3 where
 
diff --git a/testsuite/tests/dependent/should_compile/DkNameRes.hs b/testsuite/tests/dependent/should_compile/DkNameRes.hs
new file mode 100644
index 0000000000..4110b33882
--- /dev/null
+++ b/testsuite/tests/dependent/should_compile/DkNameRes.hs
@@ -0,0 +1,9 @@
+{-# LANGUAGE TypeFamilies, DataKinds, PolyKinds #-}
+
+module DkNameRes where
+
+import Data.Proxy
+import Data.Kind
+
+type family IfK (e :: Proxy (j :: Bool)) :: Type where
+   IfK (_ :: Proxy True) = ()
diff --git a/testsuite/tests/dependent/should_compile/InferDependency.hs b/testsuite/tests/dependent/should_compile/InferDependency.hs
deleted file mode 100644
index 47957d47d6..0000000000
--- a/testsuite/tests/dependent/should_compile/InferDependency.hs
+++ /dev/null
@@ -1,6 +0,0 @@
-{-# LANGUAGE TypeInType #-}
-
-module InferDependency where
-
-data Proxy k (a :: k)
-data Proxy2 k a = P (Proxy k a)
diff --git a/testsuite/tests/dependent/should_compile/KindEqualities.hs b/testsuite/tests/dependent/should_compile/KindEqualities.hs
index 4cba8281ca..1caa46f7c3 100644
--- a/testsuite/tests/dependent/should_compile/KindEqualities.hs
+++ b/testsuite/tests/dependent/should_compile/KindEqualities.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE TypeInType, GADTs, ExplicitForAll #-}
+{-# LANGUAGE PolyKinds, GADTs, ExplicitForAll #-}
 {-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
 
 module KindEqualities where
diff --git a/testsuite/tests/dependent/should_compile/KindEqualities2.hs b/testsuite/tests/dependent/should_compile/KindEqualities2.hs
index 5a6f60d40b..0bdfcfa034 100644
--- a/testsuite/tests/dependent/should_compile/KindEqualities2.hs
+++ b/testsuite/tests/dependent/should_compile/KindEqualities2.hs
@@ -1,6 +1,5 @@
 {-# LANGUAGE DataKinds, GADTs, PolyKinds, TypeFamilies, ExplicitForAll,
-             TemplateHaskell, UndecidableInstances, ScopedTypeVariables,
-             TypeInType #-}
+             TemplateHaskell, UndecidableInstances, ScopedTypeVariables #-}
 
 module KindEqualities2 where
 
diff --git a/testsuite/tests/dependent/should_compile/KindLevels.hs b/testsuite/tests/dependent/should_compile/KindLevels.hs
index 1aad299df3..5540ce40cd 100644
--- a/testsuite/tests/dependent/should_compile/KindLevels.hs
+++ b/testsuite/tests/dependent/should_compile/KindLevels.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE DataKinds, PolyKinds #-}
 
 module KindLevels where
 
diff --git a/testsuite/tests/dependent/should_compile/RAE_T32b.hs b/testsuite/tests/dependent/should_compile/RAE_T32b.hs
index 7e067099c9..ddd21db18d 100644
--- a/testsuite/tests/dependent/should_compile/RAE_T32b.hs
+++ b/testsuite/tests/dependent/should_compile/RAE_T32b.hs
@@ -1,23 +1,27 @@
 {-# LANGUAGE TemplateHaskell, TypeFamilies, GADTs, DataKinds, PolyKinds,
-             RankNTypes, TypeOperators, TypeInType #-}
+             RankNTypes, TypeOperators #-}
 
 module RAE_T32b where
 
 import Data.Kind
 
-data family Sing (k :: *) :: k -> *
+data family Sing (k :: Type) :: k -> Type
 
-data TyArr (a :: *) (b :: *) :: *
-type family (a :: TyArr k1 k2 -> *) @@ (b :: k1) :: k2
+data TyArr (a :: Type) (b :: Type) :: Type
+type family (a :: TyArr k1 k2 -> Type) @@ (b :: k1) :: k2
 $(return [])
 
-data Sigma (p :: *) (r :: TyArr p * -> *) :: * where
-  Sigma :: forall (p :: *) (r :: TyArr p * -> *) (a :: p) (b :: r @@ a).
-           Sing * p -> Sing (TyArr p * -> *) r -> Sing p a -> Sing (r @@ a) b -> Sigma p r
+data Sigma (p :: Type) (r :: TyArr p Type -> Type) :: Type where
+  Sigma :: forall (p :: Type) (r :: TyArr p Type -> Type)
+                  (a :: p) (b :: r @@ a).
+           Sing Type p -> Sing (TyArr p Type -> Type) r -> Sing p a ->
+           Sing (r @@ a) b -> Sigma p r
 $(return [])
 
-data instance Sing (Sigma p r) (x :: Sigma p r) :: * where
-  SSigma :: forall (p :: *) (r :: TyArr p * -> *) (a :: p) (b :: r @@ a)
-            (sp :: Sing * p) (sr :: Sing (TyArr p * -> *) r) (sa :: Sing p a) (sb :: Sing (r @@ a) b).
+data instance Sing (Sigma p r) (x :: Sigma p r) :: Type where
+  SSigma :: forall (p :: Type) (r :: TyArr p Type -> Type)
+                   (a :: p) (b :: r @@ a)
+                   (sp :: Sing Type p) (sr :: Sing (TyArr p Type -> Type) r)
+                   (sa :: Sing p a) (sb :: Sing (r @@ a) b).
             Sing (Sing (r @@ a) b) sb ->
             Sing (Sigma p r) ('Sigma sp sr sa sb)
diff --git a/testsuite/tests/dependent/should_compile/Rae31.hs b/testsuite/tests/dependent/should_compile/Rae31.hs
index cedc019cf3..7a50b606ee 100644
--- a/testsuite/tests/dependent/should_compile/Rae31.hs
+++ b/testsuite/tests/dependent/should_compile/Rae31.hs
@@ -1,24 +1,27 @@
 {-# LANGUAGE TemplateHaskell, TypeOperators, PolyKinds, DataKinds,
-             TypeFamilies, TypeInType #-}
+             TypeFamilies #-}
 
 module A where
 
 import Data.Kind
 
-data family Sing (k :: *) :: k -> *
+data family Sing (k :: Type) :: k -> Type
 type Sing' (x :: k) = Sing k x
-data TyFun' (a :: *) (b :: *) :: *
-type TyFun (a :: *) (b :: *) = TyFun' a b -> *
+data TyFun' (a :: Type) (b :: Type) :: Type
+type TyFun (a :: Type) (b :: Type) = TyFun' a b -> Type
 type family (a :: TyFun k1 k2) @@ (b :: k1) :: k2
-data TyPi' (a :: *) (b :: TyFun a *) :: *
-type TyPi (a :: *) (b :: TyFun a *) = TyPi' a b -> *
+data TyPi' (a :: Type) (b :: TyFun a Type) :: Type
+type TyPi (a :: Type) (b :: TyFun a Type) = TyPi' a b -> Type
 type family (a :: TyPi k1 k2) @@@ (b :: k1) :: k2 @@ b
 $(return [])
 
-data A (a :: *) (b :: a) (c :: TyFun' a *) -- A :: forall a -> a -> a ~> *
-type instance (@@) (A a b) c = *
+data A (a :: Type) (b :: a) (c :: TyFun' a Type)
+  -- A :: forall a -> a -> a ~> Type
+type instance (@@) (A a b) c = Type
 $(return [])
-data B (a :: *) (b :: TyFun' a *) -- B :: forall a -> a ~> *
+data B (a :: Type) (b :: TyFun' a Type)
+  -- B :: forall a -> a ~> Type
 type instance (@@) (B a) b = TyPi a (A a b)
 $(return [])
-data C (a :: *) (b :: TyPi a (B a)) (c :: a) (d :: a) (e :: TyFun' (b @@@ c @@@ d) *)
+data C (a :: Type) (b :: TyPi a (B a)) (c :: a) (d :: a)
+       (e :: TyFun' (b @@@ c @@@ d) Type)
diff --git a/testsuite/tests/dependent/should_compile/RaeBlogPost.hs b/testsuite/tests/dependent/should_compile/RaeBlogPost.hs
index e99c7b5dd5..b048a49e44 100644
--- a/testsuite/tests/dependent/should_compile/RaeBlogPost.hs
+++ b/testsuite/tests/dependent/should_compile/RaeBlogPost.hs
@@ -1,5 +1,4 @@
-{-# LANGUAGE DataKinds, PolyKinds, GADTs, TypeOperators, TypeFamilies,
-             TypeInType #-}
+{-# LANGUAGE DataKinds, PolyKinds, GADTs, TypeOperators, TypeFamilies #-}
 {-# OPTIONS_GHC -fwarn-unticked-promoted-constructors #-}
 
 module RaeBlogPost where
@@ -8,7 +7,7 @@ import Data.Kind
 
 -- a Proxy type with an explicit kind
 data Proxy k (a :: k) = P
-prox :: Proxy * Bool
+prox :: Proxy Type Bool
 prox = P
 
 prox2 :: Proxy Bool 'True
@@ -16,11 +15,11 @@ prox2 = P
 
 -- implicit kinds still work
 data A
-data B :: A -> *
-data C :: B a -> *
-data D :: C b -> *
-data E :: D c -> *
--- note that E :: forall (a :: A) (b :: B a) (c :: C b). D c -> *
+data B :: A -> Type
+data C :: B a -> Type
+data D :: C b -> Type
+data E :: D c -> Type
+-- note that E :: forall (a :: A) (b :: B a) (c :: C b). D c -> Type
 
 -- a kind-indexed GADT
 data TypeRep (a :: k) where
@@ -37,7 +36,7 @@ type family a + b where
   'Zero     + b = b
   ('Succ a) + b = 'Succ (a + b)
 
-data Vec :: * -> Nat -> * where
+data Vec :: Type -> Nat -> Type where
   Nil  :: Vec a 'Zero
   (:>) :: a -> Vec a n -> Vec a ('Succ n)
 infixr 5 :>
@@ -47,17 +46,17 @@ type family (x :: Vec a n) ++ (y :: Vec a m) :: Vec a (n + m) where
   'Nil      ++ y = y
   (h ':> t) ++ y = h ':> (t ++ y)
 
--- datatype that mentions *
-data U = Star (*)
+-- datatype that mentions Type
+data U = Star (Type)
        | Bool Bool
 
 -- kind synonym
-type Monadish = * -> *
+type Monadish = Type -> Type
 class MonadTrans (t :: Monadish -> Monadish) where
   lift :: Monad m => m a -> t m a
 data Free :: Monadish where
   Return :: a -> Free a
   Bind   :: Free a -> (a -> Free b) -> Free b
 
--- yes, * really does have type *.
-type Star = (* :: (* :: (* :: *)))
+-- yes, Type really does have type Type.
+type Star = (Type :: (Type :: (Type :: Type)))
diff --git a/testsuite/tests/dependent/should_compile/RaeJobTalk.hs b/testsuite/tests/dependent/should_compile/RaeJobTalk.hs
index 480db090c3..1a22573109 100644
--- a/testsuite/tests/dependent/should_compile/RaeJobTalk.hs
+++ b/testsuite/tests/dependent/should_compile/RaeJobTalk.hs
@@ -3,7 +3,7 @@
 
 {-# LANGUAGE TypeOperators, TypeFamilies, TypeApplications, AllowAmbiguousTypes,
              ExplicitForAll, ScopedTypeVariables, GADTs, TypeFamilyDependencies,
-             TypeInType, ConstraintKinds, UndecidableInstances,
+             DataKinds, PolyKinds , ConstraintKinds, UndecidableInstances,
              FlexibleInstances, MultiParamTypeClasses, FunctionalDependencies,
              FlexibleContexts, StandaloneDeriving, InstanceSigs,
              RankNTypes, UndecidableSuperClasses #-}
diff --git a/testsuite/tests/dependent/should_compile/T11405.hs b/testsuite/tests/dependent/should_compile/T11405.hs
index cdb713f118..5fdd7baed1 100644
--- a/testsuite/tests/dependent/should_compile/T11405.hs
+++ b/testsuite/tests/dependent/should_compile/T11405.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE ImplicitParams, TypeInType, ExplicitForAll #-}
+{-# LANGUAGE ImplicitParams, PolyKinds, ExplicitForAll #-}
 
 module T11405 where
 
diff --git a/testsuite/tests/dependent/should_compile/T11635.hs b/testsuite/tests/dependent/should_compile/T11635.hs
index 2292def966..61d9978e55 100644
--- a/testsuite/tests/dependent/should_compile/T11635.hs
+++ b/testsuite/tests/dependent/should_compile/T11635.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE TypeInType, KindSignatures, ExplicitForAll, RankNTypes #-}
+{-# LANGUAGE PolyKinds, KindSignatures, ExplicitForAll, RankNTypes #-}
 
 module T11635 where
 
diff --git a/testsuite/tests/dependent/should_compile/T11711.hs b/testsuite/tests/dependent/should_compile/T11711.hs
index 0cd4dceb42..814b2a4a68 100644
--- a/testsuite/tests/dependent/should_compile/T11711.hs
+++ b/testsuite/tests/dependent/should_compile/T11711.hs
@@ -5,7 +5,6 @@
 {-# LANGUAGE KindSignatures #-}
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE ViewPatterns #-}
-{-# LANGUAGE TypeInType #-}
 {-# LANGUAGE TypeSynonymInstances #-}
 {-# LANGUAGE FlexibleInstances #-}
 
diff --git a/testsuite/tests/dependent/should_compile/T11719.hs b/testsuite/tests/dependent/should_compile/T11719.hs
index ba4d7c9db4..e4c2a89bf2 100644
--- a/testsuite/tests/dependent/should_compile/T11719.hs
+++ b/testsuite/tests/dependent/should_compile/T11719.hs
@@ -1,12 +1,12 @@
-{-# LANGUAGE RankNTypes, TypeFamilies, TypeInType, TypeOperators,
+{-# LANGUAGE RankNTypes, TypeFamilies, TypeOperators, DataKinds, PolyKinds,
              UndecidableInstances #-}
 
 module T11719 where
 
 import Data.Kind
 
-data TyFun :: * -> * -> *
-type a ~> b = TyFun a b -> *
+data TyFun :: Type -> Type -> Type
+type a ~> b = TyFun a b -> Type
 
 type family (f :: a ~> b) @@ (x :: a) :: b
 
diff --git a/testsuite/tests/dependent/should_compile/T11966.hs b/testsuite/tests/dependent/should_compile/T11966.hs
index 0262a0aed3..daad450f13 100644
--- a/testsuite/tests/dependent/should_compile/T11966.hs
+++ b/testsuite/tests/dependent/should_compile/T11966.hs
@@ -3,7 +3,6 @@
 {-# LANGUAGE KindSignatures #-}
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE RankNTypes #-}
-{-# LANGUAGE TypeInType #-}
 {-# LANGUAGE TypeOperators #-}
 
 module T11966 where
diff --git a/testsuite/tests/dependent/should_compile/T12176.hs b/testsuite/tests/dependent/should_compile/T12176.hs
index 0e340068a7..a11c151567 100644
--- a/testsuite/tests/dependent/should_compile/T12176.hs
+++ b/testsuite/tests/dependent/should_compile/T12176.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE RankNTypes, TypeInType, GADTs, TypeFamilies #-}
+{-# LANGUAGE RankNTypes, DataKinds, PolyKinds, GADTs, TypeFamilies #-}
 
 module T12176 where
 
diff --git a/testsuite/tests/dependent/should_compile/T12442.hs b/testsuite/tests/dependent/should_compile/T12442.hs
index f9dbf0a486..c76dfb962e 100644
--- a/testsuite/tests/dependent/should_compile/T12442.hs
+++ b/testsuite/tests/dependent/should_compile/T12442.hs
@@ -1,7 +1,7 @@
 -- Based on https://github.com/idris-lang/Idris-dev/blob/v0.9.10/libs/effects/Effects.idr
 
-{-# LANGUAGE TypeInType, ScopedTypeVariables, TypeOperators, TypeApplications,
-             GADTs, TypeFamilies, AllowAmbiguousTypes #-}
+{-# LANGUAGE DataKinds, PolyKinds, ScopedTypeVariables, TypeOperators,
+             TypeApplications, GADTs, TypeFamilies, AllowAmbiguousTypes #-}
 
 module T12442 where
 
diff --git a/testsuite/tests/dependent/should_compile/T12742.hs b/testsuite/tests/dependent/should_compile/T12742.hs
index baa3e2c071..988d7c318a 100644
--- a/testsuite/tests/dependent/should_compile/T12742.hs
+++ b/testsuite/tests/dependent/should_compile/T12742.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE TypeInType, RankNTypes, TypeFamilies #-}
+{-# LANGUAGE DataKinds, PolyKinds, RankNTypes, TypeFamilies #-}
 
 module T12742 where
 
diff --git a/testsuite/tests/dependent/should_compile/T13910.hs b/testsuite/tests/dependent/should_compile/T13910.hs
index 82d47e45bc..b3707dd365 100644
--- a/testsuite/tests/dependent/should_compile/T13910.hs
+++ b/testsuite/tests/dependent/should_compile/T13910.hs
@@ -7,7 +7,8 @@
 {-# LANGUAGE Trustworthy #-}
 {-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE TypeFamilyDependencies #-}
-{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE TypeOperators #-}
 module T13910 where
 
@@ -17,7 +18,7 @@ import Data.Type.Equality
 data family Sing (a :: k)
 
 class SingKind k where
-  type Demote k = (r :: *) | r -> k
+  type Demote k = (r :: Type) | r -> k
   fromSing :: Sing (a :: k) -> Demote k
   toSing   :: Demote k -> SomeSing k
 
@@ -33,8 +34,8 @@ withSomeSing x f =
   case toSing x of
     SomeSing x' -> f x'
 
-data TyFun :: * -> * -> *
-type a ~> b = TyFun a b -> *
+data TyFun :: Type -> Type -> Type
+type a ~> b = TyFun a b -> Type
 infixr 0 ~>
 
 type family Apply (f :: k1 ~> k2) (x :: k1) :: k2
diff --git a/testsuite/tests/dependent/should_compile/T13938.hs b/testsuite/tests/dependent/should_compile/T13938.hs
index dd4f3d6c7c..1ce77d194f 100644
--- a/testsuite/tests/dependent/should_compile/T13938.hs
+++ b/testsuite/tests/dependent/should_compile/T13938.hs
@@ -4,7 +4,8 @@
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE TypeFamilies #-}
-{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE UndecidableInstances #-}
 module T13938 where
diff --git a/testsuite/tests/dependent/should_compile/T13938a.hs b/testsuite/tests/dependent/should_compile/T13938a.hs
index 3a09292922..5197747e87 100644
--- a/testsuite/tests/dependent/should_compile/T13938a.hs
+++ b/testsuite/tests/dependent/should_compile/T13938a.hs
@@ -7,7 +7,8 @@
 {-# LANGUAGE TemplateHaskell #-}
 {-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE TypeFamilies #-}
-{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE TypeOperators #-}
 module T13938a where
 
diff --git a/testsuite/tests/dependent/should_compile/T14038.hs b/testsuite/tests/dependent/should_compile/T14038.hs
index 839220a0ce..04b24b9f9e 100644
--- a/testsuite/tests/dependent/should_compile/T14038.hs
+++ b/testsuite/tests/dependent/should_compile/T14038.hs
@@ -6,7 +6,8 @@
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE TypeFamilies #-}
-{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE TypeOperators #-}
 module T14038 where
 
diff --git a/testsuite/tests/dependent/should_compile/T14066a.hs b/testsuite/tests/dependent/should_compile/T14066a.hs
index e1a6255520..30b203d31b 100644
--- a/testsuite/tests/dependent/should_compile/T14066a.hs
+++ b/testsuite/tests/dependent/should_compile/T14066a.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE TypeFamilies, TypeInType, ExplicitForAll, GADTs,
+{-# LANGUAGE TypeFamilies, DataKinds, PolyKinds, ExplicitForAll, GADTs,
              UndecidableInstances, RankNTypes, ScopedTypeVariables #-}
 
 module T14066a where
diff --git a/testsuite/tests/dependent/should_compile/T14556.hs b/testsuite/tests/dependent/should_compile/T14556.hs
index eebbdca888..133a9e6a44 100644
--- a/testsuite/tests/dependent/should_compile/T14556.hs
+++ b/testsuite/tests/dependent/should_compile/T14556.hs
@@ -1,4 +1,5 @@
-{-# Language UndecidableInstances, DataKinds, TypeOperators, KindSignatures, PolyKinds, TypeInType, TypeFamilies, GADTs, LambdaCase, ScopedTypeVariables #-}
+{-# Language UndecidableInstances, DataKinds, TypeOperators, PolyKinds,
+             TypeFamilies, GADTs, LambdaCase, ScopedTypeVariables #-}
 
 module T14556 where
 
diff --git a/testsuite/tests/dependent/should_compile/T14720.hs b/testsuite/tests/dependent/should_compile/T14720.hs
index c26a184689..0f053756f5 100644
--- a/testsuite/tests/dependent/should_compile/T14720.hs
+++ b/testsuite/tests/dependent/should_compile/T14720.hs
@@ -3,7 +3,8 @@
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeFamilies #-}
-{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE TypeOperators #-}
 module T14720 where
 
diff --git a/testsuite/tests/dependent/should_compile/T14749.hs b/testsuite/tests/dependent/should_compile/T14749.hs
index 79bcce66ff..c4480fad0f 100644
--- a/testsuite/tests/dependent/should_compile/T14749.hs
+++ b/testsuite/tests/dependent/should_compile/T14749.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE GADTs, TypeOperators, DataKinds, TypeFamilies, TypeInType #-}
+{-# LANGUAGE GADTs, TypeOperators, DataKinds, TypeFamilies, PolyKinds #-}
 
 module T14749 where
 
diff --git a/testsuite/tests/dependent/should_compile/T14991.hs b/testsuite/tests/dependent/should_compile/T14991.hs
index f435c37690..b2f5642ec5 100644
--- a/testsuite/tests/dependent/should_compile/T14991.hs
+++ b/testsuite/tests/dependent/should_compile/T14991.hs
@@ -1,5 +1,6 @@
 {-# LANGUAGE TypeFamilies #-}
-{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE UndecidableInstances #-}
 module T14991 where
diff --git a/testsuite/tests/dependent/should_compile/T9632.hs b/testsuite/tests/dependent/should_compile/T9632.hs
index bea468fff3..f2099aa22b 100644
--- a/testsuite/tests/dependent/should_compile/T9632.hs
+++ b/testsuite/tests/dependent/should_compile/T9632.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE DataKinds, PolyKinds #-}
 
 module T9632 where
 
diff --git a/testsuite/tests/dependent/should_compile/TypeLevelVec.hs b/testsuite/tests/dependent/should_compile/TypeLevelVec.hs
index 19f605c8cd..0e2f0c7744 100644
--- a/testsuite/tests/dependent/should_compile/TypeLevelVec.hs
+++ b/testsuite/tests/dependent/should_compile/TypeLevelVec.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE TypeInType, UnicodeSyntax, GADTs, NoImplicitPrelude,
+{-# LANGUAGE DataKinds, PolyKinds, UnicodeSyntax, GADTs, NoImplicitPrelude,
              TypeOperators, TypeFamilies #-}
 {-# OPTIONS_GHC -fno-warn-unticked-promoted-constructors #-}
 
diff --git a/testsuite/tests/dependent/should_compile/all.T b/testsuite/tests/dependent/should_compile/all.T
index e153cafe41..40ba2110f9 100644
--- a/testsuite/tests/dependent/should_compile/all.T
+++ b/testsuite/tests/dependent/should_compile/all.T
@@ -48,3 +48,4 @@ test('T14720', normal, compile, [''])
 test('T14066a', normal, compile, [''])
 test('T14749', normal, compile, [''])
 test('T14991', normal, compile, [''])
+test('DkNameRes', normal, compile, [''])
\ No newline at end of file
diff --git a/testsuite/tests/dependent/should_compile/dynamic-paper.hs b/testsuite/tests/dependent/should_compile/dynamic-paper.hs
index 1aa4ee54d9..2c284cfeea 100644
--- a/testsuite/tests/dependent/should_compile/dynamic-paper.hs
+++ b/testsuite/tests/dependent/should_compile/dynamic-paper.hs
@@ -7,7 +7,7 @@ Stephanie Weirich, Richard Eisenberg, and Dimitrios Vytiniotis, 2016. -}
 {-#  LANGUAGE RankNTypes, PolyKinds, TypeOperators,
              ScopedTypeVariables, GADTs, FlexibleInstances,
              UndecidableInstances, RebindableSyntax,
-             DataKinds, MagicHash, AutoDeriveTypeable, TypeInType  #-}
+             DataKinds, MagicHash, AutoDeriveTypeable #-}
 {-# OPTIONS_GHC -Wno-missing-methods -Wno-redundant-constraints #-}
 {-# OPTIONS_GHC -Wno-simplifiable-class-constraints #-}
   -- Because we define a local Typeable class and have
@@ -127,7 +127,7 @@ gcast x = do  Refl <- eqT  (typeRep :: TypeRep a)
                            (typeRep :: TypeRep b)
               return x
 
-data SameKind :: k -> k -> *
+data SameKind :: k -> k -> Type
 type CheckAppResult = SameKind AppResult AppResultNoKind
   --  not the most thorough check
 foo :: AppResult x -> AppResultNoKind x
@@ -170,17 +170,20 @@ dynFst :: Dynamic -> Maybe Dynamic
 dynFst (Dyn (rpab :: TypeRep pab) (x :: pab))
 
   = do  App (rpa  :: TypeRep pa ) (rb :: TypeRep b)  <- splitApp rpab
-            --  introduces kind |k2|, and types |pa :: k2 -> *|, |b :: k2|
+            --  introduces kind |k2|, and types |pa :: k2 -> Type|, |b :: k2|
 
         App (rp   :: TypeRep p  ) (ra :: TypeRep a)  <- splitApp rpa
-            --  introduces kind |k1|, and types |p :: k1 -> k2 -> *|, |a :: k1|
+            --  introduces kind |k1|, and types |p :: k1 -> k2 -> Type|,
+            --                                  |a :: k1|
 
         Refl       <- eqT rp (typeRep :: TypeRep (,))
-            --  introduces |p ~ (,)| and |(k1 -> k2 -> *) ~ (* -> * -> *)|
+            --  introduces |p ~ (,)| and
+            --             |(k1 -> k2 -> Type) ~ (Type -> Type -> Type)|
 
         return (Dyn ra (fst x))
 
-eqT :: forall k1 k2 (a :: k1) (b :: k2). TypeRep a -> TypeRep b -> Maybe (a :~: b)
+eqT :: forall k1 k2 (a :: k1) (b :: k2).
+       TypeRep a -> TypeRep b -> Maybe (a :~: b)
 
 data (a :: k1) :~: (b :: k2) where
   Refl :: forall k (a :: k). a :~: a
@@ -201,11 +204,13 @@ data SomeTypeRep where
 
 type TyMapLessTyped = Map SomeTypeRep Dynamic
 
-insertLessTyped    ::  forall a. Typeable a => a -> TyMapLessTyped -> TyMapLessTyped
-insertLessTyped x  =   Map.insert (SomeTypeRep (typeRep :: TypeRep a)) (toDynamic x)
+insertLessTyped :: forall a. Typeable a => a -> TyMapLessTyped -> TyMapLessTyped
+insertLessTyped x
+  = Map.insert (SomeTypeRep (typeRep :: TypeRep a)) (toDynamic x)
 
-lookupLessTyped  ::  forall a. Typeable a => TyMapLessTyped -> Maybe a
-lookupLessTyped  =   fromDynamic <=< Map.lookup (SomeTypeRep (typeRep :: TypeRep a))
+lookupLessTyped :: forall a. Typeable a => TyMapLessTyped -> Maybe a
+lookupLessTyped
+  = fromDynamic <=< Map.lookup (SomeTypeRep (typeRep :: TypeRep a))
 
 instance Ord SomeTypeRep where
   compare (SomeTypeRep tr1) (SomeTypeRep tr2) = compareTypeRep tr1 tr2
@@ -329,7 +334,7 @@ dynApplyOld (DynOld trf f) (DynOld trx x) =
 data DynamicClosed where
   DynClosed :: TypeRepClosed a -> a -> DynamicClosed
 
-data TypeRepClosed (a :: *) where
+data TypeRepClosed (a :: Type) where
   TBool  :: TypeRepClosed Bool
   TFun   :: TypeRepClosed a -> TypeRepClosed b -> TypeRepClosed (a -> b)
   TProd  :: TypeRepClosed a -> TypeRepClosed b -> TypeRepClosed (a, b)
diff --git a/testsuite/tests/dependent/should_compile/mkGADTVars.hs b/testsuite/tests/dependent/should_compile/mkGADTVars.hs
index 1e74c6980a..9b48e8c395 100644
--- a/testsuite/tests/dependent/should_compile/mkGADTVars.hs
+++ b/testsuite/tests/dependent/should_compile/mkGADTVars.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE GADTs, TypeInType #-}
+{-# LANGUAGE GADTs, PolyKinds #-}
 
 module GADTVars where
 
diff --git a/testsuite/tests/dependent/should_fail/BadTelescope.hs b/testsuite/tests/dependent/should_fail/BadTelescope.hs
index acabffec54..11b52f36e2 100644
--- a/testsuite/tests/dependent/should_fail/BadTelescope.hs
+++ b/testsuite/tests/dependent/should_fail/BadTelescope.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE DataKinds, PolyKinds #-}
 
 module BadTelescope where
 
diff --git a/testsuite/tests/dependent/should_fail/BadTelescope2.hs b/testsuite/tests/dependent/should_fail/BadTelescope2.hs
index 6237df4488..b12adbd8e3 100644
--- a/testsuite/tests/dependent/should_fail/BadTelescope2.hs
+++ b/testsuite/tests/dependent/should_fail/BadTelescope2.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE TypeInType, ExplicitForAll #-}
+{-# LANGUAGE DataKinds, PolyKinds, ExplicitForAll #-}
 
 module BadTelescope2 where
 
diff --git a/testsuite/tests/dependent/should_fail/BadTelescope3.hs b/testsuite/tests/dependent/should_fail/BadTelescope3.hs
index 807479f634..470f5fb9fe 100644
--- a/testsuite/tests/dependent/should_fail/BadTelescope3.hs
+++ b/testsuite/tests/dependent/should_fail/BadTelescope3.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE TypeInType, ExplicitForAll #-}
+{-# LANGUAGE PolyKinds, ExplicitForAll #-}
 
 module BadTelescope3 where
 
diff --git a/testsuite/tests/dependent/should_fail/BadTelescope4.hs b/testsuite/tests/dependent/should_fail/BadTelescope4.hs
index 566922a4a0..bdaf674c2f 100644
--- a/testsuite/tests/dependent/should_fail/BadTelescope4.hs
+++ b/testsuite/tests/dependent/should_fail/BadTelescope4.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE ExistentialQuantification, TypeInType #-}
+{-# LANGUAGE ExistentialQuantification, DataKinds, PolyKinds #-}
 module BadTelescope4 where
 
 import Data.Proxy
diff --git a/testsuite/tests/dependent/should_fail/DepFail1.hs b/testsuite/tests/dependent/should_fail/DepFail1.hs
index 425a8159c4..26e5d46832 100644
--- a/testsuite/tests/dependent/should_fail/DepFail1.hs
+++ b/testsuite/tests/dependent/should_fail/DepFail1.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE PolyKinds #-}
 
 module DepFail1 where
 
diff --git a/testsuite/tests/dependent/should_fail/InferDependency.hs b/testsuite/tests/dependent/should_fail/InferDependency.hs
index 47957d47d6..c2bec19d44 100644
--- a/testsuite/tests/dependent/should_fail/InferDependency.hs
+++ b/testsuite/tests/dependent/should_fail/InferDependency.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE PolyKinds #-}
 
 module InferDependency where
 
diff --git a/testsuite/tests/dependent/should_fail/KindLevelsB.hs b/testsuite/tests/dependent/should_fail/KindLevelsB.hs
deleted file mode 100644
index 80762978b2..0000000000
--- a/testsuite/tests/dependent/should_fail/KindLevelsB.hs
+++ /dev/null
@@ -1,9 +0,0 @@
-{-# LANGUAGE DataKinds, PolyKinds #-}
-
-module KindLevels where
-
-data A
-data B :: A -> *
-data C :: B a -> *
-data D :: C b -> *
-data E :: D c -> *
diff --git a/testsuite/tests/dependent/should_fail/KindLevelsB.stderr b/testsuite/tests/dependent/should_fail/KindLevelsB.stderr
deleted file mode 100644
index 587eb97bfa..0000000000
--- a/testsuite/tests/dependent/should_fail/KindLevelsB.stderr
+++ /dev/null
@@ -1,5 +0,0 @@
-
-KindLevelsB.hs:7:13: error:
-    • Expected kind ‘A’, but ‘a’ has kind ‘*’
-    • In the first argument of ‘B’, namely ‘a’
-      In the kind ‘B a -> *’
diff --git a/testsuite/tests/dependent/should_fail/PromotedClass.hs b/testsuite/tests/dependent/should_fail/PromotedClass.hs
index 6c3f415e5d..53d581015d 100644
--- a/testsuite/tests/dependent/should_fail/PromotedClass.hs
+++ b/testsuite/tests/dependent/should_fail/PromotedClass.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE TypeInType, GADTs #-}
+{-# LANGUAGE DataKinds, GADTs #-}
 
 module PromotedClass where
 
diff --git a/testsuite/tests/dependent/should_fail/RAE_T32a.hs b/testsuite/tests/dependent/should_fail/RAE_T32a.hs
index 08a4ad78a8..d71b863f02 100644
--- a/testsuite/tests/dependent/should_fail/RAE_T32a.hs
+++ b/testsuite/tests/dependent/should_fail/RAE_T32a.hs
@@ -1,34 +1,36 @@
 {-# LANGUAGE TemplateHaskell, RankNTypes, TypeOperators, DataKinds,
-             PolyKinds, TypeFamilies, GADTs, TypeInType #-}
+             PolyKinds, TypeFamilies, GADTs #-}
 
 module RAE_T32a where
 
 import Data.Kind
 
-data family Sing (k :: *) :: k -> *
+data family Sing (k :: Type) :: k -> Type
 
-data TyArr' (a :: *) (b :: *) :: *
-type TyArr (a :: *) (b :: *) = TyArr' a b -> *
+data TyArr' (a :: Type) (b :: Type) :: Type
+type TyArr (a :: Type) (b :: Type) = TyArr' a b -> Type
 type family (a :: TyArr k1 k2) @@ (b :: k1) :: k2
-data TyPi' (a :: *) (b :: TyArr a *) :: *
-type TyPi (a :: *) (b :: TyArr a *) = TyPi' a b -> *
+data TyPi' (a :: Type) (b :: TyArr a Type) :: Type
+type TyPi (a :: Type) (b :: TyArr a Type) = TyPi' a b -> Type
 type family (a :: TyPi k1 k2) @@@ (b :: k1) :: k2 @@ b
 $(return [])
 
-data MkStar (p :: *) (x :: TyArr' p *)
-type instance MkStar p @@ x = *
+data MkStar (p :: Type) (x :: TyArr' p Type)
+type instance MkStar p @@ x = Type
 $(return [])
 
-data Sigma (p :: *) (r :: TyPi p (MkStar p)) :: * where
+data Sigma (p :: Type) (r :: TyPi p (MkStar p)) :: Type where
   Sigma ::
-    forall (p :: *) (r :: TyPi p (MkStar p)) (a :: p) (b :: r @@@ a).
-    Sing * p -> Sing (TyPi p (MkStar p)) r -> Sing p a -> Sing (r @@@ a) b -> Sigma p r
+    forall (p :: Type) (r :: TyPi p (MkStar p)) (a :: p) (b :: r @@@ a).
+    Sing Type p -> Sing (TyPi p (MkStar p)) r -> Sing p a ->
+    Sing (r @@@ a) b -> Sigma p r
 $(return [])
 
 data instance Sing Sigma (Sigma p r) x where
   SSigma ::
-    forall (p :: *) (r :: TyPi p (MkStar p)) (a :: p) (b :: r @@@ a)
-    (sp :: Sing * p) (sr :: Sing (TyPi p (MkStar p)) r) (sa :: Sing p a) (sb :: Sing (r @@@ a) b).
+    forall (p :: Type) (r :: TyPi p (MkStar p)) (a :: p) (b :: r @@@ a)
+           (sp :: Sing Type p) (sr :: Sing (TyPi p (MkStar p)) r)
+           (sa :: Sing p a) (sb :: Sing (r @@@ a) b).
     Sing (Sing (r @@@ a) b) sb ->
     Sing (Sigma p r) ('Sigma sp sr sa sb)
 
diff --git a/testsuite/tests/dependent/should_fail/RAE_T32a.stderr b/testsuite/tests/dependent/should_fail/RAE_T32a.stderr
index 046a1e1aa4..41f5d7cd4c 100644
--- a/testsuite/tests/dependent/should_fail/RAE_T32a.stderr
+++ b/testsuite/tests/dependent/should_fail/RAE_T32a.stderr
@@ -1,10 +1,10 @@
 
-RAE_T32a.hs:28:1: error:
+RAE_T32a.hs:29:1: error:
     • Expected kind ‘k0 -> *’,
         but ‘Sing Sigma (Sigma p r)’ has kind ‘*’
     • In the data instance declaration for ‘Sing’
 
-RAE_T32a.hs:28:20: error:
+RAE_T32a.hs:29:20: error:
     • Expecting two more arguments to ‘Sigma’
       Expected a type, but
       ‘Sigma’ has kind
@@ -12,7 +12,7 @@ RAE_T32a.hs:28:20: error:
     • In the first argument of ‘Sing’, namely ‘Sigma’
       In the data instance declaration for ‘Sing’
 
-RAE_T32a.hs:28:27: error:
+RAE_T32a.hs:29:27: error:
     • Expected kind ‘Sigma’, but ‘Sigma p r’ has kind ‘*’
     • In the second argument of ‘Sing’, namely ‘(Sigma p r)’
       In the data instance declaration for ‘Sing’
diff --git a/testsuite/tests/dependent/should_fail/RenamingStar.hs b/testsuite/tests/dependent/should_fail/RenamingStar.hs
index 255021c8d9..f9344b0fd9 100644
--- a/testsuite/tests/dependent/should_fail/RenamingStar.hs
+++ b/testsuite/tests/dependent/should_fail/RenamingStar.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE KindSignatures, NoStarIsType #-}
 
 module RenamingStar where
 
diff --git a/testsuite/tests/dependent/should_fail/RenamingStar.stderr b/testsuite/tests/dependent/should_fail/RenamingStar.stderr
index 5efda699fd..4001811f1f 100644
--- a/testsuite/tests/dependent/should_fail/RenamingStar.stderr
+++ b/testsuite/tests/dependent/should_fail/RenamingStar.stderr
@@ -1,11 +1,5 @@
 
-RenamingStar.hs:5:13: error:
-    Not in scope: type constructor or class ‘*’
-    NB: With TypeInType, you must import * from Data.Kind
-
-RenamingStar.hs:5:13: error:
-    Illegal operator ‘*’ in type ‘*’
-      Use TypeOperators to allow operators in types
-
 RenamingStar.hs:5:13: error:
     Operator applied to too few arguments: *
+    With NoStarIsType, ‘*’ is treated as a regular type operator. 
+    Did you mean to use ‘Type’ from Data.Kind instead?
diff --git a/testsuite/tests/dependent/should_fail/SelfDep.hs b/testsuite/tests/dependent/should_fail/SelfDep.hs
index f54b92752b..22ac9ede98 100644
--- a/testsuite/tests/dependent/should_fail/SelfDep.hs
+++ b/testsuite/tests/dependent/should_fail/SelfDep.hs
@@ -1,3 +1,5 @@
+{-# LANGUAGE KindSignatures #-}
+
 module SelfDep where
 
 data T :: T -> *
diff --git a/testsuite/tests/dependent/should_fail/SelfDep.stderr b/testsuite/tests/dependent/should_fail/SelfDep.stderr
index f4014f7277..8ac4be8c0c 100644
--- a/testsuite/tests/dependent/should_fail/SelfDep.stderr
+++ b/testsuite/tests/dependent/should_fail/SelfDep.stderr
@@ -1,5 +1,5 @@
 
-SelfDep.hs:3:11: error:
-    Type constructor ‘T’ cannot be used here
-      (it is defined and used in the same recursive group)
-    In the kind ‘T -> *’
+SelfDep.hs:5:11: error:
+    • Type constructor ‘T’ cannot be used here
+        (it is defined and used in the same recursive group)
+    • In the kind ‘T -> *’
diff --git a/testsuite/tests/dependent/should_fail/T11407.hs b/testsuite/tests/dependent/should_fail/T11407.hs
index 533870f94b..e94eaba1e7 100644
--- a/testsuite/tests/dependent/should_fail/T11407.hs
+++ b/testsuite/tests/dependent/should_fail/T11407.hs
@@ -1,5 +1,5 @@
 {-# LANGUAGE TypeFamilies #-}
-{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE DataKinds, PolyKinds #-}
 module T11407 where
 
 import Data.Kind
diff --git a/testsuite/tests/dependent/should_fail/T11473.hs b/testsuite/tests/dependent/should_fail/T11473.hs
index 12d95caac6..ebfeeb8a13 100644
--- a/testsuite/tests/dependent/should_fail/T11473.hs
+++ b/testsuite/tests/dependent/should_fail/T11473.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE PolyKinds, TypeFamilies, MagicHash, DataKinds, TypeInType, RankNTypes #-}
+{-# LANGUAGE PolyKinds, TypeFamilies, MagicHash, DataKinds, RankNTypes #-}
 
 module T11473 where
 
diff --git a/testsuite/tests/dependent/should_fail/T12081.hs b/testsuite/tests/dependent/should_fail/T12081.hs
index f68de420cb..0bf03b1950 100644
--- a/testsuite/tests/dependent/should_fail/T12081.hs
+++ b/testsuite/tests/dependent/should_fail/T12081.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE DataKinds, PolyKinds #-}
 
 module T12081 where
 
diff --git a/testsuite/tests/dependent/should_fail/T12174.hs b/testsuite/tests/dependent/should_fail/T12174.hs
index 29064d6a96..800759d690 100644
--- a/testsuite/tests/dependent/should_fail/T12174.hs
+++ b/testsuite/tests/dependent/should_fail/T12174.hs
@@ -1,7 +1,7 @@
 {-# LANGUAGE DataKinds #-}
+{-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE ExistentialQuantification #-}
 {-# LANGUAGE KindSignatures #-}
-{-# LANGUAGE TypeInType #-}
 module T12174 where
 
 data V a
diff --git a/testsuite/tests/dependent/should_fail/T13135.hs b/testsuite/tests/dependent/should_fail/T13135.hs
index 772ac78bfa..8f78ccbfb1 100644
--- a/testsuite/tests/dependent/should_fail/T13135.hs
+++ b/testsuite/tests/dependent/should_fail/T13135.hs
@@ -8,11 +8,11 @@
 {-# LANGUAGE UndecidableInstances #-}
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE PolyKinds #-}
-{-# LANGUAGE TypeInType #-}
 {-# LANGUAGE TypeFamilyDependencies #-}
 
 
-module T12135 where
+
+module T13135 where
 
 
 import Data.Kind (Type)
diff --git a/testsuite/tests/dependent/should_fail/T13601.hs b/testsuite/tests/dependent/should_fail/T13601.hs
index 5e98c7a657..a8fa34d4a0 100644
--- a/testsuite/tests/dependent/should_fail/T13601.hs
+++ b/testsuite/tests/dependent/should_fail/T13601.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE TypeFamilies, DataKinds, TypeInType #-}
+{-# LANGUAGE TypeFamilies, DataKinds, PolyKinds #-}
 
 import GHC.Exts
 import Prelude (Bool(True,False),Integer,Ordering,undefined)
diff --git a/testsuite/tests/dependent/should_fail/T13780a.hs b/testsuite/tests/dependent/should_fail/T13780a.hs
index 1f7c95c40a..b7e1510672 100644
--- a/testsuite/tests/dependent/should_fail/T13780a.hs
+++ b/testsuite/tests/dependent/should_fail/T13780a.hs
@@ -1,6 +1,6 @@
 {-# LANGUAGE ExistentialQuantification #-}
 {-# LANGUAGE TypeFamilies #-}
-{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE DataKinds, PolyKinds #-}
 module T13780a where
 
 data family Sing (a :: k)
diff --git a/testsuite/tests/dependent/should_fail/T13780b.hs b/testsuite/tests/dependent/should_fail/T13780b.hs
index 238e7a1af9..dc6ac89c08 100644
--- a/testsuite/tests/dependent/should_fail/T13780b.hs
+++ b/testsuite/tests/dependent/should_fail/T13780b.hs
@@ -1,6 +1,7 @@
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE TypeFamilies #-}
-{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE PolyKinds #-}
 module T13780b where
 
 data family Sing (a :: k)
diff --git a/testsuite/tests/dependent/should_fail/T13780c.hs b/testsuite/tests/dependent/should_fail/T13780c.hs
index eee6436237..78e09f5ef1 100644
--- a/testsuite/tests/dependent/should_fail/T13780c.hs
+++ b/testsuite/tests/dependent/should_fail/T13780c.hs
@@ -1,6 +1,6 @@
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE TypeFamilies #-}
-{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE DataKinds, PolyKinds #-}
 module T13780c where
 
 import Data.Kind
diff --git a/testsuite/tests/dependent/should_fail/T13780c.stderr b/testsuite/tests/dependent/should_fail/T13780c.stderr
index 065c700dfc..9a196f4bd7 100644
--- a/testsuite/tests/dependent/should_fail/T13780c.stderr
+++ b/testsuite/tests/dependent/should_fail/T13780c.stderr
@@ -2,11 +2,13 @@
 [2 of 2] Compiling T13780c          ( T13780c.hs, T13780c.o )
 
 T13780c.hs:11:16: error:
-    • Expected kind ‘Sing _1’, but ‘SFalse’ has kind ‘Sing 'False’
+    • Data constructor ‘SFalse’ cannot be used here
+        (it comes from a data family instance)
     • In the third argument of ‘ElimBool’, namely ‘SFalse’
       In the type family declaration for ‘ElimBool’
 
 T13780c.hs:12:16: error:
-    • Expected kind ‘Sing _1’, but ‘STrue’ has kind ‘Sing 'True’
+    • Data constructor ‘STrue’ cannot be used here
+        (it comes from a data family instance)
     • In the third argument of ‘ElimBool’, namely ‘STrue’
       In the type family declaration for ‘ElimBool’
diff --git a/testsuite/tests/dependent/should_fail/T14066.hs b/testsuite/tests/dependent/should_fail/T14066.hs
index 58396df591..709d507a34 100644
--- a/testsuite/tests/dependent/should_fail/T14066.hs
+++ b/testsuite/tests/dependent/should_fail/T14066.hs
@@ -1,7 +1,7 @@
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE PolyKinds #-}
-{-# LANGUAGE TypeInType #-}
-{-# LANGUAGE KindSignatures #-}
+
+
 
 module T14066 where
 
diff --git a/testsuite/tests/dependent/should_fail/T14066c.hs b/testsuite/tests/dependent/should_fail/T14066c.hs
index b4597d2cec..4dd6f41973 100644
--- a/testsuite/tests/dependent/should_fail/T14066c.hs
+++ b/testsuite/tests/dependent/should_fail/T14066c.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE TypeFamilies, TypeInType, UndecidableInstances #-}
+{-# LANGUAGE TypeFamilies, DataKinds, PolyKinds, UndecidableInstances #-}
 
 module T14066c where
 
diff --git a/testsuite/tests/dependent/should_fail/T14066d.hs b/testsuite/tests/dependent/should_fail/T14066d.hs
index ea47644688..dd5676826d 100644
--- a/testsuite/tests/dependent/should_fail/T14066d.hs
+++ b/testsuite/tests/dependent/should_fail/T14066d.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE RankNTypes, ScopedTypeVariables, TypeInType #-}
+{-# LANGUAGE RankNTypes, ScopedTypeVariables, PolyKinds #-}
 
 module T14066d where
 
diff --git a/testsuite/tests/dependent/should_fail/T14066e.hs b/testsuite/tests/dependent/should_fail/T14066e.hs
index 9b799e542c..9bce332527 100644
--- a/testsuite/tests/dependent/should_fail/T14066e.hs
+++ b/testsuite/tests/dependent/should_fail/T14066e.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE MonoLocalBinds, TypeInType, ScopedTypeVariables #-}
+{-# LANGUAGE MonoLocalBinds, PolyKinds, ScopedTypeVariables #-}
 
 module T14066e where
 
diff --git a/testsuite/tests/dependent/should_fail/T14066f.hs b/testsuite/tests/dependent/should_fail/T14066f.hs
index ccb7ceac0e..b2035f2c3d 100644
--- a/testsuite/tests/dependent/should_fail/T14066f.hs
+++ b/testsuite/tests/dependent/should_fail/T14066f.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE PolyKinds #-}
 
 module T14066f where
 
diff --git a/testsuite/tests/dependent/should_fail/T14066g.hs b/testsuite/tests/dependent/should_fail/T14066g.hs
index df0e03b173..b07a2c36a9 100644
--- a/testsuite/tests/dependent/should_fail/T14066g.hs
+++ b/testsuite/tests/dependent/should_fail/T14066g.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE DataKinds, PolyKinds #-}
 
 module T14066g where
 
diff --git a/testsuite/tests/dependent/should_fail/T14066h.hs b/testsuite/tests/dependent/should_fail/T14066h.hs
index 7e7ecd31c9..a20ae30958 100644
--- a/testsuite/tests/dependent/should_fail/T14066h.hs
+++ b/testsuite/tests/dependent/should_fail/T14066h.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE ScopedTypeVariables, TypeInType, MonoLocalBinds #-}
+{-# LANGUAGE ScopedTypeVariables, PolyKinds, MonoLocalBinds #-}
 
 module T14066h where
 
diff --git a/testsuite/tests/dependent/should_fail/T15245.hs b/testsuite/tests/dependent/should_fail/T15245.hs
new file mode 100644
index 0000000000..86d9c221e0
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T15245.hs
@@ -0,0 +1,10 @@
+{-# LANGUAGE TypeFamilies, DataKinds, PolyKinds, TypeApplications #-}
+
+module T15245 where
+
+import Type.Reflection
+
+data family K
+data instance K = MkK
+
+main = print (typeRep @'MkK)
diff --git a/testsuite/tests/dependent/should_fail/T15245.stderr b/testsuite/tests/dependent/should_fail/T15245.stderr
new file mode 100644
index 0000000000..b41076636f
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T15245.stderr
@@ -0,0 +1,7 @@
+
+T15245.hs:10:24: error:
+    • Data constructor ‘MkK’ cannot be used here
+        (it comes from a data family instance)
+    • In the type ‘ 'MkK’
+      In the first argument of ‘print’, namely ‘(typeRep @ 'MkK)’
+      In the expression: print (typeRep @ 'MkK)
diff --git a/testsuite/tests/dependent/should_fail/TypeSkolEscape.hs b/testsuite/tests/dependent/should_fail/TypeSkolEscape.hs
index 02b7737499..1f958de426 100644
--- a/testsuite/tests/dependent/should_fail/TypeSkolEscape.hs
+++ b/testsuite/tests/dependent/should_fail/TypeSkolEscape.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE RankNTypes, PolyKinds, TypeInType #-}
+{-# LANGUAGE RankNTypes, PolyKinds #-}
 -- NB: -fprint-explicit-runtime-reps enabled in all.T
 
 module TypeSkolEscape where
diff --git a/testsuite/tests/dependent/should_fail/all.T b/testsuite/tests/dependent/should_fail/all.T
index 7273445548..5ae037dc54 100644
--- a/testsuite/tests/dependent/should_fail/all.T
+++ b/testsuite/tests/dependent/should_fail/all.T
@@ -10,7 +10,6 @@ test('BadTelescope4', normal, compile_fail, [''])
 test('RenamingStar', normal, compile_fail, [''])
 test('T11407', normal, compile_fail, [''])
 test('T11334b', normal, compile_fail, [''])
-test('KindLevelsB', normal, compile_fail, [''])
 test('T11473', normal, compile_fail, [''])
 test('T11471', normal, compile_fail, [''])
 test('T12174', normal, compile_fail, [''])
@@ -28,3 +27,4 @@ test('T14066f', normal, compile_fail, [''])
 test('T14066g', normal, compile_fail, [''])
 test('T14066h', normal, compile_fail, [''])
 test('InferDependency', normal, compile_fail, [''])
+test('T15245', normal, compile_fail, [''])
diff --git a/testsuite/tests/dependent/should_run/T11964a.hs b/testsuite/tests/dependent/should_run/T11964a.hs
index f0576542b6..2c6993fef0 100644
--- a/testsuite/tests/dependent/should_run/T11964a.hs
+++ b/testsuite/tests/dependent/should_run/T11964a.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE PolyKinds #-}
 module T11964a where
 import Data.Kind
 type Star = Type
-- 
cgit v1.2.1


From 2f6069ccf21d7be0e09016896238f417d2492ffa Mon Sep 17 00:00:00 2001
From: Simon Peyton Jones <simonpj@microsoft.com>
Date: Fri, 15 Jun 2018 09:46:30 +0100
Subject: Make better "fake tycons" in error recovery

Consider (Trac #15215)
  data T a = MkT ...
  data S a = ...T...MkT....

If there is an error in the definition of 'T' we add a
"fake type constructor" to the type environment, so that we
can continue to typecheck 'S'.  But we /were not/ adding
a fake anything for 'MkT' and so there was an internal
error when we met 'MkT' in the body of 'S'.

The fix is to add fake tycons for all the 'implicits' of 'T'.
This is done by mk_fake_tc in TcTyClsDecls.checkValidTyCl,
which now returns a /list/ of TyCons rather than just one.

On the way I did some refactoring:

* Rename TcTyDecls.tcAddImplicits to tcAddTyConsToGblEnv
  and make it /include/ the TyCons themeselves as well
  as their implicits

* Some incidental refactoring about tcRecSelBinds. The main
  thing is that I've avoided creating a HsValBinds that we
  immediately decompose.  That meant moving some deck chairs
  around.

NB: The new error message for the regression test T15215
has the opaque error "Illegal constraint in a type:", flagged
in Trac #14845.  But that's the fault of the latter ticket.
The fix here not to blame.
---
 testsuite/tests/dependent/should_fail/T15215.hs     | 12 ++++++++++++
 testsuite/tests/dependent/should_fail/T15215.stderr | 12 ++++++++++++
 testsuite/tests/dependent/should_fail/all.T         |  1 +
 3 files changed, 25 insertions(+)
 create mode 100644 testsuite/tests/dependent/should_fail/T15215.hs
 create mode 100644 testsuite/tests/dependent/should_fail/T15215.stderr

(limited to 'testsuite/tests/dependent')

diff --git a/testsuite/tests/dependent/should_fail/T15215.hs b/testsuite/tests/dependent/should_fail/T15215.hs
new file mode 100644
index 0000000000..96fe04385b
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T15215.hs
@@ -0,0 +1,12 @@
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeInType #-}
+module T15215 where
+
+import Data.Kind
+
+data A :: Type -> Type where
+  MkA :: Show (Maybe a) => A a
+
+data SA :: forall a. A a -> Type where
+  SMkA :: SA MkA
diff --git a/testsuite/tests/dependent/should_fail/T15215.stderr b/testsuite/tests/dependent/should_fail/T15215.stderr
new file mode 100644
index 0000000000..80181b44bd
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T15215.stderr
@@ -0,0 +1,12 @@
+
+T15215.hs:9:3: error:
+    • Non type-variable argument in the constraint: Show (Maybe a)
+      (Use FlexibleContexts to permit this)
+    • In the definition of data constructor ‘MkA’
+      In the data type declaration for ‘A’
+
+T15215.hs:12:14: error:
+    • Illegal constraint in a type: Show (Maybe a0)
+    • In the first argument of ‘SA’, namely ‘MkA’
+      In the type ‘SA MkA’
+      In the definition of data constructor ‘SMkA’
diff --git a/testsuite/tests/dependent/should_fail/all.T b/testsuite/tests/dependent/should_fail/all.T
index 5ae037dc54..8e5185f1ae 100644
--- a/testsuite/tests/dependent/should_fail/all.T
+++ b/testsuite/tests/dependent/should_fail/all.T
@@ -28,3 +28,4 @@ test('T14066g', normal, compile_fail, [''])
 test('T14066h', normal, compile_fail, [''])
 test('InferDependency', normal, compile_fail, [''])
 test('T15245', normal, compile_fail, [''])
+test('T15215', normal, compile_fail, [''])
-- 
cgit v1.2.1


From 8df24474d0194d28b8273c1539af05793156e23f Mon Sep 17 00:00:00 2001
From: Vladislav Zavialov <vlad.z.4096@gmail.com>
Date: Sat, 16 Jun 2018 23:44:39 -0400
Subject: Warn about implicit kind variables with -Wcompat

According to an accepted proposal
https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/002
4-no-kind-vars.rst

    With -Wcompat, warn if a kind variable is brought into scope
    implicitly in a type with an explicit forall. This applies to type
    signatures and to other contexts that allow a forall with the
    forall-or-nothing rule in effect (for example, class instances).

Test Plan: Validate

Reviewers: goldfire, hvr, bgamari, RyanGlScott

Reviewed By: goldfire

Subscribers: RyanGlScott, rwbarton, thomie, carter

GHC Trac Issues: #15264

Differential Revision: https://phabricator.haskell.org/D4834
---
 testsuite/tests/dependent/should_compile/T15264.hs     | 15 +++++++++++++++
 testsuite/tests/dependent/should_compile/T15264.stderr | 10 ++++++++++
 testsuite/tests/dependent/should_compile/all.T         |  1 +
 3 files changed, 26 insertions(+)
 create mode 100644 testsuite/tests/dependent/should_compile/T15264.hs
 create mode 100644 testsuite/tests/dependent/should_compile/T15264.stderr

(limited to 'testsuite/tests/dependent')

diff --git a/testsuite/tests/dependent/should_compile/T15264.hs b/testsuite/tests/dependent/should_compile/T15264.hs
new file mode 100644
index 0000000000..a03cf4346e
--- /dev/null
+++ b/testsuite/tests/dependent/should_compile/T15264.hs
@@ -0,0 +1,15 @@
+{-# LANGUAGE ExplicitForAll, PolyKinds #-}
+{-# OPTIONS -Wcompat #-}
+
+module T15264 where
+
+import Data.Proxy
+
+bad1 :: forall (a :: k). Proxy a -> ()
+bad1 _ = ()
+
+bad2 :: forall (a :: k1) (b :: k2). Proxy a -> ()
+bad2 _ = ()
+
+good :: forall k (a :: k). Proxy a -> ()
+good _ = ()
diff --git a/testsuite/tests/dependent/should_compile/T15264.stderr b/testsuite/tests/dependent/should_compile/T15264.stderr
new file mode 100644
index 0000000000..222d686513
--- /dev/null
+++ b/testsuite/tests/dependent/should_compile/T15264.stderr
@@ -0,0 +1,10 @@
+
+T15264.hs:8:22: warning: [-Wimplicit-kind-vars (in -Wcompat)]
+    An explicit ‘forall’ was used, but the following kind variables are not quantified: ‘k’
+    Despite this fact, GHC will introduce them into scope, but it will stop doing so in the future.
+    Suggested fix: add ‘forall k.’
+
+T15264.hs:11:22: warning: [-Wimplicit-kind-vars (in -Wcompat)]
+    An explicit ‘forall’ was used, but the following kind variables are not quantified: ‘k1’, ‘k2’
+    Despite this fact, GHC will introduce them into scope, but it will stop doing so in the future.
+    Suggested fix: add ‘forall k1 k2.’
diff --git a/testsuite/tests/dependent/should_compile/all.T b/testsuite/tests/dependent/should_compile/all.T
index 40ba2110f9..2865351ff5 100644
--- a/testsuite/tests/dependent/should_compile/all.T
+++ b/testsuite/tests/dependent/should_compile/all.T
@@ -48,4 +48,5 @@ test('T14720', normal, compile, [''])
 test('T14066a', normal, compile, [''])
 test('T14749', normal, compile, [''])
 test('T14991', normal, compile, [''])
+test('T15264', normal, compile, [''])
 test('DkNameRes', normal, compile, [''])
\ No newline at end of file
-- 
cgit v1.2.1


From c63754118cf6c3d0947d0c611f1db39c78acf1b7 Mon Sep 17 00:00:00 2001
From: Ryan Scott <ryan.gl.scott@gmail.com>
Date: Sun, 17 Jun 2018 12:28:23 -0400
Subject: Provide a better error message for unpromotable data constructor
 contexts

Trac #14845 brought to light a corner case where a data
constructor could not be promoted (even with `-XTypeInType`) due to
an unpromotable constraint in its context. However, the error message
was less than helpful, so this patch adds an additional check to
`tcTyVar` catch unpromotable data constructors like these //before//
they're promoted, and to give a sensible error message in such cases.

Test Plan: make test TEST="T13895 T14845"

Reviewers: simonpj, goldfire, bgamari

Reviewed By: bgamari

Subscribers: rwbarton, thomie, carter

GHC Trac Issues: #13895, #14845

Differential Revision: https://phabricator.haskell.org/D4728
---
 .../tests/dependent/should_compile/T14845_compile.hs | 16 ++++++++++++++++
 testsuite/tests/dependent/should_compile/all.T       |  3 ++-
 .../tests/dependent/should_fail/PromotedClass.stderr |  3 ++-
 testsuite/tests/dependent/should_fail/T13895.hs      | 15 +++++++++++++++
 testsuite/tests/dependent/should_fail/T13895.stderr  | 20 ++++++++++++++++++++
 testsuite/tests/dependent/should_fail/T14845.stderr  |  7 +++++++
 .../tests/dependent/should_fail/T14845_fail1.hs      | 10 ++++++++++
 .../tests/dependent/should_fail/T14845_fail1.stderr  |  7 +++++++
 .../tests/dependent/should_fail/T14845_fail2.hs      | 14 ++++++++++++++
 .../tests/dependent/should_fail/T14845_fail2.stderr  |  7 +++++++
 testsuite/tests/dependent/should_fail/T15215.stderr  |  2 +-
 testsuite/tests/dependent/should_fail/all.T          |  3 +++
 12 files changed, 104 insertions(+), 3 deletions(-)
 create mode 100644 testsuite/tests/dependent/should_compile/T14845_compile.hs
 create mode 100644 testsuite/tests/dependent/should_fail/T13895.hs
 create mode 100644 testsuite/tests/dependent/should_fail/T13895.stderr
 create mode 100644 testsuite/tests/dependent/should_fail/T14845.stderr
 create mode 100644 testsuite/tests/dependent/should_fail/T14845_fail1.hs
 create mode 100644 testsuite/tests/dependent/should_fail/T14845_fail1.stderr
 create mode 100644 testsuite/tests/dependent/should_fail/T14845_fail2.hs
 create mode 100644 testsuite/tests/dependent/should_fail/T14845_fail2.stderr

(limited to 'testsuite/tests/dependent')

diff --git a/testsuite/tests/dependent/should_compile/T14845_compile.hs b/testsuite/tests/dependent/should_compile/T14845_compile.hs
new file mode 100644
index 0000000000..04f50189b8
--- /dev/null
+++ b/testsuite/tests/dependent/should_compile/T14845_compile.hs
@@ -0,0 +1,16 @@
+{-# Language PolyKinds, DataKinds, KindSignatures, GADTs, TypeInType, ConstraintKinds #-}
+{-# Language FlexibleContexts #-}
+{-# Language RankNTypes #-}
+{-# Language TypeOperators #-}
+module T14845 where
+
+import Data.Kind
+import Data.Type.Equality
+
+data A :: Type -> Type where
+  MkA1 :: a ~  Int => A a
+  MkA2 :: a ~~ Int => A a
+
+data SA :: forall a. A a -> Type where
+  SMkA1 :: SA MkA1
+  SMkA2 :: SA MkA2
diff --git a/testsuite/tests/dependent/should_compile/all.T b/testsuite/tests/dependent/should_compile/all.T
index 2865351ff5..64782c0276 100644
--- a/testsuite/tests/dependent/should_compile/all.T
+++ b/testsuite/tests/dependent/should_compile/all.T
@@ -47,6 +47,7 @@ test('T14556', normal, compile, [''])
 test('T14720', normal, compile, [''])
 test('T14066a', normal, compile, [''])
 test('T14749', normal, compile, [''])
+test('T14845_compile', normal, compile, [''])
 test('T14991', normal, compile, [''])
 test('T15264', normal, compile, [''])
-test('DkNameRes', normal, compile, [''])
\ No newline at end of file
+test('DkNameRes', normal, compile, [''])
diff --git a/testsuite/tests/dependent/should_fail/PromotedClass.stderr b/testsuite/tests/dependent/should_fail/PromotedClass.stderr
index f0683309bc..4da1a32fca 100644
--- a/testsuite/tests/dependent/should_fail/PromotedClass.stderr
+++ b/testsuite/tests/dependent/should_fail/PromotedClass.stderr
@@ -1,5 +1,6 @@
 
 PromotedClass.hs:10:15: error:
-    • Illegal constraint in a type: Show a0
+    • Data constructor ‘MkX’ cannot be used here
+        (it has an unpromotable context ‘Show a’)
     • In the first argument of ‘Proxy’, namely ‘( 'MkX  'True)’
       In the type signature: foo :: Proxy ( 'MkX  'True)
diff --git a/testsuite/tests/dependent/should_fail/T13895.hs b/testsuite/tests/dependent/should_fail/T13895.hs
new file mode 100644
index 0000000000..5897cd8149
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T13895.hs
@@ -0,0 +1,15 @@
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeInType #-}
+module T13895 where
+
+import Data.Data (Data, Typeable)
+import Data.Kind
+
+dataCast1 :: forall (a :: Type).
+             Data a
+          => forall (c :: Type -> Type)
+                    (t :: forall (k :: Type). Typeable k => k -> Type).
+             Typeable t
+          => (forall d. Data d => c (t d))
+          -> Maybe (c a)
+dataCast1 _ = undefined
diff --git a/testsuite/tests/dependent/should_fail/T13895.stderr b/testsuite/tests/dependent/should_fail/T13895.stderr
new file mode 100644
index 0000000000..0ae1710bf0
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T13895.stderr
@@ -0,0 +1,20 @@
+
+T13895.hs:12:23: error:
+    • Illegal constraint in a kind: Typeable k0
+    • In the first argument of ‘Typeable’, namely ‘t’
+      In the type signature:
+        dataCast1 :: forall (a :: Type).
+                     Data a =>
+                     forall (c :: Type -> Type)
+                            (t :: forall (k :: Type). Typeable k => k -> Type).
+                     Typeable t => (forall d. Data d => c (t d)) -> Maybe (c a)
+
+T13895.hs:13:38: error:
+    • Illegal constraint in a kind: Typeable k0
+    • In the first argument of ‘c’, namely ‘(t d)’
+      In the type signature:
+        dataCast1 :: forall (a :: Type).
+                     Data a =>
+                     forall (c :: Type -> Type)
+                            (t :: forall (k :: Type). Typeable k => k -> Type).
+                     Typeable t => (forall d. Data d => c (t d)) -> Maybe (c a)
diff --git a/testsuite/tests/dependent/should_fail/T14845.stderr b/testsuite/tests/dependent/should_fail/T14845.stderr
new file mode 100644
index 0000000000..3c11d15195
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T14845.stderr
@@ -0,0 +1,7 @@
+
+T14845.hs:19:16: error:
+    • Data constructor ‘MkA3’ cannot be used here
+        (it has an unpromotable context ‘Coercible a Int’)
+    • In the first argument of ‘SA’, namely ‘(MkA3 :: A Int)’
+      In the type ‘SA (MkA3 :: A Int)’
+      In the definition of data constructor ‘SMkA3’
diff --git a/testsuite/tests/dependent/should_fail/T14845_fail1.hs b/testsuite/tests/dependent/should_fail/T14845_fail1.hs
new file mode 100644
index 0000000000..46c1351027
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T14845_fail1.hs
@@ -0,0 +1,10 @@
+{-# Language PolyKinds, DataKinds, KindSignatures, GADTs, TypeInType, ConstraintKinds #-}
+module T14845_fail1 where
+
+import Data.Kind
+
+data Struct :: (k -> Constraint) -> (k -> Type) where
+  S :: cls a => Struct cls a
+
+data Foo a where
+  F :: Foo (S::Struct Eq a)
diff --git a/testsuite/tests/dependent/should_fail/T14845_fail1.stderr b/testsuite/tests/dependent/should_fail/T14845_fail1.stderr
new file mode 100644
index 0000000000..c1f1c8605d
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T14845_fail1.stderr
@@ -0,0 +1,7 @@
+
+T14845_fail1.hs:10:13: error:
+    • Data constructor ‘S’ cannot be used here
+        (it has an unpromotable context ‘cls a’)
+    • In the first argument of ‘Foo’, namely ‘(S :: Struct Eq a)’
+      In the type ‘Foo (S :: Struct Eq a)’
+      In the definition of data constructor ‘F’
diff --git a/testsuite/tests/dependent/should_fail/T14845_fail2.hs b/testsuite/tests/dependent/should_fail/T14845_fail2.hs
new file mode 100644
index 0000000000..4c5dac730f
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T14845_fail2.hs
@@ -0,0 +1,14 @@
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeInType #-}
+module T14845_fail2 where
+
+import Data.Coerce
+import Data.Kind
+
+data A :: Type -> Type where
+  MkA :: Coercible a Int => A a
+
+data SA :: forall a. A a -> Type where
+  SMkA :: SA MkA
diff --git a/testsuite/tests/dependent/should_fail/T14845_fail2.stderr b/testsuite/tests/dependent/should_fail/T14845_fail2.stderr
new file mode 100644
index 0000000000..9fe733f374
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T14845_fail2.stderr
@@ -0,0 +1,7 @@
+
+T14845_fail2.hs:14:14: error:
+    • Data constructor ‘MkA’ cannot be used here
+        (it has an unpromotable context ‘Coercible a Int’)
+    • In the first argument of ‘SA’, namely ‘MkA’
+      In the type ‘SA MkA’
+      In the definition of data constructor ‘SMkA’
diff --git a/testsuite/tests/dependent/should_fail/T15215.stderr b/testsuite/tests/dependent/should_fail/T15215.stderr
index 80181b44bd..53aff765a3 100644
--- a/testsuite/tests/dependent/should_fail/T15215.stderr
+++ b/testsuite/tests/dependent/should_fail/T15215.stderr
@@ -6,7 +6,7 @@ T15215.hs:9:3: error:
       In the data type declaration for ‘A’
 
 T15215.hs:12:14: error:
-    • Illegal constraint in a type: Show (Maybe a0)
+    • Illegal constraint in a kind: Show (Maybe a0)
     • In the first argument of ‘SA’, namely ‘MkA’
       In the type ‘SA MkA’
       In the definition of data constructor ‘SMkA’
diff --git a/testsuite/tests/dependent/should_fail/all.T b/testsuite/tests/dependent/should_fail/all.T
index 8e5185f1ae..2bfc39a6b8 100644
--- a/testsuite/tests/dependent/should_fail/all.T
+++ b/testsuite/tests/dependent/should_fail/all.T
@@ -19,6 +19,7 @@ test('T13601', normal, compile_fail, [''])
 test('T13780a', normal, compile_fail, [''])
 test('T13780c', [extra_files(['T13780b.hs'])],
                 multimod_compile_fail, ['T13780c', ''])
+test('T13895', normal, compile_fail, [''])
 test('T14066', normal, compile_fail, [''])
 test('T14066c', normal, compile_fail, [''])
 test('T14066d', normal, compile_fail, [''])
@@ -26,6 +27,8 @@ test('T14066e', normal, compile_fail, [''])
 test('T14066f', normal, compile_fail, [''])
 test('T14066g', normal, compile_fail, [''])
 test('T14066h', normal, compile_fail, [''])
+test('T14845_fail1', normal, compile_fail, [''])
+test('T14845_fail2', normal, compile_fail, [''])
 test('InferDependency', normal, compile_fail, [''])
 test('T15245', normal, compile_fail, [''])
 test('T15215', normal, compile_fail, [''])
-- 
cgit v1.2.1


From 50d7b2ac2fcfe954455f0bc9081e1dd3a2eef51d Mon Sep 17 00:00:00 2001
From: Ryan Scott <ryan.gl.scott@gmail.com>
Date: Sun, 17 Jun 2018 15:31:14 -0400
Subject: Remove accidentally checked-in T14845.stderr

This was a stderr file for a WIP test in D4728. I ended up removing
the test, but forgot to remove the stderr file.
---
 testsuite/tests/dependent/should_fail/T14845.stderr | 7 -------
 1 file changed, 7 deletions(-)
 delete mode 100644 testsuite/tests/dependent/should_fail/T14845.stderr

(limited to 'testsuite/tests/dependent')

diff --git a/testsuite/tests/dependent/should_fail/T14845.stderr b/testsuite/tests/dependent/should_fail/T14845.stderr
deleted file mode 100644
index 3c11d15195..0000000000
--- a/testsuite/tests/dependent/should_fail/T14845.stderr
+++ /dev/null
@@ -1,7 +0,0 @@
-
-T14845.hs:19:16: error:
-    • Data constructor ‘MkA3’ cannot be used here
-        (it has an unpromotable context ‘Coercible a Int’)
-    • In the first argument of ‘SA’, namely ‘(MkA3 :: A Int)’
-      In the type ‘SA (MkA3 :: A Int)’
-      In the definition of data constructor ‘SMkA3’
-- 
cgit v1.2.1


From 93b7ac8d73885369f61f6eb6147352d45de4e957 Mon Sep 17 00:00:00 2001
From: Ryan Scott <ryan.gl.scott@gmail.com>
Date: Thu, 5 Jul 2018 08:30:02 -0400
Subject: Fix #15308 by suppressing invisble args more rigorously

Summary:
There was a buglet in `stripInvisArgs` (which is part of the
pretty-printing pipeline for types) in which only invisble arguments
which came before any visible arguments would be suppressed, but any
invisble arguments that came //after// visible ones would still be
printed, even if `-fprint-explicit-kinds`  wasn't enabled.
The fix is simple: make `stripInvisArgs` recursively process the
remaining types even after a visible argument is encountered.

Test Plan: make test TEST=T15308

Reviewers: goldfire, bgamari

Reviewed By: bgamari

Subscribers: simonpj, rwbarton, thomie, carter

GHC Trac Issues: #15308

Differential Revision: https://phabricator.haskell.org/D4891
---
 testsuite/tests/dependent/should_fail/T15308.hs     | 12 ++++++++++++
 testsuite/tests/dependent/should_fail/T15308.stderr |  5 +++++
 testsuite/tests/dependent/should_fail/all.T         |  1 +
 3 files changed, 18 insertions(+)
 create mode 100644 testsuite/tests/dependent/should_fail/T15308.hs
 create mode 100644 testsuite/tests/dependent/should_fail/T15308.stderr

(limited to 'testsuite/tests/dependent')

diff --git a/testsuite/tests/dependent/should_fail/T15308.hs b/testsuite/tests/dependent/should_fail/T15308.hs
new file mode 100644
index 0000000000..b49fe1f75b
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T15308.hs
@@ -0,0 +1,12 @@
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeInType #-}
+module T15308 where
+
+import Data.Kind
+
+data Foo (a :: Type) :: forall b. (a -> b -> Type) -> Type where
+  MkFoo :: Foo a f
+
+f :: Foo a f -> String
+f = show
diff --git a/testsuite/tests/dependent/should_fail/T15308.stderr b/testsuite/tests/dependent/should_fail/T15308.stderr
new file mode 100644
index 0000000000..a4bdbd5ab6
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T15308.stderr
@@ -0,0 +1,5 @@
+
+T15308.hs:12:5: error:
+    • No instance for (Show (Foo a f)) arising from a use of ‘show’
+    • In the expression: show
+      In an equation for ‘f’: f = show
diff --git a/testsuite/tests/dependent/should_fail/all.T b/testsuite/tests/dependent/should_fail/all.T
index 2bfc39a6b8..1bc3f42a92 100644
--- a/testsuite/tests/dependent/should_fail/all.T
+++ b/testsuite/tests/dependent/should_fail/all.T
@@ -32,3 +32,4 @@ test('T14845_fail2', normal, compile_fail, [''])
 test('InferDependency', normal, compile_fail, [''])
 test('T15245', normal, compile_fail, [''])
 test('T15215', normal, compile_fail, [''])
+test('T15308', normal, compile_fail, ['-fno-print-explicit-kinds'])
-- 
cgit v1.2.1


From f59332f92b30306675da22150de092eeebbf55f3 Mon Sep 17 00:00:00 2001
From: Krzysztof Gogolewski <krz.gogolewski@gmail.com>
Date: Fri, 6 Jul 2018 10:59:43 -0400
Subject: Mark AutoDeriveTypeable as deprecated

Test Plan: validate

Reviewers: bgamari, alpmestan

Reviewed By: alpmestan

Subscribers: rwbarton, thomie, carter

GHC Trac Issues: #15342

Differential Revision: https://phabricator.haskell.org/D4933
---
 testsuite/tests/dependent/should_compile/dynamic-paper.hs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'testsuite/tests/dependent')

diff --git a/testsuite/tests/dependent/should_compile/dynamic-paper.hs b/testsuite/tests/dependent/should_compile/dynamic-paper.hs
index 2c284cfeea..c998f0967c 100644
--- a/testsuite/tests/dependent/should_compile/dynamic-paper.hs
+++ b/testsuite/tests/dependent/should_compile/dynamic-paper.hs
@@ -7,7 +7,7 @@ Stephanie Weirich, Richard Eisenberg, and Dimitrios Vytiniotis, 2016. -}
 {-#  LANGUAGE RankNTypes, PolyKinds, TypeOperators,
              ScopedTypeVariables, GADTs, FlexibleInstances,
              UndecidableInstances, RebindableSyntax,
-             DataKinds, MagicHash, AutoDeriveTypeable #-}
+             DataKinds, MagicHash #-}
 {-# OPTIONS_GHC -Wno-missing-methods -Wno-redundant-constraints #-}
 {-# OPTIONS_GHC -Wno-simplifiable-class-constraints #-}
   -- Because we define a local Typeable class and have
-- 
cgit v1.2.1


From aedbf7f1c402ecbcb5ff192d5fb4dd6dd4771bf8 Mon Sep 17 00:00:00 2001
From: Simon Peyton Jones <simonpj@microsoft.com>
Date: Mon, 9 Jul 2018 17:20:06 +0100
Subject: Fix decompsePiCos and visible type application

Trac #15343 was caused by two things

First, in TcHsType.tcHsTypeApp, which deals with the type argment
in visible type application, we were failing to call
solveLocalEqualities. But the type argument is like a user type
signature so it's at least inconsitent not to do so.

I thought that would nail it.  But it didn't. It turned out that we
were ended up calling decomposePiCos on a type looking like this
    (f |> co) Int

where co :: (forall a. ty) ~ (t1 -> t2)

Now, 'co' is insoluble, and we'll report that later.  But meanwhile
we don't want to crash in decomposePiCos.

My fix involves keeping track of the type on both sides of the
coercion, and ensuring that the outer shape matches before
decomposing.  I wish there was a simpler way to do this. But
I think this one is at least robust.

I suppose it is possible that the decomposePiCos fix would
have cured the original report, but I'm leaving the one-line
tcHsTypeApp fix in too because it just seems more consistent.
---
 testsuite/tests/dependent/should_fail/T15343.hs     | 14 ++++++++++++++
 testsuite/tests/dependent/should_fail/T15343.stderr |  7 +++++++
 testsuite/tests/dependent/should_fail/all.T         |  2 ++
 3 files changed, 23 insertions(+)
 create mode 100644 testsuite/tests/dependent/should_fail/T15343.hs
 create mode 100644 testsuite/tests/dependent/should_fail/T15343.stderr

(limited to 'testsuite/tests/dependent')

diff --git a/testsuite/tests/dependent/should_fail/T15343.hs b/testsuite/tests/dependent/should_fail/T15343.hs
new file mode 100644
index 0000000000..9bb59c807a
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T15343.hs
@@ -0,0 +1,14 @@
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeInType #-}
+module T15343 where
+
+import Data.Kind
+
+elimSing :: forall (p :: forall z. z). p
+elimSing = undefined
+
+data WhySym :: Type -> Type
+
+hsym = elimSing @WhySym
diff --git a/testsuite/tests/dependent/should_fail/T15343.stderr b/testsuite/tests/dependent/should_fail/T15343.stderr
new file mode 100644
index 0000000000..79d81e5772
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T15343.stderr
@@ -0,0 +1,7 @@
+
+T15343.hs:14:18: error:
+    • Expecting one more argument to ‘WhySym’
+      Expected kind ‘forall z. z’, but ‘WhySym’ has kind ‘* -> *’
+    • In the type ‘WhySym’
+      In the expression: elimSing @WhySym
+      In an equation for ‘hsym’: hsym = elimSing @WhySym
diff --git a/testsuite/tests/dependent/should_fail/all.T b/testsuite/tests/dependent/should_fail/all.T
index 1bc3f42a92..59d80375ff 100644
--- a/testsuite/tests/dependent/should_fail/all.T
+++ b/testsuite/tests/dependent/should_fail/all.T
@@ -33,3 +33,5 @@ test('InferDependency', normal, compile_fail, [''])
 test('T15245', normal, compile_fail, [''])
 test('T15215', normal, compile_fail, [''])
 test('T15308', normal, compile_fail, ['-fno-print-explicit-kinds'])
+test('T15343', normal, compile_fail, [''])
+
-- 
cgit v1.2.1


From 65c186f0fdde95fd7c63ab9bd9b33a0213dba7d1 Mon Sep 17 00:00:00 2001
From: Vladislav Zavialov <vlad.z.4096@gmail.com>
Date: Mon, 16 Jul 2018 18:46:52 -0400
Subject: Do not imply NoStarIsType by TypeOperators/TypeInType

Implementation of the "Embrace TypeInType" proposal was done according
to the spec, which specified that TypeOperators must imply NoStarIsType.
This implication was meant to prevent breakage and to be removed in 2
releases.  However, compiling head.hackage has shown that this
implication only magnified the breakage, so there is no reason to have
it in the first place.

To remain in compliance with the three-release policy, we add a
workaround to define the (*) type operator even when -XStarIsType is on.

Test Plan: ./validate

Reviewers: bgamari, RyanGlScott, goldfire, phadej, hvr

Reviewed By: bgamari, RyanGlScott

Subscribers: harpocrates, rwbarton, thomie, carter

Differential Revision: https://phabricator.haskell.org/D4865
---
 testsuite/tests/dependent/ghci/T14238.stdout | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'testsuite/tests/dependent')

diff --git a/testsuite/tests/dependent/ghci/T14238.stdout b/testsuite/tests/dependent/ghci/T14238.stdout
index 729f821af7..fddbc0de54 100644
--- a/testsuite/tests/dependent/ghci/T14238.stdout
+++ b/testsuite/tests/dependent/ghci/T14238.stdout
@@ -1 +1 @@
-Foo :: forall k -> k -> Type
+Foo :: forall k -> k -> *
-- 
cgit v1.2.1


From af624071fa063158d6e963e171280676f9c0a0b0 Mon Sep 17 00:00:00 2001
From: Richard Eisenberg <rae@cs.brynmawr.edu>
Date: Thu, 19 Jul 2018 00:16:13 -0400
Subject: Fix some casts.

This fixes #15346, and is a team effort between Ryan Scott and
myself (mostly Ryan). We discovered two errors related to FC's
"push" rules, one in the TPush rule (as implemented in pushCoTyArg)
and one in KPush rule (it shows up in liftCoSubstVarBndr).

The solution: do what the paper says, instead of whatever random
thoughts popped into my head as I was actually implementing.

Also fixes #15419, which is actually the same underlying problem.

Test case: dependent/should_compile/T{15346,15419}.
---
 testsuite/tests/dependent/should_compile/T15346.hs | 31 ++++++++++++
 testsuite/tests/dependent/should_compile/T15419.hs | 55 ++++++++++++++++++++++
 testsuite/tests/dependent/should_compile/all.T     |  2 +
 3 files changed, 88 insertions(+)
 create mode 100644 testsuite/tests/dependent/should_compile/T15346.hs
 create mode 100644 testsuite/tests/dependent/should_compile/T15419.hs

(limited to 'testsuite/tests/dependent')

diff --git a/testsuite/tests/dependent/should_compile/T15346.hs b/testsuite/tests/dependent/should_compile/T15346.hs
new file mode 100644
index 0000000000..3d8d49b9d2
--- /dev/null
+++ b/testsuite/tests/dependent/should_compile/T15346.hs
@@ -0,0 +1,31 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE TypeApplications #-}
+module T15346 where
+
+import Data.Kind
+import Data.Proxy
+
+-----
+
+type family Rep (a :: Type) :: Type
+type instance Rep () = ()
+
+type family PFrom (x :: a) :: Rep a
+
+-----
+
+class SDecide k where
+  test :: forall (a :: k). Proxy a
+
+instance SDecide () where
+  test = undefined
+
+test1 :: forall (a :: k). SDecide (Rep k) => Proxy a
+test1 = seq (test @_ @(PFrom a)) Proxy
+
+test2 :: forall (a :: ()). Proxy a
+test2 = test1
diff --git a/testsuite/tests/dependent/should_compile/T15419.hs b/testsuite/tests/dependent/should_compile/T15419.hs
new file mode 100644
index 0000000000..68f20e5604
--- /dev/null
+++ b/testsuite/tests/dependent/should_compile/T15419.hs
@@ -0,0 +1,55 @@
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE UndecidableInstances #-}
+module T15419 where
+
+import Data.Kind
+
+data Prod a b
+data Proxy p = Proxy
+
+-----
+
+data family Sing :: forall k. k -> Type
+data instance Sing x = STuple
+
+-----
+
+type family Rep1 (f :: k -> Type) :: k -> Type
+type instance Rep1 ((,) a) = Prod a
+
+type family From1 (f :: Type -> Type) a (z :: f a) :: Rep1 f a
+type family To1 (f :: Type -> Type) a (z :: Rep1 f a) :: f a
+
+class Generic1 (f :: Type -> Type) where
+  sFrom1 :: forall (a :: Type) (z :: f a).      Proxy z -> Sing (From1 f a z)
+  sTo1   :: forall (a :: Type) (r :: Rep1 f a). Proxy r -> Proxy (To1 f a r :: f a)
+
+instance Generic1 ((,) a) where
+  sFrom1 Proxy = undefined
+  sTo1   Proxy = undefined
+
+-----
+
+type family Fmap (g :: b) (x :: f a) :: f b
+type instance Fmap (g :: b) (x :: (u, a)) = To1 ((,) u) b (Fmap g (From1 ((,) u) a x))
+
+class PFunctor (f :: Type -> Type) where
+  sFmap         :: forall a b (g :: b) (x :: f a).
+                   Proxy g -> Sing x -> Proxy (Fmap g x)
+
+instance PFunctor (Prod a) where
+  sFmap _ STuple = undefined
+
+sFmap1 :: forall (f :: Type -> Type) (u :: Type) (b :: Type) (g :: b) (x :: f u).
+                 (Generic1 f,
+                  PFunctor (Rep1 f),
+                  Fmap g x ~ To1 f b (Fmap g (From1 f u x)) )
+              => Proxy g -> Proxy x -> Proxy (Fmap g x)
+sFmap1 sg sx = sTo1 (sFmap sg (sFrom1 sx))
+
+sFmap2  :: forall (p :: Type) (a :: Type) (b :: Type) (g :: b) (x :: (p, a)).
+          Proxy g -> Proxy x -> Proxy (Fmap g x)
+sFmap2 = sFmap1
diff --git a/testsuite/tests/dependent/should_compile/all.T b/testsuite/tests/dependent/should_compile/all.T
index 64782c0276..4e096c1f71 100644
--- a/testsuite/tests/dependent/should_compile/all.T
+++ b/testsuite/tests/dependent/should_compile/all.T
@@ -51,3 +51,5 @@ test('T14845_compile', normal, compile, [''])
 test('T14991', normal, compile, [''])
 test('T15264', normal, compile, [''])
 test('DkNameRes', normal, compile, [''])
+test('T15346', normal, compile, [''])
+test('T15419', normal, compile, [''])
-- 
cgit v1.2.1


From f8618a9b15177ee8c84771b927cb3583c9cd8408 Mon Sep 17 00:00:00 2001
From: Richard Eisenberg <rae@cs.brynmawr.edu>
Date: Tue, 17 Jul 2018 00:12:34 -0400
Subject: Remove the type-checking knot.

Bug #15380 hangs because a knot-tied TyCon ended up in a kind.
Looking at the code in tcInferApps, I'm amazed this hasn't happened
before! I couldn't think of a good way to fix it (with dependent
types, we can't really keep types out of kinds, after all), so
I just went ahead and removed the knot.

This was remarkably easy to do. In tcTyVar, when we find a TcTyCon,
just use it. (Previously, we looked up the knot-tied TyCon and used
that.) Then, during the final zonk, replace TcTyCons with the real,
full-blooded TyCons in the global environment. It's all very easy.

The new bit is explained in the existing
Note [Type checking recursive type and class declarations]
in TcTyClsDecls.

Naturally, I removed various references to the knot and the
zonkTcTypeInKnot (and related) functions. Now, we can print types
during type checking with abandon!

NB: There is a teensy error message regression with this patch,
around the ordering of quantified type variables. This ordering
problem is fixed (I believe) with the patch for #14880. The ordering
affects only internal variables that cannot be instantiated with
any kind of visible type application.

There is also a teensy regression around the printing of types
in TH splices. I think this is really a TH bug and will file
separately.

Test case: dependent/should_fail/T15380
---
 .../tests/dependent/should_compile/T14066a.stderr    |  2 +-
 testsuite/tests/dependent/should_fail/T15380.hs      | 20 ++++++++++++++++++++
 testsuite/tests/dependent/should_fail/T15380.stderr  |  6 ++++++
 testsuite/tests/dependent/should_fail/all.T          |  2 +-
 4 files changed, 28 insertions(+), 2 deletions(-)
 create mode 100644 testsuite/tests/dependent/should_fail/T15380.hs
 create mode 100644 testsuite/tests/dependent/should_fail/T15380.stderr

(limited to 'testsuite/tests/dependent')

diff --git a/testsuite/tests/dependent/should_compile/T14066a.stderr b/testsuite/tests/dependent/should_compile/T14066a.stderr
index 906695f3f7..610e434d6c 100644
--- a/testsuite/tests/dependent/should_compile/T14066a.stderr
+++ b/testsuite/tests/dependent/should_compile/T14066a.stderr
@@ -1,5 +1,5 @@
 
 T14066a.hs:13:3: warning:
     Type family instance equation is overlapped:
-      forall c d (x :: c) (y :: d).
+      forall d c (x :: c) (y :: d).
         Bar x y = Bool -- Defined at T14066a.hs:13:3
diff --git a/testsuite/tests/dependent/should_fail/T15380.hs b/testsuite/tests/dependent/should_fail/T15380.hs
new file mode 100644
index 0000000000..32ea8ec724
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T15380.hs
@@ -0,0 +1,20 @@
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE TypeOperators #-}
+
+module T15380 where
+
+import Data.Kind
+
+class Generic a where
+  type Rep a :: Type
+
+class PGeneric a where
+  type To a (x :: Rep a) :: a
+
+type family MDefault (x :: a) :: a where
+  MDefault x = To (M x)
+
+class C a where
+  type M (x :: a) :: a
+  type M (x :: a) = MDefault x
diff --git a/testsuite/tests/dependent/should_fail/T15380.stderr b/testsuite/tests/dependent/should_fail/T15380.stderr
new file mode 100644
index 0000000000..9b30078c64
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T15380.stderr
@@ -0,0 +1,6 @@
+
+T15380.hs:16:16: error:
+    • Expecting one more argument to ‘To (M x)’
+      Expected a type, but ‘To (M x)’ has kind ‘Rep (M x) -> M x’
+    • In the type ‘To (M x)’
+      In the type family declaration for ‘MDefault’
diff --git a/testsuite/tests/dependent/should_fail/all.T b/testsuite/tests/dependent/should_fail/all.T
index 59d80375ff..593b7787a1 100644
--- a/testsuite/tests/dependent/should_fail/all.T
+++ b/testsuite/tests/dependent/should_fail/all.T
@@ -34,4 +34,4 @@ test('T15245', normal, compile_fail, [''])
 test('T15215', normal, compile_fail, [''])
 test('T15308', normal, compile_fail, ['-fno-print-explicit-kinds'])
 test('T15343', normal, compile_fail, [''])
-
+test('T15380', normal, compile_fail, [''])
-- 
cgit v1.2.1


From c955a514f033a12f6d0ab0fbacec3e18a5757ab5 Mon Sep 17 00:00:00 2001
From: Richard Eisenberg <rae@cs.brynmawr.edu>
Date: Sat, 14 Jul 2018 16:02:13 -0400
Subject: Remove decideKindGeneralisationPlan

TypeInType came with a new function: decideKindGeneralisationPlan.
This type-level counterpart to the term-level decideGeneralisationPlan
chose whether or not a kind should be generalized. The thinking was
that if `let` should not be generalized, then kinds shouldn't either
(under the same circumstances around -XMonoLocalBinds).

However, this is too conservative -- the situation described in the
motivation for "let should be be generalized" does not occur in types.

This commit thus removes decideKindGeneralisationPlan, always
generalizing.

One consequence is that tc_hs_sig_type_and_gen no longer calls
solveEqualities, which reports all unsolved constraints, instead
relying on the solveLocalEqualities in tcImplicitTKBndrs. An effect
of this is that reporing kind errors gets delayed more frequently.
This seems to be a net benefit in error reporting; often, alongside
a kind error, the type error is now reported (and users might find
type errors easier to understand).

Some of these errors ended up at the top level, where it was
discovered that the GlobalRdrEnv containing the definitions in the
local module was not in the TcGblEnv, and thus errors were reported
with qualified names unnecessarily. This commit rejiggers some of
the logic around captureTopConstraints accordingly.

One error message (typecheck/should_fail/T1633)
is a regression, mentioning the name of a default method. However,
that problem is already reported as #10087, its solution is far from
clear, and so I'm not addressing it here.

This commit fixes #15141. As it's an internal refactor, there is
no concrete test case for it.

Along the way, we no longer need the hsib_closed field of
HsImplicitBndrs (it was used only in decideKindGeneralisationPlan)
and so it's been removed, simplifying the datatype structure.

Along the way, I removed code in the validity checker that looks
at coercions. This isn't related to this patch, really (though
it was, at one point), but it's an improvement, so I kept it.

This updates the haddock submodule.
---
 .../tests/dependent/should_compile/T14066h.hs      | 11 ++++++++++
 testsuite/tests/dependent/should_compile/all.T     |  1 +
 .../tests/dependent/should_fail/DepFail1.stderr    | 22 ++++++++++++++++----
 .../tests/dependent/should_fail/T13895.stderr      | 24 ++++++++++++++++++++++
 .../tests/dependent/should_fail/T14066.stderr      |  6 ++++--
 .../tests/dependent/should_fail/T14066e.stderr     | 11 +++++++++-
 testsuite/tests/dependent/should_fail/T14066h.hs   | 11 ----------
 .../tests/dependent/should_fail/T14066h.stderr     | 16 ---------------
 testsuite/tests/dependent/should_fail/all.T        |  1 -
 9 files changed, 68 insertions(+), 35 deletions(-)
 create mode 100644 testsuite/tests/dependent/should_compile/T14066h.hs
 delete mode 100644 testsuite/tests/dependent/should_fail/T14066h.hs
 delete mode 100644 testsuite/tests/dependent/should_fail/T14066h.stderr

(limited to 'testsuite/tests/dependent')

diff --git a/testsuite/tests/dependent/should_compile/T14066h.hs b/testsuite/tests/dependent/should_compile/T14066h.hs
new file mode 100644
index 0000000000..df3db1c15d
--- /dev/null
+++ b/testsuite/tests/dependent/should_compile/T14066h.hs
@@ -0,0 +1,11 @@
+{-# LANGUAGE ScopedTypeVariables, PolyKinds, MonoLocalBinds #-}
+
+module T14066h where
+
+import Data.Proxy
+
+f :: forall b. b -> (Proxy Int, Proxy Maybe)
+f x = (fst y :: Proxy Int, fst y :: Proxy Maybe)
+  where
+    y :: (Proxy a, b)  -- this generalizes over the kind of a
+    y = (Proxy, x)
diff --git a/testsuite/tests/dependent/should_compile/all.T b/testsuite/tests/dependent/should_compile/all.T
index 4e096c1f71..418fba2d85 100644
--- a/testsuite/tests/dependent/should_compile/all.T
+++ b/testsuite/tests/dependent/should_compile/all.T
@@ -53,3 +53,4 @@ test('T15264', normal, compile, [''])
 test('DkNameRes', normal, compile, [''])
 test('T15346', normal, compile, [''])
 test('T15419', normal, compile, [''])
+test('T14066h', normal, compile, [''])
diff --git a/testsuite/tests/dependent/should_fail/DepFail1.stderr b/testsuite/tests/dependent/should_fail/DepFail1.stderr
index 630f010fa3..a8e64d4e0c 100644
--- a/testsuite/tests/dependent/should_fail/DepFail1.stderr
+++ b/testsuite/tests/dependent/should_fail/DepFail1.stderr
@@ -2,11 +2,25 @@
 DepFail1.hs:7:6: error:
     • Expecting one more argument to ‘Proxy Bool’
       Expected a type, but ‘Proxy Bool’ has kind ‘Bool -> *’
-    • In the type signature:
-        z :: Proxy Bool
+    • In the type signature: z :: Proxy Bool
+
+DepFail1.hs:8:5: error:
+    • Couldn't match expected type ‘Proxy Bool’
+                  with actual type ‘Proxy k0 a1’
+    • In the expression: P
+      In an equation for ‘z’: z = P
 
 DepFail1.hs:10:16: error:
     • Expected kind ‘Int’, but ‘Bool’ has kind ‘*’
     • In the second argument of ‘Proxy’, namely ‘Bool’
-      In the type signature:
-        a :: Proxy Int Bool
+      In the type signature: a :: Proxy Int Bool
+
+DepFail1.hs:11:5: error:
+    • Couldn't match kind ‘*’ with ‘Int’
+      When matching types
+        a0 :: Int
+        Bool :: *
+      Expected type: Proxy Int Bool
+        Actual type: Proxy Int a0
+    • In the expression: P
+      In an equation for ‘a’: a = P
diff --git a/testsuite/tests/dependent/should_fail/T13895.stderr b/testsuite/tests/dependent/should_fail/T13895.stderr
index 0ae1710bf0..3e8bef6858 100644
--- a/testsuite/tests/dependent/should_fail/T13895.stderr
+++ b/testsuite/tests/dependent/should_fail/T13895.stderr
@@ -1,4 +1,28 @@
 
+T13895.hs:8:14: error:
+    • Could not deduce (Typeable (t dict0))
+      from the context: (Data a, Typeable (t dict))
+        bound by the type signature for:
+                   dataCast1 :: forall k (dict :: Typeable k) (dict1 :: Typeable
+                                                                          *) a (c :: *
+                                                                                     -> *) (t :: forall k1.
+                                                                                                 Typeable
+                                                                                                   k1 =>
+                                                                                                 k1
+                                                                                                 -> *).
+                                (Data a, Typeable (t dict)) =>
+                                (forall d. Data d => c (t dict1 d)) -> Maybe (c a)
+        at T13895.hs:(8,14)-(14,24)
+      The type variable ‘dict0’ is ambiguous
+    • In the ambiguity check for ‘dataCast1’
+      To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
+      In the type signature:
+        dataCast1 :: forall (a :: Type).
+                     Data a =>
+                     forall (c :: Type -> Type)
+                            (t :: forall (k :: Type). Typeable k => k -> Type).
+                     Typeable t => (forall d. Data d => c (t d)) -> Maybe (c a)
+
 T13895.hs:12:23: error:
     • Illegal constraint in a kind: Typeable k0
     • In the first argument of ‘Typeable’, namely ‘t’
diff --git a/testsuite/tests/dependent/should_fail/T14066.stderr b/testsuite/tests/dependent/should_fail/T14066.stderr
index cd0142f5c1..e5179e510b 100644
--- a/testsuite/tests/dependent/should_fail/T14066.stderr
+++ b/testsuite/tests/dependent/should_fail/T14066.stderr
@@ -1,6 +1,6 @@
 
 T14066.hs:15:59: error:
-    • Expected kind ‘k0’, but ‘b’ has kind ‘k’
+    • Expected kind ‘k’, but ‘b’ has kind ‘k1’
     • In the second argument of ‘SameKind’, namely ‘b’
       In the type signature: g :: forall k (b :: k). SameKind a b
       In the expression:
@@ -8,4 +8,6 @@ T14066.hs:15:59: error:
           g :: forall k (b :: k). SameKind a b
           g = undefined
         in ()
-    • Relevant bindings include x :: Proxy a (bound at T14066.hs:15:4)
+    • Relevant bindings include
+        x :: Proxy a (bound at T14066.hs:15:4)
+        f :: Proxy a -> () (bound at T14066.hs:15:1)
diff --git a/testsuite/tests/dependent/should_fail/T14066e.stderr b/testsuite/tests/dependent/should_fail/T14066e.stderr
index 504ca5a80e..193c74d193 100644
--- a/testsuite/tests/dependent/should_fail/T14066e.stderr
+++ b/testsuite/tests/dependent/should_fail/T14066e.stderr
@@ -1,6 +1,15 @@
 
 T14066e.hs:13:59: error:
-    • Expected kind ‘c’, but ‘b'’ has kind ‘k0’
+    • Couldn't match kind ‘k1’ with ‘*’
+      ‘k1’ is a rigid type variable bound by
+        the type signature for:
+          j :: forall k k1 (c :: k1) (b :: k).
+               Proxy a -> Proxy b -> Proxy c -> Proxy b
+        at T14066e.hs:12:5-61
+      When matching kinds
+        k :: *
+        c :: k1
+      Expected kind ‘c’, but ‘b'’ has kind ‘k’
     • In the first argument of ‘Proxy’, namely ‘(b' :: c')’
       In an expression type signature: Proxy (b' :: c')
       In the expression: (p1 :: Proxy (b' :: c'))
diff --git a/testsuite/tests/dependent/should_fail/T14066h.hs b/testsuite/tests/dependent/should_fail/T14066h.hs
deleted file mode 100644
index a20ae30958..0000000000
--- a/testsuite/tests/dependent/should_fail/T14066h.hs
+++ /dev/null
@@ -1,11 +0,0 @@
-{-# LANGUAGE ScopedTypeVariables, PolyKinds, MonoLocalBinds #-}
-
-module T14066h where
-
-import Data.Proxy
-
-f :: forall b. b -> (Proxy Int, Proxy Maybe)
-f x = (fst y :: Proxy Int, fst y :: Proxy Maybe)
-  where
-    y :: (Proxy a, b)  -- MonoLocalBinds means this won't generalize over the kind of a
-    y = (Proxy, x)
diff --git a/testsuite/tests/dependent/should_fail/T14066h.stderr b/testsuite/tests/dependent/should_fail/T14066h.stderr
deleted file mode 100644
index bfd33693b6..0000000000
--- a/testsuite/tests/dependent/should_fail/T14066h.stderr
+++ /dev/null
@@ -1,16 +0,0 @@
-
-T14066h.hs:8:28: error:
-    • Couldn't match kind ‘* -> *’ with ‘*’
-      When matching types
-        a0 :: *
-        Maybe :: * -> *
-      Expected type: Proxy Maybe
-        Actual type: Proxy a0
-    • In the expression: fst y :: Proxy Maybe
-      In the expression: (fst y :: Proxy Int, fst y :: Proxy Maybe)
-      In an equation for ‘f’:
-          f x
-            = (fst y :: Proxy Int, fst y :: Proxy Maybe)
-            where
-                y :: (Proxy a, b)
-                y = (Proxy, x)
diff --git a/testsuite/tests/dependent/should_fail/all.T b/testsuite/tests/dependent/should_fail/all.T
index 593b7787a1..0f7129020e 100644
--- a/testsuite/tests/dependent/should_fail/all.T
+++ b/testsuite/tests/dependent/should_fail/all.T
@@ -26,7 +26,6 @@ test('T14066d', normal, compile_fail, [''])
 test('T14066e', normal, compile_fail, [''])
 test('T14066f', normal, compile_fail, [''])
 test('T14066g', normal, compile_fail, [''])
-test('T14066h', normal, compile_fail, [''])
 test('T14845_fail1', normal, compile_fail, [''])
 test('T14845_fail2', normal, compile_fail, [''])
 test('InferDependency', normal, compile_fail, [''])
-- 
cgit v1.2.1


From a50244c6a87176a4df8d41e6a1a3f102ba129032 Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Thu, 16 Aug 2018 17:16:44 -0700
Subject: Rename SigTv to TyVarTv (#15480)

because since #15050, these are no longer used in pattern SIGnatures,
but still in other places where meta-variables should only be unified
with TYpe VARiables.

I also found mentions of `SigTv` in parts of the renamer and desugarer
that do not seem to directly relate to `SigTv` as used in the type
checker, but rather to uses of `forall a.` in type signatures. I renamed
these to `ScopedTv`.

Differential Revision: https://phabricator.haskell.org/D5074
---
 testsuite/tests/dependent/should_compile/T14066a.hs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'testsuite/tests/dependent')

diff --git a/testsuite/tests/dependent/should_compile/T14066a.hs b/testsuite/tests/dependent/should_compile/T14066a.hs
index 30b203d31b..1d6b72491e 100644
--- a/testsuite/tests/dependent/should_compile/T14066a.hs
+++ b/testsuite/tests/dependent/should_compile/T14066a.hs
@@ -10,7 +10,7 @@ import Data.Type.Bool
 
 type family Bar x y where
   Bar (x :: a) (y :: b) = Int
-  Bar (x :: c) (y :: d) = Bool   -- a,b,c,d should be SigTvs and unify appropriately
+  Bar (x :: c) (y :: d) = Bool   -- a,b,c,d should be TyVarTvs and unify appropriately
 
 
   -- the two k's, even though they have different scopes, should unify in the
-- 
cgit v1.2.1


From ff29fc84c03c800cfa04c2a00eb8edf6fa5f4183 Mon Sep 17 00:00:00 2001
From: Simon Peyton Jones <simonpj@microsoft.com>
Date: Fri, 24 Aug 2018 16:40:28 +0100
Subject: Better error reporting for inaccessible code

This patch fixes Trac #15558.  There turned out to be
two distinct problems

* In TcExpr.tc_poly_expr_nc we had

    tc_poly_expr_nc (L loc expr) res_ty
      = do { traceTc "tcPolyExprNC" (ppr res_ty)
           ; (wrap, expr')
               <- tcSkolemiseET GenSigCtxt res_ty $ \ res_ty ->
                  setSrcSpan loc $
                    -- NB: setSrcSpan *after* skolemising,
                    -- so we get better skolem locations
                  tcExpr expr res_ty

  Putting the setSrcSpan inside the tcSkolemise means that
  the location on the Implication constraint is the /call/
  to the function rather than the /argument/ to the call,
  and that is really quite wrong.

  I don't know what Richard's comment NB means -- I moved the
  setSrcSpan outside, and the "binding site" info in error
  messages actually improved.

  The reason I found this is that it affects the span reported
  for Trac #15558.

* In TcErrors.mkGivenErrorReporter we carefully munge the location
  for an insoluble Given constraint (Note [Inaccessible code]).
  But the 'implic' passed in wasn't necesarily the immediately-
  enclosing implication -- but for location-munging purposes
  it jolly well should be.

  Solution: use the innermost implication. This actually
  simplifies the code -- no need to pass an implication in to
  mkGivenErrorReporter.
---
 testsuite/tests/dependent/should_fail/T14066d.stderr | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'testsuite/tests/dependent')

diff --git a/testsuite/tests/dependent/should_fail/T14066d.stderr b/testsuite/tests/dependent/should_fail/T14066d.stderr
index 3f5eb9825a..8ece51029b 100644
--- a/testsuite/tests/dependent/should_fail/T14066d.stderr
+++ b/testsuite/tests/dependent/should_fail/T14066d.stderr
@@ -4,7 +4,7 @@ T14066d.hs:11:35: error:
       ‘b1’ is a rigid type variable bound by
         a type expected by the context:
           forall c b1 (a :: c). (Proxy a, Proxy c, b1)
-        at T14066d.hs:11:33-35
+        at T14066d.hs:11:35
       ‘b’ is a rigid type variable bound by
         the type signature for:
           f :: forall b. b -> (Proxy Maybe, ())
-- 
cgit v1.2.1