-----------------------------------------
-Choosing Q
-~~~~~~~~~~
+Note [Choosing which variables to quantify]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Here's a good way to choose Q:
Q = grow( fv(T), C ) \ oclose( fv(G), C )
; gbl_tvs <- tcGetGlobalTyVars
; let preds = fdPredsOfInsts wanted'
qtvs = grow preds tau_tvs' `minusVarSet` oclose preds gbl_tvs
- (free, bound) = partition (isFreeWhenInferring qtvs) wanted'
- ; traceTc (text "infer" <+> (ppr preds $$ ppr (grow preds tau_tvs') $$ ppr gbl_tvs $$ ppr (oclose preds gbl_tvs) $$ ppr free $$ ppr bound))
- ; extendLIEs free
+ -- See Note [Choosing which variables to quantify]
+
+ -- To maximise sharing, remove from consideration any
+ -- constraints that don't mention qtvs at all
+ ; let (free1, bound) = partition (isFreeWhenInferring qtvs) wanted'
+ ; extendLIEs free1
-- To make types simple, reduce as much as possible
+ ; traceTc (text "infer" <+> (ppr preds $$ ppr (grow preds tau_tvs') $$ ppr gbl_tvs $$
+ ppr (oclose preds gbl_tvs) $$ ppr free1 $$ ppr bound))
; let try_me inst = ReduceMe AddSCs
; (irreds, binds) <- checkLoop (mkRedEnv doc try_me []) bound
-
; qtvs' <- zonkQuantifiedTyVars (varSetElems qtvs)
- -- We can't abstract over implications
- ; let (dicts, implics) = partition isDict irreds
+ -- Do not quantify over constraints that *now* do not
+ -- mention quantified type variables, because they are
+ -- simply ambiguous. Example:
+ -- f :: Eq b => a -> (a, b)
+ -- g x = fst (f x)
+ -- From the RHS of g we get the MethodInst f77 :: alpha -> (alpha, beta)
+ -- We decide to quantify over 'alpha' alone, bur free1 does not include f77
+ -- because f77 mentions 'alpha'. Then reducing leaves only the (ambiguous)
+ -- constraint (Eq beta), which we dump back into the free set
+ -- See test tcfail181
+ ; let (free2, irreds2) = partition (isFreeWhenInferring (mkVarSet qtvs')) irreds
+ ; extendLIEs free2
+
+ -- We can't abstract over implications
+ ; let (dicts, implics) = partition isDict irreds2
; loc <- getInstLoc (ImplicOrigin doc)
; implic_bind <- bindIrreds loc qtvs' dicts implics
| otherwise -- Otherwise we must generate a binding
= do { uniq <- newUnique
; span <- getSrcSpanM
- ; let name = mkInternalName uniq (mkVarOcc "ic") (srcSpanStart span)
+ ; let name = mkInternalName uniq (mkVarOcc "ic") span
implic_inst = ImplicInst { tci_name = name, tci_reft = reft,
tci_tyvars = all_tvs,
tci_given = givens,
; gbl_tvs' <- tcGetGlobalTyVars
; constrained_dicts' <- mappM zonkInst constrained_dicts
- ; let constrained_tvs' = tyVarsOfInsts constrained_dicts'
- qtvs = (tau_tvs' `minusVarSet` oclose (fdPredsOfInsts constrained_dicts) gbl_tvs')
- `minusVarSet` constrained_tvs'
+ ; let qtvs1 = tau_tvs' `minusVarSet` oclose (fdPredsOfInsts constrained_dicts) gbl_tvs'
+ -- As in tcSimplifyInfer
+
+ -- Do not quantify over constrained type variables:
+ -- this is the monomorphism restriction
+ constrained_tvs' = tyVarsOfInsts constrained_dicts'
+ qtvs = qtvs1 `minusVarSet` constrained_tvs'
+ pp_bndrs = pprWithCommas (quotes . ppr) bndrs
+
+ -- Warn in the mono
+ ; warn_mono <- doptM Opt_WarnMonomorphism
+ ; warnTc (warn_mono && (constrained_tvs' `intersectsVarSet` qtvs1))
+ (vcat[ ptext SLIT("the Monomorphism Restriction applies to the binding")
+ <> plural bndrs <+> ptext SLIT("for") <+> pp_bndrs,
+ ptext SLIT("Consider giving a type signature for") <+> pp_bndrs])
+
; traceTc (text "tcSimplifyRestricted" <+> vcat [
pprInsts wanteds, pprInsts constrained_dicts',
ppr _binds,
getDefaultTys :: Bool -> Bool -> TcM [Type]
getDefaultTys extended_deflts ovl_strings
= do { mb_defaults <- getDeclaredDefaultTys
- ; case mb_defaults of
- Just tys -> return tys -- User-supplied defaults
+ ; case mb_defaults of {
+ Just tys -> return tys ; -- User-supplied defaults
Nothing -> do
-- No use-supplied default
++
[integer_ty,doubleTy]
++
- opt_deflt ovl_strings string_ty) }}
+ opt_deflt ovl_strings string_ty) } } }
where
opt_deflt True ty = [ty]
opt_deflt False ty = []
quotes (pprWithCommas ppr (varSetElems (tyVarsOfInst dict))),
ptext SLIT("Use -fallow-incoherent-instances to use the first choice above")])]
where
- ispecs = [ispec | (_, ispec) <- matches]
+ ispecs = [ispec | (ispec, _) <- matches]
mk_no_inst_err insts
| null insts = empty
= findGlobals (mkVarSet inst_tvs) tidy_env `thenM` \ (tidy_env, docs) ->
returnM (tidy_env, mk_msg docs)
where
+ mk_msg _ | any isRuntimeUnk inst_tvs
+ = vcat [ptext SLIT("Cannot resolve unknown runtime types:") <+>
+ (pprWithCommas ppr inst_tvs),
+ ptext SLIT("Use :print or :force to determine these types")]
mk_msg [] = ptext SLIT("Probable fix: add a type signature that fixes these type variable(s)")
-- This happens in things like
-- f x = show (read "foo")
nest 2 (vcat docs),
monomorphism_fix
]
+
+isRuntimeUnk :: TcTyVar -> Bool
+isRuntimeUnk x | SkolemTv RuntimeUnkSkol <- tcTyVarDetails x = True
+ | otherwise = False
+
monomorphism_fix :: SDoc
monomorphism_fix = ptext SLIT("Probable fix:") <+>
(ptext SLIT("give these definition(s) an explicit type signature")