[commit: ghc] wip/T8503: Extend Coercible to newtype instances (ed526c3)

[git at git.haskell.org]

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

On branch  : wip/T8503
Link       : http://ghc.haskell.org/trac/ghc/changeset/ed526c30a19ca24656a9412a26483cb5565d6d1a/ghc

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

commit ed526c30a19ca24656a9412a26483cb5565d6d1a
Author: Joachim Breitner <mail at joachim-breitner.de>
Date:   Fri Nov 22 10:15:01 2013 +0000

    Extend Coercible to newtype instances
    
    This fixes: #8548


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

ed526c30a19ca24656a9412a26483cb5565d6d1a
 compiler/deSugar/DsBinds.lhs      |   12 ++++++------
 compiler/typecheck/TcInteract.lhs |   16 +++++++---------
 compiler/types/FamInstEnv.lhs     |   25 ++++++++++++++++++++++++-
 3 files changed, 37 insertions(+), 16 deletions(-)

diff --git a/compiler/deSugar/DsBinds.lhs b/compiler/deSugar/DsBinds.lhs
index a1ea8b5..2fccba1 100644
--- a/compiler/deSugar/DsBinds.lhs
+++ b/compiler/deSugar/DsBinds.lhs
@@ -44,7 +44,7 @@ import Unique( Unique )
 import Digraph
 
 
-import TyCon      ( isTupleTyCon, tyConDataCons_maybe, unwrapNewTyCon_maybe )
+import TyCon      ( isTupleTyCon, tyConDataCons_maybe )
 import TcEvidence
 import TcType
 import Type
@@ -53,6 +53,7 @@ import TysWiredIn ( eqBoxDataCon, coercibleTyCon, coercibleDataCon, tupleCon )
 import Id
 import Class
 import DataCon	( dataConWorkId )
+import FamInstEnv ( instNewTyConTF_maybe )
 import Name
 import MkId	( seqId )
 import Var
@@ -797,12 +798,11 @@ dsEvTerm (EvCoercible (EvCoercibleTyCon tyCon evs)) = do
 
 dsEvTerm (EvCoercible (EvCoercibleNewType lor tyCon tys v)) = do
   ntEv <- dsEvTerm v
+  famenv <- dsGetFamInstEnvs
+  let Just (_, ntCo) = instNewTyConTF_maybe famenv tyCon tys
   wrapInEqRCase ntEv $ \co -> do
-          return $ mkCoercible $
-                connect lor co $
-                mkUnbranchedAxInstCo Representational coAxiom tys
-  where Just (_, _, coAxiom) = unwrapNewTyCon_maybe tyCon
-        connect CLeft co2 co1 = mkTransCo co1 co2
+          return $ mkCoercible $ connect lor co ntCo
+  where connect CLeft co2 co1 = mkTransCo co1 co2
         connect CRight co2 co1 = mkTransCo co2 (mkSymCo co1)
 
 wrapInEqRCase :: CoreExpr -> (Coercion -> DsM CoreExpr) -> DsM CoreExpr
diff --git a/compiler/typecheck/TcInteract.lhs b/compiler/typecheck/TcInteract.lhs
index aedc6b3..34cbd03 100644
--- a/compiler/typecheck/TcInteract.lhs
+++ b/compiler/typecheck/TcInteract.lhs
@@ -26,6 +26,7 @@ import Name
 import RdrName ( GlobalRdrEnv, lookupGRE_Name, mkRdrQual, is_as,
                  is_decl, Provenance(Imported), gre_prov )
 import FunDeps
+import FamInstEnv ( FamInstEnvs, instNewTyConTF_maybe )
 
 import TcEvidence
 import Outputable
@@ -1845,8 +1846,9 @@ matchClassInst _ clas [ _k, ty1, ty2 ] loc
   | clas == coercibleClass =  do
       traceTcS "matchClassInst for" $ ppr clas <+> ppr ty1 <+> ppr ty2 <+> text "at depth" <+> ppr (ctLocDepth loc)
       rdr_env <- getGlobalRdrEnvTcS
+      famenv <- getFamInstEnvs
       safeMode <- safeLanguageOn `fmap` getDynFlags
-      ev <- getCoercibleInst safeMode rdr_env loc ty1 ty2
+      ev <- getCoercibleInst safeMode famenv rdr_env loc ty1 ty2
       traceTcS "matchClassInst returned" $ ppr ev
       return ev
 
@@ -1932,8 +1934,8 @@ matchClassInst inerts clas tys loc
 
 -- See Note [Coercible Instances]
 -- Changes to this logic should likely be reflected in coercible_msg in TcErrors.
