[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 (file)
--- 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 (file)
--- 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