-----------------------------------------
-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
+ red_env = mkRedEnv doc try_me []
+ ; (irreds1, binds1) <- checkLoop red_env bound
+
+ -- Note [Inference and implication constraints]
+ -- By putting extra_dicts first, we make them available
+ -- to solve the implication constraints
+ ; let extra_dicts = getImplicWanteds qtvs irreds1
+ ; (irreds2, binds2) <- if null extra_dicts
+ then return (irreds1, emptyBag)
+ else do { extra_dicts' <- mapM cloneDict extra_dicts
+ ; checkLoop red_env (extra_dicts' ++ irreds1) }
+
+ -- By now improvment may have taken place, and we must *not*
+ -- quantify over any variable free in the environment
+ -- tc137 (function h inside g) is an example
+ ; gbl_tvs <- tcGetGlobalTyVars
+ ; qtvs1 <- zonkTcTyVarsAndFV (varSetElems qtvs)
+ ; qtvs2 <- zonkQuantifiedTyVars (varSetElems (qtvs1 `minusVarSet` gbl_tvs))
+
+ -- Do not quantify over constraints that *now* do not
+ -- mention quantified type variables, because they are
+ -- simply ambiguous (or might be bound further out). 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, but 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 (free3, irreds3) = partition (isFreeWhenInferring (mkVarSet qtvs2)) irreds2
+ ; extendLIEs free3
+
+ -- We can't abstract over any remaining unsolved
+ -- implications so instead just float them outwards. Ugh.
+ ; let (q_dicts, implics) = partition isDict irreds3
; loc <- getInstLoc (ImplicOrigin doc)
- ; implic_bind <- bindIrreds loc qtvs' dicts implics
+ ; implic_bind <- bindIrreds loc qtvs2 q_dicts implics
- ; return (qtvs', dicts, binds `unionBags` implic_bind) }
+ ; return (qtvs2, q_dicts, binds1 `unionBags` binds2 `unionBags` implic_bind) }
-- NB: when we are done, we might have some bindings, but
-- the final qtvs might be empty. See Note [NO TYVARS] below.
+
+getImplicWanteds :: TcTyVarSet -> [Inst] -> [Inst]
+-- See Note [Inference and implication constraints]
+-- Find the wanted constraints in implication constraints that mention the
+-- quantified type variables, and are not bound by forall's in the constraint itself
+-- Returns only Dicts
+getImplicWanteds qtvs implics
+ = concatMap get implics
+ where
+ get d@(Dict {}) | tyVarsOfInst d `intersectsVarSet` qtvs = [d]
+ | otherwise = []
+ get (ImplicInst {tci_tyvars = tvs, tci_wanted = wanteds})
+ = [ d | let tv_set = mkVarSet tvs
+ , d <- getImplicWanteds qtvs wanteds
+ , not (tyVarsOfInst d `intersectsVarSet` tv_set)]
\end{code}
+Note [Inference and implication constraints]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+We can't (or at least don't) abstract over implications. But we might
+have an implication constraint (perhaps arising from a nested pattern
+match) like
+ C a => D a
+when we are now trying to quantify over 'a'. Our best approximation
+is to make (D a) part of the inferred context, so we can use that to
+discharge the implication. Hence getImplicWanteds.
+
+See Trac #1430 and test tc228.
+
+
\begin{code}
-----------------------------------------------------------
-- tcSimplifyInferCheck is used when we know the constraints we are to simplify
| 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,
Hence we have a dictionary for Show [a] available; and indeed we
need it. We are going to build an implication contraint
forall a. (b~[a]) => Show [a]
-Later, we will solve this constraint using the knowledge (Show b)
+Later, we will solve this constraint using the knowledg e(Show b)
But we MUST NOT reduce (Show [a]) to (Show a), else the whole
thing becomes insoluble. So we simplify gently (get rid of literals
; 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,
-- to fromInteger; this looks fragile to me
; lookup_result <- lookupSimpleInst w'
; case lookup_result of
- GenInst ws' rhs -> go dicts (addBind binds w rhs) (ws' ++ ws)
+ GenInst ws' rhs -> go dicts (addBind binds (instToId w) rhs) (ws' ++ ws)
NoInstance -> pprPanic "tcSimplifyRuleLhs" (ppr w)
}
\end{code}
text "----",
text "avails" <+> pprAvails avails,
text "improved =" <+> ppr improved,
+ text "irreds = " <+> ppr irreds,
text "----------------------"
]))
-- Extract the binding
; (binds, irreds) <- extractResults avails wanteds
+ ; traceTc (text "reduceImplication result" <+> vcat
+ [ ppr irreds, ppr binds])
+
-- We always discard the extra avails we've generated;
-- but we remember if we have done any (global) improvement
; let ret_avails = updateImprovement orig_avails avails
return (ret_avails, NoInstance)
else do
{ (implic_insts, bind) <- makeImplicationBind inst_loc tvs reft extra_givens irreds
- -- This binding is useless if the recursive simplification
- -- made no progress; but currently we don't try to optimise that
- -- case. After all, we only try hard to reduce at top level, or
- -- when inferring types.
; let dict_ids = map instToId extra_givens
co = mkWpTyLams tvs <.> mkWpLams dict_ids <.> WpLet (binds `unionBags` bind)
rhs = mkHsWrap co payload
loc = instLocSpan inst_loc
- payload | isSingleton wanteds = HsVar (instToId (head wanteds))
+ payload | [wanted] <- wanteds = HsVar (instToId wanted)
| otherwise = ExplicitTuple (map (L loc . HsVar . instToId) wanteds) Boxed
-- If there are any irreds, we back off and return NoInstance
type AvailEnv = FiniteMap Inst AvailHow
data AvailHow
- = IsIrred -- Used for irreducible dictionaries,
+ = IsIrred TcId -- Used for irreducible dictionaries,
-- which are going to be lambda bound
| Given TcId -- Used for dictionaries for which we have a binding
-------------------------
pprAvail :: AvailHow -> SDoc
-pprAvail IsIrred = text "Irred"
+pprAvail (IsIrred x) = text "Irred" <+> ppr x
pprAvail (Given x) = text "Given" <+> ppr x
pprAvail (Rhs rhs bs) = text "Rhs" <+> ppr rhs <+> braces (ppr bs)
Nothing -> pprTrace "Urk: extractResults" (ppr w) $
go avails binds irreds ws
- Just IsIrred -> go (add_given avails w) binds (w:irreds) ws
-
Just (Given id)
- | id == instToId w
- -> go avails binds irreds ws
+ | id == w_id -> go avails binds irreds ws
+ | otherwise -> go avails (addBind binds w_id (nlHsVar id)) irreds ws
-- The sought Id can be one of the givens, via a superclass chain
-- and then we definitely don't want to generate an x=x binding!
- | otherwise
- -> go avails (addBind binds w (nlHsVar id)) irreds ws
+ Just (IsIrred id)
+ | id == w_id -> go (add_given avails w) binds (w:irreds) ws
+ | otherwise -> go avails (addBind binds w_id (nlHsVar id)) irreds ws
+ -- The add_given handles the case where we want (Ord a, Eq a), and we
+ -- don't want to emit *two* Irreds for Ord a, one via the superclass chain
+ -- This showed up in a dupliated Ord constraint in the error message for
+ -- test tcfail043
Just (Rhs rhs ws') -> go (add_given avails w) new_binds irreds (ws' ++ ws)
- where
- new_binds = addBind binds w rhs
+ where
+ new_binds = addBind binds w_id rhs
+ where
+ w_id = instToId w
add_given avails w = extendAvailEnv avails w (Given (instToId w))
+ -- Don't add the same binding twice
-addBind binds inst rhs = binds `unionBags` unitBag (L (instSpan inst)
- (VarBind (instToId inst) rhs))
+addBind binds id rhs = binds `unionBags` unitBag (L (getSrcSpan id) (VarBind id rhs))
\end{code}
\begin{code}
addIrred :: WantSCs -> Avails -> Inst -> TcM Avails
addIrred want_scs avails irred = ASSERT2( not (irred `elemAvails` avails), ppr irred $$ ppr avails )
- addAvailAndSCs want_scs avails irred IsIrred
+ addAvailAndSCs want_scs avails irred (IsIrred (instToId irred))
addAvailAndSCs :: WantSCs -> Avails -> Inst -> AvailHow -> TcM Avails
addAvailAndSCs want_scs avails inst avail
-- NB: irreds are already zonked
; dflags <- getDOpts
; disambiguate interactive dflags irreds1 -- Does unification
- ; (irreds2, binds2) <- topCheckLoop doc irreds1
+ -- hence try again
- -- Deal with implicit parameter
+ -- Deal with implicit parameters
+ ; (irreds2, binds2) <- topCheckLoop doc irreds1
; let (bad_ips, non_ips) = partition isIPDict irreds2
(ambigs, others) = partition isTyVarDict non_ips
; return () }
| otherwise
= do { -- Figure out what default types to use
- mb_defaults <- getDefaultTys
- ; default_tys <- case mb_defaults of
- Just tys -> return tys
- Nothing -> -- No use-supplied default;
- -- use [Integer, Double]
- do { integer_ty <- tcMetaTy integerTyConName
- ; checkWiredInTyCon doubleTyCon
- ; string_ty <- tcMetaTy stringTyConName
- ; if ovl_strings -- Add String if -foverloaded-strings
- then return [integer_ty,doubleTy,string_ty]
- else return [integer_ty,doubleTy] }
+ ; default_tys <- getDefaultTys extended_defaulting ovl_strings
; traceTc (text "disambigutate" <+> vcat [ppr unaries, ppr bad_tvs, ppr defaultable_groups])
; mapM_ (disambigGroup default_tys) defaultable_groups }
is_std_class cls = isStandardClass cls || (ovl_strings && (cls `hasKey` isStringClassKey))
-- Similarly is_std_class
+-----------------------
disambigGroup :: [Type] -- The default types
-> [(Inst,Class,TcTyVar)] -- All standard classes of form (C a)
-> TcM () -- Just does unification, to fix the default types
-- After this we can't fail
; warnDefault dicts default_ty
; unifyType default_ty (mkTyVarTy tyvar) }
+
+
+-----------------------
+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
+ Nothing -> do
+
+ -- No use-supplied default
+ -- Use [Integer, Double], plus modifications
+ { integer_ty <- tcMetaTy integerTyConName
+ ; checkWiredInTyCon doubleTyCon
+ ; string_ty <- tcMetaTy stringTyConName
+ ; return (opt_deflt extended_deflts unitTy
+ -- Note [Default unitTy]
+ ++
+ [integer_ty,doubleTy]
+ ++
+ opt_deflt ovl_strings string_ty) } } }
+ where
+ opt_deflt True ty = [ty]
+ opt_deflt False ty = []
+
+-----------------------
+getDefaultableDicts :: [Inst] -> ([(Inst, Class, TcTyVar)], TcTyVarSet)
+-- Look for free dicts of the form (C tv), even inside implications
+-- *and* the set of tyvars mentioned by all *other* constaints
+-- This disgustingly ad-hoc function is solely to support defaulting
+getDefaultableDicts insts
+ = (concat ps, unionVarSets tvs)
+ where
+ (ps, tvs) = mapAndUnzip get insts
+ get d@(Dict {tci_pred = ClassP cls [ty]})
+ | Just tv <- tcGetTyVar_maybe ty = ([(d,cls,tv)], emptyVarSet)
+ | otherwise = ([], tyVarsOfType ty)
+ get (ImplicInst {tci_tyvars = tvs, tci_wanted = wanteds})
+ = ([ up | up@(_,_,tv) <- ups, not (tv `elemVarSet` tv_set)],
+ ftvs `minusVarSet` tv_set)
+ where
+ tv_set = mkVarSet tvs
+ (ups, ftvs) = getDefaultableDicts wanteds
+ get inst = ([], tyVarsOfInst inst)
\end{code}
+Note [Default unitTy]
+~~~~~~~~~~~~~~~~~~~~~
+In interative mode (or with -fextended-default-rules) we add () as the first type we
+try when defaulting. This has very little real impact, except in the following case.
+Consider:
+ Text.Printf.printf "hello"
+This has type (forall a. IO a); it prints "hello", and returns 'undefined'. We don't
+want the GHCi repl loop to try to print that 'undefined'. The neatest thing is to
+default the 'a' to (), rather than to Integer (which is what would otherwise happen;
+and then GHCi doesn't attempt to print the (). So in interactive mode, we add
+() to the list of defaulting types. See Trac #1200.
+
Note [Avoiding spurious errors]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When doing the unification for defaulting, we check for skolem
addTopIPErrs bndrs []
= return ()
addTopIPErrs bndrs ips
- = addErrTcM (tidy_env, mk_msg tidy_ips)
+ = do { dflags <- getDOpts
+ ; addErrTcM (tidy_env, mk_msg dflags tidy_ips) }
where
(tidy_env, tidy_ips) = tidyInsts ips
- mk_msg ips = vcat [sep [ptext SLIT("Implicit parameters escape from"),
- nest 2 (ptext SLIT("the monomorphic top-level binding")
+ mk_msg dflags ips
+ = vcat [sep [ptext SLIT("Implicit parameters escape from"),
+ nest 2 (ptext SLIT("the monomorphic top-level binding")
<> plural bndrs <+> ptext SLIT("of")
<+> pprBinders bndrs <> colon)],
- nest 2 (vcat (map ppr_ip ips)),
- monomorphism_fix]
+ nest 2 (vcat (map ppr_ip ips)),
+ monomorphism_fix dflags]
ppr_ip ip = pprPred (dictPred ip) <+> pprInstArising ip
topIPErrs :: [Inst] -> TcM ()
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
-- Try to identify the offending variable
-- ASSUMPTION: the Insts are fully zonked
mkMonomorphismMsg tidy_env inst_tvs
- = findGlobals (mkVarSet inst_tvs) tidy_env `thenM` \ (tidy_env, docs) ->
- returnM (tidy_env, mk_msg docs)
+ = do { dflags <- getDOpts
+ ; (tidy_env, docs) <- findGlobals (mkVarSet inst_tvs) tidy_env
+ ; return (tidy_env, mk_msg dflags docs) }
where
- mk_msg [] = ptext SLIT("Probable fix: add a type signature that fixes these type variable(s)")
+ 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")
-- where monomorphism doesn't play any role
- mk_msg docs = vcat [ptext SLIT("Possible cause: the monomorphism restriction applied to the following:"),
- nest 2 (vcat docs),
- monomorphism_fix
- ]
-monomorphism_fix :: SDoc
-monomorphism_fix = ptext SLIT("Probable fix:") <+>
- (ptext SLIT("give these definition(s) an explicit type signature")
- $$ ptext SLIT("or use -fno-monomorphism-restriction"))
+ mk_msg dflags docs
+ = vcat [ptext SLIT("Possible cause: the monomorphism restriction applied to the following:"),
+ nest 2 (vcat docs),
+ monomorphism_fix dflags]
+
+isRuntimeUnk :: TcTyVar -> Bool
+isRuntimeUnk x | SkolemTv RuntimeUnkSkol <- tcTyVarDetails x = True
+ | otherwise = False
+
+monomorphism_fix :: DynFlags -> SDoc
+monomorphism_fix dflags
+ = ptext SLIT("Probable fix:") <+> vcat
+ [ptext SLIT("give these definition(s) an explicit type signature"),
+ if dopt Opt_MonomorphismRestriction dflags
+ then ptext SLIT("or use -fno-monomorphism-restriction")
+ else empty] -- Only suggest adding "-fno-monomorphism-restriction"
+ -- if it is not already set!
warnDefault ups default_ty
= doptM Opt_WarnTypeDefaults `thenM` \ warn_flag ->