-getCoercibleInst :: Bool -> GlobalRdrEnv -> CtLoc -> TcType -> TcType -> TcS LookupInstResult
-getCoercibleInst safeMode rdr_env loc ty1 ty2
+getCoercibleInst :: Bool -> FamInstEnvs -> GlobalRdrEnv -> CtLoc -> TcType -> TcType -> TcS LookupInstResult
+getCoercibleInst safeMode famenv rdr_env loc ty1 ty2
   | ty1 `eqType` ty2
   = do return $ GenInst []
               $ EvCoercible (EvCoercibleRefl ty1)
@@ -1957,21 +1959,17 @@ getCoercibleInst safeMode rdr_env loc ty1 ty2
               $ EvCoercible (EvCoercibleTyCon tc1 (map snd arg_evs))
 
   | Just (tc,tyArgs) <- splitTyConApp_maybe ty1,
-    Just (_, _, _) <- unwrapNewTyCon_maybe tc,
-    newTyConEtadArity tc <= length tyArgs,
+    Just (concTy, _) <- instNewTyConTF_maybe famenv tc tyArgs,
     dataConsInScope rdr_env tc -- Do noot look at all tyConsOfTyCon
   = do markDataConsAsUsed rdr_env tc
-       let concTy = newTyConInstRhs tc tyArgs
        ct_ev <- requestCoercible loc concTy ty2
        return $ GenInst (freshGoals [ct_ev])
               $ EvCoercible (EvCoercibleNewType CLeft tc tyArgs (getEvTerm ct_ev))
 
   | Just (tc,tyArgs) <- splitTyConApp_maybe ty2,
-    Just (_, _, _) <- unwrapNewTyCon_maybe tc,
-    newTyConEtadArity tc <= length tyArgs,
+    Just (concTy, _) <- instNewTyConTF_maybe famenv tc tyArgs,
     dataConsInScope rdr_env tc -- Do noot look at all tyConsOfTyCon
   = do markDataConsAsUsed rdr_env tc
-       let concTy = newTyConInstRhs tc tyArgs
        ct_ev <- requestCoercible loc ty1 concTy
        return $ GenInst (freshGoals [ct_ev])
               $ EvCoercible (EvCoercibleNewType CRight tc tyArgs (getEvTerm ct_ev))
diff --git a/compiler/types/FamInstEnv.lhs b/compiler/types/FamInstEnv.lhs
index b158da2..adf75bc 100644
--- a/compiler/types/FamInstEnv.lhs
+++ b/compiler/types/FamInstEnv.lhs
@@ -28,7 +28,7 @@ module FamInstEnv (
         isDominatedBy,
 
         -- Normalisation
-        chooseBranch, topNormaliseType, topNormaliseType_maybe,
+        instNewTyConTF_maybe, chooseBranch, topNormaliseType, topNormaliseType_maybe,
         normaliseType, normaliseTcApp,
 
         -- Flattening
@@ -855,6 +855,29 @@ findBranch [] _ _ = Nothing
 %************************************************************************
 
 \begin{code}
+-- | Unwrap a newtype of a newtype intances. This is analogous to
+--   Coercion.instNewTyCon_maybe; differences are:
+--     * it also lookups up newtypes families, and
+--     * it does not require the newtype to be saturated.
+--       (a requirement using it for Coercible)
+instNewTyConTF_maybe :: FamInstEnvs -> TyCon -> [Type] -> Maybe (Type, Coercion)
+instNewTyConTF_maybe env tc tys = result
+  where
+  (co1, tc2, tys2)
+    | Just (co, rhs1) <- reduceTyFamApp_maybe env Representational tc tys
+    , Just (tc2, tys2) <- splitTyConApp_maybe rhs1
+    = (co, tc2, tys2)
+    | otherwise
+    = (mkReflCo Representational (mkTyConApp tc tys), tc, tys)
+
+  result
+     | Just (_, _, co_tc) <- unwrapNewTyCon_maybe tc2 -- Check for newtype
+     , newTyConEtadArity tc2 <= length tys2           -- Check for enough arguments
+     = Just (newTyConInstRhs tc2 tys2
+            , co1 `mkTransCo` mkUnbranchedAxInstCo Representational co_tc tys2)
+     | otherwise
+     = Nothing
+
 topNormaliseType :: FamInstEnvs -> Type -> Type
 topNormaliseType env ty = case topNormaliseType_maybe env ty of
                             Just (_co, ty') -> ty'