-- T1 b' (c : [b]=[b']) (x:Maybe b')
-- -> x `cast` Maybe (sym (right c))
-
-- Generate the refinement for b'=b,
-- and apply to (Maybe b'), to get (Maybe b)
Succeeded refinement = gadtRefine emptyRefinement ex_tvs co_tvs
(\covar -> text "Wanted" <+> ppr (TyVarTy covar) <+> dcolon <+> ppr (EqPred ty1 ty2))
(\co -> text "Given" <+> ppr co <+> dcolon <+> ppr (EqPred ty1 ty2))
pprInst inst = ppr name <> braces (pprUnique (getUnique name)) <+> dcolon
- <+> (braces (ppr (instType inst) <> implicWantedEqs) $$
- ifPprDebug implic_stuff)
+ <+> braces (ppr (instType inst) <> implicWantedEqs)
where
name = instName inst
- (implic_stuff, implicWantedEqs)
- | isImplicInst inst = (ppr (tci_reft inst),
- text " &" <+>
- ppr (filter isEqInst (tci_wanted inst)))
- | otherwise = (empty, empty)
+ implicWantedEqs
+ | isImplicInst inst = text " &" <+>
+ ppr (filter isEqInst (tci_wanted inst))
+ | otherwise = empty
pprInstInFull inst@(EqInst {}) = pprInst inst
pprInstInFull inst = sep [quotes (pprInst inst), nest 2 (pprInstArising inst)]
import TcMType
import TcBinds
import TcSimplify
-import TcGadt
import TcPat
import TcUnify
import TcRnMonad
tcLookupId, tcLookupTyVar, getScopedTyVarBinds,
lclEnvElts, getInLocalScope, findGlobals,
wrongThingErr, pprBinders,
- refineEnvironment,
tcExtendRecEnv, -- For knot-tying
import TcRnMonad
import TcMType
import TcType
-import TcGadt
-- import TcSuspension
import qualified Type
import Var
find_thing _ _ thing = pprPanic "find_thing" (ppr thing)
\end{code}
-\begin{code}
-refineEnvironment
- :: Refinement
- -> Bool -- whether type equations are involved
- -> TcM a
- -> TcM a
--- I don't think I have to refine the set of global type variables in scope
--- Reason: the refinement never increases that set
-refineEnvironment reft otherEquations thing_inside
- | isEmptyRefinement reft -- Common case
- , not otherEquations
- = thing_inside
- | otherwise
- = do { env <- getLclEnv
- ; let le' = mapNameEnv refine (tcl_env env)
- ; setLclEnv (env {tcl_env = le'}) thing_inside }
- where
- refine elt@(ATcId { tct_co = Rigid co, tct_type = ty })
- | Just (co', ty') <- refineType reft ty
- = elt { tct_co = Rigid (WpCo co' <.> co), tct_type = ty' }
- refine elt@(ATcId { tct_co = Wobbly})
--- Main new idea: make wobbly things invisible whenever there
--- is a refinement of any sort
--- | otherEquations
- = elt { tct_co = WobblyInvisible}
- refine (ATyVar tv ty)
- | Just (_, ty') <- refineType reft ty
- = ATyVar tv ty' -- Ignore the coercion that refineType returns
-
- refine elt = elt -- Common case
-\end{code}
-
%************************************************************************
%* *
\subsection{The global tyvars}
import HsSyn
import TcRnMonad
-import TcGadt
import Inst
import TcEnv
import TcPat
import TcUnify
import TcHsType
import TysWiredIn
-import TcGadt
import Type
import Coercion
import StaticFlags
; loc <- getInstLoc origin
; dicts <- newDictBndrs loc theta'
- ; dict_binds <- tcSimplifyCheckPat loc [] ex_tvs' dicts lie_req
+ ; dict_binds <- tcSimplifyCheckPat loc ex_tvs' dicts lie_req
; let res_pat = ConPatOut { pat_con = L con_span data_con,
pat_tvs = ex_tvs',
import TcHsType
import TcMType
import TcMatches
-import TcGadt
import RnTypes
import RnExpr
import IfaceEnv
import Type
import Coercion
import TcType
-import TcGadt
import InstEnv
import FamInstEnv
import IOEnv
Method 34 doubleId [Int] origin
In addition to the basic Haskell variants of 'Inst's, they can now also
-represent implication constraints 'forall tvs. (reft, given) => wanted'
+represent implication constraints 'forall tvs. given => wanted'
and equality constraints 'co :: ty1 ~ ty2'.
NB: Equalities occur in two flavours:
}
| ImplicInst { -- An implication constraint
- -- forall tvs. (reft, given) => wanted
+ -- forall tvs. given => wanted
tci_name :: Name,
tci_tyvars :: [TcTyVar], -- Quantified type variables
- -- Includes coercion variables
- -- mentioned in tci_reft
- tci_reft :: Refinement,
tci_given :: [Inst], -- Only Dicts and EqInsts
-- (no Methods, LitInsts, ImplicInsts)
tci_wanted :: [Inst], -- Only Dicts, EqInst, and ImplicInsts
tci_loc :: InstLoc
}
- -- NB: the tci_given are not necessarily rigid,
- -- although they will be if the tci_reft is non-trivial
- -- NB: the tci_reft is already applied to tci_given and tci_wanted
+ -- NB: the tci_given are not necessarily rigid
| Method {
tci_id :: TcId, -- The Id for the Inst
import Inst
import TcEnv
import InstEnv
-import TcGadt
import TcType
import TcMType
import TcIface
-----------------------------------------------------------
-- tcSimplifyCheckPat is used for existential pattern match
tcSimplifyCheckPat :: InstLoc
- -> [CoVar]
-> [TcTyVar] -- Quantify over these
-> [Inst] -- Given
-> [Inst] -- Wanted
-> TcM TcDictBinds -- Bindings
-tcSimplifyCheckPat loc co_vars qtvs givens wanteds
+tcSimplifyCheckPat loc 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 givens irreds
+ ; implic_bind <- bindIrredsR loc qtvs givens irreds
; return (binds `unionBags` implic_bind) }
-----------------------------------------------------------
-> [Inst] -> [Inst]
-> TcM TcDictBinds
bindIrreds loc qtvs givens irreds
- = bindIrredsR loc qtvs [] givens irreds
+ = bindIrredsR loc qtvs givens irreds
-bindIrredsR :: InstLoc -> [TcTyVar] -> [CoVar] -> [Inst] -> [Inst]
- -> TcM TcDictBinds
+bindIrredsR :: InstLoc -> [TcTyVar] -> [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 givens irreds
+bindIrredsR loc qtvs givens irreds
| null irreds
= return emptyBag
| otherwise
; return real_irreds }
else return irreds
- ; let all_tvs = qtvs ++ co_vars -- Abstract over all these
- ; (implics, bind) <- makeImplicationBind loc all_tvs givens' irreds'
+ ; (implics, bind) <- makeImplicationBind loc qtvs givens' irreds'
-- This call does the real work
-- If irreds' is empty, it does something sensible
; extendLIEs implics
-- 'givens' must be a simple CoVar. This MUST be cleaned up.
; let name = mkInternalName uniq (mkVarOcc "ic") span
- implic_inst = ImplicInst { tci_name = name, tci_reft = emptyRefinement,
+ implic_inst = ImplicInst { tci_name = name,
tci_tyvars = all_tvs,
tci_given = (eq_givens ++ dict_givens),
tci_wanted = irreds, tci_loc = loc }
--
reduceImplication env
orig_implic@(ImplicInst { tci_name = name, tci_loc = inst_loc,
- tci_tyvars = tvs, tci_reft = emptyRefinement,
+ tci_tyvars = tvs,
tci_given = extra_givens, tci_wanted = wanteds })
= do { -- Solve the sub-problem
; let try_me inst = ReduceMe AddSCs -- Note [Freeness and implications]
add (ClsIE cur_insts cur_tyvar) _ = ClsIE (ins_item : cur_insts)
(ins_tyvar || cur_tyvar)
ins_tyvar = not (any isJust mb_tcs)
-\end{code}
+\end{code}
%************************************************************************
-- They shouldn't because we allocate separate uniques for them
case tcUnifyTys bind_fn tpl_tys tys of
Just _ -> find ms (item:us) rest
- Nothing -> find ms us rest
+ Nothing -> find ms us rest
---------------
bind_fn :: TyVar -> BindFlag
projects / ghc-hetmet.git / commitdiff