tcSimplifyCheck, tcSimplifyRestricted,
tcSimplifyToDicts, tcSimplifyIPs, tcSimplifyTop,
- tcSimplifyThetas, tcSimplifyCheckThetas,
+ tcSimplifyDeriv, tcSimplifyDefault,
bindInstsOfLocalFuns
) where
#include "HsVersions.h"
+import {-# SOURCE #-} TcUnify( unifyTauTy )
+
import HsSyn ( MonoBinds(..), HsExpr(..), andMonoBinds, andMonoBindList )
import TcHsSyn ( TcExpr, TcId,
TcMonoBinds, TcDictBinds
)
import TcMonad
-import Inst ( lookupInst, lookupSimpleInst, LookupInstResult(..),
- tyVarsOfInst, predsOfInsts, predsOfInst,
- isDict, isClassDict, instName,
- isStdClassTyVarDict, isMethodFor,
- instToId, tyVarsOfInsts,
+import Inst ( lookupInst, LookupInstResult(..),
+ tyVarsOfInst, predsOfInsts, predsOfInst, newDicts,
+ isDict, isClassDict, isLinearInst, linearInstType,
+ isStdClassTyVarDict, isMethodFor, isMethod,
+ instToId, tyVarsOfInsts, cloneDict,
+ ipNamesOfInsts, ipNamesOfInst, dictPred,
instBindingRequired, instCanBeGeneralised,
- newDictsFromOld, instMentionsIPs,
+ newDictsFromOld, newMethodAtLoc,
getDictClassTys, isTyVarDict,
instLoc, pprInst, zonkInst, tidyInsts, tidyMoreInsts,
Inst, LIE, pprInsts, pprInstsInFull,
mkLIE, lieToList
)
-import TcEnv ( tcGetGlobalTyVars, tcGetInstEnv )
+import TcEnv ( tcGetGlobalTyVars, tcGetInstEnv, tcLookupGlobalId )
import InstEnv ( lookupInstEnv, classInstEnv, InstLookupResult(..) )
-
-import TcMType ( zonkTcTyVarsAndFV, tcInstTyVars, unifyTauTy )
-import TcType ( ThetaType, PredType, mkClassPred, isOverloadedTy,
- mkTyVarTy, tcGetTyVar, isTyVarClassPred,
- tyVarsOfPred, getClassPredTys_maybe, isClassPred, isIPPred,
- inheritablePred, predHasFDs )
-import Id ( idType )
-import NameSet ( mkNameSet )
+import TcMType ( zonkTcTyVarsAndFV, tcInstTyVars, checkAmbiguity )
+import TcType ( TcTyVar, TcTyVarSet, ThetaType,
+ mkClassPred, isOverloadedTy, mkTyConApp,
+ mkTyVarTy, tcGetTyVar, isTyVarClassPred, mkTyVarTys,
+ tyVarsOfPred, isIPPred, inheritablePred, predHasFDs )
+import Id ( idType, mkUserLocal )
+import Var ( TyVar )
+import Name ( getOccName, getSrcLoc )
+import NameSet ( NameSet, mkNameSet, elemNameSet )
import Class ( classBigSig )
-import FunDeps ( oclose, grow, improve )
-import PrelInfo ( isNumericClass, isCreturnableClass, isCcallishClass )
+import FunDeps ( oclose, grow, improve, pprEquationDoc )
+import PrelInfo ( isNumericClass, isCreturnableClass, isCcallishClass,
+ splitName, fstName, sndName )
import Subst ( mkTopTyVarSubst, substTheta, substTy )
-import TysWiredIn ( unitTy )
+import TysWiredIn ( unitTy, pairTyCon )
import VarSet
import FiniteMap
import Outputable
IDEA is that ?y should be passed at each call site (that's what
dynamic binding means) so we'd better infer the second.
-BOTTOM LINE: you *must* quantify over implicit parameters. See
-isFreeAndInheritable.
+BOTTOM LINE: when *inferring types* you *must* quantify
+over implicit parameters. See the predicate isFreeWhenInferring.
+
-BUT WATCH OUT: for *expressions*, this isn't right. Consider:
+Question 2: type signatures
+~~~~~~~~~~~~~~~~~~~~~~~~~~~
+BUT WATCH OUT: When you supply a type signature, we can't force you
+to quantify over implicit parameters. For example:
(?x + 1) :: Int
tcSimplifyCheck (which *does* allow implicit paramters to be inherited)
and tcSimplifyCheckBind (which does not).
-
-Question 2: type signatures
-~~~~~~~~~~~~~~~~~~~~~~~~~~~
-OK, so is it legal to give an explicit, user type signature to f, thus:
+What about when you supply a type signature for a binding?
+Is it legal to give the following explicit, user type
+signature to f, thus:
f :: Int -> Int
f x = (x::Int) + ?y
Indeed, simply inlining f (at the Haskell source level) would change the
dynamic semantics.
-Conclusion: the above type signature is illegal. You'll get a message
-of the form "could not deduce (?y::Int) from ()".
+Nevertheless, as Launchbury says (email Oct 01) we can't really give the
+semantics for a Haskell program without knowing its typing, so if you
+change the typing you may change the semantics.
+
+To make things consistent in all cases where we are *checking* against
+a supplied signature (as opposed to inferring a type), we adopt the
+rule:
+
+ a signature does not need to quantify over implicit params.
+
+[This represents a (rather marginal) change of policy since GHC 5.02,
+which *required* an explicit signature to quantify over all implicit
+params for the reasons mentioned above.]
+
+But that raises a new question. Consider
+
+ Given (signature) ?x::Int
+ Wanted (inferred) ?x::Int, ?y::Bool
+
+Clearly we want to discharge the ?x and float the ?y out. But
+what is the criterion that distinguishes them? Clearly it isn't
+what free type variables they have. The Right Thing seems to be
+to float a constraint that
+ neither mentions any of the quantified type variables
+ nor any of the quantified implicit parameters
+
+See the predicate isFreeWhenChecking.
Question 3: monomorphism
qtvs = grow preds tau_tvs' `minusVarSet` oclose preds gbl_tvs
try_me inst
- | isFreeAndInheritable qtvs inst = Free
- | isClassDict inst = DontReduceUnlessConstant -- Dicts
- | otherwise = ReduceMe -- Lits and Methods
+ | isFreeWhenInferring qtvs inst = Free
+ | isClassDict inst = DontReduceUnlessConstant -- Dicts
+ | otherwise = ReduceMe -- Lits and Methods
in
-- Step 2
reduceContext doc try_me [] wanteds' `thenTc` \ (no_improvement, frees, binds, irreds) ->
--
-- Hence the (irreds ++ frees)
+ -- However, NOTICE that when we are done, we might have some bindings, but
+ -- the final qtvs might be empty. See [NO TYVARS] below.
+
inferLoop doc tau_tvs (irreds ++ frees) `thenTc` \ (qtvs1, frees1, binds1, irreds1) ->
returnTc (qtvs1, frees1, binds `AndMonoBinds` binds1, irreds1)
\end{code}
on both the Lte and If constraints. What we *can't* do is start again
with (Max Z (S x) y)!
-\begin{code}
-isFreeAndInheritable qtvs inst
- = isFree qtvs inst -- Constrains no quantified vars
- && all inheritablePred (predsOfInst inst) -- And no implicit parameter involved
- -- (see "Notes on implicit parameters")
+[NO TYVARS]
+
+ class Y a b | a -> b where
+ y :: a -> X b
+
+ instance Y [[a]] a where
+ y ((x:_):_) = X x
+
+ k :: X a -> X a -> X a
-isFree qtvs inst
- = not (tyVarsOfInst inst `intersectsVarSet` qtvs)
+ g :: Num a => [X a] -> [X a]
+ g xs = h xs
+ where
+ h ys = ys ++ map (k (y [[0]])) xs
+
+The excitement comes when simplifying the bindings for h. Initially
+try to simplify {y @ [[t1]] t2, 0 @ t1}, with initial qtvs = {t2}.
+From this we get t1:=:t2, but also various bindings. We can't forget
+the bindings (because of [LOOP]), but in fact t1 is what g is
+polymorphic in.
+
+The net effect of [NO TYVARS]
+
+\begin{code}
+isFreeWhenInferring :: TyVarSet -> Inst -> Bool
+isFreeWhenInferring qtvs inst
+ = isFreeWrtTyVars qtvs inst -- Constrains no quantified vars
+ && all inheritablePred (predsOfInst inst) -- And no implicit parameter involved
+ -- (see "Notes on implicit parameters")
+
+isFreeWhenChecking :: TyVarSet -- Quantified tyvars
+ -> NameSet -- Quantified implicit parameters
+ -> Inst -> Bool
+isFreeWhenChecking qtvs ips inst
+ = isFreeWrtTyVars qtvs inst
+ && isFreeWrtIPs ips inst
+
+isFreeWrtTyVars qtvs inst = not (tyVarsOfInst inst `intersectsVarSet` qtvs)
+isFreeWrtIPs ips inst = not (any (`elemNameSet` ips) (ipNamesOfInst inst))
\end{code}
-> TcM (LIE, -- Free
TcDictBinds) -- Bindings
--- tcSimplifyCheck is used when checking exprssion type signatures,
+-- tcSimplifyCheck is used when checking expression type signatures,
-- class decls, instance decls etc.
-- Note that we psss isFree (not isFreeAndInheritable) to tcSimplCheck
-- It's important that we can float out non-inheritable predicates
-- Example: (?x :: Int) is ok!
tcSimplifyCheck doc qtvs givens wanted_lie
- = tcSimplCheck doc isFree get_qtvs
+ = tcSimplCheck doc get_qtvs
givens wanted_lie `thenTc` \ (qtvs', frees, binds) ->
returnTc (frees, binds)
where
TcDictBinds) -- Bindings
tcSimplifyInferCheck doc tau_tvs givens wanted_lie
- = tcSimplCheck doc isFreeAndInheritable get_qtvs givens wanted_lie
+ = tcSimplCheck doc get_qtvs givens wanted_lie
where
-- Figure out which type variables to quantify over
-- You might think it should just be the signature tyvars,
Here is the workhorse function for all three wrappers.
\begin{code}
-tcSimplCheck doc is_free get_qtvs givens wanted_lie
+tcSimplCheck doc get_qtvs givens wanted_lie
= check_loop givens (lieToList wanted_lie) `thenTc` \ (qtvs, frees, binds, irreds) ->
-- Complain about any irreducible ones
returnTc (qtvs, mkLIE frees, binds)
where
+ ip_set = mkNameSet (ipNamesOfInsts givens)
+
check_loop givens wanteds
= -- Step 1
mapNF_Tc zonkInst givens `thenNF_Tc` \ givens' ->
let
-- When checking against a given signature we always reduce
-- until we find a match against something given, or can't reduce
- try_me inst | is_free qtvs' inst = Free
- | otherwise = ReduceMe
+ try_me inst | isFreeWhenChecking qtvs' ip_set inst = Free
+ | otherwise = ReduceMe
in
reduceContext doc try_me givens' wanteds' `thenTc` \ (no_improvement, frees, binds, irreds) ->
--
-- 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 isFreeAndInheritable) in which we quantify over
+ -- 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
mapNF_Tc zonkInst (lieToList wanted_lie) `thenNF_Tc` \ wanteds' ->
let
- try_me inst | isFree qtvs inst = Free
- | otherwise = ReduceMe
+ try_me inst | isFreeWrtTyVars qtvs inst = Free
+ | otherwise = ReduceMe
in
reduceContext doc try_me [] wanteds' `thenTc` \ (no_improvement, frees, binds, irreds) ->
ASSERT( no_improvement )
= simpl_loop given_ips wanteds `thenTc` \ (frees, binds) ->
returnTc (mkLIE frees, binds)
where
- doc = text "tcSimplifyIPs" <+> ppr ip_names
+ doc = text "tcSimplifyIPs" <+> ppr given_ips
wanteds = lieToList wanted_lie
- ip_names = map instName given_ips
- ip_set = mkNameSet ip_names
+ ip_set = mkNameSet (ipNamesOfInsts given_ips)
-- Simplify any methods that mention the implicit parameter
- try_me inst | inst `instMentionsIPs` ip_set = ReduceMe
- | otherwise = Free
+ try_me inst | isFreeWrtIPs ip_set inst = Free
+ | otherwise = ReduceMe
simpl_loop givens wanteds
= mapNF_Tc zonkInst givens `thenNF_Tc` \ givens' ->
| Free -- Return as free
+reduceMe :: Inst -> WhatToDo
+reduceMe inst = ReduceMe
+
data WantSCs = NoSCs | AddSCs -- Tells whether we should add the superclasses
-- of a predicate when adding it to the avails
\end{code}
\begin{code}
-type RedState = (Avails, -- What's available
- [Inst]) -- Insts for which try_me returned Free
-
type Avails = FiniteMap Inst Avail
data Avail
- = Irred -- Used for irreducible dictionaries,
+ = IsFree -- Used for free Insts
+ | Irred -- Used for irreducible dictionaries,
-- which are going to be lambda bound
- | BoundTo TcId -- Used for dictionaries for which we have a binding
+ | Given TcId -- Used for dictionaries for which we have a binding
-- e.g. those "given" in a signature
+ Bool -- True <=> actually consumed (splittable IPs only)
| NoRhs -- Used for Insts like (CCallable f)
-- where no witness is required.
TcExpr -- The RHS
[Inst] -- Insts free in the RHS; we need these too
-pprAvails avails = vcat [ppr inst <+> equals <+> pprAvail avail
+ | Linear -- Splittable Insts only.
+ Int -- The Int is always 2 or more; indicates how
+ -- many copies are required
+ Inst -- The splitter
+ Avail -- Where the "master copy" is
+
+ | LinRhss -- Splittable Insts only; this is used only internally
+ -- by extractResults, where a Linear
+ -- is turned into an LinRhss
+ [TcExpr] -- A supply of suitable RHSs
+
+pprAvails avails = vcat [sep [ppr inst, nest 2 (equals <+> pprAvail avail)]
| (inst,avail) <- fmToList avails ]
instance Outputable Avail where
ppr = pprAvail
-pprAvail NoRhs = text "<no rhs>"
-pprAvail Irred = text "Irred"
-pprAvail (BoundTo x) = text "Bound to" <+> ppr x
-pprAvail (Rhs rhs bs) = ppr rhs <+> braces (ppr bs)
+pprAvail NoRhs = text "<no rhs>"
+pprAvail IsFree = text "Free"
+pprAvail Irred = text "Irred"
+pprAvail (Given x b) = text "Given" <+> ppr x <+>
+ if b then text "(used)" else empty
+pprAvail (Rhs rhs bs) = text "Rhs" <+> ppr rhs <+> braces (ppr bs)
+pprAvail (Linear n i a) = text "Linear" <+> ppr n <+> braces (ppr i) <+> ppr a
+pprAvail (LinRhss rhss) = text "LinRhss" <+> ppr rhss
\end{code}
Extracting the bindings from a bunch of Avails.
The loop startes
\begin{code}
-bindsAndIrreds :: Avails
+extractResults :: Avails
-> [Inst] -- Wanted
- -> (TcDictBinds, -- Bindings
- [Inst]) -- Irreducible ones
+ -> NF_TcM (TcDictBinds, -- Bindings
+ [Inst], -- Irreducible ones
+ [Inst]) -- Free ones
-bindsAndIrreds avails wanteds
- = go avails EmptyMonoBinds [] wanteds
+extractResults avails wanteds
+ = go avails EmptyMonoBinds [] [] wanteds
where
- go avails binds irreds [] = (binds, irreds)
+ go avails binds irreds frees []
+ = returnNF_Tc (binds, irreds, frees)
- go avails binds irreds (w:ws)
+ go avails binds irreds frees (w:ws)
= case lookupFM avails w of
- Nothing -> -- Free guys come out here
- -- (If we didn't do addFree we could use this as the
- -- criterion for free-ness, and pick up the free ones here too)
- go avails binds irreds ws
+ Nothing -> pprTrace "Urk: extractResults" (ppr w) $
+ go avails binds irreds frees ws
- Just NoRhs -> go avails binds irreds ws
+ Just NoRhs -> go avails binds irreds frees ws
+ Just IsFree -> go (add_free avails w) binds irreds (w:frees) ws
+ Just Irred -> go (add_given avails w) binds (w:irreds) frees ws
- Just Irred -> go (addToFM avails w (BoundTo (instToId w))) binds (w:irreds) ws
-
- Just (BoundTo id) -> go avails new_binds irreds ws
+ Just (Given id _) -> go avails new_binds irreds frees ws
where
- -- For implicit parameters, all occurrences share the same
- -- Id, so there is no need for synonym bindings
- new_binds | new_id == id = binds
- | otherwise = addBind binds new_id (HsVar id)
- new_id = instToId w
+ new_binds | id == instToId w = binds
+ | otherwise = addBind binds w (HsVar id)
+ -- 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 avails' (addBind binds id rhs) irreds (ws' ++ ws)
+ Just (Rhs rhs ws') -> go (add_given avails w) new_binds irreds frees (ws' ++ ws)
where
- id = instToId w
- avails' = addToFM avails w (BoundTo id)
-
-addBind binds id rhs = binds `AndMonoBinds` VarMonoBind id rhs
+ new_binds = addBind binds w rhs
+
+ Just (LinRhss (rhs:rhss)) -- Consume one of the Rhss
+ -> go new_avails new_binds irreds frees ws
+ where
+ new_binds = addBind binds w rhs
+ new_avails = addToFM avails w (LinRhss rhss)
+
+ Just (Linear n split_inst avail)
+ -> split n (instToId split_inst) avail w `thenNF_Tc` \ (binds', (rhs:rhss), irreds') ->
+ go (addToFM avails w (LinRhss rhss))
+ (binds `AndMonoBinds` addBind binds' w rhs)
+ (irreds' ++ irreds) frees (split_inst:ws)
+
+
+ add_given avails w
+ | instBindingRequired w = addToFM avails w (Given (instToId w) True)
+ | otherwise = addToFM avails w NoRhs
+ -- NB: make sure that CCallable/CReturnable use NoRhs rather
+ -- than Given, else we end up with bogus bindings.
+
+ add_free avails w | isMethod w = avails
+ | otherwise = add_given avails w
+ -- NB: Hack alert!
+ -- Do *not* replace Free by Given if it's a method.
+ -- The following situation shows why this is bad:
+ -- truncate :: forall a. RealFrac a => forall b. Integral b => a -> b
+ -- From an application (truncate f i) we get
+ -- t1 = truncate at f
+ -- t2 = t1 at i
+ -- If we have also have a second occurrence of truncate, we get
+ -- t3 = truncate at f
+ -- t4 = t3 at i
+ -- When simplifying with i,f free, we might still notice that
+ -- t1=t3; but alas, the binding for t2 (which mentions t1)
+ -- will continue to float out!
+ -- (split n i a) returns: n rhss
+ -- auxiliary bindings
+ -- 1 or 0 insts to add to irreds
+
+
+split :: Int -> TcId -> Avail -> Inst
+ -> NF_TcM (TcDictBinds, [TcExpr], [Inst])
+-- (split n split_id avail wanted) returns
+-- * a list of 'n' expressions, all of which witness 'avail'
+-- * a bunch of auxiliary bindings to support these expressions
+-- * one or zero insts needed to witness the whole lot
+-- (maybe be zero if the initial Inst is a Given)
+split n split_id avail wanted
+ = go n
+ where
+ ty = linearInstType wanted
+ pair_ty = mkTyConApp pairTyCon [ty,ty]
+ id = instToId wanted
+ occ = getOccName id
+ loc = getSrcLoc id
+
+ go 1 = case avail of
+ Given id _ -> returnNF_Tc (EmptyMonoBinds, [HsVar id], [])
+ Irred -> cloneDict wanted `thenNF_Tc` \ w' ->
+ returnNF_Tc (EmptyMonoBinds, [HsVar (instToId w')], [w'])
+
+ go n = go ((n+1) `div` 2) `thenNF_Tc` \ (binds1, rhss, irred) ->
+ expand n rhss `thenNF_Tc` \ (binds2, rhss') ->
+ returnNF_Tc (binds1 `AndMonoBinds` binds2, rhss', irred)
+
+ -- (expand n rhss)
+ -- Given ((n+1)/2) rhss, make n rhss, using auxiliary bindings
+ -- e.g. expand 3 [rhs1, rhs2]
+ -- = ( { x = split rhs1 },
+ -- [fst x, snd x, rhs2] )
+ expand n rhss
+ | n `rem` 2 == 0 = go rhss -- n is even
+ | otherwise = go (tail rhss) `thenNF_Tc` \ (binds', rhss') ->
+ returnNF_Tc (binds', head rhss : rhss')
+ where
+ go rhss = mapAndUnzipNF_Tc do_one rhss `thenNF_Tc` \ (binds', rhss') ->
+ returnNF_Tc (andMonoBindList binds', concat rhss')
+
+ do_one rhs = tcGetUnique `thenNF_Tc` \ uniq ->
+ tcLookupGlobalId fstName `thenNF_Tc` \ fst_id ->
+ tcLookupGlobalId sndName `thenNF_Tc` \ snd_id ->
+ let
+ x = mkUserLocal occ uniq pair_ty loc
+ in
+ returnNF_Tc (VarMonoBind x (mk_app split_id rhs),
+ [mk_fs_app fst_id ty x, mk_fs_app snd_id ty x])
+
+mk_fs_app id ty var = HsVar id `TyApp` [ty,ty] `HsApp` HsVar var
+
+mk_app id rhs = HsApp (HsVar id) rhs
+
+addBind binds inst rhs = binds `AndMonoBinds` VarMonoBind (instToId inst) rhs
\end{code}
])) `thenNF_Tc_`
-- Build the Avail mapping from "givens"
- foldlNF_Tc addGiven (emptyFM, []) givens `thenNF_Tc` \ init_state ->
+ foldlNF_Tc addGiven emptyFM givens `thenNF_Tc` \ init_state ->
-- Do the real work
- reduceList (0,[]) try_me wanteds init_state `thenNF_Tc` \ state@(avails, frees) ->
+ reduceList (0,[]) try_me wanteds init_state `thenNF_Tc` \ avails ->
-- Do improvement, using everything in avails
-- In particular, avails includes all superclasses of everything
tcImprove avails `thenTc` \ no_improvement ->
+ extractResults avails wanteds `thenNF_Tc` \ (binds, irreds, frees) ->
+
traceTc (text "reduceContext end" <+> (vcat [
text "----------------------",
doc,
text "no_improvement =" <+> ppr no_improvement,
text "----------------------"
])) `thenNF_Tc_`
- let
- (binds, irreds) = bindsAndIrreds avails wanteds
- in
- returnTc (no_improvement, frees, binds, irreds)
+
+ returnTc (no_improvement, frees, binds, irreds)
tcImprove avails
= tcGetInstEnv `thenTc` \ inst_env ->
if null eqns then
returnTc True
else
- traceTc (ptext SLIT("Improve:") <+> vcat (map ppr_eqn eqns)) `thenNF_Tc_`
+ traceTc (ptext SLIT("Improve:") <+> vcat (map pprEquationDoc eqns)) `thenNF_Tc_`
mapTc_ unify eqns `thenTc_`
returnTc False
where
= tcAddErrCtxt doc $
tcInstTyVars (varSetElems qtvs) `thenNF_Tc` \ (_, _, tenv) ->
unifyTauTy (substTy tenv t1) (substTy tenv t2)
- ppr_eqn ((qtvs, t1, t2), doc)
- = vcat [ptext SLIT("forall") <+> braces (pprWithCommas ppr (varSetElems qtvs))
- <+> ppr t1 <+> ptext SLIT(":=:") <+> ppr t2,
- nest 2 doc]
\end{code}
The main context-reduction function is @reduce@. Here's its game plan.
-- along with its depth
-> (Inst -> WhatToDo)
-> [Inst]
- -> RedState
- -> TcM RedState
+ -> Avails
+ -> TcM Avails
\end{code}
@reduce@ is passed
Free return this in "frees"
wanteds: The list of insts to reduce
- state: An accumulating parameter of type RedState
+ state: An accumulating parameter of type Avails
that contains the state of the algorithm
- It returns a RedState.
+ It returns a Avails.
The (n,stack) pair is just used for error reporting.
n is always the depth of the stack.
-- Base case: we're done!
reduce stack try_me wanted state
-- It's the same as an existing inst, or a superclass thereof
- | isAvailable state wanted
- = returnTc state
+ | Just avail <- isAvailable state wanted
+ = if isLinearInst wanted then
+ addLinearAvailable state avail wanted `thenNF_Tc` \ (state', wanteds') ->
+ reduceList stack try_me wanteds' state'
+ else
+ returnTc state -- No op for non-linear things
| otherwise
= case try_me wanted of {
\begin{code}
-isAvailable :: RedState -> Inst -> Bool
-isAvailable (avails, _) wanted = wanted `elemFM` avails
- -- NB: the Ord instance of Inst compares by the class/type info
+-------------------------
+isAvailable :: Avails -> Inst -> Maybe Avail
+isAvailable avails wanted = lookupFM avails wanted
+ -- NB 1: the Ord instance of Inst compares by the class/type info
-- *not* by unique. So
-- d1::C Int == d2::C Int
+addLinearAvailable :: Avails -> Avail -> Inst -> NF_TcM (Avails, [Inst])
+addLinearAvailable avails avail wanted
+ | need_split avail
+ = tcLookupGlobalId splitName `thenNF_Tc` \ split_id ->
+ newMethodAtLoc (instLoc wanted) split_id
+ [linearInstType wanted] `thenNF_Tc` \ (split_inst,_) ->
+ returnNF_Tc (addToFM avails wanted (Linear 2 split_inst avail), [split_inst])
+
+ | otherwise
+ = returnNF_Tc (addToFM avails wanted avail', [])
+ where
+ avail' = case avail of
+ Given id _ -> Given id True
+ Linear n i a -> Linear (n+1) i a
+
+ need_split Irred = True
+ need_split (Given _ used) = used
+ need_split (Linear _ _ _) = False
+
-------------------------
-addFree :: RedState -> Inst -> NF_TcM RedState
+addFree :: Avails -> Inst -> NF_TcM Avails
-- When an Inst is tossed upstairs as 'free' we nevertheless add it
-- to avails, so that any other equal Insts will be commoned up right
-- here rather than also being tossed upstairs. This is really just
-- but a is not bound here, then we *don't* want to derive
-- dn from df here lest we lose sharing.
--
- -- NB2: do *not* add the Inst to avails at all if it's a method.
- -- The following situation shows why this is bad:
- -- truncate :: forall a. RealFrac a => forall b. Integral b => a -> b
- -- From an application (truncate f i) we get
- -- t1 = truncate at f
- -- t2 = t1 at i
- -- If we have also have a second occurrence of truncate, we get
- -- t3 = truncate at f
- -- t4 = t3 at i
- -- When simplifying with i,f free, we might still notice that
- -- t1=t3; but alas, the binding for t2 (which mentions t1)
- -- will continue to float out!
- -- Solution: never put methods in avail till they are captured
- -- in which case addFree isn't used
- --
- -- NB3: make sure that CCallable/CReturnable use NoRhs rather
- -- than BoundTo, else we end up with bogus bindings.
- -- c.f. instBindingRequired in addWanted
-addFree (avails, frees) free
- | isDict free = returnNF_Tc (addToFM avails free avail, free:frees)
- | otherwise = returnNF_Tc (avails, free:frees)
- where
- avail | instBindingRequired free = BoundTo (instToId free)
- | otherwise = NoRhs
+addFree avails free = returnNF_Tc (addToFM avails free IsFree)
-addWanted :: RedState -> Inst -> TcExpr -> [Inst] -> NF_TcM RedState
-addWanted state@(avails, frees) wanted rhs_expr wanteds
+addWanted :: Avails -> Inst -> TcExpr -> [Inst] -> NF_TcM Avails
+addWanted avails wanted rhs_expr wanteds
-- Do *not* add superclasses as well. Here's an example of why not
-- class Eq a => Foo a b
-- instance Eq a => Foo [a] a
-- ToDo: this isn't entirely unsatisfactory, because
-- we may also lose some entirely-legitimate sharing this way
- = ASSERT( not (isAvailable state wanted) )
- returnNF_Tc (addToFM avails wanted avail, frees)
+ = ASSERT( not (wanted `elemFM` avails) )
+ returnNF_Tc (addToFM avails wanted avail)
where
avail | instBindingRequired wanted = Rhs rhs_expr wanteds
| otherwise = ASSERT( null wanteds ) NoRhs
-addGiven :: RedState -> Inst -> NF_TcM RedState
-addGiven state given = addAvailAndSCs state given (BoundTo (instToId given))
-
-addIrred :: WantSCs -> RedState -> Inst -> NF_TcM RedState
-addIrred NoSCs (avails,frees) irred = returnNF_Tc (addToFM avails irred Irred, frees)
-addIrred AddSCs state irred = addAvailAndSCs state irred Irred
+addGiven :: Avails -> Inst -> NF_TcM Avails
+addGiven state given = addAvailAndSCs state given (Given (instToId given) False)
-addAvailAndSCs :: RedState -> Inst -> Avail -> NF_TcM RedState
-addAvailAndSCs (avails, frees) wanted avail
- = add_avail_and_scs avails wanted avail `thenNF_Tc` \ avails' ->
- returnNF_Tc (avails', frees)
+addIrred :: WantSCs -> Avails -> Inst -> NF_TcM Avails
+addIrred NoSCs state irred = returnNF_Tc (addToFM state irred Irred)
+addIrred AddSCs state irred = addAvailAndSCs state irred Irred
----------------------
-add_avail_and_scs :: Avails -> Inst -> Avail -> NF_TcM Avails
-add_avail_and_scs avails wanted avail
+addAvailAndSCs :: Avails -> Inst -> Avail -> NF_TcM Avails
+addAvailAndSCs avails wanted avail
= add_scs (addToFM avails wanted avail) wanted
add_scs :: Avails -> Inst -> NF_TcM Avails
add_sc avails (sc_dict, sc_sel) -- Add it, and its superclasses
= case lookupFM avails sc_dict of
- Just (BoundTo _) -> returnNF_Tc avails -- See Note [SUPER] below
- other -> add_avail_and_scs avails sc_dict avail
+ Just (Given _ _) -> returnNF_Tc avails -- See Note [SUPER] below
+ other -> addAvailAndSCs avails sc_dict avail
where
sc_sel_rhs = DictApp (TyApp (HsVar sc_sel) tys) [instToId dict]
avail = Rhs sc_sel_rhs [dict]
Then we'll use the instance decl to deduce C [a] and then add the
superclasses of C [a] to avails. But we must not overwrite the binding
for d1:Ord a (which is given) with a superclass selection or we'll just
-build a loop! Hence looking for BoundTo. Crudely, BoundTo is cheaper
+build a loop! Hence looking for Given. Crudely, Given is cheaper
than a selection.
%************************************************************************
-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.
-
@tcSimplifyTop@ is called once per module to simplify all the constant
and ambiguous Insts.
\begin{code}
tcSimplifyTop :: LIE -> TcM TcDictBinds
tcSimplifyTop wanted_lie
- = simpleReduceLoop (text "tcSimplTop") try_me wanteds `thenTc` \ (frees, binds, irreds) ->
+ = simpleReduceLoop (text "tcSimplTop") reduceMe wanteds `thenTc` \ (frees, binds, irreds) ->
ASSERT( null frees )
let
returnTc (binds `andMonoBinds` andMonoBindList binds_ambig)
where
wanteds = lieToList wanted_lie
- try_me inst = ReduceMe
d1 `cmp_by_tyvar` d2 = get_tv d1 `compare` get_tv d2
(clas, [ty]) -> clas
\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.
try_default (default_ty : default_tys)
= tryTc_ (try_default default_tys) $ -- If default_ty fails, we try
-- default_tys instead
- tcSimplifyCheckThetas [] theta `thenTc` \ _ ->
+ tcSimplifyDefault theta `thenTc` \ _ ->
returnTc default_ty
where
theta = [mkClassPred clas [default_ty] | clas <- classes]
-- Bind the type variable and reduce the context, for real this time
unifyTauTy chosen_default_ty (mkTyVarTy tyvar) `thenTc_`
simpleReduceLoop (text "disambig" <+> ppr dicts)
- try_me dicts `thenTc` \ (frees, binds, ambigs) ->
+ reduceMe dicts `thenTc` \ (frees, binds, ambigs) ->
WARN( not (null frees && null ambigs), ppr frees $$ ppr ambigs )
warnDefault dicts chosen_default_ty `thenTc_`
returnTc binds
returnTc EmptyMonoBinds
where
- try_me inst = ReduceMe -- This reduce should not fail
tyvar = get_tv (head dicts) -- Should be non-empty
classes = map get_clas dicts
\end{code}
instance declarations.
\begin{code}
-tcSimplifyThetas :: ThetaType -- Wanted
- -> TcM ThetaType -- Needed
-
-tcSimplifyThetas wanteds
- = doptsTc Opt_GlasgowExts `thenNF_Tc` \ glaExts ->
- reduceSimple [] wanteds `thenNF_Tc` \ irreds ->
+tcSimplifyDeriv :: [TyVar]
+ -> ThetaType -- Wanted
+ -> TcM ThetaType -- Needed
+
+tcSimplifyDeriv tyvars theta
+ = tcInstTyVars tyvars `thenNF_Tc` \ (tvs, _, tenv) ->
+ -- The main loop may do unification, and that may crash if
+ -- it doesn't see a TcTyVar, so we have to instantiate. Sigh
+ -- ToDo: what if two of them do get unified?
+ newDicts DataDeclOrigin (substTheta tenv theta) `thenNF_Tc` \ wanteds ->
+ simpleReduceLoop doc reduceMe wanteds `thenTc` \ (frees, _, irreds) ->
+ ASSERT( null frees ) -- reduceMe never returns Free
+
+ doptsTc Opt_AllowUndecidableInstances `thenNF_Tc` \ undecidable_ok ->
let
- -- For multi-param Haskell, check that the returned dictionaries
- -- don't have any of the form (C Int Bool) for which
- -- we expect an instance here
- -- For Haskell 98, check that all the constraints are of the form C a,
- -- where a is a type variable
- bad_guys | glaExts = [pred | pred <- irreds,
- isEmptyVarSet (tyVarsOfPred pred)]
- | otherwise = [pred | pred <- irreds,
- not (isTyVarClassPred pred)]
+ tv_set = mkVarSet tvs
+ simpl_theta = map dictPred irreds -- reduceMe squashes all non-dicts
+
+ check_pred pred
+ | isEmptyVarSet pred_tyvars -- Things like (Eq T) should be rejected
+ = addErrTc (noInstErr pred)
+
+ | not undecidable_ok && not (isTyVarClassPred pred)
+ -- Check that the returned dictionaries are all of form (C a b)
+ -- (where a, b are type variables).
+ -- We allow this if we had -fallow-undecidable-instances,
+ -- but note that risks non-termination in the 'deriving' context-inference
+ -- fixpoint loop. It is useful for situations like
+ -- data Min h a = E | M a (h a)
+ -- which gives the instance decl
+ -- instance (Eq a, Eq (h a)) => Eq (Min h a)
+ = addErrTc (noInstErr pred)
+
+ | not (pred_tyvars `subVarSet` tv_set)
+ -- Check for a bizarre corner case, when the derived instance decl should
+ -- have form instance C a b => D (T a) where ...
+ -- Note that 'b' isn't a parameter of T. This gives rise to all sorts
+ -- of problems; in particular, it's hard to compare solutions for
+ -- equality when finding the fixpoint. So I just rule it out for now.
+ = addErrTc (badDerivedPred pred)
+
+ | otherwise
+ = returnNF_Tc ()
+ where
+ pred_tyvars = tyVarsOfPred pred
+
+ rev_env = mkTopTyVarSubst tvs (mkTyVarTys tyvars)
+ -- This reverse-mapping is a Royal Pain,
+ -- but the result should mention TyVars not TcTyVars
in
- if null bad_guys then
- returnTc irreds
- else
- mapNF_Tc addNoInstErr bad_guys `thenNF_Tc_`
- failTc
+
+ mapNF_Tc check_pred simpl_theta `thenNF_Tc_`
+ checkAmbiguity tvs simpl_theta tv_set `thenTc_`
+ returnTc (substTheta rev_env simpl_theta)
+ where
+ doc = ptext SLIT("deriving classes for a data type")
\end{code}
-@tcSimplifyCheckThetas@ just checks class-type constraints, essentially;
+@tcSimplifyDefault@ just checks class-type constraints, essentially;
used with \tr{default} declarations. We are only interested in
whether it worked or not.
\begin{code}
-tcSimplifyCheckThetas :: ThetaType -- Given
- -> ThetaType -- Wanted
- -> TcM ()
-
-tcSimplifyCheckThetas givens wanteds
- = reduceSimple givens wanteds `thenNF_Tc` \ irreds ->
+tcSimplifyDefault :: ThetaType -- Wanted; has no type variables in it
+ -> TcM ()
+
+tcSimplifyDefault theta
+ = newDicts DataDeclOrigin theta `thenNF_Tc` \ wanteds ->
+ simpleReduceLoop doc reduceMe wanteds `thenTc` \ (frees, _, irreds) ->
+ ASSERT( null frees ) -- try_me never returns Free
+ mapNF_Tc (addErrTc . noInstErr) irreds `thenNF_Tc_`
if null irreds then
- returnTc ()
+ returnTc ()
else
- mapNF_Tc addNoInstErr irreds `thenNF_Tc_`
- failTc
-\end{code}
-
-
-\begin{code}
-type AvailsSimple = FiniteMap PredType Bool
- -- True => irreducible
- -- False => given, or can be derived from a given or from an irreducible
-
-reduceSimple :: ThetaType -- Given
- -> ThetaType -- Wanted
- -> NF_TcM ThetaType -- Irreducible
-
-reduceSimple givens wanteds
- = reduce_simple (0,[]) givens_fm wanteds `thenNF_Tc` \ givens_fm' ->
- returnNF_Tc [pred | (pred,True) <- fmToList givens_fm']
- where
- givens_fm = foldl addNonIrred emptyFM givens
-
-reduce_simple :: (Int,ThetaType) -- Stack
- -> AvailsSimple
- -> ThetaType
- -> NF_TcM AvailsSimple
-
-reduce_simple (n,stack) avails wanteds
- = go avails wanteds
+ failTc
where
- go avails [] = returnNF_Tc avails
- go avails (w:ws) = reduce_simple_help (n+1,w:stack) avails w `thenNF_Tc` \ avails' ->
- go avails' ws
-
-reduce_simple_help stack givens wanted
- | wanted `elemFM` givens
- = returnNF_Tc givens
-
- | Just (clas, tys) <- getClassPredTys_maybe wanted
- = lookupSimpleInst clas tys `thenNF_Tc` \ maybe_theta ->
- case maybe_theta of
- Nothing -> returnNF_Tc (addSimpleIrred givens wanted)
- Just theta -> reduce_simple stack (addNonIrred givens wanted) theta
-
- | otherwise
- = returnNF_Tc (addSimpleIrred givens wanted)
-
-addSimpleIrred :: AvailsSimple -> PredType -> AvailsSimple
-addSimpleIrred givens pred
- = addSCs (addToFM givens pred True) pred
-
-addNonIrred :: AvailsSimple -> PredType -> AvailsSimple
-addNonIrred givens pred
- = addSCs (addToFM givens pred False) pred
-
-addSCs givens pred
- | not (isClassPred pred) = givens
- | otherwise = foldl add givens sc_theta
- where
- Just (clas,tys) = getClassPredTys_maybe pred
- (tyvars, sc_theta_tmpl, _, _) = classBigSig clas
- sc_theta = substTheta (mkTopTyVarSubst tyvars tys) sc_theta_tmpl
-
- add givens ct
- = case lookupFM givens ct of
- Nothing -> -- Add it and its superclasses
- addSCs (addToFM givens ct False) ct
-
- Just True -> -- Set its flag to False; superclasses already done
- addToFM givens ct False
-
- Just False -> -- Already done
- givens
-
+ doc = ptext SLIT("default declaration")
\end{code}
pprInstsInFull tidy_dicts]
complainCheck doc givens irreds
- = mapNF_Tc zonkInst given_dicts `thenNF_Tc` \ givens' ->
+ = mapNF_Tc zonkInst given_dicts_and_ips `thenNF_Tc` \ givens' ->
mapNF_Tc (addNoInstanceErrs doc givens') (groupInsts irreds) `thenNF_Tc_`
returnNF_Tc ()
where
- given_dicts = filter isDict givens
+ given_dicts_and_ips = filter (not . isMethod) givens
-- Filter out methods, which are only added to
-- the given set as an optimisation
addNoInstanceErrs what_doc givens dicts
- = tcGetInstEnv `thenNF_Tc` \ inst_env ->
+ = getDOptsTc `thenNF_Tc` \ dflags ->
+ tcGetInstEnv `thenNF_Tc` \ inst_env ->
let
(tidy_env1, tidy_givens) = tidyInsts givens
(tidy_env2, tidy_dicts) = tidyMoreInsts tidy_env1 dicts
ambig_overlap = any ambig_overlap1 dicts
ambig_overlap1 dict
| isClassDict dict
- = case lookupInstEnv inst_env clas tys of
+ = case lookupInstEnv dflags inst_env clas tys of
NoMatch ambig -> ambig
other -> False
| otherwise = False
addInstErrTcM (instLoc (head dicts)) (tidy_env2, doc)
-- Used for the ...Thetas variants; all top level
-addNoInstErr pred
- = addErrTc (ptext SLIT("No instance for") <+> quotes (ppr pred))
+noInstErr pred = ptext SLIT("No instance for") <+> quotes (ppr pred)
+
+badDerivedPred pred
+ = vcat [ptext SLIT("Can't derive instances where the instance context mentions"),
+ ptext SLIT("type variables that are not data type parameters"),
+ nest 2 (ptext SLIT("Offending constraint:") <+> ppr pred)]
reduceDepthErr n stack
= vcat [ptext SLIT("Context reduction stack overflow; size =") <+> int n,
projects / ghc-hetmet.git / blobdiff