From: simonpj <unknown>
Date: Fri, 21 Jun 2002 13:34:43 +0000 (+0000)
Subject: [project @ 2002-06-21 13:34:42 by simonpj]
X-Git-Tag: Approx_11550_changesets_converted~1939
X-Git-Url: http://git.megacz.com/?a=commitdiff_plain;ds=sidebyside;h=e91b5dcbdd7217212110a4bebb6da365ade2d961;p=ghc-hetmet.git

[project @ 2002-06-21 13:34:42 by simonpj]
---------------------------------------------
	    Calculate the free vars of a type 'right'
	---------------------------------------------

	type C u a = u

Question: is 'a' free in 'C u a'?

I think the answer should be 'no'; see typecheck/should_compile/tc157.hs
for an example of why it matters.  This commit makes it so, and adds
comments to explain a dark corner in the zonking code.
---

diff --git a/ghc/compiler/typecheck/TcMType.lhs b/ghc/compiler/typecheck/TcMType.lhs
index 28c45f0..faa7827 100644
--- a/ghc/compiler/typecheck/TcMType.lhs
+++ b/ghc/compiler/typecheck/TcMType.lhs
@@ -445,11 +445,45 @@ zonkTcTyVarToTyVar tv
 	-- so that all other occurrences of the tyvar will get zapped too
     zonkTyVar zap tv		`thenNF_Tc` \ ty2 ->
 
+	-- This warning shows up if the allegedly-unbound tyvar is
+	-- already bound to something.  It can actually happen, and 
+	-- in a harmless way (see [Silly Type Synonyms] below) so
+	-- it's only a warning
     WARN( not (immut_tv_ty `tcEqType` ty2), ppr tv $$ ppr immut_tv $$ ppr ty2 )
 
     returnNF_Tc immut_tv
 \end{code}
 
+[Silly Type Synonyms]
+
+Consider this:
+	type C u a = u	-- Note 'a' unused
+
+	foo :: (forall a. C u a -> C u a) -> u
+	foo x = ...
+
+	bar :: Num u => u
+	bar = foo (\t -> t + t)
+
+* From the (\t -> t+t) we get type  {Num d} =>  d -> d
+  where d is fresh.
+
+* Now unify with type of foo's arg, and we get:
+	{Num (C d a)} =>  C d a -> C d a
+  where a is fresh.
+
+* Now abstract over the 'a', but float out the Num (C d a) constraint
+  because it does not 'really' mention a.  (see Type.tyVarsOfType)
+  The arg to foo becomes
+	/\a -> \t -> t+t
+
+* So we get a dict binding for Num (C d a), which is zonked to give
+	a = ()
+
+* Then the /\a abstraction has a zonked 'a' in it.
+
+All very silly.   I think its harmless to ignore the problem.
+
 
 %************************************************************************
 %*									*
diff --git a/ghc/compiler/types/Type.lhs b/ghc/compiler/types/Type.lhs
index 93a421a..ad7d1c9 100644
--- a/ghc/compiler/types/Type.lhs
+++ b/ghc/compiler/types/Type.lhs
@@ -602,12 +602,27 @@ tyVarsOfType :: Type -> TyVarSet
 tyVarsOfType (TyVarTy tv)		= unitVarSet tv
 tyVarsOfType (TyConApp tycon tys)	= tyVarsOfTypes tys
 tyVarsOfType (NoteTy (FTVNote tvs) ty2) = tvs
-tyVarsOfType (NoteTy (SynNote ty1) ty2)	= tyVarsOfType ty1
+tyVarsOfType (NoteTy (SynNote ty1) ty2)	= tyVarsOfType ty2	-- See note [Syn] below
 tyVarsOfType (SourceTy sty)		= tyVarsOfSourceType sty
 tyVarsOfType (FunTy arg res)		= tyVarsOfType arg `unionVarSet` tyVarsOfType res
 tyVarsOfType (AppTy fun arg)		= tyVarsOfType fun `unionVarSet` tyVarsOfType arg
 tyVarsOfType (ForAllTy tyvar ty)	= tyVarsOfType ty `minusVarSet` unitVarSet tyvar
 
+-- 			Note [Syn]
+-- Consider
+--	type T a = Int
+-- What are the free tyvars of (T x)?  Empty, of course!  
+-- Here's the example that Ralf Laemmel showed me:
+--	foo :: (forall a. C u a -> C u a) -> u
+--	mappend :: Monoid u => u -> u -> u
+--
+--	bar :: Monoid u => u
+--	bar = foo (\t -> t `mappend` t)
+-- We have to generalise at the arg to f, and we don't
+-- want to capture the constraint (Monad (C u a)) because
+-- it appears to mention a.  Pretty silly, but it was useful to him.
+
+
 tyVarsOfTypes :: [Type] -> TyVarSet
 tyVarsOfTypes tys = foldr (unionVarSet.tyVarsOfType) emptyVarSet tys