X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=compiler%2Ftypecheck%2FTcUnify.lhs;h=eba9985ad0e03509be04a3db41b3479d813a7ae6;hb=8c839b096be9a3fd44f4f681ed7f14fd95fe8ff9;hp=f9936e7f8765f5f57b30597e0e554eeee5af824b;hpb=d2b27dcd73c7d3aa21059e2a26ee7923fd7bca0a;p=ghc-hetmet.git

diff --git a/compiler/typecheck/TcUnify.lhs b/compiler/typecheck/TcUnify.lhs
index f9936e7..eba9985 100644
--- a/compiler/typecheck/TcUnify.lhs
+++ b/compiler/typecheck/TcUnify.lhs
@@ -65,8 +65,7 @@ import TyCon		( TyCon, tyConArity, tyConTyVars, isSynTyCon )
 import TysWiredIn	( listTyCon )
 import Id		( Id, mkSysLocal )
 import Var		( Var, varName, tyVarKind, isTcTyVar, tcTyVarDetails )
-import VarSet		( emptyVarSet, mkVarSet, unitVarSet, unionVarSet, elemVarSet, varSetElems,
-			  extendVarSet, intersectsVarSet )
+import VarSet
 import VarEnv
 import Name		( Name, isSystemName )
 import ErrUtils		( Message )
@@ -356,7 +355,9 @@ preSubType :: [TcTyVar]		-- Quantified type variables
 -- instantiate it to a monotype (non-boxy) type variable
 	
 preSubType qtvs btvs qty expected_ty
-  = mapM inst_tv qtvs
+  = do { tys <- mapM inst_tv qtvs
+	; traceTc (text "preSubType" <+> (ppr qtvs $$ ppr btvs $$ ppr qty $$ ppr expected_ty $$ ppr pre_subst $$ ppr tys))
+	; return tys }
   where
     pre_subst = boxySubMatchType (mkVarSet qtvs) qty expected_ty
     inst_tv tv	
@@ -375,26 +376,37 @@ boxySubMatchType
 -- "Boxy types: inference for higher rank types and impredicativity"
 
 boxySubMatchType tmpl_tvs tmpl_ty boxy_ty
-  = go tmpl_ty emptyVarSet boxy_ty
+  = go tmpl_tvs tmpl_ty emptyVarSet boxy_ty
   where
-    go t_ty b_tvs b_ty
-	| Just t_ty' <- tcView t_ty = go t_ty' b_tvs b_ty
-	| Just b_ty' <- tcView b_ty = go t_ty b_tvs b_ty'
+    go t_tvs t_ty b_tvs b_ty
+	| Just t_ty' <- tcView t_ty = go t_tvs t_ty' b_tvs b_ty
+	| Just b_ty' <- tcView b_ty = go t_tvs t_ty b_tvs b_ty'
 
-    go (TyVarTy _) b_tvs b_ty = emptyTvSubst	-- Rule S-ANY; no bindings
+    go t_tvs (TyVarTy _) b_tvs b_ty = emptyTvSubst	-- Rule S-ANY; no bindings
 	-- Rule S-ANY covers (a) type variables and (b) boxy types
 	-- in the template.  Both look like a TyVarTy.
 	-- See Note [Sub-match] below
 
-    go (ForAllTy tv t_ty) b_tvs b_ty = go t_ty b_tvs b_ty	-- Rule S-SPEC
-    go t_ty b_tvs (ForAllTy tv b_ty) = go t_ty b_tvs' b_ty	-- Rule S-SKOL
-	where b_tvs' = extendVarSet b_tvs tv
+    go t_tvs t_ty b_tvs b_ty
+	| isSigmaTy t_ty, (tvs, _, t_tau) <- tcSplitSigmaTy t_ty 
+	= go (t_tvs `delVarSetList` tvs) t_tau b_tvs b_ty	-- Rule S-SPEC
+		-- Under a forall on the left, if there is shadowing, 
+		-- do not bind! Hence the delVarSetList.
+	| isSigmaTy b_ty, (tvs, _, b_tau) <- tcSplitSigmaTy b_ty 
+	= go t_tvs t_ty (extendVarSetList b_tvs tvs) b_tau	-- Rule S-SKOL
+		-- Add to the variables we must not bind to
+	-- NB: it's *important* to discard the theta part. Otherwise
+	-- consider (forall a. Eq a => a -> b) ~<~ (Int -> Int -> Bool)
+	-- and end up with a completely bogus binding (b |-> Bool), by lining
+	-- up the (Eq a) with the Int, whereas it should be (b |-> (Int->Bool)).  
+	-- This pre-subsumption stuff can return too few bindings, but it 
+	-- must *never* return bogus info.
 							
