Commit f8c8de8e authored by Simon Peyton Jones's avatar Simon Peyton Jones

Zonk the free tvs of a RULE lhs to TyVars

Previously we were making them into skolem TcTyVars,
which is wrong for the output of the type checker, which
no TcTyVars should surive.

See Note [Zonking the LHS of a RULE] in TcHsSyn

This was flushed out by the new IfaceTcTyVar thing;
I found some more TcTyVars that were being serialised into
an interface file, which is wrong wrong wrong.
parent abd4a4c1
......@@ -895,7 +895,7 @@ Consider
After type checking the LHS becomes (foo alpha (C alpha)), where alpha
is an unbound meta-tyvar. The zonker in TcHsSyn is careful not to
turn the free alpha into Any (as it usually does). Instead it turns it
into a skolem 'a'. See TcHsSyn Note [Zonking the LHS of a RULE].
into a TyVar 'a'. See TcHsSyn Note [Zonking the LHS of a RULE].
Now we must quantify over that 'a'. It's /really/ inconvenient to do that
in the zonker, because the HsExpr data type is very large. But it's /easy/
......
......@@ -187,7 +187,9 @@ the environment manipulation is tiresome.
-- Confused by zonking? See Note [What is zonking?] in TcMType.
type UnboundTyVarZonker = TcTyVar -> TcM Type
-- How to zonk an unbound type variable
-- The TcTyVar is (a) a MetaTv (b) Flexi and
-- The TcTyVar is
-- (a) a MetaTv
-- (b) Flexi and
-- (c) its kind is alrady zonked
-- Note [Zonking the LHS of a RULE]
......@@ -1617,8 +1619,13 @@ zonkTvSkolemising :: UnboundTyVarZonker
-- This variant is used for the LHS of rules
-- See Note [Zonking the LHS of a RULE].
zonkTvSkolemising tv
= do { tv' <- skolemiseUnboundMetaTyVar tv
; return (mkTyVarTy tv') }
= do { let tv' = mkTyVar (tyVarName tv) (tyVarKind tv)
-- NB: the kind of tv is already zonked
ty = mkTyVarTy tv'
-- Make a proper TyVar (remember we
-- are now done with type checking)
; writeMetaTyVar tv ty
; return ty }
zonkTypeZapping :: UnboundTyVarZonker
-- This variant is used for everything except the LHS of rules
......@@ -1652,9 +1659,10 @@ over it!
We do this in two stages.
* During zonking, we skolemise 'alpha' to 'a'. We do this by using
zonkTvSkolemising as the UnboundTyVarZonker in the ZonkEnv.
(This is the whole reason that the ZonkEnv has a UnboundTyVarZonker.)
* During zonking, we skolemise the TcTyVar 'alpha' to TyVar 'a'. We
do this by using zonkTvSkolemising as the UnboundTyVarZonker in the
ZonkEnv. (This is in fact the whole reason that the ZonkEnv has a
UnboundTyVarZonker.)
* In DsBinds, we quantify over it. See DsBinds
Note [Free tyvars on rule LHS]
......
......@@ -68,7 +68,7 @@ module TcMType (
zonkTidyTcType, zonkTidyOrigin,
mkTypeErrorThing, mkTypeErrorThingArgs,
tidyEvVar, tidyCt, tidySkolemInfo,
skolemiseUnboundMetaTyVar, skolemiseRuntimeUnk,
skolemiseRuntimeUnk,
zonkTcTyVar, zonkTcTyVars, zonkTcTyVarToTyVar,
zonkTyCoVarsAndFV, zonkTcTypeAndFV,
zonkTyCoVarsAndFVList,
......
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