[commit: ghc] wip/impredicativity: Implement second rule for InstanceOf canon. (06820b4)

[git at git.haskell.org]

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

On branch  : wip/impredicativity
Link       : http://ghc.haskell.org/trac/ghc/changeset/06820b45707e6df02f5df20564acc3b8dee5acb6/ghc

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

commit 06820b45707e6df02f5df20564acc3b8dee5acb6
Author: Alejandro Serrano <trupill at gmail.com>
Date:   Wed Jun 17 13:42:31 2015 +0200

    Implement second rule for InstanceOf canon.
    
    Rule InstanceOf (T ...) (forall a. Q => ty)
     --> [a/alpha]Q /\ T ... ~ [a/alpha]ty


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

06820b45707e6df02f5df20564acc3b8dee5acb6
 compiler/typecheck/TcCanonical.hs | 20 +++++++++++++++++++-
 compiler/typecheck/TcEvidence.hs  | 11 +++++++----
 compiler/typecheck/TcSMonad.hs    | 12 +++++++++++-
 compiler/typecheck/TcSimplify.hs  |  1 +
 4 files changed, 38 insertions(+), 6 deletions(-)

diff --git a/compiler/typecheck/TcCanonical.hs b/compiler/typecheck/TcCanonical.hs
index 3159cb8..d1c56cf 100644
--- a/compiler/typecheck/TcCanonical.hs
+++ b/compiler/typecheck/TcCanonical.hs
@@ -1665,8 +1665,26 @@ can_instance_of ct@(CInstanceOfCan { cc_ev = ev, cc_lhs = lhs, cc_rhs = rhs })
            CtDerived {} -> canEqNC (ev { ctev_pred = eq }) NomEq lhs rhs
            CtGiven {ctev_loc = loc } ->
              do { emitNewDerivedEq loc eq
-                ; stopWith ev "Given instance equality" }
+                ; stopWith ev "Given instanceOf equality" }
            CtWanted { ctev_evar = evar, ctev_loc = loc } ->
              do { new_ev <- newWantedEvVarNC loc eq
                 ; setWantedEvBind evar (mkInstanceOfEq (ctEvCoercion new_ev))
                 ; canEqNC new_ev NomEq lhs rhs } }
