[commit: ghc] wip/impredicativity: Fix wrong canonicalization of InstanceOf constraints (3606e9a)
git at git.haskell.org
git at git.haskell.org
Thu Jun 25 12:37:36 UTC 2015
Repository : ssh://git@git.haskell.org/ghc
On branch : wip/impredicativity
Link : http://ghc.haskell.org/trac/ghc/changeset/3606e9adbcb977b1a419c1ef60fae243b7157aa8/ghc
>---------------------------------------------------------------
commit 3606e9adbcb977b1a419c1ef60fae243b7157aa8
Author: Alejandro Serrano <trupill at gmail.com>
Date: Thu Jun 25 14:34:34 2015 +0200
Fix wrong canonicalization of InstanceOf constraints
Previously, constraints of the form
> InstanceOf (forall a. F a => forall b. G a b => ty)
that is, where the type is not directly of the form type variables
then constraints then a forall-less type, were not handled correctly.
This patch ensures that it now works, by replacing the equality
constraint that was obtained in that situation with a more
general InstanceOf constraint.
The evidence generation and desugaring has been changed accordingly.
>---------------------------------------------------------------
3606e9adbcb977b1a419c1ef60fae243b7157aa8
compiler/deSugar/DsBinds.hs | 3 +--
compiler/typecheck/TcCanonical.hs | 6 +++---
compiler/typecheck/TcEvidence.hs | 16 +++++++++-------
compiler/typecheck/TcExpr.hs | 30 +++++++++++++++++++-----------
compiler/typecheck/TcHsSyn.hs | 4 ++--
5 files changed, 34 insertions(+), 25 deletions(-)
diff --git a/compiler/deSugar/DsBinds.hs b/compiler/deSugar/DsBinds.hs
index 085c0e3..9d4d875 100644
--- a/compiler/deSugar/DsBinds.hs
+++ b/compiler/deSugar/DsBinds.hs
@@ -1166,8 +1166,7 @@ dsEvInstanceOf ty (EvInstanceOfInst qvars co qs)
; qs' <- mapM dsEvTerm qs
; let exprTy = mkCoreApps (Var bndr) (map Type qvars)
exprEv = mkCoreApps exprTy qs'
- ; expr <- dsTcCoercion co (\c -> mkCast exprEv (mkSubCo c))
- ; return (mkCoreLams [bndr] expr) }
+ ; return (mkCoreLams [bndr] (mkCoreApp (Var co) exprEv)) }
dsEvInstanceOf ty (EvInstanceOfLet tyvars qvars qs rest)
= do { bndr <- newSysLocalDs ty
; q_binds <- dsTcEvBinds qs
diff --git a/compiler/typecheck/TcCanonical.hs b/compiler/typecheck/TcCanonical.hs
index 9fd5393..fd7a191 100644
--- a/compiler/typecheck/TcCanonical.hs
+++ b/compiler/typecheck/TcCanonical.hs
@@ -1671,16 +1671,16 @@ can_instance_of (CInstanceOfCan { cc_ev = ev, cc_lhs = lhs, cc_rhs = rhs })
do { (qvars, q, ty) <- splitInst lhs
-- generate new constraints
; new_ev_qs <- mapM (newWantedEvVarNC loc) q
- ; let eq = mkTcEqPred ty rhs
+ ; let eq = mkInstanceOfPred ty rhs
; new_ev_ty <- newWantedEvVarNC loc eq
-- compute the evidence for the instantiation
; let qvars' = map mkTyVarTy qvars
- ; setWantedEvBind evar (mkInstanceOfInst lhs qvars' (ctEvCoercion new_ev_ty)
+ ; setWantedEvBind evar (mkInstanceOfInst lhs qvars' (ctEvId new_ev_ty)
(map ctev_evar new_ev_qs))
-- emit new work
; emitWorkNC new_ev_qs
; traceTcS "can_instance_of/INST" (vcat [ ppr new_ev_ty, ppr new_ev_qs ])
- ; canEqNC new_ev_ty NomEq ty rhs }
+ ; canInstanceOfNC new_ev_ty }
_ -> stopWith ev "Given/Derived instanceOf instantiation"
| Just _ <- splitForAllTy_maybe rhs
= case ev of
diff --git a/compiler/typecheck/TcEvidence.hs b/compiler/typecheck/TcEvidence.hs
index c5c9660..faac293 100644
--- a/compiler/typecheck/TcEvidence.hs
+++ b/compiler/typecheck/TcEvidence.hs
@@ -772,18 +772,20 @@ data EvCallStack
data EvInstanceOf
= EvInstanceOfVar EvId
| EvInstanceOfEq TcCoercion -- ^ term witnessing equality
- | EvInstanceOfInst [Type] TcCoercion [EvTerm]
- | EvInstanceOfLet [TyVar] -- ^ type variables
- [EvId] -- ^ constraint variables
- TcEvBinds -- ^ inner bindings
- EvId -- ^ inner instantiation constraint
+ | EvInstanceOfInst [Type] -- ^ type variables to apply
+ EvId -- ^ witness for inner instantiation
+ [EvTerm] -- ^ witness for inner constraints
+ | EvInstanceOfLet [TyVar] -- ^ type variables
+ [EvId] -- ^ constraint variables
+ TcEvBinds -- ^ inner bindings
+ EvId -- ^ inner instantiation constraint
deriving ( Data.Data, Data.Typeable )
mkInstanceOfEq :: Type -> TcCoercion -> EvTerm
mkInstanceOfEq ty co
= EvInstanceOf ty (EvInstanceOfEq co)
-mkInstanceOfInst :: Type -> [Type] -> TcCoercion -> [EvVar] -> EvTerm
+mkInstanceOfInst :: Type -> [Type] -> EvId -> [EvVar] -> EvTerm
mkInstanceOfInst ty vars co q
= EvInstanceOf ty (EvInstanceOfInst vars co (map EvId q))
@@ -1056,7 +1058,7 @@ evVarsOfInstanceOf ev =
case ev of
EvInstanceOfVar v -> unitVarSet v
EvInstanceOfEq co -> coVarsOfTcCo co
- EvInstanceOfInst _ co q -> coVarsOfTcCo co `unionVarSet` evVarsOfTerms q
+ EvInstanceOfInst _ co q -> unitVarSet co `unionVarSet` evVarsOfTerms q
EvInstanceOfLet _ qvars (EvBinds bs) co ->
(foldrBag (unionVarSet . go_bind) (unitVarSet co) bs
`minusVarSet` get_bndrs bs) `minusVarSet` mkVarSet qvars
diff --git a/compiler/typecheck/TcExpr.hs b/compiler/typecheck/TcExpr.hs
index 2a39b40..ea84eec 100644
--- a/compiler/typecheck/TcExpr.hs
+++ b/compiler/typecheck/TcExpr.hs
@@ -957,7 +957,7 @@ tcAppWorker special fun@(L loc (HsVar fun_name)) args res_ty
, (actual_fun@(L loc (HsVar actual_fun_name)) : rest_args) <- args
= do { -- Typing without ($)
actual_fun_ty <- tc_app_get_fn_ty actual_fun_name
- (tc_app_inst (length rest_args) res_ty)
+ (tc_app_unknown_fn (length rest_args) res_ty)
; result <- tc_app actual_fun rest_args actual_fun_ty res_ty special
-- Build the ($) application
; dollar <- tcCheckId fun_name (mkFunTy actual_fun_ty actual_fun_ty)
@@ -966,13 +966,13 @@ tcAppWorker special fun@(L loc (HsVar fun_name)) args res_ty
| otherwise -- fallback case
= do { fun_ty <- tc_app_get_fn_ty fun_name
- (tc_app_inst (length args) res_ty)
+ (tc_app_unknown_fn (length args) res_ty)
; tc_app fun args fun_ty res_ty special }
tcAppWorker special fun args res_ty
-- Normal case, where the function is not a variable
= do { -- Create function type schema
- ; fun_ty <- tc_app_inst (length args) res_ty
+ ; fun_ty <- tc_app_unknown_fn (length args) res_ty
-- Run with new type schema
; tc_app fun args fun_ty res_ty special }
@@ -991,20 +991,28 @@ tc_app_get_fn_ty fun_name not_found
; return pat_ty }
_ -> not_found
-- Instantiate type
- ; let (tvs, theta, rho) = tcSplitSigmaTy fun_ty
- ; (subst, _tvs') <- tcInstTyVars tvs
- ; let theta' = substTheta subst theta
- rho' = substTy subst rho
+ ; (theta, rho) <- tc_app_inst fun_ty
-- Run with instantiated type
- ; _theta_w <- instCallConstraints (OccurrenceOf fun_name) theta'
- ; return rho' }
+ ; _theta_w <- instCallConstraints (OccurrenceOf fun_name) theta
+ ; return rho }
-tc_app_inst :: Int -> TcSigmaType -> TcM TcRhoType
-tc_app_inst nb_args res_ty
+tc_app_unknown_fn :: Int -> TcSigmaType -> TcM TcRhoType
+tc_app_unknown_fn nb_args res_ty
= do { args_tys <- replicateM nb_args (newFlexiTyVarTy openTypeKind)
; let fun_ty = mkFunTys args_tys res_ty
; return fun_ty }
+tc_app_inst :: TcSigmaType -> TcM (ThetaType, TcRhoType)
+tc_app_inst sigma
+ | Just _ <- splitForAllTy_maybe sigma
+ = do { let (tvs, theta, ty) = tcSplitSigmaTy sigma
+ ; (subst, _tvs') <- tcInstTyVars tvs
+ ; let theta' = substTheta subst theta
+ ty' = substTy subst ty
+ ; (theta'', ty'') <- tc_app_inst ty'
+ ; return (theta' ++ theta'', ty'') }
+tc_app_inst ty = return ([], ty)
+
tc_app :: LHsExpr Name -> [LHsExpr Name]
-> TcSigmaType -- type pushed for the function
-> TcRhoType -- type pushed for the result
diff --git a/compiler/typecheck/TcHsSyn.hs b/compiler/typecheck/TcHsSyn.hs
index 0f38770..f9eacf6 100644
--- a/compiler/typecheck/TcHsSyn.hs
+++ b/compiler/typecheck/TcHsSyn.hs
@@ -1335,8 +1335,8 @@ zonkEvInstanceOf env (EvInstanceOfEq co)
; return (EvInstanceOfEq co') }
zonkEvInstanceOf env (EvInstanceOfInst tys co q)
= do { tys' <- mapM (zonkTcTypeToType env) tys
- ; co' <- zonkTcCoToCo env co
- ; q' <- mapM (zonkEvTerm env) q
+ ; let co' = zonkIdOcc env co
+ ; q' <- mapM (zonkEvTerm env) q
; return (EvInstanceOfInst tys' co' q') }
zonkEvInstanceOf env (EvInstanceOfLet tys qvars bnds i)
= do { let qvars' = map (zonkIdOcc env) qvars
More information about the ghc-commits
mailing list