Commit 976a1087 authored by Joachim Breitner's avatar Joachim Breitner
Browse files

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.
parent 0346dee9
......@@ -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}
......
......@@ -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}
......
......@@ -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 =
......
......@@ -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
......
......@@ -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))
......
......@@ -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}
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment