[commit: ghc] wip/impredicativity: Switch the order of arguments in InstanceOf (30e9fa2)
git at git.haskell.org
git at git.haskell.org
Fri Jun 19 11:49:34 UTC 2015
Repository : ssh://git@git.haskell.org/ghc
On branch : wip/impredicativity
Link : http://ghc.haskell.org/trac/ghc/changeset/30e9fa281cae44ae56a1cd19378e375282cd95a1/ghc
>---------------------------------------------------------------
commit 30e9fa281cae44ae56a1cd19378e375282cd95a1
Author: Alejandro Serrano <trupill at gmail.com>
Date: Fri Jun 19 13:29:40 2015 +0200
Switch the order of arguments in InstanceOf
In that way, we can make InstanceOf = (->)
at zonking stage
>---------------------------------------------------------------
30e9fa281cae44ae56a1cd19378e375282cd95a1
compiler/deSugar/DsBinds.hs | 4 ++--
compiler/typecheck/TcCanonical.hs | 20 ++++++++++----------
compiler/typecheck/TcExpr.hs | 4 ++--
compiler/typecheck/TcHsSyn.hs | 14 ++++++++++++--
libraries/ghc-prim/GHC/Types.hs | 2 +-
5 files changed, 27 insertions(+), 17 deletions(-)
diff --git a/compiler/deSugar/DsBinds.hs b/compiler/deSugar/DsBinds.hs
index 528f641..4d7ab9d 100644
--- a/compiler/deSugar/DsBinds.hs
+++ b/compiler/deSugar/DsBinds.hs
@@ -1159,12 +1159,12 @@ dsEvInstanceOf _ (EvInstanceOfVar v)
= return (Var v)
dsEvInstanceOf ty (EvInstanceOfEq co)
= do { bndr <- newSysLocalDs ty
- ; expr <- dsTcCoercion (TcSymCo co) (mkCast (Var bndr))
+ ; expr <- dsTcCoercion co (mkCast (Var bndr))
; return (mkCoreLams [bndr] expr) }
dsEvInstanceOf ty (EvInstanceOfInst qvars co qs)
= do { bndr <- newSysLocalDs ty
; qs' <- mapM dsEvTerm qs
; let exprTy = foldl (\e t -> App e (Type t)) (Var bndr) qvars
exprEv = foldl App exprTy qs'
- ; expr <- dsTcCoercion (TcSymCo co) (mkCast exprEv)
+ ; expr <- dsTcCoercion co (mkCast exprEv)
; return (mkCoreLams [bndr] expr) }
diff --git a/compiler/typecheck/TcCanonical.hs b/compiler/typecheck/TcCanonical.hs
index 46ba17a..bb0b83d 100644
--- a/compiler/typecheck/TcCanonical.hs
+++ b/compiler/typecheck/TcCanonical.hs
@@ -1661,26 +1661,26 @@ can_instance_of (CInstanceOfCan { cc_ev = ev, cc_lhs = lhs, cc_rhs = rhs })
-- case InstanceOf sigma sigma, for the exact same sigma
| lhs `eqType` rhs
= can_instance_to_eq ev lhs rhs
- -- case InstanceOf sigma (T ...) --> sigma ~ T ...
- | Nothing <- getTyVar_maybe rhs, Nothing <- splitForAllTy_maybe rhs
- = can_instance_to_eq ev lhs rhs
- -- case InstanceOf (T ...) (forall qvars. Q => ty)
+ -- case InstanceOf (T ...) sigma --> T ... ~ sigma
| Nothing <- getTyVar_maybe lhs, Nothing <- splitForAllTy_maybe lhs
- , Just _ <- splitForAllTy_maybe rhs
+ = can_instance_to_eq ev lhs rhs
+ -- case InstanceOf (forall qvars. Q => ty) (T ...)
+ | Nothing <- getTyVar_maybe rhs, Nothing <- splitForAllTy_maybe rhs
+ , Just _ <- splitForAllTy_maybe lhs
= case ev of
CtWanted { ctev_evar = evar, ctev_loc = loc } ->
- do { (qvars, q, ty) <- splitInst rhs
+ do { (qvars, q, ty) <- splitInst lhs
-- 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
; let qvars' = map TyVarTy qvars
- ; setWantedEvBind evar (mkInstanceOfInst rhs qvars' (ctEvCoercion new_ev_ty)
+ ; setWantedEvBind evar (mkInstanceOfInst lhs qvars' (ctEvCoercion new_ev_ty)
(map ctev_evar new_ev_qs))
-- emit new work
; emitWorkNC new_ev_qs
- ; canEqNC new_ev_ty NomEq lhs ty }
+ ; canEqNC new_ev_ty NomEq rhs ty }
_ -> stopWith ev "Given/Derived instanceOf instantiation"
can_instance_of _ = panic "can_instance_of in a non InstanceOf constraint"
@@ -1689,10 +1689,10 @@ can_instance_to_eq ev lhs rhs
= do { let eq = mkTcEqPredRole Nominal lhs rhs
; case ev of
CtDerived {} -> canEqNC (ev { ctev_pred = eq }) NomEq lhs rhs
- CtGiven {ctev_loc = loc } ->
+ CtGiven { ctev_loc = loc } ->
do { emitNewDerivedEq loc eq
; stopWith ev "Given instanceOf equality" }
CtWanted { ctev_evar = evar, ctev_loc = loc } ->
do { new_ev <- newWantedEvVarNC loc eq
- ; setWantedEvBind evar (mkInstanceOfEq rhs (ctEvCoercion new_ev))
+ ; setWantedEvBind evar (mkInstanceOfEq lhs (ctEvCoercion new_ev))
; canEqNC new_ev NomEq lhs rhs } }
diff --git a/compiler/typecheck/TcExpr.hs b/compiler/typecheck/TcExpr.hs
index 4112d45..f819f22 100644
--- a/compiler/typecheck/TcExpr.hs
+++ b/compiler/typecheck/TcExpr.hs
@@ -959,7 +959,7 @@ tc_app fun args fun_ty res_ty post_proc
-- Rather like tcWrapResult, but (perhaps for historical reasons)
-- we do this before typechecking the arguments
; ev_res <- addErrCtxtM (funResCtxt True (unLoc fun) actual_res_ty res_ty) $
- emitWanted AppOrigin (mkInstanceOfPred res_ty actual_res_ty)
+ emitWanted AppOrigin (mkInstanceOfPred actual_res_ty res_ty)
-- Typecheck the arguments
; args1 <- tcArgs fun args expected_arg_tys
@@ -1142,7 +1142,7 @@ tc_check_id orig id_name res_ty
-> do { co <- unifyType res_ty actual_ty
; return (mkHsWrap (mkWpCast co) (HsVar id)) }
TcIdUnrestricted
- -> do { ev <- emitWanted orig (mkInstanceOfPred res_ty actual_ty)
+ -> do { ev <- emitWanted orig (mkInstanceOfPred actual_ty res_ty)
; return (mkHsWrap (mkWpInstanceOf actual_ty ev) (HsVar id)) } }
inst_data_con con
diff --git a/compiler/typecheck/TcHsSyn.hs b/compiler/typecheck/TcHsSyn.hs
index 63f51eb..caf1642 100644
--- a/compiler/typecheck/TcHsSyn.hs
+++ b/compiler/typecheck/TcHsSyn.hs
@@ -1442,8 +1442,18 @@ zonkTcTypeToType :: ZonkEnv -> TcType -> TcM Type
zonkTcTypeToType env ty
= go ty
where
- go (TyConApp tc tys) = do tys' <- mapM go tys
- return (mkTyConApp tc tys')
+ go (TyConApp tc tys)
+ | tc `hasKey` instanceOfTyConKey
+ = do tys' <- mapM go tys
+ -- Zonc instantiations to functions
+ return $ case tys' of
+ [] -> (mkTyConApp funTyCon [])
+ [_] -> (mkTyConApp funTyCon tys')
+ [_,_] -> (mkTyConApp funTyCon tys')
+ _ -> pprPanic "zonkTcTypeToType/instanceOf" (ppr ty)
+
+ | otherwise = do tys' <- mapM go tys
+ return (mkTyConApp tc tys')
-- Establish Type invariants
-- See Note [Zonking inside the knot] in TcHsType
diff --git a/libraries/ghc-prim/GHC/Types.hs b/libraries/ghc-prim/GHC/Types.hs
index 06ff898..b0c02d6 100644
--- a/libraries/ghc-prim/GHC/Types.hs
+++ b/libraries/ghc-prim/GHC/Types.hs
@@ -177,7 +177,7 @@ data Coercible a b = MkCoercible ((~#) a b)
-- Also see Note [Kind-changing of (~) and Coercible]
-- | A constraint inhabited only if type `a` is an instance of type `b`.
-data InstanceOf a b = MkInstanceOf (b -> a)
+data InstanceOf b a = MkInstanceOf (b -> a)
-- | Alias for 'tagToEnum#'. Returns True if its parameter is 1# and False
-- if it is 0#.
More information about the ghc-commits
mailing list