Commit f9686e13 authored by Richard Eisenberg's avatar Richard Eisenberg Committed by Marge Bot

Do more validity checks for quantified constraints

Close #17583.

Test case: typecheck/should_fail/T17563
parent 75355fde
Pipeline #13784 canceled with stages
......@@ -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
......
......@@ -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,
......
......@@ -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
......
......@@ -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)
......
......@@ -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
......
......@@ -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
......
......@@ -7,6 +7,7 @@
{-# Language TypeSynonymInstances #-}
{-# Language FlexibleInstances #-}
{-# Language QuantifiedConstraints #-}
{-# Language FlexibleContexts #-}
module T15943 where
......
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE FlexibleContexts #-}
module T15738 where
import Language.Haskell.TH
......
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
......
{-# LANGUAGE QuantifiedConstraints #-}
module T17563 where
blah :: (forall a. a b ~ a c) => b -> c
blah = undefined
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
......@@ -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, [''])
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment