Commit 452755de authored by Simon Peyton Jones's avatar Simon Peyton Jones

Do not discard insolubles in implications

Trac #14000 showed up two errors

* In TcRnTypes.dropInsolubles we dropped all implications, which
  might contain the very insolubles we wanted to keep.  This was
  an outright error, and is why the out-of-scope error was actually
  lost altogether in Trac #14000

* In TcSimplify.simplifyInfer, if there are definite (insoluble)
  errors, it's better to suppress the following ambiguity test,
  because the type may be bogus anyway.  See TcSimplify
  Note [Quantification with errors].  This fix seems a bit clunky,
  but it'll do for now.
parent b1317a35
......@@ -787,12 +787,12 @@ tcPolyInfer rec_tc prag_fn tc_sig_fn mono bind_list
; mapM_ (checkOverloadedSig mono) sigs
; traceTc "simplifyInfer call" (ppr tclvl $$ ppr name_taus $$ ppr wanted)
; (qtvs, givens, ev_binds)
; (qtvs, givens, ev_binds, insoluble)
<- simplifyInfer tclvl infer_mode sigs name_taus wanted
; let inferred_theta = map evVarPred givens
; exports <- checkNoErrs $
mapM (mkExport prag_fn qtvs inferred_theta) mono_infos
mapM (mkExport prag_fn insoluble qtvs inferred_theta) mono_infos
; loc <- getSrcSpanM
; let poly_ids = map abe_poly exports
......@@ -807,6 +807,8 @@ tcPolyInfer rec_tc prag_fn tc_sig_fn mono bind_list
--------------
mkExport :: TcPragEnv
-> Bool -- True <=> there was an insoluble type error
-- when typechecking the bindings
-> [TyVar] -> TcThetaType -- Both already zonked
-> MonoBindInfo
-> TcM (ABExport GhcTc)
......@@ -823,12 +825,12 @@ mkExport :: TcPragEnv
-- Pre-condition: the qtvs and theta are already zonked
mkExport prag_fn qtvs theta
mkExport prag_fn insoluble qtvs theta
mono_info@(MBI { mbi_poly_name = poly_name
, mbi_sig = mb_sig
, mbi_mono_id = mono_id })
= do { mono_ty <- zonkTcType (idType mono_id)
; poly_id <- mkInferredPolyId qtvs theta poly_name mb_sig mono_ty
; poly_id <- mkInferredPolyId insoluble qtvs theta poly_name mb_sig mono_ty
-- NB: poly_id has a zonked type
; poly_id <- addInlinePrags poly_id prag_sigs
......@@ -863,10 +865,12 @@ mkExport prag_fn qtvs theta
prag_sigs = lookupPragEnv prag_fn poly_name
sig_ctxt = InfSigCtxt poly_name
mkInferredPolyId :: [TyVar] -> TcThetaType
mkInferredPolyId :: Bool -- True <=> there was an insoluble error when
-- checking the binding group for this Id
-> [TyVar] -> TcThetaType
-> Name -> Maybe TcIdSigInst -> TcType
-> TcM TcId
mkInferredPolyId qtvs inferred_theta poly_name mb_sig_inst mono_ty
mkInferredPolyId insoluble qtvs inferred_theta poly_name mb_sig_inst mono_ty
| Just (TISI { sig_inst_sig = sig }) <- mb_sig_inst
, CompleteSig { sig_bndr = poly_id } <- sig
= return poly_id
......@@ -894,9 +898,13 @@ mkInferredPolyId qtvs inferred_theta poly_name mb_sig_inst mono_ty
; traceTc "mkInferredPolyId" (vcat [ppr poly_name, ppr qtvs, ppr theta'
, ppr inferred_poly_ty])
; addErrCtxtM (mk_inf_msg poly_name inferred_poly_ty) $
; unless insoluble $
addErrCtxtM (mk_inf_msg poly_name inferred_poly_ty) $
checkValidType (InfSigCtxt poly_name) inferred_poly_ty
-- See Note [Validity of inferred types]
-- If we found an insoluble error in the function definition, don't
-- do this check; otherwise (Trac #14000) we may report an ambiguity
-- error for a rather bogus type.
; return (mkLocalIdOrCoVar poly_name inferred_poly_ty) }
......
......@@ -1561,7 +1561,7 @@ tcExprSig expr sig@(PartialSig { psig_name = name, sig_loc = loc })
= ApplyMR
| otherwise
= NoRestrictions
; (qtvs, givens, ev_binds)
; (qtvs, givens, ev_binds, _)
<- simplifyInfer tclvl infer_mode [sig_inst] [(name, tau)] wanted
; tau <- zonkTcType tau
; let inferred_theta = map evVarPred givens
......
......@@ -80,8 +80,8 @@ tcInferPatSynDecl PSB{ psb_id = lname@(L _ name), psb_args = details,
; let named_taus = (name, pat_ty) : map (\arg -> (getName arg, varType arg)) args
; (qtvs, req_dicts, ev_binds) <- simplifyInfer tclvl NoRestrictions []
named_taus wanted
; (qtvs, req_dicts, ev_binds, _) <- simplifyInfer tclvl NoRestrictions []
named_taus wanted
; let (ex_tvs, prov_dicts) = tcCollectEx lpat'
ex_tv_set = mkVarSet ex_tvs
......
......@@ -2191,9 +2191,9 @@ tcRnExpr hsc_env mode rdr_expr
else return expr_ty } ;
-- Generalise
((qtvs, dicts, _), lie_top) <- captureTopConstraints $
{-# SCC "simplifyInfer" #-}
simplifyInfer tclvl
((qtvs, dicts, _, _), lie_top) <- captureTopConstraints $
{-# SCC "simplifyInfer" #-}
simplifyInfer tclvl
infer_mode
[] {- No sig vars -}
[(fresh_it, res_ty)]
......
......@@ -2254,7 +2254,13 @@ getInsolubles = wc_insol
insolublesOnly :: WantedConstraints -> WantedConstraints
-- Keep only the insolubles
insolublesOnly wc = wc { wc_simple = emptyBag, wc_impl = emptyBag }
insolublesOnly (WC { wc_insol = insols, wc_impl = implics })
= WC { wc_simple = emptyBag
, wc_insol = insols
, wc_impl = mapBag implic_insols_only implics }
where
implic_insols_only implic
= implic { ic_wanted = insolublesOnly (ic_wanted implic) }
dropDerivedWC :: WantedConstraints -> WantedConstraints
-- See Note [Dropping derived constraints]
......
......@@ -22,6 +22,7 @@ import Class ( Class, classKey, classTyCon )
import DynFlags ( WarningFlag ( Opt_WarnMonomorphism )
, WarnReason ( Reason )
, DynFlags( solverIterations ) )
import Id ( idType )
import Inst
import ListSetOps
import Maybes
......@@ -576,14 +577,16 @@ simplifyInfer :: TcLevel -- Used when generating the constraints
-> WantedConstraints
-> TcM ([TcTyVar], -- Quantify over these type variables
[EvVar], -- ... and these constraints (fully zonked)
TcEvBinds) -- ... binding these evidence variables
TcEvBinds, -- ... binding these evidence variables
Bool) -- True <=> there was an insoluble type error
-- in these bindings
simplifyInfer rhs_tclvl infer_mode sigs name_taus wanteds
| isEmptyWC wanteds
= do { gbl_tvs <- tcGetGlobalTyCoVars
; dep_vars <- zonkTcTypesAndSplitDepVars (map snd name_taus)
; qtkvs <- quantifyTyVars gbl_tvs dep_vars
; traceTc "simplifyInfer: empty WC" (ppr name_taus $$ ppr qtkvs)
; return (qtkvs, [], emptyTcEvBinds) }
; return (qtkvs, [], emptyTcEvBinds, False) }
| otherwise
= do { traceTc "simplifyInfer {" $ vcat
......@@ -618,26 +621,24 @@ simplifyInfer rhs_tclvl infer_mode sigs name_taus wanteds
; wanteds' <- solveWanteds wanteds
; TcS.zonkWC wanteds' }
-- Find quant_pred_candidates, the predicates that
-- we'll consider quantifying over
-- NB1: wanted_transformed does not include anything provable from
-- the psig_theta; it's just the extra bit
-- NB2: We do not do any defaulting when inferring a type, this can lead
-- to less polymorphic types, see Note [Default while Inferring]
; let wanted_transformed = dropDerivedWC wanted_transformed_incl_derivs
quant_pred_candidates -- Fully zonked
| insolubleWC wanted_transformed_incl_derivs
= [] -- See Note [Quantification with errors]
-- NB: must include derived errors in this test,
-- hence "incl_derivs"
| otherwise
= ctsPreds (approximateWC False wanted_transformed)
-- NB: quant_pred_candidates is already fully zonked
; let definite_error = insolubleWC wanted_transformed_incl_derivs
-- See Note [Quantification with errors]
-- NB: must include derived errors in this test,
-- hence "incl_derivs"
wanted_transformed = dropDerivedWC wanted_transformed_incl_derivs
quant_pred_candidates
| definite_error = []
| otherwise = ctsPreds (approximateWC False wanted_transformed)
-- Decide what type variables and constraints to quantify
-- NB: quant_pred_candidates is already fully zonked
-- NB: bound_theta are constraints we want to quantify over,
-- /apart from/ the psig_theta, which we always quantify over
; (qtvs, bound_theta) <- decideQuantification infer_mode rhs_tclvl
......@@ -648,41 +649,58 @@ simplifyInfer rhs_tclvl infer_mode sigs name_taus wanteds
-- remaining constraints from the RHS.
-- We must retain the psig_theta_vars, because we've used them in
-- evidence bindings constructed by solveWanteds earlier
; psig_theta_vars <- mapM zonkId psig_theta_vars
; psig_theta_vars <- mapM zonkId psig_theta_vars
; bound_theta_vars <- mapM TcM.newEvVar bound_theta
; let full_theta = psig_theta ++ bound_theta
full_theta_vars = psig_theta_vars ++ bound_theta_vars
skol_info = InferSkol [ (name, mkSigmaTy [] full_theta ty)
| (name, ty) <- name_taus ]
-- Don't add the quantified variables here, because
-- they are also bound in ic_skols and we want them
-- to be tidied uniformly
; let full_theta_vars = psig_theta_vars ++ bound_theta_vars
implic = Implic { ic_tclvl = rhs_tclvl
, ic_skols = qtvs
, ic_no_eqs = False
, ic_given = full_theta_vars
, ic_wanted = wanted_transformed
, ic_status = IC_Unsolved
, ic_binds = ev_binds_var
, ic_info = skol_info
, ic_needed = emptyVarSet
, ic_env = tc_lcl_env }
; emitImplication implic
; emitResidualImplication rhs_tclvl tc_lcl_env ev_binds_var
name_taus qtvs full_theta_vars
wanted_transformed
-- All done!
; traceTc "} simplifyInfer/produced residual implication for quantification" $
vcat [ text "quant_pred_candidates =" <+> ppr quant_pred_candidates
, text "psig_theta =" <+> ppr psig_theta
, text "bound_theta =" <+> ppr bound_theta
, text "full_theta =" <+> ppr full_theta
, text "full_theta =" <+> ppr (map idType full_theta_vars)
, text "qtvs =" <+> ppr qtvs
, text "implic =" <+> ppr implic ]
, text "definite_error =" <+> ppr definite_error ]
; return ( qtvs, full_theta_vars, TcEvBinds ev_binds_var ) }
; return ( qtvs, full_theta_vars, TcEvBinds ev_binds_var, definite_error ) }
-- NB: full_theta_vars must be fully zonked
--------------------
emitResidualImplication :: TcLevel -> TcLclEnv -> EvBindsVar
-> [(Name, TcTauType)] -> [TcTyVar] -> [EvVar]
-> WantedConstraints -> TcM ()
emitResidualImplication rhs_tclvl tc_lcl_env ev_binds_var
name_taus qtvs full_theta_vars wanteds
| isEmptyWC wanteds
= return ()
| otherwise
= do { traceTc "emitResidualImplication" (ppr implic)
; emitImplication implic }
where
implic = Implic { ic_tclvl = rhs_tclvl
, ic_skols = qtvs
, ic_no_eqs = False
, ic_given = full_theta_vars
, ic_wanted = wanteds
, ic_status = IC_Unsolved
, ic_binds = ev_binds_var
, ic_info = skol_info
, ic_needed = emptyVarSet
, ic_env = tc_lcl_env }
full_theta = map idType full_theta_vars
skol_info = InferSkol [ (name, mkSigmaTy [] full_theta ty)
| (name, ty) <- name_taus ]
-- Don't add the quantified variables here, because
-- they are also bound in ic_skols and we want them
-- to be tidied uniformly
--------------------
ctsPreds :: Cts -> [PredType]
ctsPreds cts = [ ctEvPred ev | ct <- bagToList cts
, let ev = ctEvidence ct ]
......@@ -1092,13 +1110,33 @@ Notice that
Note [Quantification with errors]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
If we find that the RHS of the definition has some absolutely-insoluble
constraints, we abandon all attempts to find a context to quantify
over, and instead make the function fully-polymorphic in whatever
type we have found. For two reasons
a) Minimise downstream errors
b) Avoid spurious errors from this function
But NB that we must include *derived* errors in the check. Example:
constraints (including especially "variable not in scope"), we
* Abandon all attempts to find a context to quantify over,
and instead make the function fully-polymorphic in whatever
type we have found
* Return a flag from simplifyInfer, indicating that we found an
insoluble constraint. This flag is used to suppress the ambiguity
check for the inferred type, which may well be bogus, and which
tends to obscure the real error. This fix feels a bit clunky,
but I failed to come up with anything better.
Reasons:
- Avoid downstream errors
- Do not perform an ambiguity test on a bogus type, which might well
fail spuriously, thereby obfuscating the original insoluble error.
Trac #14000 is an example
I tried an alterantive approach: simply failM, after emitting the
residual implication constraint; the exception will be caught in
TcBinds.tcPolyBinds, which gives all the binders in the group the type
(forall a. a). But that didn't work with -fdefer-type-errors, because
the recovery from failM emits no code at all, so there is no function
to run! But -fdefer-type-errors aspires to produce a runnable program.
NB that we must include *derived* errors in the check for insolubles.
Example:
(a::*) ~ Int#
We get an insoluble derived error *~#, and we don't want to discard
it before doing the isInsolubleWC test! (Trac #8262)
......
......@@ -8,4 +8,4 @@ x (+) ((&)@z) ((:&&) a b) (c :&& d) (e `A` f) (A g h) = y
y _ = (&)
{-# INLINE (&) #-}
{-# SPECIALIZE (&) :: a #-}
(&) = x
(&) = 'c'
T7848.hs:6:1: error:
• Occurs check: cannot construct the infinite type:
t ~ p0 -> p1 -> A -> A -> A -> A -> p2 -> t
• Relevant bindings include x :: t (bound at T7848.hs:6:1)
T7848.hs:10:9: error:
• Couldn't match expected type ‘t’ with actual type ‘a’
because type variable ‘a’ would escape its scope
This (rigid, skolem) type variable is bound by
• Couldn't match expected type ‘Char’ with actual type ‘a’
‘a’ is a rigid type variable bound by
the type signature for:
(&) :: forall a. a
at T7848.hs:10:9-35
......@@ -20,5 +14,4 @@ T7848.hs:10:9: error:
y _ = (&)
{-# INLINE (&) #-}
{-# SPECIALIZE (&) :: a #-}
(&) = x
• Relevant bindings include x :: t (bound at T7848.hs:6:1)
(&) = 'c'
T5358.hs:10:13: error:
• Couldn't match expected type ‘t -> a0’ with actual type ‘Int’
• The function ‘T5358.t1’ is applied to one argument,
but its type ‘Int’ has none
In the first argument of ‘(==)’, namely ‘T5358.t1 x’
In the expression: T5358.t1 x == T5358.t2 x
• Relevant bindings include
x :: t (bound at T5358.hs:10:9)
T5358.prop_x1 :: t -> Bool (bound at T5358.hs:10:1)
T5358.hs:10:21: error:
• Couldn't match expected type ‘t -> a0’ with actual type ‘Int’
• The function ‘T5358.t2’ is applied to one argument,
but its type ‘Int’ has none
In the second argument of ‘(==)’, namely ‘T5358.t2 x’
In the expression: T5358.t1 x == T5358.t2 x
• Relevant bindings include
x :: t (bound at T5358.hs:10:9)
T5358.prop_x1 :: t -> Bool (bound at T5358.hs:10:1)
T5358.hs:14:12: error:
• Exception when trying to run compile-time code:
runTest called error: forall (t_0 :: *) . t_0 -> GHC.Types.Bool
......
{-# LANGUAGE TypeFamilies #-}
module T14000 where
class C a where
type T a
c :: a -> T a
foo = c noSuchThing -- noSuchThing is not in scope
T14000.hs:8:9: error: Variable not in scope: noSuchThing
T8142.hs:6:18: error:
• Couldn't match type ‘Nu g0’ with ‘Nu g
Expected type: Nu ((,) a) -> Nu g
T8142.hs:6:10: error:
• Couldn't match type ‘Nu ((,) a0)’ with ‘c -> f c
Expected type: (c -> f c) -> c -> f c
Actual type: Nu ((,) a0) -> Nu g0
NB: ‘Nu’ is a type function, and may not be injective
The type variable ‘g0’ is ambiguous
• In the ambiguity check for the inferred type for ‘h’
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
When checking the inferred type
h :: forall a (g :: * -> *). Nu ((,) a) -> Nu g
The type variable ‘a0’ is ambiguous
• In the expression: h
In an equation for ‘tracer’:
tracer
= h
where
h = (\ (_, b) -> ((outI . fmap h) b)) . out
• Relevant bindings include
tracer :: (c -> f c) -> c -> f c (bound at T8142.hs:6:1)
T8142.hs:6:57: error:
• Couldn't match type ‘Nu ((,) a)’ with ‘g (Nu ((,) a))’
Expected type: Nu ((,) a) -> (a, g (Nu ((,) a)))
Actual type: Nu ((,) a) -> (a, Nu ((,) a))
• In the second argument of ‘(.)’, namely ‘out’
In the expression: (\ (_, b) -> ((outI . fmap h) b)) . out
In an equation for ‘h’: h = (\ (_, b) -> ((outI . fmap h) b)) . out
• Relevant bindings include
h :: Nu ((,) a) -> Nu g (bound at T8142.hs:6:18)
......@@ -452,3 +452,4 @@ test('T13610', normal, compile_fail, [''])
test('T11672', normal, compile_fail, [''])
test('T13819', normal, compile_fail, [''])
test('T11963', normal, compile_fail, [''])
test('T14000', 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