Note [Implicit parameters and ambiguity]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-What type should we infer for this?
- f x = (show ?y, x::Int)
-Since we must quantify over the ?y, the most plausible type is
- f :: (Show a, ?y::a) => Int -> (String, Int)
-But notice that the type of the RHS is (String,Int), with no type
-varibables mentioned at all! The type of f looks ambiguous. But
-it isn't, because at a call site we might have
- let ?y = 5::Int in f 7
+Only a *class* predicate can give rise to ambiguity
+An *implicit parameter* cannot. For example:
+ foo :: (?x :: [a]) => Int
+ foo = length ?x
+is fine. The call site will suppply a particular 'x'
+
+Furthermore, the type variables fixed by an implicit parameter
+propagate to the others. E.g.
+ foo :: (Show a, ?x::[a]) => Int
+ foo = show (?x++?x)
+The type of foo looks ambiguous. But it isn't, because at a call site
+we might have
+ let ?x = 5::Int in foo
and all is well. In effect, implicit parameters are, well, parameters,
so we can take their type variables into account as part of the
"tau-tvs" stuff. This is done in the function 'FunDeps.grow'.
checkLoop env wanteds
= go env wanteds []
where go env wanteds needed_givens
- = do { -- Givens are skolems, so no need to zonk them
- wanteds' <- zonkInsts wanteds
+ = do { -- We do need to zonk the givens; cf Note [Zonking RedEnv]
+ ; env' <- zonkRedEnv env
+ ; wanteds' <- zonkInsts wanteds
- ; (improved, binds, irreds, more_needed_givens) <- reduceContext env wanteds'
+ ; (improved, binds, irreds, more_needed_givens) <- reduceContext env' wanteds'
; let all_needed_givens = needed_givens ++ more_needed_givens
-- Using an instance decl might have introduced a fresh type variable
-- which might have been unified, so we'd get an infinite loop
-- if we started again with wanteds! See Note [LOOP]
- { (irreds1, binds1, all_needed_givens1) <- go env irreds all_needed_givens
+ { (irreds1, binds1, all_needed_givens1) <- go env' irreds all_needed_givens
; return (irreds1, binds `unionBags` binds1, all_needed_givens1) } }
\end{code}
+Note [Zonking RedEnv]
+~~~~~~~~~~~~~~~~~~~~~
+It might appear as if the givens in RedEnv are always rigid, but that is not
+necessarily the case for programs involving higher-rank types that have class
+contexts constraining the higher-rank variables. An example from tc237 in the
+testsuite is
+
+ class Modular s a | s -> a
+
+ wim :: forall a w. Integral a
+ => a -> (forall s. Modular s a => M s w) -> w
+ wim i k = error "urk"
+
+ test5 :: (Modular s a, Integral a) => M s a
+ test5 = error "urk"
+
+ test4 = wim 4 test4'
+
+Notice how the variable 'a' of (Modular s a) in the rank-2 type of wim is
+quantified further outside. When type checking test4, we have to check
+whether the signature of test5 is an instance of
+
+ (forall s. Modular s a => M s w)
+
+Consequently, we will get (Modular s t_a), where t_a is a TauTv into the
+givens.
+
+Given the FD of Modular in this example, class improvement will instantiate
+t_a to 'a', where 'a' is the skolem from test5's signatures (due to the
+Modular s a predicate in that signature). If we don't zonk (Modular s t_a) in
+the givens, we will get into a loop as improveOne uses the unification engine
+TcGadt.tcUnifyTys, which doesn't know about mutable type variables.
+
+
Note [LOOP]
~~~~~~~~~~~
class If b t e r | b t e -> r
-- 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 (addInstToDictBind binds w rhs) (ws' ++ ws)
NoInstance -> pprPanic "tcSimplifyRuleLhs" (ppr w)
}
\end{code}
-- of a predicate when adding it to the avails
-- The reason for this flag is entirely the super-class loop problem
-- Note [SUPER-CLASS LOOP 1]
+
+zonkRedEnv :: RedEnv -> TcM RedEnv
+zonkRedEnv env
+ = do { givens' <- mappM zonkInst (red_givens env)
+ ; return $ env {red_givens = givens'}
+ }
\end{code}
; traceTc $ text "reduceContext: ancestor eqs" <+> ppr ancestor_eqs
-- 1. Normalise the *given* *equality* constraints
- ; (given_eqs, eliminate_skolems) <- normaliseGivens given_eqs0
+ ; (given_eqs, eliminate_skolems) <- normaliseGivenEqs given_eqs0
-- 2. Normalise the *given* *dictionary* constraints
-- wrt. the toplevel and given equations
given_dicts0
-- 3. Solve the *wanted* *equation* constraints
- ; eq_irreds0 <- solveWanteds given_eqs wanted_eqs
+ ; eq_irreds0 <- solveWantedEqs given_eqs wanted_eqs
-- 4. Normalise the *wanted* equality constraints with respect to
-- each other
- ; eq_irreds <- normaliseWanteds eq_irreds0
+ ; eq_irreds <- normaliseWantedEqs eq_irreds0
-- 5. Build the Avail mapping from "given_dicts"
; init_state <- foldlM addGiven emptyAvails given_dicts
go wanteds state }
where
go [] state = return state
- go (w:ws) state = do { traceTc (text "reduceList " <+> ppr (w:ws) <+> ppr state)
+ go (w:ws) state = do { traceTc (text "reduceList " <+> (ppr (w:ws) $$ ppr state))
; state' <- reduce (env {red_stack = (n+1, w:stk)}) w state
; go ws state' }
Note [Reducing implication constraints]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Suppose we are trying to simplify
- (Ord a, forall b. C a b => (W [a] b, D c b))
+ ( do: Ord a,
+ ic: (forall b. C a b => (W [a] b, D c b)) )
where
instance (C a b, Ord a) => W [a] b
When solving the implication constraint, we'll start with
in the Avails. Then we add (C a b -> Given) and solve. Extracting
the results gives us a binding for the (W [a] b), with an Irred of
(Ord a, D c b). Now, the (Ord a) comes from "outside" the implication,
-but the (D d b) is from "inside". So we want to generate a Rhs binding
+but the (D d b) is from "inside". So we want to generate a GenInst
like this
- ic = /\b \dc:C a b). (df a b dc do, ic' b dc)
- depending on
- do :: Ord a
- ic' :: forall b. C a b => D c b
+ ic = GenInst
+ [ do :: Ord a,
+ ic' :: forall b. C a b => D c b]
+ (/\b \(dc:C a b). (df a b dc do, ic' b dc))
+
+The first arg of GenInst gives the free dictionary variables of the
+second argument -- the "needed givens". And that list in turn is
+vital because it's used to determine what other dicts must be solved.
+This very list ends up in the second field of the Rhs, and drives
+extractResults.
+
+The need for this field is why we have to return "needed givens"
+from extractResults, reduceContext, checkLoop, and so on.
-The 'depending on' part of the Rhs is important, because it drives
-the extractResults code.
+NB: the "needed givens" in a GenInst or Rhs, may contain two dicts
+with the same type but different Ids, e.g. [d12 :: Eq a, d81 :: Eq a]
+That says we must generate a binding for both d12 and d81.
The "inside" and "outside" distinction is what's going on with 'inner' and
'outer' in reduceImplication
-> TcM ( TcDictBinds, -- Bindings
[Inst], -- Irreducible ones
[Inst]) -- Needed givens, i.e. ones used in the bindings
+ -- Postcondition: needed-givens = free vars( binds ) \ irreds
+ -- Note [Reducing implication constraints]
extractResults (Avails _ avails) wanteds
= go avails emptyBag [] [] wanteds
Just (Given id)
| id == w_id -> go avails binds irreds (w:givens) ws
- | otherwise -> go avails (addBind binds w (nlHsVar id)) irreds (update_id w id:givens) ws
+ | otherwise ->
+ go avails (addInstToDictBind binds w (nlHsVar id)) irreds
+ (update_id w id:givens) 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!
Just (Rhs rhs ws') -> go (add_given avails w) new_binds irreds givens (ws' ++ ws)
where
- new_binds = addBind binds w rhs
+ new_binds = addInstToDictBind binds w rhs
where
w_id = instToId w
update_id m@(Method{}) id = m {tci_id = id}
Just (Rhs rhs ws') -> go (add_given avails w) new_binds givens (ws' ++ ws)
where
- new_binds = addBind binds w rhs
+ new_binds = addInstToDictBind binds w rhs
where
w_id = instToId w
find_all :: IdSet -> Inst -> IdSet
find_all so_far kid
+ | isEqInst kid = so_far
| kid_id `elemVarSet` so_far = so_far
| Just avail <- findAvail avails kid = findAllDeps so_far' avail
| otherwise = so_far'
where
(clas, tys) = getDictClassTys dict
(tyvars, sc_theta, sc_sels, _) = classBigSig clas
- sc_theta' = substTheta (zipTopTvSubst tyvars tys) sc_theta
+ sc_theta' = filter (not . isEqPred) $
+ substTheta (zipTopTvSubst tyvars tys) sc_theta
add_sc avails (sc_dict, sc_sel)
| is_loop (dictPred sc_dict) = return avails -- See Note [SUPERCLASS-LOOP 2]
; mapM_ complain_implic implics
; mapM_ (\doc -> addErrTcM (tidy_env, doc)) overlaps
; groupErrs complain_no_inst insts3
- ; mapM_ complain_eq eqInsts
+ ; mapM_ eqInstMisMatch eqInsts
}
where
complain_no_inst insts = addErrTcM (tidy_env, mk_no_inst_err insts)
(Just (tci_loc inst, tci_given inst))
(tci_wanted inst)
- complain_eq EqInst {tci_left = lty, tci_right = rty,
- tci_loc = InstLoc _ _ ctxt}
- = do { (env, msg) <- misMatchMsg lty rty
- ; setErrCtxt ctxt $
- failWithTcM (env, msg)
- }
-
check_overlap :: (InstEnv,InstEnv) -> Inst -> Either Inst SDoc
-- Right msg => overlap message
-- Left inst => no instance
nest 4 (pprStack stack)]
pprStack stack = vcat (map pprInstInFull stack)
-
------------------------
-misMatchMsg :: TcType -> TcType -> TcM (TidyEnv, SDoc)
--- Generate the message when two types fail to match,
--- going to some trouble to make it helpful.
--- The argument order is: actual type, expected type
-misMatchMsg ty_act ty_exp
- = do { env0 <- tcInitTidyEnv
- ; ty_exp <- zonkTcType ty_exp
- ; ty_act <- zonkTcType ty_act
- ; (env1, pp_exp, extra_exp) <- ppr_ty env0 ty_exp
- ; (env2, pp_act, extra_act) <- ppr_ty env1 ty_act
- ; return (env2,
- sep [sep [ptext SLIT("Couldn't match expected type") <+> pp_exp,
- nest 7 $
- ptext SLIT("against inferred type") <+> pp_act],
- nest 2 (extra_exp $$ extra_act)]) }
-
-ppr_ty :: TidyEnv -> TcType -> TcM (TidyEnv, SDoc, SDoc)
-ppr_ty env ty
- = do { let (env1, tidy_ty) = tidyOpenType env ty
- ; (env2, extra) <- ppr_extra env1 tidy_ty
- ; return (env2, quotes (ppr tidy_ty), extra) }
-
--- (ppr_extra env ty) shows extra info about 'ty'
-ppr_extra env (TyVarTy tv)
- | isSkolemTyVar tv || isSigTyVar tv
- = return (env1, pprSkolTvBinding tv1)
- where
- (env1, tv1) = tidySkolemTyVar env tv
-
-ppr_extra env ty = return (env, empty) -- Normal case
\end{code}
projects / ghc-hetmet.git / blobdiff