%
% (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
%
-\section[Unify]{Unifier}
-
-The unifier is now squarely in the typechecker monad (because of the
-updatable substitution).
+\section{Type subsumption and unification}
\begin{code}
-module TcUnify ( unifyTauTy, unifyTauTyList, unifyTauTyLists,
- unifyFunTy, unifyListTy, unifyTupleTy,
- unifyKind, unifyKinds, unifyOpenTypeKind
- ) where
+module TcUnify (
+ -- Full-blown subsumption
+ tcSubExp, tcGen,
+ checkSigTyVars, checkSigTyVarsWrt, bleatEscapedTvs, sigCtxt,
+
+ -- Various unifications
+ 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"
--- friends:
-import TcMonad
-import TypeRep ( Type(..), PredType(..) ) -- friend
-import Type ( funTyCon, Kind, unboxedTypeKind, boxedTypeKind, openTypeKind,
- superBoxity, typeCon, openKindCon, hasMoreBoxityInfo,
- tyVarsOfType, typeKind,
- mkTyVarTy, mkFunTy, splitFunTy_maybe, splitTyConApp_maybe,
- isNotUsgTy, splitAppTy_maybe, mkTyConApp,
- tidyOpenType, tidyOpenTypes, tidyTyVar
- )
-import TyCon ( TyCon, isTupleTyCon, tupleTyConBoxity, tyConArity )
-import Name ( hasBetterProv )
-import Var ( TyVar, tyVarKind, varName, isSigTyVar )
-import VarSet ( varSetElems )
-import TcType ( TcType, TcTauType, TcTyVar, TcKind, newBoxityVar,
- newTyVarTy, newTyVarTys, tcGetTyVar, tcPutTyVar, zonkTcType
- )
-
--- others:
-import BasicTypes ( Arity, Boxity, isBoxed )
-import TysWiredIn ( listTyCon, mkListTy, mkTupleTy )
+import HsSyn ( ExprCoFn(..), idCoercion, isIdCoercion, (<.>) )
+import TypeRep ( Type(..), PredType(..) )
+
+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 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, mkTyVarTys,
+ tyVarsOfType, mkPhiTy, mkTyVarTy, mkPredTy,
+ typeKind, mkForAllTys, mkAppTy, isBoxyTyVar,
+ tidyOpenType, tidyOpenTypes, 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 )
+import ErrUtils ( Message )
+import Maybes ( fromJust, 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{The Kind variants}
+ subFunTys
%* *
%************************************************************************
\begin{code}
-unifyKind :: TcKind -- Expected
- -> TcKind -- Actual
- -> TcM ()
-unifyKind k1 k2
- = tcAddErrCtxtM (unifyCtxt "kind" k1 k2) $
- uTys k1 k1 k2 k2
+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
-unifyKinds :: [TcKind] -> [TcKind] -> TcM ()
-unifyKinds [] [] = returnTc ()
-unifyKinds (k1:ks1) (k2:ks2) = unifyKind k1 k2 `thenTc_`
- unifyKinds ks1 ks2
-unifyKinds _ _ = panic "unifyKinds: length mis-match"
+
+{- 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}
+----------------------
+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
+ 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 actual_ty expected_ty
\end{code}
+
+--------------------------------
+-- withBoxes: the key utility function
+--------------------------------
+
\begin{code}
-unifyOpenTypeKind :: TcKind -> TcM ()
--- Ensures that the argument kind is of the form (Type bx)
--- for some boxity bx
-
-unifyOpenTypeKind ty@(TyVarTy tyvar)
- = tcGetTyVar tyvar `thenNF_Tc` \ maybe_ty ->
- case maybe_ty of
- Just ty' -> unifyOpenTypeKind ty'
- other -> unify_open_kind_help ty
-
-unifyOpenTypeKind ty
- = case splitTyConApp_maybe ty of
- Just (tycon, [_]) | tycon == typeCon -> returnTc ()
- other -> unify_open_kind_help ty
-
-unify_open_kind_help ty -- Revert to ordinary unification
- = newBoxityVar `thenNF_Tc` \ boxity ->
- unifyKind ty (mkTyConApp typeCon [boxity])
+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}
%************************************************************************
%* *
-\subsection[Unify-exported]{Exported unification functions}
+ Approximate boxy matching
%* *
%************************************************************************
-The exported functions are all defined as versions of some
-non-exported generic functions.
+\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}
-Unify two @TauType@s. Dead straightforward.
+
+%************************************************************************
+%* *
+ Subsumption checking
+%* *
+%************************************************************************
+
+All the tcSub calls have the form
+
+ tcSub expected_ty offered_ty
+which checks
+ offered_ty <= expected_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.
\begin{code}
-unifyTauTy :: TcTauType -> TcTauType -> TcM ()
-unifyTauTy ty1 ty2 -- ty1 expected, ty2 inferred
- = tcAddErrCtxtM (unifyCtxt "type" ty1 ty2) $
- uTys ty1 ty1 ty2 ty2
+-----------------
+tcSubExp :: BoxySigmaType -> BoxySigmaType -> TcM ExprCoFn -- Locally used only
+ -- (tcSub act exp) checks that
+ -- act <= exp
+tcSubExp actual_ty expected_ty
+ = traceTc (text "tcSub" <+> details) `thenM_`
+ addErrCtxtM (unifyCtxt "type" actual_ty expected_ty)
+ (tc_sub actual_ty actual_ty expected_ty expected_ty)
+ where
+ details = vcat [text "Expected:" <+> ppr expected_ty,
+ text "Actual: " <+> ppr actual_ty]
+
+-----------------
+tc_sub :: BoxySigmaType -- actual_ty, before expanding synonyms
+ -> BoxySigmaType -- ..and after
+ -> BoxySigmaType -- expected_ty, before
+ -> BoxySigmaType -- ..and after
+ -> TcM ExprCoFn
+
+tc_sub act_sty act_ty exp_sty exp_ty
+ | Just exp_ty' <- tcView exp_ty = tc_sub act_sty act_ty exp_sty exp_ty'
+tc_sub act_sty act_ty exp_sty exp_ty
+ | Just act_ty' <- tcView act_ty = tc_sub 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 act_sty (TyVarTy tv) exp_sty exp_ty
+ = do { uVar False tv False exp_sty exp_ty
+ ; return idCoercion }
+
+-----------------------------------
+-- 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
+
+-- 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 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 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 (rule ASPEC):
+-- actual_ty: forall a. Ord a => a->a
+-- expected_ty: Int -> Int
+-- co_fn e = e Int dOrdInt
+
+tc_sub act_sty actual_ty exp_sty expected_ty
+ | isSigmaTy actual_ty
+ = 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 tau tau exp_sty expected_ty
+ ; return (co_fn <.> inst_fn) }
+
+-----------------------------------
+-- 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 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 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 act_sty actual_ty exp_sty expected_ty
+ = do { u_tys False act_sty actual_ty False exp_sty expected_ty
+ ; return idCoercion }
+
+
+-----------------------------------
+tc_sub_funs act_arg act_res exp_arg exp_res
+ = do { uTys False act_arg False exp_arg
+ ; co_fn_res <- tc_sub act_res act_res exp_res exp_res
+ ; wrapFunResCoercion [exp_arg] co_fn_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}
-@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.
+
+
+%************************************************************************
+%* *
+\subsection{Generalisation}
+%* *
+%************************************************************************
+
+\begin{code}
+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 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
+ ; (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
+ -- 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.
+
+ ; dicts <- newDicts (SigOrigin skol_info) theta
+ ; inst_binds <- tcSimplifyCheck sig_msg forall_tvs dicts lie
+
+ ; checkSigTyVarsWrt free_tvs forall_tvs
+ ; traceTc (text "tcGen:done")
+
+ ; 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 = CoTyLams forall_tvs $ CoLams dict_ids $ CoLet inst_binds CoHole
+ ; returnM (co_fn, result) }
+ where
+ free_tvs = tyVarsOfType expected_ty `unionVarSet` extra_tvs
+ sig_msg = ptext SLIT("expected type of an expression")
+\end{code}
+
+
+
+%************************************************************************
+%* *
+ Boxy unification
+%* *
+%************************************************************************
+
+The exported functions are all defined as versions of some
+non-exported generic functions.
\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 "type" ty1 ty2) $
+ uTys 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 "type" ty1 ty2) $
+ uTys True ty1 True ty2
+
+---------------
+unifyPred :: PredType -> PredType -> TcM ()
+-- Acutal and expected types
+unifyPred p1 p2 = addErrCtxtM (unifyCtxt "type constraint" (mkPredTy p1) (mkPredTy p2)) $
+ uPred 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
+type NoBoxes = Bool -- True <=> definitely no boxes in this type
+ -- False <=> there might be boxes (always safe)
- -> TcTauType -> TcTauType -- Error reporting ty2 and real ty2
- -- ty2 is the *actual* type
+uTys :: NoBoxes -> TcType -- ty1 is the *expected* type
+ -> NoBoxes -> TcType -- ty2 is the *actual* type
-> TcM ()
+uTys nb1 ty1 nb2 ty2 = u_tys 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 :: NoBoxes -> TcType -> TcType -- ty1 is the *actual* type
+ -> NoBoxes -> TcType -> TcType -- ty2 is the *expected* type
+ -> TcM ()
+
+u_tys nb1 orig_ty1 ty1 nb2 orig_ty2 ty2
+ = go ty1 ty2
+ where
-- Always expand synonyms (see notes at end)
- -- (this also throws away FTVs and usage annots)
-uTys ps_ty1 (NoteTy _ ty1) ps_ty2 ty2 = uTys ps_ty1 ty1 ps_ty2 ty2
-uTys ps_ty1 ty1 ps_ty2 (NoteTy _ ty2) = uTys ps_ty1 ty1 ps_ty2 ty2
+ -- (this also throws away FTVs)
+ go ty1 ty2
+ | Just ty1' <- tcView ty1 = go ty1' ty2
+ | Just ty2' <- tcView ty2 = go 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 (TyVarTy tyvar1) ty2 = uVar False tyvar1 nb2 orig_ty2 ty2
+ go ty1 (TyVarTy tyvar2) = uVar True tyvar2 nb1 orig_ty1 ty1
+ -- "True" means args swapped
-- Predicates
-uTys _ (PredTy (IParam n1 t1)) _ (PredTy (IParam n2 t2))
- | n1 == n2 = uTys t1 t1 t2 t2
-uTys _ (PredTy (Class c1 tys1)) _ (PredTy (Class c2 tys2))
- | c1 == c2 = 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 (PredTy p1) (PredTy p2) = uPred nb1 p1 nb2 p2
-- Type constructors must match
-uTys ps_ty1 (TyConApp con1 tys1) ps_ty2 (TyConApp con2 tys2)
- | con1 == con2 && length tys1 == length 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 splitAppTy_maybe ty2 of
- Just (s2,t2) -> uTys s1 s1 s2 s2 `thenTc_` uTys t1 t1 t2 t2
- Nothing -> unifyMisMatch ps_ty1 ps_ty2
+ go (AppTy s1 t1) ty2
+ = case tcSplitAppTy_maybe ty2 of
+ Just (s2,t2) -> do { uTys nb1 s1 nb2 s2; uTys nb1 t1 nb2 t2 }
+ Nothing -> unifyMisMatch False orig_ty1 orig_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 splitAppTy_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 ty1 (AppTy s2 t2)
+ = case tcSplitAppTy_maybe ty1 of
+ Just (s1,t1) -> do { uTys nb1 s1 nb2 s2; uTys nb1 t1 nb2 t2 }
+ Nothing -> unifyMisMatch False orig_ty1 orig_ty2
+
+ 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 _ _ = unifyMisMatch False orig_ty1 orig_ty2
+
+----------
+uPred nb1 (IParam n1 t1) nb2 (IParam n2 t2)
+ | n1 == n2 = uTys nb1 t1 nb2 t2
+uPred nb1 (ClassP c1 tys1) nb2 (ClassP c2 tys2)
+ | c1 == c2 = uTys_s nb1 tys1 nb2 tys2 -- Guaranteed equal lengths because the kinds check
+uPred _ p1 _ p2 = unifyMisMatch 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
~~~~~~~~~~~~~~~~~
If you are tempted to make a short cut on synonyms, as in this
pseudocode...
\begin{verbatim}
-uTys (SynTy con1 args1 ty1) (SynTy con2 args2 ty2)
- = if (con1 == con2) then
- -- Good news! Same synonym constructors, so we can shortcut
- -- by unifying their arguments and ignoring their expansions.
- unifyTauTypeLists args1 args2
- else
- -- Never mind. Just expand them and try again
- uTys ty1 ty2
+-- 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 unifyTypepeLists args1 args2
+-- NO else
+-- NO -- Never mind. Just expand them and try again
+-- NO uTys ty1 ty2
\end{verbatim}
then THINK AGAIN. Here is the whole story, as detected and reported
uVar :: 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
- = tcGetTyVar 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; ignore usage annots
-uUnboundVar swapped tv1 maybe_ty1 ps_ty2 (NoteTy _ 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 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 nb2 ps_ty2 ty2 True ty1 ty1 -- Swap back
+ | otherwise -> u_tys True ty1 ty1 nb2 ps_ty2 ty2 -- Same order
+ -- The 'True' here says that ty1
+ -- is definitely box-free
+ DoneTv details1 -> uUnfilledVar swapped tv1 details1 nb2 ps_ty2 ty2
+ }
+
+----------------
+uUnfilledVar :: Bool -- Args are swapped
+ -> TcTyVar -> TcTyVarDetails -- Tyvar 1
+ -> NoBoxes -> TcTauType -> TcTauType -- Type 2
+ -> TcM ()
+-- Invariant: tyvar 1 is not unified with anything
+
+uUnfilledVar swapped tv1 details1 nb2 ps_ty2 ty2
+ | Just ty2' <- tcView ty2
+ = -- Expand synonyms; ignore FTVs
+ uUnfilledVar swapped tv1 details1 nb2 ps_ty2 ty2'
+
+uUnfilledVar 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
- = tcGetTyVar tv2 `thenNF_Tc` \ maybe_ty2 ->
- case maybe_ty2 of
- Just ty2' -> uUnboundVar swapped tv1 maybe_ty1 ty2' ty2'
-
- Nothing | tv1_dominates_tv2
-
- -> WARN( not (k1 `hasMoreBoxityInfo` k2), (ppr tv1 <+> ppr k1) $$ (ppr tv2 <+> ppr k2) )
- tcPutTyVar tv2 (TyVarTy tv1) `thenNF_Tc_`
- returnTc ()
- | otherwise
-
- -> WARN( not (k2 `hasMoreBoxityInfo` k1), (ppr tv2 <+> ppr k2) $$ (ppr tv1 <+> ppr k1) )
- (ASSERT( isNotUsgTy ps_ty2 )
- tcPutTyVar tv1 ps_ty2 `thenNF_Tc_`
- returnTc ())
+ = do { lookup2 <- lookupTcTyVar tv2
+ ; case lookup2 of
+ IndirectTv ty2' -> uUnfilledVar swapped tv1 details1 True ty2' ty2'
+ DoneTv details2 -> uUnfilledVars swapped tv1 details1 tv2 details2
+ }
+
+uUnfilledVar 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
- k1 = tyVarKind tv1
- k2 = tyVarKind tv2
- tv1_dominates_tv2 = isSigTyVar tv1
- -- Don't unify a signature type variable if poss
- || k2 == openTypeKind
- -- Try to get rid of open type variables as soon as poss
- || varName tv1 `hasBetterProv` 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
- = checkKinds swapped tv1 non_var_ty2 `thenTc_`
- occur_check non_var_ty2 `thenTc_`
- ASSERT( isNotUsgTy ps_ty2 )
- checkTcM (not (isSigTyVar tv1))
- (failWithTcM (unifyWithSigErr tv1 ps_ty2)) `thenTc_`
-
- warnTc (not (typeKind non_var_ty2 `hasMoreBoxityInfo` tyVarKind tv1))
- ((ppr tv1 <+> ppr (tyVarKind tv1)) $$
- (ppr non_var_ty2 <+> ppr (typeKind non_var_ty2))) `thenNF_Tc_`
-
- tcPutTyVar tv1 non_var_ty2 `thenNF_Tc_`
- -- This used to say "ps_ty2" instead of "non_var_ty2"
-
- -- But that led to an infinite loop in the type checker!
- -- Consider
- -- type A a = ()
- --
- -- f :: (A a -> a -> ()) -> ()
- -- f = \ _ -> ()
- --
- -- x :: ()
- -- x = f (\ x p -> p x)
- --
- -- Here, we try to match "t" with "A t", and succeed
- -- because the unifier looks through synonyms. The occurs
- -- check doesn't kick in because we are "really" binding "t" to "()",
- -- but we *actually* bind "t" to "A t" if we store ps_ty2.
- -- That leads the typechecker into an infinite loop later.
-
- returnTc ()
+ mis_match = unifyMisMatch 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 :: 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 swapped tv1 (SkolemTv _) tv2 (SkolemTv _)
+ = unifyMisMatch swapped (mkTyVarTy tv1) (mkTyVarTy tv2)
+
+uUnfilledVars swapped tv1 (MetaTv info1 ref1) tv2 (SkolemTv _)
+ = checkUpdateMeta swapped tv1 ref1 (mkTyVarTy tv2)
+uUnfilledVars 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 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
- occur_check ty = mapTc occur_check_tv (varSetElems (tyVarsOfType ty)) `thenTc_`
- returnTc ()
+ -- Kinds should be guaranteed ok at this point
+ update_tv1 = updateMeta tv1 ref1 (mkTyVarTy tv2)
+ update_tv2 = updateMeta tv2 ref2 (mkTyVarTy tv1)
+
+ box_meets_box | k1_sub_k2 = fill_with k1
+ | k2_sub_k1 = fill_with k2
+ | otherwise = kind_err
- occur_check_tv tv2
- | tv1 == tv2 -- Same tyvar; fail
- = zonkTcType ps_ty2 `thenNF_Tc` \ zonked_ty2 ->
- failWithTcM (unifyOccurCheck tv1 zonked_ty2)
+ fill_with kind = do { tau_ty <- newFlexiTyVarTy kind
+ ; updateMeta tv1 ref1 tau_ty
+ ; updateMeta tv2 ref2 tau_ty }
- | otherwise -- A different tyvar
- = tcGetTyVar tv2 `thenNF_Tc` \ maybe_ty2 ->
- case maybe_ty2 of
- Just ty2' -> occur_check ty2'
- other -> returnTc ()
+ kind_err = addErrCtxtM (unifyKindCtxt swapped tv1 (mkTyVarTy tv2)) $
+ unifyKindMisMatch k1 k2
+ k1 = tyVarKind tv1
+ k2 = tyVarKind tv2
+ 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.
--- We need to check that we don't unify a boxed type variable with an
--- unboxed type: e.g. (id 3#) is illegal
- | tk1 == boxedTypeKind && tk2 == unboxedTypeKind
- = tcAddErrCtxtM (unifyKindCtxt swapped tv1 ty2) $
- unifyMisMatch k1 k2
+-- 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
- = returnTc ()
+ -- 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
+ = 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 (fromJust (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
+
+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).
+
+\begin{code}
+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
+--
+-- 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-fun]{@unifyFunTy@}
+ Kind unification
%* *
%************************************************************************
-@unifyFunTy@ is used to avoid the fruitless creation of type variables.
+Unifying kinds is much, much simpler than unifying types.
\begin{code}
-unifyFunTy :: TcType -- Fail if ty isn't a function type
- -> TcM (TcType, TcType) -- otherwise return arg and result types
-
-unifyFunTy ty@(TyVarTy tyvar)
- = tcGetTyVar tyvar `thenNF_Tc` \ maybe_ty ->
- case maybe_ty of
- Just ty' -> unifyFunTy ty'
- other -> unify_fun_ty_help ty
-
-unifyFunTy ty
- = case splitFunTy_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}
+unifyKind :: TcKind -- Expected
+ -> TcKind -- Actual
+ -> TcM ()
+unifyKind LiftedTypeKind LiftedTypeKind = returnM ()
+unifyKind UnliftedTypeKind UnliftedTypeKind = returnM ()
-\begin{code}
-unifyListTy :: TcType -- expected list type
- -> TcM TcType -- list element type
-
-unifyListTy ty@(TyVarTy tyvar)
- = tcGetTyVar tyvar `thenNF_Tc` \ maybe_ty ->
- case maybe_ty of
- Just ty' -> unifyListTy ty'
- other -> unify_list_ty_help ty
-
-unifyListTy ty
- = case splitTyConApp_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 boxedTypeKind `thenNF_Tc` \ elt_ty ->
- unifyTauTy ty (mkListTy elt_ty) `thenTc_`
- returnTc elt_ty
-\end{code}
+unifyKind OpenTypeKind k2 | isOpenTypeKind k2 = returnM ()
+unifyKind ArgTypeKind k2 | isArgTypeKind k2 = returnM ()
+ -- Respect sub-kinding
-\begin{code}
-unifyTupleTy :: Boxity -> Arity -> TcType -> TcM [TcType]
-unifyTupleTy boxity arity ty@(TyVarTy tyvar)
- = tcGetTyVar 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 splitTyConApp_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
+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 [] [] = returnM ()
+unifyKinds (k1:ks1) (k2:ks2) = unifyKind k1 k2 `thenM_`
+ unifyKinds ks1 ks2
+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
- kind | isBoxed boxity = boxedTypeKind
- | otherwise = openTypeKind
+ 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}
+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}
%************************************************************************
%* *
~~~~~~
\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')
+unifyCtxt s ty1 ty2 tidy_env -- ty1 inferred, ty2 expected
+ = zonkTcType ty1 `thenM` \ ty1' ->
+ zonkTcType ty2 `thenM` \ ty2' ->
+ returnM (err ty1' ty2')
where
err ty1 ty2 = (env1,
- nest 4
+ nest 2
(vcat [
- text "Expected" <+> text s <> colon <+> ppr tidy_ty1,
- text "Inferred" <+> text s <> colon <+> ppr tidy_ty2
+ text "Expected" <+> text s <> colon <+> ppr tidy_ty2,
+ text "Inferred" <+> text s <> colon <+> ppr tidy_ty1
]))
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')
+ -- tv1 and ty2 are zonked already
+ = returnM msg
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') = tidyTyVar 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)))
+ 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 swapped ty1 ty2
+ = do { (env, msg) <- if swapped then misMatchMsg ty2 ty1
+ else misMatchMsg ty1 ty2
+ ; 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") <+> pp1,
+ nest 7 (ptext SLIT("against") <+> 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 = ptext SLIT("the rigid variable") <+> quotes (ppr tv)
+
+
+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
- (env1, tidy_tyvar) = tidyTyVar emptyTidyEnv tyvar
- (env2, tidy_ty) = tidyOpenType env1 ty
+ msg = ptext SLIT("Occurs check: cannot construct the infinite type:")
+\end{code}
+
+
+%************************************************************************
+%* *
+ Checking kinds
+%* *
+%************************************************************************
+
+---------------------------
+-- 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}
+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}
-unifyOccurCheck tyvar ty
- = (env2, hang (ptext SLIT("Occurs check: cannot construct the infinite type:"))
- 4 (sep [ppr tidy_tyvar, char '=', ppr tidy_ty]))
+%************************************************************************
+%* *
+\subsection{Checking signature type variables}
+%* *
+%************************************************************************
+
+@checkSigTyVars@ checks that a set of universally quantified type varaibles
+are not mentioned in the environment. In particular:
+
+ (a) Not mentioned in the type of a variable in the envt
+ eg the signature for f in this:
+
+ g x = ... where
+ f :: a->[a]
+ f y = [x,y]
+
+ Here, f is forced to be monorphic by the free occurence of x.
+
+ (d) Not (unified with another type variable that is) in scope.
+ eg f x :: (r->r) = (\y->y) :: forall a. a->r
+ when checking the expression type signature, we find that
+ even though there is nothing in scope whose type mentions r,
+ nevertheless the type signature for the expression isn't right.
+
+ Another example is in a class or instance declaration:
+ class C a where
+ op :: forall b. a -> b
+ op x = x
+ Here, b gets unified with a
+
+Before doing this, the substitution is applied to the signature type variable.
+
+\begin{code}
+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
+ main_msg = ptext SLIT("Inferred type is less polymorphic than expected")
+
+ 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) }
+
+-----------------------
+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
- (env1, tidy_tyvar) = tidyTyVar emptyTidyEnv tyvar
- (env2, tidy_ty) = tidyOpenType env1 ty
+ 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 :: 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_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
+ returnM (env3, msg)
+\end{code}