[commit: ghc] wip/T8541: Make Coercible higher-kinded (8959c69)

[git at git.haskell.org]

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

On branch  : wip/T8541
Link       : http://ghc.haskell.org/trac/ghc/changeset/8959c69104eb032b75ec94dcf9cda3edd2b46423/ghc

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

commit 8959c69104eb032b75ec94dcf9cda3edd2b46423
Author: Joachim Breitner <mail at joachim-breitner.de>
Date:   Tue Nov 19 11:46:25 2013 +0000

    Make Coercible higher-kinded
    
    This implements #8541. The changes are fully straight forward and work
    nicely for the examples from the ticket; this is mostly due to the
    existing code not checking for saturation and kindness.


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

8959c69104eb032b75ec94dcf9cda3edd2b46423
 compiler/basicTypes/MkId.lhs      |   18 +++++++++++-------
 compiler/coreSyn/MkCore.lhs       |    2 +-
 compiler/deSugar/DsBinds.lhs      |    2 +-
 compiler/prelude/TysWiredIn.lhs   |   18 +++++++++++-------
 compiler/typecheck/TcErrors.lhs   |    2 +-
 compiler/typecheck/TcInteract.lhs |    6 ++++--
 6 files changed, 29 insertions(+), 19 deletions(-)

diff --git a/compiler/basicTypes/MkId.lhs b/compiler/basicTypes/MkId.lhs
index df2af85..6f277c6 100644
--- a/compiler/basicTypes/MkId.lhs
+++ b/compiler/basicTypes/MkId.lhs
@@ -1141,13 +1141,17 @@ coerceId = pcMiscPrelId coerceName ty info
   where
     info = noCafIdInfo `setInlinePragInfo` alwaysInlinePragma
                        `setUnfoldingInfo`  mkCompulsoryUnfolding rhs
-    eqRTy = mkTyConApp coercibleTyCon [alphaTy, betaTy]
-    eqRPrimTy = mkTyConApp eqReprPrimTyCon [liftedTypeKind, alphaTy, betaTy]
-    ty   = mkForAllTys [alphaTyVar, betaTyVar] (mkFunTys [eqRTy, alphaTy] betaTy)
-
-    [eqR,x,eq] = mkTemplateLocals [eqRTy, alphaTy,eqRPrimTy]
-    rhs = mkLams [alphaTyVar,betaTyVar,eqR,x] $
-          mkWildCase (Var eqR) eqRTy betaTy $
+    kv = kKiVar
+    k = mkTyVarTy kv
+    a:b:_ = tyVarList k
+    [aTy,bTy] = map mkTyVarTy [a,b]
+    eqRTy     = mkTyConApp coercibleTyCon  [k, aTy, bTy]
+    eqRPrimTy = mkTyConApp eqReprPrimTyCon [k, aTy, bTy]
+    ty   = mkForAllTys [kv, a, b] (mkFunTys [eqRTy, aTy] bTy)
+
+    [eqR,x,eq] = mkTemplateLocals [eqRTy, aTy,eqRPrimTy]
+    rhs = mkLams [kv,a,b,eqR,x] $
+          mkWildCase (Var eqR) eqRTy bTy $
 	  [(DataAlt coercibleDataCon, [eq], Cast (Var x) (CoVarCo eq))]
 \end{code}
 
