diff options
-rw-r--r-- | compiler/GHC/Tc/Gen/App.hs | 36 | ||||
-rw-r--r-- | compiler/GHC/Tc/Solver/Interact.hs | 6 | ||||
-rw-r--r-- | compiler/GHC/Tc/Types/Origin.hs | 3 | ||||
-rw-r--r-- | compiler/GHC/Tc/Utils/Monad.hs | 2 | ||||
-rw-r--r-- | testsuite/tests/indexed-types/should_fail/T13877.stderr | 60 | ||||
-rw-r--r-- | testsuite/tests/polykinds/T15577.stderr | 47 | ||||
-rw-r--r-- | testsuite/tests/typecheck/should_fail/T13819.stderr | 13 | ||||
-rw-r--r-- | testsuite/tests/typecheck/should_fail/T19482.hs | 23 | ||||
-rw-r--r-- | testsuite/tests/typecheck/should_fail/T19482.stderr | 19 | ||||
-rw-r--r-- | testsuite/tests/typecheck/should_fail/all.T | 1 |
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, ['']) |