-    go (FunTy arg1 res1) b_tvs (FunTy arg2 res2)	-- Rule S-FUN
-	= boxy_match tmpl_tvs arg1 b_tvs arg2 (go res1 b_tvs res2)
+    go t_tvs (FunTy arg1 res1) b_tvs (FunTy arg2 res2)	-- Rule S-FUN
+	= boxy_match t_tvs arg1 b_tvs arg2 (go t_tvs res1 b_tvs res2)
 	-- Match the args, and sub-match the results
 
-    go t_ty b_tvs b_ty = boxy_match tmpl_tvs t_ty b_tvs b_ty emptyTvSubst
+    go t_tvs t_ty b_tvs b_ty = boxy_match t_tvs t_ty b_tvs b_ty emptyTvSubst
 	-- Otherwise defer to boxy matching
 	-- This covers TyConApp, AppTy, PredTy
 \end{code}
@@ -434,9 +446,7 @@ boxyMatchTypes
 --	It does no unification, and cannot fail
 --
 -- Precondition: the arg lengths are equal
--- Precondition: none of the template type variables appear in the [BoxySigmaType]
--- Precondition: any nested quantifiers in either type differ from 
--- 		 the template type variables passed as arguments
+-- Precondition: none of the template type variables appear anywhere in the [BoxySigmaType]
 --
 	
 ------------
@@ -448,8 +458,9 @@ boxyMatchTypes tmpl_tvs tmpl_tys boxy_tys
 boxy_match_s tmpl_tvs [] boxy_tvs [] subst
   = subst
 boxy_match_s tmpl_tvs (t_ty:t_tys) boxy_tvs (b_ty:b_tys) subst
-  = boxy_match_s tmpl_tvs t_tys boxy_tvs b_tys $
-    boxy_match tmpl_tvs t_ty boxy_tvs b_ty subst
+  = boxy_match tmpl_tvs t_ty boxy_tvs b_ty $
+    boxy_match_s tmpl_tvs t_tys boxy_tvs b_tys subst
+    
 
 ------------
 boxy_match :: TcTyVarSet -> TcType	-- Template
@@ -470,8 +481,13 @@ boxy_match tmpl_tvs orig_tmpl_ty boxy_tvs orig_boxy_ty subst
 	| Just t_ty' <- tcView t_ty = go t_ty' b_ty
 	| Just b_ty' <- tcView b_ty = go t_ty b_ty'
 
-    go (ForAllTy _ ty1) (ForAllTy tv2 ty2)
-	= boxy_match tmpl_tvs ty1 (boxy_tvs `extendVarSet` tv2) ty2 subst
+    go ty1 ty2		-- C.f. the isSigmaTy case for boxySubMatchType
+	| isSigmaTy ty1
+	, (tvs1, _, tau1) <- tcSplitSigmaTy ty1
+	, (tvs2, _, tau2) <- tcSplitSigmaTy ty2
+	, equalLength tvs1 tvs2
+	= boxy_match (tmpl_tvs `delVarSetList` tvs1)    tau1 
+		     (boxy_tvs `extendVarSetList` tvs2) tau2 subst
 
     go (TyConApp tc1 tys1) (TyConApp tc2 tys2)
 	| tc1 == tc2 = go_s tys1 tys2
@@ -490,12 +506,20 @@ boxy_match tmpl_tvs orig_tmpl_ty boxy_tvs orig_boxy_ty subst
 	, not (intersectsVarSet boxy_tvs (tyVarsOfType orig_boxy_ty))
 	, typeKind b_ty `isSubKind` tyVarKind tv  -- See Note [Matching kinds]
 	= extendTvSubst subst tv boxy_ty'
+	| otherwise
+	= subst				-- Ignore others
 	where
 	  boxy_ty' = case lookupTyVar subst tv of
 			Nothing -> orig_boxy_ty
 			Just ty -> ty `boxyLub` orig_boxy_ty
 
-    go _ _ = subst	-- Always safe
+    go _ _ = emptyTvSubst	-- It's important to *fail* by returning the empty substitution
+	-- Example:  Tree a ~ Maybe Int
+	-- We do not want to bind (a |-> Int) in pre-matching, because that can give very
+	-- misleading error messages.  An even more confusing case is
+	--	     a -> b ~ Maybe Int
+	-- Then we do not want to bind (b |-> Int)!  It's always safe to discard bindings
+	-- from this pre-matching phase.
 
     --------
     go_s tys1 tys2 = boxy_match_s tmpl_tvs tys1 boxy_tvs tys2 subst
@@ -1491,7 +1515,7 @@ notMonoType ty
   = do	{ ty' <- zonkTcType ty
 	; env0 <- tcInitTidyEnv
 	; let (env1, tidy_ty) = tidyOpenType env0 ty'
-	      msg = ptext SLIT("Cannot match a monotype with") <+> ppr tidy_ty
+	      msg = ptext SLIT("Cannot match a monotype with") <+> quotes (ppr tidy_ty)
 	; failWithTcM (env1, msg) }
 
 occurCheck tyvar ty