Fix an awkward error in Visible Type Applicationwip/T19482

This error, shown up by #19482, happens if a visible type argument is
ill-kinded.  Then we failed *in the monad*, but that led to an
insoluble constraint (the error) that was not properly wrapped in
implications that bind its enclosing skolems.  Alas.

The fix is a bit clumsy, but it works. Note [VTA error recovery]
explains.

I also fixed a bug in GHC.Tc.Solver.Interact.findMatchingIrreds,
where there was a missing kind check.  Somehow this bug has never
manifested before, but it was tickled by an existing test case,
after the enhaced errror recovery in this patch.

10 files changed, 202 insertions, 8 deletions

diff --git a/compiler/GHC/Tc/Gen/App.hs b/compiler/GHC/Tc/Gen/App.hs
index 4f4f53f1cf..2271e44ed7 100644
--- a/compiler/GHC/Tc/Gen/App.hs
+++ b/compiler/GHC/Tc/Gen/App.hs
@@ -40,6 +40,7 @@ import GHC.Core.TyCo.FVs( shallowTyCoVarsOfType )
 import GHC.Core.Type
 import GHC.Tc.Types.Evidence
 import GHC.Types.Var.Set
+import GHC.Types.Error( errorsFound )
 import GHC.Builtin.PrimOps( tagToEnumKey )
 import GHC.Builtin.Names
 import GHC.Driver.Session
