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/should_fail')

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 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/should_fail')

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/should_fail')

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 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.
---
 .../tests/dependent/should_fail/RAE_T32a.stderr    | 25 +++++++++++-----------
 testsuite/tests/dependent/should_fail/all.T        |  2 +-
 2 files changed, 13 insertions(+), 14 deletions(-)

(limited to 'testsuite/tests/dependent/should_fail')

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 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}
---
 .../tests/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 ++++++----
 testsuite/tests/dependent/should_fail/T13601.stderr |  3 +--
 .../tests/dependent/should_fail/T13780c.stderr      |  2 +-
 testsuite/tests/dependent/should_fail/T14066.hs     | 17 +++++++++++++++++
 testsuite/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 +++++++++--
 24 files changed, 193 insertions(+), 30 deletions(-)
 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/should_fail')

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 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/should_fail')

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 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
---
 .../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 +-
 36 files changed, 76 insertions(+), 72 deletions(-)
 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/should_fail')

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, [''])
-- 
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/should_fail')

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 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_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 +++
 10 files changed, 86 insertions(+), 2 deletions(-)
 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/should_fail')

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/should_fail')

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/should_fail')

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 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/should_fail')

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 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
---
 testsuite/tests/dependent/should_fail/T15380.hs     | 20 ++++++++++++++++++++
 testsuite/tests/dependent/should_fail/T15380.stderr |  6 ++++++
 testsuite/tests/dependent/should_fail/all.T         |  2 +-
 3 files changed, 27 insertions(+), 1 deletion(-)
 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/should_fail')

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_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 -
 7 files changed, 56 insertions(+), 35 deletions(-)
 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/should_fail')

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 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/should_fail')

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