-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 { (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 { wanteds' <- mappM zonkInst 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' <- mappM zonkInst 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
-%* *
-%************************************************************************
-
-On the LHS of transformation rules we only simplify methods and constants,
-getting dictionaries. We want to keep all of them unsimplified, to serve
-as the available stuff for the RHS of the rule.
-
-Example. Consider the following left-hand side of a rule
-
- f (x == y) (y > z) = ...
-
-If we typecheck this expression we get constraints
-
- d1 :: Ord a, d2 :: Eq a
-
-We do NOT want to "simplify" to the LHS
-
- forall x::a, y::a, z::a, d1::Ord a.
- f ((==) (eqFromOrd d1) x y) ((>) d1 y z) = ...
-
-Instead we want
-
- forall x::a, y::a, z::a, d1::Ord a, d2::Eq a.
- f ((==) d2 x y) ((>) d1 y z) = ...
-
-Here is another example:
-
- fromIntegral :: (Integral a, Num b) => a -> b
- {-# RULES "foo" fromIntegral = id :: Int -> Int #-}
-
-In the rule, a=b=Int, and Num Int is a superclass of Integral Int. But
-we *dont* want to get
-
- forall dIntegralInt.
- fromIntegral Int Int dIntegralInt (scsel dIntegralInt) = id Int
-
-because the scsel will mess up RULE matching. Instead we want
-
- forall dIntegralInt, dNumInt.
- fromIntegral Int Int dIntegralInt dNumInt = id Int
-
-Even if we have
-
- g (x == y) (y == z) = ..
-
-where the two dictionaries are *identical*, we do NOT WANT
-
- forall x::a, y::a, z::a, d1::Eq a
- f ((==) d1 x y) ((>) d1 y z) = ...
-
-because that will only match if the dict args are (visibly) equal.
-Instead we want to quantify over the dictionaries separately.
-
-In short, tcSimplifyRuleLhs must *only* squash LitInst and MethInts, leaving
-all dicts unchanged, with absolutely no sharing. It's simpler to do this
-from scratch, rather than further parameterise simpleReduceLoop etc
-
-\begin{code}
-tcSimplifyRuleLhs :: [Inst] -> TcM ([Inst], TcDictBinds)
-tcSimplifyRuleLhs wanteds
- = go [] emptyBag wanteds
- where
- go dicts binds []
- = return (dicts, binds)
- go dicts binds (w:ws)
- | isDict w
- = go (w:dicts) binds ws
- | otherwise
- = do { w' <- zonkInst w -- So that (3::Int) does not generate a call
- -- to fromInteger; this looks fragile to me
- ; lookup_result <- lookupSimpleInst w'
- ; case lookup_result of
- GenInst ws' rhs -> go dicts (addBind binds (instToId w) rhs) (ws' ++ ws)
- NoInstance -> pprPanic "tcSimplifyRuleLhs" (ppr w)
- }
-\end{code}
-
-tcSimplifyBracket is used when simplifying the constraints arising from
-a Template Haskell bracket [| ... |]. We want to check that there aren't
-any constraints that can't be satisfied (e.g. Show Foo, where Foo has no
-Show instance), but we aren't otherwise interested in the results.
-Nor do we care about ambiguous dictionaries etc. We will type check
-this bracket again at its usage site.
-
-\begin{code}
-tcSimplifyBracket :: [Inst] -> TcM ()
-tcSimplifyBracket wanteds
- = do { tryHardCheckLoop doc wanteds
- ; return () }
- where
- doc = text "tcSimplifyBracket"
-\end{code}
-
-
-%************************************************************************
-%* *
-\subsection{Filtering at a dynamic binding}
-%* *
-%************************************************************************
-
-When we have
- let ?x = R in B
-
-we must discharge all the ?x constraints from B. We also do an improvement
-step; if we have ?x::t1 and ?x::t2 we must unify t1, t2.
-
-Actually, the constraints from B might improve the types in ?x. For example
-
- f :: (?x::Int) => Char -> Char
- let ?x = 3 in f 'c'
-
-then the constraint (?x::Int) arising from the call to f will
-force the binding for ?x to be of type Int.
-
-\begin{code}
-tcSimplifyIPs :: [Inst] -- The implicit parameters bound here
- -> [Inst] -- Wanted
- -> TcM TcDictBinds
- -- We need a loop so that we do improvement, and then
- -- (next time round) generate a binding to connect the two
- -- let ?x = e in ?x
- -- Here the two ?x's have different types, and improvement
- -- makes them the same.
-
-tcSimplifyIPs given_ips wanteds
- = do { wanteds' <- mappM zonkInst wanteds
- ; given_ips' <- mappM zonkInst given_ips
- -- Unusually for checking, we *must* zonk the given_ips
-
- ; let env = mkRedEnv doc try_me given_ips'
- ; (improved, binds, irreds) <- reduceContext env wanteds'
-
- ; if not improved then
- ASSERT( all is_free irreds )
- do { extendLIEs irreds
- ; return binds }
- else
- tcSimplifyIPs given_ips wanteds }
- where
- doc = text "tcSimplifyIPs" <+> ppr given_ips
- ip_set = mkNameSet (ipNamesOfInsts given_ips)
- is_free inst = isFreeWrtIPs ip_set inst
-
- -- Simplify any methods that mention the implicit parameter
- try_me inst | is_free inst = Stop
- | otherwise = ReduceMe NoSCs
-\end{code}
-
-
-%************************************************************************
-%* *
-\subsection[binds-for-local-funs]{@bindInstsOfLocalFuns@}
-%* *
-%************************************************************************
-
-When doing a binding group, we may have @Insts@ of local functions.
-For example, we might have...
-\begin{verbatim}
-let f x = x + 1 -- orig local function (overloaded)
- f.1 = f Int -- two instances of f
- f.2 = f Float
- in
- (f.1 5, f.2 6.7)
-\end{verbatim}
-The point is: we must drop the bindings for @f.1@ and @f.2@ here,
-where @f@ is in scope; those @Insts@ must certainly not be passed
-upwards towards the top-level. If the @Insts@ were binding-ified up
-there, they would have unresolvable references to @f@.
-
-We pass in an @init_lie@ of @Insts@ and a list of locally-bound @Ids@.
-For each method @Inst@ in the @init_lie@ that mentions one of the
-@Ids@, we create a binding. We return the remaining @Insts@ (in an
-@LIE@), as well as the @HsBinds@ generated.
-
-\begin{code}
-bindInstsOfLocalFuns :: [Inst] -> [TcId] -> TcM TcDictBinds
--- Simlifies only MethodInsts, and generate only bindings of form
--- fm = f tys dicts
--- We're careful not to even generate bindings of the form
--- d1 = d2
--- You'd think that'd be fine, but it interacts with what is
--- arguably a bug in Match.tidyEqnInfo (see notes there)
-
-bindInstsOfLocalFuns wanteds local_ids
- | null overloaded_ids
- -- Common case
- = extendLIEs wanteds `thenM_`
- returnM emptyLHsBinds
-
- | otherwise
- = do { (irreds, binds) <- checkLoop env for_me
- ; extendLIEs not_for_me
- ; extendLIEs irreds
- ; return binds }
- where
- env = mkRedEnv doc try_me []
- doc = text "bindInsts" <+> ppr local_ids
- overloaded_ids = filter is_overloaded local_ids
- is_overloaded id = isOverloadedTy (idType id)
- (for_me, not_for_me) = partition (isMethodFor overloaded_set) wanteds
-
- overloaded_set = mkVarSet overloaded_ids -- There can occasionally be a lot of them
- -- so it's worth building a set, so that
- -- lookup (in isMethodFor) is faster
- try_me inst | isMethod inst = ReduceMe NoSCs
- | otherwise = Stop
-\end{code}
-
-
-%************************************************************************
-%* *
-\subsection{Data types for the reduction mechanism}
-%* *
-%************************************************************************
-
-The main control over context reduction is here
-
-\begin{code}
-data RedEnv
- = RedEnv { red_doc :: SDoc -- The context
- , red_try_me :: Inst -> WhatToDo
- , red_improve :: Bool -- True <=> do improvement
- , red_givens :: [Inst] -- All guaranteed rigid
- -- Always dicts
- -- but see Note [Rigidity]
- , red_stack :: (Int, [Inst]) -- Recursion stack (for err msg)
- -- See Note [RedStack]
- }
-
--- Note [Rigidity]
--- The red_givens are rigid so far as cmpInst is concerned.
--- There is one case where they are not totally rigid, namely in tcSimplifyIPs
--- let ?x = e in ...
--- Here, the given is (?x::a), where 'a' is not necy a rigid type
--- But that doesn't affect the comparison, which is based only on mame.
-
--- Note [RedStack]
--- The red_stack pair (n,insts) pair is just used for error reporting.
--- 'n' is always the depth of the stack.
--- The 'insts' is the stack of Insts being reduced: to produce X
--- I had to produce Y, to produce Y I had to produce Z, and so on.
-
-
-mkRedEnv :: SDoc -> (Inst -> WhatToDo) -> [Inst] -> RedEnv
-mkRedEnv doc try_me givens
- = RedEnv { red_doc = doc, red_try_me = try_me,
- red_givens = givens, red_stack = (0,[]),
- red_improve = True }
-
-mkNoImproveRedEnv :: SDoc -> (Inst -> WhatToDo) -> RedEnv
--- Do not do improvement; no givens
-mkNoImproveRedEnv doc try_me
- = RedEnv { red_doc = doc, red_try_me = try_me,
- red_givens = [], red_stack = (0,[]),
- red_improve = True }
-
-data WhatToDo
- = ReduceMe WantSCs -- Try to reduce this
- -- If there's no instance, add the inst to the
- -- irreductible ones, but don't produce an error
- -- message of any kind.
- -- It might be quite legitimate such as (Eq a)!
-
- | Stop -- Return as irreducible unless it can
- -- be reduced to a constant in one step
- -- Do not add superclasses; see
-
-data WantSCs = NoSCs | AddSCs -- Tells whether we should add the superclasses
- -- 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]
-\end{code}
-
-%************************************************************************
-%* *
-\subsection[reduce]{@reduce@}
-%* *
-%************************************************************************
-
-
-\begin{code}
-reduceContext :: RedEnv
- -> [Inst] -- Wanted
- -> TcM (ImprovementDone,
- TcDictBinds, -- Dictionary bindings
- [Inst]) -- Irreducible
-
-reduceContext env wanteds
- = do { traceTc (text "reduceContext" <+> (vcat [
- text "----------------------",
- red_doc env,
- text "given" <+> ppr (red_givens env),
- text "wanted" <+> ppr wanteds,
- text "----------------------"
- ]))
-
- -- Build the Avail mapping from "givens"
- ; init_state <- foldlM addGiven emptyAvails (red_givens env)
-
- -- Do the real work
- -- Process non-implication constraints first, so that they are
- -- available to help solving the implication constraints
- -- ToDo: seems a bit inefficient and ad-hoc
- ; let (implics, rest) = partition isImplicInst wanteds
- ; avails <- reduceList env (rest ++ implics) init_state
-
- ; let improved = availsImproved avails
- ; (binds, irreds) <- extractResults avails wanteds
-
- ; traceTc (text "reduceContext end" <+> (vcat [
- text "----------------------",
- red_doc env,
- text "given" <+> ppr (red_givens env),
- text "wanted" <+> ppr wanteds,
- text "----",
- text "avails" <+> pprAvails avails,
- text "improved =" <+> ppr improved,
- text "irreds = " <+> ppr irreds,
- text "----------------------"
- ]))
-
- ; return (improved, binds, irreds) }
-
-tcImproveOne :: Avails -> Inst -> TcM ImprovementDone
-tcImproveOne avails inst
- | not (isDict inst) = return False
- | otherwise
- = do { inst_envs <- tcGetInstEnvs
- ; let eqns = improveOne (classInstances inst_envs)
- (dictPred inst, pprInstArising inst)
- [ (dictPred p, pprInstArising p)
- | p <- availsInsts avails, isDict p ]
- -- Avails has all the superclasses etc (good)
- -- It also has all the intermediates of the deduction (good)
- -- It does not have duplicates (good)
- -- NB that (?x::t1) and (?x::t2) will be held separately in avails
- -- so that improve will see them separate
- ; traceTc (text "improveOne" <+> ppr inst)
- ; unifyEqns eqns }
-
-unifyEqns :: [(Equation,(PredType,SDoc),(PredType,SDoc))]
- -> TcM ImprovementDone
-unifyEqns [] = return False
-unifyEqns eqns
- = do { traceTc (ptext SLIT("Improve:") <+> vcat (map pprEquationDoc eqns))
- ; mappM_ unify eqns
- ; return True }
- where
- unify ((qtvs, pairs), what1, what2)
- = addErrCtxtM (mkEqnMsg what1 what2) $
- tcInstTyVars (varSetElems qtvs) `thenM` \ (_, _, tenv) ->
- mapM_ (unif_pr tenv) pairs
- unif_pr tenv (ty1,ty2) = unifyType (substTy tenv ty1) (substTy tenv ty2)
-
-pprEquationDoc (eqn, (p1,w1), (p2,w2)) = vcat [pprEquation eqn, nest 2 (ppr p1), nest 2 (ppr p2)]
-
-mkEqnMsg (pred1,from1) (pred2,from2) tidy_env
- = do { pred1' <- zonkTcPredType pred1; pred2' <- zonkTcPredType pred2
- ; let { pred1'' = tidyPred tidy_env pred1'; pred2'' = tidyPred tidy_env pred2' }
- ; let msg = vcat [ptext SLIT("When using functional dependencies to combine"),
- nest 2 (sep [ppr pred1'' <> comma, nest 2 from1]),
- nest 2 (sep [ppr pred2'' <> comma, nest 2 from2])]
- ; return (tidy_env, msg) }
-\end{code}
-
-The main context-reduction function is @reduce@. Here's its game plan.
-
-\begin{code}
-reduceList :: RedEnv -> [Inst] -> Avails -> TcM Avails
-reduceList env@(RedEnv {red_stack = (n,stk)}) wanteds state
- = do { dopts <- getDOpts
-#ifdef DEBUG
- ; if n > 8 then
- dumpTcRn (hang (ptext SLIT("Interesting! Context reduction stack depth") <+> int n)
- 2 (ifPprDebug (nest 2 (pprStack stk))))
- else return ()
-#endif
- ; if n >= ctxtStkDepth dopts then
- failWithTc (reduceDepthErr n stk)
- else
- go wanteds state }
- where
- go [] state = return state
- go (w:ws) state = do { state' <- reduce (env {red_stack = (n+1, w:stk)}) w state
- ; go ws state' }
-
- -- Base case: we're done!
-reduce env wanted avails
- -- It's the same as an existing inst, or a superclass thereof
- | Just avail <- findAvail avails wanted
- = returnM avails
-
- | otherwise
- = case red_try_me env wanted of {
- ; Stop -> try_simple (addIrred NoSCs) -- See Note [No superclasses for Stop]
-
- ; ReduceMe want_scs -> -- It should be reduced
- reduceInst env avails wanted `thenM` \ (avails, lookup_result) ->
- case lookup_result of
- NoInstance -> -- No such instance!
- -- Add it and its superclasses
- addIrred want_scs avails wanted
-
- GenInst [] rhs -> addWanted want_scs avails wanted rhs []
-
- GenInst wanteds' rhs -> do { avails1 <- addIrred NoSCs avails wanted
- ; avails2 <- reduceList env wanteds' avails1
- ; addWanted want_scs avails2 wanted rhs wanteds' }
- -- Temporarily do addIrred *before* the reduceList,
- -- which has the effect of adding the thing we are trying
- -- to prove to the database before trying to prove the things it
- -- needs. See note [RECURSIVE DICTIONARIES]
- -- NB: we must not do an addWanted before, because that adds the
- -- superclasses too, and thaat can lead to a spurious loop; see
- -- the examples in [SUPERCLASS-LOOP]
- -- So we do an addIrred before, and then overwrite it afterwards with addWanted
-
- }
- where
- -- First, see if the inst can be reduced to a constant in one step
- -- Works well for literals (1::Int) and constant dictionaries (d::Num Int)
- -- Don't bother for implication constraints, which take real work
- try_simple do_this_otherwise
- = do { res <- lookupSimpleInst wanted
- ; case res of
- GenInst [] rhs -> addWanted AddSCs avails wanted rhs []
- other -> do_this_otherwise avails wanted }
-\end{code}
-
-
-Note [SUPERCLASS-LOOP 2]
-~~~~~~~~~~~~~~~~~~~~~~~~
-But the above isn't enough. Suppose we are *given* d1:Ord a,
-and want to deduce (d2:C [a]) where
-
- class Ord a => C a where
- instance Ord [a] => C [a] where ...
-
-Then we'll use the instance decl to deduce C [a] from Ord [a], and then add the
-superclasses of C [a] to avails. But we must not overwrite the binding
-for Ord [a] (which is obtained from Ord a) with a superclass selection or we'll just
-build a loop!
-
-Here's another variant, immortalised in tcrun020
- class Monad m => C1 m
- class C1 m => C2 m x
- instance C2 Maybe Bool
-For the instance decl we need to build (C1 Maybe), and it's no good if
-we run around and add (C2 Maybe Bool) and its superclasses to the avails
-before we search for C1 Maybe.
-
-Here's another example
- class Eq b => Foo a b
- instance Eq a => Foo [a] a
-If we are reducing
- (Foo [t] t)
-
-we'll first deduce that it holds (via the instance decl). We must not
-then overwrite the Eq t constraint with a superclass selection!
-
-At first I had a gross hack, whereby I simply did not add superclass constraints
-in addWanted, though I did for addGiven and addIrred. This was sub-optimal,
-becuase it lost legitimate superclass sharing, and it still didn't do the job:
-I found a very obscure program (now tcrun021) in which improvement meant the
-simplifier got two bites a the cherry... so something seemed to be an Stop
-first time, but reducible next time.
-
-Now we implement the Right Solution, which is to check for loops directly
-when adding superclasses. It's a bit like the occurs check in unification.
-
-
-Note [RECURSIVE DICTIONARIES]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Consider
- data D r = ZeroD | SuccD (r (D r));
-
- instance (Eq (r (D r))) => Eq (D r) where
- ZeroD == ZeroD = True
- (SuccD a) == (SuccD b) = a == b
- _ == _ = False;
-
- equalDC :: D [] -> D [] -> Bool;
- equalDC = (==);
-
-We need to prove (Eq (D [])). Here's how we go:
-
- d1 : Eq (D [])
-
-by instance decl, holds if
- d2 : Eq [D []]
- where d1 = dfEqD d2
-
-by instance decl of Eq, holds if
- d3 : D []
- where d2 = dfEqList d3
- d1 = dfEqD d2
-
-But now we can "tie the knot" to give
-
- d3 = d1
- d2 = dfEqList d3
- d1 = dfEqD d2
-
-and it'll even run! The trick is to put the thing we are trying to prove
-(in this case Eq (D []) into the database before trying to prove its
-contributing clauses.
-
-
-%************************************************************************
-%* *
- Reducing a single constraint
-%* *
-%************************************************************************
-
-\begin{code}
----------------------------------------------
-reduceInst :: RedEnv -> Avails -> Inst -> TcM (Avails, LookupInstResult)
-reduceInst env avails (ImplicInst { tci_tyvars = tvs, tci_reft = reft, tci_loc = loc,
- tci_given = extra_givens, tci_wanted = wanteds })
- = reduceImplication env avails reft tvs extra_givens wanteds loc
-
-reduceInst env avails other_inst
- = do { result <- lookupSimpleInst other_inst
- ; return (avails, result) }
-\end{code}
-
-\begin{code}
----------------------------------------------
-reduceImplication :: RedEnv
- -> Avails
- -> Refinement -- May refine the givens; often empty
- -> [TcTyVar] -- Quantified type variables; all skolems
- -> [Inst] -- Extra givens; all rigid
- -> [Inst] -- Wanted
- -> InstLoc
- -> TcM (Avails, LookupInstResult)
-\end{code}
-
-Suppose we are simplifying the constraint
- forall bs. extras => wanted
-in the context of an overall simplification problem with givens 'givens',
-and refinment 'reft'.
-
-Note that
- * The refinement is often empty
-
- * The 'extra givens' need not mention any of the quantified type variables
- e.g. forall {}. Eq a => Eq [a]
- forall {}. C Int => D (Tree Int)
-
- This happens when you have something like
- data T a where
- T1 :: Eq a => a -> T a
-
- f :: T a -> Int
- f x = ...(case x of { T1 v -> v==v })...
-
-\begin{code}
- -- ToDo: should we instantiate tvs? I think it's not necessary
- --
- -- ToDo: what about improvement? There may be some improvement
- -- exposed as a result of the simplifications done by reduceList
- -- which are discarded if we back off.
- -- This is almost certainly Wrong, but we'll fix it when dealing
- -- better with equality constraints
-reduceImplication env orig_avails reft tvs extra_givens wanteds inst_loc
- = do { -- Add refined givens, and the extra givens
- (refined_red_givens, avails)
- <- if isEmptyRefinement reft then return (red_givens env, orig_avails)
- else foldlM (addRefinedGiven reft) ([], orig_avails) (red_givens env)
- ; avails <- foldlM addGiven avails extra_givens
-
- -- Solve the sub-problem
- ; let try_me inst = ReduceMe AddSCs -- Note [Freeness and implications]
- env' = env { red_givens = refined_red_givens ++ extra_givens
- , red_try_me = try_me }
-
- ; traceTc (text "reduceImplication" <+> vcat
- [ ppr orig_avails,
- ppr (red_givens env), ppr extra_givens,
- ppr reft, ppr wanteds, ppr avails ])
- ; avails <- reduceList env' wanteds avails
-
- -- Extract the results
- -- Note [Reducing implication constraints]
- ; (binds, irreds) <- extractResults avails wanteds
- ; let (outer, inner) = partition (isJust . findAvail orig_avails) irreds
-
- ; traceTc (text "reduceImplication result" <+> vcat
- [ ppr outer, ppr inner, 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
-
- ; if isEmptyLHsBinds binds && null outer then -- No progress
- return (ret_avails, NoInstance)
- else do
- { (implic_insts, bind) <- makeImplicationBind inst_loc tvs reft extra_givens inner
-
- ; 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 | [wanted] <- wanteds = HsVar (instToId wanted)
- | otherwise = ExplicitTuple (map (L loc . HsVar . instToId) wanteds) Boxed
-
- ; return (ret_avails, GenInst (implic_insts ++ outer) (L loc rhs))
- } }
-\end{code}
-
-Note [Reducing implication constraints]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Suppose we are trying to simplify
- (Ord a, 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
- Ord a -> Irred
-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
-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
-
-The 'depending on' part of the Rhs is important, because it drives
-the extractResults code.
-
-The "inside" and "outside" distinction is what's going on with 'inner' and
-'outer' in reduceImplication
-
-
-Note [Freeness and implications]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-It's hard to say when an implication constraint can be floated out. Consider
- forall {} Eq a => Foo [a]
-The (Foo [a]) doesn't mention any of the quantified variables, but it
-still might be partially satisfied by the (Eq a).
-
-There is a useful special case when it *is* easy to partition the
-constraints, namely when there are no 'givens'. Consider
- forall {a}. () => Bar b
-There are no 'givens', and so there is no reason to capture (Bar b).
-We can let it float out. But if there is even one constraint we
-must be much more careful:
- forall {a}. C a b => Bar (m b)
-because (C a b) might have a superclass (D b), from which we might
-deduce (Bar [b]) when m later gets instantiated to []. Ha!
-
-Here is an even more exotic example
- class C a => D a b
-Now consider the constraint
- forall b. D Int b => C Int
-We can satisfy the (C Int) from the superclass of D, so we don't want
-to float the (C Int) out, even though it mentions no type variable in
-the constraints!
-
-Note [Pruning the givens in an implication constraint]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Suppose we are about to form the implication constraint
- forall tvs. Eq a => Ord b
-The (Eq a) cannot contribute to the (Ord b), because it has no access to
-the type variable 'b'. So we could filter out the (Eq a) from the givens.
-
-Doing so would be a bit tidier, but all the implication constraints get
-simplified away by the optimiser, so it's no great win. So I don't take
-advantage of that at the moment.
-
-If you do, BE CAREFUL of wobbly type variables.
-
-
-%************************************************************************
-%* *
- Avails and AvailHow: the pool of evidence
-%* *
-%************************************************************************
-
-
-\begin{code}
-data Avails = Avails !ImprovementDone !AvailEnv
-
-type ImprovementDone = Bool -- True <=> some unification has happened
- -- so some Irreds might now be reducible
- -- keys that are now
-
-type AvailEnv = FiniteMap Inst AvailHow
-data AvailHow
- = IsIrred -- Used for irreducible dictionaries,
- -- which are going to be lambda bound
-
- | Given TcId -- Used for dictionaries for which we have a binding
- -- e.g. those "given" in a signature
-
- | Rhs -- Used when there is a RHS
- (LHsExpr TcId) -- The RHS
- [Inst] -- Insts free in the RHS; we need these too
-
-instance Outputable Avails where
- ppr = pprAvails
-
-pprAvails (Avails imp avails)
- = vcat [ ptext SLIT("Avails") <> (if imp then ptext SLIT("[improved]") else empty)
- , nest 2 (vcat [sep [ppr inst, nest 2 (equals <+> ppr avail)]
- | (inst,avail) <- fmToList avails ])]
-
-instance Outputable AvailHow where
- ppr = pprAvail
-
--------------------------
-pprAvail :: AvailHow -> SDoc
-pprAvail IsIrred = text "Irred"
-pprAvail (Given x) = text "Given" <+> ppr x
-pprAvail (Rhs rhs bs) = text "Rhs" <+> sep [ppr rhs, braces (ppr bs)]
-
--------------------------
-extendAvailEnv :: AvailEnv -> Inst -> AvailHow -> AvailEnv
-extendAvailEnv env inst avail = addToFM env inst avail
-
-findAvailEnv :: AvailEnv -> Inst -> Maybe AvailHow
-findAvailEnv env wanted = lookupFM env wanted
- -- NB 1: the Ord instance of Inst compares by the class/type info
- -- *not* by unique. So
- -- d1::C Int == d2::C Int
-
-emptyAvails :: Avails
-emptyAvails = Avails False emptyFM
-
-findAvail :: Avails -> Inst -> Maybe AvailHow
-findAvail (Avails _ avails) wanted = findAvailEnv avails wanted
-
-elemAvails :: Inst -> Avails -> Bool
-elemAvails wanted (Avails _ avails) = wanted `elemFM` avails
-
-extendAvails :: Avails -> Inst -> AvailHow -> TcM Avails
--- Does improvement
-extendAvails avails@(Avails imp env) inst avail
- = do { imp1 <- tcImproveOne avails inst -- Do any improvement
- ; return (Avails (imp || imp1) (extendAvailEnv env inst avail)) }
-
-availsInsts :: Avails -> [Inst]
-availsInsts (Avails _ avails) = keysFM avails
-
-availsImproved (Avails imp _) = imp
-
-updateImprovement :: Avails -> Avails -> Avails
--- (updateImprovement a1 a2) sets a1's improvement flag from a2
-updateImprovement (Avails _ avails1) (Avails imp2 _) = Avails imp2 avails1
-\end{code}
-
-Extracting the bindings from a bunch of Avails.
-The bindings do *not* come back sorted in dependency order.
-We assume that they'll be wrapped in a big Rec, so that the
-dependency analyser can sort them out later
-
-\begin{code}
-extractResults :: Avails
- -> [Inst] -- Wanted
- -> TcM ( TcDictBinds, -- Bindings
- [Inst]) -- Irreducible ones
-
-extractResults (Avails _ avails) wanteds
- = go avails emptyBag [] wanteds
- where
- go :: AvailEnv -> TcDictBinds -> [Inst] -> [Inst]
- -> TcM (TcDictBinds, [Inst])
- go avails binds irreds []
- = returnM (binds, irreds)
-
- go avails binds irreds (w:ws)
- = case findAvailEnv avails w of
- Nothing -> pprTrace "Urk: extractResults" (ppr w) $
- go avails binds irreds ws
-
- Just (Given id)
- | 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!
-
- Just IsIrred -> go (add_given avails w) binds (w: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_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 id rhs = binds `unionBags` unitBag (L (getSrcSpan id) (VarBind id rhs))
-\end{code}
-
-
-Note [No superclasses for Stop]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-When we decide not to reduce an Inst -- the 'WhatToDo' --- we still
-add it to avails, so that any other equal Insts will be commoned up
-right here. However, we do *not* add superclasses. If we have
- df::Floating a
- dn::Num a
-but a is not bound here, then we *don't* want to derive dn from df
-here lest we lose sharing.
-
-\begin{code}
-addWanted :: WantSCs -> Avails -> Inst -> LHsExpr TcId -> [Inst] -> TcM Avails
-addWanted want_scs avails wanted rhs_expr wanteds
- = addAvailAndSCs want_scs avails wanted avail
- where
- avail = Rhs rhs_expr wanteds
-
-addGiven :: Avails -> Inst -> TcM Avails
-addGiven avails given = addAvailAndSCs AddSCs avails given (Given (instToId given))
- -- Always add superclasses for 'givens'
- --
- -- No ASSERT( not (given `elemAvails` avails) ) because in an instance
- -- decl for Ord t we can add both Ord t and Eq t as 'givens',
- -- so the assert isn't true
-
-addRefinedGiven :: Refinement -> ([Inst], Avails) -> Inst -> TcM ([Inst], Avails)
-addRefinedGiven reft (refined_givens, avails) given
- | isDict given -- We sometimes have 'given' methods, but they
- -- are always optional, so we can drop them
- , let pred = dictPred given
- , isRefineablePred pred -- See Note [ImplicInst rigidity]
- , Just (co, pred) <- refinePred reft pred
- = do { new_given <- newDictBndr (instLoc given) pred
- ; let rhs = L (instSpan given) $
- HsWrap (WpCo co) (HsVar (instToId given))
- ; avails <- addAvailAndSCs AddSCs avails new_given (Rhs rhs [given])
- ; return (new_given:refined_givens, avails) }
- -- ToDo: the superclasses of the original given all exist in Avails
- -- so we could really just cast them, but it's more awkward to do,
- -- and hopefully the optimiser will spot the duplicated work
- | otherwise
- = return (refined_givens, avails)
-\end{code}
-
-Note [ImplicInst rigidity]
-~~~~~~~~~~~~~~~~~~~~~~~~~~
-Consider
- C :: forall ab. (Eq a, Ord b) => b -> T a
-
- ...(case x of C v -> <body>)...
-
-From the case (where x::T ty) we'll get an implication constraint
- forall b. (Eq ty, Ord b) => <body-constraints>
-Now suppose <body-constraints> itself has an implication constraint
-of form
- forall c. <reft> => <payload>
-Then, we can certainly apply the refinement <reft> to the Ord b, becuase it is
-existential, but we probably should not apply it to the (Eq ty) because it may
-be wobbly. Hence the isRigidInst
-
-@Insts@ are ordered by their class/type info, rather than by their
-unique. This allows the context-reduction mechanism to use standard finite
-maps to do their stuff. It's horrible that this code is here, rather
-than with the Avails handling stuff in TcSimplify
-
-\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 :: WantSCs -> Avails -> Inst -> AvailHow -> TcM Avails
-addAvailAndSCs want_scs avails inst avail
- | not (isClassDict inst) = extendAvails avails inst avail
- | NoSCs <- want_scs = extendAvails avails inst avail
- | otherwise = do { traceTc (text "addAvailAndSCs" <+> vcat [ppr inst, ppr deps])
- ; avails' <- extendAvails avails inst avail
- ; addSCs is_loop avails' inst }
- where
- is_loop pred = any (`tcEqType` mkPredTy pred) dep_tys
- -- Note: this compares by *type*, not by Unique
- deps = findAllDeps (unitVarSet (instToId inst)) avail
- dep_tys = map idType (varSetElems deps)
-
- findAllDeps :: IdSet -> AvailHow -> IdSet
- -- Find all the Insts that this one depends on
- -- See Note [SUPERCLASS-LOOP 2]
- -- Watch out, though. Since the avails may contain loops
- -- (see Note [RECURSIVE DICTIONARIES]), so we need to track the ones we've seen so far
- findAllDeps so_far (Rhs _ kids) = foldl find_all so_far kids
- findAllDeps so_far other = so_far
-
- find_all :: IdSet -> Inst -> IdSet
- find_all so_far kid
- | kid_id `elemVarSet` so_far = so_far
- | Just avail <- findAvail avails kid = findAllDeps so_far' avail
- | otherwise = so_far'
- where
- so_far' = extendVarSet so_far kid_id -- Add the new kid to so_far
- kid_id = instToId kid
-
-addSCs :: (TcPredType -> Bool) -> Avails -> Inst -> TcM Avails
- -- Add all the superclasses of the Inst to Avails
- -- The first param says "dont do this because the original thing
- -- depends on this one, so you'd build a loop"
- -- Invariant: the Inst is already in Avails.
-
-addSCs is_loop avails dict
- = ASSERT( isDict dict )
- do { sc_dicts <- newDictBndrs (instLoc dict) sc_theta'
- ; foldlM add_sc avails (zipEqual "add_scs" sc_dicts sc_sels) }
- where
- (clas, tys) = getDictClassTys dict
- (tyvars, sc_theta, sc_sels, _) = classBigSig clas
- sc_theta' = 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]
- | is_given sc_dict = return avails
- | otherwise = do { avails' <- extendAvails avails sc_dict (Rhs sc_sel_rhs [dict])
- ; addSCs is_loop avails' sc_dict }
- where
- sc_sel_rhs = L (instSpan dict) (HsWrap co_fn (HsVar sc_sel))
- co_fn = WpApp (instToId dict) <.> mkWpTyApps tys
-
- is_given :: Inst -> Bool
- is_given sc_dict = case findAvail avails sc_dict of
- Just (Given _) -> True -- Given is cheaper than superclass selection
- other -> False
-\end{code}
-
-%************************************************************************
-%* *
-\section{tcSimplifyTop: defaulting}
-%* *
-%************************************************************************
-
-
-@tcSimplifyTop@ is called once per module to simplify all the constant
-and ambiguous Insts.
-
-We need to be careful of one case. Suppose we have
-
- instance Num a => Num (Foo a b) where ...
-
-and @tcSimplifyTop@ is given a constraint (Num (Foo x y)). Then it'll simplify
-to (Num x), and default x to Int. But what about y??
-
-It's OK: the final zonking stage should zap y to (), which is fine.
-
-
-\begin{code}
-tcSimplifyTop, tcSimplifyInteractive :: [Inst] -> TcM TcDictBinds
-tcSimplifyTop wanteds
- = tc_simplify_top doc False wanteds
- where
- doc = text "tcSimplifyTop"
-
-tcSimplifyInteractive wanteds
- = tc_simplify_top doc True wanteds
- where
- doc = text "tcSimplifyInteractive"
-
--- The TcLclEnv should be valid here, solely to improve
--- error message generation for the monomorphism restriction
-tc_simplify_top doc interactive wanteds
- = do { dflags <- getDOpts
- ; wanteds <- mapM zonkInst wanteds
- ; mapM_ zonkTopTyVar (varSetElems (tyVarsOfInsts wanteds))
-
- ; (irreds1, binds1) <- tryHardCheckLoop doc1 wanteds
- ; (irreds2, binds2) <- approximateImplications doc2 (\d -> True) irreds1
-
- -- Use the defaulting rules to do extra unification
- -- NB: irreds2 are already zonked
- ; (irreds3, binds3) <- disambiguate doc3 interactive dflags irreds2
-
- -- Deal with implicit parameters
- ; let (bad_ips, non_ips) = partition isIPDict irreds3
- (ambigs, others) = partition isTyVarDict non_ips
-
- ; topIPErrs bad_ips -- Can arise from f :: Int -> Int
- -- f x = x + ?y
- ; addNoInstanceErrs others
- ; addTopAmbigErrs ambigs
-
- ; return (binds1 `unionBags` binds2 `unionBags` binds3) }
- where
- doc1 = doc <+> ptext SLIT("(first round)")
- doc2 = doc <+> ptext SLIT("(approximate)")
- doc3 = doc <+> ptext SLIT("(disambiguate)")
-\end{code}
-
-If a dictionary constrains a type variable which is
- * not mentioned in the environment
- * and not mentioned in the type of the expression
-then it is ambiguous. No further information will arise to instantiate
-the type variable; nor will it be generalised and turned into an extra
-parameter to a function.
-
-It is an error for this to occur, except that Haskell provided for
-certain rules to be applied in the special case of numeric types.
-Specifically, if
- * at least one of its classes is a numeric class, and
- * all of its classes are numeric or standard
-then the type variable can be defaulted to the first type in the
-default-type list which is an instance of all the offending classes.
-
-So here is the function which does the work. It takes the ambiguous
-dictionaries and either resolves them (producing bindings) or
-complains. It works by splitting the dictionary list by type
-variable, and using @disambigOne@ to do the real business.
-
-@disambigOne@ assumes that its arguments dictionaries constrain all
-the same type variable.
-
-ADR Comment 20/6/94: I've changed the @CReturnable@ case to default to
-@()@ instead of @Int@. I reckon this is the Right Thing to do since
-the most common use of defaulting is code like:
-\begin{verbatim}
- _ccall_ foo `seqPrimIO` bar
-\end{verbatim}
-Since we're not using the result of @foo@, the result if (presumably)
-@void@.
-
-\begin{code}
-disambiguate :: SDoc -> Bool -> DynFlags -> [Inst] -> TcM ([Inst], TcDictBinds)
- -- Just does unification to fix the default types
- -- The Insts are assumed to be pre-zonked
-disambiguate doc interactive dflags insts
- | null insts
- = return (insts, emptyBag)
-
- | null defaultable_groups
- = do { traceTc (text "disambiguate1" <+> vcat [ppr insts, ppr unaries, ppr bad_tvs, ppr defaultable_groups])
- ; return (insts, emptyBag) }
-
- | otherwise
- = do { -- Figure out what default types to use
- default_tys <- getDefaultTys extended_defaulting ovl_strings
-
- ; traceTc (text "disambiguate1" <+> vcat [ppr insts, ppr unaries, ppr bad_tvs, ppr defaultable_groups])
- ; mapM_ (disambigGroup default_tys) defaultable_groups
-
- -- disambigGroup does unification, hence try again
- ; tryHardCheckLoop doc insts }
-
- where
- extended_defaulting = interactive || dopt Opt_ExtendedDefaultRules dflags
- ovl_strings = dopt Opt_OverloadedStrings dflags
-
- unaries :: [(Inst, Class, TcTyVar)] -- (C tv) constraints
- bad_tvs :: TcTyVarSet -- Tyvars mentioned by *other* constraints
- (unaries, bad_tvs_s) = partitionWith find_unary insts
- bad_tvs = unionVarSets bad_tvs_s
-
- -- Finds unary type-class constraints
- find_unary d@(Dict {tci_pred = ClassP cls [ty]})
- | Just tv <- tcGetTyVar_maybe ty = Left (d,cls,tv)
- find_unary inst = Right (tyVarsOfInst inst)
-
- -- Group by type variable
- defaultable_groups :: [[(Inst,Class,TcTyVar)]]
- defaultable_groups = filter defaultable_group (equivClasses cmp_tv unaries)
- cmp_tv (_,_,tv1) (_,_,tv2) = tv1 `compare` tv2
-
- defaultable_group :: [(Inst,Class,TcTyVar)] -> Bool
- defaultable_group ds@((_,_,tv):_)
- = isTyConableTyVar tv -- Note [Avoiding spurious errors]
- && not (tv `elemVarSet` bad_tvs)
- && defaultable_classes [c | (_,c,_) <- ds]
- defaultable_group [] = panic "defaultable_group"
-
- defaultable_classes clss
- | extended_defaulting = any isInteractiveClass clss
- | otherwise = all is_std_class clss && (any is_num_class clss)
-
- -- In interactive mode, or with -fextended-default-rules,
- -- we default Show a to Show () to avoid graututious errors on "show []"
- isInteractiveClass cls
- = is_num_class cls || (classKey cls `elem` [showClassKey, eqClassKey, ordClassKey])
-
- is_num_class cls = isNumericClass cls || (ovl_strings && (cls `hasKey` isStringClassKey))
- -- is_num_class adds IsString to the standard numeric classes,
- -- when -foverloaded-strings is enabled
-
- 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
-
-disambigGroup default_tys dicts
- = try_default default_tys
- where
- (_,_,tyvar) = head dicts -- Should be non-empty
- classes = [c | (_,c,_) <- dicts]
-
- try_default [] = return ()
- try_default (default_ty : default_tys)
- = tryTcLIE_ (try_default default_tys) $
- do { tcSimplifyDefault [mkClassPred clas [default_ty] | clas <- classes]
- -- This may fail; then the tryTcLIE_ kicks in
- -- Failure here is caused by there being no type in the
- -- default list which can satisfy all the ambiguous classes.
- -- For example, if Real a is reqd, but the only type in the
- -- default list is Int.
-
- -- 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 = []
-\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.
-