+
+  -- case InstanceOf (T ...) (forall qvars. Q => ty)
+  | Nothing <- getTyVar_maybe lhs, Nothing <- splitForAllTy_maybe lhs
+  , Just _  <- splitForAllTy_maybe rhs
+  = case ev of
+      CtWanted { ctev_evar = evar, ctev_loc = loc } ->
+        do { (_qvars, q, ty) <- splitInst rhs
+             -- generate new constraints
+           ; new_ev_qs <- mapM (newWantedEvVarNC loc) q
+           ; let eq = mkTcEqPredRole Nominal lhs ty
+           ; new_ev_ty <- newWantedEvVarNC loc eq
+             -- compute the evidence for the instantiation
+           ; setWantedEvBind evar (mkInstanceOfInst (ctEvCoercion new_ev_ty)
+                                                    (map ctev_evar new_ev_qs))
+             -- emit new work
+           ; emitWorkNC new_ev_qs
+           ; canEqNC new_ev_ty NomEq lhs ty }
+      _ -> stopWith ev "Given/Derived instanceOf instantiation"
diff --git a/compiler/typecheck/TcEvidence.hs b/compiler/typecheck/TcEvidence.hs
index 904e9fd..2400a18 100644
--- a/compiler/typecheck/TcEvidence.hs
+++ b/compiler/typecheck/TcEvidence.hs
@@ -18,7 +18,7 @@ module TcEvidence (
   EvLit(..), evTermCoercion,
   EvCallStack(..),
   EvTypeable(..),
-  EvInstanceOf(..), mkInstanceOfEq,
+  EvInstanceOf(..), mkInstanceOfEq, mkInstanceOfInst,
 
   -- TcCoercion
   TcCoercion(..), LeftOrRight(..), pickLR,
@@ -767,13 +767,16 @@ data EvCallStack
 -- Evidence for instantiation / InstanceOf constraints
 data EvInstanceOf
   = EvInstanceOfEq   TcCoercion  -- ^ term witnessing equality
-  | EvInstanceOfInst TcCoercion EvTerm
+  | EvInstanceOfInst TcCoercion [EvTerm]
   | EvInstanceOfLet  TcEvBinds  EvInstanceOf
     deriving ( Data.Data, Data.Typeable )
 
 mkInstanceOfEq :: TcCoercion -> EvTerm
 mkInstanceOfEq = EvInstanceOf . EvInstanceOfEq
 
+mkInstanceOfInst :: TcCoercion -> [EvVar] -> EvTerm
+mkInstanceOfInst co q = EvInstanceOf (EvInstanceOfInst co (map EvId q))
+
 {-
 Note [Coercion evidence terms]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -1037,8 +1040,8 @@ evVarsOfTypeable ev =
 evVarsOfInstanceOf :: EvInstanceOf -> VarSet
 evVarsOfInstanceOf ev =
   case ev of
-    EvInstanceOfEq co     -> coVarsOfTcCo co
-    EvInstanceOfInst co t -> coVarsOfTcCo co `unionVarSet` evVarsOfTerm t
+    EvInstanceOfEq   co   -> coVarsOfTcCo co
+    EvInstanceOfInst co q -> coVarsOfTcCo co `unionVarSet` evVarsOfTerms q
     EvInstanceOfLet  _  _ -> emptyVarSet
 
 {-
diff --git a/compiler/typecheck/TcSMonad.hs b/compiler/typecheck/TcSMonad.hs
index 231f94a..c0c213c 100644
--- a/compiler/typecheck/TcSMonad.hs
+++ b/compiler/typecheck/TcSMonad.hs
@@ -15,7 +15,7 @@ module TcSMonad (
     TcS, runTcS, runTcSWithEvBinds,
     failTcS, tryTcS, nestTcS, nestImplicTcS, recoverTcS,
 
-    runTcPluginTcS, addUsedRdrNamesTcS, deferTcSForAllEq,
+    runTcPluginTcS, addUsedRdrNamesTcS, deferTcSForAllEq, splitInst,
 
     -- Tracing etc
     panicTcS, traceTcS,
@@ -2869,3 +2869,13 @@ deferTcSForAllEq role loc (tvs1,body1) (tvs2,body2)
                          ; return (TcLetCo ev_binds new_co) }
 
         ; return $ EvCoercion (foldr mkTcForAllCo coe_inside skol_tvs) }
+
+-- Split a sigma type and instantiate its variables
+splitInst :: Type -> TcS ([TyVar], ThetaType, Type)
+splitInst sigma
+  = do { let (qvars, q, ty) = tcSplitSigmaTy sigma
+         -- instantiate variables for q and ty
+         ; (subst, inst_vars) <- wrapTcS $ TcM.tcInstTyVars qvars
+         ; let q_subst  = map (Type.substTy subst) q
+               ty_subst = Type.substTy subst ty
+         ; return (inst_vars, q_subst, ty_subst) }
diff --git a/compiler/typecheck/TcSimplify.hs b/compiler/typecheck/TcSimplify.hs
index 2bcf5eb..5b35437 100644
--- a/compiler/typecheck/TcSimplify.hs
+++ b/compiler/typecheck/TcSimplify.hs
@@ -616,6 +616,7 @@ pickQuantifiablePreds qtvs theta
 
           EqPred NomEq ty1 ty2  -> quant_fun ty1 || quant_fun ty2
           IrredPred ty          -> tyVarsOfType ty `intersectsVarSet` qtvs
+          InstanceOfPred ty1 ty2 -> quant_fun ty1 || quant_fun ty2
 
     pick_cls_pred flex_ctxt tys
       = tyVarsOfTypes tys `intersectsVarSet` qtvs