Make sure to zonk the kind of coercion variables
authorManuel M T Chakravarty <chak@cse.unsw.edu.au>
Wed, 1 Oct 2008 05:32:43 +0000 (05:32 +0000)
committerManuel M T Chakravarty <chak@cse.unsw.edu.au>
Wed, 1 Oct 2008 05:32:43 +0000 (05:32 +0000)
  MERGE TO 6.10

compiler/basicTypes/Var.lhs
compiler/typecheck/Inst.lhs
compiler/typecheck/TcHsSyn.lhs
compiler/typecheck/TcMType.lhs
compiler/typecheck/TcPat.lhs
compiler/typecheck/TcSimplify.lhs

index eec6c80..ee09c3e 100644 (file)
@@ -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}
 
 %************************************************************************
index c009ebe..5ad0bed 100644 (file)
@@ -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, 
index fe9c808..7e15770 100644 (file)
@@ -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) }
index 02de940..543c61c 100644 (file)
@@ -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}
 
 
index 2e86583..2a2409e 100644 (file)
@@ -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)
 
index a274cab..113de25 100644 (file)
@@ -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