Do more validity checks for quantified constraints

Close #17583.

Test case: typecheck/should_fail/T17563

12 files changed, 49 insertions, 22 deletions

diff --git a/compiler/basicTypes/Name.hs b/compiler/basicTypes/Name.hs
index 221c76327e..b0dfa806e0 100644
--- a/compiler/basicTypes/Name.hs
+++ b/compiler/basicTypes/Name.hs
@@ -61,7 +61,7 @@ module Name (
         isSystemName, isInternalName, isExternalName,
         isTyVarName, isTyConName, isDataConName,
         isValName, isVarName,
-        isWiredInName, isBuiltInSyntax,
+        isWiredInName, isWiredIn, isBuiltInSyntax,
         isHoleName,
         wiredInNameTyThing_maybe,
         nameIsLocalOrFrom, nameIsHomePackage,
@@ -221,6 +221,9 @@ isWiredInName     :: Name -> Bool
 isWiredInName (Name {n_sort = WiredIn _ _ _}) = True
 isWiredInName _                               = False
 
+isWiredIn :: NamedThing thing => thing -> Bool
+isWiredIn = isWiredInName . getName
+
 wiredInNameTyThing_maybe :: Name -> Maybe TyThing
 wiredInNameTyThing_maybe (Name {n_sort = WiredIn _ thing _}) = Just thing
 wiredInNameTyThing_maybe _                                   = Nothing
diff --git a/compiler/coreSyn/CoreLint.hs b/compiler/coreSyn/CoreLint.hs
index def51f5010..3ebad40adb 100644
--- a/compiler/coreSyn/CoreLint.hs
+++ b/compiler/coreSyn/CoreLint.hs
@@ -2367,7 +2367,7 @@ lookupIdInScope id_occ
                             2 (pprBndr LetBind id_occ)
     bad_global id_bnd = isGlobalId id_occ
                      && isLocalId id_bnd
-                     && not (isWiredInName (idName id_occ))
+                     && not (isWiredIn id_occ)
        -- 'bad_global' checks for the case where an /occurrence/ is
        -- a GlobalId, but there is an enclosing binding fora a LocalId.
        -- NB: the in-scope variables are mostly LocalIds, checked by lintIdBndr,
diff --git a/compiler/main/TidyPgm.hs b/compiler/main/TidyPgm.hs
index f087d96bca..2ad9dc7bd4 100644
--- a/compiler/main/TidyPgm.hs
+++ b/compiler/main/TidyPgm.hs
@@ -174,7 +174,7 @@ mkBootModDetailsTc hsc_env
                 | id <- typeEnvIds type_env
                 , keep_it id ]
 
-    final_tcs  = filterOut (isWiredInName . getName) tcs
+    final_tcs  = filterOut isWiredIn tcs
                  -- See Note [Drop wired-in things]
     type_env1  = typeEnvFromEntities final_ids final_tcs fam_insts
     insts'     = mkFinalClsInsts type_env1 insts