diff --git a/compiler/coreSyn/MkCore.lhs b/compiler/coreSyn/MkCore.lhs
index 532d4fc..068dd6b 100644
--- a/compiler/coreSyn/MkCore.lhs
+++ b/compiler/coreSyn/MkCore.lhs
@@ -310,7 +310,7 @@ mkEqBox co = ASSERT2( typeKind ty2 `eqKind` k, ppr co $$ ppr ty1 $$ ppr ty2 $$ p
 
 mkCoercible :: Coercion -> CoreExpr
 mkCoercible co = ASSERT2( typeKind ty2 `eqKind` k, ppr co $$ ppr ty1 $$ ppr ty2 $$ ppr (typeKind ty1) $$ ppr (typeKind ty2) )
-             Var (dataConWorkId coercibleDataCon) `mkTyApps` [ty1, ty2] `App` Coercion co
+             Var (dataConWorkId coercibleDataCon) `mkTyApps` [k, ty1, ty2] `App` Coercion co
   where Pair ty1 ty2 = coercionKind co
         k = typeKind ty1
 \end{code}
diff --git a/compiler/deSugar/DsBinds.lhs b/compiler/deSugar/DsBinds.lhs
index 46ab91c..a1ea8b5 100644
--- a/compiler/deSugar/DsBinds.lhs
+++ b/compiler/deSugar/DsBinds.lhs
@@ -817,7 +817,7 @@ wrapInEqRCase e mkBody = do
                 (exprType body')
                 [(DataAlt coercibleDataCon, [cov], body')]
   where
-  Just (tc, [ty1, ty2]) = splitTyConApp_maybe (exprType e)
+  Just (tc, [_k, ty1, ty2]) = splitTyConApp_maybe (exprType e)
 
 wrapInEqRCases :: [EvCoercibleArg CoreExpr] -> ([Coercion] -> DsM CoreExpr) -> DsM CoreExpr
 wrapInEqRCases (EvCoercibleArgN t:es) mkBody =
diff --git a/compiler/prelude/TysWiredIn.lhs b/compiler/prelude/TysWiredIn.lhs
index d3b7c1f..2830ca2 100644
--- a/compiler/prelude/TysWiredIn.lhs
+++ b/compiler/prelude/TysWiredIn.lhs
@@ -466,18 +466,22 @@ eqBoxDataCon = pcDataCon eqBoxDataConName args [TyConApp eqPrimTyCon (map mkTyVa
 
 coercibleTyCon :: TyCon
 coercibleTyCon = mkClassTyCon
-    coercibleTyConName kind tvs [Representational, Representational]
+    coercibleTyConName kind tvs [Nominal, Representational, Representational]
     rhs coercibleClass NonRecursive
-  where kind = mkArrowKinds [liftedTypeKind, liftedTypeKind] constraintKind
-        a:b:_ = tyVarList liftedTypeKind
-        tvs = [a, b]
+  where kind = (ForAllTy kv $ mkArrowKinds [k, k] constraintKind)
+        kv = kKiVar
+        k = mkTyVarTy kv
+        a:b:_ = tyVarList k
+        tvs = [kv, a, b]
         rhs = DataTyCon [coercibleDataCon] False
 
 coercibleDataCon :: DataCon
-coercibleDataCon = pcDataCon coercibleDataConName args [TyConApp eqReprPrimTyCon (liftedTypeKind : map mkTyVarTy args)] coercibleTyCon
+coercibleDataCon = pcDataCon coercibleDataConName args [TyConApp eqReprPrimTyCon (map mkTyVarTy args)] coercibleTyCon
   where
-    a:b:_ = tyVarList liftedTypeKind
-    args = [a, b]
+    kv = kKiVar
+    k = mkTyVarTy kv
+    a:b:_ = tyVarList k
+    args = [kv, a, b]
 
 coercibleClass :: Class
 coercibleClass = mkClass (tyConTyVars coercibleTyCon) [] [] [] [] [] (mkAnd []) coercibleTyCon
diff --git a/compiler/typecheck/TcErrors.lhs b/compiler/typecheck/TcErrors.lhs
index 78f1554..3bf76b0 100644
--- a/compiler/typecheck/TcErrors.lhs
+++ b/compiler/typecheck/TcErrors.lhs
@@ -1161,7 +1161,7 @@ mk_dict_err ctxt (ct, (matches, unifiers, safe_haskell))
                         ptext $ sLit "and", quotes (ppr ty2),
                         ptext $ sLit "are different types." ]
       where
-        (clas, ~[ty1,ty2]) = getClassPredTys (ctPred ct)
+        (clas, ~[_k, ty1,ty2]) = getClassPredTys (ctPred ct)
 
     dataConMissing rdr_env tc =
         all (null . lookupGRE_Name rdr_env) (map dataConName (tyConDataCons tc))
diff --git a/compiler/typecheck/TcInteract.lhs b/compiler/typecheck/TcInteract.lhs
index beb8a9e..c61b8da 100644
--- a/compiler/typecheck/TcInteract.lhs
+++ b/compiler/typecheck/TcInteract.lhs
@@ -1841,7 +1841,7 @@ matchClassInst _ clas [ ty ] _
       _ -> panicTcS (text "Unexpected evidence for" <+> ppr (className clas)
                      $$ vcat (map (ppr . idType) (classMethods clas)))
 
-matchClassInst _ clas [ ty1, ty2 ] _
+matchClassInst _ clas [ _k, ty1, ty2 ] _
   | clas == coercibleClass =  do
       traceTcS "matchClassInst for" $ ppr clas <+> ppr ty1 <+> ppr ty2
       rdr_env <- getGlobalRdrEnvTcS
@@ -2003,7 +2003,9 @@ markDataConsAsUsed rdr_env tc = addUsedRdrNamesTcS
   , Imported (imp_spec:_) <- [gre_prov (head gres)] ]
 
 requestCoercible :: TcType -> TcType -> TcS MaybeNew
-requestCoercible ty1 ty2 = newWantedEvVar (coercibleClass `mkClassPred` [ty1, ty2])
+requestCoercible ty1 ty2 =
+    ASSERT2( typeKind ty1 `eqKind` typeKind ty2, ppr ty1 <+> ppr ty2)
+    newWantedEvVar (coercibleClass `mkClassPred` [typeKind ty1, ty1, ty2])
 
 \end{code}