+Type functions
+~~~~~~~~~~~~~~
+* A Given inst should be a CoVar, not a coercion
+
+* finaliseEqInst should not need to call zonk
+
+* Why do we need fromGivenEqDict? How could we construct
+ a Dict that had an EqPred?
+ newDictBndr should make an EqInst directly
+
+* tc_co should be accessed only inside Inst
+
+* Inst.mkImplicTy needs a commment about filtering out EqInsts
+ How *do* we deal with wanted equalities?
+
+* Inst.instType behaves inconsistently for EqInsts: it should
+ return an EqPred, like the instType' hack in pprDictsTheta
+
+ Consequences: adjust the uses of instType in TcSimplify
+
+* tcDeref* functions are unused, except in tcGenericNormalizeFamInst, when
+ we can equally well use TcMType.lookupTcTyVar
+
+* Coercion.mkEqPredCoI looks very peculiar.
+
+
+
-------------------------
*** unexpected failure for jtod_circint(opt)
do we need to assign to Node?
--------------------------
-* Relation between separate type sigs and pattern type sigs
-f :: forall a. a->a
-f :: b->b = e -- No: monomorphic
-
-f :: forall a. a->a
-f :: forall a. a->a -- OK
-
-f :: forall a. [a] -> [a]
-f :: forall b. b->b = e ???
-
-
-------------------------------
NB: all floats are let-binds, but some non-rec lets
may be unlifted (with RHS ok-for-speculation)
-Right hand sides and arguments
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-In many ways we want to treat
- (a) the right hand side of a let(rec), and
- (b) a function argument
-in the same way. But not always! In particular, we would
-like to leave these arguments exactly as they are, so they
-will match a RULE more easily.
-
- f (g x, h x)
- g (+ x)
-
-It's harder to make the rule match if we ANF-ise the constructor,
-or eta-expand the PAP:
-
- f (let { a = g x; b = h x } in (a,b))
- g (\y. + x y)
-
-On the other hand if we see the let-defns
-
- p = (g x, h x)
- q = + x
-
-then we *do* want to ANF-ise and eta-expand, so that p and q
-can be safely inlined.
-
-Even floating lets out is a bit dubious. For let RHS's we float lets
-out if that exposes a value, so that the value can be inlined more vigorously.
-For example
-
- r = let x = e in (x,x)
-
-Here, if we float the let out we'll expose a nice constructor. We did experiments
-that showed this to be a generally good thing. But it was a bad thing to float
-lets out unconditionally, because that meant they got allocated more often.
-
-For function arguments, there's less reason to expose a constructor (it won't
-get inlined). Just possibly it might make a rule match, but I'm pretty skeptical.
-So for the moment we don't float lets out of function arguments either.
-
Eta expansion
~~~~~~~~~~~~~~
dataConRepType, dataConSig, dataConFullSig,
dataConName, dataConIdentity, dataConTag, dataConTyCon, dataConUserType,
dataConUnivTyVars, dataConExTyVars, dataConAllTyVars,
- dataConEqSpec, eqSpecPreds, dataConTheta, dataConStupidTheta,
+ dataConEqSpec, eqSpecPreds, dataConEqTheta, dataConDictTheta, dataConStupidTheta,
dataConInstArgTys, dataConOrigArgTys, dataConOrigResTy,
- dataConInstOrigArgTys, dataConRepArgTys,
+ dataConInstOrigArgTys, dataConInstOrigDictsAndArgTys,
+ dataConRepArgTys,
dataConFieldLabels, dataConFieldType,
dataConStrictMarks, dataConExStricts,
dataConSourceArity, dataConRepArity,
import Data.Char
import Data.Word
+import Data.List ( partition )
\end{code}
--
-- *** As declared by the user
-- data T a where
- -- MkT :: forall x y. (Ord x) => x -> y -> T (x,y)
+ -- MkT :: forall x y. (x~y,Ord x) => x -> y -> T (x,y)
-- *** As represented internally
-- data T a where
- -- MkT :: forall a. forall x y. (a:=:(x,y), Ord x) => x -> y -> T a
+ -- MkT :: forall a. forall x y. (a:=:(x,y),x~y,Ord x) => x -> y -> T a
--
-- The next six fields express the type of the constructor, in pieces
-- e.g.
-- dcUnivTyVars = [a]
-- dcExTyVars = [x,y]
-- dcEqSpec = [a:=:(x,y)]
- -- dcTheta = [Ord x]
+ -- dcEqTheta = [x~y]
+ -- dcDictTheta = [Ord x]
-- dcOrigArgTys = [a,List b]
-- dcRepTyCon = T
-- Its type is of form
-- forall a1..an . t1 -> ... tm -> T a1..an
-- No existentials, no coercions, nothing.
- -- That is: dcExTyVars = dcEqSpec = dcTheta = []
+ -- That is: dcExTyVars = dcEqSpec = dcEqTheta = dcDictTheta = []
-- NB 1: newtypes always have a vanilla data con
-- NB 2: a vanilla constructor can still be declared in GADT-style
-- syntax, provided its type looks like the above.
-- Each equality is of the form (a :=: ty), where 'a' is one of
-- the universally quantified type variables
- dcTheta :: ThetaType, -- The context of the constructor
+ -- The next two fields give the type context of the data constructor
+ -- (aside from the GADT constraints,
+ -- which are given by the dcExpSpec)
-- In GADT form, this is *exactly* what the programmer writes, even if
-- the context constrains only universally quantified variables
- -- MkT :: forall a. Eq a => a -> T a
- -- It may contain user-written equality predicates too
+ -- MkT :: forall a b. (a ~ b, Ord b) => a -> T a b
+ dcEqTheta :: ThetaType, -- The *equational* constraints
+ dcDictTheta :: ThetaType, -- The *type-class and implicit-param* constraints
dcStupidTheta :: ThetaType, -- The context of the data type declaration
-- data Eq a => T a = ...
-- so the error is detected properly... it's just that asaertions here
-- are a little dodgy.
- = ASSERT( not (any isEqPred theta) )
+ = -- ASSERT( not (any isEqPred theta) )
-- We don't currently allow any equality predicates on
-- a data constructor (apart from the GADT ones in eq_spec)
con
dcVanilla = is_vanilla, dcInfix = declared_infix,
dcUnivTyVars = univ_tvs, dcExTyVars = ex_tvs,
dcEqSpec = eq_spec,
- dcStupidTheta = stupid_theta, dcTheta = theta,
+ dcStupidTheta = stupid_theta,
+ dcEqTheta = eq_theta, dcDictTheta = dict_theta,
dcOrigArgTys = orig_arg_tys, dcOrigResTy = orig_res_ty,
dcRepTyCon = tycon,
dcRepArgTys = rep_arg_tys,
-- The 'arg_stricts' passed to mkDataCon are simply those for the
-- source-language arguments. We add extra ones for the
-- dictionary arguments right here.
- dict_tys = mkPredTys theta
- real_arg_tys = dict_tys ++ orig_arg_tys
- real_stricts = map mk_dict_strict_mark theta ++ arg_stricts
+ (eq_theta,dict_theta) = partition isEqPred theta
+ dict_tys = mkPredTys dict_theta
+ real_arg_tys = dict_tys ++ orig_arg_tys
+ real_stricts = map mk_dict_strict_mark dict_theta ++ arg_stricts
-- Example
-- data instance T (b,c) where
-- The representation tycon looks like this:
-- data :R7T b c where
-- TI :: forall b1 c1. (b1 ~ c1) => b1 -> :R7T b1 c1
+ -- In this case orig_res_ty = T (e,e)
orig_res_ty = mkFamilyTyConApp tycon (substTyVars (mkTopTvSubst eq_spec) univ_tvs)
-- Representation arguments and demands
tag = assoc "mkDataCon" (tyConDataCons tycon `zip` [fIRST_TAG..]) con
ty = mkForAllTys univ_tvs $ mkForAllTys ex_tvs $
mkFunTys (mkPredTys (eqSpecPreds eq_spec)) $
+ mkFunTys (mkPredTys eq_theta) $
-- NB: the dict args are already in rep_arg_tys
-- because they might be flattened..
-- but the equality predicates are not
dataConEqSpec :: DataCon -> [(TyVar,Type)]
dataConEqSpec = dcEqSpec
-dataConTheta :: DataCon -> ThetaType
-dataConTheta = dcTheta
+dataConEqTheta :: DataCon -> ThetaType
+dataConEqTheta = dcEqTheta
+
+dataConDictTheta :: DataCon -> ThetaType
+dataConDictTheta = dcDictTheta
dataConWorkId :: DataCon -> Id
dataConWorkId dc = case dcIds dc of
dataConExStricts :: DataCon -> [StrictnessMark]
-- Strictness of *existential* arguments only
-- Usually empty, so we don't bother to cache this
-dataConExStricts dc = map mk_dict_strict_mark (dcTheta dc)
+dataConExStricts dc = map mk_dict_strict_mark $ dcDictTheta dc
dataConSourceArity :: DataCon -> Arity
-- Source-level arity of the data constructor
dataConSig :: DataCon -> ([TyVar], ThetaType, [Type], Type)
dataConSig (MkData {dcUnivTyVars = univ_tvs, dcExTyVars = ex_tvs, dcEqSpec = eq_spec,
- dcTheta = theta, dcOrigArgTys = arg_tys, dcOrigResTy = res_ty})
- = (univ_tvs ++ ex_tvs, eqSpecPreds eq_spec ++ theta, arg_tys, res_ty)
+ dcEqTheta = eq_theta, dcDictTheta = dict_theta, dcOrigArgTys = arg_tys, dcOrigResTy = res_ty})
+ = (univ_tvs ++ ex_tvs, eqSpecPreds eq_spec ++ eq_theta ++ dict_theta, arg_tys, res_ty)
dataConFullSig :: DataCon
- -> ([TyVar], [TyVar], [(TyVar,Type)], ThetaType, [Type], Type)
+ -> ([TyVar], [TyVar], [(TyVar,Type)], ThetaType, ThetaType, [Type], Type)
dataConFullSig (MkData {dcUnivTyVars = univ_tvs, dcExTyVars = ex_tvs, dcEqSpec = eq_spec,
- dcTheta = theta, dcOrigArgTys = arg_tys, dcOrigResTy = res_ty})
- = (univ_tvs, ex_tvs, eq_spec, theta, arg_tys, res_ty)
+ dcEqTheta = eq_theta, dcDictTheta = dict_theta, dcOrigArgTys = arg_tys, dcOrigResTy = res_ty})
+ = (univ_tvs, ex_tvs, eq_spec, eq_theta, dict_theta, arg_tys, res_ty)
dataConOrigResTy :: DataCon -> Type
dataConOrigResTy dc = dcOrigResTy dc
-- mentions the family tycon, not the internal one.
dataConUserType (MkData { dcUnivTyVars = univ_tvs,
dcExTyVars = ex_tvs, dcEqSpec = eq_spec,
- dcTheta = theta, dcOrigArgTys = arg_tys,
+ dcEqTheta = eq_theta, dcDictTheta = dict_theta, dcOrigArgTys = arg_tys,
dcOrigResTy = res_ty })
= mkForAllTys ((univ_tvs `minusList` map fst eq_spec) ++ ex_tvs) $
- mkFunTys (mkPredTys theta) $
+ mkFunTys (mkPredTys eq_theta) $
+ mkFunTys (mkPredTys dict_theta) $
mkFunTys arg_tys $
res_ty
map (substTyWith tyvars inst_tys) arg_tys
where
tyvars = univ_tvs ++ ex_tvs
+
+dataConInstOrigDictsAndArgTys
+ :: DataCon -- Works for any DataCon
+ -> [Type] -- Includes existential tyvar args, but NOT
+ -- equality constraints or dicts
+ -> [Type] -- Returns just the instsantiated dicts and *value* arguments
+dataConInstOrigDictsAndArgTys dc@(MkData {dcOrigArgTys = arg_tys,
+ dcDictTheta = dicts,
+ dcUnivTyVars = univ_tvs,
+ dcExTyVars = ex_tvs}) inst_tys
+ = ASSERT2( length tyvars == length inst_tys
+ , ptext SLIT("dataConInstOrigDictsAndArgTys") <+> ppr dc $$ ppr tyvars $$ ppr inst_tys )
+ map (substTyWith tyvars inst_tys) (mkPredTys dicts ++ arg_tys)
+ where
+ tyvars = univ_tvs ++ ex_tvs
\end{code}
These two functions get the real argument types of the constructor,
import TysWiredIn
import PrelRules
import Type
+import TypeRep
import TcGadt
import Coercion
import TcType
import ForeignCall
import DataCon
import Id
-import Var ( Var, TyVar)
+import Var ( Var, TyVar, mkCoVar)
import IdInfo
import NewDemand
import DmdAnal
= DCIds Nothing wrk_id
where
(univ_tvs, ex_tvs, eq_spec,
- theta, orig_arg_tys, res_ty) = dataConFullSig data_con
+ eq_theta, dict_theta, orig_arg_tys, res_ty) = dataConFullSig data_con
tycon = dataConTyCon data_con -- The representation TyCon (not family)
----------- Worker (algebraic data types only) --------------
nt_work_info = noCafIdInfo -- The NoCaf-ness is set by noCafIdInfo
`setArityInfo` 1 -- Arity 1
`setUnfoldingInfo` newtype_unf
- newtype_unf = ASSERT( isVanillaDataCon data_con &&
- isSingleton orig_arg_tys )
+ newtype_unf = -- The assertion below is no longer correct:
+ -- there may be a dict theta rather than a singleton orig_arg_ty
+ -- ASSERT( isVanillaDataCon data_con &&
+ -- isSingleton orig_arg_tys )
+ --
-- No existentials on a newtype, but it can have a context
-- e.g. newtype Eq a => T a = MkT (...)
mkCompulsoryUnfolding $
wrapNewTypeBody tycon res_ty_args
(Var id_arg1)
- id_arg1 = ASSERT( not (null orig_arg_tys) ) mkTemplateLocal 1 (head orig_arg_tys)
+ id_arg1 = mkTemplateLocal 1
+ (if null orig_arg_tys
+ then ASSERT(not (null $ dataConDictTheta data_con)) mkPredTy $ head (dataConDictTheta data_con)
+ else head orig_arg_tys
+ )
----------- Wrapper --------------
-- We used to include the stupid theta in the wrapper's args
-- extra constraints where necessary.
wrap_tvs = (univ_tvs `minusList` map fst eq_spec) ++ ex_tvs
res_ty_args = substTyVars (mkTopTvSubst eq_spec) univ_tvs
- dict_tys = mkPredTys theta
- wrap_ty = mkForAllTys wrap_tvs $ mkFunTys dict_tys $
+ eq_tys = mkPredTys eq_theta
+ dict_tys = mkPredTys dict_theta
+ wrap_ty = mkForAllTys wrap_tvs $ mkFunTys eq_tys $ mkFunTys dict_tys $
mkFunTys orig_arg_tys $ res_ty
-- NB: watch out here if you allow user-written equality
-- constraints in data constructor signatures
wrap_unf = mkTopUnfolding $ Note InlineMe $
mkLams wrap_tvs $
+ mkLams eq_args $
mkLams dict_args $ mkLams id_args $
foldr mk_case con_app
(zip (dict_args ++ id_args) all_strict_marks)
Var wrk_id `mkTyApps` res_ty_args
`mkVarApps` ex_tvs
`mkTyApps` map snd eq_spec -- Equality evidence
+ `mkVarApps` eq_args
`mkVarApps` reverse rep_ids
(dict_args,i2) = mkLocals 1 dict_tys
(id_args,i3) = mkLocals i2 orig_arg_tys
wrap_arity = i3-1
+ (eq_args,_) = mkCoVarLocals i3 eq_tys
+
+ mkCoVarLocals i [] = ([],i)
+ mkCoVarLocals i (x:xs) = let (ys,j) = mkCoVarLocals (i+1) xs
+ y = mkCoVar (mkSysTvName (mkBuiltinUnique i) FSLIT("dc_co")) x
+ in (y:ys,j)
mk_case
:: (Id, StrictnessMark) -- Arg, strictness
has_field con = field_label `elem` dataConFieldLabels con
con1 = ASSERT( not (null data_cons_w_field) ) head data_cons_w_field
- (univ_tvs, _, eq_spec, _, _, data_ty) = dataConFullSig con1
+ (univ_tvs, _, eq_spec, _, _, _, data_ty) = dataConFullSig con1
-- For a data type family, the data_ty (and hence selector_ty) mentions
-- only the family TyCon, not the instance TyCon
data_tv_set = tyVarsOfType data_ty
-- C a -> C a
-- for a single-op class (after all, the selector is the identity)
-- But it's type must expose the representation of the dictionary
- -- to gat (say) C a -> (a -> a)
+ -- to get (say) C a -> (a -> a)
info = noCafIdInfo
`setArityInfo` 1
tycon = classTyCon clas
[data_con] = tyConDataCons tycon
tyvars = dataConUnivTyVars data_con
- arg_tys = ASSERT( isVanillaDataCon data_con ) dataConRepArgTys data_con
+ arg_tys = {- ASSERT( isVanillaDataCon data_con ) -} dataConRepArgTys data_con
+ eq_theta = dataConEqTheta data_con
the_arg_id = assoc "MkId.mkDictSelId" (map idName (classSelIds clas) `zip` arg_ids) name
- pred = mkClassPred clas (mkTyVarTys tyvars)
- (dict_id:arg_ids) = mkTemplateLocals (mkPredTy pred : arg_tys)
+ pred = mkClassPred clas (mkTyVarTys tyvars)
+ dict_id = mkTemplateLocal 1 $ mkPredTy pred
+ (eq_ids,n) = mkCoVarLocals 2 $ mkPredTys eq_theta
+ arg_ids = mkTemplateLocalsNum n arg_tys
+
+ mkCoVarLocals i [] = ([],i)
+ mkCoVarLocals i (x:xs) = let (ys,j) = mkCoVarLocals (i+1) xs
+ y = mkCoVar (mkSysTvName (mkBuiltinUnique i) FSLIT("dc_co")) x
+ in (y:ys,j)
- rhs = mkLams tyvars (Lam dict_id rhs_body)
+ rhs = mkLams tyvars (Lam dict_id rhs_body)
rhs_body | isNewTyCon tycon = unwrapNewTypeBody tycon (map mkTyVarTy tyvars) (Var dict_id)
| otherwise = Case (Var dict_id) dict_id (idType the_arg_id)
- [(DataAlt data_con, arg_ids, Var the_arg_id)]
+ [(DataAlt data_con, eq_ids ++ arg_ids, Var the_arg_id)]
\end{code}
mkTcTyVar :: Name -> Kind -> TcTyVarDetails -> TyVar
mkTcTyVar name kind details
- = ASSERT( not (isCoercionKind kind) )
+ = -- TOM: no longer valid assertion?
+ -- ASSERT( not (isCoercionKind kind) )
TcTyVar { varName = name,
realUnique = getKey# (nameUnique name),
varType = kind,
dataConRepFSInstPat = dataConInstPat dataConRepArgTys
dataConOrigInstPat = dataConInstPat dc_arg_tys (repeat (FSLIT("ipv")))
where
- dc_arg_tys dc = map mkPredTy (dataConTheta dc) ++ dataConOrigArgTys dc
+ dc_arg_tys dc = map mkPredTy (dataConEqTheta dc) ++ map mkPredTy (dataConDictTheta dc) ++ dataConOrigArgTys dc
-- Remember to include the existential dictionaries
dataConInstPat :: (DataCon -> [Type]) -- function used to find arg tys
--
-- co_tvs are intended to be used as binders for coercion args and the kinds
-- of these vars have been instantiated by the inst_tys and the ex_tys
+-- The co_tvs include both GADT equalities (dcEqSpec) and
+-- programmer-specified equalities (dcEqTheta)
--
--- arg_ids are indended to be used as binders for value arguments, including
--- dicts, and their types have been instantiated with inst_tys and ex_tys
+-- arg_ids are indended to be used as binders for value arguments,
+-- and their types have been instantiated with inst_tys and ex_tys
+-- The arg_ids include both dicts (dcDictTheta) and
+-- programmer-specified arguments (after rep-ing) (deRepArgTys)
--
-- Example.
-- The following constructor T1
-- where the double-primed variables are created with the FastStrings and
-- Uniques given as fss and us
dataConInstPat arg_fun fss uniqs con inst_tys
- = (ex_bndrs, co_bndrs, id_bndrs)
+ = (ex_bndrs, co_bndrs, arg_ids)
where
univ_tvs = dataConUnivTyVars con
ex_tvs = dataConExTyVars con
arg_tys = arg_fun con
eq_spec = dataConEqSpec con
- eq_preds = eqSpecPreds eq_spec
+ eq_theta = dataConEqTheta con
+ eq_preds = eqSpecPreds eq_spec ++ eq_theta
n_ex = length ex_tvs
- n_co = length eq_spec
+ n_co = length eq_preds
-- split the Uniques and FastStrings
(ex_uniqs, uniqs') = splitAt n_ex uniqs
-- make value vars, instantiating types
mk_id_var uniq fs ty = mkUserLocal (mkVarOccFS fs) uniq (substTy subst ty) noSrcSpan
- id_bndrs = zipWith3 mk_id_var id_uniqs id_fss arg_tys
+ arg_ids = zipWith3 mk_id_var id_uniqs id_fss arg_tys
exprIsConApp_maybe :: CoreExpr -> Maybe (DataCon, [CoreExpr])
-- Returns (Just (dc, [x1..xn])) if the argument expression is
-- do its magic.
addConstraint :: TcType -> TcType -> TR ()
addConstraint t1 t2 = congruenceNewtypes t1 t2 >>= uncurry unifyType
+ >> return () -- TOMDO: what about the coercion?
+ -- we should consider family instances
val_binds = ValBindsOut [(Recursive, binds)] []
mkHsConApp :: DataCon -> [Type] -> [HsExpr Id] -> LHsExpr Id
--- Used for constructing dictinoary terms etc, so no locations
+-- Used for constructing dictionary terms etc, so no locations
mkHsConApp data_con tys args
= foldl mk_app (nlHsTyApp (dataConWrapId data_con) tys) args
where
import Type
import Coercion
+import TcRnMonad
+import Outputable
+
import Data.List
\end{code}
= Just co_tycon
| otherwise
= Nothing
+ ; traceIf (text "mkNewTyConRhs" <+> ppr cocon_maybe)
; return (NewTyCon { data_con = con,
nt_rhs = rhs_ty,
nt_etad_rhs = (etad_tvs, etad_rhs),
-- non-recursive newtypes
all_coercions = True
tvs = tyConTyVars tycon
- rhs_ty = head (dataConInstOrigArgTys con (mkTyVarTys tvs))
+ rhs_ty = ASSERT(not (null (dataConInstOrigDictsAndArgTys con (mkTyVarTys tvs))))
+ -- head (dataConInstOrigArgTys con (mkTyVarTys tvs))
+ head (dataConInstOrigDictsAndArgTys con (mkTyVarTys tvs))
-- Instantiate the data con with the
-- type variables from the tycon
-- NB: a newtype DataCon has no existentials; hence the
-> TcRnIf m n Class
buildClass class_name tvs sc_theta fds ats sig_stuff tc_isrec
- = do { tycon_name <- newImplicitBinder class_name mkClassTyConOcc
+ = do { traceIf (text "buildClass")
+ ; tycon_name <- newImplicitBinder class_name mkClassTyConOcc
; datacon_name <- newImplicitBinder class_name mkClassDataConOcc
-- The class name is the 'parent' for this datacon, not its tycon,
-- because one should import the class to get the binding for
-- the datacon
- ; sc_sel_names <- mapM (newImplicitBinder class_name . mkSuperDictSelOcc)
- [1..length sc_theta]
- -- We number off the superclass selectors, 1, 2, 3 etc so that we
- -- can construct names for the selectors. Thus
- -- class (C a, C b) => D a b where ...
- -- gives superclass selectors
- -- D_sc1, D_sc2
- -- (We used to call them D_C, but now we can have two different
- -- superclasses both called C!)
; fixM (\ rec_clas -> do { -- Only name generation inside loop
- let { rec_tycon = classTyCon rec_clas
- ; op_tys = [ty | (_,_,ty) <- sig_stuff]
- ; sc_tys = mkPredTys sc_theta
- ; dict_component_tys = sc_tys ++ op_tys
- ; sc_sel_ids = [mkDictSelId sc_name rec_clas | sc_name <- sc_sel_names]
- ; op_items = [ (mkDictSelId op_name rec_clas, dm_info)
- | (op_name, dm_info, _) <- sig_stuff ] }
+ let { rec_tycon = classTyCon rec_clas
+ ; op_tys = [ty | (_,_,ty) <- sig_stuff]
+ ; op_items = [ (mkDictSelId op_name rec_clas, dm_info)
+ | (op_name, dm_info, _) <- sig_stuff ] }
-- Build the selector id and default method id
; dict_con <- buildDataCon datacon_name
False -- Not declared infix
- (map (const NotMarkedStrict) dict_component_tys)
+ (map (const NotMarkedStrict) op_tys)
[{- No labelled fields -}]
tvs [{- no existentials -}]
- [{- No equalities -}] [{-No context-}]
- dict_component_tys
+ [{- No GADT equalities -}] sc_theta
+ op_tys
rec_tycon
- ; rhs <- case dict_component_tys of
- [rep_ty] -> mkNewTyConRhs tycon_name rec_tycon dict_con
- other -> return (mkDataTyConRhs [dict_con])
+ ; sc_sel_names <- mapM (newImplicitBinder class_name . mkSuperDictSelOcc)
+ [1..length (dataConDictTheta dict_con)]
+ -- We number off the Dict superclass selectors, 1, 2, 3 etc so that we
+ -- can construct names for the selectors. Thus
+ -- class (C a, C b) => D a b where ...
+ -- gives superclass selectors
+ -- D_sc1, D_sc2
+ -- (We used to call them D_C, but now we can have two different
+ -- superclasses both called C!)
+ ; let sc_sel_ids = [mkDictSelId sc_name rec_clas | sc_name <- sc_sel_names]
+
+ -- Use a newtype if the class constructor has exactly one field:
+ -- i.e. exactly one operation or superclass taken together
+ -- Watch out: the sc_theta includes equality predicates,
+ -- which don't count for this purpose; hence dataConDictTheta
+ ; rhs <- if ((length $ dataConDictTheta dict_con) + length sig_stuff) == 1
+ then mkNewTyConRhs tycon_name rec_tycon dict_con
+ else return (mkDataTyConRhs [dict_con])
; let { clas_kind = mkArrowKinds (map tyVarKind tvs) liftedTypeKind
-- newtype like a synonym, but that will lead to an infinite
-- type]
; atTyCons = [tycon | ATyCon tycon <- ats]
+
+ ; result = mkClass class_name tvs fds
+ sc_theta sc_sel_ids atTyCons
+ op_items tycon
}
- ; return (mkClass class_name tvs fds
- sc_theta sc_sel_ids atTyCons op_items
- tycon)
+ ; traceIf (text "buildClass" <+> ppr tycon)
+ ; return result
})}
\end{code}
ifConUnivTvs = toIfaceTvBndrs (dataConUnivTyVars data_con),
ifConExTvs = toIfaceTvBndrs (dataConExTyVars data_con),
ifConEqSpec = to_eq_spec (dataConEqSpec data_con),
- ifConCtxt = toIfaceContext (dataConTheta data_con),
+ ifConCtxt = toIfaceContext (dataConEqTheta data_con ++ dataConDictTheta data_con),
ifConArgTys = map toIfaceType (dataConOrigArgTys data_con),
ifConFields = map getOccName
(dataConFieldLabels data_con),
lookupSimpleInst, LookupInstResult(..),
tcExtendLocalInstEnv, tcGetInstEnvs, getOverlapFlag,
+ isAbstractableInst, isEqInst,
isDict, isClassDict, isMethod, isImplicInst,
isIPDict, isInheritableInst, isMethodOrLit,
isTyVarDict, isMethodFor,
zonkInst, zonkInsts,
- instToId, instToVar, instName,
+ instToId, instToVar, instType, instName,
- InstOrigin(..), InstLoc, pprInstLoc
+ InstOrigin(..), InstLoc, pprInstLoc,
+
+ mkWantedCo, mkGivenCo,
+ fromWantedCo, fromGivenCo,
+ eitherEqInst, mkEqInst, mkEqInsts,
+ finalizeEqInst, writeWantedCoercion,
+ eqInstType, updateEqInstCoercion,
+ eqInstCoercion,
+ eqInstLeftTy, eqInstRightTy
) where
#include "HsVersions.h"
import {-# SOURCE #-} TcExpr( tcPolyExpr )
-import {-# SOURCE #-} TcUnify( unifyType )
+import {-# SOURCE #-} TcUnify( boxyUnify, unifyType )
import FastString(FastString)
import HsSyn
import TcMType
import TcType
import Type
+import TypeRep
+import Class
import Unify
import Module
import Coercion
import Maybes
import Util
import Outputable
-
import Data.List
+import TypeRep
+import Class
\end{code}
~~~~~~~~~
\begin{code}
instName :: Inst -> Name
+instName (EqInst {tci_name = name}) = name
instName inst = Var.varName (instToVar inst)
instToId :: Inst -> TcId
-instToId inst = ASSERT2( isId id, ppr inst ) id
+instToId inst = WARN( not (isId id), ppr inst )
+ id
where
id = instToVar inst
instToVar (ImplicInst {tci_name = nm, tci_tyvars = tvs, tci_given = givens,
tci_wanted = wanteds})
= mkLocalId nm (mkImplicTy tvs givens wanteds)
+instToVar i@(EqInst {})
+ = eitherEqInst i id (\(TyVarTy covar) -> covar)
instType :: Inst -> Type
-instType (LitInst {tci_ty = ty}) = ty
-instType (Method {tci_id = id}) = idType id
+instType (LitInst {tci_ty = ty}) = ty
+instType (Method {tci_id = id}) = idType id
instType (Dict {tci_pred = pred}) = mkPredTy pred
instType imp@(ImplicInst {}) = mkImplicTy (tci_tyvars imp) (tci_given imp)
(tci_wanted imp)
+-- instType i@(EqInst {tci_co = co}) = eitherEqInst i TyVarTy id
+instType (EqInst {tci_left = ty1, tci_right = ty2}) = mkPredTy (EqPred ty1 ty2)
mkImplicTy tvs givens wanteds -- The type of an implication constraint
= ASSERT( all isDict givens )
-- pprTrace "mkImplicTy" (ppr givens) $
- mkForAllTys tvs $
- mkPhiTy (map dictPred givens) $
- if isSingleton wanteds then
- instType (head wanteds)
- else
- mkTupleTy Boxed (length wanteds) (map instType wanteds)
+ -- See [Equational Constraints in Implication Constraints]
+ let dict_wanteds = filter (not . isEqInst) wanteds
+ in
+ mkForAllTys tvs $
+ mkPhiTy (map dictPred givens) $
+ if isSingleton dict_wanteds then
+ instType (head dict_wanteds)
+ else
+ mkTupleTy Boxed (length dict_wanteds) (map instType dict_wanteds)
dictPred (Dict {tci_pred = pred}) = pred
+dictPred (EqInst {tci_left=ty1,tci_right=ty2}) = EqPred ty1 ty2
dictPred inst = pprPanic "dictPred" (ppr inst)
getDictClassTys (Dict {tci_pred = pred}) = getClassPredTys pred
fdPredsOfInst (ImplicInst {tci_given = gs,
tci_wanted = ws}) = fdPredsOfInsts (gs ++ ws)
fdPredsOfInst (LitInst {}) = []
+fdPredsOfInst (EqInst {}) = []
fdPredsOfInsts :: [Inst] -> [PredType]
fdPredsOfInsts insts = concatMap fdPredsOfInst insts
`minusVarSet` mkVarSet tvs
`unionVarSet` unionVarSets (map varTypeTyVars tvs)
-- Remember the free tyvars of a coercion
+tyVarsOfInst (EqInst {tci_left = ty1, tci_right = ty2}) = tyVarsOfType ty1 `unionVarSet` tyVarsOfType ty2
tyVarsOfInsts insts = foldr (unionVarSet . tyVarsOfInst) emptyVarSet insts
tyVarsOfLIE lie = tyVarsOfInsts (lieToList lie)
Predicates
~~~~~~~~~~
\begin{code}
+
+isAbstractableInst :: Inst -> Bool
+isAbstractableInst inst = isDict inst || isEqInst inst
+
+isEqInst :: Inst -> Bool
+isEqInst (EqInst {}) = True
+isEqInst other = False
+
isDict :: Inst -> Bool
isDict (Dict {}) = True
isDict other = False
newDictBndrs inst_loc theta = mapM (newDictBndr inst_loc) theta
newDictBndr :: InstLoc -> TcPredType -> TcM Inst
+newDictBndr inst_loc pred@(EqPred ty1 ty2)
+ = do { uniq <- newUnique
+ ; let name = mkPredName uniq inst_loc pred
+ ; return (EqInst {tci_name = name,
+ tci_loc = inst_loc,
+ tci_left = ty1,
+ tci_right = ty2,
+ tci_co = mkGivenCo $ TyVarTy (Var.mkCoVar name (PredTy pred))})
+ }
newDictBndr inst_loc pred
= do { uniq <- newUnique
; let name = mkPredName uniq inst_loc pred
-- (instCall o tys theta)
-- (a) Makes fresh dictionaries as necessary for the constraints (theta)
-- (b) Throws these dictionaries into the LIE
--- (c) Eeturns an HsWrapper ([.] tys dicts)
+-- (c) Returns an HsWrapper ([.] tys dicts)
instCall orig tys theta
= do { loc <- getInstLoc orig
- ; (dicts, dict_app) <- instCallDicts loc theta
- ; extendLIEs dicts
+ ; dict_app <- instCallDicts loc theta
; return (dict_app <.> mkWpTyApps tys) }
----------------
-- Used exclusively for the 'stupid theta' of a data constructor
instStupidTheta orig theta
= do { loc <- getInstLoc orig
- ; (dicts, _) <- instCallDicts loc theta
- ; extendLIEs dicts }
+ ; _co <- instCallDicts loc theta -- Discard the coercion
+ ; return () }
----------------
-instCallDicts :: InstLoc -> TcThetaType -> TcM ([Inst], HsWrapper)
+instCallDicts :: InstLoc -> TcThetaType -> TcM HsWrapper
+-- Instantiates the TcTheta, puts all constraints thereby generated
+-- into the LIE, and returns a HsWrapper to enclose the call site.
-- This is the key place where equality predicates
-- are unleashed into the world
-instCallDicts loc [] = return ([], idHsWrapper)
+instCallDicts loc [] = return idHsWrapper
+
+-- instCallDicts loc (EqPred ty1 ty2 : preds)
+-- = do { unifyType ty1 ty2 -- For now, we insist that they unify right away
+-- -- Later on, when we do associated types,
+-- -- unifyType :: Type -> Type -> TcM ([Inst], Coercion)
+-- ; (dicts, co_fn) <- instCallDicts loc preds
+-- ; return (dicts, co_fn <.> WpTyApp ty1) }
+-- -- We use type application to apply the function to the
+-- -- coercion; here ty1 *is* the appropriate identity coercion
instCallDicts loc (EqPred ty1 ty2 : preds)
- = do { unifyType ty1 ty2 -- For now, we insist that they unify right away
- -- Later on, when we do associated types,
- -- unifyType :: Type -> Type -> TcM ([Inst], Coercion)
- ; (dicts, co_fn) <- instCallDicts loc preds
- ; return (dicts, co_fn <.> WpTyApp ty1) }
- -- We use type application to apply the function to the
- -- coercion; here ty1 *is* the appropriate identity coercion
+ = do { traceTc (text "instCallDicts" <+> ppr (EqPred ty1 ty2))
+ ; coi <- boxyUnify ty1 ty2
+-- ; coi <- unifyType ty1 ty2
+ ; let co = fromCoI coi ty1
+ ; co_fn <- instCallDicts loc preds
+ ; return (co_fn <.> WpTyApp co) }
instCallDicts loc (pred : preds)
= do { uniq <- newUnique
; let name = mkPredName uniq loc pred
dict = Dict {tci_name = name, tci_pred = pred, tci_loc = loc}
- ; (dicts, co_fn) <- instCallDicts loc preds
- ; return (dict:dicts, co_fn <.> WpApp (instToId dict)) }
+ ; extendLIE dict
+ ; co_fn <- instCallDicts loc preds
+ ; return (co_fn <.> WpApp (instToId dict)) }
-------------
cloneDict :: Inst -> TcM Inst
cloneDict dict@(Dict nm ty loc) = do { uniq <- newUnique
; return (dict {tci_name = setNameUnique nm uniq}) }
+cloneDict eq@(EqInst {}) = return eq
cloneDict other = pprPanic "cloneDict" (ppr other)
-- For vanilla implicit parameters, there is only one in scope
; wanteds' <- zonkInsts (tci_wanted implic)
; return (implic {tci_given = givens',tci_wanted = wanteds'}) }
+zonkInst eqinst@(EqInst {tci_left = ty1, tci_right = ty2})
+ = do { co' <- eitherEqInst eqinst
+ (\covar -> return (mkWantedCo covar))
+ (\co -> zonkTcType co >>= \coercion -> return (mkGivenCo coercion))
+ ; ty1' <- zonkTcType ty1
+ ; ty2' <- zonkTcType ty2
+ ; return (eqinst {tci_co = co',tci_left=ty1',tci_right=ty2})
+ }
+
zonkInsts insts = mappM zonkInst insts
\end{code}
pprInst, pprInstInFull :: Inst -> SDoc
-- Debugging: print the evidence :: type
+pprInst i@(EqInst {tci_left = ty1, tci_right = ty2, tci_co = co})
+ = eitherEqInst i
+ (\covar -> text "Wanted" <+> ppr (TyVarTy covar) <+> dcolon <+> ppr (EqPred ty1 ty2))
+ (\co -> text "Given" <+> ppr co <+> dcolon <+> ppr (EqPred ty1 ty2))
pprInst inst = ppr (instName inst) <+> dcolon
<+> (braces (ppr (instType inst)) $$
ifPprDebug implic_stuff)
implic_stuff | isImplicInst inst = ppr (tci_reft inst)
| otherwise = empty
+pprInstInFull inst@(EqInst {}) = pprInst inst
pprInstInFull inst = sep [quotes (pprInst inst), nest 2 (pprInstArising inst)]
tidyInst :: TidyEnv -> Inst -> Inst
+tidyInst env eq@(EqInst {tci_left = lty, tci_right = rty, tci_co = co}) =
+ eq { tci_left = tidyType env lty
+ , tci_right = tidyType env rty
+ , tci_co = either Left (Right . tidyType env) co
+ }
tidyInst env lit@(LitInst {tci_ty = ty}) = lit {tci_ty = tidyType env ty}
tidyInst env dict@(Dict {tci_pred = pred}) = dict {tci_pred = tidyPred env pred}
tidyInst env meth@(Method {tci_tys = tys}) = meth {tci_tys = tidyTypes env tys}
-- the LIE. Instead, any Insts needed by the lookup are returned in
-- the LookupInstResult, where they can be further processed by tcSimplify
+lookupSimpleInst (EqInst {}) = return NoInstance
+
--------------------- Implications ------------------------
lookupSimpleInst (ImplicInst {}) = return NoInstance
--------------------- Methods ------------------------
lookupSimpleInst (Method {tci_oid = id, tci_tys = tys, tci_theta = theta, tci_loc = loc})
- = do { (dicts, dict_app) <- instCallDicts loc theta
+ = do { (dict_app, dicts) <- getLIE $ instCallDicts loc theta
; let co_fn = dict_app <.> mkWpTyApps tys
; return (GenInst dicts (L span $ HsWrap co_fn (HsVar id))) }
where
; if null theta then
returnM (GenInst [] (L src_loc $ HsWrap (mkWpTyApps tys) dfun))
else do
- { (dicts, dict_app) <- instCallDicts loc theta
+ { (dict_app, dicts) <- getLIE $ instCallDicts loc theta -- !!!
; let co_fn = dict_app <.> mkWpTyApps tys
; returnM (GenInst dicts (L src_loc $ HsWrap co_fn dfun))
}}}}
in
returnM (tidy_env, msg)
\end{code}
+
+%************************************************************************
+%* *
+ EqInsts
+%* *
+%************************************************************************
+
+\begin{code}
+mkGivenCo :: Coercion -> Either TcTyVar Coercion
+mkGivenCo = Right
+
+mkWantedCo :: TcTyVar -> Either TcTyVar Coercion
+mkWantedCo = Left
+
+fromGivenCo :: Either TcTyVar Coercion -> Coercion
+fromGivenCo (Right co) = co
+fromGivenCo _ = panic "fromGivenCo: not a wanted coercion"
+
+fromWantedCo :: String -> Either TcTyVar Coercion -> TcTyVar
+fromWantedCo _ (Left covar) = covar
+fromWantedCo msg _ = panic ("fromWantedCo: not a wanted coercion: " ++ msg)
+
+eitherEqInst
+ :: Inst -- given or wanted EqInst
+ -> (TcTyVar -> a) -- result if wanted
+ -> (Coercion -> a) -- result if given
+ -> a
+eitherEqInst (EqInst {tci_co = either_co}) withWanted withGiven
+ = case either_co of
+ Left covar -> withWanted covar
+ Right co -> withGiven co
+
+mkEqInsts :: [PredType] -> [Either TcTyVar Coercion] -> TcM [Inst]
+mkEqInsts preds cos = zipWithM mkEqInst preds cos
+
+mkEqInst :: PredType -> Either TcTyVar Coercion -> TcM Inst
+mkEqInst (EqPred ty1 ty2) co
+ = do { uniq <- newUnique
+ ; src_span <- getSrcSpanM
+ ; err_ctxt <- getErrCtxt
+ ; let loc = InstLoc EqOrigin src_span err_ctxt
+ name = mkName uniq src_span
+ inst = EqInst {tci_left = ty1, tci_right = ty2, tci_co = co, tci_loc = loc, tci_name = name}
+ ; return inst
+ }
+ where mkName uniq src_span = mkInternalName uniq (mkVarOcc "co") src_span
+
+-- type inference:
+-- We want to promote the wanted EqInst to a given EqInst
+-- in the signature context.
+-- This means we have to give the coercion a name
+-- and fill it in as its own name.
+finalizeEqInst
+ :: Inst -- wanted
+ -> TcM Inst -- given
+finalizeEqInst wanted@(EqInst {tci_left = ty1, tci_right = ty2, tci_name = name})
+ = do { let var = Var.mkCoVar name (PredTy $ EqPred ty1 ty2)
+ ; writeWantedCoercion wanted (TyVarTy var)
+ ; let given = wanted { tci_co = mkGivenCo $ TyVarTy var }
+ ; return given
+ }
+
+writeWantedCoercion
+ :: Inst -- wanted EqInst
+ -> Coercion -- coercion to fill the hole with
+ -> TcM ()
+writeWantedCoercion wanted co
+ = do { let cotv = fromWantedCo "writeWantedCoercion" $ tci_co wanted
+ ; writeMetaTyVar cotv co
+ }
+
+eqInstType :: Inst -> TcType
+eqInstType inst = eitherEqInst inst mkTyVarTy id
+
+eqInstCoercion :: Inst -> Either TcTyVar Coercion
+eqInstCoercion = tci_co
+
+eqInstLeftTy, eqInstRightTy :: Inst -> TcType
+eqInstLeftTy = tci_left
+eqInstRightTy = tci_right
+
+updateEqInstCoercion :: (Either TcTyVar Coercion -> Either TcTyVar Coercion) -> Inst -> Inst
+updateEqInstCoercion f inst = inst {tci_co = f $ tci_co inst}
+\end{code}
import TcMType
import TcType
import {- Kind parts of -} Type
+import Coercion
import VarEnv
import TysPrim
import Id
bindLocalInsts :: TopLevelFlag -> TcM ([LHsBinds TcId], [TcId], a) -> TcM ([LHsBinds TcId], a)
bindLocalInsts top_lvl thing_inside
| isTopLevel top_lvl = do { (binds, ids, thing) <- thing_inside; return (binds, thing) }
- -- For the top level don't bother will all this bindInstsOfLocalFuns stuff.
+ -- For the top level don't bother with all this bindInstsOfLocalFuns stuff.
-- All the top level things are rec'd together anyway, so it's fine to
-- leave them to the tcSimplifyTop, and quite a bit faster too
unify_ctxt sig@(TcSigInfo { sig_theta = theta })
= setSrcSpan (instLocSpan (sig_loc sig)) $
addErrCtxt (sigContextsCtxt sig1 sig) $
- unifyTheta theta1 theta
+ do { cois <- unifyTheta theta1 theta
+ ; -- Check whether all coercions are identity coercions
+ -- That can happen if we have, say
+ -- f :: C [a] => ...
+ -- g :: C (F a) => ...
+ -- where F is a type function and (F a ~ [a])
+ -- Then unification might succeed with a coercion. But it's much
+ -- much simpler to require that such signatures have identical contexts
+ checkTc (all isIdentityCoercion cois)
+ (ptext SLIT("Mutually dependent functions have syntactically distinct contexts"))
+ }
checkSigsTyVars :: [TcTyVar] -> [TcSigInfo] -> TcM [TcTyVar]
checkSigsTyVars qtvs sigs
rho_ty = ASSERT( length tyvars == length inst_tys )
substTyWith tyvars inst_tys rho
(preds,tau) = tcSplitPhiTy rho_ty
- first_pred = head preds
+ first_pred = ASSERT( not (null preds)) head preds
in
-- The first predicate should be of form (C a b)
-- where C is the class in question
-- case we require that the instance decl is for a single-parameter
-- type class with type variable arguments:
-- instance (...) => C (T a b)
- clas_tyvar = head (classTyVars clas)
+ clas_tyvar = ASSERT (not (null (classTyVars clas))) head (classTyVars clas)
Just tycon = maybe_tycon
maybe_tycon = case inst_tys of
[ty] -> case tcSplitTyConApp_maybe ty of
import ListSetOps
import Outputable
import Bag
-
-import Monad (unless)
\end{code}
%************************************************************************
\end{code}
Auxiliary lookup wrapper which requires that looked up family instances are
-not type instances.
+not type instances. If called with a vanilla tycon, the old type application
+is simply returned.
\begin{code}
tcLookupFamInstExact :: TyCon -> [Type] -> TcM (TyCon, [Type])
tcLookupFamInstExact tycon tys
- = do { result@(rep_tycon, rep_tys) <- tcLookupFamInst tycon tys
- ; let { tvs = map (Type.getTyVar
- "TcDeriv.tcLookupFamInstExact")
- rep_tys
- ; variable_only_subst = all Type.isTyVarTy rep_tys &&
- sizeVarSet (mkVarSet tvs) == length tvs
+ | not (isOpenTyCon tycon)
+ = return (tycon, tys)
+ | otherwise
+ = do { maybeFamInst <- tcLookupFamInst tycon tys
+ ; case maybeFamInst of
+ Nothing -> famInstNotFound tycon tys False
+ Just famInst@(_, rep_tys)
+ | not variable_only_subst -> famInstNotFound tycon tys True
+ | otherwise -> return famInst
+ where
+ tvs = map (Type.getTyVar
+ "TcDeriv.tcLookupFamInstExact")
+ rep_tys
+ variable_only_subst = all Type.isTyVarTy rep_tys &&
+ sizeVarSet (mkVarSet tvs) == length tvs
-- renaming may have no repetitions
- }
- ; unless variable_only_subst $
- famInstNotFound tycon tys [result]
- ; return result
}
-
\end{code}
= 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)]
-\end{code}
-
+famInstNotFound tycon tys notExact
+ = failWithTc (msg <+> quotes (pprTypeApp tycon (ppr tycon) tys))
+ where
+ msg = ptext $ if notExact
+ then SLIT("No family instance exactly matching")
+ else SLIT("More than one family instance for")
+\end{code}
-- New Ids
newLocalName, newDFunName, newFamInstTyConName,
-
- -- Errors
- famInstNotFound
) where
#include "HsVersions.h"
import TcMType
import TcType
import TcGadt
+-- import TcSuspension
import qualified Type
import Var
import VarSet
import FamInstEnv
import DataCon
import TyCon
+import TypeRep
+import Coercion
import Class
import Name
import PrelNames
import HscTypes
import SrcLoc
import Outputable
+import Maybes
\end{code}
tcLookupLocatedTyCon :: Located Name -> TcM TyCon
tcLookupLocatedTyCon = addLocM tcLookupTyCon
--- Look up the representation tycon of a family instance.
+-- Look up the instance tycon of a family instance.
--
-- The match must be unique - ie, match exactly one instance - but the
-- type arguments used for matching may be more specific than those of
--
-- which implies that :R42T was declared as 'data instance T [a]'.
--
-tcLookupFamInst :: TyCon -> [Type] -> TcM (TyCon, [Type])
+tcLookupFamInst :: TyCon -> [Type] -> TcM (Maybe (TyCon, [Type]))
tcLookupFamInst tycon tys
| not (isOpenTyCon tycon)
- = return (tycon, tys)
+ = return Nothing
| otherwise
= do { env <- getGblEnv
; eps <- getEps
; let instEnv = (eps_fam_inst_env eps, tcg_fam_inst_env env)
; case lookupFamInstEnv instEnv tycon tys of
- [(fam_inst, rep_tys)] -> return (famInstTyCon fam_inst, rep_tys)
- other -> famInstNotFound tycon tys other
+ [(fam_inst, rep_tys)] -> return $ Just (famInstTyCon fam_inst,
+ rep_tys)
+ other -> return Nothing
}
\end{code}
extra_env = [ (name, ATcId { tct_id = id,
tct_level = th_lvl,
tct_type = id_ty,
- tct_co = if isRefineableTy id_ty
- then Just idHsWrapper
- else Nothing })
+ tct_co = case isRefineableTy id_ty of
+ (True,_) -> Unrefineable
+ (_,True) -> Rigid idHsWrapper
+ _ -> Wobbly})
| (name,id) <- names_w_ids, let id_ty = idType id]
le' = extendNameEnvList (tcl_env env) extra_env
rdr_env' = extendLocalRdrEnv (tcl_rdr env) [name | (name,_) <- names_w_ids]
\end{code}
\begin{code}
-refineEnvironment :: Refinement -> TcM a -> TcM a
+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 thing_inside
- | isEmptyRefinement reft -- Common case
+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 = Just co, tct_type = ty })
+ refine elt@(ATcId { tct_co = Rigid co, tct_type = ty })
| Just (co', ty') <- refineType reft ty
- = elt { tct_co = Just (WpCo co' <.> co), tct_type = 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
wrongThingErr expected thing name
= failWithTc (pprTcTyThingCategory thing <+> quotes (ppr name) <+>
ptext SLIT("used as a") <+> text expected)
-
-famInstNotFound tycon tys what
- = failWithTc (msg <+> quotes (pprTypeApp tycon (ppr tycon) tys))
- where
- msg = ptext $ if length what > 1
- then SLIT("More than one family instance for")
- else SLIT("No family instance exactly matching")
\end{code}
import Name
import TyCon
import Type
+import TypeRep
+import Coercion
import Var
import VarSet
import TysWiredIn
tcPolyExpr expr res_ty
= addErrCtxt (exprCtxt (unLoc expr)) $
- tcPolyExprNC expr res_ty
+ (do {traceTc (text "tcPolyExpr") ; tcPolyExprNC expr res_ty })
tcPolyExprNC expr res_ty
| isSigmaTy res_ty
- = do { (gen_fn, expr') <- tcGen res_ty emptyVarSet (\_ -> tcPolyExprNC expr)
+ = do { traceTc (text "tcPolyExprNC" <+> ppr res_ty)
+ ; (gen_fn, expr') <- tcGen res_ty emptyVarSet (\_ -> tcPolyExprNC expr)
-- Note the recursive call to tcPolyExpr, because the
-- type may have multiple layers of for-alls
-- E.g. forall a. Eq a => forall b. Ord b => ....
\end{code}
-
%************************************************************************
%* *
tcExpr: the main expression typechecker
tcExpr :: HsExpr Name -> BoxyRhoType -> TcM (HsExpr TcId)
tcExpr (HsVar name) res_ty = tcId (OccurrenceOf name) name res_ty
-tcExpr (HsLit lit) res_ty = do { boxyUnify (hsLitType lit) res_ty
- ; return (HsLit lit) }
+tcExpr (HsLit lit) res_ty = do { let lit_ty = hsLitType lit
+ ; coi <- boxyUnify lit_ty res_ty
+ ; return $ wrapExprCoI (HsLit lit) coi
+ }
tcExpr (HsPar expr) res_ty = do { expr' <- tcMonoExpr expr res_ty
; return (HsPar expr') }
go lfun@(L loc fun) args
= do { (fun', args') <- -- addErrCtxt (callCtxt lfun args) $
tcApp fun (length args) (tcArgs lfun args) res_ty
+ ; traceTc (text "tcExpr args': " <+> ppr args')
; return (unLoc (foldl mkHsApp (L loc fun') args')) }
tcExpr (HsLam match) res_ty
; return (ExplicitList elt_ty exprs') }
where
tc_elt elt_ty expr = tcPolyExpr expr elt_ty
+{- TODO: Version from Tom's original patch. Unfortunately, we cannot do it this
+ way, but need to teach boxy splitters about match deferral and coercions.
+ = do { elt_tv <- newBoxyTyVar argTypeKind
+ ; let elt_ty = TyVarTy elt_tv
+ ; coi <- boxyUnify (mkTyConApp listTyCon [elt_ty]) res_ty
+ -- ; elt_ty <- boxySplitListTy res_ty
+ ; exprs' <- mappM (tc_elt elt_ty) exprs
+ ; return $ wrapExprCoI (ExplicitList elt_ty exprs') coi }
+ -- ; return (ExplicitList elt_ty exprs') }
+ where
+ tc_elt elt_ty expr = tcPolyExpr expr elt_ty
+ -}
tcExpr in_expr@(ExplicitPArr _ exprs) res_ty -- maybe empty
= do { [elt_ty] <- boxySplitTyConApp parrTyCon res_ty
-- tcFun work nicely for OpApp and Sections too
; fun' <- instFun orig fun res_subst tv_theta_prs
; co_fn' <- wrapFunResCoercion (substTys res_subst fun_arg_tys) co_fn
+ ; traceTc (text "tcIdApp: " <+> ppr (mkHsWrap co_fn' fun') <+> ppr tv_theta_prs <+> ppr co_fn' <+> ppr fun')
; return (mkHsWrap co_fn' fun', args') }
\end{code}
-- And pack up the results
; fun' <- instFun orig fun res_subst tv_theta_prs
+ ; traceTc (text "tcId yields" <+> ppr (mkHsWrap co_fn fun'))
; return (mkHsWrap co_fn fun') }
-- Note [Push result type in]
instFun orig fun subst tv_theta_prs
= do { let ty_theta_prs' = map subst_pr tv_theta_prs
-
+ ; traceTc (text "instFun" <+> ppr ty_theta_prs')
-- Make two ad-hoc checks
; doStupidChecks fun ty_theta_prs'
-- Now do normal instantiation
- ; go True fun ty_theta_prs' }
+ ; result <- go True fun ty_theta_prs'
+ ; traceTc (text "instFun result" <+> ppr result)
+ ; return result
+ }
where
subst_pr (tvs, theta)
= (substTyVars subst tvs, substTheta subst theta)
- go _ fun [] = return fun
+ go _ fun [] = do {traceTc (text "go _ fun [] returns" <+> ppr fun) ; return fun }
go True (HsVar fun_id) ((tys,theta) : prs)
| want_method_inst theta
- = do { meth_id <- newMethodWithGivenTy orig fun_id tys
+ = do { traceTc (text "go (HsVar fun_id) ((tys,theta) : prs) | want_method_inst theta")
+ ; meth_id <- newMethodWithGivenTy orig fun_id tys
; go False (HsVar meth_id) prs }
-- Go round with 'False' to prevent further use
-- of newMethod: see Note [Multiple instantiation]
go _ fun ((tys, theta) : prs)
= do { co_fn <- instCall orig tys theta
+ ; traceTc (text "go yields co_fn" <+> ppr co_fn)
; go False (HsWrap co_fn fun) prs }
-- See Note [No method sharing]
ATcId { tct_id = id, tct_type = ty, tct_co = mb_co, tct_level = lvl }
-> do { thLocalId orig id ty lvl
; case mb_co of
- Nothing -> return (HsVar id, ty) -- Wobbly, or no free vars
- Just co -> return (mkHsWrap co (HsVar id), ty) }
+ Unrefineable -> return (HsVar id, ty)
+ Rigid co -> return (mkHsWrap co (HsVar id), ty)
+ Wobbly -> traceTc (text "lookupFun" <+> ppr id) >> return (HsVar id, ty) -- Wobbly, or no free vars
+ WobblyInvisible -> failWithTc (ppr id_name <+> ptext SLIT(" not in scope because it has a wobbly type (solution: add a type annotation)"))
+ }
other -> failWithTc (ppr other <+> ptext SLIT("used where a value identifer was expected"))
}
= ptext SLIT("Can't splice the polymorphic local variable") <+> quotes (ppr id)
#endif
\end{code}
+
+\begin{code}
+wrapExprCoI :: HsExpr a -> CoercionI -> HsExpr a
+wrapExprCoI expr IdCo = expr
+wrapExprCoI expr (ACo co) = mkHsWrap (WpCo co) expr
+\end{code}
}
kc_pred pred@(HsEqualP ty1 ty2)
= do { (ty1', kind1) <- kcHsType ty1
- ; checkExpectedKind ty1 kind1 liftedTypeKind
+-- ; checkExpectedKind ty1 kind1 liftedTypeKind
; (ty2', kind2) <- kcHsType ty2
- ; checkExpectedKind ty2 kind2 liftedTypeKind
- ; returnM (HsEqualP ty1 ty2, liftedTypeKind)
+-- ; checkExpectedKind ty2 kind2 liftedTypeKind
+ ; checkExpectedKind ty2 kind2 kind1
+ ; returnM (HsEqualP ty1' ty2', liftedTypeKind)
}
---------------------------
import Type
import Coercion
import TyCon
+import TypeRep
import DataCon
import Class
import Var
-- (This no longer includes the associated types.)
; dfun_name <- newDFunName clas inst_tys loc
; overlap_flag <- getOverlapFlag
- ; let dfun = mkDictFunId dfun_name tyvars theta clas inst_tys
+ ; let (eq_theta,dict_theta) = partition isEqPred theta
+ theta' = eq_theta ++ dict_theta
+ dfun = mkDictFunId dfun_name tyvars theta' clas inst_tys
ispec = mkLocalInstance dfun overlap_flag
; return ([InstInfo { iSpec = ispec,
-- Instantiate the super-class context with inst_tys
sc_theta' = substTheta (zipOpenTvSubst class_tyvars inst_tys') sc_theta
+ (eq_sc_theta',dict_sc_theta') = partition isEqPred sc_theta'
origin = SigOrigin rigid_info
+ (eq_dfun_theta',dict_dfun_theta') = partition isEqPred dfun_theta'
in
-- Create dictionary Ids from the specified instance contexts.
getInstLoc InstScOrigin `thenM` \ sc_loc ->
- newDictBndrs sc_loc sc_theta' `thenM` \ sc_dicts ->
+ newDictBndrs sc_loc dict_sc_theta' `thenM` \ sc_dicts ->
getInstLoc origin `thenM` \ inst_loc ->
- newDictBndrs inst_loc dfun_theta' `thenM` \ dfun_arg_dicts ->
+ mkMetaCoVars eq_sc_theta' `thenM` \ sc_covars ->
+ mkEqInsts eq_sc_theta' (map mkWantedCo sc_covars) `thenM` \ wanted_sc_eqs ->
+ mkCoVars eq_dfun_theta' `thenM` \ dfun_covars ->
+ mkEqInsts eq_dfun_theta' (map mkGivenCo $ mkTyVarTys dfun_covars) `thenM` \ dfun_eqs ->
+ newDictBndrs inst_loc dict_dfun_theta' `thenM` \ dfun_dicts ->
newDictBndr inst_loc (mkClassPred clas inst_tys') `thenM` \ this_dict ->
-- Default-method Ids may be mentioned in synthesised RHSs,
-- but they'll already be in the environment.
-- Typecheck the methods
let -- These insts are in scope; quite a few, eh?
- avail_insts = [this_dict] ++ dfun_arg_dicts ++ sc_dicts
+ dfun_insts = dfun_eqs ++ dfun_dicts
+ wanted_sc_insts = wanted_sc_eqs ++ sc_dicts
+ given_sc_eqs = map (updateEqInstCoercion (mkGivenCo . TyVarTy . fromWantedCo "tcInstDecl2") ) wanted_sc_eqs
+ given_sc_insts = given_sc_eqs ++ sc_dicts
+ avail_insts = [this_dict] ++ dfun_insts ++ given_sc_insts
in
tcMethods origin clas inst_tyvars'
dfun_theta' inst_tys' avail_insts
-- Figure out bindings for the superclass context
-- Don't include this_dict in the 'givens', else
- -- sc_dicts get bound by just selecting from this_dict!!
+ -- wanted_sc_insts get bound by just selecting from this_dict!!
addErrCtxt superClassCtxt
(tcSimplifySuperClasses inst_loc
- dfun_arg_dicts sc_dicts) `thenM` \ sc_binds ->
+ dfun_insts wanted_sc_insts) `thenM` \ sc_binds ->
-- It's possible that the superclass stuff might unified one
-- of the inst_tyavars' with something in the envt
dict_constr = classDataCon clas
scs_and_meths = map instToId sc_dicts ++ meth_ids
this_dict_id = instToId this_dict
- inline_prag | null dfun_arg_dicts = []
- | otherwise = [L loc (InlinePrag (Inline AlwaysActive True))]
+ inline_prag | null dfun_insts = []
+ | otherwise = [L loc (InlinePrag (Inline AlwaysActive True))]
-- Always inline the dfun; this is an experimental decision
-- because it makes a big performance difference sometimes.
-- Often it means we can do the method selection, and then
-- See Note [Inline dfuns] below
dict_rhs
- = mkHsConApp dict_constr inst_tys' (map HsVar scs_and_meths)
+ = mkHsConApp dict_constr (inst_tys' ++ mkTyVarTys sc_covars) (map HsVar scs_and_meths)
-- We don't produce a binding for the dict_constr; instead we
-- rely on the simplifier to unfold this saturated application
-- We do this rather than generate an HsCon directly, because
all_binds = dict_bind `consBag` (sc_binds `unionBags` meth_binds)
main_bind = noLoc $ AbsBinds
- inst_tyvars'
- (map instToId dfun_arg_dicts)
- [(inst_tyvars', dfun_id, this_dict_id,
- inline_prag ++ prags)]
+ (inst_tyvars' ++ dfun_covars)
+ (map instToId dfun_dicts)
+ [(inst_tyvars' ++ dfun_covars, dfun_id, this_dict_id, inline_prag ++ prags)]
all_binds
in
showLIE (text "instance") `thenM_`
returnM (unitBag main_bind)
+mkCoVars :: [PredType] -> TcM [TyVar]
+mkCoVars [] = return []
+mkCoVars (pred:preds) =
+ do { uniq <- newUnique
+ ; let name = mkSysTvName uniq FSLIT("mkCoVars")
+ ; let tv = mkCoVar name (PredTy pred)
+ ; tvs <- mkCoVars preds
+ ; return (tv:tvs)
+ }
+
+mkMetaCoVars :: [PredType] -> TcM [TyVar]
+mkMetaCoVars [] = return []
+mkMetaCoVars (EqPred ty1 ty2:preds) =
+ do { tv <- newMetaTyVar TauTv (mkCoKind ty1 ty2)
+ ; tvs <- mkMetaCoVars preds
+ ; return (tv:tvs)
+ }
+
tcMethods origin clas inst_tyvars' dfun_theta' inst_tys'
avail_insts op_items monobinds uprags
zonkTcKindToKind, zonkTcKind, zonkTopTyVar,
readKindVar, writeKindVar
-
) where
#include "HsVersions.h"
-- Make a new meta tyvar out of thin air
newMetaTyVar box_info kind
= do { uniq <- newUnique
- ; ref <- newMutVar Flexi ;
+ ; ref <- newMutVar Flexi
; let name = mkSysTvName uniq fs
fs = case box_info of
BoxTv -> FSLIT("t")
-- come from an existing TyVar
instMetaTyVar box_info tyvar
= do { uniq <- newUnique
- ; ref <- newMutVar Flexi ;
+ ; ref <- newMutVar Flexi
; let name = setNameUnique (tyVarName tyvar) uniq
kind = tyVarKind tyvar
; return (mkTcTyVar name kind (MetaTv box_info ref)) }
| otherwise
= ASSERT( isMetaTyVar tyvar )
- ASSERT2( k2 `isSubKind` k1, (ppr tyvar <+> ppr k1) $$ (ppr ty <+> ppr k2) )
+ -- TOM: It should also work for coercions
+ -- ASSERT2( k2 `isSubKind` k1, (ppr tyvar <+> ppr k1) $$ (ppr ty <+> ppr k2) )
do { ASSERTM2( do { details <- readMetaTyVar tyvar; return (isFlexi details) }, ppr tyvar )
; writeMutVar (metaTvRef tyvar) (Indirect ty) }
where
readFilledBox box_tv = ASSERT( isBoxyTyVar box_tv )
do { cts <- readMetaTyVar box_tv
; case cts of
- Flexi -> pprPanic "readFilledBox" (ppr box_tv)
+ Flexi -> pprPanic "readFilledBox" (ppr box_tv)
Indirect ty -> return ty }
tcInstBoxyTyVar :: TyVar -> TcM BoxyTyVar
MetaTv _ ref -> do { meta_details <- readMutVar ref
; case meta_details of
Indirect ty -> return (IndirectTv ty)
- Flexi -> return (DoneTv details) }
+ Flexi -> return (DoneTv details) }
where
details = tcTyVarDetails tyvar
import TysWiredIn
import TcGadt
import Type
+import Coercion
import StaticFlags
import TyCon
import DataCon
-> TcM (LPat TcId, a)
tcLetPat sig_fn pat pat_ty thing_inside
= do { let init_state = PS { pat_ctxt = LetPat sig_fn,
- pat_reft = emptyRefinement }
+ pat_reft = emptyRefinement,
+ pat_eqs = False }
; (pat', ex_tvs, res) <- tc_lpat pat pat_ty init_state (\ _ -> thing_inside)
-- Don't know how to deal with pattern-bound existentials yet
-> ((Refinement,BoxyRhoType) -> TcM a) -- Checker for body, given its result type
-> TcM ([LPat TcId], a)
tc_lam_pats pat_ty_prs (reft, res_ty) thing_inside
- = do { let init_state = PS { pat_ctxt = LamPat, pat_reft = reft }
+ = do { let init_state = PS { pat_ctxt = LamPat, pat_reft = reft, pat_eqs = False }
; (pats', ex_tvs, res) <- tcMultiple tc_lpat_pr pat_ty_prs init_state $ \ pstate' ->
- refineEnvironment (pat_reft pstate') $
- thing_inside (pat_reft pstate', res_ty)
+ refineEnvironment (pat_reft pstate') (pat_eqs pstate') $
+ if (pat_eqs pstate' && (not $ isRigidTy res_ty))
+ then failWithTc (nonRigidResult res_ty)
+ else thing_inside (pat_reft pstate', res_ty)
; let tys = map snd pat_ty_prs
; tcCheckExistentialPat pats' ex_tvs tys res_ty
data PatState = PS {
pat_ctxt :: PatCtxt,
- pat_reft :: Refinement -- Binds rigid TcTyVars to their refinements
+ pat_reft :: Refinement, -- Binds rigid TcTyVars to their refinements
+ pat_eqs :: Bool -- <=> there are GADT equational constraints
+ -- for refinement
}
data PatCtxt
------------------------
-- Literal patterns
tc_pat pstate (LitPat simple_lit) pat_ty thing_inside
- = do { boxyUnify (hsLitType simple_lit) pat_ty
+ = do { let lit_ty = hsLitType simple_lit
+ ; coi <- boxyUnify lit_ty pat_ty
+ -- coi is of kind: lit_ty ~ pat_ty
; res <- thing_inside pstate
- ; returnM (LitPat simple_lit, [], res) }
+ ; span <- getSrcSpanM
+ -- pattern coercions have to
+ -- be of kind: pat_ty ~ lit_ty
+ -- hence, sym coi
+ ; returnM (wrapPatCoI (mkSymCoI coi) (LitPat simple_lit) pat_ty, [], res) }
------------------------
-- Overloaded patterns: n, and n+k
-> HsConPatDetails Name -> (PatState -> TcM a)
-> TcM (Pat TcId, [TcTyVar], a)
tcConPat pstate con_span data_con tycon pat_ty arg_pats thing_inside
- = do { let (univ_tvs, ex_tvs, eq_spec, theta, arg_tys, _) = dataConFullSig data_con
+ = do { let (univ_tvs, ex_tvs, eq_spec, eq_theta, dict_theta, arg_tys, _) = dataConFullSig data_con
skol_info = PatSkol data_con
origin = SigOrigin skol_info
; let tenv = zipTopTvSubst (univ_tvs ++ ex_tvs)
(ctxt_res_tys ++ mkTyVarTys ex_tvs')
eq_spec' = substEqSpec tenv eq_spec
- theta' = substTheta tenv theta
+ theta' = substTheta tenv (eq_theta ++ dict_theta)
arg_tys' = substTys tenv arg_tys
; co_vars <- newCoVars eq_spec' -- Make coercion variables
; pstate' <- refineAlt data_con pstate ex_tvs' co_vars pat_ty
-
+
; ((arg_pats', inner_tvs, res), lie_req) <- getLIE $
tcConArgs data_con arg_tys' arg_pats pstate' thing_inside
-> TcM PatState
refineAlt con pstate ex_tvs [] pat_ty
+ | null $ dataConEqTheta con
= return pstate -- Common case: no equational constraints
refineAlt con pstate ex_tvs co_vars pat_ty
; case gadtRefine (pat_reft pstate) ex_tvs co_vars of {
Failed msg -> failWithTc (inaccessibleAlt msg) ;
Succeeded reft -> do { traceTc trace_msg
- ; return (pstate { pat_reft = reft }) }
+ ; return (pstate { pat_reft = reft, pat_eqs = (pat_eqs pstate || not (null $ dataConEqTheta con)) }) }
-- DO NOT refine the envt right away, because we
-- might be inside a lazy pattern. Instead, refine pstate
where
= hang (ptext SLIT("GADT pattern match in non-rigid context for") <+> quotes (ppr con))
2 (ptext SLIT("Tell GHC HQ if you'd like this to unify the context"))
+nonRigidResult res_ty
+ = hang (ptext SLIT("GADT pattern match with non-rigid result type") <+> quotes (ppr res_ty))
+ 2 (ptext SLIT("Tell GHC HQ if you'd like this to unify the context"))
+
inaccessibleAlt msg
= hang (ptext SLIT("Inaccessible case alternative:")) 2 msg
\end{code}
+
+\begin{code}
+wrapPatCoI :: CoercionI -> Pat a -> TcType -> Pat a
+wrapPatCoI IdCo pat ty = pat
+wrapPatCoI (ACo co) pat ty = CoPat (WpCo co) pat ty
+\end{code}
import InstEnv
import FamInstEnv
+import Coercion
import Var
import Id
import VarSet
; let { env = Env { env_top = hsc_env,
env_us = us_var,
env_gbl = gbl_env,
- env_lcl = lcl_env } }
+ env_lcl = lcl_env} }
; runIOEnv env thing_inside
}
-- pprPanic "forkM" doc
Just r -> r) }
\end{code}
-
-
WhereFrom(..), mkModDeps,
-- Typechecker types
- TcTyThing(..), pprTcTyThingCategory,
+ TcTyThing(..), pprTcTyThingCategory, RefinementVisibility(..),
-- Template Haskell
ThStage(..), topStage, topSpliceStage,
plusLIEs, mkLIE, isEmptyLIE, lieToList, listToLIE,
-- Misc other types
- TcId, TcIdSet, TcDictBinds
+ TcId, TcIdSet, TcDictBinds,
+
) where
#include "HsVersions.h"
import HscTypes
import Packages
import Type
+import Coercion
import TcType
import TcGadt
import InstEnv
import Bag
import Outputable
import ListSetOps
+import FiniteMap
import Data.Maybe
import Data.List
env_gbl :: gbl, -- Info about things defined at the top level
-- of the module being compiled
- env_lcl :: lcl -- Nested stuff; changes as we go into
- -- an expression
+ env_lcl :: lcl -- Nested stuff; changes as we go into
}
-- TcGblEnv describes the top-level of the module at the
-- Maintained during renaming, of course, but also during
-- type checking, solely so that when renaming a Template-Haskell
-- splice we have the right environment for the renamer.
- --
- -- Used only for names bound within a value binding (bound by
- -- lambda, case, where, let etc), but *not* for top-level names.
- --
- -- Does *not* include global name envt; may shadow it
- -- Includes both ordinary variables and type variables;
- -- they are kept distinct because tyvar have a different
- -- occurrence contructor (Name.TvOcc)
--
+ -- Does *not* include global name envt; may shadow it
+ -- Includes both ordinary variables and type variables;
+ -- they are kept distinct because tyvar have a different
+ -- occurrence contructor (Name.TvOcc)
-- We still need the unsullied global name env so that
-- we can look up record field names
| ATcId { -- Ids defined in this module; may not be fully zonked
tct_id :: TcId,
- tct_co :: Maybe HsWrapper, -- Nothing <=> Do not apply a GADT type refinement
+ tct_co :: RefinementVisibility, -- Previously: Maybe HsWrapper
+ -- Nothing <=> Do not apply a GADT type refinement
-- I am wobbly, or have no free
-- type variables
-- Just co <=> Apply any type refinement to me,
| AThing TcKind -- Used temporarily, during kind checking, for the
-- tycons and clases in this recursive group
+data RefinementVisibility
+ = Unrefineable -- Do not apply a GADT refinement
+ -- I have no free variables
+
+ | Rigid HsWrapper -- Apply any refinement to me
+ -- and record it in the coercion
+
+ | Wobbly -- Do not apply a GADT refinement
+ -- I am wobbly
+
+ | WobblyInvisible -- Wobbly type, not available inside current
+ -- GADT refinement
+
instance Outputable TcTyThing where -- Debugging only
ppr (AGlobal g) = ppr g
ppr elt@(ATcId {}) = text "Identifier" <>
pprTcTyThingCategory (ATyVar {}) = ptext SLIT("Type variable")
pprTcTyThingCategory (ATcId {}) = ptext SLIT("Local identifier")
pprTcTyThingCategory (AThing {}) = ptext SLIT("Kinded thing")
+
+instance Outputable RefinementVisibility where
+ ppr Unrefineable = ptext SLIT("unrefineable")
+ ppr (Rigid co) = ptext SLIT("rigid") <+> ppr co
+ ppr Wobbly = ptext SLIT("wobbly")
+ ppr WobblyInvisible = ptext SLIT("wobbly-invisible")
+
\end{code}
\begin{code}
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'
+and equality constraints 'co :: ty1 ~ ty2'.
+
\begin{code}
data Inst
= Dict {
tci_ty :: TcType, -- The type at which the literal is used
tci_loc :: InstLoc
}
+
+ | EqInst { -- delayed unification of the form
+ -- co :: ty1 ~ ty2
+ tci_left :: TcType, -- ty1
+ tci_right :: TcType, -- ty2
+ tci_co :: Either -- co
+ TcTyVar -- a wanted equation, with a hole, to be
+ -- filled with a witness for the equality
+ -- for equation generated by the
+ -- unifier, 'ty1' is the actual and
+ -- 'ty2' the expected type
+ Coercion, -- a given equation, with a coercion
+ -- witnessing the equality
+ -- a coercion that originates from a
+ -- signature or a GADT is a CoVar, but
+ -- after normalisation of coercions,
+ -- they can be arbitrary Coercions
+ -- involving constructors and
+ -- pseudo-constructors like sym and
+ -- trans.
+ tci_loc :: InstLoc,
+
+ tci_name :: Name -- Debugging help only: this makes it easier to
+ -- follow where a constraint is used in a morass
+ -- of trace messages! Unlike other Insts, it has
+ -- no semantic significance whatsoever.
+ }
\end{code}
@Insts@ are ordered by their class/type info, rather than by their
cmpInst (ImplicInst {}) (Method {}) = GT
cmpInst (ImplicInst {}) (LitInst {}) = GT
cmpInst i1@(ImplicInst {}) i2@(ImplicInst {}) = tci_name i1 `compare` tci_name i2
+cmpInst (ImplicInst {}) other = LT
+
+ -- same for Equality constraints
+cmpInst (EqInst {}) (Dict {}) = GT
+cmpInst (EqInst {}) (Method {}) = GT
+cmpInst (EqInst {}) (LitInst {}) = GT
+cmpInst (EqInst {}) (ImplicInst {}) = GT
+cmpInst i1@(EqInst {}) i2@(EqInst {}) = tci_name i1 `compare` tci_name i2
\end{code}
| DoOrigin -- Arising from a do expression
| ProcOrigin -- Arising from a proc expression
| ImplicOrigin SDoc -- An implication constraint
+ | EqOrigin -- A type equality
instance Outputable InstOrigin where
ppr (OccurrenceOf name) = hsep [ptext SLIT("a use of"), quotes (ppr name)]
ppr ProcOrigin = ptext SLIT("a proc expression")
ppr (ImplicOrigin doc) = doc
ppr (SigOrigin info) = pprSkolInfo info
+ ppr EqOrigin = ptext SLIT("a type equality")
+
\end{code}
--- /dev/null
+\begin{code}
+module TcRnTypes where
+
+import IOEnv
+
+type TcM a = TcRn a
+type TcRn a = TcRnIf TcGblEnv TcLclEnv a
+type TcRnIf a b c = IOEnv (Env a b) c
+
+data Env a b
+data TcGblEnv
+data TcLclEnv
+\end{code}
tcSimplifyDeriv, tcSimplifyDefault,
bindInstsOfLocalFuns, bindIrreds,
+
+ misMatchMsg
) where
#include "HsVersions.h"
import TcType
import TcMType
import TcIface
+import TcTyFuns
+import TypeRep
import Var
import Name
import NameSet
import BasicTypes
import VarSet
import VarEnv
+import Module
import FiniteMap
import Bag
import Outputable
import Maybes
import ListSetOps
import Util
+import UniqSet
import SrcLoc
import DynFlags
-- We can't abstract over any remaining unsolved
-- implications so instead just float them outwards. Ugh.
- ; let (q_dicts, implics) = partition isDict irreds3
+ ; let (q_dicts0, implics) = partition isAbstractableInst irreds3
; loc <- getInstLoc (ImplicOrigin doc)
- ; implic_bind <- bindIrreds loc qtvs2 q_dicts implics
+ ; implic_bind <- bindIrreds loc qtvs2 q_dicts0 implics
+
+ -- Prepare equality instances for quantification
+ ; let (q_eqs0,q_dicts) = partition isEqInst q_dicts0
+ ; q_eqs <- mappM finalizeEqInst q_eqs0
- ; return (qtvs2, q_dicts, binds1 `unionBags` binds2 `unionBags` implic_bind) }
+ ; return (qtvs2, q_eqs ++ q_dicts, binds1 `unionBags` binds2 `unionBags` implic_bind) }
-- NB: when we are done, we might have some bindings, but
-- the final qtvs might be empty. See Note [NO TYVARS] below.
= [ d | let tv_set = mkVarSet tvs
, d <- get_dicts wanteds
, not (tyVarsOfInst d `intersectsVarSet` tv_set)]
+ get_dict i@(EqInst {}) | want_dict i = [i]
+ | otherwise = []
get_dict other = pprPanic "approximateImplications" (ppr other)
\end{code}
TcDictBinds) -- Bindings
tcSimplifyInferCheck loc tau_tvs givens wanteds
- = do { (irreds, binds) <- gentleCheckLoop loc givens wanteds
+ = do { traceTc (text "tcSimplifyInferCheck <-" <+> ppr wanteds)
+ ; (irreds, binds) <- gentleCheckLoop loc givens wanteds
-- Figure out which type variables to quantify over
-- You might think it should just be the signature tyvars,
-- Now we are back to normal (c.f. tcSimplCheck)
; implic_bind <- bindIrreds loc qtvs' givens irreds
+ ; traceTc (text "tcSimplifyInferCheck ->" <+> ppr (implic_bind))
; return (qtvs', binds `unionBags` implic_bind) }
\end{code}
-> TcM TcDictBinds -- Bindings
tcSimplifyCheck loc qtvs givens wanteds
= ASSERT( all isTcTyVar qtvs && all isSkolemTyVar qtvs )
- do { (irreds, binds) <- gentleCheckLoop loc givens wanteds
+ do { traceTc (text "tcSimplifyCheck")
+ ; (irreds, binds) <- gentleCheckLoop loc givens wanteds
; implic_bind <- bindIrreds loc qtvs givens irreds
; return (binds `unionBags` implic_bind) }
-> TcM TcDictBinds -- Bindings
tcSimplifyCheckPat loc co_vars reft qtvs givens wanteds
= ASSERT( all isTcTyVar qtvs && all isSkolemTyVar qtvs )
- do { (irreds, binds) <- gentleCheckLoop loc givens wanteds
+ do { traceTc (text "tcSimplifyCheckPat")
+ ; (irreds, binds) <- gentleCheckLoop loc givens wanteds
; implic_bind <- bindIrredsR loc qtvs co_vars reft
givens irreds
; return (binds `unionBags` implic_bind) }
--
-- This binding must line up the 'rhs' in reduceImplication
makeImplicationBind loc all_tvs reft
- givens -- Guaranteed all Dicts
+ givens -- Guaranteed all Dicts (TOMDO: true?)
irreds
| null irreds -- If there are no irreds, we are done
= return ([], emptyBag)
| otherwise -- Otherwise we must generate a binding
= do { uniq <- newUnique
; span <- getSrcSpanM
+ ; let (eq_givens,dict_givens) = partitionGivenEqInsts givens
+ eq_tyvar_cos = map TyVarTy $ uniqSetToList $ tyVarsOfTypes $ map eqInstType eq_givens
; let name = mkInternalName uniq (mkVarOcc "ic") span
implic_inst = ImplicInst { tci_name = name, tci_reft = reft,
tci_tyvars = all_tvs,
- tci_given = givens,
+ tci_given = (eq_givens ++ dict_givens),
tci_wanted = irreds, tci_loc = loc }
-
- ; let n_irreds = length irreds
- irred_ids = map instToId irreds
- tup_ty = mkTupleTy Boxed n_irreds (map idType irred_ids)
- pat = TuplePat (map nlVarPat irred_ids) Boxed tup_ty
+ ; let
+ -- only create binder for dict_irreds
+ -- we
+ (eq_irreds,dict_irreds) = partitionWantedEqInsts irreds
+ n_dict_irreds = length dict_irreds
+ dict_irred_ids = map instToId dict_irreds
+ tup_ty = mkTupleTy Boxed n_dict_irreds (map idType dict_irred_ids)
+ pat = TuplePat (map nlVarPat dict_irred_ids) Boxed tup_ty
rhs = L span (mkHsWrap co (HsVar (instToId implic_inst)))
- co = mkWpApps (map instToId givens) <.> mkWpTyApps (mkTyVarTys all_tvs)
- bind | n_irreds==1 = VarBind (head irred_ids) rhs
- | otherwise = PatBind { pat_lhs = L span pat,
- pat_rhs = unguardedGRHSs rhs,
- pat_rhs_ty = tup_ty,
- bind_fvs = placeHolderNames }
- ; -- pprTrace "Make implic inst" (ppr implic_inst) $
+ co = mkWpApps (map instToId dict_givens) <.> mkWpTyApps eq_tyvar_cos <.> mkWpTyApps (mkTyVarTys all_tvs)
+ bind | [dict_irred_id] <- dict_irred_ids = VarBind dict_irred_id rhs
+ | otherwise = PatBind { pat_lhs = L span pat,
+ pat_rhs = unguardedGRHSs rhs,
+ pat_rhs_ty = tup_ty,
+ bind_fvs = placeHolderNames }
+ ; -- pprTrace "Make implic inst" (ppr (implic_inst,irreds,dict_irreds,tup_ty)) $
return ([implic_inst], unitBag (L span bind)) }
-----------------------------------------------------------
-> TcM ([Inst], TcDictBinds)
tryHardCheckLoop doc wanteds
- = checkLoop (mkRedEnv doc try_me []) wanteds
+ = do { (irreds,binds,_) <- checkLoop (mkRedEnv doc try_me []) wanteds
+ ; return (irreds,binds)
+ }
where
try_me inst = ReduceMe AddSCs
-- Here's the try-hard bit
-> TcM ([Inst], TcDictBinds)
gentleCheckLoop inst_loc givens wanteds
- = checkLoop env wanteds
+ = do { (irreds,binds,_) <- checkLoop env wanteds
+ ; return (irreds,binds)
+ }
where
env = mkRedEnv (pprInstLoc inst_loc) try_me givens
-----------------------------------------------------------
checkLoop :: RedEnv
-> [Inst] -- Wanted
- -> TcM ([Inst], TcDictBinds)
+ -> TcM ([Inst], TcDictBinds,
+ [Inst]) -- needed givens
-- Precondition: givens are completely rigid
-- Postcondition: returned Insts are zonked
checkLoop env wanteds
- = do { -- Givens are skolems, so no need to zonk them
- wanteds' <- mappM zonkInst wanteds
-
- ; (improved, binds, irreds) <- reduceContext env wanteds'
-
- ; if not improved then
- return (irreds, binds)
- else do
+ = go env wanteds []
+ where go env wanteds needed_givens
+ = do { -- Givens are skolems, so no need to zonk them
+ wanteds' <- zonkInsts wanteds
+
+ ; (improved, binds, irreds, more_needed_givens) <- reduceContext env wanteds'
- -- If improvement did some unification, we go round again.
- -- We start again with irreds, not wanteds
- -- Using an instance decl might have introduced a fresh type variable
- -- which might have been unified, so we'd get an infinite loop
- -- if we started again with wanteds! See Note [LOOP]
- { (irreds1, binds1) <- checkLoop env irreds
- ; return (irreds1, binds `unionBags` binds1) } }
+ ; let all_needed_givens = needed_givens ++ more_needed_givens
+
+ ; if not improved then
+ return (irreds, binds, all_needed_givens)
+ else do
+
+ -- If improvement did some unification, we go round again.
+ -- We start again with irreds, not wanteds
+ -- Using an instance decl might have introduced a fresh type variable
+ -- which might have been unified, so we'd get an infinite loop
+ -- if we started again with wanteds! See Note [LOOP]
+ { (irreds1, binds1, all_needed_givens1) <- go env irreds all_needed_givens
+ ; return (irreds1, binds `unionBags` binds1, all_needed_givens1) } }
\end{code}
Note [LOOP]
-> [Inst] -- Wanted
-> TcM TcDictBinds
tcSimplifySuperClasses loc givens sc_wanteds
- = do { (irreds, binds1) <- checkLoop env sc_wanteds
+ = do { traceTc (text "tcSimplifySuperClasses")
+ ; (irreds,binds1,_) <- checkLoop env sc_wanteds
; let (tidy_env, tidy_irreds) = tidyInsts irreds
; reportNoInstances tidy_env (Just (loc, givens)) tidy_irreds
; return binds1 }
tcSimplifyRestricted doc top_lvl bndrs tau_tvs wanteds
-- Zonk everything in sight
- = do { wanteds' <- mappM zonkInst wanteds
+ = do { traceTc (text "tcSimplifyRestricted")
+ ; wanteds' <- zonkInsts wanteds
-- 'ReduceMe': Reduce as far as we can. Don't stop at
-- dicts; the idea is to get rid of as many type
-- 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'
+ ; (_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
+ ; constrained_dicts' <- zonkInsts constrained_dicts
; let qtvs1 = tau_tvs' `minusVarSet` oclose (fdPredsOfInsts constrained_dicts) gbl_tvs'
-- As in tcSimplifyInfer
(is_nested_group || isDict inst) = Stop
| otherwise = ReduceMe AddSCs
env = mkNoImproveRedEnv doc try_me
- ; (_imp, binds, irreds) <- reduceContext env wanteds'
+ ; (_imp, binds, irreds, _) <- reduceContext env wanteds'
-- See "Notes on implicit parameters, Question 4: top level"
; ASSERT( all (isFreeWrtTyVars qtvs) irreds ) -- None should be captured
-- 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)
+ GenInst ws' rhs -> go dicts (addBind binds w rhs) (ws' ++ ws)
NoInstance -> pprPanic "tcSimplifyRuleLhs" (ppr w)
}
\end{code}
-- makes them the same.
tcSimplifyIPs given_ips wanteds
- = do { wanteds' <- mappM zonkInst wanteds
- ; given_ips' <- mappM zonkInst given_ips
+ = do { wanteds' <- zonkInsts wanteds
+ ; given_ips' <- zonkInsts 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'
+ ; (improved, binds, irreds, _) <- reduceContext env wanteds'
; if not improved then
ASSERT( all is_free irreds )
returnM emptyLHsBinds
| otherwise
- = do { (irreds, binds) <- checkLoop env for_me
+ = do { (irreds, binds,_) <- checkLoop env for_me
; extendLIEs not_for_me
; extendLIEs irreds
; return binds }
-> [Inst] -- Wanted
-> TcM (ImprovementDone,
TcDictBinds, -- Dictionary bindings
- [Inst]) -- Irreducible
+ [Inst], -- Irreducible
+ [Inst]) -- Needed givens
reduceContext env wanteds
= do { traceTc (text "reduceContext" <+> (vcat [
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 givens = red_givens env
+ (given_eqs0,given_dicts0) = partitionGivenEqInsts givens
+ (wanted_eqs,wanted_dicts) = partitionWantedEqInsts wanteds
+
+ ; -- 1. Normalise the *given* *equality* constraints
+ (given_eqs,eliminate_skolems) <- normaliseGivens given_eqs0
- ; let improved = availsImproved avails
- ; (binds, irreds) <- extractResults avails wanteds
+ ; -- 2. Normalise the *given* *dictionary* constraints
+ -- wrt. the toplevel and given equations
+ (given_dicts,given_binds) <- normaliseGivenDicts given_eqs given_dicts0
+
+ ; -- 3. Solve the *wanted* *equation* constraints
+ eq_irreds0 <- solveWanteds given_eqs wanted_eqs
+
+ -- 4. Normalise the *wanted* equality constraints with respect to each other
+ ; eq_irreds <- normaliseWanteds eq_irreds0
+
+-- -- 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
+
+ -- 5. Build the Avail mapping from "given_dicts"
+ ; init_state <- foldlM addGiven emptyAvails given_dicts
+
+ -- 6. Solve the *wanted* *dictionary* constraints
+ -- This may expose some further equational constraints...
+ ; wanted_dicts' <- zonkInsts wanted_dicts
+ ; avails <- reduceList env wanted_dicts' init_state
+ ; (binds, irreds0, needed_givens) <- extractResults avails wanted_dicts'
+ ; traceTc (text "reduceContext extractresults" <+> vcat
+ [ppr avails,ppr wanted_dicts',ppr binds,ppr needed_givens])
+
+ ; -- 7. Normalise the *wanted* *dictionary* constraints
+ -- wrt. the toplevel and given equations
+ (irreds1,normalise_binds1) <- normaliseWantedDicts given_eqs irreds0
+
+ ; -- 8. Substitute the wanted *equations* in the wanted *dictionaries*
+ (irreds,normalise_binds2) <- substEqInDictInsts eq_irreds irreds1
+
+ ; -- 9. eliminate the artificial skolem constants introduced in 1.
+ eliminate_skolems
+
+ -- If there was some FD improvement,
+ -- or new wanted equations have been exposed,
+ -- we should have another go at solving.
+ ; let improved = availsImproved avails
+ || (not $ isEmptyBag normalise_binds1)
+ || (not $ isEmptyBag normalise_binds2)
+ || (not $ null $ fst $ partitionGivenEqInsts irreds)
; traceTc (text "reduceContext end" <+> (vcat [
text "----------------------",
text "avails" <+> pprAvails avails,
text "improved =" <+> ppr improved,
text "irreds = " <+> ppr irreds,
+ text "binds = " <+> ppr binds,
+ text "needed givens = " <+> ppr needed_givens,
text "----------------------"
]))
- ; return (improved, binds, irreds) }
+ ; return (improved, given_binds `unionBags` normalise_binds1 `unionBags` normalise_binds2 `unionBags` binds, irreds ++ eq_irreds, needed_givens) }
tcImproveOne :: Avails -> Inst -> TcM ImprovementDone
tcImproveOne avails inst
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 (w:ws) state = do { traceTc (text "reduceList " <+> ppr (w:ws) <+> ppr state)
+ ; state' <- reduce (env {red_stack = (n+1, w:stk)}) w state
; go ws state' }
-- 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
+ = do { traceTc (text "reduce: found " <+> ppr 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!
+ = do { traceTc (text "reduce" <+> ppr avails <+> ppr wanted)
+ ; case red_try_me env wanted of {
+ Stop -> try_simple (addIrred NoSCs);
+ -- See Note [No superclasses for Stop]
+
+ ReduceMe want_scs -> do -- It should be reduced
+ { (avails, lookup_result) <- reduceInst env avails wanted
+ ; case lookup_result of
+ NoInstance -> addIrred want_scs avails wanted
-- Add it and its superclasses
- addIrred want_scs avails wanted
-
- GenInst [] rhs -> addWanted want_scs avails wanted rhs []
+
+ 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' }
+ 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
+ -- superclasses too, and that 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)
; return (avails, result) }
\end{code}
+Note [Equational Constraints in Implication Constraints]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+An equational constraint is of the form
+ Given => Wanted
+where Given and Wanted may contain both equational and dictionary
+constraints. The delay and reduction of these two kinds of constraints
+is distinct:
+
+-) In the generated code, wanted Dictionary constraints are wrapped up in an
+ implication constraint that is created at the code site where the wanted
+ dictionaries can be reduced via a let-binding. This let-bound implication
+ constraint is deconstructed at the use-site of the wanted dictionaries.
+
+-) While the reduction of equational constraints is also delayed, the delay
+ is not manifest in the generated code. The required evidence is generated
+ in the code directly at the use-site. There is no let-binding and deconstruction
+ necessary. The main disadvantage is that we cannot exploit sharing as the
+ same evidence may be generated at multiple use-sites. However, this disadvantage
+ is limited because it only concerns coercions which are erased.
+
+The different treatment is motivated by the different in representation. Dictionary
+constraints require manifest runtime dictionaries, while equations require coercions
+which are types.
+
\begin{code}
---------------------------------------------
reduceImplication :: RedEnv
\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
+ -- Note on coercion variables:
+ --
+ -- The extra given coercion variables are bound at two different sites:
+ -- -) in the creation context of the implication constraint
+ -- the solved equational constraints use these binders
+ --
+ -- -) at the solving site of the implication constraint
+ -- the solved dictionaries use these binders
+ -- these binders are generated by reduceImplication
+ --
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
+ -- Todo fix this
+ (refined_red_givens,refined_avails)
+ <- if isEmptyRefinement reft then return (red_givens env,orig_avails)
+ else foldlM (addRefinedGiven reft) ([],orig_avails) (red_givens env)
-- Solve the sub-problem
; let try_me inst = ReduceMe AddSCs -- Note [Freeness and implications]
- env' = env { red_givens = refined_red_givens ++ extra_givens
+ env' = env { red_givens = refined_red_givens ++ extra_givens ++ availsInsts orig_avails
, 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
+ ppr reft, ppr wanteds])
+ ; (irreds,binds,needed_givens0) <- checkLoop env' wanteds
+ ; let needed_givens1 = [ng | ng <- needed_givens0, notElem ng extra_givens]
- -- Extract the results
-- Note [Reducing implication constraints]
- ; (binds, irreds) <- extractResults avails wanteds
- ; let (outer, inner) = partition (isJust . findAvail orig_avails) irreds
+ -- Tom -- update note, put somewhere!
; traceTc (text "reduceImplication result" <+> vcat
- [ ppr outer, ppr inner, ppr binds])
+ [ppr irreds, ppr binds, ppr needed_givens1])
+-- ; avails <- reduceList env' wanteds avails
+--
+-- -- Extract the binding
+-- ; (binds, irreds) <- extractResults avails wanteds
+ ; (refinement_binds,needed_givens) <- extractLocalResults refined_avails needed_givens1
+ ; traceTc (text "reduceImplication local results" <+> vcat
+ [ppr refinement_binds, ppr needed_givens])
+
+ ; -- extract superclass binds
+ -- (sc_binds,_) <- extractResults avails []
+-- ; traceTc (text "reduceImplication sc_binds" <+> vcat
+-- [ppr sc_binds, ppr avails])
+--
-- 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
+-- ; let ret_avails = avails
+ ; let ret_avails = orig_avails
+-- ; let ret_avails = updateImprovement orig_avails avails
- ; if isEmptyLHsBinds binds && null outer then -- No progress
+ ; traceTc (text "reduceImplication condition" <+> ppr ((isEmptyLHsBinds binds) || (null irreds)))
+
+-- Porgress is no longer measered by the number of bindings
+-- ; if isEmptyLHsBinds binds then -- No progress
+ ; if (isEmptyLHsBinds binds) && (not $ null irreds) then
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)
+ {
+ ; (implic_insts, bind) <- makeImplicationBind inst_loc tvs reft extra_givens irreds
+ -- This binding is useless if the recursive simplification
+ -- made no progress; but currently we don't try to optimise that
+ -- case. After all, we only try hard to reduce at top level, or
+ -- when inferring types.
+
+ ; let dict_wanteds = filter (not . isEqInst) wanteds
+ (extra_eq_givens,extra_dict_givens) = partitionGivenEqInsts extra_givens
+ dict_ids = map instToId extra_dict_givens
+ -- TOMDO: given equational constraints bug!
+ -- we need a different evidence for given
+ -- equations depending on whether we solve
+ -- dictionary constraints or equational constraints
+ eq_tyvars = uniqSetToList $ tyVarsOfTypes $ map eqInstType extra_eq_givens
+ -- dict_ids = map instToId extra_givens
+ co = mkWpTyLams tvs <.> mkWpTyLams eq_tyvars <.> mkWpLams dict_ids <.> WpLet (binds `unionBags` refinement_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
+ payload | [dict_wanted] <- dict_wanteds = HsVar (instToId dict_wanted)
+ | otherwise = ExplicitTuple (map (L loc . HsVar . instToId) dict_wanteds) Boxed
- ; return (ret_avails, GenInst (implic_insts ++ outer) (L loc rhs))
- } }
+
+ ; traceTc (text "reduceImplication ->" <+> vcat
+ [ ppr ret_avails,
+ ppr implic_insts])
+ -- If there are any irreds, we back off and return NoInstance
+ ; return (ret_avails, GenInst (implic_insts ++ needed_givens) (L loc rhs))
+ }
+ }
\end{code}
Note [Reducing implication constraints]
extractResults :: Avails
-> [Inst] -- Wanted
-> TcM ( TcDictBinds, -- Bindings
- [Inst]) -- Irreducible ones
+ [Inst], -- Irreducible ones
+ [Inst]) -- Needed givens, i.e. ones used in the bindings
extractResults (Avails _ avails) wanteds
- = go avails emptyBag [] wanteds
+ = go avails emptyBag [] [] wanteds
where
- go :: AvailEnv -> TcDictBinds -> [Inst] -> [Inst]
- -> TcM (TcDictBinds, [Inst])
- go avails binds irreds []
- = returnM (binds, irreds)
+ go :: AvailEnv -> TcDictBinds -> [Inst] -> [Inst] -> [Inst]
+ -> TcM (TcDictBinds, [Inst], [Inst])
+ go avails binds irreds givens []
+ = returnM (binds, irreds, givens)
- go avails binds irreds (w:ws)
+ go avails binds irreds givens (w:ws)
= case findAvailEnv avails w of
Nothing -> pprTrace "Urk: extractResults" (ppr w) $
- go avails binds irreds ws
+ go avails binds irreds givens ws
Just (Given id)
- | id == w_id -> go avails binds irreds ws
- | otherwise -> go avails (addBind binds w_id (nlHsVar id)) irreds ws
+ | id == w_id -> go avails binds irreds (w:givens) ws
+ | otherwise -> go avails (addBind binds w (nlHsVar id)) irreds (update_id w id:givens) ws
-- 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
+ Just IsIrred -> go (add_given avails w) binds (w:irreds) givens 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)
+ Just (Rhs rhs ws') -> go (add_given avails w) new_binds irreds givens (ws' ++ ws)
where
- new_binds = addBind binds w_id rhs
+ new_binds = addBind binds w rhs
where
w_id = instToId w
+ update_id m@(Method{}) id = m {tci_id = id}
+ update_id w id = w {tci_name = idName id}
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))
+extractLocalResults :: Avails
+ -> [Inst] -- Wanted
+ -> TcM ( TcDictBinds, -- Bindings
+ [Inst]) -- Needed givens, i.e. ones used in the bindings
+
+extractLocalResults (Avails _ avails) wanteds
+ = go avails emptyBag [] wanteds
+ where
+ go :: AvailEnv -> TcDictBinds -> [Inst] -> [Inst]
+ -> TcM (TcDictBinds, [Inst])
+ go avails binds givens []
+ = returnM (binds, givens)
+
+ go avails binds givens (w:ws)
+ = case findAvailEnv avails w of
+ Nothing -> -- pprTrace "Urk: extractLocalResults" (ppr w) $
+ go avails binds givens ws
+
+ Just IsIrred ->
+ go avails binds givens ws
+
+ Just (Given id)
+ | id == w_id -> go avails binds (w:givens) ws
+ | otherwise -> go avails binds (w{tci_name=idName id}:givens) ws
+ -- The sought Id can be one of the givens, via a superclass chain
+ -- and then we definitely don't want to generate an x=x binding!
+
+ Just (Rhs rhs ws') -> go (add_given avails w) new_binds givens (ws' ++ ws)
+ where
+ new_binds = addBind binds w rhs
+ where
+ w_id = instToId w
+
+ add_given avails w = extendAvailEnv avails w (Given (instToId w))
\end{code}
-- and hopefully the optimiser will spot the duplicated work
| otherwise
= return (refined_givens, avails)
+
+addRefinedGiven' :: Refinement -> [Inst] -> Inst -> TcM [Inst]
+addRefinedGiven' reft refined_givens 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
+ ; return (new_given:refined_givens) }
+ -- 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
\end{code}
Note [ImplicInst rigidity]
-- error message generation for the monomorphism restriction
tc_simplify_top doc interactive wanteds
= do { dflags <- getDOpts
- ; wanteds <- mapM zonkInst wanteds
+ ; wanteds <- zonkInsts wanteds
; mapM_ zonkTopTyVar (varSetElems (tyVarsOfInsts wanteds))
+ ; traceTc (text "tc_simplify_top 0: " <+> ppr wanteds)
; (irreds1, binds1) <- tryHardCheckLoop doc1 wanteds
+ ; traceTc (text "tc_simplify_top 1: " <+> ppr irreds1)
; (irreds2, binds2) <- approximateImplications doc2 (\d -> True) irreds1
+ ; traceTc (text "tc_simplify_top 2: " <+> ppr irreds2)
-- Use the defaulting rules to do extra unification
-- NB: irreds2 are already zonked
= return (insts, emptyBag)
| null defaultable_groups
- = do { traceTc (text "disambiguate1" <+> vcat [ppr insts, ppr unaries, ppr bad_tvs, ppr defaultable_groups])
+ = do { traceTc (text "disambigutate, no defaultable groups" <+> vcat [ppr unaries, ppr insts, ppr bad_tvs, ppr defaultable_groups])
; return (insts, emptyBag) }
| otherwise
disambigGroup default_tys dicts
= try_default default_tys
where
- (_,_,tyvar) = head dicts -- Should be non-empty
+ (_,_,tyvar) = ASSERT(not (null dicts)) head dicts -- Should be non-empty
classes = [c | (_,c,_) <- dicts]
try_default [] = return ()
-- After this we can't fail
; warnDefault dicts default_ty
- ; unifyType default_ty (mkTyVarTy tyvar) }
+ ; unifyType default_ty (mkTyVarTy tyvar)
+ ; return () -- TOMDO: do something with the coercion
+ }
-----------------------
= groupErrs (report_no_instances tidy_env mb_what) insts
report_no_instances tidy_env mb_what insts
- = do { inst_envs <- tcGetInstEnvs
- ; let (implics, insts1) = partition isImplicInst insts
- (insts2, overlaps) = partitionWith (check_overlap inst_envs) insts1
- ; traceTc (text "reportNoInstnces" <+> vcat
- [ppr implics, ppr insts1, ppr insts2])
- ; mapM_ complain_implic implics
- ; mapM_ (\doc -> addErrTcM (tidy_env, doc)) overlaps
- ; groupErrs complain_no_inst insts2 }
+ = do { inst_envs <- tcGetInstEnvs
+ ; let (implics, insts1) = partition isImplicInst insts
+ (insts2, overlaps) = partitionWith (check_overlap inst_envs) insts1
+ (eqInsts, insts3) = partition isEqInst insts2
+ ; traceTc (text "reportNoInstances" <+> vcat
+ [ppr implics, ppr insts1, ppr insts2])
+ ; mapM_ complain_implic implics
+ ; mapM_ (\doc -> addErrTcM (tidy_env, doc)) overlaps
+ ; groupErrs complain_no_inst insts3
+ ; mapM_ complain_eq eqInsts
+ }
where
complain_no_inst insts = addErrTcM (tidy_env, mk_no_inst_err insts)
(Just (tci_loc inst, tci_given inst))
(tci_wanted inst)
+ complain_eq EqInst {tci_left = lty, tci_right = rty,
+ tci_loc = InstLoc _ _ ctxt}
+ = do { (env, msg) <- misMatchMsg lty rty
+ ; setErrCtxt ctxt $
+ failWithTcM (env, msg)
+ }
+
check_overlap :: (InstEnv,InstEnv) -> Inst -> Either Inst SDoc
-- Right msg => overlap message
-- Left inst => no instance
| not (isClassDict wanted) = Left wanted
| otherwise
= case lookupInstEnv inst_envs clas tys of
- -- The case of exactly one match and no unifiers means
- -- a successful lookup. That can't happen here, becuase
- -- dicts only end up here if they didn't match in Inst.lookupInst
+ -- The case of exactly one match and no unifiers means a
+ -- successful lookup. That can't happen here, because dicts
+ -- only end up here if they didn't match in Inst.lookupInst
#ifdef DEBUG
([m],[]) -> pprPanic "reportNoInstance" (ppr wanted)
#endif
nest 4 (pprStack stack)]
pprStack stack = vcat (map pprInstInFull stack)
+
+-----------------------
+misMatchMsg :: TcType -> TcType -> TcM (TidyEnv, SDoc)
+-- Generate the message when two types fail to match,
+-- going to some trouble to make it helpful.
+-- The argument order is: actual type, expected type
+misMatchMsg ty_act ty_exp
+ = do { env0 <- tcInitTidyEnv
+ ; (env1, pp_exp, extra_exp) <- ppr_ty env0 ty_exp ty_act
+ ; (env2, pp_act, extra_act) <- ppr_ty env1 ty_act ty_exp
+ ; return (env2,
+ sep [sep [ptext SLIT("Couldn't match expected type") <+> pp_exp,
+ nest 7 $
+ ptext SLIT("against inferred type") <+> pp_act],
+ nest 2 (extra_exp $$ extra_act)]) }
+
+ppr_ty :: TidyEnv -> TcType -> TcType -> TcM (TidyEnv, SDoc, SDoc)
+ppr_ty env ty other_ty
+ = do { ty' <- zonkTcType ty
+ ; let (env1, tidy_ty) = tidyOpenType env ty'
+ ; (env2, extra) <- ppr_extra env1 tidy_ty other_ty
+ ; return (env2, quotes (ppr tidy_ty), extra) }
+
+-- (ppr_extra env ty other_ty) shows extra info about 'ty'
+ppr_extra env (TyVarTy tv) other_ty
+ | isSkolemTyVar tv || isSigTyVar tv
+ = return (env1, pprSkolTvBinding tv1)
+ where
+ (env1, tv1) = tidySkolemTyVar env tv
+
+ppr_extra env (TyConApp tc1 _) (TyConApp tc2 _)
+ | getOccName tc1 == getOccName tc2
+ = -- This case helps with messages that would otherwise say
+ -- Could not match 'T' does not match 'M.T'
+ -- which is not helpful
+ do { this_mod <- getModule
+ ; return (env, quotes (ppr tc1) <+> ptext SLIT("is defined") <+> mk_mod this_mod) }
+ where
+ tc_mod = nameModule (getName tc1)
+ tc_pkg = modulePackageId tc_mod
+ tc2_pkg = modulePackageId (nameModule (getName tc2))
+ mk_mod this_mod
+ | tc_mod == this_mod = ptext SLIT("in this module")
+
+ | not home_pkg && tc2_pkg /= tc_pkg = pp_pkg
+ -- Suppress the module name if (a) it's from another package
+ -- (b) other_ty isn't from that same package
+
+ | otherwise = ptext SLIT("in module") <+> quotes (ppr tc_mod) <+> pp_pkg
+ where
+ home_pkg = tc_pkg == modulePackageId this_mod
+ pp_pkg | home_pkg = empty
+ | otherwise = ptext SLIT("in package") <+> quotes (ppr tc_pkg)
+
+ppr_extra env ty other_ty = return (env, empty) -- Normal case
\end{code}
; -- (1) kind check the right-hand side of the type equation
; k_rhs <- kcCheckHsType (tcdSynRhs decl) resKind
- -- we need at least as many type parameters as the family declaration
- -- specified
+ -- we need the exact same number of type parameters as the family
+ -- declaration
; let famArity = tyConArity family
- ; checkTc (length k_typats >= famArity) $ tooFewParmsErr famArity
+ ; checkTc (length k_typats == famArity) $
+ wrongNumberOfParmsErr famArity
-- (2) type check type equation
; tcTyVarBndrs k_tvs $ \t_tvs -> do { -- turn kinded into proper tyvars
; t_typats <- mappM tcHsKindedType k_typats
; t_rhs <- tcHsKindedType k_rhs
- -- all parameters in excess of the family arity must be variables
- ; checkTc (all isTyVarTy $ drop famArity t_typats) $ excessParmVarErr
-
-- (3) check that
-- - left-hand side contains no type family applications
-- (vanilla synonyms are fine, though)
; tc_rhs <-
case new_or_data of
DataType -> return (mkDataTyConRhs data_cons)
- NewType -> ASSERT( isSingleton data_cons )
+ NewType -> ASSERT( not (null data_cons) )
mkNewTyConRhs rep_tc_name tycon (head data_cons)
; buildAlgTyCon rep_tc_name t_tvs stupid_theta tc_rhs Recursive
False h98_syntax (Just (family, t_typats))
else case new_or_data of
DataType -> return (mkDataTyConRhs data_cons)
NewType ->
- ASSERT( isSingleton data_cons )
+ ASSERT( not (null data_cons) )
mkNewTyConRhs tc_name tycon (head data_cons)
; buildAlgTyCon tc_name final_tvs stupid_theta tc_rhs is_rec
(want_generic && canDoGenerics data_cons) h98_syntax Nothing
-- One argument
; checkTc (null eq_spec) (newtypePredError con)
-- Return type is (T a b c)
- ; checkTc (null ex_tvs && null theta) (newtypeExError con)
+ ; checkTc (null ex_tvs && null eq_theta && null dict_theta) (newtypeExError con)
-- No existentials
; checkTc (not (any isMarkedStrict (dataConStrictMarks con)))
(newtypeStrictError con)
-- No strictness
}
where
- (_univ_tvs, ex_tvs, eq_spec, theta, arg_tys, _res_ty) = dataConFullSig con
+ (_univ_tvs, ex_tvs, eq_spec, eq_theta, dict_theta, arg_tys, _res_ty) = dataConFullSig con
-------------------------------
checkValidClass :: Class -> TcM ()
-- The 'tail' removes the initial (C a) from the
-- class itself, leaving just the method type
+ ; traceTc (text "class op type" <+> ppr op_ty <+> ppr tau)
; checkValidType (FunSigCtxt op_name) tau
-- Check that the type mentions at least one of
= ptext SLIT("Family instance has too few parameters; expected") <+>
ppr arity
-excessParmVarErr
- = ptext SLIT("Additional instance parameters must be variables")
+wrongNumberOfParmsErr exp_arity
+ = ptext SLIT("Number of parameters must match family declaration; expected")
+ <+> ppr exp_arity
badBootFamInstDeclErr =
ptext SLIT("Illegal family instance in hs-boot file")
--- /dev/null
+
+\begin{code}
+
+module TcTyFuns(
+ finalizeEqInst,
+ partitionWantedEqInsts, partitionGivenEqInsts,
+
+ tcNormalizeFamInst,
+
+ normaliseGivens, normaliseGivenDicts,
+ normaliseWanteds, normaliseWantedDicts,
+ solveWanteds,
+ substEqInDictInsts,
+
+ addBind -- should not be here
+ ) where
+
+
+#include "HsVersions.h"
+
+import HsSyn
+
+import TcRnMonad
+import TcEnv
+import Inst
+import FamInstEnv
+import TcType
+import TcMType
+import Coercion
+import TypeRep ( Type(..) )
+import TyCon
+import Var ( mkCoVar, isTcTyVar )
+import Type
+import HscTypes ( ExternalPackageState(..) )
+import Bag
+import Outputable
+import SrcLoc ( Located(..) )
+import Maybes
+
+import Data.List
+\end{code}
+
+%************************************************************************
+%* *
+\section{Eq Insts}
+%* *
+%************************************************************************
+
+%************************************************************************
+%* *
+\section{Utility Code}
+%* *
+%************************************************************************
+
+\begin{code}
+partitionWantedEqInsts
+ :: [Inst] -- wanted insts
+ -> ([Inst],[Inst]) -- (wanted equations,wanted dicts)
+partitionWantedEqInsts = partitionEqInsts True
+
+partitionGivenEqInsts
+ :: [Inst] -- given insts
+ -> ([Inst],[Inst]) -- (given equations,given dicts)
+partitionGivenEqInsts = partitionEqInsts False
+
+
+partitionEqInsts
+ :: Bool -- <=> wanted
+ -> [Inst] -- insts
+ -> ([Inst],[Inst]) -- (equations,dicts)
+partitionEqInsts wanted []
+ = ([],[])
+partitionEqInsts wanted (i:is)
+ | isEqInst i
+ = (i:es,ds)
+ | otherwise
+ = (es,i:ds)
+ where (es,ds) = partitionEqInsts wanted is
+
+isEqDict :: Inst -> Bool
+isEqDict (Dict {tci_pred = EqPred _ _}) = True
+isEqDict _ = False
+
+\end{code}
+
+
+%************************************************************************
+%* *
+ Normalisation of types
+%* *
+%************************************************************************
+
+Unfold a single synonym family instance and yield the witnessing coercion.
+Return 'Nothing' if the given type is either not synonym family instance
+or is a synonym family instance that has no matching instance declaration.
+(Applies only if the type family application is outermost.)
+
+For example, if we have
+
+ :Co:R42T a :: T [a] ~ :R42T a
+
+then 'T [Int]' unfolds to (:R42T Int, :Co:R42T Int).
+
+\begin{code}
+tcUnfoldSynFamInst :: Type -> TcM (Maybe (Type, Coercion))
+tcUnfoldSynFamInst (TyConApp tycon tys)
+ | not (isOpenSynTyCon tycon) -- unfold *only* _synonym_ family instances
+ = return Nothing
+ | otherwise
+ = do { maybeFamInst <- tcLookupFamInst tycon tys
+ ; case maybeFamInst of
+ Nothing -> return Nothing
+ Just (rep_tc, rep_tys) -> return $ Just (mkTyConApp rep_tc rep_tys,
+ mkTyConApp coe_tc rep_tys)
+ where
+ coe_tc = expectJust "TcTyFun.tcUnfoldSynFamInst"
+ (tyConFamilyCoercion_maybe rep_tc)
+ }
+tcUnfoldSynFamInst _other = return Nothing
+\end{code}
+
+Normalise 'Type's and 'PredType's by unfolding type family applications where
+possible (ie, we treat family instances as a TRS). Also zonk meta variables.
+
+ tcNormalizeFamInst ty = (co, ty')
+ then co : ty ~ ty'
+
+\begin{code}
+tcNormalizeFamInst :: Type -> TcM (CoercionI, Type)
+tcNormalizeFamInst = tcGenericNormalizeFamInst tcUnfoldSynFamInst
+
+tcNormalizeFamInstPred :: TcPredType -> TcM (CoercionI, TcPredType)
+tcNormalizeFamInstPred = tcGenericNormalizeFamInstPred tcUnfoldSynFamInst
+\end{code}
+
+Generic normalisation of 'Type's and 'PredType's; ie, walk the type term and
+apply the normalisation function gives as the first argument to every TyConApp
+and every TyVarTy subterm.
+
+ tcGenericNormalizeFamInst fun ty = (co, ty')
+ then co : ty ~ ty'
+
+This function is (by way of using smart constructors) careful to ensure that
+the returned coercion is exactly IdCo (and not some semantically equivalent,
+but syntactically different coercion) whenever (ty' `tcEqType` ty). This
+makes it easy for the caller to determine whether the type changed. BUT
+even if we return IdCo, ty' may be *syntactically* different from ty due to
+unfolded closed type synonyms (by way of tcCoreView). In the interest of
+good error messages, callers should discard ty' in favour of ty in this case.
+
+\begin{code}
+tcGenericNormalizeFamInst :: (TcType -> TcM (Maybe (TcType,Coercion)))
+ -- what to do with type functions and tyvars
+ -> TcType -- old type
+ -> TcM (CoercionI, Type) -- (coercion, new type)
+tcGenericNormalizeFamInst fun ty
+ | Just ty' <- tcView ty = tcGenericNormalizeFamInst fun ty'
+tcGenericNormalizeFamInst fun ty@(TyConApp tyCon tys)
+ = do { (cois, ntys) <- mapAndUnzipM (tcGenericNormalizeFamInst fun) tys
+ ; let tycon_coi = mkTyConAppCoI tyCon ntys cois
+ ; maybe_ty_co <- fun (TyConApp tyCon ntys) -- use normalised args!
+ ; case maybe_ty_co of
+ -- a matching family instance exists
+ Just (ty', co) ->
+ do { let first_coi = mkTransCoI tycon_coi (ACo co)
+ ; (rest_coi, nty) <- tcGenericNormalizeFamInst fun ty'
+ ; let fix_coi = mkTransCoI first_coi rest_coi
+ ; return (fix_coi, nty)
+ }
+ -- no matching family instance exists
+ -- we do not do anything
+ Nothing -> return (tycon_coi, TyConApp tyCon ntys)
+ }
+tcGenericNormalizeFamInst fun ty@(AppTy ty1 ty2)
+ = do { (coi1,nty1) <- tcGenericNormalizeFamInst fun ty1
+ ; (coi2,nty2) <- tcGenericNormalizeFamInst fun ty2
+ ; return (mkAppTyCoI nty1 coi1 nty2 coi2, AppTy nty1 nty2)
+ }
+tcGenericNormalizeFamInst fun ty@(FunTy ty1 ty2)
+ = do { (coi1,nty1) <- tcGenericNormalizeFamInst fun ty1
+ ; (coi2,nty2) <- tcGenericNormalizeFamInst fun ty2
+ ; return (mkFunTyCoI nty1 coi1 nty2 coi2, FunTy nty1 nty2)
+ }
+tcGenericNormalizeFamInst fun ty@(ForAllTy tyvar ty1)
+ = do { (coi,nty1) <- tcGenericNormalizeFamInst fun ty1
+ ; return (mkForAllTyCoI tyvar coi,ForAllTy tyvar nty1)
+ }
+tcGenericNormalizeFamInst fun ty@(NoteTy note ty1)
+ = do { (coi,nty1) <- tcGenericNormalizeFamInst fun ty1
+ ; return (mkNoteTyCoI note coi,NoteTy note nty1)
+ }
+tcGenericNormalizeFamInst fun ty@(TyVarTy tv)
+ | isTcTyVar tv
+ = do { traceTc (text "tcGenericNormalizeFamInst" <+> ppr ty)
+ ; res <- lookupTcTyVar tv
+ ; case res of
+ DoneTv _ ->
+ do { maybe_ty' <- fun ty
+ ; case maybe_ty' of
+ Nothing -> return (IdCo, ty)
+ Just (ty', co1) ->
+ do { (coi2, ty'') <- tcGenericNormalizeFamInst fun ty'
+ ; return (ACo co1 `mkTransCoI` coi2, ty'')
+ }
+ }
+ IndirectTv ty' -> tcGenericNormalizeFamInst fun ty'
+ }
+ | otherwise
+ = return (IdCo, ty)
+tcGenericNormalizeFamInst fun (PredTy predty)
+ = do { (coi, pred') <- tcGenericNormalizeFamInstPred fun predty
+ ; return (coi, PredTy pred') }
+
+---------------------------------
+tcGenericNormalizeFamInstPred :: (TcType -> TcM (Maybe (TcType,Coercion)))
+ -> TcPredType
+ -> TcM (CoercionI, TcPredType)
+
+tcGenericNormalizeFamInstPred fun (ClassP cls tys)
+ = do { (cois, tys')<- mapAndUnzipM (tcGenericNormalizeFamInst fun) tys
+ ; return (mkClassPPredCoI cls tys' cois, ClassP cls tys')
+ }
+tcGenericNormalizeFamInstPred fun (IParam ipn ty)
+ = do { (coi, ty') <- tcGenericNormalizeFamInst fun ty
+ ; return $ (mkIParamPredCoI ipn coi, IParam ipn ty')
+ }
+tcGenericNormalizeFamInstPred fun (EqPred ty1 ty2)
+ = do { (coi1, ty1') <- tcGenericNormalizeFamInst fun ty1
+ ; (coi2, ty2') <- tcGenericNormalizeFamInst fun ty2
+ ; return (mkEqPredCoI ty1' coi1 ty2' coi2, EqPred ty1' ty2') }
+\end{code}
+
+
+%************************************************************************
+%* *
+\section{Normalisation of Given Dictionaries}
+%* *
+%************************************************************************
+
+\begin{code}
+normaliseGivenDicts, normaliseWantedDicts
+ :: [Inst] -- given equations
+ -> [Inst] -- dictionaries
+ -> TcM ([Inst],TcDictBinds)
+
+normaliseGivenDicts eqs dicts = normalise_dicts eqs dicts False
+normaliseWantedDicts eqs dicts = normalise_dicts eqs dicts True
+
+normalise_dicts
+ :: [Inst] -- given equations
+ -> [Inst] -- dictionaries
+ -> Bool -- True <=> the dicts are wanted
+ -- Fals <=> they are given
+ -> TcM ([Inst],TcDictBinds)
+normalise_dicts given_eqs dicts is_wanted
+ = do { traceTc $ text "normaliseGivenDicts <-" <+> ppr dicts <+>
+ text "with" <+> ppr given_eqs
+ ; (dicts0, binds0) <- normaliseInsts is_wanted dicts
+ ; (dicts1, binds1) <- substEqInDictInsts given_eqs dicts0
+ ; let binds01 = binds0 `unionBags` binds1
+ ; if isEmptyBag binds1
+ then return (dicts1, binds01)
+ else do { (dicts2, binds2) <- normaliseGivenDicts given_eqs dicts1
+ ; return (dicts2, binds01 `unionBags` binds2) } }
+\end{code}
+
+
+%************************************************************************
+%* *
+\section{Normalisation of Wanteds}
+%* *
+%************************************************************************
+
+\begin{code}
+normaliseWanteds :: [Inst] -> TcM [Inst]
+normaliseWanteds insts
+ = do { traceTc (text "normaliseWanteds" <+> ppr insts)
+ ; result <- eq_rewrite
+ [ ("(Occurs)", simple_rewrite_check $ occursCheckInsts)
+ , ("(ZONK)", simple_rewrite $ zonkInsts)
+ , ("(TRIVIAL)", trivialInsts)
+ , ("(SWAP)", swapInsts)
+ , ("(DECOMP)", decompInsts)
+ , ("(TOP)", topInsts)
+ , ("(SUBST)", substInsts)
+ , ("(UNIFY)", unifyInsts)
+ ] insts
+ ; traceTc (text "normaliseWanteds ->" <+> ppr result)
+ ; return result
+ }
+\end{code}
+
+%************************************************************************
+%* *
+\section{Normalisation of Givens}
+%* *
+%************************************************************************
+
+\begin{code}
+
+normaliseGivens :: [Inst] -> TcM ([Inst],TcM ())
+normaliseGivens givens =
+ do { traceTc (text "normaliseGivens <-" <+> ppr givens)
+ ; (result,action) <- given_eq_rewrite
+ ("(SkolemOccurs)", skolemOccurs)
+ (return ())
+ [("(Occurs)", simple_rewrite_check $ occursCheckInsts),
+ ("(ZONK)", simple_rewrite $ zonkInsts),
+ ("(TRIVIAL)", trivialInsts),
+ ("(SWAP)", swapInsts),
+ ("(DECOMP)", decompInsts),
+ ("(TOP)", topInsts),
+ ("(SUBST)", substInsts)]
+ givens
+ ; traceTc (text "normaliseGivens ->" <+> ppr result)
+ ; return (result,action)
+ }
+
+skolemOccurs :: [Inst] -> TcM ([Inst],TcM ())
+skolemOccurs [] = return ([], return ())
+skolemOccurs (inst@(EqInst {}):insts)
+ = do { (insts',actions) <- skolemOccurs insts
+ -- check whether the current inst co :: ty1 ~ ty2 suffers
+ -- from the occurs check issue: F ty1 \in ty2
+ ; let occurs = go False ty2
+ ; if occurs
+ then
+ -- if it does generate two new coercions:
+ do { skolem_var <- newMetaTyVar TauTv (typeKind ty1)
+ ; let skolem_ty = TyVarTy skolem_var
+ -- ty1 :: ty1 ~ b
+ ; inst1 <- mkEqInst (EqPred ty1 skolem_ty) (mkGivenCo ty1)
+ -- sym co :: ty2 ~ b
+ ; inst2 <- mkEqInst (EqPred ty2 skolem_ty) (mkGivenCo $ fromACo $ mkSymCoI $ ACo $ fromGivenCo co)
+ -- to replace the old one
+ -- the corresponding action is
+ -- b := ty1
+ ; let action = writeMetaTyVar skolem_var ty1
+ ; return (inst1:inst2:insts', action >> actions)
+ }
+ else
+ return (inst:insts', actions)
+ }
+ where
+ ty1 = eqInstLeftTy inst
+ ty2 = eqInstRightTy inst
+ co = eqInstCoercion inst
+ check :: Bool -> TcType -> Bool
+ check flag ty
+ = if flag && ty1 `tcEqType` ty
+ then True
+ else go flag ty
+
+ go flag (TyConApp con tys) = or $ map (check (isOpenSynTyCon con || flag)) tys
+ go flag (FunTy arg res) = or $ map (check flag) [arg,res]
+ go flag (AppTy fun arg) = or $ map (check flag) [fun,arg]
+ go flag ty = False
+\end{code}
+
+%************************************************************************
+%* *
+\section{Solving of Wanteds}
+%* *
+%************************************************************************
+
+\begin{code}
+solveWanteds ::
+ [Inst] -> -- givens
+ [Inst] -> -- wanteds
+ TcM [Inst] -- irreducible wanteds
+solveWanteds givens wanteds =
+ do { traceTc (text "solveWanteds <-" <+> ppr wanteds <+> text "with" <+> ppr givens)
+ ; result <- eq_rewrite
+ [("(Occurs)", simple_rewrite_check $ occursCheckInsts),
+ ("(TRIVIAL)", trivialInsts),
+ ("(DECOMP)", decompInsts),
+ ("(TOP)", topInsts),
+ ("(GIVEN)", givenInsts givens),
+ ("(UNIFY)", unifyInsts)]
+ wanteds
+ ; traceTc (text "solveWanteds ->" <+> ppr result)
+ ; return result
+ }
+
+
+givenInsts :: [Inst] -> [Inst] -> TcM ([Inst],Bool)
+givenInsts [] wanteds
+ = return (wanteds,False)
+givenInsts (g:gs) wanteds
+ = do { (wanteds1,changed1) <- givenInsts gs wanteds
+ ; (wanteds2,changed2) <- substInst g wanteds1
+ ; return (wanteds2,changed1 || changed2)
+ }
+
+
+
+ -- fixpoint computation
+ -- of a number of rewrites of equalities
+eq_rewrite ::
+ [(String,[Inst] -> TcM ([Inst],Bool))] -> -- rewrite functions and descriptions
+ [Inst] -> -- initial equations
+ TcM [Inst] -- final equations (at fixed point)
+eq_rewrite rewrites insts
+ = go rewrites insts
+ where
+ go _ [] -- return quickly when there's nothing to be done
+ = return []
+ go [] insts
+ = return insts
+ go ((desc,r):rs) insts
+ = do { (insts',changed) <- r insts
+ ; traceTc (text desc <+> ppr insts')
+ ; if changed
+ then loop insts'
+ else go rs insts'
+ }
+ loop = eq_rewrite rewrites
+
+ -- fixpoint computation
+ -- of a number of rewrites of equalities
+given_eq_rewrite ::
+
+ (String,[Inst] -> TcM ([Inst],TcM ())) ->
+ (TcM ()) ->
+ [(String,[Inst] -> TcM ([Inst],Bool))] -> -- rewrite functions and descriptions
+ [Inst] -> -- initial equations
+ TcM ([Inst],TcM ()) -- final equations (at fixed point)
+given_eq_rewrite p@(desc,start) acc rewrites insts
+ = do { (insts',acc') <- start insts
+ ; go (acc >> acc') rewrites insts'
+ }
+ where
+ go acc _ [] -- return quickly when there's nothing to be done
+ = return ([],acc)
+ go acc [] insts
+ = return (insts,acc)
+ go acc ((desc,r):rs) insts
+ = do { (insts',changed) <- r insts
+ ; traceTc (text desc <+> ppr insts')
+ ; if changed
+ then loop acc insts'
+ else go acc rs insts'
+ }
+ loop acc = given_eq_rewrite p acc rewrites
+
+simple_rewrite ::
+ ([Inst] -> TcM [Inst]) ->
+ ([Inst] -> TcM ([Inst],Bool))
+simple_rewrite r insts
+ = do { insts' <- r insts
+ ; return (insts',False)
+ }
+
+simple_rewrite_check ::
+ ([Inst] -> TcM ()) ->
+ ([Inst] -> TcM ([Inst],Bool))
+simple_rewrite_check check insts
+ = check insts >> return (insts,False)
+
+
+\end{code}
+
+%************************************************************************
+%* *
+\section{Different forms of Inst rewritings}
+%* *
+%************************************************************************
+
+Rewrite schemata applied by way of eq_rewrite and friends.
+
+\begin{code}
+
+ -- (Trivial)
+ -- g1 : t ~ t
+ -- >-->
+ -- g1 := t
+ --
+trivialInsts ::
+ [Inst] -> -- equations
+ TcM ([Inst],Bool) -- remaining equations, any changes?
+trivialInsts []
+ = return ([],False)
+trivialInsts (i@(EqInst {}):is)
+ = do { (is',changed)<- trivialInsts is
+ ; if tcEqType ty1 ty2
+ then do { eitherEqInst i
+ (\covar -> writeMetaTyVar covar ty1)
+ (\_ -> return ())
+ ; return (is',True)
+ }
+ else return (i:is',changed)
+ }
+ where
+ ty1 = eqInstLeftTy i
+ ty2 = eqInstRightTy i
+
+-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+swapInsts :: [Inst] -> TcM ([Inst],Bool)
+-- All the inputs and outputs are equalities
+swapInsts insts = mapAndUnzipM swapInst insts >>= \(insts',changeds) -> return (insts',or changeds)
+
+
+ -- (Swap)
+ -- g1 : c ~ Fd
+ -- >-->
+ -- g2 : Fd ~ c
+ -- g1 := sym g2
+ --
+swapInst i@(EqInst {})
+ = go ty1 ty2
+ where
+ ty1 = eqInstLeftTy i
+ ty2 = eqInstRightTy i
+ go ty1 ty2 | Just ty1' <- tcView ty1
+ = go ty1' ty2
+ go ty1 ty2 | Just ty2' <- tcView ty2
+ = go ty1 ty2'
+ go (TyConApp tyCon _) _ | isOpenSynTyCon tyCon
+ = return (i,False)
+ -- we should swap!
+ go ty1 ty2@(TyConApp tyCon _)
+ | isOpenSynTyCon tyCon
+ = do { wg_co <- eitherEqInst i
+ -- old_co := sym new_co
+ (\old_covar ->
+ do { new_cotv <- newMetaTyVar TauTv (mkCoKind ty2 ty1)
+ ; let new_co = TyVarTy new_cotv
+ ; writeMetaTyVar old_covar (mkCoercion symCoercionTyCon [new_co])
+ ; return $ mkWantedCo new_cotv
+ })
+ -- new_co := sym old_co
+ (\old_co -> return $ mkGivenCo $ mkCoercion symCoercionTyCon [old_co])
+ ; new_inst <- mkEqInst (EqPred ty2 ty1) wg_co
+ ; return (new_inst,True)
+ }
+ go _ _ = return (i,False)
+
+-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+decompInsts :: [Inst] -> TcM ([Inst],Bool)
+decompInsts insts = do { (insts,bs) <- mapAndUnzipM decompInst insts
+ ; return (concat insts,or bs)
+ }
+
+ -- (Decomp)
+ -- g1 : T cs ~ T ds
+ -- >-->
+ -- g21 : c1 ~ d1, ..., g2n : cn ~ dn
+ -- g1 := T g2s
+ --
+ -- Works also for the case where T is actually an application of a
+ -- type family constructor to a set of types, provided the
+ -- applications on both sides of the ~ are identical;
+ -- see also Note [OpenSynTyCon app] in TcUnify
+ --
+decompInst :: Inst -> TcM ([Inst],Bool)
+decompInst i@(EqInst {})
+ = go ty1 ty2
+ where
+ ty1 = eqInstLeftTy i
+ ty2 = eqInstRightTy i
+ go ty1 ty2
+ | Just ty1' <- tcView ty1 = go ty1' ty2
+ | Just ty2' <- tcView ty2 = go ty1 ty2'
+
+ go ty1@(TyConApp con1 tys1) ty2@(TyConApp con2 tys2)
+ | con1 == con2 && identicalHead
+ = do { cos <- eitherEqInst i
+ -- old_co := Con1 cos
+ (\old_covar ->
+ do { cotvs <- zipWithM (\t1 t2 ->
+ newMetaTyVar TauTv
+ (mkCoKind t1 t2))
+ tys1' tys2'
+ ; let cos = map TyVarTy cotvs
+ ; writeMetaTyVar old_covar (TyConApp con1 cos)
+ ; return $ map mkWantedCo cotvs
+ })
+ -- co_i := Con_i old_co
+ (\old_co -> return $
+ map mkGivenCo $
+ mkRightCoercions (length tys1') old_co)
+ ; insts <- zipWithM mkEqInst (zipWith EqPred tys1' tys2') cos
+ ; return (insts, not $ null insts)
+ }
+ | con1 /= con2 && not (isOpenSynTyCon con1 || isOpenSynTyCon con2)
+ -- not matching data constructors (of any flavour) are bad news
+ = do { env0 <- tcInitTidyEnv
+ ; let (env1, tidy_ty1) = tidyOpenType env0 ty1
+ (env2, tidy_ty2) = tidyOpenType env1 ty2
+ extra = sep [ppr tidy_ty1, char '~', ppr tidy_ty2]
+ msg = ptext SLIT("Couldn't match expected type against inferred type")
+ ; failWithTcM (env2, hang msg 2 extra)
+ }
+ where
+ n = tyConArity con1
+ (idxTys1, tys1') = splitAt n tys1
+ (idxTys2, tys2') = splitAt n tys2
+ identicalHead = not (isOpenSynTyCon con1) ||
+ idxTys1 `tcEqTypes` idxTys2
+
+ go _ _ = return ([i], False)
+
+-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+topInsts :: [Inst] -> TcM ([Inst],Bool)
+topInsts insts
+ = do { (insts,bs) <- mapAndUnzipM topInst insts
+ ; return (insts,or bs)
+ }
+
+ -- (Top)
+ -- g1 : t ~ s
+ -- >--> co1 :: t ~ t' / co2 :: s ~ s'
+ -- g2 : t' ~ s'
+ -- g1 := co1 * g2 * sym co2
+topInst :: Inst -> TcM (Inst,Bool)
+topInst i@(EqInst {})
+ = do { (coi1,ty1') <- tcNormalizeFamInst ty1
+ ; (coi2,ty2') <- tcNormalizeFamInst ty2
+ ; case (coi1,coi2) of
+ (IdCo,IdCo) ->
+ return (i,False)
+ _ ->
+ do { wg_co <- eitherEqInst i
+ -- old_co = co1 * new_co * sym co2
+ (\old_covar ->
+ do { new_cotv <- newMetaTyVar TauTv (mkCoKind ty1 ty2)
+ ; let new_co = TyVarTy new_cotv
+ ; let old_coi = coi1 `mkTransCoI` ACo new_co `mkTransCoI` (mkSymCoI coi2)
+ ; writeMetaTyVar old_covar (fromACo old_coi)
+ ; return $ mkWantedCo new_cotv
+ })
+ -- new_co = sym co1 * old_co * co2
+ (\old_co -> return $ mkGivenCo $ fromACo $ mkSymCoI coi1 `mkTransCoI` ACo old_co `mkTransCoI` coi2)
+ ; new_inst <- mkEqInst (EqPred ty1' ty2') wg_co
+ ; return (new_inst,True)
+ }
+ }
+ where
+ ty1 = eqInstLeftTy i
+ ty2 = eqInstRightTy i
+
+-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+substInsts :: [Inst] -> TcM ([Inst],Bool)
+substInsts insts = substInstsWorker insts []
+
+substInstsWorker [] acc
+ = return (acc,False)
+substInstsWorker (i:is) acc
+ | (TyConApp con _) <- tci_left i, isOpenSynTyCon con
+ = do { (is',change) <- substInst i (acc ++ is)
+ ; if change
+ then return ((i:is'),True)
+ else substInstsWorker is (i:acc)
+ }
+ | otherwise
+ = substInstsWorker is (i:acc)
+
+ -- (Subst)
+ -- g : F c ~ t,
+ -- forall g1 : s1{F c} ~ s2{F c}
+ -- >-->
+ -- g2 : s1{t} ~ s2{t}
+ -- g1 := s1{g} * g2 * sym s2{g} <=> g2 := sym s1{g} * g1 * s2{g}
+substInst inst []
+ = return ([],False)
+substInst inst@(EqInst {tci_left = pattern, tci_right = target}) (i@(EqInst {tci_left = ty1, tci_right = ty2}):is)
+ = do { (is',changed) <- substInst inst is
+ ; (coi1,ty1') <- tcGenericNormalizeFamInst fun ty1
+ ; (coi2,ty2') <- tcGenericNormalizeFamInst fun ty2
+ ; case (coi1,coi2) of
+ (IdCo,IdCo) ->
+ return (i:is',changed)
+ _ ->
+ do { gw_co <- eitherEqInst i
+ -- old_co := co1 * new_co * sym co2
+ (\old_covar ->
+ do { new_cotv <- newMetaTyVar TauTv (mkCoKind ty1' ty2')
+ ; let new_co = TyVarTy new_cotv
+ ; let old_coi = coi1 `mkTransCoI` ACo new_co `mkTransCoI` (mkSymCoI coi2)
+ ; writeMetaTyVar old_covar (fromACo old_coi)
+ ; return $ mkWantedCo new_cotv
+ })
+ -- new_co := sym co1 * old_co * co2
+ (\old_co -> return $ mkGivenCo $ fromACo $ (mkSymCoI coi1) `mkTransCoI` ACo old_co `mkTransCoI` coi2)
+ ; new_inst <- mkEqInst (EqPred ty1' ty2') gw_co
+ ; return (new_inst:is',True)
+ }
+ }
+ where fun ty = return $ if tcEqType pattern ty then Just (target,coercion) else Nothing
+
+ coercion = eitherEqInst inst TyVarTy id
+-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+unifyInsts
+ :: [Inst] -- wanted equations
+ -> TcM ([Inst],Bool)
+unifyInsts insts
+ = do { (insts',changeds) <- mapAndUnzipM unifyInst insts
+ ; return (concat insts',or changeds)
+ }
+
+ -- (UnifyMeta)
+ -- g : alpha ~ t
+ -- >-->
+ -- alpha := t
+ -- g := t
+ --
+ -- TOMDO: you should only do this for certain `meta' type variables
+unifyInst i@(EqInst {tci_left = ty1, tci_right = ty2})
+ | TyVarTy tv1 <- ty1, isMetaTyVar tv1 = go ty2 tv1
+ | TyVarTy tv2 <- ty2, isMetaTyVar tv2 = go ty1 tv2
+ | otherwise = return ([i],False)
+ where go ty tv
+ = do { let cotv = fromWantedCo "unifyInst" $ eqInstCoercion i
+ ; writeMetaTyVar tv ty -- alpha := t
+ ; writeMetaTyVar cotv ty -- g := t
+ ; return ([],True)
+ }
+
+-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+occursCheckInsts :: [Inst] -> TcM ()
+occursCheckInsts insts = mappM_ occursCheckInst insts
+
+
+ -- (OccursCheck)
+ -- t ~ s[T t]
+ -- >-->
+ -- fail
+ --
+occursCheckInst :: Inst -> TcM ()
+occursCheckInst i@(EqInst {tci_left = ty1, tci_right = ty2})
+ = go ty2
+ where
+ check ty = if ty `tcEqType` ty1
+ then occursError
+ else go ty
+
+ go (TyConApp con tys) = if isOpenSynTyCon con then return () else mappM_ check tys
+ go (FunTy arg res) = mappM_ check [arg,res]
+ go (AppTy fun arg) = mappM_ check [fun,arg]
+ go _ = return ()
+
+ occursError = do { env0 <- tcInitTidyEnv
+ ; let (env1, tidy_ty1) = tidyOpenType env0 ty1
+ (env2, tidy_ty2) = tidyOpenType env1 ty2
+ extra = sep [ppr tidy_ty1, char '~', ppr tidy_ty2]
+ ; failWithTcM (env2, hang msg 2 extra)
+ }
+ where msg = ptext SLIT("Occurs check: cannot construct the infinite type")
+\end{code}
+
+Normalises a set of dictionaries relative to a set of given equalities (which
+are interpreted as rewrite rules). We only consider given equalities of the
+form
+
+ F ts ~ t
+
+where F is a type family.
+
+\begin{code}
+substEqInDictInsts :: [Inst] -- given equalities (used as rewrite rules)
+ -> [Inst] -- dictinaries to be normalised
+ -> TcM ([Inst], TcDictBinds)
+substEqInDictInsts eq_insts insts
+ = do { traceTc (text "substEqInDictInst <-" <+> ppr insts)
+ ; result <- foldlM rewriteWithOneEquality (insts, emptyBag) eq_insts
+ ; traceTc (text "substEqInDictInst ->" <+> ppr result)
+ ; return result
+ }
+ where
+ -- (1) Given equality of form 'F ts ~ t': use for rewriting
+ rewriteWithOneEquality (insts, dictBinds)
+ inst@(EqInst {tci_left = pattern,
+ tci_right = target})
+ | isOpenSynTyConApp pattern
+ = do { (insts', moreDictBinds) <- genericNormaliseInsts True {- wanted -}
+ applyThisEq insts
+ ; return (insts', dictBinds `unionBags` moreDictBinds)
+ }
+ where
+ applyThisEq = tcGenericNormalizeFamInstPred (return . matchResult)
+
+ -- rewrite in case of an exact match
+ matchResult ty | tcEqType pattern ty = Just (target, eqInstType inst)
+ | otherwise = Nothing
+
+ -- (2) Given equality has the wrong form: ignore
+ rewriteWithOneEquality (insts, dictBinds) _not_a_rewrite_rule
+ = return (insts, dictBinds)
+\end{code}
+
+%************************************************************************
+%* *
+ Normalisation of Insts
+%* *
+%************************************************************************
+
+Take a bunch of Insts (not EqInsts), and normalise them wrt the top-level
+type-function equations, where
+
+ (norm_insts, binds) = normaliseInsts is_wanted insts
+
+If 'is_wanted'
+ = True, (binds + norm_insts) defines insts (wanteds)
+ = False, (binds + insts) defines norm_insts (givens)
+
+\begin{code}
+normaliseInsts :: Bool -- True <=> wanted insts
+ -> [Inst] -- wanted or given insts
+ -> TcM ([Inst], TcDictBinds) -- normalized insts and bindings
+normaliseInsts isWanted insts
+ = genericNormaliseInsts isWanted tcNormalizeFamInstPred insts
+
+genericNormaliseInsts :: Bool -- True <=> wanted insts
+ -> (TcPredType -> TcM (CoercionI, TcPredType))
+ -- how to normalise
+ -> [Inst] -- wanted or given insts
+ -> TcM ([Inst], TcDictBinds) -- normalized insts & binds
+genericNormaliseInsts isWanted fun insts
+ = do { (insts', binds) <- mapAndUnzipM (normaliseOneInst isWanted fun) insts
+ ; return (insts', unionManyBags binds)
+ }
+ where
+ normaliseOneInst isWanted fun
+ dict@(Dict {tci_name = name,
+ tci_pred = pred,
+ tci_loc = loc})
+ = do { traceTc (text "genericNormaliseInst 1")
+ ; (coi, pred') <- fun pred
+ ; traceTc (text "genericNormaliseInst 2")
+
+ ; case coi of
+ IdCo -> return (dict, emptyBag)
+ -- don't use pred' in this case; otherwise, we get
+ -- more unfolded closed type synonyms in error messages
+ ACo co ->
+ do { -- an inst for the new pred
+ ; dict' <- newDictBndr loc pred'
+ -- relate the old inst to the new one
+ -- target_dict = source_dict `cast` st_co
+ ; let (target_dict, source_dict, st_co)
+ | isWanted = (dict, dict', mkSymCoercion co)
+ | otherwise = (dict', dict, co)
+ -- if isWanted
+ -- co :: dict ~ dict'
+ -- hence dict = dict' `cast` sym co
+ -- else
+ -- co :: dict ~ dict'
+ -- hence dict' = dict `cast` co
+ expr = HsVar $ instToId source_dict
+ cast_expr = HsWrap (WpCo st_co) expr
+ rhs = L (instLocSpan loc) cast_expr
+ binds = mkBind target_dict rhs
+ -- return the new inst
+ ; return (dict', binds)
+ }
+ }
+
+ -- TOMDO: treat other insts appropriately
+ normaliseOneInst isWanted fun inst
+ = do { inst' <- zonkInst inst
+ ; return (inst', emptyBag)
+ }
+
+addBind binds inst rhs = binds `unionBags` mkBind inst rhs
+
+mkBind inst rhs = unitBag (L (instSpan inst)
+ (VarBind (instToId inst) rhs))
+\end{code}
isDoubleTy, isFloatTy, isIntTy, isStringTy,
isIntegerTy, isBoolTy, isUnitTy, isCharTy,
isTauTy, isTauTyCon, tcIsTyVarTy, tcIsForAllTy,
+ isOpenSynTyConApp,
---------------------------------
-- Misc type manipulators
import Data.IORef
\end{code}
-
%************************************************************************
%* *
\subsection{Types}
-- b2 is another (currently empty) box.
data MetaDetails
- = Flexi -- Flexi type variables unify to become
- -- Indirects.
+ = Flexi -- Flexi type variables unify to become
+ -- Indirects.
- | Indirect TcType -- INVARIANT:
- -- For a BoxTv, this type must be non-boxy
- -- For a TauTv, this type must be a tau-type
+ | Indirect TcType -- INVARIANT:
+ -- For a BoxTv, this type must be non-boxy
+ -- For a TauTv, this type must be a tau-type
-- Generally speaking, SkolemInfo should not contain location info
-- that is contained in the Name of the tyvar with this SkolemInfo
-- They may be jiggled by tidying
kind_var_occ = mkOccName tvName "k"
\end{code}
-\end{code}
%************************************************************************
%* *
pprSkolInfo RuntimeUnkSkol = panic "RuntimeUnkSkol"
instance Outputable MetaDetails where
- ppr Flexi = ptext SLIT("Flexi")
+ ppr Flexi = ptext SLIT("Flexi")
ppr (Indirect ty) = ptext SLIT("Indirect") <+> ppr ty
\end{code}
isBoxyTyVar, isMetaTyVar :: TcTyVar -> Bool
isTyConableTyVar tv
- -- True of a meta-type variable tha can be filled in
+ -- True of a meta-type variable that can be filled in
-- with a type constructor application; in particular,
-- not a SigTv
= ASSERT( isTcTyVar tv)
metaTvRef :: TyVar -> IORef MetaDetails
metaTvRef tv
- = ASSERT( isTcTyVar tv )
+ = ASSERT2( isTcTyVar tv, ppr tv )
case tcTyVarDetails tv of
MetaTv _ ref -> ref
other -> pprPanic "metaTvRef" (ppr tv)
isFlexi, isIndirect :: MetaDetails -> Bool
-isFlexi Flexi = True
-isFlexi other = False
+isFlexi Flexi = True
+isFlexi other = False
isIndirect (Indirect _) = True
isIndirect other = False
-- A type is rigid if it has no meta type variables in it
isRigidTy ty = all isImmutableTyVar (varSetElems (tcTyVarsOfType ty))
-isRefineableTy :: TcType -> Bool
+isRefineableTy :: TcType -> (Bool,Bool)
-- A type should have type refinements applied to it if it has
-- free type variables, and they are all rigid
-isRefineableTy ty = not (null tc_tvs) && all isImmutableTyVar tc_tvs
+isRefineableTy ty = (null tc_tvs, all isImmutableTyVar tc_tvs)
where
tc_tvs = varSetElems (tcTyVarsOfType ty)
Nothing -> False
\end{code}
+\begin{code}
+-- NB: Currently used in places where we have already expanded type synonyms;
+-- hence no 'coreView'. This could, however, be changed without breaking
+-- any code.
+isOpenSynTyConApp :: TcTauType -> Bool
+isOpenSynTyConApp (TyConApp tc _) = isOpenSynTyCon tc
+isOpenSynTyConApp _other = False
+\end{code}
+
%************************************************************************
%* *
import TcMType
import TcSimplify
import TcEnv
+import TcTyFuns
import TcIface
import TcRnMonad -- TcType, amongst others
import TcType
import Type
+import Coercion
import TysPrim
import Inst
import TyCon
import Var
import VarSet
import VarEnv
-import Module
import Name
import ErrUtils
import Maybes
import BasicTypes
import Util
import Outputable
+import Unique
\end{code}
%************************************************************************
tcInfer tc_infer
= do { box <- newBoxyTyVar openTypeKind
; res <- tc_infer (mkTyVarTy box)
- ; res_ty <- readFilledBox box -- Guaranteed filled-in by now
+ ; res_ty <- {- pprTrace "tcInfer" (ppr (mkTyVarTy box)) $ -} readFilledBox box -- Guaranteed filled-in by now
; return (res, res_ty) }
\end{code}
--
-- If (subFunTys n_args res_ty thing_inside) = (co_fn, res)
-- and the inner call to thing_inside passes args: [a1,...,an], b
--- then co_fn :: (a1 -> ... -> an -> b) -> res_ty
+-- then co_fn :: (a1 -> ... -> an -> b) ~ res_ty
--
-- Note that it takes a BoxyRho type, and guarantees to return a BoxyRhoType
-- error message on failure
loop n args_so_far res_ty@(AppTy _ _)
= do { [arg_ty',res_ty'] <- newBoxyTyVarTys [argTypeKind, openTypeKind]
- ; (_, mb_unit) <- tryTcErrs $ boxyUnify res_ty (FunTy arg_ty' res_ty')
- ; if isNothing mb_unit then bale_out args_so_far
- else loop n args_so_far (FunTy arg_ty' res_ty') }
+ ; (_, mb_coi) <- tryTcErrs $ boxyUnify res_ty (FunTy arg_ty' res_ty')
+ ; if isNothing mb_coi then bale_out args_so_far
+ else do { case expectJust "subFunTys" mb_coi of
+ IdCo -> return ()
+ ACo co -> traceTc (text "you're dropping a coercion: " <+> ppr co)
+ ; loop n args_so_far (FunTy arg_ty' res_ty')
+ }
+ }
loop n args_so_far (TyVarTy tv)
| isTyConableTyVar tv
= do { cts <- readMetaTyVar tv
; case cts of
Indirect ty -> loop n_req args_so_far ty
- Flexi -> do { arg_tys <- withMetaTvs tv arg_kinds mk_res_ty
+ Flexi -> do { arg_tys <- withMetaTvs tv arg_kinds mk_res_ty
; return (arg_tys ++ args_so_far) }
}
where
= do { cts <- readMetaTyVar tv
; case cts of
Indirect ty -> loop ty
- Flexi -> do { [fun_ty,arg_ty] <- withMetaTvs tv kinds mk_res_ty
+ Flexi -> do { [fun_ty,arg_ty] <- withMetaTvs tv kinds mk_res_ty
; return (fun_ty, arg_ty) } }
where
mk_res_ty [fun_ty', arg_ty'] = mkAppTy fun_ty' arg_ty'
withBox kind thing_inside
= do { box_tv <- newMetaTyVar BoxTv kind
; res <- thing_inside (mkTyVarTy box_tv)
- ; ty <- readFilledBox box_tv
+ ; ty <- {- pprTrace "with_box" (ppr (mkTyVarTy box_tv)) $ -} readFilledBox box_tv
; return (res, ty) }
\end{code}
(boxy_tvs `extendVarSetList` tvs2) tau2 subst
go (TyConApp tc1 tys1) (TyConApp tc2 tys2)
- | tc1 == tc2 = go_s tys1 tys2
+ | tc1 == tc2
+ , not $ isOpenSynTyCon tc1
+ = go_s tys1 tys2
go (FunTy arg1 res1) (FunTy arg2 res2)
= go_s [arg1,res1] [arg2,res2]
-- Look inside type synonyms, but only if the naive version fails
go ty1 ty2 | Just ty1' <- tcView ty1 = go ty1' ty2
- | Just ty2' <- tcView ty2 = go ty1 ty2'
+ | Just ty2' <- tcView ty1 = go ty1 ty2'
-- For now, we don't look inside ForAlls, PredTys
go ty1 ty2 = orig_ty1 -- Default
a place expecting a value of type expected_ty.
It returns a coercion function
- co_fn :: offered_ty -> expected_ty
+ co_fn :: offered_ty ~ expected_ty
which takes an HsExpr of type offered_ty into one of type
expected_ty.
-- Just defer to boxy matching
-- This rule takes precedence over SKOL!
tc_sub1 sub_ctxt act_sty (TyVarTy tv) exp_ib exp_sty exp_ty
- = do { addSubCtxt sub_ctxt act_sty exp_sty $
- uVar True False tv exp_ib exp_sty exp_ty
- ; return idHsWrapper }
+ = do { traceTc (text "tc_sub1 - case 1")
+ ; coi <- addSubCtxt sub_ctxt act_sty exp_sty $
+ uVar True False tv exp_ib exp_sty exp_ty
+ ; traceTc (case coi of
+ IdCo -> text "tc_sub1 (Rule SBOXY) IdCo"
+ ACo co -> text "tc_sub1 (Rule SBOXY) ACo" <+> ppr co)
+ ; return $ case coi of
+ IdCo -> idHsWrapper
+ ACo co -> WpCo co
+ }
-----------------------------------
-- Skolemisation case (rule SKOL)
tc_sub1 sub_ctxt act_sty act_ty exp_ib exp_sty exp_ty
| isSigmaTy exp_ty
- = if exp_ib then -- SKOL does not apply if exp_ty is inside a box
+ = do { traceTc (text "tc_sub1 - case 2") ;
+ if exp_ib then -- SKOL does not apply if exp_ty is inside a box
defer_to_boxy_matching sub_ctxt act_sty act_ty exp_ib exp_sty exp_ty
else do
{ (gen_fn, co_fn) <- tcGen exp_ty act_tvs $ \ _ body_exp_ty ->
tc_sub sub_ctxt act_sty act_ty False body_exp_ty body_exp_ty
; return (gen_fn <.> co_fn) }
+ }
where
act_tvs = tyVarsOfType act_ty
-- It's really important to check for escape wrt
-- Pre-subsumpion finds a|->Int, and that works fine, whereas
-- just running full subsumption would fail.
| isSigmaTy actual_ty
- = do { -- Perform pre-subsumption, and instantiate
+ = do { traceTc (text "tc_sub1 - case 3")
+ ; -- Perform pre-subsumption, and instantiate
-- the type with info from the pre-subsumption;
-- boxy tyvars if pre-subsumption gives no info
let (tyvars, theta, tau) = tcSplitSigmaTy actual_ty
-----------------------------------
-- Function case (rule F1)
tc_sub1 sub_ctxt act_sty (FunTy act_arg act_res) exp_ib exp_sty (FunTy exp_arg exp_res)
- = addSubCtxt sub_ctxt act_sty exp_sty $
- tc_sub_funs act_arg act_res exp_ib exp_arg exp_res
+ = do { traceTc (text "tc_sub1 - case 4")
+ ; addSubCtxt sub_ctxt act_sty exp_sty $
+ tc_sub_funs act_arg act_res exp_ib exp_arg exp_res
+ }
-- Function case (rule F2)
tc_sub1 sub_ctxt act_sty act_ty@(FunTy act_arg act_res) _ exp_sty (TyVarTy exp_tv)
| isBoxyTyVar exp_tv
= addSubCtxt sub_ctxt act_sty exp_sty $
- do { cts <- readMetaTyVar exp_tv
+ do { traceTc (text "tc_sub1 - case 5")
+ ; cts <- readMetaTyVar exp_tv
; case cts of
Indirect ty -> tc_sub SubDone act_sty act_ty True exp_sty ty
- Flexi -> do { [arg_ty,res_ty] <- withMetaTvs exp_tv fun_kinds mk_res_ty
+ Flexi -> do { [arg_ty,res_ty] <- withMetaTvs exp_tv fun_kinds mk_res_ty
; tc_sub_funs act_arg act_res True arg_ty res_ty } }
where
mk_res_ty [arg_ty', res_ty'] = mkFunTy arg_ty' res_ty'
fun_kinds = [argTypeKind, openTypeKind]
-- Everything else: defer to boxy matching
+tc_sub1 sub_ctxt act_sty actual_ty exp_ib exp_sty expected_ty@(TyVarTy exp_tv)
+ = do { traceTc (text "tc_sub1 - case 6a" <+> ppr [isBoxyTyVar exp_tv, isMetaTyVar exp_tv, isSkolemTyVar exp_tv, isExistentialTyVar exp_tv,isSigTyVar exp_tv] )
+ ; defer_to_boxy_matching sub_ctxt act_sty actual_ty exp_ib exp_sty expected_ty
+ }
+
tc_sub1 sub_ctxt act_sty actual_ty exp_ib exp_sty expected_ty
- = defer_to_boxy_matching sub_ctxt act_sty actual_ty exp_ib exp_sty expected_ty
+ = do { traceTc (text "tc_sub1 - case 6")
+ ; defer_to_boxy_matching sub_ctxt act_sty actual_ty exp_ib exp_sty expected_ty
+ }
-----------------------------------
defer_to_boxy_matching sub_ctxt act_sty actual_ty exp_ib exp_sty expected_ty
- = do { addSubCtxt sub_ctxt act_sty exp_sty $
+ = do { coi <- addSubCtxt sub_ctxt act_sty exp_sty $
u_tys outer False act_sty actual_ty exp_ib exp_sty expected_ty
- ; return idHsWrapper }
+ ; return $ case coi of
+ IdCo -> idHsWrapper
+ ACo co -> WpCo co
+ }
where
outer = case sub_ctxt of -- Ugh
SubDone -> False
-----------------------------------
tc_sub_funs act_arg act_res exp_ib exp_arg exp_res
- = do { uTys False act_arg exp_ib exp_arg
+ = do { arg_coi <- uTys False act_arg exp_ib exp_arg
; co_fn_res <- tc_sub SubDone act_res act_res exp_ib exp_res exp_res
- ; wrapFunResCoercion [exp_arg] co_fn_res }
+ ; wrapper1 <- wrapFunResCoercion [exp_arg] co_fn_res
+ ; let wrapper2 = case arg_coi of
+ IdCo -> idHsWrapper
+ ACo co -> WpCo $ FunTy co act_res
+ ; return (wrapper1 <.> wrapper2)
+ }
-----------------------------------
wrapFunResCoercion
-> HsWrapper -- HsExpr a -> HsExpr b
-> TcM HsWrapper -- HsExpr (arg_tys -> a) -> HsExpr (arg_tys -> b)
wrapFunResCoercion arg_tys co_fn_res
- | isIdHsWrapper co_fn_res = return idHsWrapper
- | null arg_tys = return co_fn_res
+ | isIdHsWrapper co_fn_res
+ = return idHsWrapper
+ | null arg_tys
+ = return co_fn_res
| otherwise
= do { arg_ids <- newSysLocalIds FSLIT("sub") arg_tys
; return (mkWpLams arg_ids <.> co_fn_res <.> mkWpApps arg_ids) }
tcGen expected_ty extra_tvs thing_inside -- We expect expected_ty to be a forall-type
-- If not, the call is a no-op
- = do { -- We want the GenSkol info in the skolemised type variables to
+ = do { traceTc (text "tcGen")
+ -- We want the GenSkol info in the skolemised type variables to
-- mention the *instantiated* tyvar names, so that we get a
-- good error message "Rigid variable 'a' is bound by (forall a. a->a)"
-- Hence the tiresome but innocuous fixM
- ((tvs', theta', rho'), skol_info) <- fixM (\ ~(_, skol_info) ->
+ ; ((tvs', theta', rho'), skol_info) <- fixM (\ ~(_, skol_info) ->
do { (forall_tvs, theta, rho_ty) <- tcInstSkolType skol_info expected_ty
-- Get loation from monad, not from expected_ty
; let skol_info = GenSkol forall_tvs (mkPhiTy theta rho_ty)
; returnM (co_fn, result) }
where
free_tvs = tyVarsOfType expected_ty `unionVarSet` extra_tvs
-\end{code}
+\end{code}
non-exported generic functions.
\begin{code}
-boxyUnify :: BoxyType -> BoxyType -> TcM ()
+boxyUnify :: BoxyType -> BoxyType -> TcM CoercionI
-- Acutal and expected, respectively
boxyUnify ty1 ty2
= addErrCtxtM (unifyCtxt ty1 ty2) $
uTysOuter False ty1 False ty2
---------------
-boxyUnifyList :: [BoxyType] -> [BoxyType] -> TcM ()
+boxyUnifyList :: [BoxyType] -> [BoxyType] -> TcM [CoercionI]
-- Arguments should have equal length
-- Acutal and expected types
boxyUnifyList tys1 tys2 = uList boxyUnify tys1 tys2
---------------
-unifyType :: TcTauType -> TcTauType -> TcM ()
+unifyType :: TcTauType -> TcTauType -> TcM CoercionI
-- No boxes expected inside these types
-- Acutal and expected types
unifyType ty1 ty2 -- ty1 expected, ty2 inferred
uTysOuter True ty1 True ty2
---------------
-unifyPred :: PredType -> PredType -> TcM ()
+unifyPred :: PredType -> PredType -> TcM CoercionI
-- Acutal and expected types
unifyPred p1 p2 = addErrCtxtM (unifyCtxt (mkPredTy p1) (mkPredTy p2)) $
- uPred True True p1 True p2
+ uPred True True p1 True p2
-unifyTheta :: TcThetaType -> TcThetaType -> TcM ()
+unifyTheta :: TcThetaType -> TcThetaType -> TcM [CoercionI]
-- Acutal and expected types
unifyTheta theta1 theta2
= do { checkTc (equalLength theta1 theta2)
(vcat [ptext SLIT("Contexts differ in length"),
nest 2 $ parens $ ptext SLIT("Use -fglasgow-exts to allow this")])
- ; uList unifyPred theta1 theta2 }
+ ; uList unifyPred theta1 theta2
+ }
---------------
-uList :: (a -> a -> TcM ())
- -> [a] -> [a] -> TcM ()
+uList :: (a -> a -> TcM b)
+ -> [a] -> [a] -> TcM [b]
-- Unify corresponding elements of two lists of types, which
--- should be f equal length. We charge down the list explicitly so that
+-- should be of equal length. We charge down the list explicitly so that
-- we can complain if their lengths differ.
-uList unify [] [] = return ()
-uList unify (ty1:tys1) (ty2:tys2) = do { unify ty1 ty2; uList unify tys1 tys2 }
+uList unify [] [] = return []
+uList unify (ty1:tys1) (ty2:tys2) = do { x <- unify ty1 ty2;
+ ; xs <- uList unify tys1 tys2
+ ; return (x:xs)
+ }
uList unify ty1s ty2s = panic "Unify.uList: mismatched type lists!"
\end{code}
%* *
%************************************************************************
-@uTys@ is the heart of the unifier. Each arg happens twice, because
-we want to report errors in terms of synomyms if poss. The first of
+@uTys@ is the heart of the unifier. Each arg occurs twice, because
+we want to report errors in terms of synomyms if possible. The first of
the pair is used in error messages only; it is always the same as the
second, except that if the first is a synonym then the second may be a
de-synonym'd version. This way we get better error messages.
We call the first one \tr{ps_ty1}, \tr{ps_ty2} for ``possible synomym''.
\begin{code}
+type SwapFlag = Bool
+ -- False <=> the two args are (actual, expected) respectively
+ -- True <=> the two args are (expected, actual) respectively
+
type InBox = Bool -- True <=> we are inside a box
-- False <=> we are outside a box
-- The importance of this is that if we get "filled-box meets
-- pop the context to remove the "Expected/Acutal" context
uTysOuter, uTys
- :: InBox -> TcType -- ty1 is the *expected* type
- -> InBox -> TcType -- ty2 is the *actual* type
- -> TcM ()
-uTysOuter nb1 ty1 nb2 ty2 = do { traceTc (text "uTysOuter" <+> ppr ty1 <+> ppr ty2)
- ; u_tys True nb1 ty1 ty1 nb2 ty2 ty2 }
-uTys nb1 ty1 nb2 ty2 = do { traceTc (text "uTys" <+> ppr ty1 <+> ppr ty2)
- ; u_tys False nb1 ty1 ty1 nb2 ty2 ty2 }
+ :: InBox -> TcType -- ty1 is the *actual* type
+ -> InBox -> TcType -- ty2 is the *expected* type
+ -> TcM CoercionI
+uTysOuter nb1 ty1 nb2 ty2
+ = do { traceTc (text "uTysOuter" <+> ppr ty1 <+> ppr ty2)
+ ; u_tys True nb1 ty1 ty1 nb2 ty2 ty2 }
+uTys nb1 ty1 nb2 ty2
+ = do { traceTc (text "uTys" <+> ppr ty1 <+> ppr ty2)
+ ; u_tys False nb1 ty1 ty1 nb2 ty2 ty2 }
--------------
-uTys_s :: InBox -> [TcType] -- ty1 is the *actual* types
- -> InBox -> [TcType] -- ty2 is the *expected* types
- -> TcM ()
-uTys_s nb1 [] nb2 [] = returnM ()
-uTys_s nb1 (ty1:tys1) nb2 (ty2:tys2) = do { uTys nb1 ty1 nb2 ty2
- ; uTys_s nb1 tys1 nb2 tys2 }
+uTys_s :: InBox -> [TcType] -- tys1 are the *actual* types
+ -> InBox -> [TcType] -- tys2 are the *expected* types
+ -> TcM [CoercionI]
+uTys_s nb1 [] nb2 [] = returnM []
+uTys_s nb1 (ty1:tys1) nb2 (ty2:tys2) = do { coi <- uTys nb1 ty1 nb2 ty2
+ ; cois <- uTys_s nb1 tys1 nb2 tys2
+ ; return (coi:cois)
+ }
uTys_s nb1 ty1s nb2 ty2s = panic "Unify.uTys_s: mismatched type lists!"
--------------
u_tys :: Outer
-> InBox -> TcType -> TcType -- ty1 is the *actual* type
-> InBox -> TcType -> TcType -- ty2 is the *expected* type
- -> TcM ()
+ -> TcM CoercionI
u_tys outer nb1 orig_ty1 ty1 nb2 orig_ty2 ty2
- = go outer ty1 ty2
+ = do { traceTc (text "u_tys " <+> ppr ty1 <+> text " " <+> ppr ty2)
+ ; coi <- go outer ty1 ty2
+ ; traceTc (case coi of
+ ACo co -> text "u_tys yields coercion: " <+> ppr co
+ IdCo -> text "u_tys yields no coercion")
+ ; return coi
+ }
where
- -- Always expand synonyms (see notes at end)
+ go :: Outer -> TcType -> TcType -> TcM CoercionI
+ go outer ty1 ty2 =
+ do { traceTc (text "go " <+> ppr orig_ty1 <+> text "/" <+> ppr ty1
+ <+> ppr orig_ty2 <+> text "/" <+> ppr ty2)
+ ; go1 outer ty1 ty2
+ }
+
+ go1 :: Outer -> TcType -> TcType -> TcM CoercionI
+ -- Always expand synonyms: see Note [Unification and synonyms]
-- (this also throws away FTVs)
- go outer ty1 ty2
+ go1 outer ty1 ty2
| Just ty1' <- tcView ty1 = go False ty1' ty2
| Just ty2' <- tcView ty2 = go False ty1 ty2'
-- Variables; go for uVar
- go outer (TyVarTy tyvar1) ty2 = uVar outer False tyvar1 nb2 orig_ty2 ty2
- go outer ty1 (TyVarTy tyvar2) = uVar outer True tyvar2 nb1 orig_ty1 ty1
+ go1 outer (TyVarTy tyvar1) ty2 = uVar outer False tyvar1 nb2 orig_ty2 ty2
+ go1 outer ty1 (TyVarTy tyvar2) = uVar outer True tyvar2 nb1 orig_ty1 ty1
-- "True" means args swapped
-- The case for sigma-types must *follow* the variable cases
-- because a boxy variable can be filed with a polytype;
-- but must precede FunTy, because ((?x::Int) => ty) look
-- like a FunTy; there isn't necy a forall at the top
- go _ ty1 ty2
+ go1 _ ty1 ty2
| isSigmaTy ty1 || isSigmaTy ty2
- = do { checkM (equalLength tvs1 tvs2)
+ = do { traceTc (text "We have sigma types: equalLength" <+> ppr tvs1 <+> ppr tvs2)
+ ; checkM (equalLength tvs1 tvs2)
(unifyMisMatch outer False orig_ty1 orig_ty2)
-
+ ; traceTc (text "We're past the first length test")
; tvs <- tcInstSkolTyVars UnkSkol tvs1 -- Not a helpful SkolemInfo
-- Get location from monad, not from tvs1
; let tys = mkTyVarTys tvs
{ checkM (equalLength theta1 theta2)
(unifyMisMatch outer False orig_ty1 orig_ty2)
- ; uPreds False nb1 theta1 nb2 theta2
- ; uTys nb1 tau1 nb2 tau2
+ ; cois <- uPreds False nb1 theta1 nb2 theta2 -- TOMDO: do something with these pred_cois
+ ; traceTc (text "TOMDO!")
+ ; coi <- uTys nb1 tau1 nb2 tau2
-- Check for escape; e.g. (forall a. a->b) ~ (forall a. a->a)
; free_tvs <- zonkTcTyVarsAndFV (varSetElems (tyVarsOfType ty1 `unionVarSet` tyVarsOfType ty2))
-- This check comes last, because the error message is
-- extremely unhelpful.
; ifM (nb1 && nb2) (notMonoType ty1)
+ ; return coi
}}
where
(tvs1, body1) = tcSplitForAllTys ty1
(tvs2, body2) = tcSplitForAllTys ty2
-- Predicates
- go outer (PredTy p1) (PredTy p2) = uPred False nb1 p1 nb2 p2
+ go1 outer (PredTy p1) (PredTy p2)
+ = uPred False nb1 p1 nb2 p2
-- Type constructors must match
- go _ (TyConApp con1 tys1) (TyConApp con2 tys2)
- | con1 == con2 = uTys_s nb1 tys1 nb2 tys2
+ go1 _ (TyConApp con1 tys1) (TyConApp con2 tys2)
+ | con1 == con2 && not (isOpenSynTyCon con1)
+ = do { cois <- uTys_s nb1 tys1 nb2 tys2
+ ; return $ mkTyConAppCoI con1 tys1 cois
+ }
-- See Note [TyCon app]
+ | con1 == con2 && identicalOpenSynTyConApp
+ = do { cois <- uTys_s nb1 tys1' nb2 tys2'
+ ; return $ mkTyConAppCoI con1 tys1 (replicate n IdCo ++ cois)
+ }
+ where
+ n = tyConArity con1
+ (idxTys1, tys1') = splitAt n tys1
+ (idxTys2, tys2') = splitAt n tys2
+ identicalOpenSynTyConApp = idxTys1 `tcEqTypes` idxTys2
+ -- See Note [OpenSynTyCon app]
-- Functions; just check the two parts
- go _ (FunTy fun1 arg1) (FunTy fun2 arg2)
- = do { uTys nb1 fun1 nb2 fun2
- ; uTys nb1 arg1 nb2 arg2 }
+ go1 _ (FunTy fun1 arg1) (FunTy fun2 arg2)
+ = do { coi_l <- uTys nb1 fun1 nb2 fun2
+ ; coi_r <- uTys nb1 arg1 nb2 arg2
+ ; return $ mkFunTyCoI fun1 coi_l arg1 coi_r
+ }
-- Applications need a bit of care!
-- They can match FunTy and TyConApp, so use splitAppTy_maybe
-- NB: we've already dealt with type variables and Notes,
-- so if one type is an App the other one jolly well better be too
- go outer (AppTy s1 t1) ty2
+ go1 outer (AppTy s1 t1) ty2
| Just (s2,t2) <- tcSplitAppTy_maybe ty2
- = do { uTys nb1 s1 nb2 s2; uTys nb1 t1 nb2 t2 }
+ = do { coi_s <- uTys nb1 s1 nb2 s2; coi_t <- uTys nb1 t1 nb2 t2
+ ; return $ mkAppTyCoI s1 coi_s t1 coi_t }
-- Now the same, but the other way round
-- Don't swap the types, because the error messages get worse
- go outer ty1 (AppTy s2 t2)
+ go1 outer ty1 (AppTy s2 t2)
| Just (s1,t1) <- tcSplitAppTy_maybe ty1
- = do { uTys nb1 s1 nb2 s2; uTys nb1 t1 nb2 t2 }
+ = do { coi_s <- uTys nb1 s1 nb2 s2; coi_t <- uTys nb1 t1 nb2 t2
+ ; return $ mkAppTyCoI s1 coi_s t1 coi_t }
+
+ -- One or both outermost constructors are type family applications.
+ -- If we can normalise them away, proceed as usual; otherwise, we
+ -- need to defer unification by generating a wanted equality constraint.
+ go1 outer ty1 ty2
+ | ty1_is_fun || ty2_is_fun
+ = do { (coi1, ty1') <- if ty1_is_fun then tcNormalizeFamInst ty1
+ else return (IdCo, ty1)
+ ; (coi2, ty2') <- if ty2_is_fun then tcNormalizeFamInst ty2
+ else return (IdCo, ty2)
+ ; coi <- if isOpenSynTyConApp ty1' || isOpenSynTyConApp ty2'
+ then do { -- One type family app can't be reduced yet
+ -- => defer
+ ; ty1'' <- zonkTcType ty1'
+ ; ty2'' <- zonkTcType ty2'
+ ; if tcEqType ty1'' ty2''
+ then return IdCo
+ else -- see [Deferred Unification]
+ defer_unification outer False orig_ty1 orig_ty2
+ }
+ else -- unification can proceed
+ go outer ty1' ty2'
+ ; return $ coi1 `mkTransCoI` coi `mkTransCoI` (mkSymCoI coi2)
+ }
+ where
+ ty1_is_fun = isOpenSynTyConApp ty1
+ ty2_is_fun = isOpenSynTyConApp ty2
+ -- Anything else fails
+ go1 outer _ _ = unifyMisMatch outer False orig_ty1 orig_ty2
- -- Anything else fails
- go outer _ _ = unifyMisMatch outer False orig_ty1 orig_ty2
----------
uPred outer nb1 (IParam n1 t1) nb2 (IParam n2 t2)
- | n1 == n2 = uTys nb1 t1 nb2 t2
+ | n1 == n2 =
+ do { coi <- uTys nb1 t1 nb2 t2
+ ; return $ mkIParamPredCoI n1 coi
+ }
uPred outer nb1 (ClassP c1 tys1) nb2 (ClassP c2 tys2)
- | c1 == c2 = uTys_s nb1 tys1 nb2 tys2 -- Guaranteed equal lengths because the kinds check
+ | c1 == c2 =
+ do { cois <- uTys_s nb1 tys1 nb2 tys2 -- Guaranteed equal lengths because the kinds check
+ ; return $ mkClassPPredCoI c1 tys1 cois
+ }
uPred outer _ p1 _ p2 = unifyMisMatch outer False (mkPredTy p1) (mkPredTy p2)
-uPreds outer nb1 [] nb2 [] = return ()
-uPreds outer nb1 (p1:ps1) nb2 (p2:ps2) = uPred outer nb1 p1 nb2 p2 >> uPreds outer nb1 ps1 nb2 ps2
+uPreds outer nb1 [] nb2 [] = return []
+uPreds outer nb1 (p1:ps1) nb2 (p2:ps2) =
+ do { coi <- uPred outer nb1 p1 nb2 p2
+ ; cois <- uPreds outer nb1 ps1 nb2 ps2
+ ; return (coi:cois)
+ }
uPreds outer nb1 ps1 nb2 ps2 = panic "uPreds"
\end{code}
-Note [Tycon app]
+Note [TyCon app]
~~~~~~~~~~~~~~~~
When we find two TyConApps, the argument lists are guaranteed equal
length. Reason: intially the kinds of the two types to be unified is
which we do, that ensures that f1,f2 have the same kind; and that
means a1,a2 have the same kind. And now the argument repeats.
+Note [OpenSynTyCon app]
+~~~~~~~~~~~~~~~~~~~~~~~
+Given
+
+ type family T a :: * -> *
+
+the two types (T () a) and (T () Int) must unify, even if there are
+no type instances for T at all. Should we just turn them into an
+equality (T () a ~ T () Int)? I don't think so. We currently try to
+eagerly unify everything we can before generating equalities; otherwise,
+we could turn the unification of [Int] with [a] into an equality, too.
-Notes on synonyms
-~~~~~~~~~~~~~~~~~
+Note [Unification and synonyms]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
If you are tempted to make a short cut on synonyms, as in this
pseudocode...
\begin{code}
uVar :: Outer
- -> Bool -- False => tyvar is the "expected"
- -- True => ty is the "expected" thing
+ -> SwapFlag -- False => tyvar is the "actual" (ty is "expected")
+ -- True => ty is the "actual" (tyvar is "expected")
-> TcTyVar
-> InBox -- True <=> definitely no boxes in t2
-> TcTauType -> TcTauType -- printing and real versions
- -> TcM ()
+ -> TcM CoercionI
uVar outer swapped tv1 nb2 ps_ty2 ty2
= do { let expansion | showSDoc (ppr ty2) == showSDoc (ppr ps_ty2) = empty
----------------
uUnfilledVar :: Outer
- -> Bool -- Args are swapped
+ -> SwapFlag
-> TcTyVar -> TcTyVarDetails -- Tyvar 1
-> TcTauType -> TcTauType -- Type 2
- -> TcM ()
+ -> TcM CoercionI
-- Invariant: tyvar 1 is not unified with anything
uUnfilledVar outer swapped tv1 details1 ps_ty2 ty2
MetaTv BoxTv ref1 -- A boxy type variable meets itself;
-- this is box-meets-box, so fill in with a tau-type
-> do { tau_tv <- tcInstTyVar tv1
- ; updateMeta tv1 ref1 (mkTyVarTy tau_tv) }
- other -> returnM () -- No-op
+ ; updateMeta tv1 ref1 (mkTyVarTy tau_tv)
+ ; return IdCo
+ }
+ other -> returnM IdCo -- No-op
- -- Distinct type variables
- | otherwise
+ | otherwise -- Distinct type variables
= do { lookup2 <- lookupTcTyVar tv2
; case lookup2 of
- IndirectTv ty2' -> uUnfilledVar outer swapped tv1 details1 ty2' ty2'
+ IndirectTv ty2' -> uUnfilledVar outer swapped tv1 details1 ty2' ty2'
DoneTv details2 -> uUnfilledVars outer swapped tv1 details1 tv2 details2
}
-uUnfilledVar outer swapped tv1 details1 ps_ty2 non_var_ty2 -- ty2 is not a type variable
- = case details1 of
- MetaTv (SigTv _) ref1 -> mis_match -- Can't update a skolem with a non-type-variable
- MetaTv info ref1 -> uMetaVar swapped tv1 info ref1 ps_ty2 non_var_ty2
- skolem_details -> mis_match
+uUnfilledVar outer swapped tv1 details1 ps_ty2 non_var_ty2
+ = -- ty2 is not a type variable
+ case details1 of
+ MetaTv (SigTv _) _ -> rigid_variable
+ MetaTv info ref1 ->
+ do { uMetaVar swapped tv1 info ref1 ps_ty2 non_var_ty2
+ ; return IdCo
+ }
+ SkolemTv _ -> rigid_variable
where
- mis_match = unifyMisMatch outer swapped (TyVarTy tv1) ps_ty2
+ rigid_variable
+ | isOpenSynTyConApp non_var_ty2
+ = -- 'non_var_ty2's outermost constructor is a type family,
+ -- which we may may be able to normalise
+ do { (coi2, ty2') <- tcNormalizeFamInst non_var_ty2
+ ; case coi2 of
+ IdCo -> -- no progress, but maybe after other instantiations
+ defer_unification outer swapped (TyVarTy tv1) ps_ty2
+ ACo co -> -- progress: so lets try again
+ do { traceTc $
+ ppr co <+> text "::"<+> ppr non_var_ty2 <+> text "~" <+>
+ ppr ty2'
+ ; coi <- uUnfilledVar outer swapped tv1 details1 ps_ty2 ty2'
+ ; let coi2' = (if swapped then id else mkSymCoI) coi2
+ ; return $ coi2' `mkTransCoI` coi
+ }
+ }
+ | SkolemTv RuntimeUnkSkol <- details1
+ -- runtime unknown will never match
+ = unifyMisMatch outer swapped (TyVarTy tv1) ps_ty2
+ | otherwise -- defer as a given equality may still resolve this
+ = defer_unification outer swapped (TyVarTy tv1) ps_ty2
+\end{code}
+
+Note [Deferred Unification]
+~~~~~~~~~~~~~~~~~~~~
+We may encounter a unification ty1 = ty2 that cannot be performed syntactically,
+and yet its consistency is undetermined. Previously, there was no way to still
+make it consistent. So a mismatch error was issued.
+
+Now these unfications are deferred until constraint simplification, where type
+family instances and given equations may (or may not) establish the consistency.
+Deferred unifications are of the form
+ F ... ~ ...
+or x ~ ...
+where F is a type function and x is a type variable.
+E.g.
+ id :: x ~ y => x -> y
+ id e = e
+
+involves the unfication x = y. It is deferred until we bring into account the
+context x ~ y to establish that it holds.
+
+If available, we defer original types (rather than those where closed type
+synonyms have already been expanded via tcCoreView). This is as usual, to
+improve error messages.
+
+\begin{code}
+defer_unification :: Bool -- pop innermost context?
+ -> SwapFlag
+ -> TcType
+ -> TcType
+ -> TcM CoercionI
+defer_unification outer True ty1 ty2
+ = defer_unification outer False ty2 ty1
+defer_unification outer False ty1 ty2
+ = do { ty1' <- zonkTcType ty1
+ ; ty2' <- zonkTcType ty2
+ ; traceTc $ text "deferring:" <+> ppr ty1 <+> text "~" <+> ppr ty2
+ ; cotv <- newMetaTyVar TauTv (mkCoKind ty1' ty2')
+ -- put ty1 ~ ty2 in LIE
+ -- Left means "wanted"
+ ; inst <- (if outer then popErrCtxt else id) $
+ mkEqInst (EqPred ty1' ty2') (Left cotv)
+ ; extendLIE inst
+ ; return $ ACo $ TyVarTy cotv }
----------------
-uMetaVar :: Bool
+uMetaVar :: SwapFlag
-> TcTyVar -> BoxInfo -> IORef MetaDetails
-> TcType -> TcType
-> TcM ()
; case meta_details of
Indirect ty -> WARN( True, ppr tv1 <+> ppr ty )
return () -- This really should *not* happen
- Flexi -> return ()
+ Flexi -> return ()
#endif
; checkUpdateMeta swapped tv1 ref1 final_ty }
----------------
uUnfilledVars :: Outer
- -> Bool -- Args are swapped
+ -> SwapFlag
-> TcTyVar -> TcTyVarDetails -- Tyvar 1
-> TcTyVar -> TcTyVarDetails -- Tyvar 2
- -> TcM ()
+ -> TcM CoercionI
-- Invarant: The type variables are distinct,
-- Neither is filled in yet
-- They might be boxy or not
uUnfilledVars outer swapped tv1 (SkolemTv _) tv2 (SkolemTv _)
- = unifyMisMatch outer swapped (mkTyVarTy tv1) (mkTyVarTy tv2)
+ = -- see [Deferred Unification]
+ defer_unification outer swapped (mkTyVarTy tv1) (mkTyVarTy tv2)
uUnfilledVars outer swapped tv1 (MetaTv info1 ref1) tv2 (SkolemTv _)
- = checkUpdateMeta swapped tv1 ref1 (mkTyVarTy tv2)
+ = checkUpdateMeta swapped tv1 ref1 (mkTyVarTy tv2) >> return IdCo
uUnfilledVars outer swapped tv1 (SkolemTv _) tv2 (MetaTv info2 ref2)
- = checkUpdateMeta (not swapped) tv2 ref2 (mkTyVarTy tv1)
+ = checkUpdateMeta (not swapped) tv2 ref2 (mkTyVarTy tv1) >> return IdCo
-- ToDo: this function seems too long for what it acutally does!
uUnfilledVars outer swapped tv1 (MetaTv info1 ref1) tv2 (MetaTv info2 ref2)
= case (info1, info2) of
- (BoxTv, BoxTv) -> box_meets_box
+ (BoxTv, BoxTv) -> box_meets_box >> return IdCo
-- If a box meets a TauTv, but the fomer has the smaller kind
-- then we must create a fresh TauTv with the smaller kind
- (_, BoxTv) | k1_sub_k2 -> update_tv2
- | otherwise -> box_meets_box
- (BoxTv, _ ) | k2_sub_k1 -> update_tv1
- | otherwise -> box_meets_box
+ (_, BoxTv) | k1_sub_k2 -> update_tv2 >> return IdCo
+ | otherwise -> box_meets_box >> return IdCo
+ (BoxTv, _ ) | k2_sub_k1 -> update_tv1 >> return IdCo
+ | otherwise -> box_meets_box >> return IdCo
-- Avoid SigTvs if poss
- (SigTv _, _ ) | k1_sub_k2 -> update_tv2
- (_, SigTv _) | k2_sub_k1 -> update_tv1
+ (SigTv _, _ ) | k1_sub_k2 -> update_tv2 >> return IdCo
+ (_, SigTv _) | k2_sub_k1 -> update_tv1 >> return IdCo
(_, _) | k1_sub_k2 -> if k2_sub_k1 && nicer_to_update_tv1
- then update_tv1 -- Same kinds
- else update_tv2
- | k2_sub_k1 -> update_tv1
- | otherwise -> kind_err
+ then update_tv1 >> return IdCo -- Same kinds
+ else update_tv2 >> return IdCo
+ | k2_sub_k1 -> update_tv1 >> return IdCo
+ | otherwise -> kind_err >> return IdCo
-- Update the variable with least kind info
-- See notes on type inference in Kind.lhs
-- a user-written type sig
----------------
-checkUpdateMeta :: Bool -> TcTyVar -> IORef MetaDetails -> TcType -> TcM ()
+checkUpdateMeta :: SwapFlag
+ -> TcTyVar -> IORef MetaDetails -> TcType -> TcM ()
-- Update tv1, which is flexi; occurs check is alrady done
-- The 'check' version does a kind check too
-- We do a sub-kind check here: we might unify (a b) with (c d)
ASSERT( isBoxyTyVar tv1 || isTauTy ty2 )
do { ASSERTM2( do { details <- readMetaTyVar tv1; return (isFlexi details) }, ppr tv1 )
; traceTc (text "updateMeta" <+> ppr tv1 <+> text ":=" <+> ppr ty2)
- ; writeMutVar ref1 (Indirect ty2) }
+ ; writeMutVar ref1 (Indirect ty2)
+ }
----------------
checkKinds swapped tv1 ty2
| isMetaTyVar box_tv
= do { cts <- readMetaTyVar box_tv
; case cts of
- Flexi -> return ty
+ Flexi -> return ty
Indirect ty -> return ty }
refineBox other_ty = return other_ty
, MetaTv BoxTv ref <- tcTyVarDetails box_tv
= do { cts <- readMutVar ref
; case cts of
- Flexi -> fillBoxWithTau box_tv ref
+ Flexi -> fillBoxWithTau box_tv ref
Indirect ty -> return ty }
refineBoxToTau other_ty = return other_ty
, MetaTv BoxTv ref <- tcTyVarDetails tv -- NB: non-TcTyVars are possible
= do { cts <- readMutVar ref -- under nested quantifiers
; case cts of
- Flexi -> fillBoxWithTau tv ref
+ Flexi -> fillBoxWithTau tv ref
Indirect ty -> do { non_boxy_ty <- unBox ty
; if isTauTy non_boxy_ty
then return non_boxy_ty
pp2 = ppr ty2' <+> dcolon <+> ppr (typeKind ty2)
unifyMisMatch outer swapped ty1 ty2
- = do { (env, msg) <- if swapped then misMatchMsg ty1 ty2
- else misMatchMsg ty2 ty1
+ = do { (env, msg) <- if swapped then misMatchMsg ty2 ty1
+ else misMatchMsg ty1 ty2
-- This is the whole point of the 'outer' stuff
; if outer then popErrCtxt (failWithTcM (env, msg))
}
-----------------------
-misMatchMsg :: TcType -> TcType -> TcM (TidyEnv, SDoc)
--- Generate the message when two types fail to match,
--- going to some trouble to make it helpful
-misMatchMsg ty1 ty2
- = do { env0 <- tcInitTidyEnv
- ; (env1, pp1, extra1) <- ppr_ty env0 ty1 ty2
- ; (env2, pp2, extra2) <- ppr_ty env1 ty2 ty1
- ; return (env2, sep [sep [ptext SLIT("Couldn't match expected type") <+> pp1,
- nest 7 (ptext SLIT("against inferred type") <+> pp2)],
- nest 2 (extra1 $$ extra2)]) }
-
-ppr_ty :: TidyEnv -> TcType -> TcType -> TcM (TidyEnv, SDoc, SDoc)
-ppr_ty env ty other_ty
- = do { ty' <- zonkTcType ty
- ; let (env1, tidy_ty) = tidyOpenType env ty'
- ; (env2, extra) <- ppr_extra env1 tidy_ty other_ty
- ; return (env2, quotes (ppr tidy_ty), extra) }
-
--- (ppr_extra env ty other_ty) shows extra info about 'ty'
-ppr_extra env (TyVarTy tv) other_ty
- | isSkolemTyVar tv || isSigTyVar tv
- = return (env1, pprSkolTvBinding tv1)
- where
- (env1, tv1) = tidySkolemTyVar env tv
-
-ppr_extra env (TyConApp tc1 _) (TyConApp tc2 _)
- | getOccName tc1 == getOccName tc2
- = -- This case helps with messages that would otherwise say
- -- Could not match 'T' does not match 'M.T'
- -- which is not helpful
- do { this_mod <- getModule
- ; return (env, quotes (ppr tc1) <+> ptext SLIT("is defined") <+> mk_mod this_mod) }
- where
- tc_mod = nameModule (getName tc1)
- tc_pkg = modulePackageId tc_mod
- tc2_pkg = modulePackageId (nameModule (getName tc2))
- mk_mod this_mod
- | tc_mod == this_mod = ptext SLIT("in this module")
-
- | not home_pkg && tc2_pkg /= tc_pkg = pp_pkg
- -- Suppress the module name if (a) it's from another package
- -- (b) other_ty isn't from that same package
-
- | otherwise = ptext SLIT("in module") <+> quotes (ppr tc_mod) <+> pp_pkg
- where
- home_pkg = tc_pkg == modulePackageId this_mod
- pp_pkg | home_pkg = empty
- | otherwise = ptext SLIT("in package") <+> quotes (ppr tc_pkg)
-
-ppr_extra env ty other_ty = return (env, empty) -- Normal case
-
------------------------
notMonoType ty
= do { ty' <- zonkTcType ty
; env0 <- tcInitTidyEnv
= do { mb_k2 <- readKindVar kv2
; case mb_k2 of
Indirect k2 -> uUnboundKVar swapped kv1 k2
- Flexi -> writeKindVar kv1 k2 }
+ Flexi -> writeKindVar kv1 k2 }
uUnboundKVar swapped kv1 non_var_k2
= do { k2' <- zonkTcKind non_var_k2
= readKindVar kvar `thenM` \ maybe_kind ->
case maybe_kind of
Indirect fun_kind -> unifyFunKind fun_kind
- Flexi ->
+ Flexi ->
do { arg_kind <- newKindVar
; res_kind <- newKindVar
; writeKindVar kvar (mkArrowKind arg_kind res_kind)
\begin{code}
module TcUnify where
-import TcType ( TcTauType, BoxySigmaType )
+import TcType ( TcTauType, BoxySigmaType, BoxyType )
import TcRnTypes( TcM )
+import Coercion (CoercionI)
-- This boot file exists only to tie the knot between
-- TcUnify and TcSimplify
-unifyType :: TcTauType -> TcTauType -> TcM ()
+unifyType :: TcTauType -> TcTauType -> TcM CoercionI
+boxyUnify :: BoxyType -> BoxyType -> TcM CoercionI
zapToMonotype :: BoxySigmaType -> TcM TcTauType
\end{code}
isEqPred, mkEqPred, getEqPredTys, isEqPredTy,
-- Coercion transformations
+ mkCoercion,
mkSymCoercion, mkTransCoercion,
- mkLeftCoercion, mkRightCoercion, mkInstCoercion, mkAppCoercion,
+ mkLeftCoercion, mkRightCoercion, mkRightCoercions,
+ mkInstCoercion, mkAppCoercion,
mkForAllCoercion, mkFunCoercion, mkInstsCoercion, mkUnsafeCoercion,
mkNewTypeCoercion, mkFamInstCoercion, mkAppsCoercion,
mkSymCoI, mkTransCoI,
mkTyConAppCoI, mkAppTyCoI, mkFunTyCoI,
mkNoteTyCoI, mkForAllTyCoI,
- fromCoI,
- mkClassPPredCoI, mkIParamPredCoI, mkEqPredCoI,
+ fromCoI, fromACo,
+ mkClassPPredCoI, mkIParamPredCoI, mkEqPredCoI
) where
import Outputable
+type Coercion = Type
+type CoercionKind = Kind -- A CoercionKind is always of form (ty1 :=: ty2)
+
------------------------------
decomposeCo :: Arity -> Coercion -> [Coercion]
-- (decomposeCo 3 c) = [right (left (left c)), right (left c), right c]
splitCoercionKind_maybe (PredTy (EqPred ty1 ty2)) = Just (ty1, ty2)
splitCoercionKind_maybe other = Nothing
-type Coercion = Type
-type CoercionKind = Kind -- A CoercionKind is always of form (ty1 :=: ty2)
-
coercionKind :: Coercion -> (Type, Type)
-- c :: (t1 :=: t2)
-- Then (coercionKind c) = (t1,t2)
| Just (co1, co2) <- splitAppCoercion_maybe co = co2
| otherwise = mkCoercion rightCoercionTyCon [co]
+mkRightCoercions n co
+ = go n co []
+ where
+ go n co acc
+ | n > 0
+ = case splitAppCoercion_maybe co of
+ Just (co1,co2) -> go (n-1) co1 (co2:acc)
+ Nothing -> go (n-1) (mkCoercion leftCoercionTyCon [co]) (mkCoercion rightCoercionTyCon [co]:acc)
+ | otherwise
+ = acc
+
mkInstCoercion co ty
| Just (tv,co') <- splitForAllTy_maybe co
= substTyWith [tv] [ty] co' -- (forall a.co) @ ty --> co[ty/a]
-- CoercionI smart constructors
-- lifted smart constructors of ordinary coercions
-
\begin{code}
-- CoercionI is either
-- (a) proper coercion
isIdentityCoercion IdCo = True
isIdentityCoercion _ = False
+allIdCos :: [CoercionI] -> Bool
+allIdCos = all isIdentityCoercion
+
+zipCoArgs :: [CoercionI] -> [Type] -> [Coercion]
+zipCoArgs cois tys = zipWith fromCoI cois tys
+
+fromCoI :: CoercionI -> Type -> Type
+fromCoI IdCo ty = ty -- Identity coercion represented
+fromCoI (ACo co) ty = co -- by the type itself
+
mkSymCoI :: CoercionI -> CoercionI
mkSymCoI IdCo = IdCo
mkSymCoI (ACo co) = ACo $ mkCoercion symCoercionTyCon [co]
mkTransCoI (ACo co1) (ACo co2) = ACo $ mkTransCoercion co1 co2
mkTyConAppCoI :: TyCon -> [Type] -> [CoercionI] -> CoercionI
-mkTyConAppCoI tyCon tys cois =
- let (anyAcon,co_args) = f tys cois
- in if anyAcon
- then ACo (TyConApp tyCon co_args)
- else IdCo
- where
- f [] [] = (False,[])
- f (x:xs) (y:ys) =
- let (b,cos) = f xs ys
- in case y of
- IdCo -> (b,x:cos)
- ACo co -> (True,co:cos)
+mkTyConAppCoI tyCon tys cois
+ | allIdCos cois = IdCo
+ | otherwise = ACo (TyConApp tyCon (zipCoArgs cois tys))
mkAppTyCoI :: Type -> CoercionI -> Type -> CoercionI -> CoercionI
mkAppTyCoI ty1 IdCo ty2 IdCo = IdCo
mkForAllTyCoI _ IdCo = IdCo
mkForAllTyCoI tv (ACo co) = ACo $ ForAllTy tv co
-fromCoI IdCo ty = ty
-fromCoI (ACo co) ty = co
+fromACo (ACo co) = co
+
mkClassPPredCoI :: Class -> [Type] -> [CoercionI] -> CoercionI
-mkClassPPredCoI cls tys cois =
- let (anyAcon,co_args) = f tys cois
- in if anyAcon
- then ACo $ PredTy $ ClassP cls co_args
- else IdCo
- where
- f [] [] = (False,[])
- f (x:xs) (y:ys) =
- let (b,cos) = f xs ys
- in case y of
- IdCo -> (b,x:cos)
- ACo co -> (True,co:cos)
+-- mkClassPPredCoI cls tys cois = coi
+-- coi : PredTy (cls tys) ~ predTy (cls (tys `cast` cois))
+mkClassPPredCoI cls tys cois
+ | allIdCos cois = IdCo
+ | otherwise = ACo $ PredTy $ ClassP cls (zipCoArgs cois tys)
mkIParamPredCoI :: (IPName Name) -> CoercionI -> CoercionI
+-- Similar invariant to mkclassPPredCoI
mkIParamPredCoI ipn IdCo = IdCo
mkIParamPredCoI ipn (ACo co) = ACo $ PredTy $ IParam ipn co
mkEqPredCoI :: Type -> CoercionI -> Type -> CoercionI -> CoercionI
+-- Similar invariant to mkclassPPredCoI
mkEqPredCoI _ IdCo _ IdCo = IdCo
mkEqPredCoI ty1 IdCo _ (ACo co2) = ACo $ PredTy $ EqPred ty1 co2
mkEqPredCoI ty1 (ACo co1) ty2 coi2 = ACo $ PredTy $ EqPred co1 (fromCoI coi2 ty2)
-
\end{code}
isFunTyCon, isUnLiftedTyCon, isProductTyCon,
isAlgTyCon, isDataTyCon,
isNewTyCon, unwrapNewTyCon_maybe,
- isSynTyCon, isClosedSynTyCon,
+ isSynTyCon, isClosedSynTyCon, isOpenSynTyCon,
isPrimTyCon,
+
isEnumerationTyCon, isGadtSyntaxTyCon, isOpenTyCon,
assocTyConArgPoss_maybe, isTyConAssoc, setTyConArgPoss,
isTupleTyCon, isUnboxedTupleTyCon, isBoxedTupleTyCon, tupleTyConBoxity,
isClosedSynTyCon :: TyCon -> Bool
isClosedSynTyCon tycon = isSynTyCon tycon && not (isOpenTyCon tycon)
+isOpenSynTyCon :: TyCon -> Bool
+isOpenSynTyCon tycon = isSynTyCon tycon && isOpenTyCon tycon
+
isGadtSyntaxTyCon :: TyCon -> Bool
isGadtSyntaxTyCon (AlgTyCon { algTcGadtSyntax = res }) = res
isGadtSyntaxTyCon other = False
isKind :: Kind -> Bool
isKind k = isSuperKind (typeKind k)
-
-
isSubKind :: Kind -> Kind -> Bool
-- (k1 `isSubKind` k2) checks that k1 <: k2
isSubKind (TyConApp kc1 []) (TyConApp kc2 []) = kc1 `isSubKindCon` kc2
my $defaultrepo_base;
my $defaultrepo_lib;
-if ($defaultrepo =~ /:/) {
+if ($defaultrepo =~ /:\/\//) {
# HTTP or SSH
$defaultrepo_base = $defaultrepo;
$defaultrepo_base =~ s#/[^/]+/?$##;
$defaultrepo_lib = "$defaultrepo_base/packages";
}
-elsif ($defaultrepo =~ /^\//) {
+elsif (($defaultrepo =~ /^\//) or # unix
+ ($defaultrepo =~ /^.:/)) { # windows, e.g. c:
# Local filesystem, absolute path (assumes a checked-out tree):
$defaultrepo_base = $defaultrepo;
$defaultrepo_lib = "$defaultrepo/libraries";