Commit 0760818e authored by simonpj's avatar simonpj
Browse files

[project @ 2001-11-26 09:22:05 by simonpj]

Add missing files for Rank-N commit
parent 5e3f005d
_interface_ TcUnify 1
TcUnify unifyTauTy;
1 unifyTauTy _:_ TcType.TcTauType -> TcType.TcTauType -> TcMonad.TcM () ;;
-- This boot file exists only to tie the knot between
-- TcUnify and TcSimplify
__interface TcUnify 1 0 where
__export TcUnify unifyTauTy ;
1 unifyTauTy :: TcType.TcTauType -> TcType.TcTauType -> TcMonad.TcM () ;
% (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
\section{Type subsumption and unification}
module TcUnify (
-- Full-blown subsumption
tcSub, tcGen, subFunTy,
checkSigTyVars, sigCtxt, sigPatCtxt,
-- Various unifications
unifyTauTy, unifyTauTyList, unifyTauTyLists,
unifyFunTy, unifyListTy, unifyTupleTy,
unifyKind, unifyKinds, unifyOpenTypeKind,
-- Coercions
Coercion, ExprCoFn, PatCoFn,
(<$>), (<.>), mkCoercion,
idCoercion, isIdCoercion
) where
#include "HsVersions.h"
import HsSyn ( HsExpr(..) )
import TcHsSyn ( TypecheckedHsExpr, TcPat,
mkHsDictApp, mkHsTyApp, mkHsLet )
import TypeRep ( Type(..), SourceType(..),
openKindCon, typeCon )
import TcMonad -- TcType, amongst others
import TcType ( TcKind, TcType, TcSigmaType, TcPhiType, TcTyVar, TcTauType,
TcTyVarSet, TcThetaType,
isTauTy, isSigmaTy,
tcSplitAppTy_maybe, tcSplitTyConApp_maybe,
tcGetTyVar_maybe, tcGetTyVar,
mkTyConApp, mkTyVarTys, mkFunTy, tyVarsOfType, mkRhoTy,
typeKind, tcSplitFunTy_maybe, mkForAllTys,
isHoleTyVar, isSkolemTyVar, isUserTyVar, allDistinctTyVars,
tidyOpenType, tidyOpenTypes, tidyOpenTyVar, tidyOpenTyVars,
eqKind, openTypeKind, liftedTypeKind, unliftedTypeKind, isTypeKind,
hasMoreBoxityInfo, tyVarBindingInfo
import qualified Type ( getTyVar_maybe )
import Inst ( LIE, emptyLIE, plusLIE, mkLIE,
newDicts, instToId
import TcMType ( getTcTyVar, putTcTyVar, tcInstType,
newTyVarTy, newTyVarTys, newBoxityVar, newHoleTyVarTy,
zonkTcType, zonkTcTyVars, zonkTcTyVar )
import TcSimplify ( tcSimplifyCheck )
import TysWiredIn ( listTyCon, mkListTy, mkTupleTy )
import TcEnv ( TcTyThing(..), tcExtendGlobalTyVars, tcGetGlobalTyVars, tcLEnvElts )
import TyCon ( tyConArity, isTupleTyCon, tupleTyConBoxity )
import PprType ( pprType )
import CoreFVs ( idFreeTyVars )
import Id ( mkSysLocal, idType )
import Var ( Var, varName, tyVarKind )
import VarSet ( elemVarSet, varSetElems )
import VarEnv
import Name ( isSystemName, getSrcLoc )
import ErrUtils ( Message )
import BasicTypes ( Boxity, Arity, isBoxed )
import Util ( isSingleton, equalLength )
import Maybe ( isNothing )
import Outputable
%* *
%* *
tcSub :: TcSigmaType -- expected_ty; can be a type scheme;
-- can be a "hole" type variable
-> TcSigmaType -- actual_ty; can be a type scheme
-> TcM (ExprCoFn, LIE)
(tcSub expected_ty actual_ty) checks that
actual_ty <= expected_ty
That is, that a value of type actual_ty is acceptable in
a place expecting a value of type expected_ty.
It returns a coercion function
co_fn :: actual_ty -> expected_ty
which takes an HsExpr of type actual_ty into one of type
tcSub expected_ty actual_ty
= traceTc (text "tcSub" <+> details) `thenNF_Tc_`
tcAddErrCtxtM (unifyCtxt "type" expected_ty actual_ty)
(tc_sub expected_ty expected_ty actual_ty actual_ty)
details = vcat [text "Expected:" <+> ppr expected_ty,
text "Actual: " <+> ppr actual_ty]
tc_sub carries the types before and after expanding type synonyms
tc_sub :: TcSigmaType -- expected_ty, before expanding synonyms
-> TcSigmaType -- ..and after
-> TcSigmaType -- actual_ty, before
-> TcSigmaType -- ..and after
-> TcM (ExprCoFn, LIE)
-- Expand synonyms
tc_sub exp_sty (NoteTy _ exp_ty) act_sty act_ty = tc_sub exp_sty exp_ty act_sty act_ty
tc_sub exp_sty exp_ty act_sty (NoteTy _ act_ty) = tc_sub exp_sty exp_ty act_sty act_ty
-- "Hole type variable" case
-- Do this case before unwrapping for-alls in the actual_ty
tc_sub _ (TyVarTy tv) act_sty act_ty
| isHoleTyVar tv
= -- It's a "hole" type variable
getTcTyVar tv `thenNF_Tc` \ maybe_ty ->
case maybe_ty of
Just ty -> -- Already been assigned
tc_sub ty ty act_sty act_ty ;
Nothing -> -- Assign it
putTcTyVar tv act_sty `thenNF_Tc_`
returnTc (idCoercion, emptyLIE)
-- Generalisation case
-- actual_ty: d:Eq b => b->b
-- expected_ty: forall a. Ord a => a->a
-- co_fn e /\a. \d2:Ord a. let d = eqFromOrd d2 in e
-- It is essential to do this *before* the specialisation case
-- Example: f :: (Eq a => a->a) -> ...
-- g :: Ord b => b->b
-- Consider f g !
tc_sub exp_sty expected_ty act_sty actual_ty
| isSigmaTy expected_ty
= tcGen expected_ty (
\ body_exp_ty -> tc_sub body_exp_ty body_exp_ty act_sty actual_ty
) `thenTc` \ (gen_fn, co_fn, lie) ->
returnTc (gen_fn <.> co_fn, lie)
-- Specialisation case:
-- actual_ty: forall a. Ord a => a->a
-- expected_ty: Int -> Int
-- co_fn e = e Int dOrdInt
tc_sub exp_sty expected_ty act_sty actual_ty
| isSigmaTy actual_ty
= tcInstType actual_ty `thenNF_Tc` \ (tvs, theta, body_ty) ->
newDicts orig theta `thenNF_Tc` \ dicts ->
inst_fn e = mkHsDictApp (mkHsTyApp e (mkTyVarTys tvs))
(map instToId dicts)
tc_sub exp_sty expected_ty body_ty body_ty `thenTc` \ (co_fn, lie) ->
returnTc (co_fn <.> mkCoercion inst_fn, lie `plusLIE` mkLIE dicts)
orig = Rank2Origin
-- Function case
tc_sub _ (FunTy exp_arg exp_res) _ (FunTy act_arg act_res)
= tcSub_fun exp_arg exp_res act_arg act_res
-- Type variable meets function: imitate
-- MARK: can we short-cut to an error case?
-- when the arg/res is not a tau-type?
-- NO! e.g. f :: ((forall a. a->a) -> Int) -> Int
-- then x = (f,f)
-- is perfectly fine!
tc_sub exp_sty exp_ty@(FunTy exp_arg exp_res) _ (TyVarTy tv)
= getTcTyVar tv `thenNF_Tc` \ maybe_ty ->
case maybe_ty of
Just ty -> tc_sub exp_sty exp_ty ty ty
Nothing -> imitateFun tv `thenNF_Tc` \ (act_arg, act_res) ->
tcSub_fun exp_arg exp_res act_arg act_res
tc_sub _ (TyVarTy tv) act_sty act_ty@(FunTy act_arg act_res)
= getTcTyVar tv `thenNF_Tc` \ maybe_ty ->
case maybe_ty of
Just ty -> tc_sub ty ty act_sty act_ty
Nothing -> imitateFun tv `thenNF_Tc` \ (exp_arg, exp_res) ->
tcSub_fun exp_arg exp_res act_arg act_res
-- Unification case
-- If none of the above match, we revert to the plain unifier
tc_sub exp_sty expected_ty act_sty actual_ty
= uTys exp_sty expected_ty act_sty actual_ty `thenTc_`
returnTc (idCoercion, emptyLIE)
%* *
%* *
tcSub_fun exp_arg exp_res act_arg act_res
= tcSub act_arg exp_arg `thenTc` \ (co_fn_arg, lie1) ->
tcSub exp_res act_res `thenTc` \ (co_fn_res, lie2) ->
tcGetUnique `thenNF_Tc` \ uniq ->
-- co_fn_arg :: HsExpr exp_arg -> HsExpr act_arg
-- co_fn_res :: HsExpr act_res -> HsExpr exp_res
-- co_fn :: HsExpr (act_arg -> act_res) -> HsExpr (exp_arg -> exp_res)
arg_id = mkSysLocal SLIT("sub") uniq exp_arg
coercion | isIdCoercion co_fn_arg,
isIdCoercion co_fn_res = idCoercion
| otherwise = mkCoercion co_fn
co_fn e = DictLam [arg_id]
(co_fn_res <$> (HsApp e (co_fn_arg <$> (HsVar arg_id))))
-- Slight hack; using a "DictLam" to get an ordinary simple lambda
-- HsVar arg_id :: HsExpr exp_arg
-- co_fn_arg $it :: HsExpr act_arg
-- HsApp e $it :: HsExpr act_res
-- co_fn_res $it :: HsExpr exp_res
returnTc (coercion, lie1 `plusLIE` lie2)
imitateFun :: TcTyVar -> NF_TcM (TcType, TcType)
imitateFun tv
= ASSERT( not (isHoleTyVar tv) )
newTyVarTy openTypeKind `thenNF_Tc` \ arg ->
newTyVarTy openTypeKind `thenNF_Tc` \ res ->
-- NB: tv is an *ordinary* tyvar and so are the new ones
putTcTyVar tv (mkFunTy arg res) `thenNF_Tc_`
returnNF_Tc (arg,res)
%* *
%* *
tcGen :: TcSigmaType -- expected_ty
-> (TcPhiType -> TcM (result, LIE)) -- spec_ty
-> TcM (ExprCoFn, result, LIE)
-- The expression has type: spec_ty -> expected_ty
tcGen expected_ty thing_inside -- We expect expected_ty to be a forall-type
-- If not, the call is a no-op
= tcInstType expected_ty `thenNF_Tc` \ (forall_tvs, theta, phi_ty) ->
-- Type-check the arg and unify with poly type
thing_inside phi_ty `thenTc` \ (result, lie) ->
-- Check that the "forall_tvs" havn't been constrained
-- The interesting bit here is that we must include the free variables
-- of the expected_ty. Here's an example:
-- runST (newVar True)
-- Here, if we don't make a check, we'll get a type (ST s (MutVar s Bool))
-- for (newVar True), with s fresh. Then we unify with the runST's arg type
-- forall s'. ST s' a. That unifies s' with s, and a with MutVar s Bool.
-- So now s' isn't unconstrained because it's linked to a.
-- Conclusion: include the free vars of the expected_ty in the
-- list of "free vars" for the signature check.
tcExtendGlobalTyVars free_tvs $
tcAddErrCtxtM (sigCtxt forall_tvs theta phi_ty) $
newDicts SignatureOrigin theta `thenNF_Tc` \ dicts ->
tcSimplifyCheck sig_msg forall_tvs dicts lie `thenTc` \ (free_lie, inst_binds) ->
checkSigTyVars forall_tvs free_tvs `thenTc` \ zonked_tvs ->
-- This HsLet binds any Insts which came out of the simplification.
-- It's a bit out of place here, but using AbsBind involves inventing
-- a couple of new names which seems worse.
dict_ids = map instToId dicts
co_fn e = TyLam zonked_tvs (DictLam dict_ids (mkHsLet inst_binds e))
returnTc (mkCoercion co_fn, result, free_lie)
free_tvs = tyVarsOfType expected_ty
sig_msg = ptext SLIT("When generalising the type of an expression")
%* *
\subsection{Coercion functions}
%* *
type Coercion a = Maybe (a -> a)
-- Nothing => identity fn
type ExprCoFn = Coercion TypecheckedHsExpr
type PatCoFn = Coercion TcPat
(<.>) :: Coercion a -> Coercion a -> Coercion a -- Composition
Nothing <.> Nothing = Nothing
Nothing <.> Just f = Just f
Just f <.> Nothing = Just f
Just f1 <.> Just f2 = Just (f1 . f2)
(<$>) :: Coercion a -> a -> a
Just f <$> e = f e
Nothing <$> e = e
mkCoercion :: (a -> a) -> Coercion a
mkCoercion f = Just f
idCoercion :: Coercion a
idCoercion = Nothing
isIdCoercion :: Coercion a -> Bool
isIdCoercion = isNothing
%* *
\subsection[Unify-exported]{Exported unification functions}
%* *
The exported functions are all defined as versions of some
non-exported generic functions.
Unify two @TauType@s. Dead straightforward.
unifyTauTy :: TcTauType -> TcTauType -> TcM ()
unifyTauTy ty1 ty2 -- ty1 expected, ty2 inferred
= -- The unifier should only ever see tau-types
-- (no quantification whatsoever)
ASSERT2( isTauTy ty1, ppr ty1 )
ASSERT2( isTauTy ty2, ppr ty2 )
tcAddErrCtxtM (unifyCtxt "type" ty1 ty2) $
uTys ty1 ty1 ty2 ty2
@unifyTauTyList@ unifies corresponding elements of two lists of
@TauType@s. It uses @uTys@ to do the real work. The lists should be
of equal length. We charge down the list explicitly so that we can
complain if their lengths differ.
unifyTauTyLists :: [TcTauType] -> [TcTauType] -> TcM ()
unifyTauTyLists [] [] = returnTc ()
unifyTauTyLists (ty1:tys1) (ty2:tys2) = uTys ty1 ty1 ty2 ty2 `thenTc_`
unifyTauTyLists tys1 tys2
unifyTauTyLists ty1s ty2s = panic "Unify.unifyTauTyLists: mismatched type lists!"
@unifyTauTyList@ takes a single list of @TauType@s and unifies them
all together. It is used, for example, when typechecking explicit
lists, when all the elts should be of the same type.
unifyTauTyList :: [TcTauType] -> TcM ()
unifyTauTyList [] = returnTc ()
unifyTauTyList [ty] = returnTc ()
unifyTauTyList (ty1:tys@(ty2:_)) = unifyTauTy ty1 ty2 `thenTc_`
unifyTauTyList tys
%* *
\subsection[Unify-uTys]{@uTys@: getting down to business}
%* *
@uTys@ is the heart of the unifier. Each arg happens twice, because
we want to report errors in terms of synomyms if poss. The first of
the pair is used in error messages only; it is always the same as the
second, except that if the first is a synonym then the second may be a
de-synonym'd version. This way we get better error messages.
We call the first one \tr{ps_ty1}, \tr{ps_ty2} for ``possible synomym''.
uTys :: TcTauType -> TcTauType -- Error reporting ty1 and real ty1
-- ty1 is the *expected* type
-> TcTauType -> TcTauType -- Error reporting ty2 and real ty2
-- ty2 is the *actual* type
-> TcM ()
-- Always expand synonyms (see notes at end)
-- (this also throws away FTVs)
uTys ps_ty1 (NoteTy n1 ty1) ps_ty2 ty2 = uTys ps_ty1 ty1 ps_ty2 ty2
uTys ps_ty1 ty1 ps_ty2 (NoteTy n2 ty2) = uTys ps_ty1 ty1 ps_ty2 ty2
-- Ignore usage annotations inside typechecker
uTys ps_ty1 (UsageTy _ ty1) ps_ty2 ty2 = uTys ps_ty1 ty1 ps_ty2 ty2
uTys ps_ty1 ty1 ps_ty2 (UsageTy _ ty2) = uTys ps_ty1 ty1 ps_ty2 ty2
-- Variables; go for uVar
uTys ps_ty1 (TyVarTy tyvar1) ps_ty2 ty2 = uVar False tyvar1 ps_ty2 ty2
uTys ps_ty1 ty1 ps_ty2 (TyVarTy tyvar2) = uVar True tyvar2 ps_ty1 ty1
-- "True" means args swapped
-- Predicates
uTys _ (SourceTy (IParam n1 t1)) _ (SourceTy (IParam n2 t2))
| n1 == n2 = uTys t1 t1 t2 t2
uTys _ (SourceTy (ClassP c1 tys1)) _ (SourceTy (ClassP c2 tys2))
| c1 == c2 = unifyTauTyLists tys1 tys2
uTys _ (SourceTy (NType tc1 tys1)) _ (SourceTy (NType tc2 tys2))
| tc1 == tc2 = unifyTauTyLists tys1 tys2
-- Functions; just check the two parts
uTys _ (FunTy fun1 arg1) _ (FunTy fun2 arg2)
= uTys fun1 fun1 fun2 fun2 `thenTc_` uTys arg1 arg1 arg2 arg2
-- Type constructors must match
uTys ps_ty1 (TyConApp con1 tys1) ps_ty2 (TyConApp con2 tys2)
| con1 == con2 && equalLength tys1 tys2
= unifyTauTyLists tys1 tys2
| con1 == openKindCon
-- When we are doing kind checking, we might match a kind '?'
-- against a kind '*' or '#'. Notably, CCallable :: ? -> *, and
-- (CCallable Int) and (CCallable Int#) are both OK
= unifyOpenTypeKind ps_ty2
-- Applications need a bit of care!
-- They can match FunTy and TyConApp, so use splitAppTy_maybe
-- NB: we've already dealt with type variables and Notes,
-- so if one type is an App the other one jolly well better be too
uTys ps_ty1 (AppTy s1 t1) ps_ty2 ty2
= case tcSplitAppTy_maybe ty2 of
Just (s2,t2) -> uTys s1 s1 s2 s2 `thenTc_` uTys t1 t1 t2 t2
Nothing -> unifyMisMatch ps_ty1 ps_ty2
-- Now the same, but the other way round
-- Don't swap the types, because the error messages get worse
uTys ps_ty1 ty1 ps_ty2 (AppTy s2 t2)
= case tcSplitAppTy_maybe ty1 of
Just (s1,t1) -> uTys s1 s1 s2 s2 `thenTc_` uTys t1 t1 t2 t2
Nothing -> unifyMisMatch ps_ty1 ps_ty2
-- Not expecting for-alls in unification
-- ... but the error message from the unifyMisMatch more informative
-- than a panic message!
-- Anything else fails
uTys ps_ty1 ty1 ps_ty2 ty2 = unifyMisMatch ps_ty1 ps_ty2
Notes on synonyms
If you are tempted to make a short cut on synonyms, as in this
-- NO uTys (SynTy con1 args1 ty1) (SynTy con2 args2 ty2)
-- NO = if (con1 == con2) then
-- NO -- Good news! Same synonym constructors, so we can shortcut
-- NO -- by unifying their arguments and ignoring their expansions.
-- NO unifyTauTypeLists args1 args2
-- NO else
-- NO -- Never mind. Just expand them and try again
-- NO uTys ty1 ty2
then THINK AGAIN. Here is the whole story, as detected and reported
by Chris Okasaki \tr{<>}:
Here's a test program that should detect the problem:
type Bogus a = Int
x = (1 :: Bogus Char) :: Bogus Bool
The problem with [the attempted shortcut code] is that
con1 == con2
is not a sufficient condition to be able to use the shortcut!
You also need to know that the type synonym actually USES all
its arguments. For example, consider the following type synonym
which does not use all its arguments.
type Bogus a = Int
If you ever tried unifying, say, \tr{Bogus Char} with \tr{Bogus Bool},
the unifier would blithely try to unify \tr{Char} with \tr{Bool} and
would fail, even though the expanded forms (both \tr{Int}) should
Similarly, unifying \tr{Bogus Char} with \tr{Bogus t} would
unnecessarily bind \tr{t} to \tr{Char}.
... You could explicitly test for the problem synonyms and mark them
somehow as needing expansion, perhaps also issuing a warning to the
%* *
\subsection[Unify-uVar]{@uVar@: unifying with a type variable}
%* *
@uVar@ is called when at least one of the types being unified is a
variable. It does {\em not} assume that the variable is a fixed point
of the substitution; rather, notice that @uVar@ (defined below) nips
back into @uTys@ if it turns out that the variable is already bound.
uVar :: Bool -- False => tyvar is the "expected"
-- True => ty is the "expected" thing
-> TcTyVar
-> TcTauType -> TcTauType -- printing and real versions
-> TcM ()
uVar swapped tv1 ps_ty2 ty2
= traceTc (text "uVar" <+> ppr swapped <+> ppr tv1 <+> (ppr ps_ty2 $$ ppr ty2)) `thenNF_Tc_`
getTcTyVar tv1 `thenNF_Tc` \ maybe_ty1 ->
case maybe_ty1 of
Just ty1 | swapped -> uTys ps_ty2 ty2 ty1 ty1 -- Swap back
| otherwise -> uTys ty1 ty1 ps_ty2 ty2 -- Same order
other -> uUnboundVar swapped tv1 maybe_ty1 ps_ty2 ty2
-- Expand synonyms; ignore FTVs
uUnboundVar swapped tv1 maybe_ty1 ps_ty2 (NoteTy n2 ty2)
= uUnboundVar swapped tv1 maybe_ty1 ps_ty2 ty2
-- The both-type-variable case
uUnboundVar swapped tv1 maybe_ty1 ps_ty2 ty2@(TyVarTy tv2)
-- Same type variable => no-op
| tv1 == tv2
= returnTc ()
-- Distinct type variables
-- ASSERT maybe_ty1 /= Just
| otherwise
= getTcTyVar tv2 `thenNF_Tc` \ maybe_ty2 ->
case maybe_ty2 of
Just ty2' -> uUnboundVar swapped tv1 maybe_ty1 ty2' ty2'
Nothing | update_tv2
-> WARN( not (k1 `hasMoreBoxityInfo` k2), (ppr tv1 <+> ppr k1) $$ (ppr tv2 <+> ppr k2) )
putTcTyVar tv2 (TyVarTy tv1) `thenNF_Tc_`
returnTc ()
| otherwise
-> WARN( not (k2 `hasMoreBoxityInfo` k1), (ppr tv2 <+> ppr k2) $$ (ppr tv1 <+> ppr k1) )
putTcTyVar tv1 ps_ty2 `thenNF_Tc_`
returnTc ()
k1 = tyVarKind tv1
k2 = tyVarKind tv2
update_tv2 = (k2 `eqKind` openTypeKind) || (not (k1 `eqKind` openTypeKind) && nicer_to_update_tv2)
-- Try to get rid of open type variables as soon as poss
nicer_to_update_tv2 = isUserTyVar tv1
-- Don't unify a signature type variable if poss
|| isSystemName (varName tv2)
-- Try to update sys-y type variables in preference to sig-y ones
-- Second one isn't a type variable
uUnboundVar swapped tv1 maybe_ty1 ps_ty2 non_var_ty2
= -- Check that tv1 isn't a type-signature type variable
checkTcM (not (isSkolemTyVar tv1))
(failWithTcM (unifyWithSigErr tv1 ps_ty2)) `thenTc_`
-- Check that the kinds match
zonkTcType ps_ty2 `thenNF_Tc` \ ps_ty2' ->
checkKinds swapped tv1 ps_ty2' `thenTc_`
-- Occurs check
-- Basically we want to update tv1 := ps_ty2
-- because ps_ty2 has type-synonym info, which improves later error messages
-- But consider
-- type A a = ()
-- f :: (A a -> a -> ()) -> ()
-- f = \ _ -> ()
-- x :: ()
-- x = f (\ x p -> p x)
-- In the application (p x), we try to match "t" with "A t". If we go
-- ahead and bind t to A t (= ps_ty2), we'll lead the type checker into
-- an infinite loop later.
-- But we should not reject the program, because A t = ().
-- Rather, we should bind t to () (= non_var_ty2).
-- That's why we have this two-state occurs-check
if not (tv1 `elemVarSet` tyVarsOfType ps_ty2') then
putTcTyVar tv1 ps_ty2' `thenNF_Tc_`
returnTc ()
zonkTcType non_var_ty2 `thenNF_Tc` \ non_var_ty2' ->
if not (tv1 `elemVarSet` tyVarsOfType non_var_ty2') then
-- This branch rarely succeeds, except in strange cases
-- like that in the example above
putTcTyVar tv1 non_var_ty2' `thenNF_Tc_`
returnTc ()