[commit: ghc] wip/new-flatten-skolems-Oct14: Fix reduceTyFamApp_maybe (ad9c4c9)

[git at git.haskell.org]

Repository : ssh://git@git.haskell.org/ghc

On branch  : wip/new-flatten-skolems-Oct14
Link       : http://ghc.haskell.org/trac/ghc/changeset/ad9c4c9f98edc4d24098c4441c1d9f8feede13ae/ghc

>---------------------------------------------------------------

commit ad9c4c9f98edc4d24098c4441c1d9f8feede13ae
Author: Simon Peyton Jones <simonpj at microsoft.com>
Date:   Wed Oct 29 16:30:05 2014 +0000

    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.


>---------------------------------------------------------------

ad9c4c9f98edc4d24098c4441c1d9f8feede13ae
 compiler/types/FamInstEnv.lhs | 46 ++++++++++++++++++++++++++++++++-----------
 1 file changed, 34 insertions(+), 12 deletions(-)

diff --git a/compiler/types/FamInstEnv.lhs b/compiler/types/FamInstEnv.lhs
index 7fe35ff..bc21e2e 100644
--- a/compiler/types/FamInstEnv.lhs
+++ b/compiler/types/FamInstEnv.lhs
@@ -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)