Commit fd46acf1 authored by Simon Peyton Jones's avatar Simon Peyton Jones

Fix reduceTyFamApp_maybe

This function previously would expand *data* families even when it was asked
for a *Nominal* coercion.  This patch fixes it, and adds comments.
parent bdbb595c
......@@ -361,7 +361,8 @@ 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})
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)
......@@ -789,18 +790,33 @@ The lookupFamInstEnv function does a nice job for *open* type families,
but we also need to handle closed ones when normalising a type:
\begin{code}
reduceTyFamApp_maybe :: FamInstEnvs -> Role -> TyCon -> [Type] -> Maybe (Coercion, Type)
reduceTyFamApp_maybe :: FamInstEnvs
-> Role -- Desired role of result coercion
-> TyCon -> [Type]
-> Maybe (Coercion, Type)
-- Attempt to do a *one-step* reduction of a type-family application
-- but *not* newtypes
-- Works on type-synonym families always; data-families only if
-- the role we seek is representational
-- It first normalises the type arguments, wrt functions but *not* newtypes,
-- to be sure that nested calls like
-- F (G Int)
-- are correctly reduced
-- to be sure that nested calls like
-- F (G Int)
-- are correctly reduced
--
-- The TyCon can be oversaturated.
-- Works on both open and closed families
reduceTyFamApp_maybe envs role tc tys
| isOpenFamilyTyCon tc
| Phantom <- role
= Nothing
| case role of
Representational -> isOpenFamilyTyCon tc
_ -> isOpenSynFamilyTyCon tc
-- If we seek a representational coercion
-- (e.g. the call in topNormaliseType_maybe) then we can
-- unwrap data families as well as type-synonym families;
-- otherwise only type-synonym families
, [FamInstMatch { fim_instance = fam_inst
, fim_tys = inst_tys }] <- lookupFamInstEnv envs tc ntys
= let ax = famInstAxiom fam_inst
......@@ -927,12 +943,18 @@ topNormaliseType_maybe env ty
---------------
normaliseTcApp :: FamInstEnvs -> Role -> TyCon -> [Type] -> (Coercion, Type)
-- See comments on normaliseType for the arguments of this function
normaliseTcApp env role tc tys
| isTypeSynonymTyCon tc
, (co1, ntys) <- normaliseTcArgs env role tc tys
, Just (tenv, rhs, ntys') <- tcExpandTyCon_maybe tc ntys
, (co2, ninst_rhs) <- normaliseType env role (Type.substTy (mkTopTvSubst tenv) rhs)
= if isReflCo co2 then (co1, mkTyConApp tc ntys)
else (co1 `mkTransCo` co2, mkAppTys ninst_rhs ntys')
| Just (first_co, ty') <- reduceTyFamApp_maybe env role tc tys
= let -- A reduction is possible
(rest_co,nty) = normaliseType env role ty'
in
(first_co `mkTransCo` rest_co, nty)
, (rest_co,nty) <- normaliseType env role ty'
= (first_co `mkTransCo` rest_co, nty)
| otherwise -- No unique matching family instance exists;
-- we do not do anything
......@@ -958,10 +980,10 @@ normaliseType :: FamInstEnvs -- environment with family instances
-> (Coercion, Type) -- (coercion,new type), where
-- co :: old-type ~ new_type
-- Normalise the input type, by eliminating *all* type-function redexes
-- but *not* newtypes (which are visible to the programmer)
-- Returns with Refl if nothing happens
-- Try to not to disturb type syonyms if possible
normaliseType env role ty
| Just ty' <- coreView ty = normaliseType env role ty'
normaliseType env role (TyConApp tc tys)
= normaliseTcApp env role tc tys
normaliseType _env role ty@(LitTy {}) = (Refl role ty, ty)
......
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