summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--compiler/main/DynFlags.hs5
-rw-r--r--compiler/typecheck/TcBinds.hs5
-rw-r--r--compiler/typecheck/TcSimplify.hs57
-rw-r--r--compiler/typecheck/TcType.hs31
-rw-r--r--compiler/typecheck/TcValidity.hs111
-rw-r--r--testsuite/tests/typecheck/should_fail/T10351.hs6
-rw-r--r--testsuite/tests/typecheck/should_fail/T10351.stderr5
-rw-r--r--testsuite/tests/typecheck/should_fail/T6022.stderr13
-rw-r--r--testsuite/tests/typecheck/should_fail/T8883.stderr18
-rw-r--r--testsuite/tests/typecheck/should_fail/all.T1
-rw-r--r--testsuite/tests/typecheck/should_fail/tcfail108.stderr13
11 files changed, 152 insertions, 113 deletions
diff --git a/compiler/main/DynFlags.hs b/compiler/main/DynFlags.hs
index 094984be2e..f078c5162a 100644
--- a/compiler/main/DynFlags.hs
+++ b/compiler/main/DynFlags.hs
@@ -3264,11 +3264,6 @@ impliedXFlags
, (Opt_ParallelArrays, turnOn, Opt_ParallelListComp)
- -- An implicit parameter constraint, `?x::Int`, is desugared into
- -- `IP "x" Int`, which requires a flexible context/instance.
- , (Opt_ImplicitParams, turnOn, Opt_FlexibleContexts)
- , (Opt_ImplicitParams, turnOn, Opt_FlexibleInstances)
-
, (Opt_JavaScriptFFI, turnOn, Opt_InterruptibleFFI)
, (Opt_DeriveTraversable, turnOn, Opt_DeriveFunctor)
diff --git a/compiler/typecheck/TcBinds.hs b/compiler/typecheck/TcBinds.hs
index 17f60787c6..64333ebdb3 100644
--- a/compiler/typecheck/TcBinds.hs
+++ b/compiler/typecheck/TcBinds.hs
@@ -688,8 +688,9 @@ mkInferredPolyId poly_name qtvs theta mono_ty
my_tvs2 = closeOverKinds (growThetaTyVars theta (tyVarsOfType norm_mono_ty))
-- Include kind variables! Trac #7916
- my_tvs = filter (`elemVarSet` my_tvs2) qtvs -- Maintain original order
- my_theta = filter (quantifyPred my_tvs2) theta
+ ; my_theta <- pickQuantifiablePreds my_tvs2 theta
+
+ ; let my_tvs = filter (`elemVarSet` my_tvs2) qtvs -- Maintain original order
inferred_poly_ty = mkSigmaTy my_tvs my_theta norm_mono_ty
; addErrCtxtM (mk_bind_msg True False poly_name inferred_poly_ty) $
diff --git a/compiler/typecheck/TcSimplify.hs b/compiler/typecheck/TcSimplify.hs
index 5f9f417e1c..c1535f8733 100644
--- a/compiler/typecheck/TcSimplify.hs
+++ b/compiler/typecheck/TcSimplify.hs
@@ -2,7 +2,7 @@
module TcSimplify(
simplifyInfer,
- quantifyPred, growThetaTyVars,
+ pickQuantifiablePreds, growThetaTyVars,
simplifyAmbiguityCheck,
simplifyDefault,
simplifyTop, simplifyInteractive,
@@ -40,7 +40,7 @@ import Util
import PrelInfo
import PrelNames
import Control.Monad ( unless )
-import DynFlags ( ExtensionFlag( Opt_AllowAmbiguousTypes ) )
+import DynFlags ( ExtensionFlag( Opt_AllowAmbiguousTypes, Opt_FlexibleContexts ) )
import Class ( classKey )
import Maybes ( isNothing )
import Outputable
@@ -424,8 +424,9 @@ If the monomorphism restriction does not apply, then we quantify as follows:
(This actually unifies each quantifies meta-tyvar with a fresh skolem.)
Result is qtvs.
- * Filter the constraints using quantifyPred and the qtvs. We have to
- zonk the constraints first, so they "see" the freshly created skolems.
+ * Filter the constraints using pickQuantifyablePreds and the qtvs.
+ We have to zonk the constraints first, so they "see" the freshly
+ created skolems.
If the MR does apply, mono_tvs includes all the constrained tyvars,
and the quantified constraints are empty.
@@ -457,31 +458,43 @@ decideQuantification apply_mr constraints zonked_tau_tvs
-- quantifyTyVars turned some meta tyvars into
-- quantified skolems, so we have to zonk again
- ; let theta = filter (quantifyPred (mkVarSet qtvs)) constraints
- min_theta = mkMinimalBySCs theta -- See Note [Minimize by Superclasses]
+ ; theta <- pickQuantifiablePreds (mkVarSet qtvs) constraints
+ ; let min_theta = mkMinimalBySCs theta -- See Note [Minimize by Superclasses]
+
; traceTc "decideQuantification 2" (vcat [ppr constraints, ppr gbl_tvs, ppr mono_tvs
, ppr tau_tvs_plus, ppr qtvs, ppr min_theta])
; return (qtvs, min_theta, False) }
------------------
-quantifyPred :: TyVarSet -- Quantifying over these
- -> PredType -> Bool -- True <=> quantify over this wanted
+pickQuantifiablePreds :: TyVarSet -- Quantifying over these
+ -> TcThetaType -- Proposed constraints to quantify
+ -> TcM TcThetaType -- A subset that we can actually quantify
-- This function decides whether a particular constraint shoudl be
-- quantified over, given the type variables that are being quantified
-quantifyPred qtvs pred
- = case classifyPredType pred of
- ClassPred cls tys
- | isIPClass cls -> True -- See note [Inheriting implicit parameters]
- | otherwise -> tyVarsOfTypes tys `intersectsVarSet` qtvs
-
- EqPred NomEq ty1 ty2 -> quant_fun ty1 || quant_fun ty2
- -- representational equality is like a class constraint
- EqPred ReprEq ty1 ty2 -> tyVarsOfTypes [ty1, ty2] `intersectsVarSet` qtvs
-
- IrredPred ty -> tyVarsOfType ty `intersectsVarSet` qtvs
- TuplePred {} -> False
+pickQuantifiablePreds qtvs theta
+ = do { flex_ctxt <- xoptM Opt_FlexibleContexts
+ ; return (filter (pick_me flex_ctxt) theta) }
where
- -- See Note [Quantifying over equality constraints]
+ pick_me flex_ctxt pred
+ = case classifyPredType pred of
+ ClassPred cls tys
+ | isIPClass cls -> True -- See note [Inheriting implicit parameters]
+ | otherwise -> pick_cls_pred flex_ctxt tys
+
+ EqPred ReprEq ty1 ty2 -> pick_cls_pred flex_ctxt [ty1, ty2]
+ -- Representational equality is like a class constraint
+
+ EqPred NomEq ty1 ty2 -> quant_fun ty1 || quant_fun ty2
+ IrredPred ty -> tyVarsOfType ty `intersectsVarSet` qtvs
+ TuplePred {} -> False
+
+ pick_cls_pred flex_ctxt tys
+ = tyVarsOfTypes tys `intersectsVarSet` qtvs
+ && (checkValidClsArgs flex_ctxt tys)
+ -- Only quantify over predicates that checkValidType
+ -- will pass! See Trac #10351.
+
+ -- See Note [Quantifying over equality constraints]
quant_fun ty
= case tcSplitTyConApp_maybe ty of
Just (tc, tys) | isTypeFamilyTyCon tc
@@ -558,7 +571,7 @@ dynamic binding means) so we'd better infer the second.
BOTTOM LINE: when *inferring types* you must quantify over implicit
parameters, *even if* they don't mention the bound type variables.
Reason: because implicit parameters, uniquely, have local instance
-declarations. See the predicate quantifyPred.
+declarations. See the pickQuantifiablePreds.
Note [Quantification with errors]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
diff --git a/compiler/typecheck/TcType.hs b/compiler/typecheck/TcType.hs
index 4185be8214..4d4f6823f2 100644
--- a/compiler/typecheck/TcType.hs
+++ b/compiler/typecheck/TcType.hs
@@ -69,6 +69,7 @@ module TcType (
isIntegerTy, isBoolTy, isUnitTy, isCharTy,
isTauTy, isTauTyCon, tcIsTyVarTy, tcIsForAllTy,
isPredTy, isTyVarClassPred, isTyVarExposed,
+ checkValidClsArgs, hasTyVarHead,
---------------------------------
-- Misc type manipulators
@@ -1313,6 +1314,14 @@ straightforward.
************************************************************************
Deconstructors and tests on predicate types
+
+Note [Kind polymorphic type classes]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+ class C f where... -- C :: forall k. k -> Constraint
+ g :: forall (f::*). C f => f -> f
+
+Here the (C f) in the signature is really (C * f), and we
+don't want to complain that the * isn't a type variable!
-}
isTyVarClassPred :: PredType -> Bool
@@ -1320,6 +1329,28 @@ isTyVarClassPred ty = case getClassPredTys_maybe ty of
Just (_, tys) -> all isTyVarTy tys
_ -> False
+-------------------------
+checkValidClsArgs :: Bool -> [KindOrType] -> Bool
+-- If the Bool is True (flexible contexts), return True (i.e. ok)
+-- Otherwise, check that the type (not kind) args are all headed by a tyvar
+-- E.g. (Eq a) accepted, (Eq (f a)) accepted, but (Eq Int) rejected
+-- This function is here rather than in TcValidity because it is
+-- called from TcSimplify, which itself is imported by TcValidity
+checkValidClsArgs flexible_contexts kts
+ | flexible_contexts = True
+ | otherwise = all hasTyVarHead tys
+ where
+ (_, tys) = span isKind kts -- see Note [Kind polymorphic type classes]
+
+hasTyVarHead :: Type -> Bool
+-- Returns true of (a t1 .. tn), where 'a' is a type variable
+hasTyVarHead ty -- Haskell 98 allows predicates of form
+ | tcIsTyVarTy ty = True -- C (a ty1 .. tyn)
+ | otherwise -- where a is a type variable
+ = case tcSplitAppTy_maybe ty of
+ Just (ty, _) -> hasTyVarHead ty
+ Nothing -> False
+
evVarPred_maybe :: EvVar -> Maybe PredType
evVarPred_maybe v = if isPredTy ty then Just ty else Nothing
where ty = varType v
diff --git a/compiler/typecheck/TcValidity.hs b/compiler/typecheck/TcValidity.hs
index 53b492d3e6..3225b2848b 100644
--- a/compiler/typecheck/TcValidity.hs
+++ b/compiler/typecheck/TcValidity.hs
@@ -23,13 +23,14 @@ import TcSimplify ( simplifyAmbiguityCheck )
import TypeRep
import TcType
import TcMType
-import TysWiredIn ( coercibleClass )
+import TysWiredIn ( coercibleClass, eqTyConName )
import Type
import Unify( tcMatchTyX )
import Kind
import CoAxiom
import Class
import TyCon
+import PrelNames( eqTyConKey )
-- others:
import HsSyn -- HsType
@@ -44,6 +45,7 @@ import Util
import ListSetOps
import SrcLoc
import Outputable
+import Unique ( hasKey )
import BasicTypes ( IntWithInf, infinity )
import FastString
@@ -593,6 +595,7 @@ check_valid_theta ctxt theta
= do { dflags <- getDynFlags
; warnTc (wopt Opt_WarnDuplicateConstraints dflags &&
notNull dups) (dupPredWarn dups)
+ ; traceTc "check_valid_theta" (ppr theta)
; mapM_ (check_pred_ty dflags ctxt) theta }
where
(_,dups) = removeDups cmpPred theta
@@ -612,46 +615,29 @@ check_pred_help :: Bool -- True <=> under a type synonym
-> DynFlags -> UserTypeCtxt
-> PredType -> TcM ()
check_pred_help under_syn dflags ctxt pred
- | Just pred' <- coreView pred
- = check_pred_help True dflags ctxt pred'
+ | Just pred' <- coreView pred -- Switch on under_syn when going under a
+ -- synonym (Trac #9838, yuk)
+ = check_pred_help True dflags ctxt pred'
| otherwise
- = case classifyPredType pred of
- ClassPred cls tys -> check_class_pred dflags ctxt pred cls tys
- EqPred NomEq _ _ -> check_eq_pred dflags pred
- EqPred ReprEq ty1 ty2 -> check_repr_eq_pred dflags ctxt pred ty1 ty2
- TuplePred tys -> check_tuple_pred under_syn dflags ctxt pred tys
- IrredPred _ -> check_irred_pred under_syn dflags ctxt pred
-
-check_class_pred :: DynFlags -> UserTypeCtxt -> PredType -> Class -> [TcType] -> TcM ()
-check_class_pred dflags ctxt pred cls tys
- = do { -- Class predicates are valid in all contexts
- ; checkTc (arity == n_tys) arity_err
-
- ; checkTc (not (isIPClass cls) || okIPCtxt ctxt)
- (badIPPred pred)
-
- -- Check the form of the argument types
- ; check_class_pred_tys dflags ctxt pred tys
- }
- where
- class_name = className cls
- arity = classArity cls
- n_tys = length tys
- arity_err = arityErr "Class" class_name arity n_tys
-
-check_eq_pred :: DynFlags -> PredType -> TcM ()
-check_eq_pred dflags pred
+ = case splitTyConApp_maybe pred of
+ Just (tc, tys) | Just cls <- tyConClass_maybe tc
+ -> check_class_pred dflags ctxt pred cls tys -- Includes Coercible
+ | tc `hasKey` eqTyConKey
+ -> check_eq_pred dflags pred tys
+ | isTupleTyCon tc
+ -> check_tuple_pred under_syn dflags ctxt pred tys
+ _ -> check_irred_pred under_syn dflags ctxt pred
+
+check_eq_pred :: DynFlags -> PredType -> [TcType] -> TcM ()
+check_eq_pred dflags pred tys
= -- Equational constraints are valid in all contexts if type
-- families are permitted
- checkTc (xopt Opt_TypeFamilies dflags || xopt Opt_GADTs dflags)
- (eqPredTyErr pred)
-
-check_repr_eq_pred :: DynFlags -> UserTypeCtxt -> PredType
- -> TcType -> TcType -> TcM ()
-check_repr_eq_pred dflags ctxt pred ty1 ty2
- = check_class_pred_tys dflags ctxt pred tys
+ do { checkTc (n_tys == 3)
+ (arityErr "Equality constraint" eqTyConName 3 n_tys)
+ ; checkTc (xopt Opt_TypeFamilies dflags || xopt Opt_GADTs dflags)
+ (eqPredTyErr pred) }
where
- tys = [ty1, ty2]
+ n_tys = length tys
check_tuple_pred :: Bool -> DynFlags -> UserTypeCtxt -> PredType -> [PredType] -> TcM ()
check_tuple_pred under_syn dflags ctxt pred ts
@@ -670,7 +656,7 @@ check_irred_pred under_syn dflags ctxt pred
-- see Note [ConstraintKinds in predicates]
-- But (X t1 t2) is always ok because we just require ConstraintKinds
-- at the definition site (Trac #9838)
- checkTc (under_syn || xopt Opt_ConstraintKinds dflags || not (tyvar_head pred))
+ checkTc (under_syn || xopt Opt_ConstraintKinds dflags || not (hasTyVarHead pred))
(predIrredErr pred)
-- Make sure it is OK to have an irred pred in this context
@@ -708,32 +694,30 @@ It is equally dangerous to allow them in instance heads because in that case the
Paterson conditions may not detect duplication of a type variable or size change. -}
-------------------------
-check_class_pred_tys :: DynFlags -> UserTypeCtxt
- -> PredType -> [KindOrType] -> TcM ()
-check_class_pred_tys dflags ctxt pred kts
- = checkTc pred_ok (predTyVarErr pred $$ how_to_allow)
- where
- (_, tys) = span isKind kts -- see Note [Kind polymorphic type classes]
- flexible_contexts = xopt Opt_FlexibleContexts dflags
- undecidable_ok = xopt Opt_UndecidableInstances dflags
+check_class_pred :: DynFlags -> UserTypeCtxt -> PredType -> Class -> [TcType] -> TcM ()
+check_class_pred dflags ctxt pred cls tys
+ | isIPClass cls
+ = do { checkTc (arity == n_tys) arity_err
+ ; checkTc (okIPCtxt ctxt) (badIPPred pred) }
- pred_ok = case ctxt of
- SpecInstCtxt -> True -- {-# SPECIALISE instance Eq (T Int) #-} is fine
- InstDeclCtxt -> flexible_contexts || undecidable_ok || all tcIsTyVarTy tys
- -- Further checks on head and theta in
- -- checkInstTermination
- _ -> flexible_contexts || all tyvar_head tys
- how_to_allow = parens (ptext (sLit "Use FlexibleContexts to permit this"))
+ | otherwise
+ = do { checkTc (arity == n_tys) arity_err
+ ; checkTc arg_tys_ok (predTyVarErr pred) }
+ where
+ class_name = className cls
+ arity = classArity cls
+ n_tys = length tys
+ arity_err = arityErr "Class" class_name arity n_tys
+ flexible_contexts = xopt Opt_FlexibleContexts dflags
+ undecidable_ok = xopt Opt_UndecidableInstances dflags
--------------------------
-tyvar_head :: Type -> Bool
-tyvar_head ty -- Haskell 98 allows predicates of form
- | tcIsTyVarTy ty = True -- C (a ty1 .. tyn)
- | otherwise -- where a is a type variable
- = case tcSplitAppTy_maybe ty of
- Just (ty, _) -> tyvar_head ty
- Nothing -> False
+ arg_tys_ok = case ctxt of
+ SpecInstCtxt -> True -- {-# SPECIALISE instance Eq (T Int) #-} is fine
+ InstDeclCtxt -> checkValidClsArgs (flexible_contexts || undecidable_ok) tys
+ -- Further checks on head and theta
+ -- in checkInstTermination
+ _ -> checkValidClsArgs flexible_contexts tys
-------------------------
okIPCtxt :: UserTypeCtxt -> Bool
@@ -776,8 +760,9 @@ eqPredTyErr, predTyVarErr, predTupleErr, predIrredErr, predIrredBadCtxtErr :: Pr
eqPredTyErr pred = ptext (sLit "Illegal equational constraint") <+> pprType pred
$$
parens (ptext (sLit "Use GADTs or TypeFamilies to permit this"))
-predTyVarErr pred = hang (ptext (sLit "Non type-variable argument"))
- 2 (ptext (sLit "in the constraint:") <+> pprType pred)
+predTyVarErr pred = vcat [ hang (ptext (sLit "Non type-variable argument"))
+ 2 (ptext (sLit "in the constraint:") <+> pprType pred)
+ , parens (ptext (sLit "Use FlexibleContexts to permit this")) ]
predTupleErr pred = hang (ptext (sLit "Illegal tuple constraint:") <+> pprType pred)
2 (parens constraintKindsMsg)
predIrredErr pred = hang (ptext (sLit "Illegal constraint:") <+> pprType pred)
diff --git a/testsuite/tests/typecheck/should_fail/T10351.hs b/testsuite/tests/typecheck/should_fail/T10351.hs
new file mode 100644
index 0000000000..411698b397
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T10351.hs
@@ -0,0 +1,6 @@
+module T10351 where
+
+class C a where
+ op :: a -> ()
+
+f x = op [x]
diff --git a/testsuite/tests/typecheck/should_fail/T10351.stderr b/testsuite/tests/typecheck/should_fail/T10351.stderr
new file mode 100644
index 0000000000..178005a705
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T10351.stderr
@@ -0,0 +1,5 @@
+
+T10351.hs:6:7: error:
+ No instance for (C [t]) arising from a use of ‘op’
+ In the expression: op [x]
+ In an equation for ‘f’: f x = op [x]
diff --git a/testsuite/tests/typecheck/should_fail/T6022.stderr b/testsuite/tests/typecheck/should_fail/T6022.stderr
index 4408910974..7d12b8f358 100644
--- a/testsuite/tests/typecheck/should_fail/T6022.stderr
+++ b/testsuite/tests/typecheck/should_fail/T6022.stderr
@@ -1,6 +1,7 @@
-
-T6022.hs:3:1:
- Non type-variable argument in the constraint: Eq ([a] -> a)
- (Use FlexibleContexts to permit this)
- When checking that ‘f’ has the inferred type
- f :: forall a. Eq ([a] -> a) => ([a] -> a) -> Bool
+
+T6022.hs:3:9: error:
+ No instance for (Eq ([a] -> a))
+ (maybe you haven't applied a function to enough arguments?)
+ arising from a use of ‘==’
+ In the expression: x == head
+ In an equation for ‘f’: f x = x == head
diff --git a/testsuite/tests/typecheck/should_fail/T8883.stderr b/testsuite/tests/typecheck/should_fail/T8883.stderr
index 27b4d943f1..dc4bdfcca1 100644
--- a/testsuite/tests/typecheck/should_fail/T8883.stderr
+++ b/testsuite/tests/typecheck/should_fail/T8883.stderr
@@ -1,8 +1,10 @@
-
-T8883.hs:20:1:
- Non type-variable argument in the constraint: Functor (PF a)
- (Use FlexibleContexts to permit this)
- When checking that ‘fold’ has the inferred type
- fold :: forall b a.
- (Functor (PF a), Regular a) =>
- (PF a b -> b) -> a -> b
+
+T8883.hs:20:14: error:
+ Could not deduce (Functor (PF a)) arising from a use of ‘fmap’
+ from the context: Regular a
+ bound by the inferred type of
+ fold :: Regular a => (PF a b -> b) -> a -> b
+ at T8883.hs:20:1-33
+ In the first argument of ‘(.)’, namely ‘fmap (fold f)’
+ In the second argument of ‘(.)’, namely ‘fmap (fold f) . from’
+ In the expression: f . fmap (fold f) . from
diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T
index faca0791a4..b9c7d5ac1f 100644
--- a/testsuite/tests/typecheck/should_fail/all.T
+++ b/testsuite/tests/typecheck/should_fail/all.T
@@ -364,3 +364,4 @@ test('T9858e', normal, compile_fail, [''])
test('T10285',
extra_clean(['T10285a.hi', 'T10285a.o']),
multimod_compile_fail, ['T10285', '-v0'])
+test('T10351', normal, compile_fail, [''])
diff --git a/testsuite/tests/typecheck/should_fail/tcfail108.stderr b/testsuite/tests/typecheck/should_fail/tcfail108.stderr
index b23e9d91a5..3a2e5a5657 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail108.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail108.stderr
@@ -1,7 +1,6 @@
-
-tcfail108.hs:7:10:
- Non type-variable argument in the constraint: Eq (f (Rec f))
- (Use FlexibleContexts to permit this)
- In the context: Eq (f (Rec f))
- While checking an instance declaration
- In the instance declaration for ‘Eq (Rec f)’
+
+tcfail108.hs:7:10: error:
+ Variable ‘f’ occurs more often than in the instance head
+ in the constraint: Eq (f (Rec f))
+ (Use UndecidableInstances to permit this)
+ In the instance declaration for ‘Eq (Rec f)’
View Lorry Controller Status