Make the treatment of equalities more uniform

This patch (which is part of the fix for Trac #2018) makes coercion variables
be handled more uniformly.  Generally, they are treated like dictionaries
in the type checker, not like type variables, but in a couple of places we
were treating them like type variables.  Also when zonking we should use
zonkDictBndr not zonkIdBndr.

diff --git a/compiler/hsSyn/HsBinds.lhs b/compiler/hsSyn/HsBinds.lhs
index 2fa2959..90442df 100644 (file)
--- a/compiler/hsSyn/HsBinds.lhs
+++ b/compiler/hsSyn/HsBinds.lhs
@@ -343,8 +343,8 @@ data HsWrapper
 
   | WpApp Var                  -- [] d         the 'd' is a type-class dictionary
   | WpTyApp Type               -- [] t         the 't' is a type or corecion
-  | WpLam Id                   -- \d. []       the 'd' is a type-class dictionary
-  | WpTyLam TyVar              -- \a. []       the 'a' is a type or coercion variable
+  | WpLam Var                  -- \d. []       the 'd' is a type-class dictionary or coercion variable
+  | WpTyLam TyVar              -- \a. []       the 'a' is a type variable (not coercion var)
   | WpInline                   -- inline_me []   Wrap inline around the thing
 
        -- Non-empty bindings, so that the identity coercion

diff --git a/compiler/hsSyn/HsPat.lhs b/compiler/hsSyn/HsPat.lhs
index a524ab8..87f4717 100644 (file)
--- a/compiler/hsSyn/HsPat.lhs
+++ b/compiler/hsSyn/HsPat.lhs
@@ -97,9 +97,10 @@ data Pat id
 
   | ConPatOut {
        pat_con   :: Located DataCon,
-       pat_tvs   :: [TyVar],           -- Existentially bound type variables
-                                       --   including any bound coercion variables
-       pat_dicts :: [id],              -- Ditto dictionaries
+       pat_tvs   :: [TyVar],           -- Existentially bound type variables (tyvars only)
+       pat_dicts :: [id],              -- Ditto *coercion variables* and *dictionaries*
+                                       -- One reason for putting coercion variable here, I think,
+                                       --      is to ensure their kinds are zonked
        pat_binds :: DictBinds id,      -- Bindings involving those dictionaries
        pat_args  :: HsConPatDetails id,
        pat_ty    :: Type               -- The type of the pattern

diff --git a/compiler/typecheck/TcHsSyn.lhs b/compiler/typecheck/TcHsSyn.lhs
index ff5c942..bd3cb8c 100644 (file)
--- a/compiler/typecheck/TcHsSyn.lhs
+++ b/compiler/typecheck/TcHsSyn.lhs
@@ -550,7 +550,7 @@ zonkCoFn env (WpCompose c1 c2) = do { (env1, c1') <- zonkCoFn env c1
                                    ; return (env2, WpCompose c1' c2') }
 zonkCoFn env (WpCo co)      = do { co' <- zonkTcTypeToType env co
                                 ; return (env, WpCo co') }
-zonkCoFn env (WpLam id)     = do { id' <- zonkIdBndr env id
+zonkCoFn env (WpLam id)     = do { id' <- zonkDictBndr env id
                                 ; let env1 = extendZonkEnv1 env id'
                                 ; return (env1, WpLam id') }
 zonkCoFn env (WpTyLam tv)   = ASSERT( isImmutableTyVar tv )
@@ -776,7 +776,7 @@ zonk_pat env (TuplePat pats boxed ty)
 zonk_pat env p@(ConPatOut { pat_ty = ty, pat_dicts = dicts, pat_binds = binds, pat_args = args })
   = ASSERT( all isImmutableTyVar (pat_tvs p) ) 
     do { new_ty <- zonkTcTypeToType env ty
-       ; new_dicts <- zonkIdBndrs env dicts
+       ; new_dicts <- zonkDictBndrs env dicts
        ; let env1 = extendZonkEnv env new_dicts
        ; (env2, new_binds) <- zonkRecMonoBinds env1 binds
        ; (env', new_args) <- zonkConStuff env2 args

diff --git a/compiler/typecheck/TcMType.lhs b/compiler/typecheck/TcMType.lhs
index f1f9082..f7cbb2c 100644 (file)
--- a/compiler/typecheck/TcMType.lhs
+++ b/compiler/typecheck/TcMType.lhs
@@ -104,6 +104,7 @@ import Data.List    ( (\\) )
 tcInstType :: ([TyVar] -> TcM [TcTyVar])               -- How to instantiate the type variables
           -> TcType                                    -- Type to instantiate
           -> TcM ([TcTyVar], TcThetaType, TcType)      -- Result
+               -- (type vars (excl coercion vars), preds (incl equalities), rho)
 tcInstType inst_tyvars ty
   = case tcSplitForAllTys ty of
        ([],     rho) -> let    -- There may be overloading despite no type variables;

diff --git a/compiler/typecheck/TcSimplify.lhs b/compiler/typecheck/TcSimplify.lhs
index 433266e..be9d70d 100644 (file)
--- a/compiler/typecheck/TcSimplify.lhs
+++ b/compiler/typecheck/TcSimplify.lhs
@@ -2207,7 +2207,7 @@ reduceImplication env
                        --              it makes no difference
                co  = wrap_inline       -- Note [Always inline implication constraints]
                      <.> mkWpTyLams tvs
-                     <.> mkWpTyLams eq_tyvars
+                     <.> mkWpLams eq_tyvars
                      <.> mkWpLams dict_ids
                      <.> WpLet (binds `unionBags` bind)
                wrap_inline | null dict_ids = idHsWrapper

diff --git a/compiler/typecheck/TcTyFuns.lhs b/compiler/typecheck/TcTyFuns.lhs
index ca3c4a8..706fe2f 100644 (file)
--- a/compiler/typecheck/TcTyFuns.lhs
+++ b/compiler/typecheck/TcTyFuns.lhs
@@ -233,7 +233,7 @@ tcGenericNormaliseFamInst fun (ForAllTy tyvar ty1)
        }
 tcGenericNormaliseFamInst fun (NoteTy note ty1)
   = do { (coi,nty1) <- tcGenericNormaliseFamInst fun ty1
-       ; return (mkNoteTyCoI note coi, NoteTy note nty1)
+       ; return (coi, NoteTy note nty1)
        }
 tcGenericNormaliseFamInst fun ty@(TyVarTy tv)
   | isTcTyVar tv

diff --git a/compiler/typecheck/TcType.lhs b/compiler/typecheck/TcType.lhs
index 625f855..165018d 100644 (file)
--- a/compiler/typecheck/TcType.lhs
+++ b/compiler/typecheck/TcType.lhs
@@ -670,9 +670,7 @@ tcSplitPhiTy ty = split ty ty []
   split orig_ty ty tvs | Just ty' <- tcView ty = split orig_ty ty' tvs
 
   split orig_ty (ForAllTy tv ty) ts
-        | isCoVar tv = split ty ty (eq_pred:ts)
-        where
-           PredTy eq_pred = tyVarKind tv
+        | isCoVar tv = split ty ty (coVarPred tv : ts)
   split orig_ty (FunTy arg res) ts 
        | Just p <- tcSplitPredTy_maybe arg = split res res (p:ts)
   split orig_ty ty             ts = (reverse ts, orig_ty)

diff --git a/compiler/typecheck/TcUnify.lhs b/compiler/typecheck/TcUnify.lhs
index 0893850..1acef7c 100644 (file)
--- a/compiler/typecheck/TcUnify.lhs
+++ b/compiler/typecheck/TcUnify.lhs
@@ -924,7 +924,7 @@ tcGen expected_ty extra_tvs thing_inside    -- We expect expected_ty to be a forall
        -- list of "free vars" for the signature check.
 
        ; loc <- getInstLoc (SigOrigin skol_info)
-       ; dicts <- newDictBndrs loc theta'
+       ; dicts <- newDictBndrs loc theta'      -- Includes equalities
        ; inst_binds <- tcSimplifyCheck loc tvs' dicts lie
 
        ; checkSigTyVarsWrt free_tvs tvs'

diff --git a/compiler/types/FamInstEnv.lhs b/compiler/types/FamInstEnv.lhs
index a9e1548..12df25d 100644 (file)
--- a/compiler/types/FamInstEnv.lhs
+++ b/compiler/types/FamInstEnv.lhs
@@ -437,7 +437,7 @@ normaliseType env ty@(ForAllTy tyvar ty1)
     in  (mkForAllTyCoI tyvar coi,ForAllTy tyvar nty1)
 normaliseType env ty@(NoteTy note ty1)
   = let (coi,nty1) = normaliseType env ty1
-    in  (mkNoteTyCoI note coi,NoteTy note nty1)
+    in  (coi,NoteTy note nty1)
 normaliseType env ty@(TyVarTy _)
   = (IdCo,ty)
 normaliseType env (PredTy predty)

diff --git a/compiler/types/TypeRep.lhs b/compiler/types/TypeRep.lhs
index c694dc8..69ee419 100644 (file)
--- a/compiler/types/TypeRep.lhs
+++ b/compiler/types/TypeRep.lhs
@@ -31,6 +31,7 @@ module TypeRep (
         argTypeKind, ubxTupleKind,
        isLiftedTypeKindCon, isLiftedTypeKind,
        mkArrowKind, mkArrowKinds, isCoercionKind,
+       coVarPred,
 
         -- Kind constructors...
         liftedTypeKindTyCon, openTypeKindTyCon, unliftedTypeKindTyCon,
@@ -412,6 +413,13 @@ isCoercionKind :: Kind -> Bool
 isCoercionKind (NoteTy _ k)         = isCoercionKind k
 isCoercionKind (PredTy (EqPred {})) = True
 isCoercionKind other               = False
+
+coVarPred :: CoVar -> PredType
+coVarPred tv
+  = ASSERT( isCoVar tv )
+    case tyVarKind tv of
+       PredTy eq -> eq         -- There shouldn't even be a NoteTy in the way
+       other     -> pprPanic "coVarPred" (ppr tv $$ ppr other)
 \end{code}
 
 
@@ -484,7 +492,7 @@ pprParendKind = pprParendType
 ppr_type :: Prec -> Type -> SDoc
 ppr_type p (TyVarTy tv)       = ppr tv
 ppr_type p (PredTy pred)      = ifPprDebug (ptext SLIT("<pred>")) <> (ppr pred)
-ppr_type p (NoteTy other ty2) = ppr_type p ty2
+ppr_type p (NoteTy other ty2) = ifPprDebug (ptext SLIT("<note>")) <> ppr_type p ty2
 ppr_type p (TyConApp tc tys)  = ppr_tc_app p tc tys
 
 ppr_type p (AppTy t1 t2) = maybeParen p TyConPrec $
@@ -504,28 +512,27 @@ ppr_type p (FunTy ty1 ty2)
 ppr_forall_type :: Prec -> Type -> SDoc
 ppr_forall_type p ty
   = maybeParen p FunPrec $
-    sep [pprForAll tvs, pprThetaArrow (ctxt1 ++ ctxt2), pprType tau]
+    sep [pprForAll tvs, pprThetaArrow ctxt, pprType tau]
   where
-    (tvs, ctxt1, rho) = split1 [] [] ty
-    (ctxt2, tau)      = split2 [] rho
+    (tvs,  rho) = split1 [] ty
+    (ctxt, tau) = split2 [] rho
 
     -- We need to be extra careful here as equality constraints will occur as
     -- type variables with an equality kind.  So, while collecting quantified
     -- variables, we separate the coercion variables out and turn them into
     -- equality predicates.
-    split1 tvs eqs (ForAllTy tv ty) 
-      | isCoVar tv               = split1 tvs (eq:eqs) ty
-      | otherwise                = split1 (tv:tvs) eqs ty
-      where
-        PredTy eq = tyVarKind tv
-    split1 tvs eqs (NoteTy _ ty) = split1 tvs eqs ty
-    split1 tvs eqs ty           = (reverse tvs, reverse eqs, ty)
+    split1 tvs (ForAllTy tv ty) 
+      | not (isCoVar tv)     = split1 (tv:tvs) ty
+    split1 tvs (NoteTy _ ty) = split1 tvs ty
+    split1 tvs ty           = (reverse tvs, ty)
  
     split2 ps (NoteTy _ arg    -- Rather a disgusting case
-              `FunTy` res)           = split2 ps (arg `FunTy` res)
-    split2 ps (PredTy p `FunTy` ty)   = split2 (p:ps) ty
-    split2 ps (NoteTy _ ty)          = split2 ps ty
-    split2 ps ty                     = (reverse ps, ty)
+              `FunTy` res)         = split2 ps (arg `FunTy` res)
+    split2 ps (PredTy p `FunTy` ty) = split2 (p:ps) ty
+    split2 ps (ForAllTy tv ty) 
+       | isCoVar tv                = split2 (coVarPred tv : ps) ty
+    split2 ps (NoteTy _ ty)        = split2 ps ty
+    split2 ps ty                   = (reverse ps, ty)
 
 ppr_tc_app :: Prec -> TyCon -> [Type] -> SDoc
 ppr_tc_app p tc []