Commit 027e6be2 authored by simonpj@microsoft.com's avatar simonpj@microsoft.com

Robustify lookupFamInstEnv, plus some refactoring

This patch deals with the following remark

     Suppose we have
            type family T a :: * -> *
            type instance T Int = []

     and now we encounter the type (T Int Bool).  If we call
     lookupFamInstEnv on (T Int Bool) we'll fail, because T has arity 1.
     Indeed, I *think* it's a precondition of lookupFamInstEnv that the
     supplied types exactly match the arity of the type function.  But
     that precondition is neither stated, nor is there an assertion to
     check it.

With this patch, lookupFamInstEnv can take "extra" type arguments in
the over-saturated case, and does the Right Thing.

There was a nearly-identical function lookupFamInstEnvUnify, which
required the precisely analogous change, so I took the opportunity 
to combine the two into one function, so that bugs can be fixed in one
place.  This was a bit harder than I expected, but I think the result
is ok.  The conflict-decision function moves from FamInst to FamInstEnv.
Net lines code decreases, although there are more comments.

parent 27759873
......@@ -11,7 +11,6 @@ import TcMType
import TcType
import TcRnMonad
import TyCon
import Type
import Name
import Module
import SrcLoc
......@@ -178,38 +177,13 @@ checkForConflicts inst_envs famInst
-- (since we do unification).
-- We use tcInstSkolType because we don't want to allocate
-- fresh *meta* type variables.
; let { tycon = famInstTyCon famInst
; ty = case tyConFamInst_maybe tycon of
Nothing -> panic "FamInst.checkForConflicts"
Just (tc, tys) -> tc `mkTyConApp` tys
}
; (_, _, tau') <- tcInstSkolType FamInstSkol ty
; let (fam, tys') = tcSplitTyConApp tau'
; let { matches = lookupFamInstEnvUnify inst_envs fam tys'
; conflicts = [ conflictingFamInst
| match@((conflictingFamInst, _), _) <- matches
, conflicting tycon match
]
}
; skol_tvs <- tcInstSkolTyVars FamInstSkol (tyConTyVars (famInstTyCon famInst))
; let conflicts = lookupFamInstEnvConflicts inst_envs famInst skol_tvs
; unless (null conflicts) $
conflictInstErr famInst (head conflicts)
conflictInstErr famInst (fst (head conflicts))
}
where
-- - In the case of data family instances, any overlap is fundamentally a
-- conflict (as these instances imply injective type mappings).
-- - In the case of type family instances, overlap is admitted as long as
-- the right-hand sides of the overlapping rules coincide under the
-- overlap substitution. We require that they are syntactically equal;
-- anything else would be difficult to test for at this stage.
conflicting tycon1 ((famInst2, _), subst)
| isAlgTyCon tycon1 = True
| otherwise = not (rhs1 `tcEqType` rhs2)
where
tycon2 = famInstTyCon famInst2
rhs1 = substTy subst $ synTyConType tycon1
rhs2 = substTy subst $ synTyConType tycon2
conflictInstErr :: FamInst -> FamInst -> TcRn ()
conflictInstErr famInst conflictingFamInst
......
......@@ -14,7 +14,7 @@ module FamInstEnv (
extendFamInstEnv, extendFamInstEnvList,
famInstEnvElts, familyInstances,
lookupFamInstEnv, lookupFamInstEnvUnify,
lookupFamInstEnv, lookupFamInstEnvConflicts,
-- Normalisation
topNormaliseType
......@@ -218,38 +218,97 @@ desugared to
we return the matching instance '(FamInst{.., fi_tycon = :R42T}, Int)'.
Note [Over-saturated matches]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
It's ok to look up an over-saturated type constructor. E.g.
type family F a :: * -> *
type instance F (a,b) = Either (a->b)
The type instance gives rise to a newtype TyCon (at a higher kind
which you can't do in Haskell!):
newtype FPair a b = FP (Either (a->b))
\begin{code}
type FamInstMatch = (FamInst, [Type]) -- Matching type instance
-- See Note [Over-saturated matches]
Then looking up (F (Int,Bool) Char) will return a FamInstMatch
(FPair, [Int,Bool,Char])
lookupFamInstEnv
:: FamInstEnvs
-> TyCon -> [Type] -- What we are looking for
-> [FamInstMatch] -- Successful matches
lookupFamInstEnv
= lookup_fam_inst_env match
where
match _ tpl_tvs tpl_tys tys = tcMatchTys tpl_tvs tpl_tys tys
lookupFamInstEnvConflicts
:: FamInstEnvs
-> FamInst -- Putative new instance
-> [TyVar] -- Unique tyvars, matching arity of FamInst
-> [FamInstMatch] -- Conflicting matches
-- E.g. when we are about to add
-- f : type instance F [a] = a->a
-- we do (lookupFamInstConflicts f [b])
-- to find conflicting matches
-- The skolem tyvars are needed because we don't have a
-- unique supply to hand
lookupFamInstEnvConflicts envs fam_inst skol_tvs
= lookup_fam_inst_env my_unify envs fam tys'
where
inst_tycon = famInstTyCon fam_inst
(fam, tys) = expectJust "FamInstEnv.lookuFamInstEnvConflicts"
(tyConFamInst_maybe inst_tycon)
skol_tys = mkTyVarTys skol_tvs
tys' = substTys (zipTopTvSubst (tyConTyVars inst_tycon) skol_tys) tys
-- In example above, fam tys' = F [b]
my_unify old_fam_inst tpl_tvs tpl_tys match_tys
= ASSERT2( tyVarsOfTypes tys `disjointVarSet` tpl_tvs,
(ppr fam <+> ppr tys) $$
(ppr tpl_tvs <+> ppr tpl_tys) )
-- Unification will break badly if the variables overlap
-- They shouldn't because we allocate separate uniques for them
case tcUnifyTys instanceBindFun tpl_tys match_tys of
Just subst | conflicting old_fam_inst subst -> Just subst
_other -> Nothing
-- - In the case of data family instances, any overlap is fundamentally a
-- conflict (as these instances imply injective type mappings).
-- - In the case of type family instances, overlap is admitted as long as
-- the right-hand sides of the overlapping rules coincide under the
-- overlap substitution. We require that they are syntactically equal;
-- anything else would be difficult to test for at this stage.
conflicting old_fam_inst subst
| isAlgTyCon fam = True
| otherwise = not (old_rhs `tcEqType` new_rhs)
where
old_tycon = famInstTyCon old_fam_inst
old_rhs = mkTyConApp old_tycon (substTyVars subst (tyConTyVars old_tycon))
new_rhs = mkTyConApp inst_tycon (substTyVars subst skol_tvs)
\end{code}
The "extra" type argument [Char] just stays on the end.
While @lookupFamInstEnv@ uses a one-way match, the next function
@lookupFamInstEnvUnify@ uses two-way matching (ie, unification). This is
needed to check for overlapping instances.
For class instances, these two variants of lookup are combined into one
function (cf, @InstEnv@). We don't do that for family instances as the
results of matching and unification are used in two different contexts.
Moreover, matching is the wildly more frequently used operation in the case of
indexed synonyms and we don't want to slow that down by needless unification.
\begin{code}
type FamInstMatch = (FamInst, [Type]) -- Matching type instance
-- See Note [Over-saturated matches]
lookupFamInstEnv :: FamInstEnvs
-> TyCon -> [Type] -- What we are looking for
-> [FamInstMatch] -- Successful matches
lookupFamInstEnv (pkg_ie, home_ie) fam tys
------------------------------------------------------------
-- Might be a one-way match or a unifier
type MatchFun = FamInst -- The FamInst template
-> TyVarSet -> [Type] -- fi_tvs, fi_tys of that FamInst
-> [Type] -- Target to match against
-> Maybe TvSubst
lookup_fam_inst_env -- The worker, local to this module
:: MatchFun
-> FamInstEnvs
-> TyCon -> [Type] -- What we are looking for
-> [FamInstMatch] -- Successful matches
lookup_fam_inst_env match_fun (pkg_ie, home_ie) fam tys
| not (isOpenTyCon fam)
= []
| otherwise
= ASSERT( n_tys >= arity ) -- Family type applications must be saturated
home_matches ++ pkg_matches
where
rough_tcs = roughMatchTcs tys
all_tvs = all isNothing rough_tcs
home_matches = lookup home_ie
pkg_matches = lookup pkg_ie
......@@ -262,6 +321,10 @@ lookupFamInstEnv (pkg_ie, home_ie) fam tys
| otherwise = (tys, \res_tys -> res_tys)
-- The second case is the common one, hence functional representation
--------------
rough_tcs = roughMatchTcs match_tys
all_tvs = all isNothing rough_tcs
--------------
lookup env = case lookupUFM env fam of
Nothing -> [] -- No instances for this class
......@@ -282,7 +345,7 @@ lookupFamInstEnv (pkg_ie, home_ie) fam tys
= find rest
-- Proper check
| Just subst <- tcMatchTys tpl_tvs tpl_tys match_tys
| Just subst <- match_fun item tpl_tvs tpl_tys match_tys
= (item, add_extra_tys $ substTyVars subst (tyConTyVars tycon)) : find rest
-- No match => try next
......@@ -290,62 +353,23 @@ lookupFamInstEnv (pkg_ie, home_ie) fam tys
= find rest
\end{code}
While @lookupFamInstEnv@ uses a one-way match, the next function
@lookupFamInstEnvUnify@ uses two-way matching (ie, unification). This is
needed to check for overlapping instances.
Note [Over-saturated matches]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
It's ok to look up an over-saturated type constructor. E.g.
type family F a :: * -> *
type instance F (a,b) = Either (a->b)
For class instances, these two variants of lookup are combined into one
function (cf, @InstEnv@). We don't do that for family instances as the
results of matching and unification are used in two different contexts.
Moreover, matching is the wildly more frequently used operation in the case of
indexed synonyms and we don't want to slow that down by needless unification.
The type instance gives rise to a newtype TyCon (at a higher kind
which you can't do in Haskell!):
newtype FPair a b = FP (Either (a->b))
\begin{code}
lookupFamInstEnvUnify :: (FamInstEnv, FamInstEnv) -> TyCon -> [Type]
-> [(FamInstMatch, TvSubst)]
lookupFamInstEnvUnify (pkg_ie, home_ie) fam tys
| not (isOpenTyCon fam)
= []
| otherwise
= home_matches ++ pkg_matches
where
rough_tcs = roughMatchTcs tys
all_tvs = all isNothing rough_tcs
home_matches = lookup home_ie
pkg_matches = lookup pkg_ie
Then looking up (F (Int,Bool) Char) will return a FamInstMatch
(FPair, [Int,Bool,Char])
The "extra" type argument [Char] just stays on the end.
--------------
lookup env = case lookupUFM env fam of
Nothing -> [] -- No instances for this class
Just (FamIE insts has_tv_insts)
-- Short cut for common case:
-- The thing we are looking up is of form (C a
-- b c), and the FamIE has no instances of
-- that form, so don't bother to search
| all_tvs && not has_tv_insts -> []
| otherwise -> find insts
--------------
find [] = []
find (item@(FamInst { fi_tcs = mb_tcs, fi_tvs = tpl_tvs,
fi_tys = tpl_tys, fi_tycon = tycon }) : rest)
-- Fast check for no match, uses the "rough match" fields
| instanceCantMatch rough_tcs mb_tcs
= find rest
| otherwise
= ASSERT2( tyVarsOfTypes tys `disjointVarSet` tpl_tvs,
(ppr fam <+> ppr tys <+> ppr all_tvs) $$
(ppr tycon <+> ppr tpl_tvs <+> ppr tpl_tys)
)
-- Unification will break badly if the variables overlap
-- They shouldn't because we allocate separate uniques for them
case tcUnifyTys instanceBindFun tpl_tys tys of
Just subst -> let rep_tys = substTyVars subst (tyConTyVars tycon)
in
((item, rep_tys), subst) : find rest
Nothing -> find rest
\end{code}
%************************************************************************
%* *
......
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