Make sure to zonk the kind of coercion variables

  MERGE TO 6.10

6 files changed, 57 insertions, 39 deletions

diff --git a/compiler/basicTypes/Var.lhs b/compiler/basicTypes/Var.lhs
index eec6c803b4..ee09c3eedd 100644
--- a/compiler/basicTypes/Var.lhs
+++ b/compiler/basicTypes/Var.lhs
@@ -288,7 +288,7 @@ mkTcTyVar name kind details
 %************************************************************************
 
 \begin{code}
-type CoVar = Var -- A coercion variable is simply a type 
+type CoVar = TyVar -- A coercion variable is simply a type 
 			-- variable of kind @ty1 :=: ty2@. Hence its
 			-- 'varType' is always @PredTy (EqPred t1 t2)@
 
@@ -310,16 +310,9 @@ mkCoVar name kind = ASSERT( isCoercionKind kind )
 			}
 
 mkWildCoVar :: Kind -> TyVar
--- ^ Create a type variable that is never referred to, so its unique doesn't matter
-mkWildCoVar kind 
-  = ASSERT( isCoercionKind kind )
-    TyVar { varName = mkSysTvName wild_uniq (fsLit "co_wild"),
-            realUnique = _ILIT(1),
-            varType = kind,
-            isCoercionVar = True }
-  where
-    wild_uniq = mkBuiltinUnique 1
-
+-- ^ Create a type variable that is never referred to, so its unique doesn't 
+-- matter
+mkWildCoVar = mkCoVar (mkSysTvName (mkBuiltinUnique 1) (fsLit "co_wild"))
 \end{code}
 
 %************************************************************************
