Commit 1add6282 authored by chak@cse.unsw.edu.au.'s avatar chak@cse.unsw.edu.au.

Make sure to zonk the kind of coercion variables

  MERGE TO 6.10
parent eb90092d
......@@ -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}
%************************************************************************
......
......@@ -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,
......
......@@ -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) }
......
......@@ -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}
......
......@@ -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)
......
......@@ -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
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment