Never Anyify during kind inference

See Note [Error on unconstrained meta-variables] in TcMType.

Close #17301
Close #17567
Close #17562
Close #15474

21 files changed, 166 insertions, 7 deletions

diff --git a/testsuite/tests/dependent/should_compile/dynamic-paper.hs b/testsuite/tests/dependent/should_compile/dynamic-paper.hs
index 1188bf17d4..6fae39f5a1 100644
--- a/testsuite/tests/dependent/should_compile/dynamic-paper.hs
+++ b/testsuite/tests/dependent/should_compile/dynamic-paper.hs
@@ -128,7 +128,7 @@ gcast x = do  Refl <- eqT  (typeRep :: TypeRep a)
               return x
 
 data SameKind :: k -> k -> Type
-type CheckAppResult = SameKind AppResult AppResultNoKind
+
   --  not the most thorough check
 foo :: AppResult x -> AppResultNoKind x
 foo (App y z) = AppNoKind y z
diff --git a/testsuite/tests/indexed-types/should_compile/T15852.stderr b/testsuite/tests/indexed-types/should_compile/T15852.stderr
index 8c212a06b6..eab430ac83 100644
--- a/testsuite/tests/indexed-types/should_compile/T15852.stderr
+++ b/testsuite/tests/indexed-types/should_compile/T15852.stderr
@@ -3,10 +3,10 @@ TYPE CONSTRUCTORS
     roles nominal nominal nominal
 COERCION AXIOMS
   axiom T15852.D:R:DFProxyProxy0 ::
-    forall k1 k2 (j :: k1) (c :: k2).
-      DF (Proxy c) = T15852.R:DFProxyProxy k1 k2 j c
+    forall k1 (j :: k1) k2 (c :: k2).
+      DF (Proxy c) = T15852.R:DFProxyProxy k1 j k2 c
 FAMILY INSTANCES
-  data instance forall {k1} {k2} {j :: k1} {c :: k2}.
+  data instance forall {k1} {j :: k1} {k2} {c :: k2}.
                   DF (Proxy c) -- Defined at T15852.hs:10:15
 Dependent modules: []
 Dependent packages: [base-4.16.0.0, ghc-bignum-1.0, ghc-prim-0.8.0]
diff --git a/testsuite/tests/indexed-types/should_fail/T17008a.stderr b/testsuite/tests/indexed-types/should_fail/T17008a.stderr
index 795506e3b3..86d13d9ba8 100644
--- a/testsuite/tests/indexed-types/should_fail/T17008a.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T17008a.stderr
@@ -1,7 +1,7 @@
 
 T17008a.hs:11:5: error:
-    • Type variable ‘a1’ is mentioned in the RHS,
+    • Type variable ‘a2’ is mentioned in the RHS,
         but not bound on the LHS of the family instance
-        The real LHS (expanding synonyms) is: F @a2 x
+        The real LHS (expanding synonyms) is: F @a1 x
     • In the equations for closed type family ‘F’
       In the type family declaration for ‘F’
