diff options
| -rw-r--r-- | compiler/coreSyn/TrieMap.lhs | 11 | ||||
| -rw-r--r-- | compiler/ghc.mk | 2 | ||||
| -rw-r--r-- | compiler/types/FamInstEnv.lhs | 136 | ||||
| -rw-r--r-- | compiler/types/OptCoercion.lhs | 15 | ||||
| -rw-r--r-- | compiler/types/Unify.lhs | 143 | ||||
| -rw-r--r-- | docs/core-spec/core-spec.mng | 14 | ||||
| -rw-r--r-- | docs/core-spec/core-spec.pdf | bin | 347921 -> 349150 bytes |
7 files changed, 197 insertions, 124 deletions
diff --git a/compiler/coreSyn/TrieMap.lhs b/compiler/coreSyn/TrieMap.lhs index c013b5da7a..c5cd9902bc 100644 --- a/compiler/coreSyn/TrieMap.lhs +++ b/compiler/coreSyn/TrieMap.lhs @@ -14,7 +14,7 @@ {-# LANGUAGE TypeFamilies #-} module TrieMap( CoreMap, emptyCoreMap, extendCoreMap, lookupCoreMap, foldCoreMap, - TypeMap, foldTypeMap, -- lookupTypeMap_mod, + TypeMap, emptyTypeMap, extendTypeMap, lookupTypeMap, foldTypeMap, CoercionMap, MaybeMap, ListMap, @@ -588,6 +588,15 @@ instance Outputable a => Outputable (TypeMap a) where foldTypeMap :: (a -> b -> b) -> b -> TypeMap a -> b foldTypeMap k z m = fdT k m z +emptyTypeMap :: TypeMap a +emptyTypeMap = EmptyTM + +lookupTypeMap :: TypeMap a -> Type -> Maybe a +lookupTypeMap cm t = lkT emptyCME t cm + +extendTypeMap :: TypeMap a -> Type -> a -> TypeMap a +extendTypeMap m t v = xtT emptyCME t (\_ -> Just v) m + wrapEmptyTypeMap :: TypeMap a wrapEmptyTypeMap = TM { tm_var = emptyTM , tm_app = EmptyTM diff --git a/compiler/ghc.mk b/compiler/ghc.mk index c258bf2053..2a7a8c4b87 100644 --- a/compiler/ghc.mk +++ b/compiler/ghc.mk @@ -421,7 +421,7 @@ compiler_stage3_SplitObjs = NO # We therefore need to split some of the modules off into a separate # DLL. This clump are the modules reachable from DynFlags: compiler_stage2_dll0_START_MODULE = DynFlags -compiler_stage2_dll0_MODULES = Annotations Avail Bag BasicTypes Binary Bitmap BlockId BreakArray BufWrite ByteCodeAsm ByteCodeInstr ByteCodeItbls ByteCodeLink CLabel Class CmdLineParser Cmm CmmCallConv CmmExpr CmmInfo CmmMachOp CmmNode CmmType CmmUtils CoAxiom CodeGen.Platform CodeGen.Platform.ARM CodeGen.Platform.NoRegs CodeGen.Platform.PPC CodeGen.Platform.PPC_Darwin CodeGen.Platform.SPARC CodeGen.Platform.X86 CodeGen.Platform.X86_64 Coercion Config Constants CoreArity CoreFVs CoreSubst CoreSyn CoreTidy CoreUnfold CoreUtils CostCentre DataCon Demand Digraph DriverPhases DynFlags Encoding ErrUtils Exception FamInstEnv FastBool FastFunctions FastMutInt FastString FastTypes Fingerprint FiniteMap ForeignCall Hoopl Hoopl.Dataflow HsBinds HsDecls HsDoc HsExpr HsImpExp HsLit HsPat HsSyn HsTypes HsUtils HscTypes Id IdInfo IfaceSyn IfaceType InstEnv InteractiveEvalTypes Kind ListSetOps Literal Maybes MkCore MkGraph MkId Module MonadUtils Name NameEnv NameSet ObjLink OccName OccurAnal OptCoercion OrdList Outputable PackageConfig Packages Pair Panic Platform PlatformConstants PprCmm PprCmmDecl PprCmmExpr PprCore PrelNames PrelRules Pretty PrimOp RdrName Reg RegClass Rules SMRep Serialized SrcLoc StaticFlags StgCmmArgRep StgCmmClosure StgCmmEnv StgCmmLayout StgCmmMonad StgCmmProf StgCmmTicky StgCmmUtils StgSyn Stream StringBuffer TcEvidence TcType TyCon Type TypeRep TysPrim TysWiredIn Unify UniqFM UniqSet UniqSupply Unique Util Var VarEnv VarSet +compiler_stage2_dll0_MODULES = Annotations Avail Bag BasicTypes Binary Bitmap BlockId BreakArray BufWrite ByteCodeAsm ByteCodeInstr ByteCodeItbls ByteCodeLink CLabel Class CmdLineParser Cmm CmmCallConv CmmExpr CmmInfo CmmMachOp CmmNode CmmType CmmUtils CoAxiom CodeGen.Platform CodeGen.Platform.ARM CodeGen.Platform.NoRegs CodeGen.Platform.PPC CodeGen.Platform.PPC_Darwin CodeGen.Platform.SPARC CodeGen.Platform.X86 CodeGen.Platform.X86_64 Coercion Config Constants CoreArity CoreFVs CoreSubst CoreSyn CoreTidy CoreUnfold CoreUtils CostCentre DataCon Demand Digraph DriverPhases DynFlags Encoding ErrUtils Exception FamInstEnv FastBool FastFunctions FastMutInt FastString FastTypes Fingerprint FiniteMap ForeignCall Hoopl Hoopl.Dataflow HsBinds HsDecls HsDoc HsExpr HsImpExp HsLit HsPat HsSyn HsTypes HsUtils HscTypes Id IdInfo IfaceSyn IfaceType InstEnv InteractiveEvalTypes Kind ListSetOps Literal Maybes MkCore MkGraph MkId Module MonadUtils Name NameEnv NameSet ObjLink OccName OccurAnal OptCoercion OrdList Outputable PackageConfig Packages Pair Panic Platform PlatformConstants PprCmm PprCmmDecl PprCmmExpr PprCore PrelNames PrelRules Pretty PrimOp RdrName Reg RegClass Rules SMRep Serialized SrcLoc StaticFlags StgCmmArgRep StgCmmClosure StgCmmEnv StgCmmLayout StgCmmMonad StgCmmProf StgCmmTicky StgCmmUtils StgSyn Stream StringBuffer TcEvidence TcType TrieMap TyCon Type TypeRep TysPrim TysWiredIn Unify UniqFM UniqSet UniqSupply Unique Util Var VarEnv VarSet compiler_stage2_dll0_HS_OBJS = \ $(patsubst %,compiler/stage2/build/%.$(dyn_osuf),$(subst .,/,$(compiler_stage2_dll0_MODULES))) diff --git a/compiler/types/FamInstEnv.lhs b/compiler/types/FamInstEnv.lhs index d7bdeccea3..63a4c50e2c 100644 --- a/compiler/types/FamInstEnv.lhs +++ b/compiler/types/FamInstEnv.lhs @@ -28,7 +28,10 @@ module FamInstEnv ( isDominatedBy, -- Normalisation - chooseBranch, topNormaliseType, normaliseType, normaliseTcApp + chooseBranch, topNormaliseType, normaliseType, normaliseTcApp, + + -- Flattening + flattenTys ) where #include "HsVersions.h" @@ -47,7 +50,10 @@ import Name import UniqFM import Outputable import Maybes +import TrieMap +import Unique import Util +import Var import Pair import SrcLoc import NameSet @@ -378,6 +384,18 @@ identicalFamInst (FamInst { fi_axiom = ax1 }) (FamInst { fi_axiom = ax2 }) %* * %************************************************************************ +Note [Apartness] +~~~~~~~~~~~~~~~~ +In dealing with closed type families, we must be able to check that one type +will never reduce to another. This check is called /apartness/. The check +is always between a target (which may be an arbitrary type) and a pattern. +Here is how we do it: + +apart(target, pattern) = not (unify(flatten(target), pattern)) + +where flatten (implemented in flattenTys, below) converts all type-family +applications into fresh variables. (See Note [Flattening].) + Note [Compatibility] ~~~~~~~~~~~~~~~~~~~~ Two patterns are /compatible/ if either of the following conditions hold: @@ -402,7 +420,7 @@ only when we can be sure that 'a' is not Int. To achieve this, after finding a possible match within the equations, we have to go back to all previous equations and check that, under the substitution induced by the match, other branches are surely apart. (See -[Apartness] in types/Unify.lhs.) This is similar to what happens with class +[Apartness].) This is similar to what happens with class instance selection, when we need to guarantee that there is only a match and no unifiers. The exact algorithm is different here because the the potentially-overlapping group is closed. @@ -433,7 +451,7 @@ b is instantiated with Int, but the RHSs coincide there, so it's all OK. So, the rule is this: when looking up a branch in a closed type family, we find a branch that matches the target, but then we make sure that the target is apart from every previous *incompatible* branch. We don't check the -branches that are compatible with the matching branch, because they are eithe +branches that are compatible with the matching branch, because they are either irrelevant (clause 1 of compatible) or benign (clause 2 of compatible). \begin{code} @@ -441,7 +459,7 @@ irrelevant (clause 1 of compatible) or benign (clause 2 of compatible). compatibleBranches :: CoAxBranch -> CoAxBranch -> Bool compatibleBranches (CoAxBranch { cab_lhs = lhs1, cab_rhs = rhs1 }) (CoAxBranch { cab_lhs = lhs2, cab_rhs = rhs2 }) - = case tcApartTys instanceBindFun lhs1 lhs2 of + = case tcUnifyTysFG instanceBindFun lhs1 lhs2 of SurelyApart -> True Unifiable subst | Type.substTy subst rhs1 `eqType` Type.substTy subst rhs2 @@ -469,7 +487,7 @@ computeAxiomIncomps ax@(CoAxiom { co_ax_branches = branches }) %************************************************************************ %* * Constructing axioms - These functions are here because tidyType / tcApartTys + These functions are here because tidyType / tcUnifyTysFG are not available in CoAxiom %* * %************************************************************************ @@ -783,7 +801,7 @@ findBranch (CoAxBranch { cab_tvs = tpl_tvs, cab_lhs = tpl_lhs, cab_incomps = inc = case tcMatchTys (mkVarSet tpl_tvs) tpl_lhs target_tys of Just subst -- matching worked. now, check for apartness. | all (isSurelyApart - . tcApartTys instanceBindFun target_tys + . tcUnifyTysFG instanceBindFun flattened_target . coAxBranchLHS) incomps -> -- matching worked & we're apart from all incompatible branches. success Just (ind, substTyVars subst tpl_tvs) @@ -794,6 +812,10 @@ findBranch (CoAxBranch { cab_tvs = tpl_tvs, cab_lhs = tpl_lhs, cab_incomps = inc where isSurelyApart SurelyApart = True isSurelyApart _ = False + flattened_target = flattenTys in_scope target_tys + in_scope = mkInScopeSet (unionVarSets $ + map (tyVarsOfTypes . coAxBranchLHS) incomps) + -- fail if no branches left findBranch [] _ _ = Nothing @@ -901,3 +923,105 @@ normaliseType env (ForAllTy tyvar ty1) normaliseType _ ty@(TyVarTy _) = (Refl ty,ty) \end{code} + +%************************************************************************ +%* * + Flattening +%* * +%************************************************************************ + +Note [Flattening] +~~~~~~~~~~~~~~~~~ + +As described in +http://research.microsoft.com/en-us/um/people/simonpj/papers/ext-f/axioms-extended.pdf +we sometimes need to flatten core types before unifying them. Flattening +means replacing all top-level uses of type functions with fresh variables, +taking care to preserve sharing. That is, the type (Either (F a b) (F a b)) should +flatten to (Either c c), never (Either c d). + +Defined here because of module dependencies. + +\begin{code} + +type FlattenMap = TypeMap TyVar + +-- See Note [Flattening] +flattenTys :: InScopeSet -> [Type] -> [Type] +flattenTys in_scope tys = snd $ coreFlattenTys all_in_scope emptyTypeMap tys + where + -- when we hit a type function, we replace it with a fresh variable + -- but, we need to make sure that this fresh variable isn't mentioned + -- *anywhere* in the types we're flattening, even if locally-bound in + -- a forall. That way, we can ensure consistency both within and outside + -- of that forall. + all_in_scope = in_scope `extendInScopeSetSet` allTyVarsInTys tys + +coreFlattenTys :: InScopeSet -> FlattenMap -> [Type] -> (FlattenMap, [Type]) +coreFlattenTys in_scope = go [] + where + go rtys m [] = (m, reverse rtys) + go rtys m (ty : tys) + = let (m', ty') = coreFlattenTy in_scope m ty in + go (ty' : rtys) m' tys + +coreFlattenTy :: InScopeSet -> FlattenMap -> Type -> (FlattenMap, Type) +coreFlattenTy in_scope = go + where + go m ty@(TyVarTy {}) = (m, ty) + go m (AppTy ty1 ty2) = let (m1, ty1') = go m ty1 + (m2, ty2') = go m1 ty2 in + (m2, AppTy ty1' ty2') + go m (TyConApp tc tys) + | isFamilyTyCon tc + = let (m', tv) = coreFlattenTyFamApp in_scope m tc tys in + (m', mkTyVarTy tv) + + | otherwise + = let (m', tys') = coreFlattenTys in_scope m tys in + (m', mkTyConApp tc tys') + + go m (FunTy ty1 ty2) = let (m1, ty1') = go m ty1 + (m2, ty2') = go m1 ty2 in + (m2, FunTy ty1' ty2') + + -- Note to RAE: this will have to be changed with kind families + go m (ForAllTy tv ty) = let (m', ty') = go m ty in + (m', ForAllTy tv ty') + + go m ty@(LitTy {}) = (m, ty) + +coreFlattenTyFamApp :: InScopeSet -> FlattenMap + -> TyCon -- type family tycon + -> [Type] -- args + -> (FlattenMap, TyVar) +coreFlattenTyFamApp in_scope m fam_tc fam_args + = case lookupTypeMap m fam_ty of + Just tv -> (m, tv) + -- we need fresh variables here, but this is called far from + -- any good source of uniques. So, we generate one from thin + -- air, using the arbitrary prime number 71 as a seed + Nothing -> let tyvar_unique = deriveUnique (getUnique fam_tc) 71 + tyvar_name = mkSysTvName tyvar_unique (fsLit "fl") + tv = uniqAway in_scope $ mkTyVar tyvar_name (typeKind fam_ty) + m' = extendTypeMap m fam_ty tv in + (m', tv) + where fam_ty = TyConApp fam_tc fam_args + +allTyVarsInTys :: [Type] -> VarSet +allTyVarsInTys [] = emptyVarSet +allTyVarsInTys (ty:tys) = allTyVarsInTy ty `unionVarSet` allTyVarsInTys tys + +allTyVarsInTy :: Type -> VarSet +allTyVarsInTy = go + where + go (TyVarTy tv) = unitVarSet tv + go (AppTy ty1 ty2) = (go ty1) `unionVarSet` (go ty2) + go (TyConApp _ tys) = allTyVarsInTys tys + go (FunTy ty1 ty2) = (go ty1) `unionVarSet` (go ty2) + go (ForAllTy tv ty) = (go (tyVarKind tv)) `unionVarSet` + unitVarSet tv `unionVarSet` + (go ty) -- don't remove tv + go (LitTy {}) = emptyVarSet + +\end{code}
\ No newline at end of file diff --git a/compiler/types/OptCoercion.lhs b/compiler/types/OptCoercion.lhs index d3dd2a4697..03175f33f9 100644 --- a/compiler/types/OptCoercion.lhs +++ b/compiler/types/OptCoercion.lhs @@ -21,6 +21,7 @@ import TyCon import CoAxiom import Var import VarSet +import FamInstEnv ( flattenTys ) import VarEnv import StaticFlags ( opt_NoOptCoercion ) import Outputable @@ -393,14 +394,18 @@ checkAxInstCo (AxiomInstCo ax ind cos) incomps = coAxBranchIncomps branch tys = map (pFst . coercionKind) cos subst = zipOpenTvSubst tvs tys - lhs' = Type.substTys subst (coAxBranchLHS branch) in - check_no_conflict lhs' incomps + target = Type.substTys subst (coAxBranchLHS branch) + in_scope = mkInScopeSet $ + unionVarSets (map (tyVarsOfTypes . coAxBranchLHS) incomps) + flattened_target = flattenTys in_scope target in + check_no_conflict flattened_target incomps where check_no_conflict :: [Type] -> [CoAxBranch] -> Maybe CoAxBranch check_no_conflict _ [] = Nothing - check_no_conflict lhs' (b@CoAxBranch { cab_lhs = lhs_incomp } : rest) - | SurelyApart <- tcApartTys instanceBindFun lhs' lhs_incomp - = check_no_conflict lhs' rest + check_no_conflict flat (b@CoAxBranch { cab_lhs = lhs_incomp } : rest) + -- See Note [Apartness] in FamInstEnv + | SurelyApart <- tcUnifyTysFG instanceBindFun flat lhs_incomp + = check_no_conflict flat rest | otherwise = Just b checkAxInstCo _ = Nothing diff --git a/compiler/types/Unify.lhs b/compiler/types/Unify.lhs index 34bc4b5ec4..35f4ef5576 100644 --- a/compiler/types/Unify.lhs +++ b/compiler/types/Unify.lhs @@ -25,7 +25,7 @@ module Unify ( tcUnifyTys, BindFlag(..), niFixTvSubst, niSubstTvSet, - UnifyResultM(..), UnifyResult, tcApartTys + UnifyResultM(..), UnifyResult, tcUnifyTysFG ) where @@ -356,102 +356,32 @@ typesCantMatch prs = any (\(s,t) -> cant_match s t) prs %* * %************************************************************************ -Note [Apartness] -~~~~~~~~~~~~~~~~ +Note [Fine-grained unification] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Do the types (x, x) and ([y], y) unify? The answer is seemingly "no" -- +no substitution to finite types makes these match. But, a substitution to +*infinite* types can unify these two types: [x |-> [[[...]]], y |-> [[[...]]] ]. +Why do we care? Consider these two type family instances: -Definition: Two types t1 and t2 are /apart/ when, for all well-kinded -substitutions Q, there exists no safe coercion witnessing the equality -between Q(t1) and Q(t2). +type instance F x x = Int +type instance F [y] y = Bool -- Every two types that unify are not apart. +If we also have -- A type family application (i.e. TyConApp F tys) might or might not be - apart from any given type; it depends on the instances available. Because - we can't know what instances are available (as they might be included in - another module), we conclude that a type family application is *maybe apart* - from any other type. +type instance Looper = [Looper] -Note [Unification and apartness] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -The workhorse function behind unification actually is testing for apartness, -not unification. (See [Apartness], above.) There are three -possibilities here: +then the instances potentially overlap. The solution is to use unification +over infinite terms. This is possible (see [1] for lots of gory details), but +a full algorithm is a little more power than we need. Instead, we make a +conservative approximation and just omit the occurs check. - - two types might be Unifiable, which means a substitution can be found between - them, +[1]: http://research.microsoft.com/en-us/um/people/simonpj/papers/ext-f/axioms-extended.pdf - Example: (Either a Int) and (Either Bool b) are Unifiable, with - [a |-> Bool, b |-> Int] +tcUnifyTys considers an occurs-check problem as the same as general unification +failure. - - they might be MaybeApart, which means that we're not sure, but a substitution - cannot be found - - Example: Int and F a (for some type family F) are MaybeApart - - - they might be SurelyApart, in which case we can guarantee that they never - unify - - Example: (Either Int a) and (Either Bool b) are SurelyApart - -In the Unifiable case, the apartness finding function also returns a -substitution, which we can then use to unify the types. It is necessary for -the unification algorithm to depend on the apartness algorithm, because -apartness is finer-grained than unification. - -Note [Unifying with type families] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -We wish to separate out the case where unification fails on a type family -from other unification failure. What does "fail on a type family" look like? -According to the TyConApp invariant, a type family application must always -be in a TyConApp. This TyConApp may not be buried within the left-hand-side -of an AppTy. - -Furthermore, we wish to proceed with unification if we are unifying -(F a b) with (F Int Bool). Here, unification should succeed with -[a |-> Int, b |-> Bool]. So, here is what we do: - - - If we are unifying two TyConApps, check the heads for equality and - proceed iff they are equal. - - - Otherwise, if either (or both) type is a TyConApp headed by a type family, - we know they cannot fully unify. But, they might unify later, depending - on the type family. So, we return "maybeApart". - -Note that we never want to unify, say, (a Int) with (F Int), because doing so -leads to an unsaturated type family. So, we don't have to worry about any -unification between type families and AppTys. - -But wait! There is one more possibility. What about nullary type families? -If G is a nullary type family, we *do* want to unify (a) with (G). This is -handled in uVar, which is triggered before we look at TyConApps. Ah. All is -well again. - -Note [Apartness with skolems] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -If we discover that two types unify if and only if a skolem variable is -substituted, we can't properly unify the types. But, that skolem variable -may later be instantiated with a unifyable type. So, we return maybeApart -in these cases. - -Note [Apartness and the occurs check] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Are the types (x, x) and ([y], y) apart? The answer is "maybe". They clearly -don't unify, but they also don't have a direct conflict. This is somewhere -between unifiable and surely apart, so we use maybeApart. - -It turns out that this whole area is rather delicate, as regards soundness of -type families. Specifically, we need to disallow the two instances - - F x x = Int - F [y] y = Bool - -because if we have - - Looper = [Looper] - -then the instances potentially overlap. A simple unification doesn't eliminate -the overlap, so we use an apartness check with this special handling of the -occurs check. +tcUnifyTysFG ("fine-grained") returns one of three results: success, occurs-check +failure ("MaybeApart"), or general failure ("SurelyApart"). Note [The substitution in MaybeApart] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -467,6 +397,12 @@ Int is SurelyApart from Bool, and therefore the types are apart. This has practical consequences for the ability for closed type family applications to reduce. See test case indexed-types/should_compile/Overlap14. +Note [Unifying with skolems] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +If we discover that two types unify if and only if a skolem variable is +substituted, we can't properly unify the types. But, that skolem variable +may later be instantiated with a unifyable type. So, we return maybeApart +in these cases. \begin{code} -- See Note [Unification and apartness] @@ -477,7 +413,7 @@ tcUnifyTys :: (TyVar -> BindFlag) -- second call to tcUnifyTys in FunDeps.checkClsFD -- tcUnifyTys bind_fn tys1 tys2 - | Unifiable subst <- tcApartTys bind_fn tys1 tys2 + | Unifiable subst <- tcUnifyTysFG bind_fn tys1 tys2 = Just subst | otherwise = Nothing @@ -491,10 +427,11 @@ data UnifyResultM a = Unifiable a -- the subst that unifies the types -- See Note [The substitution in MaybeApart] | SurelyApart -tcApartTys :: (TyVar -> BindFlag) - -> [Type] -> [Type] - -> UnifyResult -tcApartTys bind_fn tys1 tys2 +-- See Note [Fine-grained unification] +tcUnifyTysFG :: (TyVar -> BindFlag) + -> [Type] -> [Type] + -> UnifyResult +tcUnifyTysFG bind_fn tys1 tys2 = initUM bind_fn $ do { subst <- unifyList emptyTvSubstEnv tys1 tys2 @@ -566,14 +503,8 @@ unify subst ty1 ty2 | Just ty1' <- tcView ty1 = unify subst ty1' ty2 unify subst ty1 ty2 | Just ty2' <- tcView ty2 = unify subst ty1 ty2' unify subst (TyConApp tyc1 tys1) (TyConApp tyc2 tys2) - | tyc1 == tyc2 = unify_tys subst tys1 tys2 - | isSynFamilyTyCon tyc1 || isSynFamilyTyCon tyc2 = maybeApart subst - --- See Note [Unifying with type families] -unify subst (TyConApp tyc _) _ - | isSynFamilyTyCon tyc = maybeApart subst -unify subst _ (TyConApp tyc _) - | isSynFamilyTyCon tyc = maybeApart subst + | tyc1 == tyc2 + = unify_tys subst tys1 tys2 unify subst (FunTy ty1a ty1b) (FunTy ty2a ty2b) = do { subst' <- unify subst ty1a ty2a @@ -661,14 +592,14 @@ uUnrefined subst tv1 ty2 (TyVarTy tv2) ; b2 <- tvBindFlag tv2 ; let ty1 = TyVarTy tv1 ; case (b1, b2) of - (Skolem, Skolem) -> maybeApart subst' -- See Note [Apartness with skolems] + (Skolem, Skolem) -> maybeApart subst' -- See Note [Unification with skolems] (BindMe, _) -> return (extendVarEnv subst' tv1 ty2) (_, BindMe) -> return (extendVarEnv subst' tv2 ty1) } uUnrefined subst tv1 ty2 ty2' -- ty2 is not a type variable | tv1 `elemVarSet` niSubstTvSet subst (tyVarsOfType ty2') = maybeApart subst -- Occurs check - -- See Note [Apartness and the occurs check] + -- See Note [Fine-grained unification] | otherwise = do { subst' <- unify subst k1 k2 ; bindTv subst' tv1 ty2 } -- Bind tyvar to the synonym if poss @@ -680,7 +611,7 @@ bindTv :: TvSubstEnv -> TyVar -> Type -> UM TvSubstEnv bindTv subst tv ty -- ty is not a type variable = do { b <- tvBindFlag tv ; case b of - Skolem -> maybeApart subst -- See Note [Apartness with skolems] + Skolem -> maybeApart subst -- See Note [Unification with skolems] BindMe -> return $ extendVarEnv subst tv ty } \end{code} diff --git a/docs/core-spec/core-spec.mng b/docs/core-spec/core-spec.mng index 40560df1ec..246be067fc 100644 --- a/docs/core-spec/core-spec.mng +++ b/docs/core-spec/core-spec.mng @@ -29,7 +29,7 @@ System FC, as implemented in GHC\footnote{This document was originally prepared by Richard Eisenberg (\texttt{eir@cis.upenn.edu}), but it should be maintained by anyone who edits the functions or data structures mentioned in this file. Please feel free to contact Richard for more information.}\\ -\Large 8 July, 2013 +\Large 2 August, 2013 \end{center} \section{Introduction} @@ -339,10 +339,14 @@ check for compatibility here. \ottdefncheckXXnoXXconflict{} -The judgment $[[apart]]$ checks to see whether two lists of types are surely apart. -It checks to see if \coderef{types/Unify.lhs}{tcApartTys} returns \texttt{SurelyApart}. -Two types are apart if neither type is a type family application and if they do not -unify. +The judgment $[[apart]]$ checks to see whether two lists of types are surely +apart. $[[apart( </ ti // i />, </ si // i /> )]]$, where $[[ </ ti // i /> +]]$ is a list of types and $[[ </ si // i /> ]]$ is a list of type +\emph{patterns} (as in a type family equation), first flattens the $[[ </ ti + // i /> ]]$ using \coderef{types/FamInstEnv.lhs}{flattenTys} and then checks to +see if \coderef{types/Unify.lhs}{tcUnifyTysFG} returns \texttt{SurelyApart}. +Flattening takes all type family applications and replaces them with fresh variables, +taking care to map identical type family applications to the same fresh variable. The algorithm $[[unify]]$ is implemented in \coderef{types/Unify.lhs}{tcUnifyTys}. It performs a standard unification, returning a substitution upon success. diff --git a/docs/core-spec/core-spec.pdf b/docs/core-spec/core-spec.pdf Binary files differindex 11f52d6476..180d9bed78 100644 --- a/docs/core-spec/core-spec.pdf +++ b/docs/core-spec/core-spec.pdf |