@@ -678,7 +679,16 @@ tcVTA fun_ty hs_ty
     -- See Note [Required quantifiers in the type of a term]
   = do { let tv   = binderVar tvb
              kind = tyVarKind tv
-       ; ty_arg <- tcHsTypeApp hs_ty kind
+
+       -- Kind-check the type argument
+       -- If that fails, use a fresh unification variable so we can carry on
+       -- This is tricky: see Note [VTA error recovery]
+       ; (mb_ty_arg, msgs) <- tryTc (tcHsTypeApp hs_ty kind)
+       ; addMessages msgs
+       ; when (errorsFound msgs) failM
+       ; ty_arg <- case mb_ty_arg of
+                     Just ty -> return ty
+                     Nothing -> newFlexiTyVarTy kind
 
        ; inner_ty <- zonkTcType inner_ty
              -- See Note [Visible type application zonk]
@@ -719,6 +729,30 @@ GHCs we had an ASSERT that Required could not occur here.
 The ice is thin; c.f. Note [No Required TyCoBinder in terms]
 in GHC.Core.TyCo.Rep.
 
+Note [VTA error recovery]
+~~~~~~~~~~~~~~~~~~~~~~~~~
+An awkward case was shown in #19482.  Consider
+  testF :: forall a (b :: [a]). ()
+
+  foo :: forall r (s::r). ()
+  foo = testF @r @s
+
+The visible type args are ill-kinded: `a` is instantiated to `r`, and
+`b` to `s`.  But the kind of `s` doesn't match the kind of `b`.  This
+is detected tcHsTypeApp, which fails in the monad (in solveEqualities,
+which calls simplifyAndEmitFlatConstraints).  We don't want to propagate
+this failure outwards, because then we'll fail to wrap it in an implication
+that binds the skolems r and s and we get a "No skolem info" error.
+
+So we recover here, and treat an ill-kinded visible type arg as if it
+were `_`, a unification variable.  Unless there is a real life error message
+coming from the failure, in which case we *can* propagate because that
+message will "win".
+
+None of this is satisfying; it's very tricky having errors in the constraints
+that have to be wrapped by enclosing implications.  We may get a cascade
+of errors from an ill-kinded VTA argument.  But it does at least work.
+
 Note [VTA for out-of-scope functions]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Suppose 'wurble' is not in scope, and we have
diff --git a/compiler/GHC/Tc/Solver/Interact.hs b/compiler/GHC/Tc/Solver/Interact.hs
index 8474ca7007..105558c3a2 100644
--- a/compiler/GHC/Tc/Solver/Interact.hs
+++ b/compiler/GHC/Tc/Solver/Interact.hs
@@ -710,6 +710,7 @@ findMatchingIrreds irreds ev
     match_non_eq ct
       | ctPred ct `tcEqTypeNoKindCheck` pred = Left (ct, NotSwapped)
       | otherwise                            = Right ct
+      -- NoKindCheck: pred has kind Constraint
 
     match_eq eq_rel1 lty1 rty1 ct
       | EqPred eq_rel2 lty2 rty2 <- classifyPredType (ctPred ct)
@@ -720,9 +721,10 @@ findMatchingIrreds irreds ev
       = Right ct
 
     match_eq_help lty1 rty1 lty2 rty2
-      | lty1 `tcEqTypeNoKindCheck` lty2, rty1 `tcEqTypeNoKindCheck` rty2
+      | lty1 `tcEqType` lty2, rty1 `tcEqTypeNoKindCheck` rty2
+        -- NoKindCheck: if LHSs have same kind, so have RHSs
       = Just NotSwapped
-      | lty1 `tcEqTypeNoKindCheck` rty2, rty1 `tcEqTypeNoKindCheck` lty2
+      | lty1 `tcEqType` rty2, rty1 `tcEqTypeNoKindCheck` lty2
       = Just IsSwapped
       | otherwise
       = Nothing
diff --git a/compiler/GHC/Tc/Types/Origin.hs b/compiler/GHC/Tc/Types/Origin.hs
index 4ddb0ee000..4e6eb2e9b8 100644
--- a/compiler/GHC/Tc/Types/Origin.hs
+++ b/compiler/GHC/Tc/Types/Origin.hs
@@ -46,7 +46,6 @@ import GHC.Data.FastString
 
 import GHC.Utils.Outputable
 import GHC.Utils.Panic
-import GHC.Driver.Ppr
 
 {- *********************************************************************
 *                                                                      *
@@ -269,7 +268,7 @@ pprSkolInfo RuntimeUnkSkol     = text "Unknown type from GHCi runtime"
 -- UnkSkol
 -- For type variables the others are dealt with by pprSkolTvBinding.
 -- For Insts, these cases should not happen
-pprSkolInfo UnkSkol = WARN( True, text "pprSkolInfo: UnkSkol" ) text "UnkSkol"
+pprSkolInfo UnkSkol = text "UnkSkol"
 
 pprSigSkolInfo :: UserTypeCtxt -> TcType -> SDoc
 -- The type is already tidied
diff --git a/compiler/GHC/Tc/Utils/Monad.hs b/compiler/GHC/Tc/Utils/Monad.hs
index a3d5b15c98..fe0a111938 100644
--- a/compiler/GHC/Tc/Utils/Monad.hs
+++ b/compiler/GHC/Tc/Utils/Monad.hs
@@ -78,7 +78,7 @@ module GHC.Tc.Utils.Monad(
   -- * Shared error message stuff: renamer and typechecker
   mkLongErrAt, mkDecoratedSDocAt, addLongErrAt, reportErrors, reportError,
   reportWarning, recoverM, mapAndRecoverM, mapAndReportM, foldAndRecoverM,
-  attemptM, tryTc,
+  attemptM, tryTc, tcTryM,
   askNoErrs, discardErrs, tryTcDiscardingErrs,
   checkNoErrs, whenNoErrs,
   ifErrsM, failIfErrsM,
diff --git a/testsuite/tests/indexed-types/should_fail/T13877.stderr b/testsuite/tests/indexed-types/should_fail/T13877.stderr
index fdbc89ab1e..ed84505356 100644
--- a/testsuite/tests/indexed-types/should_fail/T13877.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T13877.stderr
@@ -1,7 +1,63 @@
 
+T13877.hs:65:17: error:
+    • Couldn't match type: Apply p l
+                     with: t0 l
+      Expected: Sing l
+                -> (p @@ '[])
+                -> (forall (x :: a1) (xs :: [a1]).
+                    Sing x -> Sing xs -> (p @@ xs) -> p @@ (x : xs))
+                -> p @@ l
+        Actual: Sing l
+                -> App [a1] (':->) (*) t0 '[]
+                -> (forall (x :: a1) (xs :: [a1]).
+                    Sing x
+                    -> Sing xs
+                    -> App [a1] (':->) (*) t0 xs
+                    -> App [a1] (':->) (*) t0 (x : xs))
+                -> App [a1] (':->) (*) t0 l
+      The type variable ‘t0’ is ambiguous
+    • In the expression: listElimPoly @(:->) @a @p @l
+      In an equation for ‘listElimTyFun’:
+          listElimTyFun = listElimPoly @(:->) @a @p @l
+    • Relevant bindings include
+        listElimTyFun :: Sing l
+                         -> (p @@ '[])
+                         -> (forall (x :: a1) (xs :: [a1]).
+                             Sing x -> Sing xs -> (p @@ xs) -> p @@ (x : xs))
+                         -> p @@ l
+          (bound at T13877.hs:65:1)
+
+T13877.hs:65:17: error:
+    • Couldn't match type: Apply p xs
+                     with: t0 xs
+      Expected: Sing l
+                -> (p @@ '[])
+                -> (forall (x :: a1) (xs :: [a1]).
+                    Sing x -> Sing xs -> (p @@ xs) -> p @@ (x : xs))
+                -> p @@ l
+        Actual: Sing l
+                -> App [a1] (':->) (*) t0 '[]
+                -> (forall (x :: a1) (xs :: [a1]).
+                    Sing x
+                    -> Sing xs
+                    -> App [a1] (':->) (*) t0 xs
+                    -> App [a1] (':->) (*) t0 (x : xs))
+                -> App [a1] (':->) (*) t0 l
+      The type variable ‘t0’ is ambiguous
+    • In the expression: listElimPoly @(:->) @a @p @l
+      In an equation for ‘listElimTyFun’:
+          listElimTyFun = listElimPoly @(:->) @a @p @l
+    • Relevant bindings include
+        listElimTyFun :: Sing l
+                         -> (p @@ '[])
+                         -> (forall (x :: a1) (xs :: [a1]).
+                             Sing x -> Sing xs -> (p @@ xs) -> p @@ (x : xs))
+                         -> p @@ l
+          (bound at T13877.hs:65:1)
+
 T13877.hs:65:41: error:
     • Expecting one more argument to ‘p’
-      Expected kind ‘(-?>) [a] (*) (':->)’, but ‘p’ has kind ‘[a] ~> *’
+      Expected kind ‘(-?>) [a1] (*) (':->)’, but ‘p’ has kind ‘[a1] ~> *’
     • In the type ‘p’
       In the expression: listElimPoly @(:->) @a @p @l
       In an equation for ‘listElimTyFun’:
@@ -9,7 +65,7 @@ T13877.hs:65:41: error:
     • Relevant bindings include
         listElimTyFun :: Sing l
                          -> (p @@ '[])
-                         -> (forall (x :: a) (xs :: [a]).
+                         -> (forall (x :: a1) (xs :: [a1]).
                              Sing x -> Sing xs -> (p @@ xs) -> p @@ (x : xs))
                          -> p @@ l
           (bound at T13877.hs:65:1)
diff --git a/testsuite/tests/polykinds/T15577.stderr b/testsuite/tests/polykinds/T15577.stderr
index 5478da8b4a..8aaf3b581f 100644
--- a/testsuite/tests/polykinds/T15577.stderr
+++ b/testsuite/tests/polykinds/T15577.stderr
@@ -7,3 +7,50 @@ T15577.hs:20:18: error:
                      an equation for ‘g’:
         Refl <- f @f @a @r r
       In an equation for ‘g’: g r | Refl <- f @f @a @r r = Refl
+
+T15577.hs:20:21: error:
+    • Expected kind ‘f1 a1 -> *’, but ‘a’ has kind ‘*’
+    • In the type ‘a’
+      In a stmt of a pattern guard for
+                     an equation for ‘g’:
+        Refl <- f @f @a @r r
+      In an equation for ‘g’: g r | Refl <- f @f @a @r r = Refl
+    • Relevant bindings include
+        r :: Proxy r1 (bound at T15577.hs:18:3)
+        g :: Proxy r1 -> F r1 :~: r1 (bound at T15577.hs:18:1)
+
+T15577.hs:20:26: error:
+    • Couldn't match kind ‘GHC.Types.RuntimeRep’ with ‘*’
+      When matching kinds
+        f1 :: * -> *
+        TYPE :: GHC.Types.RuntimeRep -> *
+    • In the fourth argument of ‘f’, namely ‘r’
+      In a stmt of a pattern guard for
+                     an equation for ‘g’:
+        Refl <- f @f @a @r r
+      In an equation for ‘g’: g r | Refl <- f @f @a @r r = Refl
+    • Relevant bindings include
+        r :: Proxy r1 (bound at T15577.hs:18:3)
+        g :: Proxy r1 -> F r1 :~: r1 (bound at T15577.hs:18:1)
+
+T15577.hs:21:7: error:
+    • Could not deduce: F r1 ~ r1
+      from the context: r0 ~ F r0
+        bound by a pattern with constructor:
+                   Refl :: forall {k} (a :: k). a :~: a,
+                 in a pattern binding in
+                      a pattern guard for
+                        an equation for ‘g’
+        at T15577.hs:18:7-10
+      Expected: F r1 :~: r1
+        Actual: r1 :~: r1
+      ‘r1’ is a rigid type variable bound by
+        the type signature for:
+          g :: forall (f1 :: * -> *) a1 (r1 :: f1 a1).
+               Proxy r1 -> F r1 :~: r1
+        at T15577.hs:17:1-76
+    • In the expression: Refl
+      In an equation for ‘g’: g r | Refl <- f @f @a @r r = Refl
+    • Relevant bindings include
+        r :: Proxy r1 (bound at T15577.hs:18:3)
+        g :: Proxy r1 -> F r1 :~: r1 (bound at T15577.hs:18:1)
diff --git a/testsuite/tests/typecheck/should_fail/T13819.stderr b/testsuite/tests/typecheck/should_fail/T13819.stderr
index 917345f710..d0453c3d1a 100644
--- a/testsuite/tests/typecheck/should_fail/T13819.stderr
+++ b/testsuite/tests/typecheck/should_fail/T13819.stderr
@@ -1,4 +1,17 @@
 
+T13819.hs:12:10: error:
+    • Couldn't match type: w0 -> A w0
+                     with: A a
+      Expected: a -> A a
+        Actual: a -> w0 -> A w0
+    • Probable cause: ‘pure’ is applied to too few arguments
+      In the expression: pure @(_ -> WrappedMonad A _) @(_ -> A _) pure
+      In an equation for ‘pure’:
+          pure = pure @(_ -> WrappedMonad A _) @(_ -> A _) pure
+      In the instance declaration for ‘Applicative A’
+    • Relevant bindings include
+        pure :: a -> A a (bound at T13819.hs:12:3)
+
 T13819.hs:12:17: error:
     • Expected kind ‘* -> *’, but ‘_ -> WrappedMonad A _’ has kind ‘*’
     • In the type ‘(_ -> WrappedMonad A _)’
diff --git a/testsuite/tests/typecheck/should_fail/T19482.hs b/testsuite/tests/typecheck/should_fail/T19482.hs
new file mode 100644
index 0000000000..fe2f026739
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T19482.hs
@@ -0,0 +1,23 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE AllowAmbiguousTypes #-}
+
+module T19482 where
+
+testF :: forall a (b :: [a]). ()
+testF = ()
+
+-- Both Test1 and Test2 led to "no skolem info" errors in GHC 9.0
+
+-- Test1
+class BugClass k where
+    bugList :: ()
+instance BugClass ((s : sx) :: [r]) where
+    bugList = testF @r @s
+
+-- Test2
+foo :: forall r (s::r). ()
+foo = testF @r @s
diff --git a/testsuite/tests/typecheck/should_fail/T19482.stderr b/testsuite/tests/typecheck/should_fail/T19482.stderr
new file mode 100644
index 0000000000..1cac952c36
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T19482.stderr
@@ -0,0 +1,19 @@
+
+T19482.hs:19:25: error:
+    • Expected kind ‘[r]’, but ‘s’ has kind ‘r’
+      ‘r’ is a rigid type variable bound by
+        the instance declaration
+        at T19482.hs:18:10-35
+    • In the type ‘s’
+      In the expression: testF @r @s
+      In an equation for ‘bugList’: bugList = testF @r @s
+
+T19482.hs:23:17: error:
+    • Expected kind ‘[r]’, but ‘s’ has kind ‘r’
+      ‘r’ is a rigid type variable bound by
+        the type signature for:
+          foo :: forall r (s :: r). ()
+        at T19482.hs:22:1-26
+    • In the type ‘s’
+      In the expression: testF @r @s
+      In an equation for ‘foo’: foo = testF @r @s
diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T
index cdf26c15be..2ed8e9b093 100644
--- a/testsuite/tests/typecheck/should_fail/all.T
+++ b/testsuite/tests/typecheck/should_fail/all.T
@@ -626,3 +626,4 @@ test('T19397E3', extra_files(['T19397S.hs']), multimod_compile_fail,
     ['T19397E3.hs', '-v0 -main-is foo'])
 test('T19397E4', extra_files(['T19397S.hs']), multimod_compile_fail,
     ['T19397E4.hs', '-v0 -main-is foo'])
+test('T19482', normal, compile_fail, [''])