diff --git a/compiler/typecheck/Inst.lhs b/compiler/typecheck/Inst.lhs
index c009ebe083..5ad0bed317 100644
--- a/compiler/typecheck/Inst.lhs
+++ b/compiler/typecheck/Inst.lhs
@@ -287,7 +287,7 @@ newDictBndr :: InstLoc -> TcPredType -> TcM Inst
 newDictBndr inst_loc pred@(EqPred ty1 ty2)
   = do { uniq <- newUnique 
 	; let name = mkPredName uniq inst_loc pred 
-	      co = mkGivenCo $ TyVarTy (Var.mkCoVar name (PredTy pred))
+	      co   = mkGivenCo $ TyVarTy (Var.mkCoVar name (PredTy pred))
 	; return (EqInst {tci_name  = name, 
 			  tci_loc   = inst_loc, 
 			  tci_left  = ty1, 
diff --git a/compiler/typecheck/TcHsSyn.lhs b/compiler/typecheck/TcHsSyn.lhs
index fe9c808be8..7e15770270 100644
--- a/compiler/typecheck/TcHsSyn.lhs
+++ b/compiler/typecheck/TcHsSyn.lhs
@@ -251,11 +251,22 @@ zonkDictBndrs :: ZonkEnv -> [Var] -> TcM [Var]
 zonkDictBndrs env ids = mappM (zonkDictBndr env) ids
 
 zonkDictBndr :: ZonkEnv -> Var -> TcM Var
-zonkDictBndr env var | isTyVar var = return var
+zonkDictBndr env var | isTyVar var = zonkTyVarBndr env var
 		     | otherwise   = zonkIdBndr env var
 
 zonkTopBndrs :: [TcId] -> TcM [Id]
 zonkTopBndrs ids = zonkIdBndrs emptyZonkEnv ids
+
+-- Zonk the kind of a non-TC tyvar in case it is a coercion variable (their
+-- kind contains types).
+--
+zonkTyVarBndr :: ZonkEnv -> TyVar -> TcM TyVar
+zonkTyVarBndr env tv
+  | isCoVar tv
+  = do { kind <- zonkTcTypeToType env (tyVarKind tv)
+       ; return $ setTyVarKind tv kind
+       }
+  | otherwise = return tv
 \end{code}
 
 
@@ -607,7 +618,8 @@ 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 )
-			      return (env, WpTyLam tv)
+                              do { tv' <- zonkTyVarBndr env tv
+			         ; return (env, WpTyLam tv') }
 zonkCoFn env (WpApp v)
 	| isTcTyVar v  	    = do { co <- zonkTcTyVar v
 				 ; return (env, WpTyApp co) }
diff --git a/compiler/typecheck/TcMType.lhs b/compiler/typecheck/TcMType.lhs
index 02de94079a..543c61c195 100644
--- a/compiler/typecheck/TcMType.lhs
+++ b/compiler/typecheck/TcMType.lhs
@@ -763,8 +763,11 @@ zonkQuantifiedTyVar :: TcTyVar -> TcM TcTyVar
 --
 -- We leave skolem TyVars alone; they are immutable.
 zonkQuantifiedTyVar tv
-  | ASSERT( isTcTyVar tv ) 
-    isSkolemTyVar tv = return tv
+  | ASSERT2( isTcTyVar tv, ppr tv ) 
+    isSkolemTyVar tv 
+  = do { kind <- zonkTcType (tyVarKind tv)
+       ; return $ setTyVarKind tv kind
+       }
 	-- It might be a skolem type variable, 
 	-- for example from a user type signature
 
@@ -896,12 +899,14 @@ zonkType unbound_var_fn ty
 
 	-- The two interesting cases!
     go (TyVarTy tyvar) | isTcTyVar tyvar = zonk_tc_tyvar unbound_var_fn tyvar
-		       | otherwise	 = return (TyVarTy tyvar)
+		       | otherwise	 = liftM TyVarTy $ 
+                                             zonkTyVar unbound_var_fn tyvar
 		-- Ordinary (non Tc) tyvars occur inside quantified types
 
     go (ForAllTy tyvar ty) = ASSERT( isImmutableTyVar tyvar ) do
                              ty' <- go ty
-                             return (ForAllTy tyvar ty')
+                             tyvar' <- zonkTyVar unbound_var_fn tyvar
+                             return (ForAllTy tyvar' ty')
 
     go_pred (ClassP c tys)   = do tys' <- mapM go tys
                                   return (ClassP c tys')
@@ -911,7 +916,7 @@ zonkType unbound_var_fn ty
                                   ty2' <- go ty2
                                   return (EqPred ty1' ty2')
 
-zonk_tc_tyvar :: (TcTyVar -> TcM Type)		-- What to do for an unbound mutable variable
+zonk_tc_tyvar :: (TcTyVar -> TcM Type)	-- What to do for an unbound mutable var
  	      -> TcTyVar -> TcM TcType
 zonk_tc_tyvar unbound_var_fn tyvar 
   | not (isMetaTyVar tyvar)	-- Skolems
@@ -922,6 +927,18 @@ zonk_tc_tyvar unbound_var_fn tyvar
 	; case cts of
 	    Flexi       -> unbound_var_fn tyvar    -- Unbound meta type variable
 	    Indirect ty -> zonkType unbound_var_fn ty  }
+
+-- Zonk the kind of a non-TC tyvar in case it is a coercion variable (their
+-- kind contains types).
+--
+zonkTyVar :: (TcTyVar -> TcM Type)      -- What to do for an unbound mutable var
+ 	  -> TyVar -> TcM TyVar
+zonkTyVar unbound_var_fn tv 
+  | isCoVar tv
+  = do { kind <- zonkType unbound_var_fn (tyVarKind tv)
+       ; return $ setTyVarKind tv kind
+       }
+  | otherwise = return tv
 \end{code}
 
 
diff --git a/compiler/typecheck/TcPat.lhs b/compiler/typecheck/TcPat.lhs
index 2e865835b6..2a2409e7ba 100644
--- a/compiler/typecheck/TcPat.lhs
+++ b/compiler/typecheck/TcPat.lhs
@@ -617,10 +617,6 @@ tcConPat pstate con_span data_con tycon pat_ty arg_pats thing_inside
                 where
                   uwScrut = unwrapFamInstScrutinee tycon ctxt_res_tys res_pat
 
-        ; traceTc $ case sym_coi of
-                      IdCo -> text "sym_coi:IdCo" 
-                      ACo co -> text "sym_coi: ACoI" <+> ppr co
-
 	  -- Add the stupid theta
 	; addDataConStupidTheta data_con ctxt_res_tys
 
@@ -655,7 +651,7 @@ tcConPat pstate con_span data_con tycon pat_ty arg_pats thing_inside
           -- ex_tvs was non-null.
 --        ; unless (null theta') $
           -- FIXME: AT THE MOMENT WE CHEAT!  We only perform the rigidity test
-          --   if we explicit or implicit (by a GADT def) have equality 
+          --   if we explicitly or implicitly (by a GADT def) have equality 
           --   constraints.
         ; let eq_preds = [mkEqPred (mkTyVarTy tv, ty) | (tv, ty) <- eq_spec]
 	      theta'   = substTheta tenv (eq_preds ++ full_theta)
@@ -665,8 +661,8 @@ tcConPat pstate con_span data_con tycon pat_ty arg_pats thing_inside
 	      pstate' | no_equalities = pstate
 		      | otherwise     = pstate { pat_eqs = True }
 
-	; unless no_equalities (checkTc (isRigidTy pat_ty)
-                                        (nonRigidMatch data_con))
+	; unless no_equalities $ 
+            checkTc (isRigidTy pat_ty) (nonRigidMatch data_con)
 
 	; ((arg_pats', inner_tvs, res), lie_req) <- getLIE $
 		tcConArgs data_con arg_tys' arg_pats pstate' thing_inside
@@ -719,7 +715,6 @@ tcConPat pstate con_span data_con tycon pat_ty arg_pats thing_inside
       | otherwise
       = pat
 
-
 tcConArgs :: DataCon -> [TcSigmaType]
 	  -> Checker (HsConPatDetails Name) (HsConPatDetails Id)
 
diff --git a/compiler/typecheck/TcSimplify.lhs b/compiler/typecheck/TcSimplify.lhs
index a274cab231..113de258ac 100644
--- a/compiler/typecheck/TcSimplify.lhs
+++ b/compiler/typecheck/TcSimplify.lhs
@@ -2211,7 +2211,8 @@ Note that
 reduceImplication env
 	orig_implic@(ImplicInst { tci_name = name, tci_loc = inst_loc,
 		      	   	  tci_tyvars = tvs,
-		      	   	  tci_given = extra_givens, tci_wanted = wanteds })
+		      	   	  tci_given = extra_givens, tci_wanted = wanteds
+                                })
   = do	{ 	-- Solve the sub-problem
 	; let try_me _ = ReduceMe  -- Note [Freeness and implications]
 	      env' = env { red_givens = extra_givens ++ red_givens env
@@ -2225,13 +2226,6 @@ reduceImplication env
 			[ ppr (red_givens env), ppr extra_givens, 
 			  ppr wanteds])
 	; (irreds, binds) <- checkLoop env' wanteds
-	; let   (extra_eq_givens, extra_dict_givens) = partition isEqInst extra_givens
-			-- SLPJ Sept 07: I think this is bogus; currently
-			-- there are no Eqinsts in extra_givens
-		dict_ids = map instToId extra_dict_givens 
-
-		-- Note [Reducing implication constraints]
-		-- Tom -- update note, put somewhere!
 
 	; traceTc (text "reduceImplication result" <+> vcat
 			[ppr irreds, ppr binds])
@@ -2251,8 +2245,6 @@ reduceImplication env
                           -- we may have instantiated a cotv 
                           -- => must make a new implication constraint!
 
-	; traceTc $ text "reduceImplication condition" <+> ppr backOff
-
           -- Progress is no longer measered by the number of bindings
 	; if backOff then 	-- No progress
 		-- If there are any irreds, we back off and do nothing
@@ -2271,13 +2263,22 @@ reduceImplication env
 		--  equations depending on whether we solve
 		--  dictionary constraints or equational constraints
 
-		eq_tyvars = varSetElems $ tyVarsOfTypes $ map eqInstType extra_eq_givens
+	        (extra_eq_givens, extra_dict_givens) 
+                  = partition isEqInst extra_givens
+			-- SLPJ Sept 07: I think this is bogus; currently
+			-- there are no Eqinsts in extra_givens
+		dict_ids = map instToId extra_dict_givens 
+
+		-- Note [Reducing implication constraints]
+		-- Tom -- update note, put somewhere!
+	; let	eq_tyvars = varSetElems $ tyVarsOfTypes $ 
+                              map eqInstType extra_eq_givens
 			-- SLPJ Sept07: this looks Utterly Wrong to me, but I think
 			--	        that current extra_givens has no EqInsts, so
 			--		it makes no difference
 		co  = wrap_inline	-- Note [Always inline implication constraints]
 		      <.> mkWpTyLams tvs
-		      <.> mkWpLams eq_tyvars
+		      <.> mkWpTyLams eq_tyvars
 		      <.> mkWpLams dict_ids
 		      <.> WpLet (binds `unionBags` bind)
 		wrap_inline | null dict_ids = idHsWrapper