[commit: ghc] wip/new-flatten-skolems-Aug14: More flatten-skolem progress (0d2ce1d)

[git at git.haskell.org]

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

On branch  : wip/new-flatten-skolems-Aug14
Link       : http://ghc.haskell.org/trac/ghc/changeset/0d2ce1ddae9cb8400b3d228a73023019cbe4f789/ghc

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

commit 0d2ce1ddae9cb8400b3d228a73023019cbe4f789
Author: Simon Peyton Jones <simonpj at microsoft.com>
Date:   Wed Oct 1 12:54:27 2014 +0100

    More flatten-skolem progress


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

0d2ce1ddae9cb8400b3d228a73023019cbe4f789
 compiler/typecheck/Flattening-notes |  2 ++
 compiler/typecheck/TcEvidence.lhs   | 23 +++++++++++++++++++++++
 compiler/typecheck/TcRnTypes.lhs    |  2 ++
 compiler/typecheck/TcSMonad.lhs     | 19 ++++++++++++-------
 4 files changed, 39 insertions(+), 7 deletions(-)

diff --git a/compiler/typecheck/Flattening-notes b/compiler/typecheck/Flattening-notes
index a945d03..da8441a 100644
--- a/compiler/typecheck/Flattening-notes
+++ b/compiler/typecheck/Flattening-notes
@@ -1,5 +1,7 @@
 ToDo:
 
+* ctev_loc should have a decent name ctEvLoc
+
 * Float only CTyEqCans.   kind-incompatible things should be CNonCanonical,
   so they won't float and generate a duplicate kind-unify message
 
diff --git a/compiler/typecheck/TcEvidence.lhs b/compiler/typecheck/TcEvidence.lhs
index 3b2a3d6..d0481c8 100644
--- a/compiler/typecheck/TcEvidence.lhs
+++ b/compiler/typecheck/TcEvidence.lhs
@@ -28,6 +28,7 @@ module TcEvidence (
   mkTcAxiomRuleCo,
   tcCoercionKind, coVarsOfTcCo, isEqVar, mkTcCoVarCo,
   isTcReflCo, getTcCoVar_maybe,
+  tcLiftCoSubst, 
   tcCoercionRole, eqVarRole
   ) where
 #include "HsVersions.h"
@@ -339,6 +340,28 @@ coVarsOfTcCo tc_co
 
     get_bndrs :: Bag EvBind -> VarSet
     get_bndrs = foldrBag (\ (EvBind b _) bs -> extendVarSet bs b) emptyVarSet
+
+tcLiftCoSubst :: TcTyVar -> TcCoercion -> TcType -> TcCoercion
+-- Substitute the_tv -> the_co in the given type, at Nominal role
+-- Like Coercion.liftCoSubst, but for TcCoercion, and 
+-- specialised for Nominal role
+tcLiftCoSubst the_tv the_co ty
+ = ASSERT( tcCoercionRole the_co == Nominal )
+   go ty
+ where
+   go ty@(TyVarTy tv)
+     | tv == the_tv = the_co
+     | otherwise    = TcRefl Nominal ty
+   go ty@(LitTy {}) = TcRefl Nominal ty
+
+   go (AppTy ty1 ty2)   = mkTcAppCo         (go ty1) (go ty2)
+   go (FunTy ty1 ty2)   = mkTcFunCo Nominal (go ty1) (go ty2)
+   go (TyConApp tc tys) = mkTcTyConAppCo Nominal tc (map go tys)
+                          -- We are building a Nominal coercion, so the TyCon's
+                          -- args must all be Nominal coercions too, regardless
+                          -- of the TyCon's arg rules (c.f. Coercion.tyConRolesX)
+   go ty@(ForAllTy _ _) = pprPanic "tcLiftCoSubst" (ppr ty)
+     -- Substituting under a for-all is awkward
 \end{code}
 
 Pretty printing
diff --git a/compiler/typecheck/TcRnTypes.lhs b/compiler/typecheck/TcRnTypes.lhs
index d5315d2..584115f 100644
--- a/compiler/typecheck/TcRnTypes.lhs
+++ b/compiler/typecheck/TcRnTypes.lhs
@@ -960,6 +960,8 @@ data Ct
   | CFunEqCan {  -- F xis ~ fsk
        -- Invariant: * isSynFamilyTyCon cc_fun
        --            * typeKind (F xis) `subKind` typeKind xi
+       --            * always Nominal role
+       --            * always Given or Watned, never Derived
        --       See Note [Kind orientation for CFunEqCan]
       cc_ev     :: CtEvidence,  -- See Note [Ct/evidence invariant]
       cc_fun    :: TyCon,       -- A type function
diff --git a/compiler/typecheck/TcSMonad.lhs b/compiler/typecheck/TcSMonad.lhs
index 25b22e9..b05368f 100644
--- a/compiler/typecheck/TcSMonad.lhs
+++ b/compiler/typecheck/TcSMonad.lhs
@@ -687,21 +687,22 @@ getInertUnsolved
     unflatten_funeq :: DynFlags
                     -> Ct -> TcS Cts -> TcS Cts
     unflatten_funeq dflags (CFunEqCan { cc_fun = tc, cc_tyargs = xis
-                                      , cc_fsk = tv, cc_ev = ev }) rest
+                                      , cc_fsk = fsk, cc_ev = ev }) rest
       | isGiven ev -- tv should be a FlatSkol; zonking will eliminate it
       = rest
 
       | otherwise  -- A flatten meta-tv; we now fix its final
                    -- value, and then zonking will eliminate it
-      = do { unsolved <- rest
+      = ASSERT( isWanted ev )  -- CFunEqCans are never Derived
+        do { unsolved <- rest
            ; fn_app <- wrapTcS (TcM.zonkTcType (mkTyConApp tc xis))
-           ; case occurCheckExpand dflags tv fn_app of
+           ; case occurCheckExpand dflags fsk fn_app of
                OC_OK fn_app' 
                  ->    -- Normal case: unflatten
                     do { let evterm = EvCoercion (mkTcNomReflCo fn_app')
                              evvar  = ctev_evar ev
                        ; setEvBind evvar evterm
-                       ; wrapTcS (TcM.writeMetaTyVar tv fn_app')
+                       ; wrapTcS (TcM.writeMetaTyVar fsk fn_app')
                              -- Write directly into the mutable tyvar
                              -- Flatten meta-vars are born locally and 
                              -- die locally
@@ -709,9 +710,13 @@ getInertUnsolved
 
                _ ->    -- Occurs check; don't unflatten, instead turn it into a NonCanonical
                        -- Don't forget to get rid ofthe 
-                    do { tv_ty <- newFlexiTcSTy (tyVarKind tv)
-                       ; wrapTcS (TcM.writeMetaTyVar tv tv_ty)
-                       ; return (unsolved `extendCts` mkNonCanonical ev) } }
+                    do { tv_ty <- newFlexiTcSTy (tyVarKind fsk)
+                       ; let fn_app' = substTyWith [fsk] [tv_ty] fn_app
+                       ; wrapTcS (TcM.writeMetaTyVar fsk fn_app')
+                       ; new_ev <- newWantedEvVarNC (ctev_loc ev) (mkEqPred fn_app' tv_ty)
+                                   -- w' :: F tau[alpha] ~ alpha
+                       ; setEvBind (ctEvId ev) (EvCoercion (tcLiftCoSubst fsk (ctEvCoercion new_ev) fn_app))
+                       ; return (unsolved `extendCts` mkNonCanonical new_ev) } }
 
     unflatten_funeq _ other_ct _ 
       = pprPanic "unflatten_funeq" (ppr other_ct)