[commit: ghc] overlapping-tyfams: Fixing merge errors. Checkpoint on manual update. (c04be8e)
Richard Eisenberg
eir at cis.upenn.edu
Fri Jun 21 15:17:24 CEST 2013
Repository : http://darcs.haskell.org/ghc.git/
On branch : overlapping-tyfams
https://github.com/ghc/ghc/commit/c04be8ef8de95349c202b3ce1fd50047651d2fe7
>---------------------------------------------------------------
commit c04be8ef8de95349c202b3ce1fd50047651d2fe7
Author: Richard Eisenberg <eir at cis.upenn.edu>
Date: Thu Jun 20 22:42:44 2013 +0100
Fixing merge errors. Checkpoint on manual update.
>---------------------------------------------------------------
compiler/typecheck/TcDeriv.lhs | 4 +--
compiler/types/FamInstEnv.lhs | 18 +++++------
docs/users_guide/glasgow_exts.xml | 65 +++++++++++++++++++++++----------------
3 files changed, 47 insertions(+), 40 deletions(-)
diff --git a/compiler/typecheck/TcDeriv.lhs b/compiler/typecheck/TcDeriv.lhs
index bd68201..21e2bbb 100644
--- a/compiler/typecheck/TcDeriv.lhs
+++ b/compiler/typecheck/TcDeriv.lhs
@@ -743,10 +743,8 @@ mkEqnHelp orig tvs cls cls_tys tc_app mtheta
Nothing -> bale_out (ptext (sLit "No family instance for")
<+> quotes (pprTypeApp tycon tys))
Just (FamInstMatch { fim_instance = famInst
- , fim_index = index
, fim_tys = tys })
- -> ASSERT( index == 0 )
- let tycon' = dataFamInstRepTyCon famInst
+ -> let tycon' = dataFamInstRepTyCon famInst
in return (tycon', tys) }
\end{code}
diff --git a/compiler/types/FamInstEnv.lhs b/compiler/types/FamInstEnv.lhs
index b1f26de..e7e1702 100644
--- a/compiler/types/FamInstEnv.lhs
+++ b/compiler/types/FamInstEnv.lhs
@@ -336,7 +336,7 @@ extendFamInstEnvList :: FamInstEnv -> [FamInst] -> FamInstEnv
extendFamInstEnvList inst_env fis = foldl extendFamInstEnv inst_env fis
extendFamInstEnv :: FamInstEnv -> FamInst -> FamInstEnv
-extendFamInstEnv inst_env ins_item@(FamInst {fi_fam = cls_nm, fi_tcs = mb_tcs})
+extendFamInstEnv inst_env ins_item@(FamInst {fi_fam = cls_nm})
= addToUFM_C add inst_env cls_nm (FamIE [ins_item])
where
add (FamIE items) _ = FamIE (ins_item:items)
@@ -640,7 +640,7 @@ lookup_fam_inst_env' -- The worker, local to this module
lookup_fam_inst_env' match_fun _one_sided ie fam tys
| isOpenFamilyTyCon fam
, Just (FamIE insts) <- lookupUFM ie fam
- = find match_fun tys insts -- The common case
+ = find insts -- The common case
| otherwise = []
where
@@ -662,11 +662,11 @@ lookup_fam_inst_env' match_fun _one_sided ie fam tys
= find rest
-- Precondition: the tycon is saturated (or over-saturated)
- where
- -- Deal with over-saturation
- -- See Note [Over-saturated matches]
- (match_tys1, match_tys2) = splitAtList mb_tcs match_tys
- rough_tcs = roughMatchTcs match_tys1
+
+ -- Deal with over-saturation
+ -- See Note [Over-saturated matches]
+ (match_tys1, match_tys2) = splitAt (tyConArity fam) tys
+ rough_tcs = roughMatchTcs match_tys1
lookup_fam_inst_env -- The worker, local to this module
:: MatchFun
@@ -828,10 +828,6 @@ topNormaliseType env ty
-- are correctly top-normalised
, not (isReflCo co)
= add_co co rec_nts ty
- where
- nt_rhs = newTyConInstRhs tc tys
- rec_nts' | isRecursiveTyCon tc = tc:rec_nts
- | otherwise = rec_nts
go _ _ = Nothing
diff --git a/docs/users_guide/glasgow_exts.xml b/docs/users_guide/glasgow_exts.xml
index 7486be7..fb9574c 100644
--- a/docs/users_guide/glasgow_exts.xml
+++ b/docs/users_guide/glasgow_exts.xml
@@ -5193,6 +5193,7 @@ type family F a where
</sect3>
<sect3 id="type-family-examples">
+ <title>Type family examples</title>
<para>
Here are some examples of admissible and illegal type
instances:
@@ -5203,13 +5204,11 @@ type instance F String = Char -- OK!
type instance F (F a) = a -- WRONG: type parameter mentions a type family
type instance F (forall a. (a, b)) = b -- WRONG: a forall type appears in a type parameter
type instance F Float = forall a.a -- WRONG: right-hand side may not be a forall type
-type instance where -- OK!
- F (Maybe Int) = Int
- F (Maybe Bool) = Bool
- F (Maybe a) = String
-type instance where -- WRONG: conflicts with earlier instances (see below)
- F Int = Float
- F a = [a]
+type family H a where -- OK!
+ H Int = Int
+ H Bool = Bool
+ H a = String
+type instance H Char = Char -- WRONG: cannot have instances of closed family
type family G a b :: * -> *
type instance G Int = (,) -- WRONG: must be two type parameters
@@ -5218,35 +5217,49 @@ type instance G Int Char Float = Double -- WRONG: must be two type parameters
</para>
</sect3>
<sect3 id="type-family-overlap">
- <title>Overlap of type synonym instances</title>
+ <title>Compatibility and apartness of type family equations</title>
<para>
- The unbranched instance declarations of a type family used in a single
- program may only overlap if the right-hand sides of the overlapping
- instances coincide for the overlapping types. More formally, two
- instance declarations overlap if there is a substitution that makes
- the left-hand sides of the instances syntactically the same. Whenever
- that is the case, if the instances are unbranched, the right-hand
- sides of the instances must also be syntactically equal under the same
- substitution. This condition is independent of whether the type family
- is associated or not, and it is not only a matter of consistency, but
- one of type safety. Branched instances are not permitted to overlap
- with any other instances, branched or unbranched.
+ There must be some restrictions on the equations of type families, lest
+ we define an ambiguous rewrite system. So, equations of open type families
+ are restricted to be <firstterm>compatible</firstterm>. Two type patterns
+ are compatible if
+<orderedlist>
+<listitem><para>all corresponding types in the patterns are <firstterm>apart</firstterm>, or</para></listitem>
+<listitem><para>the two patterns unify producing a substitution, and the right-hand sides are equal under that substitution.</para></listitem>
+</orderedlist>
+ Two types are considered <firstterm>apart</firstterm> if, for all possible
+ substitutions, the types cannot reduce to a common reduct.
</para>
+
<para>
- Here are two example to illustrate the condition under which overlap
- is permitted.
+ The first clause of "compatible" is the more straightforward one. It says
+ that the patterns of two distinct type family instances cannot overlap.
+ For example, the following is disallowed:
+<programlisting>
+type instance F Int = Bool
+type instance F Int = Char
+</programlisting>
+ The second clause is a little more interesting. It says that two
+ overlapping type family instances are allowed if the right-hand
+ sides coincide in the region of overlap. Some examples help here:
<programlisting>
type instance F (a, Int) = [a]
type instance F (Int, b) = [b] -- overlap permitted
type instance G (a, Int) = [a]
type instance G (Char, a) = [a] -- ILLEGAL overlap, as [Char] /= [Int]
-
-type instance H Int = Int
-type instance where -- ILLEGAL overlap, as branched instances may not overlap
- H a = a
</programlisting>
- </para>
+ Note that this compatibility condition is independent of whether the type family
+ is associated or not, and it is not only a matter of consistency, but
+ one of type safety. </para>
+
+ <para>
+ The definition for "compatible" uses a notion of "apart", whose definition
+ in turn relies on type family reduction. This condition of "apartness", as
+ stated, is impossible to check, so we use this conservative approximation:
+ two types are considered to be apart when the two types cannot be unified,
+ even by a potentially infinite unifier.
+
<para> However see <xref linkend="ghci-decls"/> for the overlap rules in GHCi.</para>
</sect3>
More information about the ghc-commits
mailing list