diff options
Diffstat (limited to 'compiler')
31 files changed, 2345 insertions, 643 deletions
diff --git a/compiler/NOTES b/compiler/NOTES index 8c62750008..db6756e94e 100644 --- a/compiler/NOTES +++ b/compiler/NOTES @@ -1,3 +1,30 @@ +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) @@ -46,18 +73,6 @@ Cmm parser notes 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) @@ -118,46 +133,6 @@ completeLazyBind: [given a simplified RHS] -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 ~~~~~~~~~~~~~~ diff --git a/compiler/basicTypes/DataCon.lhs b/compiler/basicTypes/DataCon.lhs index dbc6355204..2c4400b3b6 100644 --- a/compiler/basicTypes/DataCon.lhs +++ b/compiler/basicTypes/DataCon.lhs @@ -12,9 +12,10 @@ module DataCon ( 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, @@ -48,6 +49,7 @@ import Module import Data.Char import Data.Word +import Data.List ( partition ) \end{code} @@ -224,11 +226,11 @@ data DataCon -- -- *** 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. @@ -236,7 +238,8 @@ data DataCon -- dcUnivTyVars = [a] -- dcExTyVars = [x,y] -- dcEqSpec = [a:=:(x,y)] - -- dcTheta = [Ord x] + -- dcEqTheta = [x~y] + -- dcDictTheta = [Ord x] -- dcOrigArgTys = [a,List b] -- dcRepTyCon = T @@ -244,7 +247,7 @@ data DataCon -- 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. @@ -272,11 +275,14 @@ data DataCon -- 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 = ... @@ -460,7 +466,7 @@ mkDataCon name declared_infix -- 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 @@ -470,7 +476,8 @@ mkDataCon name declared_infix 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, @@ -486,9 +493,10 @@ mkDataCon name declared_infix -- 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 @@ -497,6 +505,7 @@ mkDataCon name declared_infix -- 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 @@ -506,6 +515,7 @@ mkDataCon name declared_infix 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 @@ -548,8 +558,11 @@ dataConAllTyVars (MkData { dcUnivTyVars = univ_tvs, dcExTyVars = ex_tvs }) 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 @@ -585,7 +598,7 @@ dataConStrictMarks = dcStrictMarks 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 @@ -608,14 +621,14 @@ dataConRepStrictness dc = dcRepStrictness dc 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 @@ -633,10 +646,11 @@ dataConUserType :: DataCon -> Type -- 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 @@ -671,6 +685,21 @@ dataConInstOrigArgTys dc@(MkData {dcOrigArgTys = arg_tys, 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, diff --git a/compiler/basicTypes/MkId.lhs b/compiler/basicTypes/MkId.lhs index 229d390473..8485e1867f 100644 --- a/compiler/basicTypes/MkId.lhs +++ b/compiler/basicTypes/MkId.lhs @@ -44,6 +44,7 @@ import TysPrim import TysWiredIn import PrelRules import Type +import TypeRep import TcGadt import Coercion import TcType @@ -59,7 +60,7 @@ import PrimOp import ForeignCall import DataCon import Id -import Var ( Var, TyVar) +import Var ( Var, TyVar, mkCoVar) import IdInfo import NewDemand import DmdAnal @@ -223,7 +224,7 @@ mkDataConIds wrap_name wkr_name data_con = 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) -------------- @@ -270,8 +271,11 @@ mkDataConIds wrap_name wkr_name data_con 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 $ @@ -279,7 +283,11 @@ mkDataConIds wrap_name wkr_name data_con 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 @@ -287,8 +295,9 @@ mkDataConIds wrap_name wkr_name data_con -- 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 @@ -318,6 +327,7 @@ mkDataConIds wrap_name wkr_name data_con 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) @@ -327,11 +337,18 @@ mkDataConIds wrap_name wkr_name data_con 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 @@ -493,7 +510,7 @@ mkRecordSelId tycon field_label 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 @@ -792,7 +809,7 @@ mkDictSelId name clas -- 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 @@ -814,16 +831,24 @@ mkDictSelId name clas 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} diff --git a/compiler/basicTypes/Var.lhs b/compiler/basicTypes/Var.lhs index cd21b9dd9f..2b7b1d69ee 100644 --- a/compiler/basicTypes/Var.lhs +++ b/compiler/basicTypes/Var.lhs @@ -201,7 +201,8 @@ mkTyVar name kind = ASSERT( not (isCoercionKind kind ) ) 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, diff --git a/compiler/coreSyn/CoreUtils.lhs b/compiler/coreSyn/CoreUtils.lhs index cb6770e4e0..24cf2e539e 100644 --- a/compiler/coreSyn/CoreUtils.lhs +++ b/compiler/coreSyn/CoreUtils.lhs @@ -664,7 +664,7 @@ dataConRepInstPat = dataConInstPat dataConRepArgTys (repeat (FSLIT("ipv"))) 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 @@ -680,9 +680,13 @@ 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 @@ -702,16 +706,17 @@ dataConInstPat :: (DataCon -> [Type]) -- function used to find arg tys -- 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 @@ -739,7 +744,7 @@ dataConInstPat arg_fun fss uniqs con inst_tys -- 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 diff --git a/compiler/ghci/RtClosureInspect.hs b/compiler/ghci/RtClosureInspect.hs index 97e47f7b1d..255c8e1f92 100644 --- a/compiler/ghci/RtClosureInspect.hs +++ b/compiler/ghci/RtClosureInspect.hs @@ -468,6 +468,8 @@ instScheme ty | (tvs, rho) <- tcSplitForAllTys ty = liftTcM$ do -- 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 diff --git a/compiler/hsSyn/HsUtils.lhs b/compiler/hsSyn/HsUtils.lhs index e16a0bde83..6efddcd069 100644 --- a/compiler/hsSyn/HsUtils.lhs +++ b/compiler/hsSyn/HsUtils.lhs @@ -100,7 +100,7 @@ mkHsDictLet binds expr 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 diff --git a/compiler/iface/BuildTyCl.lhs b/compiler/iface/BuildTyCl.lhs index 9f35453b59..1825ae0e3b 100644 --- a/compiler/iface/BuildTyCl.lhs +++ b/compiler/iface/BuildTyCl.lhs @@ -29,6 +29,9 @@ import TyCon import Type import Coercion +import TcRnMonad +import Outputable + import Data.List \end{code} @@ -132,6 +135,7 @@ mkNewTyConRhs tycon_name tycon con = 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), @@ -145,7 +149,9 @@ mkNewTyConRhs tycon_name tycon con -- 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 @@ -274,44 +280,48 @@ buildClass :: Name -> [TyVar] -> ThetaType -> 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 @@ -326,10 +336,13 @@ buildClass class_name tvs sc_theta fds ats sig_stuff tc_isrec -- 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} diff --git a/compiler/iface/MkIface.lhs b/compiler/iface/MkIface.lhs index 0d200d89be..6bbb5998e3 100644 --- a/compiler/iface/MkIface.lhs +++ b/compiler/iface/MkIface.lhs @@ -1218,7 +1218,7 @@ tyThingToIfaceDecl (ATyCon tycon) 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), diff --git a/compiler/typecheck/Inst.lhs b/compiler/typecheck/Inst.lhs index 8195a822fc..c4cf7e11a9 100644 --- a/compiler/typecheck/Inst.lhs +++ b/compiler/typecheck/Inst.lhs @@ -29,20 +29,29 @@ module Inst ( 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 @@ -54,6 +63,8 @@ import FunDeps import TcMType import TcType import Type +import TypeRep +import Class import Unify import Module import Coercion @@ -76,8 +87,9 @@ import DynFlags import Maybes import Util import Outputable - import Data.List +import TypeRep +import Class \end{code} @@ -85,10 +97,12 @@ Selection ~~~~~~~~~ \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 @@ -103,25 +117,33 @@ instToVar (Dict {tci_name = nm, tci_pred = pred}) 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 @@ -138,6 +160,7 @@ fdPredsOfInst (Method {tci_theta = theta}) = theta fdPredsOfInst (ImplicInst {tci_given = gs, tci_wanted = ws}) = fdPredsOfInsts (gs ++ ws) fdPredsOfInst (LitInst {}) = [] +fdPredsOfInst (EqInst {}) = [] fdPredsOfInsts :: [Inst] -> [PredType] fdPredsOfInsts insts = concatMap fdPredsOfInst insts @@ -171,6 +194,7 @@ tyVarsOfInst (ImplicInst {tci_tyvars = tvs, tci_given = givens, tci_wanted = wan `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) @@ -179,6 +203,14 @@ 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 @@ -233,6 +265,15 @@ newDictBndrs :: InstLoc -> TcThetaType -> TcM [Inst] 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 @@ -244,12 +285,11 @@ instCall :: InstOrigin -> [TcType] -> TcThetaType -> TcM HsWrapper -- (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) } ---------------- @@ -258,35 +298,47 @@ instStupidTheta :: InstOrigin -> TcThetaType -> TcM () -- 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 @@ -483,6 +535,15 @@ zonkInst implic@(ImplicInst {}) ; 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} @@ -518,6 +579,10 @@ pprInsts insts = brackets (interpp'SP insts) 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) @@ -525,9 +590,15 @@ pprInst inst = ppr (instName inst) <+> dcolon 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} @@ -667,12 +738,14 @@ lookupSimpleInst :: Inst -> TcM LookupInstResult -- 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 @@ -748,7 +821,7 @@ lookupSimpleInst (Dict {tci_pred = pred, tci_loc = loc}) ; 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)) }}}} @@ -877,3 +950,87 @@ syntaxNameCtxt name orig ty tidy_env 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} diff --git a/compiler/typecheck/TcBinds.lhs b/compiler/typecheck/TcBinds.lhs index 93a9010157..35c5c2c859 100644 --- a/compiler/typecheck/TcBinds.lhs +++ b/compiler/typecheck/TcBinds.lhs @@ -30,6 +30,7 @@ import TcPat import TcMType import TcType import {- Kind parts of -} Type +import Coercion import VarEnv import TysPrim import Id @@ -241,7 +242,7 @@ tc_haskell98 top_lvl sig_fn prag_fn rec_flag binds thing_inside 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 @@ -769,7 +770,17 @@ unifyCtxts (sig1 : sigs) -- Argument is always non-empty 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 diff --git a/compiler/typecheck/TcClassDcl.lhs b/compiler/typecheck/TcClassDcl.lhs index c545dc7e26..67f2945464 100644 --- a/compiler/typecheck/TcClassDcl.lhs +++ b/compiler/typecheck/TcClassDcl.lhs @@ -425,7 +425,7 @@ mkMethId origin clas sel_id inst_tys 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 @@ -528,7 +528,7 @@ mkDefMethRhs origin clas inst_tys sel_id loc GenDefMeth -- 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 diff --git a/compiler/typecheck/TcDeriv.lhs b/compiler/typecheck/TcDeriv.lhs index c9b3967c4c..58a391621d 100644 --- a/compiler/typecheck/TcDeriv.lhs +++ b/compiler/typecheck/TcDeriv.lhs @@ -47,8 +47,6 @@ import Util import ListSetOps import Outputable import Bag - -import Monad (unless) \end{code} %************************************************************************ @@ -443,24 +441,29 @@ baleOut err = addErrTc err >> returnM (Nothing, Nothing) \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} @@ -1165,6 +1168,11 @@ badDerivedPred pred = vcat [ptext SLIT("Can't derive instances where the instance context mentions"), ptext SLIT("type variables that are not data type parameters"), nest 2 (ptext SLIT("Offending constraint:") <+> ppr pred)] -\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} diff --git a/compiler/typecheck/TcEnv.lhs b/compiler/typecheck/TcEnv.lhs index 330e73b8a2..4f48f7fde5 100644 --- a/compiler/typecheck/TcEnv.lhs +++ b/compiler/typecheck/TcEnv.lhs @@ -44,9 +44,6 @@ module TcEnv( -- New Ids newLocalName, newDFunName, newFamInstTyConName, - - -- Errors - famInstNotFound ) where #include "HsVersions.h" @@ -58,6 +55,7 @@ import TcRnMonad import TcMType import TcType import TcGadt +-- import TcSuspension import qualified Type import Var import VarSet @@ -67,6 +65,8 @@ import InstEnv import FamInstEnv import DataCon import TyCon +import TypeRep +import Coercion import Class import Name import PrelNames @@ -75,6 +75,7 @@ import OccName import HscTypes import SrcLoc import Outputable +import Maybes \end{code} @@ -162,7 +163,7 @@ tcLookupLocatedClass = addLocM tcLookupClass 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 @@ -178,17 +179,18 @@ tcLookupLocatedTyCon = addLocM tcLookupTyCon -- -- 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} @@ -378,9 +380,10 @@ tc_extend_local_id_env env th_lvl names_w_ids thing_inside 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] @@ -445,20 +448,30 @@ find_thing _ _ thing = pprPanic "find_thing" (ppr thing) \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 @@ -705,11 +718,4 @@ notFound name 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} diff --git a/compiler/typecheck/TcExpr.lhs b/compiler/typecheck/TcExpr.lhs index a3ed96ceb2..d595ed1cd1 100644 --- a/compiler/typecheck/TcExpr.lhs +++ b/compiler/typecheck/TcExpr.lhs @@ -35,6 +35,8 @@ import DataCon import Name import TyCon import Type +import TypeRep +import Coercion import Var import VarSet import TysWiredIn @@ -70,11 +72,12 @@ tcPolyExpr, tcPolyExprNC 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 => .... @@ -111,7 +114,6 @@ tcInferRho expr = tcInfer (tcMonoExpr expr) \end{code} - %************************************************************************ %* * tcExpr: the main expression typechecker @@ -122,8 +124,10 @@ tcInferRho expr = tcInfer (tcMonoExpr expr) 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') } @@ -167,6 +171,7 @@ tcExpr (HsApp e1 e2) res_ty 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 @@ -282,6 +287,18 @@ tcExpr in_expr@(ExplicitList _ exprs) res_ty -- Non-empty list ; 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 @@ -671,6 +688,7 @@ tcIdApp fun_name n_args arg_checker 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} @@ -714,6 +732,7 @@ tcId orig fun_name res_ty -- 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] @@ -758,27 +777,32 @@ instFun orig fun subst [] 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] @@ -952,8 +976,11 @@ lookupFun orig id_name 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")) } @@ -1180,3 +1207,9 @@ polySpliceErr id = 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} diff --git a/compiler/typecheck/TcHsType.lhs b/compiler/typecheck/TcHsType.lhs index fc7a8486f9..f4c493ea59 100644 --- a/compiler/typecheck/TcHsType.lhs +++ b/compiler/typecheck/TcHsType.lhs @@ -417,10 +417,11 @@ kc_pred pred@(HsClassP cls tys) } 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) } --------------------------- diff --git a/compiler/typecheck/TcInstDcls.lhs b/compiler/typecheck/TcInstDcls.lhs index d314e1e21f..21c89287bb 100644 --- a/compiler/typecheck/TcInstDcls.lhs +++ b/compiler/typecheck/TcInstDcls.lhs @@ -29,6 +29,7 @@ import TcSimplify import Type import Coercion import TyCon +import TypeRep import DataCon import Class import Var @@ -257,7 +258,9 @@ tcLocalInstDecl1 decl@(L loc (InstDecl poly_ty binds uprags ats)) -- (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, @@ -603,20 +606,30 @@ tcInstDecl2 (InstInfo { iSpec = ispec, iBinds = VanillaInst monobinds uprags }) -- 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 @@ -624,10 +637,10 @@ tcInstDecl2 (InstInfo { iSpec = ispec, iBinds = VanillaInst monobinds uprags }) -- 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 @@ -641,8 +654,8 @@ tcInstDecl2 (InstInfo { iSpec = ispec, iBinds = VanillaInst monobinds uprags }) 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 @@ -655,7 +668,7 @@ tcInstDecl2 (InstInfo { iSpec = ispec, iBinds = VanillaInst monobinds uprags }) -- 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 @@ -667,15 +680,32 @@ tcInstDecl2 (InstInfo { iSpec = ispec, iBinds = VanillaInst monobinds uprags }) 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 diff --git a/compiler/typecheck/TcMType.lhs b/compiler/typecheck/TcMType.lhs index eee4ec2403..7186b3c3b5 100644 --- a/compiler/typecheck/TcMType.lhs +++ b/compiler/typecheck/TcMType.lhs @@ -53,7 +53,6 @@ module TcMType ( zonkTcKindToKind, zonkTcKind, zonkTopTyVar, readKindVar, writeKindVar - ) where #include "HsVersions.h" @@ -199,7 +198,7 @@ newMetaTyVar :: BoxInfo -> Kind -> TcM TcTyVar -- 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") @@ -216,7 +215,7 @@ instMetaTyVar :: BoxInfo -> TyVar -> TcM TcTyVar -- 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)) } @@ -236,7 +235,8 @@ writeMetaTyVar tyvar ty | 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 @@ -331,7 +331,7 @@ readFilledBox :: BoxyTyVar -> TcM TcType 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 @@ -365,7 +365,7 @@ lookupTcTyVar tyvar 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 diff --git a/compiler/typecheck/TcPat.lhs b/compiler/typecheck/TcPat.lhs index 9cea0eaa7b..8b2fac26ca 100644 --- a/compiler/typecheck/TcPat.lhs +++ b/compiler/typecheck/TcPat.lhs @@ -31,6 +31,7 @@ import TcHsType import TysWiredIn import TcGadt import Type +import Coercion import StaticFlags import TyCon import DataCon @@ -59,7 +60,8 @@ tcLetPat :: (Name -> Maybe TcRhoType) -> 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 @@ -104,11 +106,13 @@ tc_lam_pats :: [(LPat Name,BoxySigmaType)] -> ((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 @@ -138,7 +142,9 @@ tcCheckExistentialPat pats ex_tvs pat_tys body_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 @@ -434,9 +440,15 @@ tc_pat pstate pat_in@(ConPatIn (L con_span con_name) arg_pats) pat_ty thing_insi ------------------------ -- 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 @@ -547,7 +559,7 @@ tcConPat :: PatState -> SrcSpan -> DataCon -> TyCon -> 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 @@ -558,12 +570,12 @@ tcConPat pstate con_span data_con tycon pat_ty arg_pats thing_inside ; 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 @@ -725,6 +737,7 @@ refineAlt :: DataCon -- For tracing only -> 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 @@ -751,7 +764,7 @@ 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 @@ -965,6 +978,16 @@ nonRigidMatch con = 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} diff --git a/compiler/typecheck/TcRnMonad.lhs b/compiler/typecheck/TcRnMonad.lhs index f36be69fa8..ea01b1a8c3 100644 --- a/compiler/typecheck/TcRnMonad.lhs +++ b/compiler/typecheck/TcRnMonad.lhs @@ -23,6 +23,7 @@ import TcType import InstEnv import FamInstEnv +import Coercion import Var import Id import VarSet @@ -177,7 +178,7 @@ initTcRnIf uniq_tag hsc_env gbl_env lcl_env thing_inside ; 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 } @@ -1022,5 +1023,3 @@ forkM doc thing_inside -- pprPanic "forkM" doc Just r -> r) } \end{code} - - diff --git a/compiler/typecheck/TcRnTypes.lhs b/compiler/typecheck/TcRnTypes.lhs index d11ee27d57..4138c00a18 100644 --- a/compiler/typecheck/TcRnTypes.lhs +++ b/compiler/typecheck/TcRnTypes.lhs @@ -18,7 +18,7 @@ module TcRnTypes( WhereFrom(..), mkModDeps, -- Typechecker types - TcTyThing(..), pprTcTyThingCategory, + TcTyThing(..), pprTcTyThingCategory, RefinementVisibility(..), -- Template Haskell ThStage(..), topStage, topSpliceStage, @@ -34,7 +34,8 @@ module TcRnTypes( plusLIEs, mkLIE, isEmptyLIE, lieToList, listToLIE, -- Misc other types - TcId, TcIdSet, TcDictBinds + TcId, TcIdSet, TcDictBinds, + ) where #include "HsVersions.h" @@ -43,6 +44,7 @@ import HsSyn hiding (LIE) import HscTypes import Packages import Type +import Coercion import TcType import TcGadt import InstEnv @@ -65,6 +67,7 @@ import Util import Bag import Outputable import ListSetOps +import FiniteMap import Data.Maybe import Data.List @@ -115,8 +118,7 @@ data Env gbl lcl -- Changes as we move into an expression 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 @@ -316,15 +318,11 @@ data TcLclEnv -- Changes as we move inside an expression -- 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 @@ -435,7 +433,8 @@ data TcTyThing | 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, @@ -450,6 +449,19 @@ data TcTyThing | 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" <> @@ -463,6 +475,13 @@ pprTcTyThingCategory (AGlobal thing) = pprTyThingCategory thing 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} @@ -605,6 +624,10 @@ type Int, represented by 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 { @@ -671,6 +694,33 @@ data Inst 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 @@ -707,6 +757,14 @@ cmpInst (ImplicInst {}) (Dict {}) = GT 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} @@ -808,6 +866,7 @@ data InstOrigin | 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)] @@ -826,4 +885,6 @@ instance Outputable InstOrigin where 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} diff --git a/compiler/typecheck/TcRnTypes.lhs-boot b/compiler/typecheck/TcRnTypes.lhs-boot new file mode 100644 index 0000000000..36c43fc496 --- /dev/null +++ b/compiler/typecheck/TcRnTypes.lhs-boot @@ -0,0 +1,13 @@ +\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} diff --git a/compiler/typecheck/TcSimplify.lhs b/compiler/typecheck/TcSimplify.lhs index f87b04426e..4341229667 100644 --- a/compiler/typecheck/TcSimplify.lhs +++ b/compiler/typecheck/TcSimplify.lhs @@ -16,6 +16,8 @@ module TcSimplify ( tcSimplifyDeriv, tcSimplifyDefault, bindInstsOfLocalFuns, bindIrreds, + + misMatchMsg ) where #include "HsVersions.h" @@ -31,6 +33,8 @@ import TcGadt import TcType import TcMType import TcIface +import TcTyFuns +import TypeRep import Var import Name import NameSet @@ -44,12 +48,14 @@ import ErrUtils 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 @@ -702,11 +708,15 @@ tcSimplifyInfer doc tau_tvs wanted -- 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. @@ -739,6 +749,8 @@ approximateImplications doc want_dict irreds = [ 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} @@ -781,7 +793,8 @@ tcSimplifyInferCheck 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, @@ -805,6 +818,7 @@ tcSimplifyInferCheck loc tau_tvs givens wanteds -- 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} @@ -887,7 +901,8 @@ tcSimplifyCheck :: InstLoc -> 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) } @@ -901,7 +916,8 @@ tcSimplifyCheckPat :: InstLoc -> 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) } @@ -959,31 +975,36 @@ makeImplicationBind :: InstLoc -> [TcTyVar] -> Refinement -- -- 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)) } ----------------------------------------------------------- @@ -992,7 +1013,9 @@ tryHardCheckLoop :: SDoc -> 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 @@ -1004,7 +1027,9 @@ gentleCheckLoop :: InstLoc -> 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 @@ -1042,27 +1067,32 @@ with tryHardCheckLooop. ----------------------------------------------------------- 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] @@ -1135,7 +1165,8 @@ tcSimplifySuperClasses -> [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 } @@ -1262,7 +1293,8 @@ tcSimplifyRestricted -- Used for restricted binding groups 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 @@ -1274,12 +1306,12 @@ tcSimplifyRestricted doc top_lvl bndrs tau_tvs wanteds -- 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 @@ -1323,7 +1355,7 @@ tcSimplifyRestricted doc top_lvl bndrs tau_tvs wanteds (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 @@ -1413,7 +1445,7 @@ tcSimplifyRuleLhs wanteds -- 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} @@ -1466,12 +1498,12 @@ tcSimplifyIPs :: [Inst] -- The implicit parameters bound here -- 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 ) @@ -1531,7 +1563,7 @@ bindInstsOfLocalFuns wanteds local_ids 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 } @@ -1626,7 +1658,8 @@ reduceContext :: RedEnv -> [Inst] -- Wanted -> TcM (ImprovementDone, TcDictBinds, -- Dictionary bindings - [Inst]) -- Irreducible + [Inst], -- Irreducible + [Inst]) -- Needed givens reduceContext env wanteds = do { traceTc (text "reduceContext" <+> (vcat [ @@ -1637,18 +1670,59 @@ reduceContext env wanteds text "----------------------" ])) - -- Build the Avail mapping from "givens" - ; init_state <- foldlM addGiven emptyAvails (red_givens env) - -- Do the real work - -- Process non-implication constraints first, so that they are - -- available to help solving the implication constraints - -- ToDo: seems a bit inefficient and ad-hoc - ; let (implics, rest) = partition isImplicInst wanteds - ; avails <- reduceList env (rest ++ implics) init_state + ; let 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 "----------------------", @@ -1659,10 +1733,12 @@ reduceContext env wanteds 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 @@ -1724,41 +1800,45 @@ reduceList env@(RedEnv {red_stack = (n,stk)}) wanteds state 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) @@ -1867,6 +1947,31 @@ reduceInst env avails other_inst ; 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 @@ -1901,55 +2006,97 @@ Note that \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] @@ -2104,43 +2251,78 @@ dependency analyser can sort them out later 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} @@ -2186,6 +2368,21 @@ addRefinedGiven reft (refined_givens, avails) given -- 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] @@ -2310,11 +2507,14 @@ tcSimplifyInteractive wanteds -- 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 @@ -2377,7 +2577,7 @@ disambiguate doc interactive dflags insts = 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 @@ -2440,7 +2640,7 @@ disambigGroup :: [Type] -- The default types 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 () @@ -2455,7 +2655,9 @@ disambigGroup default_tys dicts -- 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 + } ----------------------- @@ -2700,14 +2902,17 @@ reportNoInstances tidy_env mb_what insts = 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) @@ -2716,6 +2921,13 @@ report_no_instances tidy_env mb_what 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 @@ -2723,9 +2935,9 @@ report_no_instances tidy_env mb_what insts | 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 @@ -2868,4 +3080,59 @@ reduceDepthErr n stack 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} diff --git a/compiler/typecheck/TcTyClsDecls.lhs b/compiler/typecheck/TcTyClsDecls.lhs index f827117623..863cd6df1f 100644 --- a/compiler/typecheck/TcTyClsDecls.lhs +++ b/compiler/typecheck/TcTyClsDecls.lhs @@ -263,19 +263,17 @@ tcFamInstDecl1 (decl@TySynonym {tcdLName = L loc tc_name}) ; -- (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) @@ -337,7 +335,7 @@ tcFamInstDecl1 (decl@TyData {tcdND = new_or_data, tcdLName = L loc tc_name, ; 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)) @@ -754,7 +752,7 @@ tcTyClDecl1 calc_isrec 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 @@ -1074,14 +1072,14 @@ checkNewDataCon con -- 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 () @@ -1117,6 +1115,7 @@ checkValidClass cls -- 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 @@ -1264,8 +1263,9 @@ tooFewParmsErr arity = 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") diff --git a/compiler/typecheck/TcTyFuns.lhs b/compiler/typecheck/TcTyFuns.lhs new file mode 100644 index 0000000000..b3f97be530 --- /dev/null +++ b/compiler/typecheck/TcTyFuns.lhs @@ -0,0 +1,868 @@ + +\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} diff --git a/compiler/typecheck/TcType.lhs b/compiler/typecheck/TcType.lhs index 50659d522d..a27a0c5da7 100644 --- a/compiler/typecheck/TcType.lhs +++ b/compiler/typecheck/TcType.lhs @@ -58,6 +58,7 @@ module TcType ( isDoubleTy, isFloatTy, isIntTy, isStringTy, isIntegerTy, isBoolTy, isUnitTy, isCharTy, isTauTy, isTauTyCon, tcIsTyVarTy, tcIsForAllTy, + isOpenSynTyConApp, --------------------------------- -- Misc type manipulators @@ -162,7 +163,6 @@ import Data.List import Data.IORef \end{code} - %************************************************************************ %* * \subsection{Types} @@ -295,12 +295,12 @@ data BoxInfo -- 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 @@ -387,7 +387,6 @@ kind_var_occ :: OccName -- Just one for all KindVars -- They may be jiggled by tidying kind_var_occ = mkOccName tvName "k" \end{code} -\end{code} %************************************************************************ %* * @@ -475,7 +474,7 @@ pprSkolInfo UnkSkol = panic "UnkSkol" 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} @@ -497,7 +496,7 @@ isTyConableTyVar, isSkolemTyVar, isExistentialTyVar, 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) @@ -539,14 +538,14 @@ isSigTyVar 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 @@ -595,10 +594,10 @@ isRigidTy :: TcType -> Bool -- 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) @@ -976,6 +975,15 @@ is_tc uniq ty = case tcSplitTyConApp_maybe ty of 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} + %************************************************************************ %* * diff --git a/compiler/typecheck/TcUnify.lhs b/compiler/typecheck/TcUnify.lhs index 821a1cc086..c9def34136 100644 --- a/compiler/typecheck/TcUnify.lhs +++ b/compiler/typecheck/TcUnify.lhs @@ -33,10 +33,12 @@ import TypeRep 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 @@ -44,13 +46,13 @@ import TysWiredIn import Var import VarSet import VarEnv -import Module import Name import ErrUtils import Maybes import BasicTypes import Util import Outputable +import Unique \end{code} %************************************************************************ @@ -64,7 +66,7 @@ tcInfer :: (BoxyType -> TcM a) -> TcM (a, TcType) 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} @@ -87,7 +89,7 @@ subFunTys :: SDoc -- Somthing like "The function f has 3 arguments" -- -- 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 @@ -139,9 +141,14 @@ subFunTys error_herald n_pats res_ty thing_inside -- 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 @@ -204,7 +211,7 @@ boxySplitTyConApp tc orig_ty = 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 @@ -241,7 +248,7 @@ boxySplitAppTy orig_ty = 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' @@ -301,7 +308,7 @@ withBox :: Kind -> (BoxySigmaType -> TcM a) -> TcM (a, TcType) 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} @@ -474,7 +481,9 @@ boxy_match tmpl_tvs orig_tmpl_ty boxy_tvs orig_boxy_ty subst (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] @@ -527,7 +536,7 @@ boxyLub orig_ty1 orig_ty2 -- 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 @@ -563,7 +572,7 @@ That is, that a value of type offered_ty is acceptable in 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. @@ -627,9 +636,16 @@ tc_sub1 sub_ctxt act_sty act_ty exp_ib exp_sty exp_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) @@ -644,12 +660,14 @@ tc_sub1 sub_ctxt act_sty (TyVarTy tv) exp_ib exp_sty exp_ty 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 @@ -670,7 +688,8 @@ tc_sub1 sub_ctxt act_sty actual_ty exp_ib exp_sty expected_ty -- 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 @@ -702,17 +721,20 @@ tc_sub1 sub_ctxt act_sty actual_ty exp_ib exp_sty expected_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' @@ -720,14 +742,24 @@ tc_sub1 sub_ctxt act_sty act_ty@(FunTy act_arg act_res) _ exp_sty (TyVarTy exp_t 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 @@ -735,9 +767,14 @@ defer_to_boxy_matching sub_ctxt act_sty actual_ty exp_ib exp_sty expected_ty ----------------------------------- 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 @@ -745,8 +782,10 @@ 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) } @@ -771,11 +810,12 @@ tcGen :: BoxySigmaType -- expected_ty 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) @@ -816,7 +856,7 @@ tcGen expected_ty extra_tvs thing_inside -- We expect expected_ty to be a forall ; returnM (co_fn, result) } where free_tvs = tyVarsOfType expected_ty `unionVarSet` extra_tvs -\end{code} +\end{code} @@ -830,20 +870,20 @@ The exported functions are all defined as versions of some 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 @@ -853,27 +893,31 @@ 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} @@ -895,8 +939,8 @@ unifyTypeList (ty1:tys@(ty2:_)) = do { unifyType ty1 ty2 %* * %************************************************************************ -@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. @@ -904,6 +948,10 @@ 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 @@ -919,54 +967,73 @@ type Outer = Bool -- True <=> this is the outer level of a unification -- 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 @@ -980,8 +1047,9 @@ u_tys outer nb1 orig_ty1 ty1 nb2 orig_ty2 ty2 { 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)) @@ -995,55 +1063,111 @@ u_tys outer nb1 orig_ty1 ty1 nb2 orig_ty2 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 @@ -1053,9 +1177,20 @@ the f1,f2 (because it'd absorb the app). If we unify f1:=:f2 first, 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... @@ -1119,12 +1254,12 @@ back into @uTys@ if it turns out that the variable is already bound. \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 @@ -1144,10 +1279,10 @@ uVar outer swapped tv1 nb2 ps_ty2 ty2 ---------------- 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 @@ -1161,27 +1296,97 @@ uUnfilledVar outer swapped tv1 details1 ps_ty2 (TyVarTy tv2) 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 () @@ -1202,7 +1407,7 @@ uMetaVar swapped tv1 BoxTv ref1 ps_ty2 non_var_ty2 ; 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 } @@ -1212,43 +1417,44 @@ uMetaVar swapped tv1 info1 ref1 ps_ty2 non_var_ty2 ---------------- 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 @@ -1286,7 +1492,8 @@ uUnfilledVars outer swapped tv1 (MetaTv info1 ref1) tv2 (MetaTv info2 ref2) -- 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) @@ -1302,7 +1509,8 @@ updateMeta tv1 ref1 ty2 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 @@ -1431,7 +1639,7 @@ refineBox ty@(TyVarTy box_tv) | 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 @@ -1443,7 +1651,7 @@ refineBoxToTau ty@(TyVarTy box_tv) , 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 @@ -1483,7 +1691,7 @@ unBox (TyVarTy tv) , 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 @@ -1577,8 +1785,8 @@ unifyKindCtxt swapped tv1 ty2 tidy_env -- not swapped => tv1 expected, ty2 infer 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)) @@ -1586,58 +1794,6 @@ unifyMisMatch outer swapped ty1 ty2 } ----------------------- -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 @@ -1710,7 +1866,7 @@ uUnboundKVar swapped kv1 k2@(TyVarTy kv2) = 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 @@ -1781,7 +1937,7 @@ unifyFunKind (TyVarTy kvar) = 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) diff --git a/compiler/typecheck/TcUnify.lhs-boot b/compiler/typecheck/TcUnify.lhs-boot index b39573e076..4d385b123c 100644 --- a/compiler/typecheck/TcUnify.lhs-boot +++ b/compiler/typecheck/TcUnify.lhs-boot @@ -1,11 +1,13 @@ \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} diff --git a/compiler/types/Coercion.lhs b/compiler/types/Coercion.lhs index 02d92d73e1..6417e41b0c 100644 --- a/compiler/types/Coercion.lhs +++ b/compiler/types/Coercion.lhs @@ -22,8 +22,10 @@ module Coercion ( 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, @@ -39,8 +41,8 @@ module Coercion ( mkSymCoI, mkTransCoI, mkTyConAppCoI, mkAppTyCoI, mkFunTyCoI, mkNoteTyCoI, mkForAllTyCoI, - fromCoI, - mkClassPPredCoI, mkIParamPredCoI, mkEqPredCoI, + fromCoI, fromACo, + mkClassPPredCoI, mkIParamPredCoI, mkEqPredCoI ) where @@ -60,6 +62,9 @@ import BasicTypes 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] @@ -102,9 +107,6 @@ splitCoercionKind_maybe co | Just co' <- kindView co = splitCoercionKind_maybe 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) @@ -227,6 +229,17 @@ mkRightCoercion co | 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] @@ -451,7 +464,6 @@ splitNewTypeRepCo_maybe other -- CoercionI smart constructors -- lifted smart constructors of ordinary coercions - \begin{code} -- CoercionI is either -- (a) proper coercion @@ -462,6 +474,16 @@ isIdentityCoercion :: CoercionI -> Bool 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] @@ -474,18 +496,9 @@ mkTransCoI aco IdCo = aco 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 @@ -505,31 +518,25 @@ mkForAllTyCoI :: TyVar -> CoercionI -> CoercionI 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} diff --git a/compiler/types/TyCon.lhs b/compiler/types/TyCon.lhs index 1471f57c54..3a8209987a 100644 --- a/compiler/types/TyCon.lhs +++ b/compiler/types/TyCon.lhs @@ -20,8 +20,9 @@ module TyCon( 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, @@ -682,6 +683,9 @@ isSynTyCon _ = False 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 diff --git a/compiler/types/Type.lhs b/compiler/types/Type.lhs index 8f23a35853..de7e460664 100644 --- a/compiler/types/Type.lhs +++ b/compiler/types/Type.lhs @@ -1467,8 +1467,6 @@ isSuperKind 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 |