Commit bf1bf9fb authored by's avatar
Browse files

Remove GADT refinements, part 4

- MkId.mkRecordSelId only used a special case of refineGadt, which doesn't
  need full unification.  That special case is now implemented as 
  TcGadt.matchRefine and TcGadt.refineGadt can finally go.
parent 3023a007
......@@ -594,8 +594,8 @@ mkRecordSelId tycon field_label
-- Allocate Ids. We do it a funny way round because field_dict_tys is
-- almost always empty. Also note that we use max_dict_tys
-- rather than n_dict_tys, because the latter gives an infinite loop:
-- n_dict tys depends on the_alts, which depens on arg_ids, which depends
-- on arity, which depends on n_dict tys. Sigh! Mega sigh!
-- n_dict tys depends on the_alts, which depens on arg_ids, which
-- depends on arity, which depends on n_dict tys. Sigh! Mega sigh!
stupid_dict_ids = mkTemplateLocalsNum 1 stupid_dict_tys
max_stupid_dicts = length (tyConStupidTheta tycon)
field_dict_base = max_stupid_dicts + 1
......@@ -638,13 +638,15 @@ mkRecordSelId tycon field_label
-- foo :: forall a. T -> a -> a
-- foo = /\a. \t:T. case t of { MkT f -> f a }
mk_alt data_con
= ASSERT2( data_ty `tcEqType` field_ty, ppr data_con $$ ppr data_ty $$ ppr field_ty )
mk_alt data_con
= ASSERT2( data_ty `tcEqType` field_ty,
ppr data_con $$ ppr data_ty $$ ppr field_ty )
mkReboxingAlt rebox_uniqs data_con (ex_tvs ++ co_tvs ++ arg_vs) rhs
-- get pattern binders with types appropriately instantiated
arg_uniqs = map mkBuiltinUnique [arg_base..]
(ex_tvs, co_tvs, arg_vs) = dataConOrigInstPat arg_uniqs data_con scrut_ty_args
(ex_tvs, co_tvs, arg_vs) = dataConOrigInstPat arg_uniqs data_con
rebox_base = arg_base + length ex_tvs + length co_tvs + length arg_vs
rebox_uniqs = map mkBuiltinUnique [rebox_base..]
......@@ -658,14 +660,16 @@ mkRecordSelId tycon field_label
-- Generate the refinement for b'=b,
-- and apply to (Maybe b'), to get (Maybe b)
Succeeded refinement = gadtRefine emptyRefinement ex_tvs co_tvs
the_arg_id_ty = idType the_arg_id
(rhs, data_ty) = case refineType refinement the_arg_id_ty of
Just (co, data_ty) -> (Cast (Var the_arg_id) co, data_ty)
Nothing -> (Var the_arg_id, the_arg_id_ty)
reft = matchRefine co_tvs
the_arg_id_ty = idType the_arg_id
(rhs, data_ty) =
case refineType reft the_arg_id_ty of
Just (co, data_ty) -> (Cast (Var the_arg_id) co, data_ty)
Nothing -> (Var the_arg_id, the_arg_id_ty)
field_vs = filter (not . isPredTy . idType) arg_vs
the_arg_id = assoc "mkRecordSelId:mk_alt" (field_lbls `zip` field_vs) field_label
the_arg_id = assoc "mkRecordSelId:mk_alt"
(field_lbls `zip` field_vs) field_label
field_lbls = dataConFieldLabels data_con
error_expr = mkRuntimeErrorApp rEC_SEL_ERROR_ID field_ty full_msg
......@@ -10,16 +10,9 @@
{-# OPTIONS -w #-}
-- The above warning supression flag is a temporary kludge.
-- While working on this module you are encouraged to remove it and fix
-- any warnings in the module. See
-- for details
module TcGadt (
Refinement, emptyRefinement, isEmptyRefinement,
refineType, refinePred, refineResType,
tcUnifyTys, BindFlag(..)
) where
......@@ -39,7 +32,6 @@ import Maybes
import Control.Monad
import Outputable
import TcType
import Unique
import UniqFM
import FastString
......@@ -59,7 +51,7 @@ type InternalReft = TyVarEnv (Coercion, Type)
-- Not necessarily idemopotent
instance Outputable Refinement where
ppr (Reft in_scope env)
ppr (Reft _in_scope env)
= ptext SLIT("Refinement") <+>
braces (ppr env)
......@@ -109,86 +101,73 @@ refineResType reft ty
%* *
Generating a type refinement
Simple generation of a type refinement
%* *
gadtRefine :: Refinement
-> [TyVar] -- Bind these by preference
-> [CoVar]
-> MaybeErr Message Refinement
matchRefine :: [CoVar] -> Refinement
(gadtRefine cvs) takes a list of coercion variables, and returns a
list of coercions, obtained by unifying the types equated by the
incoming coercions. The returned coercions all have kinds of form
(a:=:ty), where a is a rigid type variable.
gadtRefine [c :: (a,Int):=:(Bool,b)]
= [ right (left c) :: a:=:Bool,
sym (right c) :: b:=:Int ]
That is, given evidence 'c' that (a,Int)=(Bool,b), it returns derived
evidence in easy-to-use form. In particular, given any e::ty, we know
e `cast` ty[right (left c)/a, sym (right c)/b]
:: ty [Bool/a, Int/b]
Two refinements:
- It can fail, if the coercion is unsatisfiable.
- It's biased, by being given a set of type variables to bind
when there is a choice. Example:
MkT :: forall a. a -> T [a]
f :: forall b. T [b] -> b
f x = let v = case x of { MkT y -> y }
in ...
Here we want to bind [a->b], not the other way round, because
in this example the return type is wobbly, and we want the
program to typecheck
-- E.g. (a, Bool, right (left c))
-- INVARIANT: in the triple (tv, ty, co), we have (co :: tv:=:ty)
-- The result is idempotent: the
Given a list of coercions, where for each coercion c::(ty1~ty2), the type ty2
is a specialisation of ty1, produce a type refinement that maps the variables
of ty1 to the corresponding sub-terms of ty2 using appropriate coercions; eg,
matchRefine (co :: [(a, b)] ~ [(c, Maybe d)])
= { right (left (right co)) :: a ~ c
, right (right co) :: b ~ Maybe d
Precondition: The rhs types must indeed be a specialisation of the lhs types;
i.e., some free variables of the lhs are replaced with either distinct free
variables or proper type terms to obtain the rhs. (We don't perform full
unification or type matching here!)
NB: matchRefine does *not* expand the type synonyms.
gadtRefine (Reft in_scope env1)
ex_tvs co_vars
-- Precondition: fvs( co_vars ) # env1
-- That is, the kinds of the co_vars are a
-- fixed point of the incoming refinement
= ASSERT2( not $ any (`elemVarEnv` env1) (varSetElems $ tyVarsOfTypes $ map tyVarKind co_vars),
ppr env1 $$ ppr co_vars $$ ppr (map tyVarKind co_vars) )
initUM (tryToBind tv_set) $
do { -- Run the unifier, starting with an empty env
; env2 <- foldM do_one emptyInternalReft co_vars
-- Find the fixed point of the resulting
-- non-idempotent substitution
; let tmp_env = env1 `plusVarEnv` env2
out_env = fixTvCoEnv in_scope' tmp_env
; WARN( not (null (badReftElts tmp_env)), ppr (badReftElts tmp_env) $$ ppr tmp_env )
WARN( not (null (badReftElts out_env)), ppr (badReftElts out_env) $$ ppr out_env )
return (Reft in_scope' out_env) }
matchRefine co_vars
= Reft in_scope (foldr plusVarEnv emptyVarEnv (map refineOne co_vars))
tv_set = mkVarSet ex_tvs
in_scope' = foldr extend in_scope co_vars
in_scope = foldr extend emptyInScopeSet co_vars
-- For each co_var, add it *and* the tyvars it mentions, to in_scope
extend co_var in_scope
= extendInScopeSetSet in_scope $
= extendInScopeSetSet in_scope $
extendVarSet (tyVarsOfType (tyVarKind co_var)) co_var
do_one reft co_var = unify reft (TyVarTy co_var) ty1 ty2
(ty1,ty2) = splitCoercionKind (tyVarKind co_var)
refineOne co_var = refine (TyVarTy co_var) ty1 ty2
(ty1, ty2) = splitCoercionKind (tyVarKind co_var)
refine co (TyVarTy tv) ty = unitVarEnv tv (co, ty)
refine co (TyConApp _ tys) (TyConApp _ tys') = refineArgs co tys tys'
refine co (NoteTy _ ty) ty' = refine co ty ty'
refine co ty (NoteTy _ ty') = refine co ty ty'
refine _ (PredTy _) (PredTy _) =
error "TcGadt.matchRefine: PredTy"
refine co (FunTy arg res) (FunTy arg' res') =
refine (mkRightCoercion (mkLeftCoercion co)) arg arg'
refine (mkRightCoercion co) res res'
refine co (AppTy fun arg) (AppTy fun' arg') =
refine (mkLeftCoercion co) fun fun'
refine (mkRightCoercion co) arg arg'
refine co (ForAllTy tv ty) (ForAllTy _tv ty') =
refine (mkForAllCoercion tv co) ty ty' `delVarEnv` tv
refine _ _ _ = error "RcGadt.matchRefine: mismatch"
refineArgs :: Coercion -> [Type] -> [Type] -> InternalReft
refineArgs co tys tys' =
fst $ foldr refineArg (emptyVarEnv, id) (zip tys tys')
refineArg (ty, ty') (reft, coWrapper)
= (refine (mkRightCoercion (coWrapper co)) ty ty' `plusVarEnv` reft,
mkLeftCoercion . coWrapper)
%* *
......@@ -221,23 +200,6 @@ tcUnifyTys bind_fn tys1 tys2
fixTvCoEnv :: InScopeSet -> InternalReft -> InternalReft
-- Find the fixed point of a Refinement
-- (assuming it has no loops!)
fixTvCoEnv in_scope env
= fixpt
fixpt = mapVarEnv step env
step (co, ty) = case refineType (Reft in_scope fixpt) ty of
Nothing -> (co, ty)
Just (co', ty') -> (mkTransCoercion co co', ty')
-- Apply fixpt one step:
-- Use refineType to get a substituted type, ty', and a coercion, co_fn,
-- which justifies the substitution. If the coercion is not the identity
-- then use transitivity with the original coercion
-- XXX Can we do this more nicely, by exploiting laziness?
-- Or avoid needing it in the first place?
fixTvSubstEnv :: InScopeSet -> TvSubstEnv -> TvSubstEnv
......@@ -248,11 +210,6 @@ fixTvSubstEnv in_scope env = f env
then e
else f e'
tryToBind :: TyVarSet -> TyVar -> BindFlag
tryToBind tv_set tv | tv `elemVarSet` tv_set = BindMe
| otherwise = AvoidMe
......@@ -263,19 +220,6 @@ tryToBind tv_set tv | tv `elemVarSet` tv_set = BindMe
badReftElts :: InternalReft -> [(Unique, (Coercion,Type))]
-- Return the BAD elements of the refinement
-- Should be empty; used in asserions only
badReftElts env
= filter (not . ok) (ufmToList env)
ok :: (Unique, (Coercion, Type)) -> Bool
ok (u, (co, ty)) | Just tv <- tcGetTyVar_maybe ty1
= varUnique tv == u && ty `tcEqType` ty2
| otherwise = False
(ty1,ty2) = coercionKind co
emptyInternalReft :: InternalReft
emptyInternalReft = emptyVarEnv
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