@@ -385,10 +385,10 @@ tidyProgram hsc_env  (ModGuts { mg_module    = mod
               ; final_ids  = [ if omit_prags then trimId id else id
                              | id <- bindersOfBinds tidy_binds
                              , isExternalName (idName id)
-                             , not (isWiredInName (getName id))
+                             , not (isWiredIn id)
                              ]   -- See Note [Drop wired-in things]
 
-              ; final_tcs      = filterOut (isWiredInName . getName) tcs
+              ; final_tcs      = filterOut isWiredIn tcs
                                  -- See Note [Drop wired-in things]
               ; type_env       = typeEnvFromEntities final_ids final_tcs fam_insts
               ; tidy_cls_insts = mkFinalClsInsts type_env cls_insts
diff --git a/compiler/typecheck/TcDeriv.hs b/compiler/typecheck/TcDeriv.hs
index 3f89e2c033..d43afe32bc 100644
--- a/compiler/typecheck/TcDeriv.hs
+++ b/compiler/typecheck/TcDeriv.hs
@@ -1915,7 +1915,7 @@ doDerivInstErrorChecks1 mechanism =
 
         rdr_env <- lift getGlobalRdrEnv
         let data_con_names = map dataConName (tyConDataCons rep_tc)
-            hidden_data_cons = not (isWiredInName (tyConName rep_tc)) &&
+            hidden_data_cons = not (isWiredIn rep_tc) &&
                                (isAbstractTyCon rep_tc ||
                                 any not_in_scope data_con_names)
             not_in_scope dc  = isNothing (lookupGRE_Name rdr_env dc)
diff --git a/compiler/typecheck/TcTyClsDecls.hs b/compiler/typecheck/TcTyClsDecls.hs
index 0695dd8970..7fec6f4dd3 100644
--- a/compiler/typecheck/TcTyClsDecls.hs
+++ b/compiler/typecheck/TcTyClsDecls.hs
@@ -3394,6 +3394,12 @@ checkValidTyCon tc
   | isPrimTyCon tc   -- Happens when Haddock'ing GHC.Prim
   = return ()
 
+  | isWiredIn tc     -- validity-checking wired-in tycons is a waste of
+                     -- time. More importantly, a wired-in tycon might
+                     -- violate assumptions. Example: (~) has a superclass
+                     -- mentioning (~#), which is ill-kinded in source Haskell
+  = traceTc "Skipping validity check for wired-in" (ppr tc)
+
   | otherwise
   = do { traceTc "checkValidTyCon" (ppr tc $$ ppr (tyConClass_maybe tc))
        ; if | Just cl <- tyConClass_maybe tc
diff --git a/compiler/typecheck/TcValidity.hs b/compiler/typecheck/TcValidity.hs
index 3f780fe546..1b5777e33b 100644
--- a/compiler/typecheck/TcValidity.hs
+++ b/compiler/typecheck/TcValidity.hs
@@ -1116,15 +1116,14 @@ check_pred_help under_syn env dflags ctxt pred
         | isCTupleClass cls   -> check_tuple_pred under_syn env dflags ctxt pred tys
         | otherwise           -> check_class_pred env dflags ctxt pred cls tys
 
-      EqPred NomEq _ _  -> -- a ~# b
-                           check_eq_pred env dflags pred
-
-      EqPred ReprEq _ _ -> -- Ugh!  When inferring types we may get
-                           -- f :: (a ~R# b) => blha
-                           -- And we want to treat that like (Coercible a b)
-                           -- We should probably check argument shapes, but we
-                           -- didn't do so before, so I'm leaving it for now
-                           return ()
+      EqPred _ _ _      -> pprPanic "check_pred_help" (ppr pred)
+              -- EqPreds, such as (t1 ~ #t2) or (t1 ~R# t2), don't even have kind Constraint
+              -- and should never appear before the '=>' of a type.  Thus
+              --     f :: (a ~# b) => blah
+              -- is wrong.  For user written signatures, it'll be rejected by kind-checking
+              -- well before we get to validity checking.  For inferred types we are careful
+              -- to box such constraints in TcType.pickQuantifiablePreds, as described
+              -- in Note [Lift equality constraints when quantifying] in TcType
 
       ForAllPred _ theta head -> check_quant_pred env dflags ctxt pred theta head
       IrredPred {}            -> check_irred_pred under_syn env dflags ctxt pred
@@ -1139,13 +1138,18 @@ check_eq_pred env dflags pred
 
 check_quant_pred :: TidyEnv -> DynFlags -> UserTypeCtxt
                  -> PredType -> ThetaType -> PredType -> TcM ()
-check_quant_pred env dflags _ctxt pred theta head_pred
+check_quant_pred env dflags ctxt pred theta head_pred
   = addErrCtxt (text "In the quantified constraint" <+> quotes (ppr pred)) $
     do { -- Check the instance head
          case classifyPredType head_pred of
-            ClassPred cls tys -> checkValidInstHead SigmaCtxt cls tys
                                  -- SigmaCtxt tells checkValidInstHead that
                                  -- this is the head of a quantified constraint
+            ClassPred cls tys -> do { checkValidInstHead SigmaCtxt cls tys
+                                    ; check_pred_help False env dflags ctxt head_pred }
+                               -- need check_pred_help to do extra pred-only validity
+                               -- checks, such as for (~). Otherwise, we get #17563
+                               -- NB: checks for the context are covered by the check_type
+                               -- in check_pred_ty
             IrredPred {}      | hasTyVarHead head_pred
                               -> return ()
             _                 -> failWithTcM (badQuantHeadErr env pred)
@@ -1216,10 +1220,9 @@ solved to add+canonicalise another (Foo a) constraint.  -}
 check_class_pred :: TidyEnv -> DynFlags -> UserTypeCtxt
                  -> PredType -> Class -> [TcType] -> TcM ()
 check_class_pred env dflags ctxt pred cls tys
-  |  isEqPredClass cls    -- (~) and (~~) are classified as classes,
-                          -- but here we want to treat them as equalities
-  = -- pprTrace "check_class" (ppr cls) $
-    check_eq_pred env dflags pred
+  | isEqPredClass cls    -- (~) and (~~) are classified as classes,
+                         -- but here we want to treat them as equalities
+  = check_eq_pred env dflags pred
 
   | isIPClass cls
   = do { check_arity
diff --git a/testsuite/tests/indexed-types/should_compile/T15943.hs b/testsuite/tests/indexed-types/should_compile/T15943.hs
index 36edbbc62b..1f03f81fd2 100644
--- a/testsuite/tests/indexed-types/should_compile/T15943.hs
+++ b/testsuite/tests/indexed-types/should_compile/T15943.hs
@@ -7,6 +7,7 @@
 {-# Language TypeSynonymInstances   #-}
 {-# Language FlexibleInstances      #-}
 {-# Language QuantifiedConstraints  #-}
+{-# Language FlexibleContexts       #-}
 
 module T15943 where
 
diff --git a/testsuite/tests/th/T15738.hs b/testsuite/tests/th/T15738.hs
index 4bc2d45686..63f47516d7 100644
--- a/testsuite/tests/th/T15738.hs
+++ b/testsuite/tests/th/T15738.hs
@@ -1,5 +1,6 @@
 {-# LANGUAGE QuantifiedConstraints #-}
 {-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE FlexibleContexts #-}
 module T15738 where
 
 import Language.Haskell.TH
diff --git a/testsuite/tests/th/T15738.stderr b/testsuite/tests/th/T15738.stderr
index 580a02a62e..f158e54e06 100644
--- a/testsuite/tests/th/T15738.stderr
+++ b/testsuite/tests/th/T15738.stderr
@@ -1,7 +1,7 @@
 f_0 :: (forall a_1 . GHC.Classes.Eq (T15738.Foo a_1)) =>
        T15738.Foo x_2 -> T15738.Foo x_2 -> GHC.Types.Bool
 f_0 = (GHC.Classes.==)
-T15738.hs:(10,2)-(13,12): Splicing declarations
+T15738.hs:(11,2)-(14,12): Splicing declarations
     do d <- [d| f :: (forall a. Eq (Foo a)) => Foo x -> Foo x -> Bool
                 f = (==) |]
        runIO $ hPutStrLn stderr $ pprint d
diff --git a/testsuite/tests/typecheck/should_fail/T17563.hs b/testsuite/tests/typecheck/should_fail/T17563.hs
new file mode 100644
index 0000000000..cab972a1bf
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T17563.hs
@@ -0,0 +1,6 @@
+{-# LANGUAGE QuantifiedConstraints #-}
+
+module T17563 where
+
+blah :: (forall a. a b ~ a c) => b -> c
+blah = undefined
diff --git a/testsuite/tests/typecheck/should_fail/T17563.stderr b/testsuite/tests/typecheck/should_fail/T17563.stderr
new file mode 100644
index 0000000000..c24587c1a6
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T17563.stderr
@@ -0,0 +1,6 @@
+
+T17563.hs:5:9: error:
+    • Illegal equational constraint a b ~ a c
+      (Use GADTs or TypeFamilies to permit this)
+    • In the quantified constraint ‘forall (a :: * -> *). a b ~ a c’
+      In the type signature: blah :: (forall a. a b ~ a c) => b -> c
diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T
index 75c1fe6f19..e46f694dd3 100644
--- a/testsuite/tests/typecheck/should_fail/all.T
+++ b/testsuite/tests/typecheck/should_fail/all.T
@@ -548,3 +548,4 @@ test('T16512b', normal, compile_fail, [''])
 test('T17213', [extra_files(['T17213a.hs'])], multimod_compile_fail, ['T17213', '-v0'])
 test('T17355', normal, compile_fail, [''])
 test('T17360', normal, compile_fail, [''])
+test('T17563', normal, compile_fail, [''])