-@tcSimplifyCheck@ is used when we know exactly the set of variables
-we are going to quantify over. For example, a class or instance declaration.
-
-\begin{code}
------------------------------------------------------------
--- tcSimplifyCheck is used when checking expression type signatures,
--- class decls, instance decls etc.
-tcSimplifyCheck :: InstLoc
- -> [TcTyVar] -- Quantify over these
- -> [Inst] -- Given
- -> [Inst] -- Wanted
- -> TcM TcDictBinds -- Bindings
-tcSimplifyCheck loc qtvs givens wanteds
- = ASSERT( all isTcTyVar qtvs && all isSkolemTyVar qtvs )
- do { traceTc (text "tcSimplifyCheck")
- ; (irreds, binds) <- gentleCheckLoop loc givens wanteds
- ; implic_bind <- bindIrreds loc qtvs givens irreds
- ; return (binds `unionBags` implic_bind) }
-
------------------------------------------------------------
--- tcSimplifyCheckPat is used for existential pattern match
-tcSimplifyCheckPat :: InstLoc
- -> [CoVar] -> Refinement
- -> [TcTyVar] -- Quantify over these
- -> [Inst] -- Given
- -> [Inst] -- Wanted
- -> TcM TcDictBinds -- Bindings
-tcSimplifyCheckPat loc co_vars reft qtvs givens wanteds
- = ASSERT( all isTcTyVar qtvs && all isSkolemTyVar qtvs )
- do { traceTc (text "tcSimplifyCheckPat")
- ; (irreds, binds) <- gentleCheckLoop loc givens wanteds
- ; implic_bind <- bindIrredsR loc qtvs co_vars reft
- givens irreds
- ; return (binds `unionBags` implic_bind) }
-
------------------------------------------------------------
-bindIrreds :: InstLoc -> [TcTyVar]
- -> [Inst] -> [Inst]
- -> TcM TcDictBinds
-bindIrreds loc qtvs givens irreds
- = bindIrredsR loc qtvs [] emptyRefinement givens irreds
-
-bindIrredsR :: InstLoc -> [TcTyVar] -> [CoVar]
- -> Refinement -> [Inst] -> [Inst]
- -> TcM TcDictBinds
--- Make a binding that binds 'irreds', by generating an implication
--- constraint for them, *and* throwing the constraint into the LIE
-bindIrredsR loc qtvs co_vars reft givens irreds
- | null irreds
- = return emptyBag
- | otherwise
- = do { let givens' = filter isAbstractableInst givens
- -- The givens can (redundantly) include methods
- -- We want to retain both EqInsts and Dicts
- -- There should be no implicadtion constraints
- -- See Note [Pruning the givens in an implication constraint]
-
- -- If there are no 'givens' *and* the refinement is empty
- -- (the refinement is like more givens), then it's safe to
- -- partition the 'wanteds' by their qtvs, thereby trimming irreds
- -- See Note [Freeness and implications]
- ; irreds' <- if null givens' && isEmptyRefinement reft
- then do
- { let qtv_set = mkVarSet qtvs
- (frees, real_irreds) = partition (isFreeWrtTyVars qtv_set) irreds
- ; extendLIEs frees
- ; return real_irreds }
- else return irreds
-
- ; let all_tvs = qtvs ++ co_vars -- Abstract over all these
- ; (implics, bind) <- makeImplicationBind loc all_tvs reft givens' irreds'
- -- This call does the real work
- -- If irreds' is empty, it does something sensible
- ; extendLIEs implics
- ; return bind }
-
-
-makeImplicationBind :: InstLoc -> [TcTyVar] -> Refinement
- -> [Inst] -> [Inst]
- -> TcM ([Inst], TcDictBinds)
--- Make a binding that binds 'irreds', by generating an implication
--- constraint for them, *and* throwing the constraint into the LIE
--- The binding looks like
--- (ir1, .., irn) = f qtvs givens
--- where f is (evidence for) the new implication constraint
--- f :: forall qtvs. {reft} givens => (ir1, .., irn)
--- qtvs includes coercion variables
---
--- This binding must line up the 'rhs' in reduceImplication
-makeImplicationBind loc all_tvs reft
- givens -- Guaranteed all Dicts
- -- or EqInsts
- irreds
- | null irreds -- If there are no irreds, we are done
- = return ([], emptyBag)
- | otherwise -- Otherwise we must generate a binding
- = do { uniq <- newUnique
- ; span <- getSrcSpanM
- ; let (eq_givens, dict_givens) = partition isEqInst givens
- eq_tyvar_cos = map TyVarTy $ uniqSetToList $ tyVarsOfTypes $ map eqInstType eq_givens
- ; let name = mkInternalName uniq (mkVarOcc "ic") span
- implic_inst = ImplicInst { tci_name = name, tci_reft = reft,
- tci_tyvars = all_tvs,
- tci_given = (eq_givens ++ dict_givens),
- tci_wanted = irreds, tci_loc = loc }
- ; let -- only create binder for dict_irreds
- (eq_irreds, dict_irreds) = partition isEqInst irreds
- n_dict_irreds = length dict_irreds
- dict_irred_ids = map instToId dict_irreds
- tup_ty = mkTupleTy Boxed n_dict_irreds (map idType dict_irred_ids)
- pat = TuplePat (map nlVarPat dict_irred_ids) Boxed tup_ty
- rhs = L span (mkHsWrap co (HsVar (instToId implic_inst)))
- co = mkWpApps (map instToId dict_givens) <.> mkWpTyApps eq_tyvar_cos <.> mkWpTyApps (mkTyVarTys all_tvs)
- bind | [dict_irred_id] <- dict_irred_ids = VarBind dict_irred_id rhs
- | otherwise = PatBind { pat_lhs = L span pat,
- pat_rhs = unguardedGRHSs rhs,
- pat_rhs_ty = tup_ty,
- bind_fvs = placeHolderNames }
- ; -- pprTrace "Make implic inst" (ppr (implic_inst,irreds,dict_irreds,tup_ty)) $
- return ([implic_inst], unitBag (L span bind)) }
-
------------------------------------------------------------
-tryHardCheckLoop :: SDoc
- -> [Inst] -- Wanted
- -> TcM ([Inst], TcDictBinds)
-
-tryHardCheckLoop doc wanteds
- = do { (irreds,binds,_) <- checkLoop (mkRedEnv doc try_me []) wanteds
- ; return (irreds,binds)
- }
- where
- try_me inst = ReduceMe AddSCs
- -- Here's the try-hard bit
-
------------------------------------------------------------
-gentleCheckLoop :: InstLoc
- -> [Inst] -- Given
- -> [Inst] -- Wanted
- -> TcM ([Inst], TcDictBinds)
-
-gentleCheckLoop inst_loc givens wanteds
- = do { (irreds,binds,_) <- checkLoop env wanteds
- ; return (irreds,binds)
- }
- where
- env = mkRedEnv (pprInstLoc inst_loc) try_me givens
-
- try_me inst | isMethodOrLit inst = ReduceMe AddSCs
- | otherwise = Stop
- -- When checking against a given signature
- -- we MUST be very gentle: Note [Check gently]
-
-gentleInferLoop :: SDoc -> [Inst]
- -> TcM ([Inst], TcDictBinds)
-gentleInferLoop doc wanteds
- = do { (irreds, binds, _) <- checkLoop env wanteds
- ; return (irreds, binds) }
- where
- env = mkRedEnv doc try_me []
- try_me inst | isMethodOrLit inst = ReduceMe AddSCs
- | otherwise = Stop
-\end{code}
-
-Note [Check gently]
-~~~~~~~~~~~~~~~~~~~~
-We have to very careful about not simplifying too vigorously
-Example:
- data T a where
- MkT :: a -> T [a]
-
- f :: Show b => T b -> b
- f (MkT x) = show [x]
-
-Inside the pattern match, which binds (a:*, x:a), we know that
- b ~ [a]
-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)
-
-But we MUST NOT reduce (Show [a]) to (Show a), else the whole
-thing becomes insoluble. So we simplify gently (get rid of literals
-and methods only, plus common up equal things), deferring the real
-work until top level, when we solve the implication constraint
-with tryHardCheckLooop.
-
-
-\begin{code}
------------------------------------------------------------
-checkLoop :: RedEnv
- -> [Inst] -- Wanted
- -> TcM ([Inst], TcDictBinds,
- [Inst]) -- needed givens
--- Precondition: givens are completely rigid
--- Postcondition: returned Insts are zonked
-
-checkLoop env wanteds
- = go env wanteds []
- where go env wanteds needed_givens
- = 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'
-
- ; let all_needed_givens = needed_givens ++ more_needed_givens
-
- ; if not improved then
- return (irreds, binds, all_needed_givens)
- else do
-
- -- If improvement did some unification, we go round again.
- -- We start again with irreds, not wanteds
- -- 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
- ; 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
- instance If T t e t
- instance If F t e e
- class Lte a b c | a b -> c where lte :: a -> b -> c
- instance Lte Z b T
- instance (Lte a b l,If l b a c) => Max a b c
-
-Wanted: Max Z (S x) y
-
-Then we'll reduce using the Max instance to:
- (Lte Z (S x) l, If l (S x) Z y)
-and improve by binding l->T, after which we can do some reduction
-on both the Lte and If constraints. What we *can't* do is start again
-with (Max Z (S x) y)!
-
-
-
-%************************************************************************
-%* *
- tcSimplifySuperClasses
-%* *
-%************************************************************************
-
-Note [SUPERCLASS-LOOP 1]
-~~~~~~~~~~~~~~~~~~~~~~~~
-We have to be very, very careful when generating superclasses, lest we
-accidentally build a loop. Here's an example:
-
- class S a
-
- class S a => C a where { opc :: a -> a }
- class S b => D b where { opd :: b -> b }
-
- instance C Int where
- opc = opd
-
- instance D Int where
- opd = opc
-
-From (instance C Int) we get the constraint set {ds1:S Int, dd:D Int}
-Simplifying, we may well get:
- $dfCInt = :C ds1 (opd dd)
- dd = $dfDInt
- ds1 = $p1 dd
-Notice that we spot that we can extract ds1 from dd.
-
-Alas! Alack! We can do the same for (instance D Int):
-
- $dfDInt = :D ds2 (opc dc)
- dc = $dfCInt
- ds2 = $p1 dc
-
-And now we've defined the superclass in terms of itself.
-
-Solution: never generate a superclass selectors at all when
-satisfying the superclass context of an instance declaration.
-
-Two more nasty cases are in
- tcrun021
- tcrun033
-
-\begin{code}
-tcSimplifySuperClasses
- :: InstLoc
- -> [Inst] -- Given
- -> [Inst] -- Wanted
- -> TcM TcDictBinds
-tcSimplifySuperClasses loc givens sc_wanteds
- = do { traceTc (text "tcSimplifySuperClasses")
- ; (irreds,binds1,_) <- checkLoop env sc_wanteds
- ; let (tidy_env, tidy_irreds) = tidyInsts irreds
- ; reportNoInstances tidy_env (Just (loc, givens)) tidy_irreds
- ; return binds1 }
- where
- env = mkRedEnv (pprInstLoc loc) try_me givens
- try_me inst = ReduceMe NoSCs
- -- Like tryHardCheckLoop, but with NoSCs
-\end{code}
-
-
-%************************************************************************
-%* *
-\subsection{tcSimplifyRestricted}
-%* *
-%************************************************************************
-
-tcSimplifyRestricted infers which type variables to quantify for a
-group of restricted bindings. This isn't trivial.
-
-Eg1: id = \x -> x
- We want to quantify over a to get id :: forall a. a->a
-
-Eg2: eq = (==)
- We do not want to quantify over a, because there's an Eq a
- constraint, so we get eq :: a->a->Bool (notice no forall)
-
-So, assume:
- RHS has type 'tau', whose free tyvars are tau_tvs
- RHS has constraints 'wanteds'
-
-Plan A (simple)
- Quantify over (tau_tvs \ ftvs(wanteds))
- This is bad. The constraints may contain (Monad (ST s))
- where we have instance Monad (ST s) where...
- so there's no need to be monomorphic in s!
-
- Also the constraint might be a method constraint,
- whose type mentions a perfectly innocent tyvar:
- op :: Num a => a -> b -> a
- Here, b is unconstrained. A good example would be
- foo = op (3::Int)
- We want to infer the polymorphic type
- foo :: forall b. b -> b
-
-
-Plan B (cunning, used for a long time up to and including GHC 6.2)
- Step 1: Simplify the constraints as much as possible (to deal
- with Plan A's problem). Then set
- qtvs = tau_tvs \ ftvs( simplify( wanteds ) )
-
- Step 2: Now simplify again, treating the constraint as 'free' if
- it does not mention qtvs, and trying to reduce it otherwise.
- The reasons for this is to maximise sharing.
-
- This fails for a very subtle reason. Suppose that in the Step 2
- a constraint (Foo (Succ Zero) (Succ Zero) b) gets thrown upstairs as 'free'.
- In the Step 1 this constraint might have been simplified, perhaps to
- (Foo Zero Zero b), AND THEN THAT MIGHT BE IMPROVED, to bind 'b' to 'T'.
- This won't happen in Step 2... but that in turn might prevent some other
- constraint (Baz [a] b) being simplified (e.g. via instance Baz [a] T where {..})
- and that in turn breaks the invariant that no constraints are quantified over.
-
- Test typecheck/should_compile/tc177 (which failed in GHC 6.2) demonstrates
- the problem.
-
-
-Plan C (brutal)
- Step 1: Simplify the constraints as much as possible (to deal
- with Plan A's problem). Then set
- qtvs = tau_tvs \ ftvs( simplify( wanteds ) )
- Return the bindings from Step 1.
-
-
-A note about Plan C (arising from "bug" reported by George Russel March 2004)
-Consider this:
-
- instance (HasBinary ty IO) => HasCodedValue ty
-
- foo :: HasCodedValue a => String -> IO a
-
- doDecodeIO :: HasCodedValue a => () -> () -> IO a
- doDecodeIO codedValue view
- = let { act = foo "foo" } in act
-
-You might think this should work becuase the call to foo gives rise to a constraint
-(HasCodedValue t), which can be satisfied by the type sig for doDecodeIO. But the
-restricted binding act = ... calls tcSimplifyRestricted, and PlanC simplifies the
-constraint using the (rather bogus) instance declaration, and now we are stuffed.
-
-I claim this is not really a bug -- but it bit Sergey as well as George. So here's
-plan D
-
-
-Plan D (a variant of plan B)
- Step 1: Simplify the constraints as much as possible (to deal
- with Plan A's problem), BUT DO NO IMPROVEMENT. Then set
- qtvs = tau_tvs \ ftvs( simplify( wanteds ) )
-
- Step 2: Now simplify again, treating the constraint as 'free' if
- it does not mention qtvs, and trying to reduce it otherwise.
-
- The point here is that it's generally OK to have too few qtvs; that is,
- to make the thing more monomorphic than it could be. We don't want to
- do that in the common cases, but in wierd cases it's ok: the programmer
- can always add a signature.
-
- Too few qtvs => too many wanteds, which is what happens if you do less
- improvement.
-
-
-\begin{code}
-tcSimplifyRestricted -- Used for restricted binding groups
- -- i.e. ones subject to the monomorphism restriction
- :: SDoc
- -> TopLevelFlag
- -> [Name] -- Things bound in this group
- -> TcTyVarSet -- Free in the type of the RHSs
- -> [Inst] -- Free in the RHSs
- -> TcM ([TyVar], -- Tyvars to quantify (zonked and quantified)
- TcDictBinds) -- Bindings
- -- tcSimpifyRestricted returns no constraints to
- -- quantify over; by definition there are none.
- -- They are all thrown back in the LIE
-
-tcSimplifyRestricted doc top_lvl bndrs tau_tvs wanteds
- -- Zonk everything in sight
- = do { traceTc (text "tcSimplifyRestricted")
- ; wanteds' <- zonkInsts wanteds
-
- -- 'ReduceMe': Reduce as far as we can. Don't stop at
- -- dicts; the idea is to get rid of as many type
- -- variables as possible, and we don't want to stop
- -- at (say) Monad (ST s), because that reduces
- -- immediately, with no constraint on s.
- --
- -- BUT do no improvement! See Plan D above
- -- HOWEVER, some unification may take place, if we instantiate
- -- a method Inst with an equality constraint
- ; let env = mkNoImproveRedEnv doc (\i -> ReduceMe AddSCs)
- ; (_imp, _binds, constrained_dicts, _) <- reduceContext env wanteds'
-
- -- Next, figure out the tyvars we will quantify over
- ; tau_tvs' <- zonkTcTyVarsAndFV (varSetElems tau_tvs)
- ; gbl_tvs' <- tcGetGlobalTyVars
- ; constrained_dicts' <- zonkInsts constrained_dicts
-
- ; 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,
- ppr constrained_tvs', ppr tau_tvs', ppr qtvs ])
-
- -- The first step may have squashed more methods than
- -- necessary, so try again, this time more gently, knowing the exact
- -- set of type variables to quantify over.
- --
- -- We quantify only over constraints that are captured by qtvs;
- -- these will just be a subset of non-dicts. This in contrast
- -- to normal inference (using isFreeWhenInferring) in which we quantify over
- -- all *non-inheritable* constraints too. This implements choice
- -- (B) under "implicit parameter and monomorphism" above.
- --
- -- Remember that we may need to do *some* simplification, to
- -- (for example) squash {Monad (ST s)} into {}. It's not enough
- -- just to float all constraints
- --
- -- At top level, we *do* squash methods becuase we want to
- -- expose implicit parameters to the test that follows
- ; let is_nested_group = isNotTopLevel top_lvl
- try_me inst | isFreeWrtTyVars qtvs inst,
- (is_nested_group || isDict inst) = Stop
- | otherwise = ReduceMe AddSCs
- env = mkNoImproveRedEnv doc try_me
- ; (_imp, binds, irreds, _) <- reduceContext env wanteds'
-
- -- See "Notes on implicit parameters, Question 4: top level"
- ; ASSERT( all (isFreeWrtTyVars qtvs) irreds ) -- None should be captured
- if is_nested_group then
- extendLIEs irreds
- else do { let (bad_ips, non_ips) = partition isIPDict irreds
- ; addTopIPErrs bndrs bad_ips
- ; extendLIEs non_ips }
-
- ; qtvs' <- zonkQuantifiedTyVars (varSetElems qtvs)
- ; return (qtvs', binds) }
-\end{code}
-
-
-%************************************************************************
-%* *
- tcSimplifyRuleLhs
-%* *
-%************************************************************************