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

Use partial-sig constraints as givens

In TcSimplify.simplifyInfer, use the context of a partial type
signature as 'givens' when simplifying the inferred constraints of the
group.  This way we get maximum benefit from them.  See
Note [Add signature contexts as givens].

This (finally) fixes test EqualityConstraints in Trac #9478.

And it's a nice tidy-up.
parent e7e5939d
......@@ -777,10 +777,10 @@ chooseInferredQuantifiers :: TcThetaType -- inferred
-> Maybe TcIdSigInfo
-> TcM ([TcTyBinder], TcThetaType)
chooseInferredQuantifiers inferred_theta tau_tvs qtvs Nothing
= -- No type signature for this binder
= -- No type signature (partial or complete) for this binder,
do { let free_tvs = closeOverKinds (growThetaTyVars inferred_theta tau_tvs)
-- Include kind variables! Trac #7916
my_theta = pickQuantifiablePreds free_tvs [] inferred_theta
my_theta = pickCapturedPreds free_tvs inferred_theta
binders = [ mkNamedBinder Invisible tv
| tv <- qtvs
, tv `elemVarSet` free_tvs ]
......@@ -804,16 +804,15 @@ chooseInferredQuantifiers inferred_theta tau_tvs qtvs
= do { annotated_theta <- zonkTcTypes annotated_theta
; let free_tvs = closeOverKinds (tyCoVarsOfTypes annotated_theta
`unionVarSet` tau_tvs)
my_theta = pickQuantifiablePreds free_tvs annotated_theta inferred_theta
my_theta = pickCapturedPreds free_tvs inferred_theta
-- Report the inferred constraints for an extra-constraints wildcard/hole as
-- an error message, unless the PartialTypeSignatures flag is enabled. In this
-- case, the extra inferred constraints are accepted without complaining.
-- Returns the annotated constraints combined with the inferred constraints.
-- NB: inferred_theta already includes all the annotated constraints
inferred_diff = [ pred
| pred <- my_theta
, all (not . (`eqType` pred)) annotated_theta ]
final_theta = annotated_theta ++ inferred_diff
; partial_sigs <- xoptM LangExt.PartialTypeSignatures
; warn_partial_sigs <- woptM Opt_WarnPartialTypeSignatures
; msg <- mkLongErrAt loc (mk_msg inferred_diff partial_sigs hs_ty) empty
......@@ -827,7 +826,7 @@ chooseInferredQuantifiers inferred_theta tau_tvs qtvs
| otherwise -> return ()
False -> reportError msg
; return (mk_binders free_tvs, final_theta) }
; return (mk_binders free_tvs, my_theta) }
| otherwise -- A complete type signature is dealt with in mkInferredPolyId
= pprPanic "chooseInferredQuantifiers" (ppr bndr_info)
......
This diff is collapsed.
......@@ -91,7 +91,7 @@ module TcType (
---------------------------------
-- Predicate types
mkMinimalBySCs, transSuperClasses,
pickQuantifiablePreds,
pickQuantifiablePreds, pickCapturedPreds,
immSuperClasses,
isImprovementPred,
......@@ -100,7 +100,7 @@ module TcType (
-- * Finding "exact" (non-dead) type variables
exactTyCoVarsOfType, exactTyCoVarsOfTypes,
splitDepVarsOfType, splitDepVarsOfTypes, TcDepVars(..), depVarsTyVars,
splitDepVarsOfType, splitDepVarsOfTypes, TcDepVars(..), tcDepVarSet,
-- * Extracting bound variables
allBoundVariables, allBoundVariabless,
......@@ -861,8 +861,10 @@ data TcDepVars -- See Note [Dependent type variables]
-- See Note [Dependent type variables]
}
depVarsTyVars :: TcDepVars -> DTyVarSet
depVarsTyVars = dv_tvs
tcDepVarSet :: TcDepVars -> TyVarSet
-- Actually can contain CoVars, but never mind
tcDepVarSet (DV { dv_kvs = kvs, dv_tvs = tvs })
= dVarSetToVarSet kvs `unionVarSet` dVarSetToVarSet tvs
instance Monoid TcDepVars where
mempty = DV { dv_kvs = emptyDVarSet, dv_tvs = emptyDVarSet }
......@@ -1832,12 +1834,11 @@ evVarPred var
-- [Inheriting implicit parameters] and [Quantifying over equality constraints]
pickQuantifiablePreds
:: TyVarSet -- Quantifying over these
-> TcThetaType -- Context from PartialTypeSignatures
-> TcThetaType -- Proposed constraints to quantify
-> TcThetaType -- A subset that we can actually quantify
-- This function decides whether a particular constraint should be
-- quantified over, given the type variables that are being quantified
pickQuantifiablePreds qtvs annotated_theta theta
pickQuantifiablePreds qtvs theta
= let flex_ctxt = True in -- Quantify over non-tyvar constraints, even without
-- -XFlexibleContexts: see Trac #10608, #10351
-- flex_ctxt <- xoptM Opt_FlexibleContexts
......@@ -1847,14 +1848,13 @@ pickQuantifiablePreds qtvs annotated_theta theta
= case classifyPredType pred of
ClassPred cls tys
| Just str <- isCallStackPred pred
-- NEVER infer a CallStack constraint, unless we were
-- given one in a partial type signatures.
| Just {} <- isCallStackPred pred
-- NEVER infer a CallStack constraint
-- Otherwise, we let the constraints bubble up to be
-- solved from the outer context, or be defaulted when we
-- reach the top-level.
-- see Note [Overview of implicit CallStacks]
-> str `elem` givenStks
-> False
| isIPClass cls -> True -- See note [Inheriting implicit parameters]
......@@ -1867,9 +1867,6 @@ pickQuantifiablePreds qtvs annotated_theta theta
EqPred NomEq ty1 ty2 -> quant_fun ty1 || quant_fun ty2
IrredPred ty -> tyCoVarsOfType ty `intersectsVarSet` qtvs
givenStks = [ str | (str, ty) <- mapMaybe isIPPred_maybe annotated_theta
, isCallStackTy ty ]
pick_cls_pred flex_ctxt cls tys
= tyCoVarsOfTypes tys `intersectsVarSet` qtvs
&& (checkValidClsArgs flex_ctxt cls tys)
......@@ -1883,6 +1880,19 @@ pickQuantifiablePreds qtvs annotated_theta theta
-> tyCoVarsOfTypes tys `intersectsVarSet` qtvs
_ -> False
pickCapturedPreds
:: TyVarSet -- Quantifying over these
-> TcThetaType -- Proposed constraints to quantify
-> TcThetaType -- A subset that we can actually quantify
-- A simpler version of pickQuantifiablePreds, used to winnow down
-- the inferred constrains of a group of bindings, into those for
-- one particular identifier
pickCapturedPreds qtvs theta
= filter captured theta
where
captured pred = isIPPred pred || (tyCoVarsOfType pred `intersectsVarSet` qtvs)
-- Superclasses
type PredWithSCs = (PredType, [PredType])
......
{-# LANGUAGE PartialTypeSignatures, NamedWildCards #-}
module SuperCls where
f :: (Ord a, _) => a -> Bool
-- We'd like to see that the wildcard _ unifies with ()
f x = x == x
SuperCls.hs:4:14: warning: [-Wpartial-type-signatures (in -Wdefault)]
Found constraint wildcard ‘_’ standing for ‘()’
In the type signature: f :: (Ord a, _) => a -> Bool
TYPE SIGNATURES
bar :: forall t t1. t1 -> (t1 -> t) -> t
foo :: forall a. (Show a, Enum a) => a -> String
TYPE CONSTRUCTORS
COERCION AXIOMS
Dependent modules: []
Dependent packages: [base-4.9.0.0, ghc-prim-0.5.0.0,
integer-gmp-1.0.0.1]
WarningWildcardInstantiations.hs:5:14: warning: [-Wpartial-type-signatures (in -Wdefault)]
• Found type wildcard ‘_a’ standing for ‘a’
Where: ‘a’ is a rigid type variable bound by
the inferred type of foo :: (Enum a, Show a) => a -> String
at WarningWildcardInstantiations.hs:6:1
• In the type signature: foo :: (Show _a, _) => _a -> _
• Relevant bindings include
foo :: a -> String (bound at WarningWildcardInstantiations.hs:6:1)
WarningWildcardInstantiations.hs:5:18: warning: [-Wpartial-type-signatures (in -Wdefault)]
Found constraint wildcard ‘_’ standing for ‘Enum a’
In the type signature: foo :: (Show _a, _) => _a -> _
WarningWildcardInstantiations.hs:5:30: warning: [-Wpartial-type-signatures (in -Wdefault)]
• Found type wildcard ‘_’ standing for ‘String’
• In the type signature: foo :: (Show _a, _) => _a -> _
• Relevant bindings include
foo :: a -> String (bound at WarningWildcardInstantiations.hs:6:1)
WarningWildcardInstantiations.hs:8:8: warning: [-Wpartial-type-signatures (in -Wdefault)]
• Found type wildcard ‘_’ standing for ‘t1’
Where: ‘t1’ is a rigid type variable bound by
the inferred type of bar :: t1 -> (t1 -> t) -> t
at WarningWildcardInstantiations.hs:9:1
• In the type signature: bar :: _ -> _ -> _
• Relevant bindings include
bar :: t1 -> (t1 -> t) -> t
(bound at WarningWildcardInstantiations.hs:9:1)
WarningWildcardInstantiations.hs:8:13: warning: [-Wpartial-type-signatures (in -Wdefault)]
• Found type wildcard ‘_’ standing for ‘t1 -> t’
Where: ‘t’ is a rigid type variable bound by
the inferred type of bar :: t1 -> (t1 -> t) -> t
at WarningWildcardInstantiations.hs:9:1
‘t1’ is a rigid type variable bound by
the inferred type of bar :: t1 -> (t1 -> t) -> t
at WarningWildcardInstantiations.hs:9:1
• In the type signature: bar :: _ -> _ -> _
• Relevant bindings include
bar :: t1 -> (t1 -> t) -> t
(bound at WarningWildcardInstantiations.hs:9:1)
WarningWildcardInstantiations.hs:8:18: warning: [-Wpartial-type-signatures (in -Wdefault)]
• Found type wildcard ‘_’ standing for ‘t’
Where: ‘t’ is a rigid type variable bound by
the inferred type of bar :: t1 -> (t1 -> t) -> t
at WarningWildcardInstantiations.hs:9:1
• In the type signature: bar :: _ -> _ -> _
• Relevant bindings include
bar :: t1 -> (t1 -> t) -> t
(bound at WarningWildcardInstantiations.hs:9:1)
TYPE SIGNATURES
bar :: forall t t1. t1 -> (t1 -> t) -> t
foo :: forall a. (Show a, Enum a) => a -> String
TYPE CONSTRUCTORS
COERCION AXIOMS
Dependent modules: []
Dependent packages: [base-4.9.0.0, ghc-prim-0.5.0.0,
integer-gmp-1.0.0.1]
WarningWildcardInstantiations.hs:5:14: warning: [-Wpartial-type-signatures (in -Wdefault)]
• Found type wildcard ‘_a’ standing for ‘a’
Where: ‘a’ is a rigid type variable bound by
the inferred type of foo :: (Show a, Enum a) => a -> String
at WarningWildcardInstantiations.hs:6:1
• In the type signature: foo :: (Show _a, _) => _a -> _
• Relevant bindings include
foo :: a -> String (bound at WarningWildcardInstantiations.hs:6:1)
WarningWildcardInstantiations.hs:5:18: warning: [-Wpartial-type-signatures (in -Wdefault)]
Found constraint wildcard ‘_’ standing for ‘Enum a’
In the type signature: foo :: (Show _a, _) => _a -> _
WarningWildcardInstantiations.hs:5:30: warning: [-Wpartial-type-signatures (in -Wdefault)]
• Found type wildcard ‘_’ standing for ‘String’
• In the type signature: foo :: (Show _a, _) => _a -> _
• Relevant bindings include
foo :: a -> String (bound at WarningWildcardInstantiations.hs:6:1)
WarningWildcardInstantiations.hs:8:8: warning: [-Wpartial-type-signatures (in -Wdefault)]
• Found type wildcard ‘_’ standing for ‘t1’
Where: ‘t1’ is a rigid type variable bound by
the inferred type of bar :: t1 -> (t1 -> t) -> t
at WarningWildcardInstantiations.hs:9:1
• In the type signature: bar :: _ -> _ -> _
• Relevant bindings include
bar :: t1 -> (t1 -> t) -> t
(bound at WarningWildcardInstantiations.hs:9:1)
WarningWildcardInstantiations.hs:8:13: warning: [-Wpartial-type-signatures (in -Wdefault)]
• Found type wildcard ‘_’ standing for ‘t1 -> t’
Where: ‘t’ is a rigid type variable bound by
the inferred type of bar :: t1 -> (t1 -> t) -> t
at WarningWildcardInstantiations.hs:9:1
‘t1’ is a rigid type variable bound by
the inferred type of bar :: t1 -> (t1 -> t) -> t
at WarningWildcardInstantiations.hs:9:1
• In the type signature: bar :: _ -> _ -> _
• Relevant bindings include
bar :: t1 -> (t1 -> t) -> t
(bound at WarningWildcardInstantiations.hs:9:1)
WarningWildcardInstantiations.hs:8:18: warning: [-Wpartial-type-signatures (in -Wdefault)]
• Found type wildcard ‘_’ standing for ‘t’
Where: ‘t’ is a rigid type variable bound by
the inferred type of bar :: t1 -> (t1 -> t) -> t
at WarningWildcardInstantiations.hs:9:1
• In the type signature: bar :: _ -> _ -> _
• Relevant bindings include
bar :: t1 -> (t1 -> t) -> t
(bound at WarningWildcardInstantiations.hs:9:1)
......@@ -60,3 +60,4 @@ test('T10463', normal, compile, [''])
test('ExprSigLocal', normal, compile, [''])
test('T11016', normal, compile, [''])
test('T11192', normal, compile, [''])
test('SuperCls', normal, compile, [''])
\ No newline at end of file
WildcardInstantiations.hs:5:14: error:
• Found type wildcard ‘_a’ standing for ‘a’
Where: ‘a’ is a rigid type variable bound by
the inferred type of foo :: (Enum a, Show a) => a -> String
at WildcardInstantiations.hs:6:1
To use the inferred type, enable PartialTypeSignatures
• In the type signature: foo :: (Show _a, _) => _a -> _
• Relevant bindings include
foo :: a -> String (bound at WildcardInstantiations.hs:6:1)
WildcardInstantiations.hs:5:18: error:
Found constraint wildcard ‘_’ standing for ‘Enum a’
To use the inferred type, enable PartialTypeSignatures
In the type signature: foo :: (Show _a, _) => _a -> _
WildcardInstantiations.hs:5:30: error:
• Found type wildcard ‘_’ standing for ‘String’
To use the inferred type, enable PartialTypeSignatures
• In the type signature: foo :: (Show _a, _) => _a -> _
• Relevant bindings include
foo :: a -> String (bound at WildcardInstantiations.hs:6:1)
WildcardInstantiations.hs:8:8: error:
• Found type wildcard ‘_’ standing for ‘t1’
Where: ‘t1’ is a rigid type variable bound by
the inferred type of bar :: t1 -> (t1 -> t) -> t
at WildcardInstantiations.hs:9:1
To use the inferred type, enable PartialTypeSignatures
• In the type signature: bar :: _ -> _ -> _
• Relevant bindings include
bar :: t1 -> (t1 -> t) -> t
(bound at WildcardInstantiations.hs:9:1)
WildcardInstantiations.hs:8:13: error:
• Found type wildcard ‘_’ standing for ‘t1 -> t’
Where: ‘t’ is a rigid type variable bound by
the inferred type of bar :: t1 -> (t1 -> t) -> t
at WildcardInstantiations.hs:9:1
‘t1’ is a rigid type variable bound by
the inferred type of bar :: t1 -> (t1 -> t) -> t
at WildcardInstantiations.hs:9:1
To use the inferred type, enable PartialTypeSignatures
• In the type signature: bar :: _ -> _ -> _
• Relevant bindings include
bar :: t1 -> (t1 -> t) -> t
(bound at WildcardInstantiations.hs:9:1)
WildcardInstantiations.hs:8:18: error:
• Found type wildcard ‘_’ standing for ‘t’
Where: ‘t’ is a rigid type variable bound by
the inferred type of bar :: t1 -> (t1 -> t) -> t
at WildcardInstantiations.hs:9:1
To use the inferred type, enable PartialTypeSignatures
• In the type signature: bar :: _ -> _ -> _
• Relevant bindings include
bar :: t1 -> (t1 -> t) -> t
(bound at WildcardInstantiations.hs:9:1)
WildcardInstantiations.hs:5:14: error:
• Found type wildcard ‘_a’ standing for ‘a’
Where: ‘a’ is a rigid type variable bound by
the inferred type of foo :: (Show a, Enum a) => a -> String
at WildcardInstantiations.hs:6:1
To use the inferred type, enable PartialTypeSignatures
• In the type signature: foo :: (Show _a, _) => _a -> _
• Relevant bindings include
foo :: a -> String (bound at WildcardInstantiations.hs:6:1)
WildcardInstantiations.hs:5:18: error:
Found constraint wildcard ‘_’ standing for ‘Enum a’
To use the inferred type, enable PartialTypeSignatures
In the type signature: foo :: (Show _a, _) => _a -> _
WildcardInstantiations.hs:5:30: error:
• Found type wildcard ‘_’ standing for ‘String’
To use the inferred type, enable PartialTypeSignatures
• In the type signature: foo :: (Show _a, _) => _a -> _
• Relevant bindings include
foo :: a -> String (bound at WildcardInstantiations.hs:6:1)
WildcardInstantiations.hs:8:8: error:
• Found type wildcard ‘_’ standing for ‘t1’
Where: ‘t1’ is a rigid type variable bound by
the inferred type of bar :: t1 -> (t1 -> t) -> t
at WildcardInstantiations.hs:9:1
To use the inferred type, enable PartialTypeSignatures
• In the type signature: bar :: _ -> _ -> _
• Relevant bindings include
bar :: t1 -> (t1 -> t) -> t
(bound at WildcardInstantiations.hs:9:1)
WildcardInstantiations.hs:8:13: error:
• Found type wildcard ‘_’ standing for ‘t1 -> t’
Where: ‘t’ is a rigid type variable bound by
the inferred type of bar :: t1 -> (t1 -> t) -> t
at WildcardInstantiations.hs:9:1
‘t1’ is a rigid type variable bound by
the inferred type of bar :: t1 -> (t1 -> t) -> t
at WildcardInstantiations.hs:9:1
To use the inferred type, enable PartialTypeSignatures
• In the type signature: bar :: _ -> _ -> _
• Relevant bindings include
bar :: t1 -> (t1 -> t) -> t
(bound at WildcardInstantiations.hs:9:1)
WildcardInstantiations.hs:8:18: error:
• Found type wildcard ‘_’ standing for ‘t’
Where: ‘t’ is a rigid type variable bound by
the inferred type of bar :: t1 -> (t1 -> t) -> t
at WildcardInstantiations.hs:9:1
To use the inferred type, enable PartialTypeSignatures
• In the type signature: bar :: _ -> _ -> _
• Relevant bindings include
bar :: t1 -> (t1 -> t) -> t
(bound at WildcardInstantiations.hs:9:1)
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