\begin{code}
module TcUnify (
-- Full-blown subsumption
- tcSubOff, tcSubExp, tcGen,
- checkSigTyVars, checkSigTyVarsWrt, sigCtxt, findGlobals,
+ tcSubExp, tcGen,
+ checkSigTyVars, checkSigTyVarsWrt, bleatEscapedTvs, sigCtxt,
-- Various unifications
- unifyTauTy, unifyTauTyList, unifyTauTyLists,
- unifyKind, unifyKinds, unifyOpenTypeKind, unifyFunKind,
+ unifyType, unifyTypeList, unifyTheta,
+ unifyKind, unifyKinds, unifyFunKind,
+ checkExpectedKind,
+ boxySubMatchType, boxyMatchTypes,
--------------------------------
-- Holes
- Expected(..), newHole, readExpectedType,
- zapExpectedType, zapExpectedTo, zapExpectedBranches,
- subFunTys, unifyFunTy,
- zapToListTy, unifyListTy,
- zapToPArrTy, unifyPArrTy,
- zapToTupleTy, unifyTupleTy
-
+ 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 ( mkHsLet,
- ExprCoFn, idCoercion, isIdCoercion, mkCoercion, (<.>), (<$>) )
-import TypeRep ( Type(..), SourceType(..), TyNote(..), openKindCon )
-
-import TcRnMonad -- TcType, amongst others
-import TcType ( TcKind, TcType, TcSigmaType, TcRhoType, TcTyVar, TcTauType,
- TcTyVarSet, TcThetaType, TyVarDetails(SigTv),
- isTauTy, isSigmaTy, mkFunTys,
- tcSplitAppTy_maybe, tcSplitTyConApp_maybe,
- tcGetTyVar_maybe, tcGetTyVar,
- mkFunTy, tyVarsOfType, mkPhiTy,
- typeKind, tcSplitFunTy_maybe, mkForAllTys,
- isSkolemTyVar, isUserTyVar,
- tidyOpenType, tidyOpenTypes, tidyOpenTyVar, tidyOpenTyVars,
- eqKind, openTypeKind, liftedTypeKind, isTypeKind, mkArrowKind,
- hasMoreBoxityInfo, allDistinctTyVars
- )
-import Inst ( newDicts, instToId, tcInstCall )
-import TcMType ( getTcTyVar, putTcTyVar, tcInstType, newKindVar,
- newTyVarTy, newTyVarTys, newOpenTypeKind,
- zonkTcType, zonkTcTyVars, zonkTcTyVarsAndFV )
+import TcMType ( lookupTcTyVar, LookupTyVarResult(..),
+ tcInstSkolType, newKindVar, newMetaTyVar,
+ tcInstBoxy, newBoxyTyVar, readFilledBox,
+ readMetaTyVar, writeMetaTyVar, newFlexiTyVarTy,
+ tcInstSkolTyVars,
+ zonkTcKind, zonkType, zonkTcType, zonkTcTyVarsAndFV,
+ readKindVar, writeKindVar )
import TcSimplify ( tcSimplifyCheck )
-import TysWiredIn ( listTyCon, parrTyCon, mkListTy, mkPArrTy, mkTupleTy )
import TcEnv ( tcGetGlobalTyVars, findGlobals )
-import TyCon ( tyConArity, isTupleTyCon, tupleTyConBoxity )
-import PprType ( pprType )
+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 )
-import VarSet ( emptyVarSet, unitVarSet, unionVarSet, elemVarSet, varSetElems )
+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 BasicTypes ( Boxity, Arity, isBoxed )
-import Util ( equalLength, lengthExceeds, notNull )
+import Maybes ( fromJust )
+import BasicTypes ( Arity )
+import UniqSupply ( uniqsFromSupply )
+import Util ( notNull, equalLength )
import Outputable
-\end{code}
-Notes on holes
-~~~~~~~~~~~~~~
-* A hole is always filled in with an ordinary type, not another hole.
+-- Assertion imports
+#ifdef DEBUG
+import TcType ( isBoxyTy, isFlexi )
+#endif
+\end{code}
%************************************************************************
%* *
%************************************************************************
\begin{code}
-data Expected ty = Infer (TcRef ty) -- The hole to fill in for type inference
- | Check ty -- The type to check during type checking
-
-newHole :: TcM (TcRef ty)
-newHole = newMutVar (error "Empty hole in typechecker")
-
-readExpectedType :: Expected ty -> TcM ty
-readExpectedType (Infer hole) = readMutVar hole
-readExpectedType (Check ty) = returnM ty
-
-zapExpectedType :: Expected TcType -> TcM TcTauType
--- In the inference case, ensure we have a monotype
-zapExpectedType (Infer hole)
- = do { ty <- newTyVarTy openTypeKind ;
- writeMutVar hole ty ;
- return ty }
-
-zapExpectedType (Check ty) = return ty
-
-zapExpectedTo :: Expected TcType -> TcTauType -> TcM ()
-zapExpectedTo (Infer hole) ty2 = writeMutVar hole ty2
-zapExpectedTo (Check ty1) ty2 = unifyTauTy ty1 ty2
-
-zapExpectedBranches :: [a] -> Expected TcType -> TcM (Expected TcType)
--- Zap the expected type to a monotype if there is more than one branch
-zapExpectedBranches branches exp_ty
- | lengthExceeds branches 1 = zapExpectedType exp_ty `thenM` \ exp_ty' ->
- return (Check exp_ty')
- | otherwise = returnM exp_ty
-
-instance Outputable ty => Outputable (Expected ty) where
- ppr (Check ty) = ptext SLIT("Expected type") <+> ppr ty
- ppr (Infer hole) = ptext SLIT("Inferring type")
+tcInfer :: (BoxyType -> TcM a) -> TcM (a, TcType)
+tcInfer tc_infer
+ = do { box <- newBoxyTyVar
+ ; res <- tc_infer (mkTyVarTy box)
+ ; res_ty <- readFilledBox box -- Guaranteed filled-in by now
+ ; return (res, res_ty) }
\end{code}
%************************************************************************
%* *
-\subsection[Unify-fun]{@unifyFunTy@}
+ subFunTys
%* *
%************************************************************************
-@subFunTy@ and @unifyFunTy@ is used to avoid the fruitless
-creation of type variables.
+\begin{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
+
-* subFunTy is used when we might be faced with a "hole" type variable,
- in which case we should create two new holes.
+{- Error messages from subFunTys
-* unifyFunTy is used when we expect to encounter only "ordinary"
- type variables, so we should create new ordinary type variables
+ The abstraction `\Just 1 -> ...' has two arguments
+ but its type `Maybe a -> a' has only one
-\begin{code}
-subFunTys :: [pat]
- -> Expected TcRhoType -- Fail if ty isn't a function type
- -> ([(pat, Expected TcRhoType)] -> Expected TcRhoType -> TcM a)
- -> TcM a
+ The equation(s) for `f' have two arguments
+ but its type `Maybe a -> a' has only one
-subFunTys pats (Infer hole) thing_inside
- = -- This is the interesting case
- mapM new_pat_hole pats `thenM` \ pats_w_holes ->
- newHole `thenM` \ res_hole ->
+ The section `(f 3)' requires 'f' to take two arguments
+ but its type `Int -> Int' has only one
- -- Do the business
- thing_inside pats_w_holes (Infer res_hole) `thenM` \ answer ->
+ The function 'f' is applied to two arguments
+ but its type `Int -> Int' has only one
+-}
- -- Extract the answers
- mapM read_pat_hole pats_w_holes `thenM` \ arg_tys ->
- readMutVar res_hole `thenM` \ res_ty ->
- -- Write the answer into the incoming hole
- writeMutVar hole (mkFunTys arg_tys res_ty) `thenM_`
+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 first, 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) }
+
+ 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
+ = failWithTc (mk_msg (length args_so_far))
+
+ mk_msg 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}
- -- And return the answer
- returnM answer
+\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
- new_pat_hole pat = newHole `thenM` \ hole -> return (pat, Infer hole)
- read_pat_hole (pat, Infer hole) = readMutVar hole
+ 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 }
-subFunTys pats (Check ty) thing_inside
- = go pats ty `thenM` \ (pats_w_tys, res_ty) ->
- thing_inside pats_w_tys res_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
- go [] ty = return ([], Check ty)
- go (pat:pats) ty = unifyFunTy ty `thenM` \ (arg,res) ->
- go pats res `thenM` \ (pats_w_tys, final_res) ->
- return ((pat, Check arg) : pats_w_tys, final_res)
-
-unifyFunTy :: TcRhoType -- Fail if ty isn't a function type
- -> TcM (TcType, TcType) -- otherwise return arg and result types
-
-unifyFunTy ty@(TyVarTy tyvar)
- = getTcTyVar tyvar `thenM` \ 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 -> returnM arg_and_res
- Nothing -> unify_fun_ty_help ty
-
-unify_fun_ty_help ty -- Special cases failed, so revert to ordinary unification
- = newTyVarTy openTypeKind `thenM` \ arg ->
- newTyVarTy openTypeKind `thenM` \ res ->
- unifyTauTy ty (mkFunTy arg res) `thenM_`
- returnM (arg,res)
+ 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}
-zapToListTy :: Expected TcType -- expected list type
- -> TcM TcType -- list element type
-
-zapToListTy (Check ty) = unifyListTy ty
-zapToListTy (Infer hole) = do { elt_ty <- newTyVarTy liftedTypeKind ;
- writeMutVar hole (mkListTy elt_ty) ;
- return elt_ty }
-
-unifyListTy :: TcType -> TcM TcType
-unifyListTy ty@(TyVarTy tyvar)
- = getTcTyVar tyvar `thenM` \ 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 -> returnM arg_ty
- other -> unify_list_ty_help ty
-
-unify_list_ty_help ty -- Revert to ordinary unification
- = newTyVarTy liftedTypeKind `thenM` \ elt_ty ->
- unifyTauTy ty (mkListTy elt_ty) `thenM_`
- returnM elt_ty
-
--- variant for parallel arrays
---
-zapToPArrTy :: Expected TcType -- Expected list type
- -> TcM TcType -- List element type
-
-zapToPArrTy (Check ty) = unifyPArrTy ty
-zapToPArrTy (Infer hole) = do { elt_ty <- newTyVarTy liftedTypeKind ;
- writeMutVar hole (mkPArrTy elt_ty) ;
- return elt_ty }
-
-unifyPArrTy :: TcType -> TcM TcType
-
-unifyPArrTy ty@(TyVarTy tyvar)
- = getTcTyVar tyvar `thenM` \ 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 -> returnM arg_ty
- _ -> unify_parr_ty_help ty
-
-unify_parr_ty_help ty -- Revert to ordinary unification
- = newTyVarTy liftedTypeKind `thenM` \ elt_ty ->
- unifyTauTy ty (mkPArrTy elt_ty) `thenM_`
- returnM elt_ty
+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}
+
+%************************************************************************
+%* *
+ Approximate boxy matching
+%* *
+%************************************************************************
+
\begin{code}
-zapToTupleTy :: Boxity -> Arity -> Expected TcType -> TcM [TcType]
-zapToTupleTy boxity arity (Check ty) = unifyTupleTy boxity arity ty
-zapToTupleTy boxity arity (Infer hole) = do { (tup_ty, arg_tys) <- new_tuple_ty boxity arity ;
- writeMutVar hole tup_ty ;
- return arg_tys }
-
-unifyTupleTy boxity arity ty@(TyVarTy tyvar)
- = getTcTyVar tyvar `thenM` \ 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
- -> returnM arg_tys
- other -> unify_tuple_ty_help boxity arity ty
-
-unify_tuple_ty_help boxity arity ty
- = new_tuple_ty boxity arity `thenM` \ (tup_ty, arg_tys) ->
- unifyTauTy ty tup_ty `thenM_`
- returnM arg_tys
-
-new_tuple_ty boxity arity
- = newTyVarTys arity kind `thenM` \ arg_tys ->
- return (mkTupleTy boxity arity arg_tys, arg_tys)
+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
- kind | isBoxed boxity = liftedTypeKind
- | otherwise = openTypeKind
+ 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) = AppTy (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}
%************************************************************************
%* *
-\subsection{Subsumption}
+ Subsumption checking
%* *
%************************************************************************
expected_ty.
\begin{code}
-tcSubExp :: Expected TcRhoType -> TcRhoType -> TcM ExprCoFn
-tcSubOff :: TcSigmaType -> Expected TcSigmaType -> TcM ExprCoFn
-\end{code}
-
-These two check for holes
-
-\begin{code}
-tcSubExp expected_ty offered_ty
- = traceTc (text "tcSubExp" <+> (ppr expected_ty $$ ppr offered_ty)) `thenM_`
- checkHole expected_ty offered_ty tcSub
-
-tcSubOff expected_ty offered_ty
- = checkHole offered_ty expected_ty (\ off exp -> tcSub exp off)
-
--- checkHole looks for a hole in its first arg;
--- If so, and it is uninstantiated, it fills in the hole
--- with its second arg
--- Otherwise it calls thing_inside, passing the two args, looking
--- through any instantiated hole
-
-checkHole (Infer hole) other_ty thing_inside
- = do { writeMutVar hole other_ty; return idCoercion }
-
-checkHole (Check ty) other_ty thing_inside
- = thing_inside ty other_ty
-\end{code}
-
-No holes expected now. Add some error-check context info.
-
-\begin{code}
-tcSub :: TcSigmaType -> TcSigmaType -> TcM ExprCoFn -- Locally used only
-tcSub expected_ty actual_ty
+-----------------
+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" expected_ty actual_ty)
- (tc_sub expected_ty expected_ty actual_ty actual_ty)
+ 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]
-\end{code}
-tc_sub carries the types before and after expanding type synonyms
-
-\begin{code}
-tc_sub :: TcSigmaType -- expected_ty, before expanding synonyms
- -> TcSigmaType -- ..and after
- -> TcSigmaType -- actual_ty, before
- -> TcSigmaType -- ..and after
+-----------------
+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
+
-----------------------------------
--- 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
+-- 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 }
-----------------------------------
--- 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 (tyVarsOfType actual_ty) (
- -- It's really important to check for escape wrt the free vars of
- -- both expected_ty *and* actual_ty
- \ body_exp_ty -> tc_sub body_exp_ty body_exp_ty act_sty actual_ty
- ) `thenM` \ (gen_fn, co_fn) ->
- returnM (gen_fn <.> co_fn)
+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:
+-- 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 act_sty actual_ty exp_sty expected_ty
| isSigmaTy actual_ty
- = tcInstCall Rank2Origin actual_ty `thenM` \ (inst_fn, body_ty) ->
- tc_sub exp_sty expected_ty body_ty body_ty `thenM` \ co_fn ->
- returnM (co_fn <.> inst_fn)
+ = 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
+-- 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 _ (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, because we can instantiat f's type to a monotype
---
--- However, we get can get jolly unhelpful error messages.
--- e.g. foo = id runST
---
--- Inferred type is less polymorphic than expected
--- Quantified type variable `s' escapes
--- Expected type: ST s a -> t
--- Inferred type: (forall s1. ST s1 a) -> a
--- In the first argument of `id', namely `runST'
--- In a right-hand side of function `foo': id runST
---
--- I'm not quite sure what to do about this!
-
-tc_sub exp_sty exp_ty@(FunTy exp_arg exp_res) _ (TyVarTy tv)
- = getTcTyVar tv `thenM` \ maybe_ty ->
- case maybe_ty of
- Just ty -> tc_sub exp_sty exp_ty ty ty
- Nothing -> imitateFun tv exp_sty `thenM` \ (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 `thenM` \ maybe_ty ->
- case maybe_ty of
- Just ty -> tc_sub ty ty act_sty act_ty
- Nothing -> imitateFun tv act_sty `thenM` \ (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 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 `thenM_`
- returnM idCoercion
-\end{code}
-
-%************************************************************************
-%* *
-\subsection{Functions}
-%* *
-%************************************************************************
-
-\begin{code}
-tcSub_fun exp_arg exp_res act_arg act_res
- = tc_sub act_arg act_arg exp_arg exp_arg `thenM` \ co_fn_arg ->
- tc_sub exp_res exp_res act_res act_res `thenM` \ co_fn_res ->
- newUnique `thenM` \ 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 FSLIT("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
- returnM coercion
-
-imitateFun :: TcTyVar -> TcType -> TcM (TcType, TcType)
-imitateFun tv ty
- = -- 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.)
- checkM (not (isSkolemTyVar tv))
- (failWithTcM (unifyWithSigErr tv ty)) `thenM_`
-
- newTyVarTy openTypeKind `thenM` \ arg ->
- newTyVarTy openTypeKind `thenM` \ res ->
- putTcTyVar tv (mkFunTy arg res) `thenM_`
- returnM (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
+tcGen :: BoxySigmaType -- expected_ty
-> TcTyVarSet -- Extra tyvars that the universally
-- quantified tyvars of expected_ty
-- must not be unified
- -> (TcRhoType -> TcM result) -- spec_ty
+ -> (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
- = tcInstType SigTv expected_ty `thenM` \ (forall_tvs, theta, phi_ty) ->
+ = 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
- getLIE (thing_inside phi_ty) `thenM` \ (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.
- newDicts SignatureOrigin theta `thenM` \ dicts ->
- tcSimplifyCheck sig_msg forall_tvs dicts lie `thenM` \ inst_binds ->
+ ; dicts <- newDicts (SigOrigin skol_info) theta
+ ; inst_binds <- tcSimplifyCheck sig_msg forall_tvs dicts lie
-#ifdef DEBUG
- zonkTcTyVars forall_tvs `thenM` \ forall_tys ->
- 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 phi_ty,
- text "free_tvs" <+> ppr free_tvs,
- text "forall_tys" <+> ppr forall_tys]) `thenM_`
-#endif
+ ; checkSigTyVarsWrt free_tvs forall_tvs
+ ; traceTc (text "tcGen:done")
- checkSigTyVarsWrt free_tvs forall_tvs `thenM` \ zonked_tvs ->
-
- traceTc (text "tcGen:done") `thenM_`
-
- 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
- returnM (mkCoercion co_fn, result)
+ 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")
%************************************************************************
%* *
-\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 )
+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 ty1 ty1 ty2 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@ 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 [] [] = returnM ()
-unifyTauTyLists (ty1:tys1) (ty2:tys2) = uTys ty1 ty1 ty2 ty2 `thenM_`
- unifyTauTyLists tys1 tys2
-unifyTauTyLists ty1s ty2s = panic "Unify.unifyTauTyLists: 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 [] = returnM ()
-unifyTauTyList [ty] = returnM ()
-unifyTauTyList (ty1:tys@(ty2:_)) = unifyTauTy ty1 ty2 `thenM_`
- 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)
-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 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 _ (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 `thenM_` 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 && 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 `thenM_` 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 tcSplitAppTy_maybe ty1 of
- Just (s1,t1) -> uTys s1 s1 s2 s2 `thenM_` 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
~~~~~~~~~~~~~~~~~
-- 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
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
- = traceTc (text "uVar" <+> ppr swapped <+> ppr tv1 <+> (ppr ps_ty2 $$ ppr ty2)) `thenM_`
- getTcTyVar tv1 `thenM` \ 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 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
= returnM ()
-- Distinct type variables
- -- ASSERT maybe_ty1 /= Just
| otherwise
- = getTcTyVar tv2 `thenM` \ 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 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
+ 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
+ -- 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) `thenM_`
- returnM ()
- | 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 `thenM_`
- returnM ()
- 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
- checkM (not (isSkolemTyVar tv1))
- (failWithTcM (unifyWithSigErr tv1 ps_ty2)) `thenM_`
-
- -- Do the occurs check, and check that we are not
- -- unifying a type variable with a polytype
- -- Returns a zonked type ready for the update
- checkValue tv1 ps_ty2 non_var_ty2 `thenM` \ ty2 ->
-
- -- Check that the kinds match
- checkKinds swapped tv1 ty2 `thenM_`
-
- -- Perform the update
- putTcTyVar tv1 ty2 `thenM_`
- returnM ()
-\end{code}
+ k1_sub_k2 = k1 `isSubKind` k2
+ k2_sub_k1 = k2 `isSubKind` k1
-\begin{code}
+ 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, which ensures that
-- its kind has as much boxity information visible as possible.
- | tk2 `hasMoreBoxityInfo` tk1 = returnM ()
+ | tk2 `isSubKind` tk1 = returnM ()
| otherwise
-- Either the kinds aren't compatible
-- or we are unifying a lifted type variable with an
-- unlifted type: e.g. (id 3#) is illegal
= addErrCtxtM (unifyKindCtxt swapped tv1 ty2) $
- unifyMisMatch k1 k2
-
+ 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}
-\begin{code}
-checkValue tv1 ps_ty2 non_var_ty2
--- Do the occurs check, and check that we are not
--- unifying a type variable with a polytype
--- Return the type to update the type variable with, or fail
+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
--- 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
--
--- But consider
--- type A a = ()
+-- 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
--
--- f :: (A a -> a -> ()) -> ()
--- f = \ _ -> ()
+-- Compare this wth checkTauTvUpdate
--
--- 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
- = zonkTcType ps_ty2 `thenM` \ ps_ty2' ->
- case okToUnifyWith tv1 ps_ty2' of {
- Nothing -> returnM ps_ty2' ; -- Success
- other ->
-
- zonkTcType non_var_ty2 `thenM` \ non_var_ty2' ->
- case okToUnifyWith tv1 non_var_ty2' of
- Nothing -> -- This branch rarely succeeds, except in strange cases
- -- like that in the example above
- returnM non_var_ty2'
-
- Just problem -> failWithTcM (unifyCheck problem tv1 ps_ty2')
- }
-
-data Problem = OccurCheck | NotMonoType
-
-okToUnifyWith :: TcTyVar -> TcType -> Maybe Problem
--- (okToUnifyWith tv ty) checks whether it's ok to unify
--- tv :=: ty
--- Nothing => ok
--- Just p => not ok, problem p
-
-okToUnifyWith tv ty
- = ok ty
- where
- ok (TyVarTy tv') | tv == tv' = Just OccurCheck
- | otherwise = Nothing
- ok (AppTy t1 t2) = ok t1 `and` ok t2
- ok (FunTy t1 t2) = ok t1 `and` ok t2
- ok (TyConApp _ ts) = oks ts
- ok (ForAllTy _ _) = Just NotMonoType
- ok (SourceTy st) = ok_st st
- ok (NoteTy (FTVNote _) t) = ok t
- ok (NoteTy (SynNote t1) t2) = ok t1 `and` ok t2
- -- Type variables may be free in t1 but not t2
- -- A forall may be in t2 but not t1
-
- oks ts = foldr (and . ok) Nothing ts
-
- ok_st (ClassP _ ts) = oks ts
- ok_st (IParam _ t) = ok t
- ok_st (NType _ ts) = oks ts
-
- Nothing `and` m = m
- Just p `and` m = Just p
+-- 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{Kind unification}
+ Kind unification
%* *
%************************************************************************
+Unifying kinds is much, much simpler than unifying types.
+
\begin{code}
unifyKind :: TcKind -- Expected
-> TcKind -- Actual
-> TcM ()
-unifyKind 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 [] [] = returnM ()
unifyKinds (k1:ks1) (k2:ks2) = unifyKind k1 k2 `thenM_`
unifyKinds ks1 ks2
-unifyKinds _ _ = panic "unifyKinds: length mis-match"
-\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 `thenM` \ maybe_ty ->
- case maybe_ty of
- Just ty' -> unifyOpenTypeKind ty'
- other -> unify_open_kind_help ty
-
-unifyOpenTypeKind ty
- | isTypeKind ty = returnM ()
- | otherwise = unify_open_kind_help ty
-
-unify_open_kind_help ty -- Revert to ordinary unification
- = newOpenTypeKind `thenM` \ open_kind ->
- unifyKind ty open_kind
+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}
unifyFunKind :: TcKind -> TcM (Maybe (TcKind, TcKind))
-- Like unifyFunTy, but does not fail; instead just returns Nothing
-unifyFunKind (TyVarTy tyvar)
- = getTcTyVar tyvar `thenM` \ maybe_ty ->
- case maybe_ty of
+unifyFunKind (KindVar kvar)
+ = readKindVar kvar `thenM` \ maybe_kind ->
+ case maybe_kind of
Just fun_kind -> unifyFunKind fun_kind
- Nothing -> newKindVar `thenM` \ arg_kind ->
- newKindVar `thenM` \ res_kind ->
- putTcTyVar tyvar (mkArrowKind arg_kind res_kind) `thenM_`
- returnM (Just (arg_kind,res_kind))
+ Nothing -> do { arg_kind <- newKindVar
+ ; res_kind <- newKindVar
+ ; writeKindVar kvar (mkArrowKind arg_kind res_kind)
+ ; returnM (Just (arg_kind,res_kind)) }
-unifyFunKind (FunTy arg_kind res_kind) = returnM (Just (arg_kind,res_kind))
-unifyFunKind (NoteTy _ ty) = unifyFunKind ty
-unifyFunKind other = returnM Nothing
+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
+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 `thenM` \ ty2' ->
- returnM (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') = tidyOpenTyVar tidy_env tv1
- (env2, ty2') = tidyOpenType env1 ty2
- pp1 = ppr tv1'
- pp2 = ppr ty2'
-
-unifyMisMatch ty1 ty2
- = zonkTcType ty1 `thenM` \ ty1' ->
- zonkTcType ty2 `thenM` \ 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
- (env1, tidy_tyvar) = tidyOpenTyVar emptyTidyEnv tyvar
- (env2, tidy_ty) = tidyOpenType env1 ty
-
-unifyCheck problem tyvar ty
- = (env2, hang msg
- 4 (sep [ppr tidy_tyvar, char '=', ppr tidy_ty]))
+ 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) = tidyOpenTyVar emptyTidyEnv tyvar
- (env2, tidy_ty) = tidyOpenType env1 ty
-
- msg = case problem of
- OccurCheck -> ptext SLIT("Occurs check: cannot construct the infinite type:")
- NotMonoType -> ptext SLIT("Cannot unify a type variable with a type scheme:")
+ 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}
%************************************************************************
%* *
%* *
%************************************************************************
-@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] -> TcM [TcTyVar]
+checkSigTyVars :: [TcTyVar] -> TcM ()
checkSigTyVars sig_tvs = check_sig_tyvars emptyVarSet sig_tvs
-checkSigTyVarsWrt :: TcTyVarSet -> [TcTyVar] -> TcM [TcTyVar]
+checkSigTyVarsWrt :: TcTyVarSet -> [TcTyVar] -> TcM ()
+-- The extra_tvs can include boxy type variables;
+-- e.g. TcMatches.tcCheckExistentialPat
checkSigTyVarsWrt extra_tvs sig_tvs
- = zonkTcTyVarsAndFV (varSetElems extra_tvs) `thenM` \ extra_tvs' ->
- check_sig_tyvars 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
- -- Not guaranteed zonked.
- -> TcM [TcTyVar] -- Zonked signature type variables
-
+ :: 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 []
+ = returnM ()
check_sig_tyvars extra_tvs sig_tvs
- = zonkTcTyVars sig_tvs `thenM` \ sig_tys ->
- tcGetGlobalTyVars `thenM` \ gbl_tvs ->
- let
- env_tvs = gbl_tvs `unionVarSet` extra_tvs
- in
- traceTc (text "check_sig_tyvars" <+> (vcat [text "sig_tys" <+> ppr sig_tys,
+ = 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])) `thenM_`
-
- checkM (allDistinctTyVars sig_tys env_tvs)
- (complain sig_tys env_tvs) `thenM_`
-
- returnM (map (tcGetTyVar "checkSigTyVars") sig_tys)
-
+ 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
- foldlM check
- (env2, emptyVarEnv, [])
- (tidy_tvs `zip` tidy_tys) `thenM` \ (env3, _, msgs) ->
+ main_msg = ptext SLIT("Inferred type is less polymorphic than expected")
- failWithTcM (env3, main_msg $$ nest 4 (vcat msgs))
- where
- (env1, tidy_tvs) = tidyOpenTyVars emptyTidyEnv sig_tvs
- (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)!
- returnM (tidy_env, acc, unify_msg sig_tyvar (quotes (ppr ty)) : msgs) ;
-
- Just tv ->
-
- case lookupVarEnv acc tv of {
- Just sig_tyvar' -> -- Error (b)!
- returnM (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:
- -- get the local TcIds and TyVars from the environment,
- -- and pass them to find_globals (they might have tv free)
- then findGlobals (unitVarSet tv) tidy_env `thenM` \ (tidy_env1, globs) ->
- returnM (tidy_env1, acc, escape_msg sig_tyvar tv globs : msgs)
-
- else -- All OK
- returnM (tidy_env, extendVarEnv acc tv sig_tyvar, msgs)
- }}
-\end{code}
+ 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) }
-
-\begin{code}
-----------------------
-escape_msg sig_tv tv globs
- = mk_msg sig_tv <+> ptext SLIT("escapes") $$
- if notNull globs then
- vcat [pp_it <+> ptext SLIT("is mentioned in the environment:"),
- nest 2 (vcat globs)]
- else
- empty -- 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.
+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
- pp_it | sig_tv /= tv = ptext SLIT("It unifies with") <+> quotes (ppr tv) <> comma <+> ptext SLIT("which")
- | otherwise = ptext SLIT("It")
-
-
-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
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 4 sub_msg]
+ nest 2 sub_msg]
in
returnM (env3, msg)
\end{code}
projects / ghc-hetmet.git / blobdiff