Commit b83160d0 authored by Simon Peyton Jones's avatar Simon Peyton Jones

Tidy up treatment of FlexibleContexts

Previously (Trac #10351) we could get

    Non type-variable argument in the constraint: C [t]
    (Use FlexibleContexts to permit this)
    When checking that `f' has the inferred type
      f :: forall t. C [t] => t -> ()

which is a bit stupid: we have *inferred* a type that we
immediately *reject*.  This patch arranges that that the
generalisation mechanism (TcSimplify.decideQuantification)
doesn't pick a predicate that will be rejected by the
subsequent validity check.

This forced some minor refactoring, as usual.
parent 54cefbd7
......@@ -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)
......
......@@ -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) $
......
......@@ -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]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
......
......@@ -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
......
......@@ -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)
......
module T10351 where
class C a where
op :: a -> ()
f x = op [x]
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]
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
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
......@@ -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, [''])
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)’
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