diff --git a/testsuite/tests/polykinds/NestedProxies.hs b/testsuite/tests/polykinds/NestedProxies.hs
new file mode 100644
index 0000000000..d59d026544
--- /dev/null
+++ b/testsuite/tests/polykinds/NestedProxies.hs
@@ -0,0 +1,28 @@
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE StarIsType #-}
+{-# OPTIONS_GHC -Wno-star-is-type #-}
+-- NB: -XNoPolyKinds. All the variables in the Proxies should be defaulted to *.
+
+module NestedProxies where
+
+import Data.Proxy
+
+-- | 'F1' docs
+type family F1 a b :: * -> *
+-- | 'F2' docs
+type family F2 a b :: * -> * where
+  F2 Int b = Maybe
+  F2 a   b = []
+-- | 'D' docs
+data family D a :: * -> *
+
+v :: Int
+v = 42
+
+-- | 'C' docs
+class C a where
+  -- | 'AT' docs
+  type AT a
+  type AT a = Proxy (Proxy (Proxy (Proxy (Proxy (Proxy (Proxy (Proxy (Proxy (Proxy)))))))))
diff --git a/testsuite/tests/polykinds/T13393.hs b/testsuite/tests/polykinds/T13393.hs
index f1c4af3fa0..28cf87a6d5 100644
--- a/testsuite/tests/polykinds/T13393.hs
+++ b/testsuite/tests/polykinds/T13393.hs
@@ -28,7 +28,7 @@ newtype AacEncSt (rate :: Rate) channels (codec :: AacCodec) = MkAacEncSt
 
 -- makeLenses ''AacEncSt
 
-type Iso s t a b = forall p f. (Functor f) => (a -> f b) -> s -> (f t)
+type Iso s t a b = forall f. (Functor f) => (a -> f b) -> s -> (f t)
 instance (Monad m, Monoid w) => MonadState s (RWST r w s m) where
 
 iso :: (s -> a) -> (b -> t) -> Iso s t a b
diff --git a/testsuite/tests/polykinds/all.T b/testsuite/tests/polykinds/all.T
index 52529f882a..c82f275f65 100644
--- a/testsuite/tests/polykinds/all.T
+++ b/testsuite/tests/polykinds/all.T
@@ -228,6 +228,7 @@ test('T18300', normal, compile_fail, [''])
 test('T18451', normal, compile_fail, [''])
 test('T18451a', normal, compile_fail, [''])
 test('T18451b', normal, compile_fail, [''])
+test('NestedProxies', normal, compile, [''])
 test('T18522-ppr', normal, ghci_script, ['T18522-ppr.script'])
 test('T18855', normal, compile, [''])
 test('T19092', normal, compile, [''])
diff --git a/testsuite/tests/typecheck/should_compile/T17562b.hs b/testsuite/tests/typecheck/should_compile/T17562b.hs
new file mode 100644
index 0000000000..0d635d9248
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T17562b.hs
@@ -0,0 +1,6 @@
+{-# LANGUAGE QuantifiedConstraints, MultiParamTypeClasses, TypeFamilies #-}
+-- NB: No PolyKinds
+
+module T17562b where
+
+class (forall a. a b ~ a c) => C b c
diff --git a/testsuite/tests/typecheck/should_compile/T17567StupidThetaB.hs b/testsuite/tests/typecheck/should_compile/T17567StupidThetaB.hs
new file mode 100644
index 0000000000..36a4bca1e5
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T17567StupidThetaB.hs
@@ -0,0 +1,6 @@
+{-# LANGUAGE QuantifiedConstraints, DatatypeContexts, TypeFamilies #-}
+-- NB: -XNoPolyKinds, to get defaulting.
+
+module T17567StupidThetaB where
+
+data (forall a. a b ~ a c) => T b c
diff --git a/testsuite/tests/typecheck/should_compile/T17567StupidThetaB.stderr b/testsuite/tests/typecheck/should_compile/T17567StupidThetaB.stderr
new file mode 100644
index 0000000000..5e98268d8b
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T17567StupidThetaB.stderr
@@ -0,0 +1,3 @@
+
+T17567StupidThetaB.hs:1:37: warning:
+    -XDatatypeContexts is deprecated: It was widely considered a misfeature, and has been removed from the Haskell language.
diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T
index a461ed7257..396d7ce15a 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -730,6 +730,8 @@ test('T18831', normal, compile, [''])
 test('T18920', normal, compile, [''])
 test('T18939_Compile', normal, compile, [''])
 test('T15942', normal, compile, [''])
+test('T17562b', normal, compile, [''])
+test('T17567StupidThetaB', normal, compile, [''])
 test('ClassDefaultInHsBoot', [extra_files(['ClassDefaultInHsBootA1.hs','ClassDefaultInHsBootA2.hs','ClassDefaultInHsBootA2.hs-boot','ClassDefaultInHsBootA3.hs'])], multimod_compile, ['ClassDefaultInHsBoot', '-v0'])
 test('T17812', normal, compile, [''])
 test('T17186', normal, compile, [''])
diff --git a/testsuite/tests/typecheck/should_fail/T15474.hs b/testsuite/tests/typecheck/should_fail/T15474.hs
new file mode 100644
index 0000000000..2fb68e8020
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T15474.hs
@@ -0,0 +1,15 @@
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeInType #-}
+module T15474 where
+
+import Data.Kind (Type)
+
+data Proxy a
+
+type Forall = forall t. Proxy t
+
+f1 :: forall (t :: Type). Proxy t
+f1 = f1
+
+f2 :: Forall
+f2 = f1
diff --git a/testsuite/tests/typecheck/should_fail/T15474.stderr b/testsuite/tests/typecheck/should_fail/T15474.stderr
new file mode 100644
index 0000000000..7fd96ebaa1
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T15474.stderr
@@ -0,0 +1,5 @@
+
+T15474.hs:9:1: error:
+    • Uninferrable type variable k0 in
+      the type synonym right-hand side: forall (t :: k0). Proxy @{k0} t
+    • In the type declaration for ‘Forall’
diff --git a/testsuite/tests/typecheck/should_fail/T17301.hs b/testsuite/tests/typecheck/should_fail/T17301.hs
new file mode 100644
index 0000000000..2fdaace98b
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T17301.hs
@@ -0,0 +1,36 @@
+{-# LANGUAGE DataKinds            #-}
+{-# LANGUAGE GADTs                #-}
+{-# LANGUAGE PolyKinds            #-}
+{-# LANGUAGE TypeFamilies         #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+module T17301 where
+
+import GHC.TypeLits
+  ( TypeError, ErrorMessage(..) )
+
+data A = MkA
+data B (a :: A)
+
+data TySing ty where
+  SB :: TySing (B a)
+
+data ATySing where
+  MkATySing :: TySing ty -> ATySing
+
+type family Forget ty :: ATySing where
+  Forget (B a) = MkATySing SB
+
+type family Message ty where
+  Message (MkATySing (_ :: TySing ty)) =
+    TypeError ( ShowType ty )
+
+
+
+type KnownType = B MkA
+
+foo :: Message (Forget KnownType) => ()
+foo = ()
+
+bar :: ()
+bar = foo
diff --git a/testsuite/tests/typecheck/should_fail/T17301.stderr b/testsuite/tests/typecheck/should_fail/T17301.stderr
new file mode 100644
index 0000000000..7c7e20f005
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T17301.stderr
@@ -0,0 +1,5 @@
+
+T17301.hs:22:3: error:
+    • Uninferrable type variable (a0 :: A) in
+      type family equation right-hand side: 'MkATySing @(B a0) ('SB @a0)
+    • In the type family declaration for ‘Forget’
diff --git a/testsuite/tests/typecheck/should_fail/T17562.hs b/testsuite/tests/typecheck/should_fail/T17562.hs
new file mode 100644
index 0000000000..a758a8cfe6
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T17562.hs
@@ -0,0 +1,7 @@
+{-# LANGUAGE QuantifiedConstraints, MultiParamTypeClasses, PolyKinds #-}
+-- NB: PolyKinds. This is actually accepted with -XNoPolyKinds because of defaulting.
+-- See T17562b for the NoPolyKinds case.
+
+module T17562 where
+
+class (forall a. a b ~ a c) => C b c
diff --git a/testsuite/tests/typecheck/should_fail/T17562.stderr b/testsuite/tests/typecheck/should_fail/T17562.stderr
new file mode 100644
index 0000000000..22086bdd0d
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T17562.stderr
@@ -0,0 +1,5 @@
+
+T17562.hs:7:1: error:
+    • Uninferrable type variable k0 in
+      the class context: forall (a :: k -> k0). (a b :: k0) ~ (a c :: k0)
+    • In the class declaration for ‘C’
diff --git a/testsuite/tests/typecheck/should_fail/T17567.hs b/testsuite/tests/typecheck/should_fail/T17567.hs
new file mode 100644
index 0000000000..2ea82aae13
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T17567.hs
@@ -0,0 +1,15 @@
+{-# LANGUAGE PolyKinds, RankNTypes #-}
+
+module T17567 where
+
+import Data.Proxy
+
+type T = forall a. Proxy a
+
+p :: T
+p = Proxy
+
+x :: Proxy a -> a
+x = undefined
+
+y = x p
diff --git a/testsuite/tests/typecheck/should_fail/T17567.stderr b/testsuite/tests/typecheck/should_fail/T17567.stderr
new file mode 100644
index 0000000000..75b4de2960
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T17567.stderr
@@ -0,0 +1,5 @@
+
+T17567.hs:7:1: error:
+    • Uninferrable type variable k0 in
+      the type synonym right-hand side: forall (a :: k0). Proxy @{k0} a
+    • In the type declaration for ‘T’
diff --git a/testsuite/tests/typecheck/should_fail/T17567StupidTheta.hs b/testsuite/tests/typecheck/should_fail/T17567StupidTheta.hs
new file mode 100644
index 0000000000..a023c0f7f8
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T17567StupidTheta.hs
@@ -0,0 +1,6 @@
+{-# LANGUAGE QuantifiedConstraints, DatatypeContexts, PolyKinds #-}
+-- NB: This actually works with -XNoPolyKinds, due to defaulting.
+
+module T17567StupidTheta where
+
+data (forall a. a b ~ a c) => T b c
diff --git a/testsuite/tests/typecheck/should_fail/T17567StupidTheta.stderr b/testsuite/tests/typecheck/should_fail/T17567StupidTheta.stderr
new file mode 100644
index 0000000000..7ae2b35ab8
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T17567StupidTheta.stderr
@@ -0,0 +1,9 @@
+
+T17567StupidTheta.hs:1:37: warning:
+    -XDatatypeContexts is deprecated: It was widely considered a misfeature, and has been removed from the Haskell language.
+
+T17567StupidTheta.hs:6:1: error:
+    • Uninferrable type variable k0 in
+      the datatype context:
+      forall (a :: k -> k0). (a b :: k0) ~ (a c :: k0)
+    • In the data declaration for ‘T’
diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T
index e92404fbc5..c9318dd18f 100644
--- a/testsuite/tests/typecheck/should_fail/all.T
+++ b/testsuite/tests/typecheck/should_fail/all.T
@@ -578,6 +578,11 @@ test('ExplicitSpecificity10', normal, compile_fail, [''])
 test('T18357', normal, compile_fail, [''])
 test('T18357a', normal, compile_fail, [''])
 test('T18357b', normal, compile_fail, [''])
+test('T17301', normal, compile_fail, [''])
+test('T17567', normal, compile_fail, [''])
+test('T17562', normal, compile_fail, [''])
+test('T17567StupidTheta', normal, compile_fail, [''])
+test('T15474', normal, compile_fail, [''])
 test('T18455', normal, compile_fail, [''])
 test('T18534', normal, compile_fail, [''])
 test('T18714', normal, compile_fail, [''])