Commit b20ad447 authored by simonpj's avatar simonpj

[project @ 2001-07-23 10:24:57 by simonpj]

Yet another newtype-squashing bug; this time TcType.unifyTyX
parent 6ea86573
......@@ -1141,8 +1141,8 @@ tcImprove avails
unifyTauTy (substTy tenv t1) (substTy tenv t2)
ppr_eqn ((qtvs, t1, t2), doc)
= vcat [ptext SLIT("forall") <+> braces (pprWithCommas ppr (varSetElems qtvs))
<+> ppr t1 <+> equals <+> ppr t2,
doc]
<+> ppr t1 <+> ptext SLIT(":=:") <+> ppr t2,
nest 2 doc]
\end{code}
The main context-reduction function is @reduce@. Here's its game plan.
......
......@@ -752,6 +752,14 @@ uTysX ty1 (TyVarTy tyvar2) k subst@(tmpls,_)
| tyvar2 `elemVarSet` tmpls
= uVarX tyvar2 ty1 k subst
-- Predicates
uTysX (SourceTy (IParam n1 t1)) (SourceTy (IParam n2 t2)) k subst
| n1 == n2 = uTysX t1 t2 k subst
uTysX (SourceTy (ClassP c1 tys1)) (SourceTy (ClassP c2 tys2)) k subst
| c1 == c2 = uTyListsX tys1 tys2 k subst
uTysX (SourceTy (NType tc1 tys1)) (SourceTy (NType tc2 tys2)) k subst
| tc1 == tc2 = uTyListsX tys1 tys2 k subst
-- Functions; just check the two parts
uTysX (FunTy fun1 arg1) (FunTy fun2 arg2) k subst
= uTysX fun1 fun2 (uTysX arg1 arg2 k) subst
......@@ -891,6 +899,15 @@ match (TyVarTy v) ty tmpls k senv
-- variable may not match the pattern (TyVarTy v') as one would
-- expect, due to an intervening Note. KSW 2000-06.
-- Predicates
match (SourceTy (IParam n1 t1)) (SourceTy (IParam n2 t2)) tmpls k senv
| n1 == n2 = match t1 t2 tmpls k senv
match (SourceTy (ClassP c1 tys1)) (SourceTy (ClassP c2 tys2)) tmpls k senv
| c1 == c2 = match_list_exactly tys1 tys2 tmpls k senv
match (SourceTy (NType tc1 tys1)) (SourceTy (NType tc2 tys2)) tmpls k senv
| tc1 == tc2 = match_list_exactly tys1 tys2 tmpls k senv
-- Functions; just check the two parts
match (FunTy arg1 res1) (FunTy arg2 res2) tmpls k senv
= match arg1 arg2 tmpls (match res1 res2 tmpls k) senv
......@@ -900,11 +917,11 @@ match (AppTy fun1 arg1) ty2 tmpls k senv
Nothing -> Nothing -- Fail
match (TyConApp tc1 tys1) (TyConApp tc2 tys2) tmpls k senv
| tc1 == tc2 = match_tc_app tys1 tys2 tmpls k senv
| tc1 == tc2 = match_list_exactly tys1 tys2 tmpls k senv
-- Newtypes are opaque; other source types should not happen
match (SourceTy (NType tc1 tys1)) (SourceTy (NType tc2 tys2)) tmpls k senv
| tc1 == tc2 = match_tc_app tys1 tys2 tmpls k senv
| tc1 == tc2 = match_list_exactly tys1 tys2 tmpls k senv
match (UsageTy _ ty1) ty2 tmpls k senv = match ty1 ty2 tmpls k senv
match ty1 (UsageTy _ ty2) tmpls k senv = match ty1 ty2 tmpls k senv
......@@ -919,7 +936,7 @@ match ty1 (NoteTy n2 ty2) tmpls k senv = match ty1 ty2 tmpls k senv
-- Catch-all fails
match _ _ _ _ _ = Nothing
match_tc_app tys1 tys2 tmpls k senv
match_list_exactly tys1 tys2 tmpls k senv
= match_list tys1 tys2 tmpls k' senv
where
k' (senv', tys2') | null tys2' = k senv' -- Succeed
......
......@@ -264,20 +264,35 @@ mkEqnMsg (pred1,from1) (pred2,from2)
nest 2 (sep [ppr pred2 <> comma, nest 2 from2])]
----------
checkClsFD :: TyVarSet -- The quantified type variables, which
-- can be instantiated to make the types match
checkClsFD :: TyVarSet -- Quantified type variables; see note below
-> FunDep TyVar -> [TyVar] -- One functional dependency from the class
-> [Type] -> [Type]
-> [Equation]
checkClsFD qtvs fd clas_tvs tys1 tys2
-- 'qtvs' are the quantified type variables, the ones which an be instantiated
-- to make the types match. For example, given
-- class C a b | a->b where ...
-- instance C (Maybe x) (Tree x) where ..
-- and an Inst of form (C (Maybe t1 t2),
-- then we will call checkClsFD with
--
-- qtvs = {x}, tys1 = [Maybe x, Tree x]
-- tys2 = [Maybe t1, t2]
--
-- We can instantiate x to t1, and then we want to force
-- Tree x [t1/x] :=: t2
-- We use 'unify' even though we are often only matching
-- unifyTyListsX will only bind variables in qtvs, so it's OK!
= case unifyTyListsX qtvs ls1 ls2 of
Nothing -> []
Just unif -> [ (qtvs', substTy full_unif r1, substTy full_unif r2)
| (r1,r2) <- rs1 `zip` rs2,
not (maybeToBool (unifyExtendTysX qtvs unif r1 r2))]
not (maybeToBool (unifyExtendTysX qtvs' unif r1 r2))]
-- Don't include any equations that already hold
-- taking account of the fact that any qtvs that aren't
-- already instantiated can be instantiated to anything at all
where
full_unif = mkSubst emptyInScopeSet unif
-- No for-alls in sight; hmm
......
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