diff options
author | Richard Eisenberg <rae@richarde.dev> | 2019-12-10 17:52:11 +0000 |
---|---|---|
committer | Marge Bot <ben+marge-bot@smart-cactus.org> | 2019-12-16 19:32:21 -0500 |
commit | f9686e132a7fe5bbe517a4748fef6094fe74d43d (patch) | |
tree | a0ce85a36dd3c8c60c5101bd87f2f579b63cd4d4 | |
parent | 75355fdef61da44a395ee9bfa2b9dca0eecea58a (diff) | |
download | haskell-f9686e132a7fe5bbe517a4748fef6094fe74d43d.tar.gz |
Do more validity checks for quantified constraints
Close #17583.
Test case: typecheck/should_fail/T17563
-rw-r--r-- | compiler/basicTypes/Name.hs | 5 | ||||
-rw-r--r-- | compiler/coreSyn/CoreLint.hs | 2 | ||||
-rw-r--r-- | compiler/main/TidyPgm.hs | 6 | ||||
-rw-r--r-- | compiler/typecheck/TcDeriv.hs | 2 | ||||
-rw-r--r-- | compiler/typecheck/TcTyClsDecls.hs | 6 | ||||
-rw-r--r-- | compiler/typecheck/TcValidity.hs | 33 | ||||
-rw-r--r-- | testsuite/tests/indexed-types/should_compile/T15943.hs | 1 | ||||
-rw-r--r-- | testsuite/tests/th/T15738.hs | 1 | ||||
-rw-r--r-- | testsuite/tests/th/T15738.stderr | 2 | ||||
-rw-r--r-- | testsuite/tests/typecheck/should_fail/T17563.hs | 6 | ||||
-rw-r--r-- | testsuite/tests/typecheck/should_fail/T17563.stderr | 6 | ||||
-rw-r--r-- | testsuite/tests/typecheck/should_fail/all.T | 1 |
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, ['']) |