\begin{code}
module TcUnify (
-- Full-blown subsumption
- tcSub, tcGen, subFunTy,
- checkSigTyVars, sigCtxt, sigPatCtxt,
+ tcSubExp, tcFunResTy, tcGen,
+ checkSigTyVars, checkSigTyVarsWrt, bleatEscapedTvs, sigCtxt,
-- Various unifications
- unifyTauTy, unifyTauTyList, unifyTauTyLists,
- unifyFunTy, unifyListTy, unifyPArrTy, unifyTupleTy,
- unifyKind, unifyKinds, unifyOpenTypeKind,
-
- -- Coercions
- Coercion, ExprCoFn, PatCoFn,
- (<$>), (<.>), mkCoercion,
- idCoercion, isIdCoercion
-
+ unifyType, unifyTypeList, unifyTheta,
+ unifyKind, unifyKinds, unifyFunKind,
+ checkExpectedKind,
+ boxySubMatchType, boxyMatchTypes,
+
+ --------------------------------
+ -- Holes
+ tcInfer, subFunTys, unBox, stripBoxyType, withBox,
+ boxyUnify, boxyUnifyList, zapToMonotype,
+ boxySplitListTy, boxySplitTyConApp, boxySplitAppTy,
+ wrapFunResCoercion
) where
#include "HsVersions.h"
+import HsSyn ( ExprCoFn(..), idCoercion, isIdCoercion, (<.>) )
+import TypeRep ( Type(..), PredType(..) )
-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 TcMType ( lookupTcTyVar, LookupTyVarResult(..),
+ tcInstSkolType, newKindVar, newMetaTyVar,
+ tcInstBoxy, newBoxyTyVar, newBoxyTyVarTys, readFilledBox,
+ readMetaTyVar, writeMetaTyVar, newFlexiTyVarTy,
+ tcInstSkolTyVars,
+ zonkTcKind, zonkType, zonkTcType, zonkTcTyVarsAndFV,
+ readKindVar, writeKindVar )
import TcSimplify ( tcSimplifyCheck )
-import TysWiredIn ( listTyCon, parrTyCon, mkListTy, mkPArrTy, 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 TcEnv ( tcGetGlobalTyVars, findGlobals )
+import TcIface ( checkWiredInTyCon )
+import TcRnMonad -- TcType, amongst others
+import TcType ( TcKind, TcType, TcTyVar, TcTauType,
+ BoxySigmaType, BoxyRhoType, BoxyType,
+ TcTyVarSet, TcThetaType, TcTyVarDetails(..), BoxInfo(..),
+ SkolemInfo( GenSkol, UnkSkol ), MetaDetails(..), isImmutableTyVar,
+ pprSkolTvBinding, isTauTy, isTauTyCon, isSigmaTy,
+ mkFunTy, mkFunTys, mkTyConApp, isMetaTyVar,
+ tcSplitForAllTys, tcSplitAppTy_maybe, tcSplitFunTys, mkTyVarTys,
+ tyVarsOfType, mkPhiTy, mkTyVarTy, mkPredTy,
+ typeKind, mkForAllTys, mkAppTy, isBoxyTyVar,
+ tidyOpenType, tidyOpenTyVar, tidyOpenTyVars,
+ pprType, tidyKind, tidySkolemTyVar, isSkolemTyVar, tcView,
+ TvSubst, mkTvSubst, zipTyEnv, substTy, emptyTvSubst,
+ lookupTyVar, extendTvSubst )
+import Kind ( Kind(..), SimpleKind, KindVar, isArgTypeKind,
+ openTypeKind, liftedTypeKind, mkArrowKind, defaultKind,
+ isOpenTypeKind, argTypeKind, isLiftedTypeKind, isUnliftedTypeKind,
+ isSubKind, pprKind, splitKindFunTys )
+import TysPrim ( alphaTy, betaTy )
+import Inst ( newDicts, instToId )
+import TyCon ( TyCon, tyConArity, tyConTyVars, isSynTyCon )
+import TysWiredIn ( listTyCon )
+import Id ( Id, mkSysLocal )
+import Var ( Var, varName, tyVarKind, isTcTyVar, tcTyVarDetails )
+import VarSet ( emptyVarSet, mkVarSet, unitVarSet, unionVarSet, elemVarSet, varSetElems,
+ extendVarSet, intersectsVarSet )
import VarEnv
-import Name ( isSystemName, getSrcLoc )
+import Name ( Name, isSystemName )
import ErrUtils ( Message )
-import BasicTypes ( Boxity, Arity, isBoxed )
-import Util ( isSingleton, equalLength )
-import Maybe ( isNothing )
+import Maybes ( expectJust, isNothing )
+import BasicTypes ( Arity )
+import UniqSupply ( uniqsFromSupply )
+import Util ( notNull, equalLength )
import Outputable
+
+-- Assertion imports
+#ifdef DEBUG
+import TcType ( isBoxyTy, isFlexi )
+#endif
\end{code}
+%************************************************************************
+%* *
+\subsection{'hole' type variables}
+%* *
+%************************************************************************
+
+\begin{code}
+tcInfer :: (BoxyType -> TcM a) -> TcM (a, TcType)
+tcInfer tc_infer
+ = do { box <- newBoxyTyVar openTypeKind
+ ; res <- tc_infer (mkTyVarTy box)
+ ; res_ty <- readFilledBox box -- Guaranteed filled-in by now
+ ; return (res, res_ty) }
+\end{code}
+
%************************************************************************
%* *
-\subsection{Subsumption}
+ subFunTys
%* *
%************************************************************************
\begin{code}
-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)
-\end{code}
+subFunTys :: SDoc -- Somthing like "The function f has 3 arguments"
+ -- or "The abstraction (\x.e) takes 1 argument"
+ -> Arity -- Expected # of args
+ -> BoxyRhoType -- res_ty
+ -> ([BoxySigmaType] -> BoxyRhoType -> TcM a)
+ -> TcM (ExprCoFn, a)
+-- Attempt to decompse res_ty to have enough top-level arrows to
+-- match the number of patterns in the match group
+--
+-- If (subFunTys n_args res_ty thing_inside) = (co_fn, res)
+-- and the inner call to thing_inside passes args: [a1,...,an], b
+-- then co_fn :: (a1 -> ... -> an -> b) -> res_ty
+--
+-- Note that it takes a BoxyRho type, and guarantees to return a BoxyRhoType
-(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
-expected_ty.
+{- Error messages from subFunTys
+
+ The abstraction `\Just 1 -> ...' has two arguments
+ but its type `Maybe a -> a' has only one
+
+ The equation(s) for `f' have two arguments
+ but its type `Maybe a -> a' has only one
+
+ The section `(f 3)' requires 'f' to take two arguments
+ but its type `Int -> Int' has only one
+
+ The function 'f' is applied to two arguments
+ but its type `Int -> Int' has only one
+-}
+
+
+subFunTys error_herald n_pats res_ty thing_inside
+ = loop n_pats [] res_ty
+ where
+ -- In 'loop', the parameter 'arg_tys' accumulates
+ -- the arg types so far, in *reverse order*
+ loop n args_so_far res_ty
+ | Just res_ty' <- tcView res_ty = loop n args_so_far res_ty'
+
+ loop n args_so_far res_ty
+ | isSigmaTy res_ty -- Do this before checking n==0, because we
+ -- guarantee to return a BoxyRhoType, not a BoxySigmaType
+ = do { (gen_fn, (co_fn, res)) <- tcGen res_ty emptyVarSet $ \ res_ty' ->
+ loop n args_so_far res_ty'
+ ; return (gen_fn <.> co_fn, res) }
+
+ loop 0 args_so_far res_ty
+ = do { res <- thing_inside (reverse args_so_far) res_ty
+ ; return (idCoercion, res) }
+
+ loop n args_so_far (FunTy arg_ty res_ty)
+ = do { (co_fn, res) <- loop (n-1) (arg_ty:args_so_far) res_ty
+ ; co_fn' <- wrapFunResCoercion [arg_ty] co_fn
+ ; return (co_fn', res) }
+
+ -- res_ty might have a type variable at the head, such as (a b c),
+ -- in which case we must fill in with (->). Simplest thing to do
+ -- is to use boxyUnify, but we catch failure and generate our own
+ -- error message on failure
+ loop n args_so_far res_ty@(AppTy _ _)
+ = do { [arg_ty',res_ty'] <- newBoxyTyVarTys [argTypeKind, openTypeKind]
+ ; (_, mb_unit) <- tryTcErrs $ boxyUnify res_ty (FunTy arg_ty' res_ty')
+ ; if isNothing mb_unit then bale_out args_so_far res_ty
+ else loop n args_so_far (FunTy arg_ty' res_ty') }
+
+ loop n args_so_far (TyVarTy tv)
+ | not (isImmutableTyVar tv)
+ = do { cts <- readMetaTyVar tv
+ ; case cts of
+ Indirect ty -> loop n args_so_far ty
+ Flexi -> do { (res_ty:arg_tys) <- withMetaTvs tv kinds mk_res_ty
+ ; res <- thing_inside (reverse args_so_far ++ arg_tys) res_ty
+ ; return (idCoercion, res) } }
+ where
+ mk_res_ty (res_ty' : arg_tys') = mkFunTys arg_tys' res_ty'
+ kinds = openTypeKind : take n (repeat argTypeKind)
+ -- Note argTypeKind: the args can have an unboxed type,
+ -- but not an unboxed tuple.
+
+ loop n args_so_far res_ty = bale_out args_so_far res_ty
+
+ bale_out args_so_far res_ty
+ = do { env0 <- tcInitTidyEnv
+ ; res_ty' <- zonkTcType res_ty
+ ; let (env1, res_ty'') = tidyOpenType env0 res_ty'
+ ; failWithTcM (env1, mk_msg res_ty'' (length args_so_far)) }
+
+ mk_msg res_ty n_actual
+ = error_herald <> comma $$
+ sep [ptext SLIT("but its type") <+> quotes (pprType res_ty),
+ if n_actual == 0 then ptext SLIT("has none")
+ else ptext SLIT("has only") <+> speakN n_actual]
+\end{code}
\begin{code}
-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)
+----------------------
+boxySplitTyConApp :: TyCon -- T :: k1 -> ... -> kn -> *
+ -> BoxyRhoType -- Expected type (T a b c)
+ -> TcM [BoxySigmaType] -- Element types, a b c
+ -- It's used for wired-in tycons, so we call checkWiredInTyCOn
+ -- Precondition: never called with FunTyCon
+ -- Precondition: input type :: *
+
+boxySplitTyConApp tc orig_ty
+ = do { checkWiredInTyCon tc
+ ; loop (tyConArity tc) [] orig_ty }
+ where
+ loop n_req args_so_far ty
+ | Just ty' <- tcView ty = loop n_req args_so_far ty'
+
+ loop n_req args_so_far (TyConApp tycon args)
+ | tc == tycon
+ = ASSERT( n_req == length args) -- ty::*
+ return (args ++ args_so_far)
+
+ loop n_req args_so_far (AppTy fun arg)
+ = loop (n_req - 1) (arg:args_so_far) fun
+
+ loop n_req args_so_far (TyVarTy tv)
+ | not (isImmutableTyVar tv)
+ = do { cts <- readMetaTyVar tv
+ ; case cts of
+ Indirect ty -> loop n_req args_so_far ty
+ Flexi -> do { arg_tys <- withMetaTvs tv arg_kinds mk_res_ty
+ ; return (arg_tys ++ args_so_far) }
+ }
+ where
+ mk_res_ty arg_tys' = mkTyConApp tc arg_tys'
+ arg_kinds = map tyVarKind (take n_req (tyConTyVars tc))
+
+ loop _ _ _ = boxySplitFailure (mkTyConApp tc (mkTyVarTys (tyConTyVars tc))) orig_ty
+
+----------------------
+boxySplitListTy :: BoxyRhoType -> TcM BoxySigmaType -- Special case for lists
+boxySplitListTy exp_ty = do { [elt_ty] <- boxySplitTyConApp listTyCon exp_ty
+ ; return elt_ty }
+
+
+----------------------
+boxySplitAppTy :: BoxyRhoType -- Type to split: m a
+ -> TcM (BoxySigmaType, BoxySigmaType) -- Returns m, a
+-- Assumes (m: * -> k), where k is the kind of the incoming type
+-- If the incoming type is boxy, then so are the result types; and vice versa
+
+boxySplitAppTy orig_ty
+ = loop orig_ty
where
- details = vcat [text "Expected:" <+> ppr expected_ty,
- text "Actual: " <+> ppr actual_ty]
+ loop ty
+ | Just ty' <- tcView ty = loop ty'
+
+ loop ty
+ | Just (fun_ty, arg_ty) <- tcSplitAppTy_maybe ty
+ = return (fun_ty, arg_ty)
+
+ loop (TyVarTy tv)
+ | not (isImmutableTyVar tv)
+ = do { cts <- readMetaTyVar tv
+ ; case cts of
+ Indirect ty -> loop ty
+ Flexi -> do { [fun_ty,arg_ty] <- withMetaTvs tv kinds mk_res_ty
+ ; return (fun_ty, arg_ty) } }
+ where
+ mk_res_ty [fun_ty', arg_ty'] = mkAppTy fun_ty' arg_ty'
+ tv_kind = tyVarKind tv
+ kinds = [mkArrowKind liftedTypeKind (defaultKind tv_kind),
+ -- m :: * -> k
+ liftedTypeKind] -- arg type :: *
+ -- The defaultKind is a bit smelly. If you remove it,
+ -- try compiling f x = do { x }
+ -- and you'll get a kind mis-match. It smells, but
+ -- not enough to lose sleep over.
+
+ loop _ = boxySplitFailure (mkAppTy alphaTy betaTy) orig_ty
+
+------------------
+boxySplitFailure actual_ty expected_ty
+ = unifyMisMatch False False actual_ty expected_ty
+ -- "outer" is False, so we don't pop the context
+ -- which is what we want since we have not pushed one!
\end{code}
-tc_sub carries the types before and after expanding type synonyms
+
+--------------------------------
+-- withBoxes: the key utility function
+--------------------------------
\begin{code}
-tc_sub :: TcSigmaType -- expected_ty, before expanding synonyms
- -> TcSigmaType -- ..and after
- -> TcSigmaType -- actual_ty, before
- -> TcSigmaType -- ..and after
- -> TcM (ExprCoFn, LIE)
+withMetaTvs :: TcTyVar -- An unfilled-in, non-skolem, meta type variable
+ -> [Kind] -- Make fresh boxes (with the same BoxTv/TauTv setting as tv)
+ -> ([BoxySigmaType] -> BoxySigmaType)
+ -- Constructs the type to assign
+ -- to the original var
+ -> TcM [BoxySigmaType] -- Return the fresh boxes
+
+-- It's entirely possible for the [kind] to be empty.
+-- For example, when pattern-matching on True,
+-- we call boxySplitTyConApp passing a boolTyCon
+
+-- Invariant: tv is still Flexi
+
+withMetaTvs tv kinds mk_res_ty
+ | isBoxyTyVar tv
+ = do { box_tvs <- mapM (newMetaTyVar BoxTv) kinds
+ ; let box_tys = mkTyVarTys box_tvs
+ ; writeMetaTyVar tv (mk_res_ty box_tys)
+ ; return box_tys }
+
+ | otherwise -- Non-boxy meta type variable
+ = do { tau_tys <- mapM newFlexiTyVarTy kinds
+ ; writeMetaTyVar tv (mk_res_ty tau_tys) -- Write it *first*
+ -- Sure to be a tau-type
+ ; return tau_tys }
+
+withBox :: Kind -> (BoxySigmaType -> TcM a) -> TcM (a, TcType)
+-- Allocate a *boxy* tyvar
+withBox kind thing_inside
+ = do { box_tv <- newMetaTyVar BoxTv kind
+ ; res <- thing_inside (mkTyVarTy box_tv)
+ ; ty <- readFilledBox box_tv
+ ; return (res, ty) }
+\end{code}
------------------------------------
--- 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
+%************************************************************************
+%* *
+ Approximate boxy matching
+%* *
+%************************************************************************
+
+\begin{code}
+boxySubMatchType
+ :: TcTyVarSet -> TcType -- The "template"; the tyvars are skolems
+ -> BoxyRhoType -- Type to match (note a *Rho* type)
+ -> TvSubst -- Substitution of the [TcTyVar] to BoxySigmaTypes
+
+boxyMatchTypes
+ :: TcTyVarSet -> [TcType] -- The "template"; the tyvars are skolems
+ -> [BoxySigmaType] -- Type to match
+ -> TvSubst -- Substitution of the [TcTyVar] to BoxySigmaTypes
+
+-- Find a *boxy* substitution that makes the template look as much
+-- like the BoxySigmaType as possible.
+-- It's always ok to return an empty substitution;
+-- anything more is jam on the pudding
+--
+-- NB1: This is a pure, non-monadic function.
+-- It does no unification, and cannot fail
+--
+-- Note [Matching kinds]
+-- The target type might legitimately not be a sub-kind of template.
+-- For example, suppose the target is simply a box with an OpenTypeKind,
+-- and the template is a type variable with LiftedTypeKind.
+-- Then it's ok (because the target type will later be refined).
+-- We simply don't bind the template type variable.
+--
+-- It might also be that the kind mis-match is an error. For example,
+-- suppose we match the template (a -> Int) against (Int# -> Int),
+-- where the template type variable 'a' has LiftedTypeKind. This
+-- matching function does not fail; it simply doesn't bind the template.
+-- Later stuff will fail.
+--
+-- Precondition: the arg lengths are equal
+-- Precondition: none of the template type variables appear in the [BoxySigmaType]
+-- Precondition: any nested quantifiers in either type differ from
+-- the template type variables passed as arguments
+--
+-- Note [Sub-match]
+-- ~~~~~~~~~~~~~~~~
+-- Consider this
+-- head :: [a] -> a
+-- |- head xs : <rhobox>
+-- We will do a boxySubMatchType between a ~ <rhobox>
+-- But we *don't* want to match [a |-> <rhobox>] because
+-- (a) The box should be filled in with a rho-type, but
+-- but the returned substitution maps TyVars to boxy *sigma*
+-- types
+-- (b) In any case, the right final answer might be *either*
+-- instantiate 'a' with a rho-type or a sigma type
+-- head xs : Int vs head xs : forall b. b->b
+-- So the matcher MUST NOT make a choice here. In general, we only
+-- bind a template type variable in boxyMatchType, not in boxySubMatchType.
+
+boxySubMatchType tmpl_tvs tmpl_ty boxy_ty
+ = go tmpl_ty boxy_ty
+ where
+ go t_ty b_ty
+ | Just t_ty' <- tcView t_ty = go t_ty' b_ty
+ | Just b_ty' <- tcView b_ty = go t_ty b_ty'
+
+ go (FunTy arg1 res1) (FunTy arg2 res2)
+ = do_match arg1 arg2 (go res1 res2)
+ -- Match the args, and sub-match the results
+
+ go (TyVarTy _) b_ty = emptyTvSubst -- Do not bind! See Note [Sub-match]
+
+ go t_ty b_ty = do_match t_ty b_ty emptyTvSubst -- Otherwise we are safe to bind
+
+ do_match t_ty b_ty subst = boxy_match tmpl_tvs t_ty emptyVarSet b_ty subst
+
+------------
+boxyMatchTypes tmpl_tvs tmpl_tys boxy_tys
+ = ASSERT( length tmpl_tys == length boxy_tys )
+ boxy_match_s tmpl_tvs tmpl_tys emptyVarSet boxy_tys emptyTvSubst
+ -- ToDo: add error context?
+
+boxy_match_s tmpl_tvs [] boxy_tvs [] subst
+ = subst
+boxy_match_s tmpl_tvs (t_ty:t_tys) boxy_tvs (b_ty:b_tys) subst
+ = boxy_match_s tmpl_tvs t_tys boxy_tvs b_tys $
+ boxy_match tmpl_tvs t_ty boxy_tvs b_ty subst
+
+------------
+boxy_match :: TcTyVarSet -> TcType -- Template
+ -> TcTyVarSet -- boxy_tvs: do not bind template tyvars to any of these
+ -> BoxySigmaType -- Match against this type
+ -> TvSubst
+ -> TvSubst
+
+-- The boxy_tvs argument prevents this match:
+-- [a] forall b. a ~ forall b. b
+-- We don't want to bind the template variable 'a'
+-- to the quantified type variable 'b'!
+
+boxy_match tmpl_tvs orig_tmpl_ty boxy_tvs orig_boxy_ty subst
+ = go orig_tmpl_ty orig_boxy_ty
+ where
+ go t_ty b_ty
+ | Just t_ty' <- tcView t_ty = go t_ty' b_ty
+ | Just b_ty' <- tcView b_ty = go t_ty b_ty'
+
+ go (ForAllTy _ ty1) (ForAllTy tv2 ty2)
+ = boxy_match tmpl_tvs ty1 (boxy_tvs `extendVarSet` tv2) ty2 subst
+
+ go (TyConApp tc1 tys1) (TyConApp tc2 tys2)
+ | tc1 == tc2 = go_s tys1 tys2
+
+ go (FunTy arg1 res1) (FunTy arg2 res2)
+ = go_s [arg1,res1] [arg2,res2]
+
+ go t_ty b_ty
+ | Just (s1,t1) <- tcSplitAppTy_maybe t_ty,
+ Just (s2,t2) <- tcSplitAppTy_maybe b_ty,
+ typeKind t2 `isSubKind` typeKind t1 -- Maintain invariant
+ = go_s [s1,t1] [s2,t2]
+
+ go (TyVarTy tv) b_ty
+ | tv `elemVarSet` tmpl_tvs -- Template type variable in the template
+ , not (intersectsVarSet boxy_tvs (tyVarsOfType orig_boxy_ty))
+ , typeKind b_ty `isSubKind` tyVarKind tv
+ = extendTvSubst subst tv boxy_ty'
+ where
+ boxy_ty' = case lookupTyVar subst tv of
+ Nothing -> orig_boxy_ty
+ Just ty -> ty `boxyLub` orig_boxy_ty
+
+ go _ _ = subst -- Always safe
+
+ --------
+ go_s tys1 tys2 = boxy_match_s tmpl_tvs tys1 boxy_tvs tys2 subst
+
+
+boxyLub :: BoxySigmaType -> BoxySigmaType -> BoxySigmaType
+-- Combine boxy information from the two types
+-- If there is a conflict, return the first
+boxyLub orig_ty1 orig_ty2
+ = go orig_ty1 orig_ty2
+ where
+ go (AppTy f1 a1) (AppTy f2 a2) = AppTy (boxyLub f1 f2) (boxyLub a1 a2)
+ go (FunTy f1 a1) (FunTy f2 a2) = FunTy (boxyLub f1 f2) (boxyLub a1 a2)
+ go (TyConApp tc1 ts1) (TyConApp tc2 ts2)
+ | tc1 == tc2, length ts1 == length ts2
+ = TyConApp tc1 (zipWith boxyLub ts1 ts2)
+
+ go (TyVarTy tv1) ty2 -- This is the whole point;
+ | isTcTyVar tv1, isMetaTyVar tv1 -- choose ty2 if ty2 is a box
+ = ty2
+
+ -- Look inside type synonyms, but only if the naive version fails
+ go ty1 ty2 | Just ty1' <- tcView ty1 = go ty1' ty2
+ | Just ty2' <- tcView ty1 = go ty1 ty2'
+
+ -- For now, we don't look inside ForAlls, PredTys
+ go ty1 ty2 = orig_ty1 -- Default
+\end{code}
+
+
+%************************************************************************
+%* *
+ Subsumption checking
+%* *
+%************************************************************************
-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
+All the tcSub calls have the form
+
+ tcSub expected_ty offered_ty
+which checks
+ offered_ty <= expected_ty
- Just ty -> -- Already been assigned
- tc_sub ty ty act_sty act_ty ;
+That is, that a value of type offered_ty is acceptable in
+a place expecting a value of type expected_ty.
+
+It returns a coercion function
+ co_fn :: offered_ty -> expected_ty
+which takes an HsExpr of type offered_ty into one of type
+expected_ty.
- Nothing -> -- Assign it
- putTcTyVar tv act_sty `thenNF_Tc_`
- returnTc (idCoercion, emptyLIE)
+\begin{code}
+-----------------
+tcSubExp :: BoxySigmaType -> BoxySigmaType -> TcM ExprCoFn -- Locally used only
+ -- (tcSub act exp) checks that
+ -- act <= exp
+tcSubExp actual_ty expected_ty
+ = addErrCtxtM (unifyCtxt actual_ty expected_ty)
+ (tc_sub True actual_ty actual_ty expected_ty expected_ty)
+
+tcFunResTy :: Name -> BoxySigmaType -> BoxySigmaType -> TcM ExprCoFn -- Locally used only
+tcFunResTy fun actual_ty expected_ty
+ = addErrCtxtM (checkFunResCtxt fun actual_ty expected_ty) $
+ (tc_sub True actual_ty actual_ty expected_ty expected_ty)
+
+-----------------
+tc_sub :: Outer -- See comments with uTys
+ -> BoxySigmaType -- actual_ty, before expanding synonyms
+ -> BoxySigmaType -- ..and after
+ -> BoxySigmaType -- expected_ty, before
+ -> BoxySigmaType -- ..and after
+ -> TcM ExprCoFn
+
+tc_sub outer act_sty act_ty exp_sty exp_ty
+ | Just exp_ty' <- tcView exp_ty = tc_sub False act_sty act_ty exp_sty exp_ty'
+tc_sub outer act_sty act_ty exp_sty exp_ty
+ | Just act_ty' <- tcView act_ty = tc_sub False act_sty act_ty' exp_sty exp_ty
+-----------------------------------
+-- Rule SBOXY, plus other cases when act_ty is a type variable
+-- Just defer to boxy matching
+-- This rule takes precedence over SKOL!
+tc_sub outer act_sty (TyVarTy tv) exp_sty exp_ty
+ = do { uVar outer False tv False exp_sty exp_ty
+ ; return idCoercion }
-----------------------------------
--- Generalisation case
+-- Skolemisation case (rule SKOL)
-- 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
-- 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)
+tc_sub outer act_sty act_ty exp_sty exp_ty
+ | isSigmaTy exp_ty
+ = do { (gen_fn, co_fn) <- tcGen exp_ty act_tvs $ \ body_exp_ty ->
+ tc_sub False act_sty act_ty body_exp_ty body_exp_ty
+ ; return (gen_fn <.> co_fn) }
+ where
+ act_tvs = tyVarsOfType act_ty
+ -- It's really important to check for escape wrt the free vars of
+ -- both expected_ty *and* actual_ty
-----------------------------------
--- Specialisation case:
+-- Specialisation case (rule ASPEC):
-- 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
+tc_sub outer act_sty actual_ty exp_sty expected_ty
| isSigmaTy actual_ty
- = tcInstType actual_ty `thenNF_Tc` \ (tvs, theta, body_ty) ->
- newDicts orig theta `thenNF_Tc` \ dicts ->
- let
- inst_fn e = mkHsDictApp (mkHsTyApp e (mkTyVarTys tvs))
- (map instToId dicts)
- in
- tc_sub exp_sty expected_ty body_ty body_ty `thenTc` \ (co_fn, lie) ->
- returnTc (co_fn <.> mkCoercion inst_fn, lie `plusLIE` mkLIE dicts)
- where
- orig = Rank2Origin
+ = do { (tyvars, theta, tau) <- tcInstBoxy actual_ty
+ ; dicts <- newDicts InstSigOrigin theta
+ ; extendLIEs dicts
+ ; let inst_fn = CoApps (CoTyApps CoHole (mkTyVarTys tyvars))
+ (map instToId dicts)
+ ; co_fn <- tc_sub False tau tau exp_sty expected_ty
+ ; return (co_fn <.> inst_fn) }
-----------------------------------
--- Function case
+-- Function case (rule F1)
+tc_sub _ _ (FunTy act_arg act_res) _ (FunTy exp_arg exp_res)
+ = tc_sub_funs act_arg act_res exp_arg exp_res
+
+-- Function case (rule F2)
+tc_sub outer act_sty act_ty@(FunTy act_arg act_res) exp_sty (TyVarTy exp_tv)
+ | isBoxyTyVar exp_tv
+ = do { cts <- readMetaTyVar exp_tv
+ ; case cts of
+ Indirect ty -> do { u_tys outer False act_sty act_ty True exp_sty ty
+ ; return idCoercion }
+ Flexi -> do { [arg_ty,res_ty] <- withMetaTvs exp_tv fun_kinds mk_res_ty
+ ; tc_sub_funs act_arg act_res arg_ty res_ty } }
+ where
+ mk_res_ty [arg_ty', res_ty'] = mkFunTy arg_ty' res_ty'
+ fun_kinds = [argTypeKind, openTypeKind]
+
+-- Everything else: defer to boxy matching
+tc_sub outer act_sty actual_ty exp_sty expected_ty
+ = do { u_tys outer False act_sty actual_ty False exp_sty expected_ty
+ ; return idCoercion }
-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
---
--- NB 1: we can't just unify the type variable with the type
--- because the type might not be a tau-type, and we aren't
--- allowed to instantiate an ordinary type variable with
--- a sigma-type
---
--- NB 2: 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 exp_sty `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 act_sty `thenNF_Tc` \ (exp_arg, exp_res) ->
- tcSub_fun exp_arg exp_res act_arg act_res
+tc_sub_funs act_arg act_res exp_arg exp_res
+ = do { uTys False act_arg False exp_arg
+ ; co_fn_res <- tc_sub False act_res act_res exp_res exp_res
+ ; wrapFunResCoercion [exp_arg] co_fn_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)
-\end{code}
-
-%************************************************************************
-%* *
-\subsection{Functions}
-%* *
-%************************************************************************
-
-\begin{code}
-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 ->
- let
- -- 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
- in
- returnTc (coercion, lie1 `plusLIE` lie2)
-
-imitateFun :: TcTyVar -> TcType -> NF_TcM (TcType, TcType)
-imitateFun tv ty
- = ASSERT( not (isHoleTyVar tv) )
- -- NB: tv is an *ordinary* tyvar and so are the new ones
-
- -- Check that tv isn't a type-signature type variable
- -- (This would be found later in checkSigTyVars, but
- -- we get a better error message if we do it here.)
- checkTcM (not (isSkolemTyVar tv))
- (failWithTcM (unifyWithSigErr tv ty)) `thenTc_`
-
- newTyVarTy openTypeKind `thenNF_Tc` \ arg ->
- newTyVarTy openTypeKind `thenNF_Tc` \ res ->
- putTcTyVar tv (mkFunTy arg res) `thenNF_Tc_`
- returnNF_Tc (arg,res)
+wrapFunResCoercion
+ :: [TcType] -- Type of args
+ -> ExprCoFn -- HsExpr a -> HsExpr b
+ -> TcM ExprCoFn -- HsExpr (arg_tys -> a) -> HsExpr (arg_tys -> b)
+wrapFunResCoercion arg_tys co_fn_res
+ | isIdCoercion co_fn_res = return idCoercion
+ | null arg_tys = return co_fn_res
+ | otherwise
+ = do { us <- newUniqueSupply
+ ; let arg_ids = zipWith (mkSysLocal FSLIT("sub")) (uniqsFromSupply us) arg_tys
+ ; return (CoLams arg_ids (co_fn_res <.> (CoApps CoHole arg_ids))) }
\end{code}
+
%************************************************************************
%* *
\subsection{Generalisation}
%************************************************************************
\begin{code}
-tcGen :: TcSigmaType -- expected_ty
- -> (TcPhiType -> TcM (result, LIE)) -- spec_ty
- -> TcM (ExprCoFn, result, LIE)
+tcGen :: BoxySigmaType -- expected_ty
+ -> TcTyVarSet -- Extra tyvars that the universally
+ -- quantified tyvars of expected_ty
+ -- must not be unified
+ -> (BoxyRhoType -> TcM result) -- spec_ty
+ -> TcM (ExprCoFn, result)
-- 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) ->
+tcGen expected_ty extra_tvs thing_inside -- We expect expected_ty to be a forall-type
+ -- If not, the call is a no-op
+ = do { -- We want the GenSkol info in the skolemised type variables to
+ -- mention the *instantiated* tyvar names, so that we get a
+ -- good error message "Rigid variable 'a' is bound by (forall a. a->a)"
+ -- Hence the tiresome but innocuous fixM
+ ((forall_tvs, theta, rho_ty), skol_info) <- fixM (\ ~(_, skol_info) ->
+ do { (forall_tvs, theta, rho_ty) <- tcInstSkolType skol_info expected_ty
+ ; span <- getSrcSpanM
+ ; let skol_info = GenSkol forall_tvs (mkPhiTy theta rho_ty) span
+ ; return ((forall_tvs, theta, rho_ty), skol_info) })
+
+#ifdef DEBUG
+ ; traceTc (text "tcGen" <+> vcat [text "extra_tvs" <+> ppr extra_tvs,
+ text "expected_ty" <+> ppr expected_ty,
+ text "inst ty" <+> ppr forall_tvs <+> ppr theta <+> ppr rho_ty,
+ text "free_tvs" <+> ppr free_tvs,
+ text "forall_tvs" <+> ppr forall_tvs])
+#endif
-- Type-check the arg and unify with poly type
- thing_inside phi_ty `thenTc` \ (result, lie) ->
+ ; (result, lie) <- getLIE (thing_inside rho_ty)
-- Check that the "forall_tvs" havn't been constrained
-- The interesting bit here is that we must include the free variables
-- 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) $
+ ; dicts <- newDicts (SigOrigin skol_info) theta
+ ; inst_binds <- tcSimplifyCheck sig_msg forall_tvs dicts lie
- 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 ->
+ ; checkSigTyVarsWrt free_tvs forall_tvs
+ ; traceTc (text "tcGen:done")
- let
+ ; let
-- 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))
- in
- returnTc (mkCoercion co_fn, result, free_lie)
+ dict_ids = map instToId dicts
+ co_fn = CoTyLams forall_tvs $ CoLams dict_ids $ CoLet inst_binds CoHole
+ ; returnM (co_fn, result) }
where
- free_tvs = tyVarsOfType expected_ty
- sig_msg = ptext SLIT("When generalising the type of an expression")
+ free_tvs = tyVarsOfType expected_ty `unionVarSet` extra_tvs
+ sig_msg = ptext SLIT("expected type of an expression")
\end{code}
%************************************************************************
%* *
-\subsection{Coercion functions}
-%* *
-%************************************************************************
-
-\begin{code}
-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
-\end{code}
-
-%************************************************************************
-%* *
-\subsection[Unify-exported]{Exported unification functions}
+ Boxy unification
%* *
%************************************************************************
The exported functions are all defined as versions of some
non-exported generic functions.
-Unify two @TauType@s. Dead straightforward.
-
-\begin{code}
-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
-\end{code}
-
-@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.
-
\begin{code}
-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!"
+boxyUnify :: BoxyType -> BoxyType -> TcM ()
+-- Acutal and expected, respectively
+boxyUnify ty1 ty2
+ = addErrCtxtM (unifyCtxt ty1 ty2) $
+ uTysOuter False ty1 False ty2
+
+---------------
+boxyUnifyList :: [BoxyType] -> [BoxyType] -> TcM ()
+-- Arguments should have equal length
+-- Acutal and expected types
+boxyUnifyList tys1 tys2 = uList boxyUnify tys1 tys2
+
+---------------
+unifyType :: TcTauType -> TcTauType -> TcM ()
+-- No boxes expected inside these types
+-- Acutal and expected types
+unifyType ty1 ty2 -- ty1 expected, ty2 inferred
+ = ASSERT2( not (isBoxyTy ty1), ppr ty1 )
+ ASSERT2( not (isBoxyTy ty2), ppr ty2 )
+ addErrCtxtM (unifyCtxt ty1 ty2) $
+ uTysOuter True ty1 True ty2
+
+---------------
+unifyPred :: PredType -> PredType -> TcM ()
+-- Acutal and expected types
+unifyPred p1 p2 = addErrCtxtM (unifyCtxt (mkPredTy p1) (mkPredTy p2)) $
+ uPred True True p1 True p2
+
+unifyTheta :: TcThetaType -> TcThetaType -> TcM ()
+-- Acutal and expected types
+unifyTheta theta1 theta2
+ = do { checkTc (equalLength theta1 theta2)
+ (ptext SLIT("Contexts differ in length"))
+ ; uList unifyPred theta1 theta2 }
+
+---------------
+uList :: (a -> a -> TcM ())
+ -> [a] -> [a] -> TcM ()
+-- Unify corresponding elements of two lists of types, which
+-- should be f equal length. We charge down the list explicitly so that
+-- we can complain if their lengths differ.
+uList unify [] [] = return ()
+uList unify (ty1:tys1) (ty2:tys2) = do { unify ty1 ty2; uList unify tys1 tys2 }
+uList unify ty1s ty2s = panic "Unify.uList: mismatched type lists!"
\end{code}
-@unifyTauTyList@ takes a single list of @TauType@s and unifies them
+@unifyTypeList@ 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.
\begin{code}
-unifyTauTyList :: [TcTauType] -> TcM ()
-unifyTauTyList [] = returnTc ()
-unifyTauTyList [ty] = returnTc ()
-unifyTauTyList (ty1:tys@(ty2:_)) = unifyTauTy ty1 ty2 `thenTc_`
- unifyTauTyList tys
+unifyTypeList :: [TcTauType] -> TcM ()
+unifyTypeList [] = returnM ()
+unifyTypeList [ty] = returnM ()
+unifyTypeList (ty1:tys@(ty2:_)) = do { unifyType ty1 ty2
+ ; unifyTypeList tys }
\end{code}
%************************************************************************
We call the first one \tr{ps_ty1}, \tr{ps_ty2} for ``possible synomym''.
\begin{code}
-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
+type NoBoxes = Bool -- True <=> definitely no boxes in this type
+ -- False <=> there might be boxes (always safe)
+
+type Outer = Bool -- True <=> this is the outer level of a unification
+ -- so that the types being unified are the
+ -- very ones we began with, not some sub
+ -- component or synonym expansion
+-- The idea is that if Outer is true then unifyMisMatch should
+-- pop the context to remove the "Expected/Acutal" context
+
+uTysOuter, uTys
+ :: NoBoxes -> TcType -- ty1 is the *expected* type
+ -> NoBoxes -> TcType -- ty2 is the *actual* type
-> TcM ()
+uTysOuter nb1 ty1 nb2 ty2 = u_tys True nb1 ty1 ty1 nb2 ty2 ty2
+uTys nb1 ty1 nb2 ty2 = u_tys False nb1 ty1 ty1 nb2 ty2 ty2
+
+
+--------------
+uTys_s :: NoBoxes -> [TcType] -- ty1 is the *actual* types
+ -> NoBoxes -> [TcType] -- ty2 is the *expected* types
+ -> TcM ()
+uTys_s nb1 [] nb2 [] = returnM ()
+uTys_s nb1 (ty1:tys1) nb2 (ty2:tys2) = do { uTys nb1 ty1 nb2 ty2
+ ; uTys_s nb1 tys1 nb2 tys2 }
+uTys_s nb1 ty1s nb2 ty2s = panic "Unify.uTys_s: mismatched type lists!"
+
+--------------
+u_tys :: Outer
+ -> NoBoxes -> TcType -> TcType -- ty1 is the *actual* type
+ -> NoBoxes -> TcType -> TcType -- ty2 is the *expected* type
+ -> TcM ()
+
+u_tys outer nb1 orig_ty1 ty1 nb2 orig_ty2 ty2
+ = go outer ty1 ty2
+ where
-- 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
+ go outer ty1 ty2
+ | Just ty1' <- tcView ty1 = go False ty1' ty2
+ | Just ty2' <- tcView ty2 = go False ty1 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
-
+ go outer (TyVarTy tyvar1) ty2 = uVar outer False tyvar1 nb2 orig_ty2 ty2
+ go outer ty1 (TyVarTy tyvar2) = uVar outer True tyvar2 nb1 orig_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
+ go outer (PredTy p1) (PredTy p2) = uPred outer nb1 p1 nb2 p2
-- Type constructors must match
-uTys ps_ty1 (TyConApp con1 tys1) ps_ty2 (TyConApp con2 tys2)
- | con1 == con2 && equalLength tys1 tys2
- = unifyTauTyLists tys1 tys2
+ go _ (TyConApp con1 tys1) (TyConApp con2 tys2)
+ | con1 == con2 = uTys_s nb1 tys1 nb2 tys2
+ -- See Note [TyCon app]
- | 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
+ -- Functions; just check the two parts
+ go _ (FunTy fun1 arg1) (FunTy fun2 arg2)
+ = do { uTys nb1 fun1 nb2 fun2
+ ; uTys nb1 arg1 nb2 arg2 }
-- 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
+ go outer (AppTy s1 t1) ty2
+ | Just (s2,t2) <- tcSplitAppTy_maybe ty2
+ = do { uTys nb1 s1 nb2 s2; uTys nb1 t1 nb2 t2 }
-- 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!
+ go outer ty1 (AppTy s2 t2)
+ | Just (s1,t1) <- tcSplitAppTy_maybe ty1
+ = do { uTys nb1 s1 nb2 s2; uTys nb1 t1 nb2 t2 }
+
+ go _ ty1@(ForAllTy _ _) ty2@(ForAllTy _ _)
+ | length tvs1 == length tvs2
+ = do { tvs <- tcInstSkolTyVars UnkSkol tvs1 -- Not a helpful SkolemInfo
+ ; let tys = mkTyVarTys tvs
+ in_scope = mkInScopeSet (mkVarSet tvs)
+ subst1 = mkTvSubst in_scope (zipTyEnv tvs1 tys)
+ subst2 = mkTvSubst in_scope (zipTyEnv tvs2 tys)
+ ; uTys nb1 (substTy subst1 body1) nb2 (substTy subst2 body2)
+
+ -- If both sides are inside a box, we should not have
+ -- a polytype at all. This check comes last, because
+ -- the error message is extremely unhelpful.
+ ; ifM (nb1 && nb2) (notMonoType ty1)
+ }
+ where
+ (tvs1, body1) = tcSplitForAllTys ty1
+ (tvs2, body2) = tcSplitForAllTys ty2
-- Anything else fails
-uTys ps_ty1 ty1 ps_ty2 ty2 = unifyMisMatch ps_ty1 ps_ty2
+ go outer _ _ = unifyMisMatch outer False orig_ty1 orig_ty2
+
+----------
+uPred outer nb1 (IParam n1 t1) nb2 (IParam n2 t2)
+ | n1 == n2 = uTys nb1 t1 nb2 t2
+uPred outer nb1 (ClassP c1 tys1) nb2 (ClassP c2 tys2)
+ | c1 == c2 = uTys_s nb1 tys1 nb2 tys2 -- Guaranteed equal lengths because the kinds check
+uPred outer _ p1 _ p2 = unifyMisMatch outer False (mkPredTy p1) (mkPredTy p2)
\end{code}
+Note [Tycon app]
+~~~~~~~~~~~~~~~~
+When we find two TyConApps, the argument lists are guaranteed equal
+length. Reason: intially the kinds of the two types to be unified is
+the same. The only way it can become not the same is when unifying two
+AppTys (f1 a1):=:(f2 a2). In that case there can't be a TyConApp in
+the f1,f2 (because it'd absorb the app). If we unify f1:=:f2 first,
+which we do, that ensures that f1,f2 have the same kind; and that
+means a1,a2 have the same kind. And now the argument repeats.
+
Notes on synonyms
~~~~~~~~~~~~~~~~~
-- 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 unifyTypepeLists args1 args2
-- NO else
-- NO -- Never mind. Just expand them and try again
-- NO uTys ty1 ty2
back into @uTys@ if it turns out that the variable is already bound.
\begin{code}
-uVar :: Bool -- False => tyvar is the "expected"
+uVar :: Outer
+ -> Bool -- False => tyvar is the "expected"
-- True => ty is the "expected" thing
-> TcTyVar
+ -> NoBoxes -- True <=> definitely no boxes in t2
-> 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)
-
+uVar outer swapped tv1 nb2 ps_ty2 ty2
+ = do { let expansion | showSDoc (ppr ty2) == showSDoc (ppr ps_ty2) = empty
+ | otherwise = brackets (equals <+> ppr ty2)
+ ; traceTc (text "uVar" <+> ppr swapped <+>
+ sep [ppr tv1 <+> dcolon <+> ppr (tyVarKind tv1 ),
+ nest 2 (ptext SLIT(" :=: ")),
+ ppr ps_ty2 <+> dcolon <+> ppr (typeKind ty2) <+> expansion])
+ ; details <- lookupTcTyVar tv1
+ ; case details of
+ IndirectTv ty1
+ | swapped -> u_tys outer nb2 ps_ty2 ty2 True ty1 ty1 -- Swap back
+ | otherwise -> u_tys outer True ty1 ty1 nb2 ps_ty2 ty2 -- Same order
+ -- The 'True' here says that ty1
+ -- is definitely box-free
+ DoneTv details1 -> uUnfilledVar outer swapped tv1 details1 nb2 ps_ty2 ty2
+ }
+
+----------------
+uUnfilledVar :: Outer
+ -> Bool -- Args are swapped
+ -> TcTyVar -> TcTyVarDetails -- Tyvar 1
+ -> NoBoxes -> TcTauType -> TcTauType -- Type 2
+ -> TcM ()
+-- Invariant: tyvar 1 is not unified with anything
+
+uUnfilledVar outer swapped tv1 details1 nb2 ps_ty2 ty2
+ | Just ty2' <- tcView ty2
+ = -- Expand synonyms; ignore FTVs
+ uUnfilledVar False swapped tv1 details1 nb2 ps_ty2 ty2'
+
+uUnfilledVar outer swapped tv1 details1 nb2 ps_ty2 ty2@(TyVarTy tv2)
-- Same type variable => no-op
| tv1 == tv2
- = returnTc ()
+ = returnM ()
-- 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'
+ = do { lookup2 <- lookupTcTyVar tv2
+ ; case lookup2 of
+ IndirectTv ty2' -> uUnfilledVar outer swapped tv1 details1 True ty2' ty2'
+ DoneTv details2 -> uUnfilledVars outer swapped tv1 details1 tv2 details2
+ }
+
+uUnfilledVar outer swapped tv1 details1 nb2 ps_ty2 non_var_ty2 -- ty2 is not a type variable
+ = case details1 of
+ MetaTv (SigTv _) ref1 -> mis_match -- Can't update a skolem with a non-type-variable
+ MetaTv info ref1 -> uMetaVar swapped tv1 info ref1 nb2 ps_ty2 non_var_ty2
+ skolem_details -> mis_match
+ where
+ mis_match = unifyMisMatch outer swapped (TyVarTy tv1) ps_ty2
+
+----------------
+uMetaVar :: Bool
+ -> TcTyVar -> BoxInfo -> IORef MetaDetails
+ -> NoBoxes -> TcType -> TcType
+ -> TcM ()
+-- tv1 is an un-filled-in meta type variable (maybe boxy, maybe tau)
+-- ty2 is not a type variable
+
+uMetaVar swapped tv1 info1 ref1 nb2 ps_ty2 non_var_ty2
+ = do { final_ty <- case info1 of
+ BoxTv -> unBox ps_ty2 -- No occurs check
+ other -> checkTauTvUpdate tv1 ps_ty2 -- Occurs check + monotype check
+ ; checkUpdateMeta swapped tv1 ref1 final_ty }
+
+----------------
+uUnfilledVars :: Outer
+ -> Bool -- Args are swapped
+ -> TcTyVar -> TcTyVarDetails -- Tyvar 1
+ -> TcTyVar -> TcTyVarDetails -- Tyvar 2
+ -> TcM ()
+-- Invarant: The type variables are distinct,
+-- Neither is filled in yet
+-- They might be boxy or not
+
+uUnfilledVars outer swapped tv1 (SkolemTv _) tv2 (SkolemTv _)
+ = unifyMisMatch outer swapped (mkTyVarTy tv1) (mkTyVarTy tv2)
+
+uUnfilledVars outer swapped tv1 (MetaTv info1 ref1) tv2 (SkolemTv _)
+ = checkUpdateMeta swapped tv1 ref1 (mkTyVarTy tv2)
+uUnfilledVars outer swapped tv1 (SkolemTv _) tv2 (MetaTv info2 ref2)
+ = checkUpdateMeta (not swapped) tv2 ref2 (mkTyVarTy tv1)
+
+-- ToDo: this function seems too long for what it acutally does!
+uUnfilledVars outer swapped tv1 (MetaTv info1 ref1) tv2 (MetaTv info2 ref2)
+ = case (info1, info2) of
+ (BoxTv, BoxTv) -> box_meets_box
+
+ -- If a box meets a TauTv, but the fomer has the smaller kind
+ -- then we must create a fresh TauTv with the smaller kind
+ (_, BoxTv) | k1_sub_k2 -> update_tv2
+ | otherwise -> box_meets_box
+ (BoxTv, _ ) | k2_sub_k1 -> update_tv1
+ | otherwise -> box_meets_box
+
+ -- Avoid SigTvs if poss
+ (SigTv _, _ ) | k1_sub_k2 -> update_tv2
+ (_, SigTv _) | k2_sub_k1 -> update_tv1
+
+ (_, _) | k1_sub_k2 -> if k2_sub_k1 && nicer_to_update_tv1
+ then update_tv1 -- Same kinds
+ else update_tv2
+ | k2_sub_k1 -> update_tv1
+ | otherwise -> kind_err
+
+ -- Update the variable with least kind info
+ -- See notes on type inference in Kind.lhs
+ -- The "nicer to" part only applies if the two kinds are the same,
+ -- so we can choose which to do.
+ where
+ -- Kinds should be guaranteed ok at this point
+ update_tv1 = updateMeta tv1 ref1 (mkTyVarTy tv2)
+ update_tv2 = updateMeta tv2 ref2 (mkTyVarTy tv1)
- Nothing | update_tv2
+ box_meets_box | k1_sub_k2 = fill_with k1
+ | k2_sub_k1 = fill_with k2
+ | otherwise = kind_err
- -> WARN( not (k1 `hasMoreBoxityInfo` k2), (ppr tv1 <+> ppr k1) $$ (ppr tv2 <+> ppr k2) )
- putTcTyVar tv2 (TyVarTy tv1) `thenNF_Tc_`
- returnTc ()
- | otherwise
+ fill_with kind = do { tau_ty <- newFlexiTyVarTy kind
+ ; updateMeta tv1 ref1 tau_ty
+ ; updateMeta tv2 ref2 tau_ty }
+
+ kind_err = addErrCtxtM (unifyKindCtxt swapped tv1 (mkTyVarTy tv2)) $
+ unifyKindMisMatch k1 k2
- -> WARN( not (k2 `hasMoreBoxityInfo` k1), (ppr tv2 <+> ppr k2) $$ (ppr tv1 <+> ppr k1) )
- putTcTyVar tv1 ps_ty2 `thenNF_Tc_`
- returnTc ()
- where
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 ()
- else
- 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 ()
- else
- failWithTcM (unifyOccurCheck tv1 ps_ty2')
-
+ k1_sub_k2 = k1 `isSubKind` k2
+ k2_sub_k1 = k2 `isSubKind` k1
+ nicer_to_update_tv1 = isSystemName (varName tv1)
+ -- Try to update sys-y type variables in preference to ones
+ -- gotten (say) by instantiating a polymorphic function with
+ -- a user-written type sig
+
+----------------
+checkUpdateMeta :: Bool -> TcTyVar -> IORef MetaDetails -> TcType -> TcM ()
+-- Update tv1, which is flexi; occurs check is alrady done
+-- The 'check' version does a kind check too
+-- We do a sub-kind check here: we might unify (a b) with (c d)
+-- where b::*->* and d::*; this should fail
+
+checkUpdateMeta swapped tv1 ref1 ty2
+ = do { checkKinds swapped tv1 ty2
+ ; updateMeta tv1 ref1 ty2 }
+
+updateMeta :: TcTyVar -> IORef MetaDetails -> TcType -> TcM ()
+updateMeta tv1 ref1 ty2
+ = ASSERT( isMetaTyVar tv1 )
+ ASSERT( isBoxyTyVar tv1 || isTauTy ty2 )
+ do { ASSERTM2( do { details <- readMetaTyVar tv1; return (isFlexi details) }, ppr tv1 )
+ ; traceTc (text "updateMeta" <+> ppr tv1 <+> text ":=" <+> ppr ty2)
+ ; writeMutVar ref1 (Indirect ty2) }
+
+----------------
checkKinds swapped tv1 ty2
-- We're about to unify a type variable tv1 with a non-tyvar-type ty2.
--- ty2 has been zonked at this stage.
-
- | tk2 `hasMoreBoxityInfo` tk1 = returnTc ()
+-- ty2 has been zonked at this stage, which ensures that
+-- its kind has as much boxity information visible as possible.
+ | tk2 `isSubKind` tk1 = returnM ()
| otherwise
-- Either the kinds aren't compatible
-- (can happen if we unify (a b) with (c d))
-- or we are unifying a lifted type variable with an
-- unlifted type: e.g. (id 3#) is illegal
- = tcAddErrCtxtM (unifyKindCtxt swapped tv1 ty2) $
- unifyMisMatch k1 k2
-
+ = addErrCtxtM (unifyKindCtxt swapped tv1 ty2) $
+ unifyKindMisMatch k1 k2
where
(k1,k2) | swapped = (tk2,tk1)
| otherwise = (tk1,tk2)
tk1 = tyVarKind tv1
tk2 = typeKind ty2
+
+----------------
+checkTauTvUpdate :: TcTyVar -> TcType -> TcM TcType
+-- (checkTauTvUpdate tv ty)
+-- We are about to update the TauTv tv with ty.
+-- Check (a) that tv doesn't occur in ty (occurs check)
+-- (b) that ty is a monotype
+-- Furthermore, in the interest of (b), if you find an
+-- empty box (BoxTv that is Flexi), fill it in with a TauTv
+--
+-- Returns the (non-boxy) type to update the type variable with, or fails
+
+checkTauTvUpdate orig_tv orig_ty
+ = go orig_ty
+ where
+ go (TyConApp tc tys)
+ | isSynTyCon tc = go_syn tc tys
+ | otherwise = do { tys' <- mappM go tys; return (TyConApp tc tys') }
+ go (NoteTy _ ty2) = go ty2 -- Discard free-tyvar annotations
+ go (PredTy p) = do { p' <- go_pred p; return (PredTy p') }
+ go (FunTy arg res) = do { arg' <- go arg; res' <- go res; return (FunTy arg' res') }
+ go (AppTy fun arg) = do { fun' <- go fun; arg' <- go arg; return (mkAppTy fun' arg') }
+ -- NB the mkAppTy; we might have instantiated a
+ -- type variable to a type constructor, so we need
+ -- to pull the TyConApp to the top.
+ go (ForAllTy tv ty) = notMonoType orig_ty -- (b)
+
+ go (TyVarTy tv)
+ | orig_tv == tv = occurCheck tv orig_ty -- (a)
+ | isTcTyVar tv = go_tyvar tv (tcTyVarDetails tv)
+ | otherwise = return (TyVarTy tv)
+ -- Ordinary (non Tc) tyvars
+ -- occur inside quantified types
+
+ go_pred (ClassP c tys) = do { tys' <- mapM go tys; return (ClassP c tys') }
+ go_pred (IParam n ty) = do { ty' <- go ty; return (IParam n ty') }
+
+ go_tyvar tv (SkolemTv _) = return (TyVarTy tv)
+ go_tyvar tv (MetaTv box ref)
+ = do { cts <- readMutVar ref
+ ; case cts of
+ Indirect ty -> go ty
+ Flexi -> case box of
+ BoxTv -> do { tau <- newFlexiTyVarTy (tyVarKind tv)
+ ; writeMutVar ref (Indirect tau)
+ ; return tau }
+ other -> return (TyVarTy tv)
+ }
+
+ -- go_syn is called for synonyms only
+ -- See Note [Type synonyms and the occur check]
+ go_syn tc tys
+ | not (isTauTyCon tc)
+ = notMonoType orig_ty -- (b) again
+ | otherwise
+ = do { (msgs, mb_tys') <- tryTc (mapM go tys)
+ ; case mb_tys' of
+ Just tys' -> return (TyConApp tc tys')
+ -- Retain the synonym (the common case)
+ Nothing -> go (expectJust "checkTauTvUpdate"
+ (tcView (TyConApp tc tys)))
+ -- Try again, expanding the synonym
+ }
\end{code}
+Note [Type synonyms and the occur check]
+~~~~~~~~~~~~~~~~~~~~
+Basically we want to update tv1 := ps_ty2
+because ps_ty2 has type-synonym info, which improves later error messages
-%************************************************************************
-%* *
-\subsection[Unify-fun]{@unifyFunTy@}
-%* *
-%************************************************************************
+But consider
+ type A a = ()
-@subFunTy@ and @unifyFunTy@ is used to avoid the fruitless
-creation of type variables.
+ f :: (A a -> a -> ()) -> ()
+ f = \ _ -> ()
-* subFunTy is used when we might be faced with a "hole" type variable,
- in which case we should create two new holes.
+ x :: ()
+ x = f (\ x p -> p x)
-* unifyFunTy is used when we expect to encounter only "ordinary"
- type variables, so we should create new ordinary type variables
-
-\begin{code}
-subFunTy :: TcSigmaType -- Fail if ty isn't a function type
- -> TcM (TcType, TcType) -- otherwise return arg and result types
-subFunTy ty@(TyVarTy tyvar)
-
- = getTcTyVar tyvar `thenNF_Tc` \ maybe_ty ->
- case maybe_ty of
- Just ty -> subFunTy ty
- Nothing | isHoleTyVar tyvar
- -> newHoleTyVarTy `thenNF_Tc` \ arg ->
- newHoleTyVarTy `thenNF_Tc` \ res ->
- putTcTyVar tyvar (mkFunTy arg res) `thenNF_Tc_`
- returnTc (arg,res)
- | otherwise
- -> unify_fun_ty_help ty
-
-subFunTy ty
- = case tcSplitFunTy_maybe ty of
- Just arg_and_res -> returnTc arg_and_res
- Nothing -> unify_fun_ty_help ty
-
-
-unifyFunTy :: TcPhiType -- Fail if ty isn't a function type
- -> TcM (TcType, TcType) -- otherwise return arg and result types
-
-unifyFunTy ty@(TyVarTy tyvar)
- = getTcTyVar tyvar `thenNF_Tc` \ maybe_ty ->
- case maybe_ty of
- Just ty' -> unifyFunTy ty'
- Nothing -> unify_fun_ty_help ty
-
-unifyFunTy ty
- = case tcSplitFunTy_maybe ty of
- Just arg_and_res -> returnTc arg_and_res
- Nothing -> unify_fun_ty_help ty
-
-unify_fun_ty_help ty -- Special cases failed, so revert to ordinary unification
- = newTyVarTy openTypeKind `thenNF_Tc` \ arg ->
- newTyVarTy openTypeKind `thenNF_Tc` \ res ->
- unifyTauTy ty (mkFunTy arg res) `thenTc_`
- returnTc (arg,res)
-\end{code}
+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).
\begin{code}
-unifyListTy :: TcType -- expected list type
- -> TcM TcType -- list element type
-
-unifyListTy ty@(TyVarTy tyvar)
- = getTcTyVar tyvar `thenNF_Tc` \ maybe_ty ->
- case maybe_ty of
- Just ty' -> unifyListTy ty'
- other -> unify_list_ty_help ty
-
-unifyListTy ty
- = case tcSplitTyConApp_maybe ty of
- Just (tycon, [arg_ty]) | tycon == listTyCon -> returnTc arg_ty
- other -> unify_list_ty_help ty
-
-unify_list_ty_help ty -- Revert to ordinary unification
- = newTyVarTy liftedTypeKind `thenNF_Tc` \ elt_ty ->
- unifyTauTy ty (mkListTy elt_ty) `thenTc_`
- returnTc elt_ty
-
--- variant for parallel arrays
+stripBoxyType :: BoxyType -> TcM TcType
+-- Strip all boxes from the input type, returning a non-boxy type.
+-- It's fine for there to be a polytype inside a box (c.f. unBox)
+-- All of the boxes should have been filled in by now;
+-- hence we return a TcType
+stripBoxyType ty = zonkType strip_tv ty
+ where
+ strip_tv tv = ASSERT( not (isBoxyTyVar tv) ) return (TyVarTy tv)
+ -- strip_tv will be called for *Flexi* meta-tyvars
+ -- There should not be any Boxy ones; hence the ASSERT
+
+zapToMonotype :: BoxySigmaType -> TcM TcTauType
+-- Subtle... we must zap the boxy res_ty
+-- to kind * before using it to instantiate a LitInst
+-- Calling unBox instead doesn't do the job, because the box
+-- often has an openTypeKind, and we don't want to instantiate
+-- with that type.
+zapToMonotype res_ty
+ = do { res_tau <- newFlexiTyVarTy liftedTypeKind
+ ; boxyUnify res_tau res_ty
+ ; return res_tau }
+
+unBox :: BoxyType -> TcM TcType
+-- unBox implements the judgement
+-- |- s' ~ box(s)
+-- with input s', and result s
+--
+-- It remove all boxes from the input type, returning a non-boxy type.
+-- A filled box in the type can only contain a monotype; unBox fails if not
+-- The type can have empty boxes, which unBox fills with a monotype
+--
+-- Compare this wth checkTauTvUpdate
--
-unifyPArrTy :: TcType -- expected list type
- -> TcM TcType -- list element type
-
-unifyPArrTy ty@(TyVarTy tyvar)
- = getTcTyVar tyvar `thenNF_Tc` \ maybe_ty ->
- case maybe_ty of
- Just ty' -> unifyPArrTy ty'
- _ -> unify_parr_ty_help ty
-unifyPArrTy ty
- = case tcSplitTyConApp_maybe ty of
- Just (tycon, [arg_ty]) | tycon == parrTyCon -> returnTc arg_ty
- _ -> unify_parr_ty_help ty
-
-unify_parr_ty_help ty -- Revert to ordinary unification
- = newTyVarTy liftedTypeKind `thenNF_Tc` \ elt_ty ->
- unifyTauTy ty (mkPArrTy elt_ty) `thenTc_`
- returnTc elt_ty
+-- For once, it's safe to treat synonyms as opaque!
+
+unBox (NoteTy n ty) = do { ty' <- unBox ty; return (NoteTy n ty') }
+unBox (TyConApp tc tys) = do { tys' <- mapM unBox tys; return (TyConApp tc tys') }
+unBox (AppTy f a) = do { f' <- unBox f; a' <- unBox a; return (mkAppTy f' a') }
+unBox (FunTy f a) = do { f' <- unBox f; a' <- unBox a; return (FunTy f' a') }
+unBox (PredTy p) = do { p' <- unBoxPred p; return (PredTy p') }
+unBox (ForAllTy tv ty) = ASSERT( isImmutableTyVar tv )
+ do { ty' <- unBox ty; return (ForAllTy tv ty') }
+unBox (TyVarTy tv)
+ | isTcTyVar tv -- It's a boxy type variable
+ , MetaTv BoxTv ref <- tcTyVarDetails tv -- NB: non-TcTyVars are possible
+ = do { cts <- readMutVar ref -- under nested quantifiers
+ ; case cts of
+ Indirect ty -> do { non_boxy_ty <- unBox ty
+ ; if isTauTy non_boxy_ty
+ then return non_boxy_ty
+ else notMonoType non_boxy_ty }
+ Flexi -> do { tau <- newFlexiTyVarTy (tyVarKind tv)
+ ; writeMutVar ref (Indirect tau)
+ ; return tau }
+ }
+ | otherwise -- Skolems, and meta-tau-variables
+ = return (TyVarTy tv)
+
+unBoxPred (ClassP cls tys) = do { tys' <- mapM unBox tys; return (ClassP cls tys') }
+unBoxPred (IParam ip ty) = do { ty' <- unBox ty; return (IParam ip ty') }
\end{code}
+
+
+%************************************************************************
+%* *
+\subsection[Unify-context]{Errors and contexts}
+%* *
+%************************************************************************
+
+Errors
+~~~~~~
+
\begin{code}
-unifyTupleTy :: Boxity -> Arity -> TcType -> TcM [TcType]
-unifyTupleTy boxity arity ty@(TyVarTy tyvar)
- = getTcTyVar tyvar `thenNF_Tc` \ maybe_ty ->
- case maybe_ty of
- Just ty' -> unifyTupleTy boxity arity ty'
- other -> unify_tuple_ty_help boxity arity ty
-
-unifyTupleTy boxity arity ty
- = case tcSplitTyConApp_maybe ty of
- Just (tycon, arg_tys)
- | isTupleTyCon tycon
- && tyConArity tycon == arity
- && tupleTyConBoxity tycon == boxity
- -> returnTc arg_tys
- other -> unify_tuple_ty_help boxity arity ty
-
-unify_tuple_ty_help boxity arity ty
- = newTyVarTys arity kind `thenNF_Tc` \ arg_tys ->
- unifyTauTy ty (mkTupleTy boxity arity arg_tys) `thenTc_`
- returnTc arg_tys
+unifyCtxt act_ty exp_ty tidy_env
+ = do { act_ty' <- zonkTcType act_ty
+ ; exp_ty' <- zonkTcType exp_ty
+ ; let (env1, exp_ty'') = tidyOpenType tidy_env exp_ty'
+ (env2, act_ty'') = tidyOpenType env1 act_ty'
+ ; return (env2, mkExpectedActualMsg act_ty'' exp_ty'') }
+
+----------------
+mkExpectedActualMsg act_ty exp_ty
+ = nest 2 (vcat [ text "Expected type" <> colon <+> ppr exp_ty,
+ text "Inferred type" <> colon <+> ppr act_ty ])
+
+----------------
+-- If an error happens we try to figure out whether the function
+-- function has been given too many or too few arguments, and say so.
+checkFunResCtxt fun actual_res_ty expected_res_ty tidy_env
+ = do { exp_ty' <- zonkTcType expected_res_ty
+ ; act_ty' <- zonkTcType actual_res_ty
+ ; let
+ (env1, exp_ty'') = tidyOpenType tidy_env exp_ty'
+ (env2, act_ty'') = tidyOpenType env1 act_ty'
+ (exp_args, _) = tcSplitFunTys exp_ty''
+ (act_args, _) = tcSplitFunTys act_ty''
+
+ len_act_args = length act_args
+ len_exp_args = length exp_args
+
+ message | len_exp_args < len_act_args = wrongArgsCtxt "too few" fun
+ | len_exp_args > len_act_args = wrongArgsCtxt "too many" fun
+ | otherwise = mkExpectedActualMsg act_ty'' exp_ty''
+ ; return (env2, message) }
+
+ where
+ wrongArgsCtxt too_many_or_few fun
+ = ptext SLIT("Probable cause:") <+> quotes (ppr fun)
+ <+> ptext SLIT("is applied to") <+> text too_many_or_few
+ <+> ptext SLIT("arguments")
+
+------------------
+unifyKindCtxt swapped tv1 ty2 tidy_env -- not swapped => tv1 expected, ty2 inferred
+ -- tv1 and ty2 are zonked already
+ = returnM msg
+ where
+ msg = (env2, ptext SLIT("When matching the kinds of") <+>
+ sep [quotes pp_expected <+> ptext SLIT("and"), quotes pp_actual])
+
+ (pp_expected, pp_actual) | swapped = (pp2, pp1)
+ | otherwise = (pp1, pp2)
+ (env1, tv1') = tidyOpenTyVar tidy_env tv1
+ (env2, ty2') = tidyOpenType env1 ty2
+ pp1 = ppr tv1' <+> dcolon <+> ppr (tyVarKind tv1)
+ pp2 = ppr ty2' <+> dcolon <+> ppr (typeKind ty2)
+
+unifyMisMatch outer swapped ty1 ty2
+ = do { (env, msg) <- if swapped then misMatchMsg ty1 ty2
+ else misMatchMsg ty2 ty1
+
+ -- This is the whole point of the 'outer' stuff
+ ; if outer then popErrCtxt (failWithTcM (env, msg))
+ else failWithTcM (env, msg)
+ }
+
+misMatchMsg ty1 ty2
+ = do { env0 <- tcInitTidyEnv
+ ; (env1, pp1, extra1) <- ppr_ty env0 ty1
+ ; (env2, pp2, extra2) <- ppr_ty env1 ty2
+ ; return (env2, sep [sep [ptext SLIT("Couldn't match expected type") <+> pp1,
+ nest 7 (ptext SLIT("against inferred type") <+> pp2)],
+ nest 2 extra1, nest 2 extra2]) }
+
+ppr_ty :: TidyEnv -> TcType -> TcM (TidyEnv, SDoc, SDoc)
+ppr_ty env ty
+ = do { ty' <- zonkTcType ty
+ ; let (env1,tidy_ty) = tidyOpenType env ty'
+ simple_result = (env1, quotes (ppr tidy_ty), empty)
+ ; case tidy_ty of
+ TyVarTy tv
+ | isSkolemTyVar tv -> return (env2, pp_rigid tv',
+ pprSkolTvBinding tv')
+ | otherwise -> return simple_result
+ where
+ (env2, tv') = tidySkolemTyVar env1 tv
+ other -> return simple_result }
+ where
+ pp_rigid tv = quotes (ppr tv) <+> parens (ptext SLIT("a rigid variable"))
+
+
+notMonoType ty
+ = do { ty' <- zonkTcType ty
+ ; env0 <- tcInitTidyEnv
+ ; let (env1, tidy_ty) = tidyOpenType env0 ty'
+ msg = ptext SLIT("Cannot match a monotype with") <+> ppr tidy_ty
+ ; failWithTcM (env1, msg) }
+
+occurCheck tyvar ty
+ = do { env0 <- tcInitTidyEnv
+ ; ty' <- zonkTcType ty
+ ; let (env1, tidy_tyvar) = tidyOpenTyVar env0 tyvar
+ (env2, tidy_ty) = tidyOpenType env1 ty'
+ extra = sep [ppr tidy_tyvar, char '=', ppr tidy_ty]
+ ; failWithTcM (env2, hang msg 2 extra) }
where
- kind | isBoxed boxity = liftedTypeKind
- | otherwise = openTypeKind
+ msg = ptext SLIT("Occurs check: cannot construct the infinite type:")
\end{code}
%************************************************************************
%* *
-\subsection{Kind unification}
+ Kind unification
%* *
%************************************************************************
+Unifying kinds is much, much simpler than unifying types.
+
\begin{code}
unifyKind :: TcKind -- Expected
-> TcKind -- Actual
-> TcM ()
-unifyKind k1 k2
- = tcAddErrCtxtM (unifyCtxt "kind" k1 k2) $
- uTys k1 k1 k2 k2
+unifyKind LiftedTypeKind LiftedTypeKind = returnM ()
+unifyKind UnliftedTypeKind UnliftedTypeKind = returnM ()
+
+unifyKind OpenTypeKind k2 | isOpenTypeKind k2 = returnM ()
+unifyKind ArgTypeKind k2 | isArgTypeKind k2 = returnM ()
+ -- Respect sub-kinding
+
+unifyKind (FunKind a1 r1) (FunKind a2 r2)
+ = do { unifyKind a2 a1; unifyKind r1 r2 }
+ -- Notice the flip in the argument,
+ -- so that the sub-kinding works right
+
+unifyKind (KindVar kv1) k2 = uKVar False kv1 k2
+unifyKind k1 (KindVar kv2) = uKVar True kv2 k1
+unifyKind k1 k2 = unifyKindMisMatch k1 k2
unifyKinds :: [TcKind] -> [TcKind] -> TcM ()
-unifyKinds [] [] = returnTc ()
-unifyKinds (k1:ks1) (k2:ks2) = unifyKind k1 k2 `thenTc_`
+unifyKinds [] [] = returnM ()
+unifyKinds (k1:ks1) (k2:ks2) = unifyKind k1 k2 `thenM_`
unifyKinds ks1 ks2
-unifyKinds _ _ = panic "unifyKinds: length mis-match"
+unifyKinds _ _ = panic "unifyKinds: length mis-match"
+
+----------------
+uKVar :: Bool -> KindVar -> TcKind -> TcM ()
+uKVar swapped kv1 k2
+ = do { mb_k1 <- readKindVar kv1
+ ; case mb_k1 of
+ Nothing -> uUnboundKVar swapped kv1 k2
+ Just k1 | swapped -> unifyKind k2 k1
+ | otherwise -> unifyKind k1 k2 }
+
+----------------
+uUnboundKVar :: Bool -> KindVar -> TcKind -> TcM ()
+uUnboundKVar swapped kv1 k2@(KindVar kv2)
+ | kv1 == kv2 = returnM ()
+ | otherwise -- Distinct kind variables
+ = do { mb_k2 <- readKindVar kv2
+ ; case mb_k2 of
+ Just k2 -> uUnboundKVar swapped kv1 k2
+ Nothing -> writeKindVar kv1 k2 }
+
+uUnboundKVar swapped kv1 non_var_k2
+ = do { k2' <- zonkTcKind non_var_k2
+ ; kindOccurCheck kv1 k2'
+ ; k2'' <- kindSimpleKind swapped k2'
+ -- KindVars must be bound only to simple kinds
+ -- Polarities: (kindSimpleKind True ?) succeeds
+ -- returning *, corresponding to unifying
+ -- expected: ?
+ -- actual: kind-ver
+ ; writeKindVar kv1 k2'' }
+
+----------------
+kindOccurCheck kv1 k2 -- k2 is zonked
+ = checkTc (not_in k2) (kindOccurCheckErr kv1 k2)
+ where
+ not_in (KindVar kv2) = kv1 /= kv2
+ not_in (FunKind a2 r2) = not_in a2 && not_in r2
+ not_in other = True
+
+kindSimpleKind :: Bool -> Kind -> TcM SimpleKind
+-- (kindSimpleKind True k) returns a simple kind sk such that sk <: k
+-- If the flag is False, it requires k <: sk
+-- E.g. kindSimpleKind False ?? = *
+-- What about (kv -> *) :=: ?? -> *
+kindSimpleKind orig_swapped orig_kind
+ = go orig_swapped orig_kind
+ where
+ go sw (FunKind k1 k2) = do { k1' <- go (not sw) k1
+ ; k2' <- go sw k2
+ ; return (FunKind k1' k2') }
+ go True OpenTypeKind = return liftedTypeKind
+ go True ArgTypeKind = return liftedTypeKind
+ go sw LiftedTypeKind = return liftedTypeKind
+ go sw k@(KindVar _) = return k -- KindVars are always simple
+ go swapped kind = failWithTc (ptext SLIT("Unexpected kind unification failure:")
+ <+> ppr orig_swapped <+> ppr orig_kind)
+ -- I think this can't actually happen
+
+-- T v = MkT v v must be a type
+-- T v w = MkT (v -> w) v must not be an umboxed tuple
+
+----------------
+kindOccurCheckErr tyvar ty
+ = hang (ptext SLIT("Occurs check: cannot construct the infinite kind:"))
+ 2 (sep [ppr tyvar, char '=', ppr ty])
+
+unifyKindMisMatch ty1 ty2
+ = zonkTcKind ty1 `thenM` \ ty1' ->
+ zonkTcKind ty2 `thenM` \ ty2' ->
+ let
+ msg = hang (ptext SLIT("Couldn't match kind"))
+ 2 (sep [quotes (ppr ty1'),
+ ptext SLIT("against"),
+ quotes (ppr ty2')])
+ in
+ failWithTc msg
\end{code}
\begin{code}
-unifyOpenTypeKind :: TcKind -> TcM ()
--- Ensures that the argument kind is of the form (Type bx)
--- for some boxity bx
-
-unifyOpenTypeKind ty@(TyVarTy tyvar)
- = getTcTyVar tyvar `thenNF_Tc` \ maybe_ty ->
- case maybe_ty of
- Just ty' -> unifyOpenTypeKind ty'
- other -> unify_open_kind_help ty
-
-unifyOpenTypeKind ty
- | isTypeKind ty = returnTc ()
- | otherwise = unify_open_kind_help ty
-
-unify_open_kind_help ty -- Revert to ordinary unification
- = newBoxityVar `thenNF_Tc` \ boxity ->
- unifyKind ty (mkTyConApp typeCon [boxity])
+unifyFunKind :: TcKind -> TcM (Maybe (TcKind, TcKind))
+-- Like unifyFunTy, but does not fail; instead just returns Nothing
+
+unifyFunKind (KindVar kvar)
+ = readKindVar kvar `thenM` \ maybe_kind ->
+ case maybe_kind of
+ Just fun_kind -> unifyFunKind fun_kind
+ Nothing -> do { arg_kind <- newKindVar
+ ; res_kind <- newKindVar
+ ; writeKindVar kvar (mkArrowKind arg_kind res_kind)
+ ; returnM (Just (arg_kind,res_kind)) }
+
+unifyFunKind (FunKind arg_kind res_kind) = returnM (Just (arg_kind,res_kind))
+unifyFunKind other = returnM Nothing
\end{code}
-
%************************************************************************
%* *
-\subsection[Unify-context]{Errors and contexts}
+ Checking kinds
%* *
%************************************************************************
-Errors
-~~~~~~
+---------------------------
+-- We would like to get a decent error message from
+-- (a) Under-applied type constructors
+-- f :: (Maybe, Maybe)
+-- (b) Over-applied type constructors
+-- f :: Int x -> Int x
+--
\begin{code}
-unifyCtxt s ty1 ty2 tidy_env -- ty1 expected, ty2 inferred
- = zonkTcType ty1 `thenNF_Tc` \ ty1' ->
- zonkTcType ty2 `thenNF_Tc` \ ty2' ->
- returnNF_Tc (err ty1' ty2')
- where
- err ty1 ty2 = (env1,
- nest 4
- (vcat [
- text "Expected" <+> text s <> colon <+> ppr tidy_ty1,
- text "Inferred" <+> text s <> colon <+> ppr tidy_ty2
- ]))
- where
- (env1, [tidy_ty1,tidy_ty2]) = tidyOpenTypes tidy_env [ty1,ty2]
-
-unifyKindCtxt swapped tv1 ty2 tidy_env -- not swapped => tv1 expected, ty2 inferred
- -- tv1 is zonked already
- = zonkTcType ty2 `thenNF_Tc` \ ty2' ->
- returnNF_Tc (err ty2')
- where
- err ty2 = (env2, ptext SLIT("When matching types") <+>
- sep [quotes pp_expected, ptext SLIT("and"), quotes pp_actual])
- where
- (pp_expected, pp_actual) | swapped = (pp2, pp1)
- | otherwise = (pp1, pp2)
- (env1, tv1') = tidyOpenTyVar tidy_env tv1
- (env2, ty2') = tidyOpenType env1 ty2
- pp1 = ppr tv1'
- pp2 = ppr ty2'
-
-unifyMisMatch ty1 ty2
- = zonkTcType ty1 `thenNF_Tc` \ ty1' ->
- zonkTcType ty2 `thenNF_Tc` \ ty2' ->
- let
- (env, [tidy_ty1, tidy_ty2]) = tidyOpenTypes emptyTidyEnv [ty1',ty2']
- msg = hang (ptext SLIT("Couldn't match"))
- 4 (sep [quotes (ppr tidy_ty1),
- ptext SLIT("against"),
- quotes (ppr tidy_ty2)])
- in
- failWithTcM (env, msg)
-
-unifyWithSigErr tyvar ty
- = (env2, hang (ptext SLIT("Cannot unify the type-signature variable") <+> quotes (ppr tidy_tyvar))
- 4 (ptext SLIT("with the type") <+> quotes (ppr tidy_ty)))
- where
- (env1, tidy_tyvar) = tidyOpenTyVar emptyTidyEnv tyvar
- (env2, tidy_ty) = tidyOpenType env1 ty
-
-unifyOccurCheck tyvar ty
- = (env2, hang (ptext SLIT("Occurs check: cannot construct the infinite type:"))
- 4 (sep [ppr tidy_tyvar, char '=', ppr tidy_ty]))
- where
- (env1, tidy_tyvar) = tidyOpenTyVar emptyTidyEnv tyvar
- (env2, tidy_ty) = tidyOpenType env1 ty
+checkExpectedKind :: Outputable a => a -> TcKind -> TcKind -> TcM ()
+-- A fancy wrapper for 'unifyKind', which tries
+-- to give decent error messages.
+checkExpectedKind ty act_kind exp_kind
+ | act_kind `isSubKind` exp_kind -- Short cut for a very common case
+ = returnM ()
+ | otherwise
+ = tryTc (unifyKind exp_kind act_kind) `thenM` \ (_errs, mb_r) ->
+ case mb_r of {
+ Just r -> returnM () ; -- Unification succeeded
+ Nothing ->
+
+ -- So there's definitely an error
+ -- Now to find out what sort
+ zonkTcKind exp_kind `thenM` \ exp_kind ->
+ zonkTcKind act_kind `thenM` \ act_kind ->
+
+ tcInitTidyEnv `thenM` \ env0 ->
+ let (exp_as, _) = splitKindFunTys exp_kind
+ (act_as, _) = splitKindFunTys act_kind
+ n_exp_as = length exp_as
+ n_act_as = length act_as
+
+ (env1, tidy_exp_kind) = tidyKind env0 exp_kind
+ (env2, tidy_act_kind) = tidyKind env1 act_kind
+
+ err | n_exp_as < n_act_as -- E.g. [Maybe]
+ = quotes (ppr ty) <+> ptext SLIT("is not applied to enough type arguments")
+
+ -- Now n_exp_as >= n_act_as. In the next two cases,
+ -- n_exp_as == 0, and hence so is n_act_as
+ | isLiftedTypeKind exp_kind && isUnliftedTypeKind act_kind
+ = ptext SLIT("Expecting a lifted type, but") <+> quotes (ppr ty)
+ <+> ptext SLIT("is unlifted")
+
+ | isUnliftedTypeKind exp_kind && isLiftedTypeKind act_kind
+ = ptext SLIT("Expecting an unlifted type, but") <+> quotes (ppr ty)
+ <+> ptext SLIT("is lifted")
+
+ | otherwise -- E.g. Monad [Int]
+ = ptext SLIT("Kind mis-match")
+
+ more_info = sep [ ptext SLIT("Expected kind") <+>
+ quotes (pprKind tidy_exp_kind) <> comma,
+ ptext SLIT("but") <+> quotes (ppr ty) <+>
+ ptext SLIT("has kind") <+> quotes (pprKind tidy_act_kind)]
+ in
+ failWithTcM (env2, err $$ more_info)
+ }
\end{code}
-
-
%************************************************************************
%* *
\subsection{Checking signature type variables}
%* *
%************************************************************************
-@checkSigTyVars@ is used after the type in a type signature has been unified with
-the actual type found. It then checks that the type variables of the type signature
-are
- (a) Still all type variables
- eg matching signature [a] against inferred type [(p,q)]
- [then a will be unified to a non-type variable]
+@checkSigTyVars@ checks that a set of universally quantified type varaibles
+are not mentioned in the environment. In particular:
- (b) Still all distinct
- eg matching signature [(a,b)] against inferred type [(p,p)]
- [then a and b will be unified together]
-
- (c) Not mentioned in the environment
+ (a) Not mentioned in the type of a variable in the envt
eg the signature for f in this:
g x = ... where
Before doing this, the substitution is applied to the signature type variable.
-We used to have the notion of a "DontBind" type variable, which would
-only be bound to itself or nothing. Then points (a) and (b) were
-self-checking. But it gave rise to bogus consequential error messages.
-For example:
-
- f = (*) -- Monomorphic
-
- g :: Num a => a -> a
- g x = f x x
-
-Here, we get a complaint when checking the type signature for g,
-that g isn't polymorphic enough; but then we get another one when
-dealing with the (Num x) context arising from f's definition;
-we try to unify x with Int (to default it), but find that x has already
-been unified with the DontBind variable "a" from g's signature.
-This is really a problem with side-effecting unification; we'd like to
-undo g's effects when its type signature fails, but unification is done
-by side effect, so we can't (easily).
-
-So we revert to ordinary type variables for signatures, and try to
-give a helpful message in checkSigTyVars.
-
\begin{code}
-checkSigTyVars :: [TcTyVar] -- Universally-quantified type variables in the signature
- -> TcTyVarSet -- Tyvars that are free in the type signature
- -- Not necessarily zonked
- -- These should *already* be in the free-in-env set,
- -- and are used here only to improve the error message
- -> TcM [TcTyVar] -- Zonked signature type variables
-
-checkSigTyVars [] free = returnTc []
-checkSigTyVars sig_tyvars free_tyvars
- = zonkTcTyVars sig_tyvars `thenNF_Tc` \ sig_tys ->
- tcGetGlobalTyVars `thenNF_Tc` \ globals ->
-
- checkTcM (allDistinctTyVars sig_tys globals)
- (complain sig_tys globals) `thenTc_`
-
- returnTc (map (tcGetTyVar "checkSigTyVars") sig_tys)
-
+checkSigTyVars :: [TcTyVar] -> TcM ()
+checkSigTyVars sig_tvs = check_sig_tyvars emptyVarSet sig_tvs
+
+checkSigTyVarsWrt :: TcTyVarSet -> [TcTyVar] -> TcM ()
+-- The extra_tvs can include boxy type variables;
+-- e.g. TcMatches.tcCheckExistentialPat
+checkSigTyVarsWrt extra_tvs sig_tvs
+ = do { extra_tvs' <- zonkTcTyVarsAndFV (varSetElems extra_tvs)
+ ; check_sig_tyvars extra_tvs' sig_tvs }
+
+check_sig_tyvars
+ :: TcTyVarSet -- Global type variables. The universally quantified
+ -- tyvars should not mention any of these
+ -- Guaranteed already zonked.
+ -> [TcTyVar] -- Universally-quantified type variables in the signature
+ -- Guaranteed to be skolems
+ -> TcM ()
+check_sig_tyvars extra_tvs []
+ = returnM ()
+check_sig_tyvars extra_tvs sig_tvs
+ = ASSERT( all isSkolemTyVar sig_tvs )
+ do { gbl_tvs <- tcGetGlobalTyVars
+ ; traceTc (text "check_sig_tyvars" <+> (vcat [text "sig_tys" <+> ppr sig_tvs,
+ text "gbl_tvs" <+> ppr gbl_tvs,
+ text "extra_tvs" <+> ppr extra_tvs]))
+
+ ; let env_tvs = gbl_tvs `unionVarSet` extra_tvs
+ ; ifM (any (`elemVarSet` env_tvs) sig_tvs)
+ (bleatEscapedTvs env_tvs sig_tvs sig_tvs)
+ }
+
+bleatEscapedTvs :: TcTyVarSet -- The global tvs
+ -> [TcTyVar] -- The possibly-escaping type variables
+ -> [TcTyVar] -- The zonked versions thereof
+ -> TcM ()
+-- Complain about escaping type variables
+-- We pass a list of type variables, at least one of which
+-- escapes. The first list contains the original signature type variable,
+-- while the second contains the type variable it is unified to (usually itself)
+bleatEscapedTvs globals sig_tvs zonked_tvs
+ = do { env0 <- tcInitTidyEnv
+ ; let (env1, tidy_tvs) = tidyOpenTyVars env0 sig_tvs
+ (env2, tidy_zonked_tvs) = tidyOpenTyVars env1 zonked_tvs
+
+ ; (env3, msgs) <- foldlM check (env2, []) (tidy_tvs `zip` tidy_zonked_tvs)
+ ; failWithTcM (env3, main_msg $$ nest 2 (vcat msgs)) }
where
- complain sig_tys globals
- = -- "check" checks each sig tyvar in turn
- foldlNF_Tc check
- (env2, emptyVarEnv, [])
- (tidy_tvs `zip` tidy_tys) `thenNF_Tc` \ (env3, _, msgs) ->
-
- failWithTcM (env3, main_msg $$ vcat msgs)
- where
- (env1, tidy_tvs) = tidyOpenTyVars emptyTidyEnv sig_tyvars
- (env2, tidy_tys) = tidyOpenTypes env1 sig_tys
-
- main_msg = ptext SLIT("Inferred type is less polymorphic than expected")
-
- check (tidy_env, acc, msgs) (sig_tyvar,ty)
- -- sig_tyvar is from the signature;
- -- ty is what you get if you zonk sig_tyvar and then tidy it
- --
- -- acc maps a zonked type variable back to a signature type variable
- = case tcGetTyVar_maybe ty of {
- Nothing -> -- Error (a)!
- returnNF_Tc (tidy_env, acc, unify_msg sig_tyvar (quotes (ppr ty)) : msgs) ;
-
- Just tv ->
-
- case lookupVarEnv acc tv of {
- Just sig_tyvar' -> -- Error (b)!
- returnNF_Tc (tidy_env, acc, unify_msg sig_tyvar thing : msgs)
- where
- thing = ptext SLIT("another quantified type variable") <+> quotes (ppr sig_tyvar')
-
- ; Nothing ->
-
- if tv `elemVarSet` globals -- Error (c) or (d)! Type variable escapes
- -- The least comprehensible, so put it last
- -- Game plan:
- -- a) get the local TcIds and TyVars from the environment,
- -- and pass them to find_globals (they might have tv free)
- -- b) similarly, find any free_tyvars that mention tv
- then tcGetEnv `thenNF_Tc` \ ve ->
- find_globals tv tidy_env (tcLEnvElts ve) `thenNF_Tc` \ (tidy_env1, globs) ->
- find_frees tv tidy_env1 [] (varSetElems free_tyvars) `thenNF_Tc` \ (tidy_env2, frees) ->
- returnNF_Tc (tidy_env2, acc, escape_msg sig_tyvar tv globs frees : msgs)
-
- else -- All OK
- returnNF_Tc (tidy_env, extendVarEnv acc tv sig_tyvar, msgs)
- }}
-
------------------------
--- find_globals looks at the value environment and finds values
--- whose types mention the offending type variable. It has to be
--- careful to zonk the Id's type first, so it has to be in the monad.
--- We must be careful to pass it a zonked type variable, too.
-
-find_globals :: Var
- -> TidyEnv
- -> [TcTyThing]
- -> NF_TcM (TidyEnv, [SDoc])
-
-find_globals tv tidy_env things
- = go tidy_env [] things
- where
- go tidy_env acc [] = returnNF_Tc (tidy_env, acc)
- go tidy_env acc (thing : things)
- = find_thing ignore_it tidy_env thing `thenNF_Tc` \ (tidy_env1, maybe_doc) ->
- case maybe_doc of
- Just d -> go tidy_env1 (d:acc) things
- Nothing -> go tidy_env1 acc things
-
- ignore_it ty = not (tv `elemVarSet` tyVarsOfType ty)
+ main_msg = ptext SLIT("Inferred type is less polymorphic than expected")
------------------------
-find_thing ignore_it tidy_env (ATcId id)
- = zonkTcType (idType id) `thenNF_Tc` \ id_ty ->
- if ignore_it id_ty then
- returnNF_Tc (tidy_env, Nothing)
- else let
- (tidy_env', tidy_ty) = tidyOpenType tidy_env id_ty
- msg = sep [ppr id <+> dcolon <+> ppr tidy_ty,
- nest 2 (parens (ptext SLIT("bound at") <+>
- ppr (getSrcLoc id)))]
- in
- returnNF_Tc (tidy_env', Just msg)
-
-find_thing ignore_it tidy_env (ATyVar tv)
- = zonkTcTyVar tv `thenNF_Tc` \ tv_ty ->
- if ignore_it tv_ty then
- returnNF_Tc (tidy_env, Nothing)
- else let
- (tidy_env1, tv1) = tidyOpenTyVar tidy_env tv
- (tidy_env2, tidy_ty) = tidyOpenType tidy_env1 tv_ty
- msg = sep [ptext SLIT("Type variable") <+> quotes (ppr tv1) <+> eq_stuff, nest 2 bound_at]
-
- eq_stuff | Just tv' <- Type.getTyVar_maybe tv_ty, tv == tv' = empty
- | otherwise = equals <+> ppr tv_ty
- -- It's ok to use Type.getTyVar_maybe because ty is zonked by now
-
- bound_at = tyVarBindingInfo tv
- in
- returnNF_Tc (tidy_env2, Just msg)
+ check (tidy_env, msgs) (sig_tv, zonked_tv)
+ | not (zonked_tv `elemVarSet` globals) = return (tidy_env, msgs)
+ | otherwise
+ = do { (tidy_env1, globs) <- findGlobals (unitVarSet zonked_tv) tidy_env
+ ; returnM (tidy_env1, escape_msg sig_tv zonked_tv globs : msgs) }
-----------------------
-find_frees tv tidy_env acc []
- = returnNF_Tc (tidy_env, acc)
-find_frees tv tidy_env acc (ftv:ftvs)
- = zonkTcTyVar ftv `thenNF_Tc` \ ty ->
- if tv `elemVarSet` tyVarsOfType ty then
- let
- (tidy_env', ftv') = tidyOpenTyVar tidy_env ftv
- in
- find_frees tv tidy_env' (ftv':acc) ftvs
- else
- find_frees tv tidy_env acc ftvs
-
-
-escape_msg sig_tv tv globs frees
- = mk_msg sig_tv <+> ptext SLIT("escapes") $$
- if not (null globs) then
- vcat [pp_it <+> ptext SLIT("is mentioned in the environment:"),
- nest 2 (vcat globs)]
- else if not (null frees) then
- vcat [ptext SLIT("It is reachable from the type variable(s)") <+> pprQuotedList frees,
- nest 2 (ptext SLIT("which") <+> is_are <+> ptext SLIT("free in the signature"))
- ]
- else
- empty -- Sigh. It's really hard to give a good error message
- -- all the time. One bad case is an existential pattern match
+escape_msg sig_tv zonked_tv globs
+ | notNull globs
+ = vcat [sep [msg, ptext SLIT("is mentioned in the environment:")],
+ nest 2 (vcat globs)]
+ | otherwise
+ = msg <+> ptext SLIT("escapes")
+ -- Sigh. It's really hard to give a good error message
+ -- all the time. One bad case is an existential pattern match.
+ -- We rely on the "When..." context to help.
where
- is_are | isSingleton frees = ptext SLIT("is")
- | otherwise = ptext SLIT("are")
- pp_it | sig_tv /= tv = ptext SLIT("It unifies with") <+> quotes (ppr tv) <> comma <+> ptext SLIT("which")
- | otherwise = ptext SLIT("It")
-
- vcat_first :: Int -> [SDoc] -> SDoc
- vcat_first n [] = empty
- vcat_first 0 (x:xs) = text "...others omitted..."
- vcat_first n (x:xs) = x $$ vcat_first (n-1) xs
-
-
-unify_msg tv thing = mk_msg tv <+> ptext SLIT("is unified with") <+> thing
-mk_msg tv = ptext SLIT("Quantified type variable") <+> quotes (ppr tv)
+ msg = ptext SLIT("Quantified type variable") <+> quotes (ppr sig_tv) <+> is_bound_to
+ is_bound_to
+ | sig_tv == zonked_tv = empty
+ | otherwise = ptext SLIT("is unified with") <+> quotes (ppr zonked_tv) <+> ptext SLIT("which")
\end{code}
These two context are used with checkSigTyVars
\begin{code}
-sigCtxt :: [TcTyVar] -> TcThetaType -> TcTauType
- -> TidyEnv -> NF_TcM (TidyEnv, Message)
-sigCtxt sig_tyvars sig_theta sig_tau tidy_env
- = zonkTcType sig_tau `thenNF_Tc` \ actual_tau ->
+sigCtxt :: Id -> [TcTyVar] -> TcThetaType -> TcTauType
+ -> TidyEnv -> TcM (TidyEnv, Message)
+sigCtxt id sig_tvs sig_theta sig_tau tidy_env
+ = zonkTcType sig_tau `thenM` \ actual_tau ->
let
- (env1, tidy_sig_tyvars) = tidyOpenTyVars tidy_env sig_tyvars
- (env2, tidy_sig_rho) = tidyOpenType env1 (mkRhoTy sig_theta sig_tau)
- (env3, tidy_actual_tau) = tidyOpenType env2 actual_tau
- msg = vcat [ptext SLIT("Signature type: ") <+> pprType (mkForAllTys tidy_sig_tyvars tidy_sig_rho),
- ptext SLIT("Type to generalise:") <+> pprType tidy_actual_tau
+ (env1, tidy_sig_tvs) = tidyOpenTyVars tidy_env sig_tvs
+ (env2, tidy_sig_rho) = tidyOpenType env1 (mkPhiTy sig_theta sig_tau)
+ (env3, tidy_actual_tau) = tidyOpenType env2 actual_tau
+ sub_msg = vcat [ptext SLIT("Signature type: ") <+> pprType (mkForAllTys tidy_sig_tvs tidy_sig_rho),
+ ptext SLIT("Type to generalise:") <+> pprType tidy_actual_tau
]
+ msg = vcat [ptext SLIT("When trying to generalise the type inferred for") <+> quotes (ppr id),
+ nest 2 sub_msg]
in
- returnNF_Tc (env3, msg)
-
-sigPatCtxt bound_tvs bound_ids tidy_env
- = returnNF_Tc (env1,
- sep [ptext SLIT("When checking a pattern that binds"),
- nest 4 (vcat (zipWith ppr_id show_ids tidy_tys))])
- where
- show_ids = filter is_interesting bound_ids
- is_interesting id = any (`elemVarSet` idFreeTyVars id) bound_tvs
-
- (env1, tidy_tys) = tidyOpenTypes tidy_env (map idType show_ids)
- ppr_id id ty = ppr id <+> dcolon <+> ppr ty
- -- Don't zonk the types so we get the separate, un-unified versions
+ returnM (env3, msg)
\end{code}
-
-
projects / ghc-hetmet.git / blobdiff