Commit e91b5dcb authored by simonpj's avatar simonpj
Browse files

[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.
parent f2123a38
......@@ -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.
%************************************************************************
%* *
......
......@@ -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
......
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