[commit: ghc] master: Coercible for impredicative types (9bc5b53)

[git at git.haskell.org]

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

On branch  : master
Link       : http://ghc.haskell.org/trac/ghc/changeset/9bc5b530811407b19882b6c479a05b99c1329962/ghc

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

commit 9bc5b530811407b19882b6c479a05b99c1329962
Author: Joachim Breitner <mail at joachim-breitner.de>
Date:   Wed Nov 27 17:19:20 2013 +0000

    Coercible for impredicative types
    
    using deferTcSForAllEq, just like for ~ types, during canonicalization


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

9bc5b530811407b19882b6c479a05b99c1329962
 compiler/typecheck/TcCanonical.lhs |   18 ++++++++++++++++--
 compiler/typecheck/TcInteract.lhs  |    1 -
 compiler/typecheck/TcSMonad.lhs    |   10 +++++++---
 3 files changed, 23 insertions(+), 6 deletions(-)

diff --git a/compiler/typecheck/TcCanonical.lhs b/compiler/typecheck/TcCanonical.lhs
index 5b594b8..5428d74 100644
--- a/compiler/typecheck/TcCanonical.lhs
+++ b/compiler/typecheck/TcCanonical.lhs
@@ -19,7 +19,7 @@ import VarEnv
 import OccName( OccName )
 import Outputable
 import Control.Monad    ( when )
-import TysWiredIn ( eqTyCon )
+import TysWiredIn ( eqTyCon, coercibleClass )
 import DynFlags( DynFlags )
 import VarSet
 import TcSMonad
@@ -233,6 +233,20 @@ canClassNC ev cls tys
   = canClass ev cls tys
     `andWhenContinue` emitSuperclasses
 
+-- This case implements Coercible (forall a. body) (forall b. body)
+canClass ev cls tys
+  | cls == coercibleClass
+  , [_k, ty1, ty2] <- tys
+  , tcIsForAllTy ty1
+  , tcIsForAllTy ty2
+  , let (tvs1,body1) = tcSplitForAllTys ty1
+        (tvs2,body2) = tcSplitForAllTys ty2
+  , CtWanted { ctev_loc = loc, ctev_evar = orig_ev } <- ev
+  , equalLength tvs1 tvs2
+  = do { traceTcS "Creating implication for polytype coercible equality" $ ppr ev
+       ; deferTcSForAllEq Representational (loc,orig_ev) (tvs1,body1) (tvs2,body2)
+       ; return Stop }
+
 canClass ev cls tys
   = do { (xis, cos) <- flattenMany FMFullFlatten ev tys
        ; let co = mkTcTyConAppCo Nominal (classTyCon cls) cos
@@ -751,7 +765,7 @@ canEqNC ev s1@(ForAllTy {}) s2@(ForAllTy {})
           canEqFailure ev s1 s2
         else
           do { traceTcS "Creating implication for polytype equality" $ ppr ev
-             ; deferTcSForAllEq (loc,orig_ev) (tvs1,body1) (tvs2,body2)
+             ; deferTcSForAllEq Nominal (loc,orig_ev) (tvs1,body1) (tvs2,body2)
              ; return Stop } }
  | otherwise
  = do { traceTcS "Ommitting decomposition of given polytype equality" $
diff --git a/compiler/typecheck/TcInteract.lhs b/compiler/typecheck/TcInteract.lhs
index 0993397..0ede57c 100644
--- a/compiler/typecheck/TcInteract.lhs
+++ b/compiler/typecheck/TcInteract.lhs
@@ -1939,7 +1939,6 @@ getCoercibleInst safeMode famenv rdr_env loc ty1 ty2
   | ty1 `tcEqType` ty2
   = do return $ GenInst []
               $ EvCoercion (TcRefl Representational ty1)
-
   | Just (tc1,tyArgs1) <- splitTyConApp_maybe ty1,
     Just (tc2,tyArgs2) <- splitTyConApp_maybe ty2,
     tc1 == tc2,
diff --git a/compiler/typecheck/TcSMonad.lhs b/compiler/typecheck/TcSMonad.lhs
index f4e33e4..57b13ed 100644
--- a/compiler/typecheck/TcSMonad.lhs
+++ b/compiler/typecheck/TcSMonad.lhs
@@ -1750,19 +1750,23 @@ matchFam tycon args
 -- Deferring forall equalities as implications
 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-deferTcSForAllEq :: (CtLoc,EvVar)  -- Original wanted equality flavor
+deferTcSForAllEq :: Role -- Nominal or Representational
+                 -> (CtLoc,EvVar)  -- Original wanted equality flavor
                  -> ([TyVar],TcType)   -- ForAll tvs1 body1
                  -> ([TyVar],TcType)   -- ForAll tvs2 body2
                  -> TcS ()
 -- Some of this functionality is repeated from TcUnify,
 -- consider having a single place where we create fresh implications.
-deferTcSForAllEq (loc,orig_ev) (tvs1,body1) (tvs2,body2)
+deferTcSForAllEq role (loc,orig_ev) (tvs1,body1) (tvs2,body2)
  = do { (subst1, skol_tvs) <- wrapTcS $ TcM.tcInstSkolTyVars tvs1
       ; let tys  = mkTyVarTys skol_tvs
             phi1 = Type.substTy subst1 body1
             phi2 = Type.substTy (zipTopTvSubst tvs2 tys) body2
             skol_info = UnifyForAllSkol skol_tvs phi1
-        ; mev <- newWantedEvVar loc (mkTcEqPred phi1 phi2)
+        ; mev <- newWantedEvVar loc $ case role of
+                Nominal ->          mkTcEqPred      phi1 phi2
+                Representational -> mkCoerciblePred phi1 phi2
+                Phantom ->          panic "deferTcSForAllEq Phantom"
         ; coe_inside <- case mev of
             Cached ev_tm -> return (evTermCoercion ev_tm)
             Fresh ctev   -> do { ev_binds_var <- wrapTcS $ TcM.newTcEvBinds