Commit bd0ab6c2 authored by eir@cis.upenn.edu's avatar eir@cis.upenn.edu

Fix Trac #8020.

The solution is to use a different notion of apartness. See
http://research.microsoft.com/en-us/um/people/simonpj/papers/ext-f/axioms-extended.pdf
for the gory details. Some comments are also in Notes [Compatibility]
and [Apartness] in FamInstEnv.
parent abb3a9fa
......@@ -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
......
......@@ -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)))
......
......@@ -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
......@@ -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
......
......@@ -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}
......
......@@ -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.
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment