unifyType, unifyTypeList, unifyTheta,
unifyKind, unifyKinds, unifyFunKind,
checkExpectedKind,
- boxySubMatchType, boxyMatchTypes,
+ preSubType, boxyMatchTypes,
--------------------------------
-- Holes
#include "HsVersions.h"
-import HsSyn ( ExprCoFn(..), idCoercion, isIdCoercion, (<.>) )
+import HsSyn ( HsWrapper(..), idHsWrapper, isIdHsWrapper, (<.>),
+ mkWpLams, mkWpTyLams, mkWpApps )
import TypeRep ( Type(..), PredType(..) )
import TcMType ( lookupTcTyVar, LookupTyVarResult(..),
- tcInstSkolType, newKindVar, newMetaTyVar,
- tcInstBoxy, newBoxyTyVar, newBoxyTyVarTys, readFilledBox,
+ tcInstBoxyTyVar, newKindVar, newMetaTyVar,
+ newBoxyTyVar, newBoxyTyVarTys, readFilledBox,
readMetaTyVar, writeMetaTyVar, newFlexiTyVarTy,
- tcInstSkolTyVars, tcInstTyVar,
+ tcInstSkolTyVars, tcInstTyVar, tcInstSkolType,
zonkTcKind, zonkType, zonkTcType, zonkTcTyVarsAndFV,
readKindVar, writeKindVar )
import TcSimplify ( tcSimplifyCheck )
pprSkolTvBinding, isTauTy, isTauTyCon, isSigmaTy,
mkFunTy, mkFunTys, mkTyConApp, isMetaTyVar,
tcSplitForAllTys, tcSplitAppTy_maybe, tcSplitFunTys, mkTyVarTys,
- tyVarsOfType, mkPhiTy, mkTyVarTy, mkPredTy,
+ tcSplitSigmaTy, tyVarsOfType, mkPhiTy, mkTyVarTy, mkPredTy,
typeKind, mkForAllTys, mkAppTy, isBoxyTyVar,
+ tcView, exactTyVarsOfType,
tidyOpenType, tidyOpenTyVar, tidyOpenTyVars,
- pprType, tidyKind, tidySkolemTyVar, isSkolemTyVar, tcView,
- TvSubst, mkTvSubst, zipTyEnv, substTy, emptyTvSubst,
+ pprType, tidyKind, tidySkolemTyVar, isSkolemTyVar, isSigTyVar,
+ TvSubst, mkTvSubst, zipTyEnv, zipOpenTvSubst, emptyTvSubst,
+ substTy, substTheta,
lookupTyVar, extendTvSubst )
-import Kind ( Kind(..), SimpleKind, KindVar, isArgTypeKind,
+import Type ( Kind, SimpleKind, KindVar,
openTypeKind, liftedTypeKind, unliftedTypeKind,
mkArrowKind, defaultKind,
- isOpenTypeKind, argTypeKind, isLiftedTypeKind, isUnliftedTypeKind,
- isSubKind, pprKind, splitKindFunTys )
+ argTypeKind, isLiftedTypeKind, isUnliftedTypeKind,
+ isSubKind, pprKind, splitKindFunTys, isSubKindCon,
+ isOpenTypeKind, isArgTypeKind )
import TysPrim ( alphaTy, betaTy )
-import Inst ( newDicts, instToId )
+import Inst ( newDictBndrsO, instCall, instToId )
import TyCon ( TyCon, tyConArity, tyConTyVars, isSynTyCon )
import TysWiredIn ( listTyCon )
-import Id ( Id, mkSysLocal )
+import Id ( Id )
import Var ( Var, varName, tyVarKind, isTcTyVar, tcTyVarDetails )
-import VarSet ( emptyVarSet, mkVarSet, unitVarSet, unionVarSet, elemVarSet, varSetElems,
- extendVarSet, intersectsVarSet )
+import VarSet
import VarEnv
import Name ( Name, isSystemName )
import ErrUtils ( Message )
import Maybes ( expectJust, isNothing )
import BasicTypes ( Arity )
-import UniqSupply ( uniqsFromSupply )
import Util ( notNull, equalLength )
import Outputable
-> Arity -- Expected # of args
-> BoxyRhoType -- res_ty
-> ([BoxySigmaType] -> BoxyRhoType -> TcM a)
- -> TcM (ExprCoFn, a)
+ -> TcM (HsWrapper, a)
-- Attempt to decompse res_ty to have enough top-level arrows to
-- match the number of patterns in the match group
--
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' ->
+ = 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) }
+ ; return (idHsWrapper, 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
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
+ ; if isNothing mb_unit then bale_out args_so_far
else loop n args_so_far (FunTy arg_ty' res_ty') }
loop n args_so_far (TyVarTy tv)
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) } }
+ ; return (idHsWrapper, res) } }
where
mk_res_ty (res_ty' : arg_tys') = mkFunTys arg_tys' res_ty'
+ mk_res_ty [] = panic "TcUnify.mk_res_ty1"
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
+ loop n args_so_far res_ty = bale_out args_so_far
- bale_out args_so_far res_ty
+ bale_out args_so_far
= do { env0 <- tcInitTidyEnv
; res_ty' <- zonkTcType res_ty
; let (env1, res_ty'') = tidyOpenType env0 res_ty'
; return (fun_ty, arg_ty) } }
where
mk_res_ty [fun_ty', arg_ty'] = mkAppTy fun_ty' arg_ty'
+ mk_res_ty other = panic "TcUnify.mk_res_ty2"
tv_kind = tyVarKind tv
kinds = [mkArrowKind liftedTypeKind (defaultKind tv_kind),
-- m :: * -> k
%************************************************************************
\begin{code}
+preSubType :: [TcTyVar] -- Quantified type variables
+ -> TcTyVarSet -- Subset of quantified type variables
+ -- see Note [Pre-sub boxy]
+ -> TcType -- The rho-type part; quantified tyvars scopes over this
+ -> BoxySigmaType -- Matching type from the context
+ -> TcM [TcType] -- Types to instantiate the tyvars
+-- Perform pre-subsumption, and return suitable types
+-- to instantiate the quantified type varibles:
+-- info from the pre-subsumption, if there is any
+-- a boxy type variable otherwise
+--
+-- Note [Pre-sub boxy]
+-- The 'btvs' are a subset of 'qtvs'. They are the ones we can
+-- instantiate to a boxy type variable, because they'll definitely be
+-- filled in later. This isn't always the case; sometimes we have type
+-- variables mentioned in the context of the type, but not the body;
+-- f :: forall a b. C a b => a -> a
+-- Then we may land up with an unconstrained 'b', so we want to
+-- instantiate it to a monotype (non-boxy) type variable
+--
+-- The 'qtvs' that are *neither* fixed by the pre-subsumption, *nor* are in 'btvs',
+-- are instantiated to TauTv meta variables.
+
+preSubType qtvs btvs qty expected_ty
+ = do { tys <- mapM inst_tv qtvs
+ ; traceTc (text "preSubType" <+> (ppr qtvs $$ ppr btvs $$ ppr qty $$ ppr expected_ty $$ ppr pre_subst $$ ppr tys))
+ ; return tys }
+ where
+ pre_subst = boxySubMatchType (mkVarSet qtvs) qty expected_ty
+ inst_tv tv
+ | Just boxy_ty <- lookupTyVar pre_subst tv = return boxy_ty
+ | tv `elemVarSet` btvs = do { tv' <- tcInstBoxyTyVar tv
+ ; return (mkTyVarTy tv') }
+ | otherwise = do { tv' <- tcInstTyVar tv
+ ; return (mkTyVarTy tv') }
+
boxySubMatchType
:: TcTyVarSet -> TcType -- The "template"; the tyvars are skolems
-> BoxyRhoType -- Type to match (note a *Rho* type)
-> TvSubst -- Substitution of the [TcTyVar] to BoxySigmaTypes
+-- boxySubMatchType implements the Pre-subsumption judgement, in Fig 5 of the paper
+-- "Boxy types: inference for higher rank types and impredicativity"
+
+boxySubMatchType tmpl_tvs tmpl_ty boxy_ty
+ = go tmpl_tvs tmpl_ty emptyVarSet boxy_ty
+ where
+ go t_tvs t_ty b_tvs b_ty
+ | Just t_ty' <- tcView t_ty = go t_tvs t_ty' b_tvs b_ty
+ | Just b_ty' <- tcView b_ty = go t_tvs t_ty b_tvs b_ty'
+
+ go t_tvs (TyVarTy _) b_tvs b_ty = emptyTvSubst -- Rule S-ANY; no bindings
+ -- Rule S-ANY covers (a) type variables and (b) boxy types
+ -- in the template. Both look like a TyVarTy.
+ -- See Note [Sub-match] below
+
+ go t_tvs t_ty b_tvs b_ty
+ | isSigmaTy t_ty, (tvs, _, t_tau) <- tcSplitSigmaTy t_ty
+ = go (t_tvs `delVarSetList` tvs) t_tau b_tvs b_ty -- Rule S-SPEC
+ -- Under a forall on the left, if there is shadowing,
+ -- do not bind! Hence the delVarSetList.
+ | isSigmaTy b_ty, (tvs, _, b_tau) <- tcSplitSigmaTy b_ty
+ = go t_tvs t_ty (extendVarSetList b_tvs tvs) b_tau -- Rule S-SKOL
+ -- Add to the variables we must not bind to
+ -- NB: it's *important* to discard the theta part. Otherwise
+ -- consider (forall a. Eq a => a -> b) ~<~ (Int -> Int -> Bool)
+ -- and end up with a completely bogus binding (b |-> Bool), by lining
+ -- up the (Eq a) with the Int, whereas it should be (b |-> (Int->Bool)).
+ -- This pre-subsumption stuff can return too few bindings, but it
+ -- must *never* return bogus info.
+
+ go t_tvs (FunTy arg1 res1) b_tvs (FunTy arg2 res2) -- Rule S-FUN
+ = boxy_match t_tvs arg1 b_tvs arg2 (go t_tvs res1 b_tvs res2)
+ -- Match the args, and sub-match the results
+
+ go t_tvs t_ty b_tvs b_ty = boxy_match t_tvs t_ty b_tvs b_ty emptyTvSubst
+ -- Otherwise defer to boxy matching
+ -- This covers TyConApp, AppTy, PredTy
+\end{code}
+
+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.
+
+
+\begin{code}
boxyMatchTypes
:: TcTyVarSet -> [TcType] -- The "template"; the tyvars are skolems
-> [BoxySigmaType] -- Type to match
-> TvSubst -- Substitution of the [TcTyVar] to BoxySigmaTypes
+-- boxyMatchTypes implements the Pre-matching judgement, in Fig 5 of the paper
+-- "Boxy types: inference for higher rank types and impredicativity"
+
-- 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;
-- 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
+-- Precondition: none of the template type variables appear anywhere in the [BoxySigmaType]
--
--- 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 [] 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 tmpl_tvs t_ty boxy_tvs b_ty $
+ boxy_match_s tmpl_tvs t_tys boxy_tvs b_tys subst
+boxy_match_s tmpl_tvs _ boxy_tvs _ subst
+ = panic "boxy_match_s" -- Lengths do not match
+
------------
boxy_match :: TcTyVarSet -> TcType -- Template
| 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 ty1 ty2 -- C.f. the isSigmaTy case for boxySubMatchType
+ | isSigmaTy ty1
+ , (tvs1, _, tau1) <- tcSplitSigmaTy ty1
+ , (tvs2, _, tau2) <- tcSplitSigmaTy ty2
+ , equalLength tvs1 tvs2
+ = boxy_match (tmpl_tvs `delVarSetList` tvs1) tau1
+ (boxy_tvs `extendVarSetList` tvs2) tau2 subst
go (TyConApp tc1 tys1) (TyConApp tc2 tys2)
| tc1 == tc2 = go_s tys1 tys2
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
+ , boxy_tvs `disjointVarSet` tyVarsOfType orig_boxy_ty
+ , typeKind b_ty `isSubKind` tyVarKind tv -- See Note [Matching kinds]
= extendTvSubst subst tv boxy_ty'
+ | otherwise
+ = subst -- Ignore others
where
boxy_ty' = case lookupTyVar subst tv of
Nothing -> orig_boxy_ty
Just ty -> ty `boxyLub` orig_boxy_ty
- go _ _ = subst -- Always safe
+ go _ _ = emptyTvSubst -- It's important to *fail* by returning the empty substitution
+ -- Example: Tree a ~ Maybe Int
+ -- We do not want to bind (a |-> Int) in pre-matching, because that can give very
+ -- misleading error messages. An even more confusing case is
+ -- a -> b ~ Maybe Int
+ -- Then we do not want to bind (b |-> Int)! It's always safe to discard bindings
+ -- from this pre-matching phase.
--------
go_s tys1 tys2 = boxy_match_s tmpl_tvs tys1 boxy_tvs tys2 subst
= 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
+ | isTcTyVar tv1, isBoxyTyVar tv1 -- choose ty2 if ty2 is a box
+ = orig_ty2
-- Look inside type synonyms, but only if the naive version fails
go ty1 ty2 | Just ty1' <- tcView ty1 = go ty1' ty2
go ty1 ty2 = orig_ty1 -- Default
\end{code}
+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.
%************************************************************************
%* *
\begin{code}
-----------------
-tcSubExp :: BoxySigmaType -> BoxySigmaType -> TcM ExprCoFn -- Locally used only
+tcSubExp :: BoxySigmaType -> BoxySigmaType -> TcM HsWrapper -- Locally used only
-- (tcSub act exp) checks that
-- act <= exp
tcSubExp actual_ty expected_ty
- = addErrCtxtM (unifyCtxt actual_ty expected_ty)
- (tc_sub True actual_ty actual_ty expected_ty expected_ty)
-
-tcFunResTy :: Name -> BoxySigmaType -> BoxySigmaType -> TcM ExprCoFn -- Locally used only
+ = -- addErrCtxtM (unifyCtxt actual_ty expected_ty) $
+ -- Adding the error context here leads to some very confusing error
+ -- messages, such as "can't match forall a. a->a with forall a. a->a"
+ -- Example is tcfail165:
+ -- do var <- newEmptyMVar :: IO (MVar (forall a. Show a => a -> String))
+ -- putMVar var (show :: forall a. Show a => a -> String)
+ -- Here the info does not flow from the 'var' arg of putMVar to its 'show' arg
+ -- but after zonking it looks as if it does!
+ --
+ -- So instead I'm adding the error context when moving from tc_sub to u_tys
+
+ traceTc (text "tcSubExp" <+> ppr actual_ty <+> ppr expected_ty) >>
+ tc_sub SubOther actual_ty actual_ty False expected_ty expected_ty
+
+tcFunResTy :: Name -> BoxySigmaType -> BoxySigmaType -> TcM HsWrapper -- Locally used only
tcFunResTy fun actual_ty expected_ty
- = addErrCtxtM (checkFunResCtxt fun actual_ty expected_ty) $
- (tc_sub True actual_ty actual_ty expected_ty expected_ty)
+ = traceTc (text "tcFunResTy" <+> ppr actual_ty <+> ppr expected_ty) >>
+ tc_sub (SubFun fun) actual_ty actual_ty False expected_ty expected_ty
-----------------
-tc_sub :: Outer -- See comments with uTys
+data SubCtxt = SubDone -- Error-context already pushed
+ | SubFun Name -- Context is tcFunResTy
+ | SubOther -- Context is something else
+
+tc_sub :: SubCtxt -- How to add an error-context
-> BoxySigmaType -- actual_ty, before expanding synonyms
-> BoxySigmaType -- ..and after
+ -> InBox -- True <=> expected_ty is inside a box
-> BoxySigmaType -- expected_ty, before
-> BoxySigmaType -- ..and after
- -> TcM ExprCoFn
+ -> TcM HsWrapper
+ -- The acual_ty is never inside a box
+-- IMPORTANT pre-condition: if the args contain foralls, the bound type
+-- variables are visible non-monadically
+-- (i.e. tha args are sufficiently zonked)
+-- This invariant is needed so that we can "see" the foralls, ad
+-- e.g. in the SPEC rule where we just use splitSigmaTy
+
+tc_sub sub_ctxt act_sty act_ty exp_ib exp_sty exp_ty
+ = tc_sub1 sub_ctxt act_sty act_ty exp_ib exp_sty exp_ty
+ -- This indirection is just here to make
+ -- it easy to insert a debug trace!
-tc_sub outer act_sty act_ty exp_sty exp_ty
- | Just exp_ty' <- tcView exp_ty = tc_sub False act_sty act_ty exp_sty exp_ty'
-tc_sub outer act_sty act_ty exp_sty exp_ty
- | Just act_ty' <- tcView act_ty = tc_sub False act_sty act_ty' exp_sty exp_ty
+tc_sub1 sub_ctxt act_sty act_ty exp_ib exp_sty exp_ty
+ | Just exp_ty' <- tcView exp_ty = tc_sub sub_ctxt act_sty act_ty exp_ib exp_sty exp_ty'
+tc_sub1 sub_ctxt act_sty act_ty exp_ib exp_sty exp_ty
+ | Just act_ty' <- tcView act_ty = tc_sub sub_ctxt act_sty act_ty' exp_ib exp_sty exp_ty
-----------------------------------
-- Rule SBOXY, plus other cases when act_ty is a type variable
-- Just defer to boxy matching
-- This rule takes precedence over SKOL!
-tc_sub outer act_sty (TyVarTy tv) exp_sty exp_ty
- = do { uVar outer False tv False exp_sty exp_ty
- ; return idCoercion }
+tc_sub1 sub_ctxt act_sty (TyVarTy tv) exp_ib exp_sty exp_ty
+ = do { addSubCtxt sub_ctxt act_sty exp_sty $
+ uVar True False tv exp_ib exp_sty exp_ty
+ ; return idHsWrapper }
-----------------------------------
-- Skolemisation case (rule SKOL)
-- g :: Ord b => b->b
-- Consider f g !
-tc_sub outer act_sty act_ty exp_sty exp_ty
- | isSigmaTy exp_ty
- = do { (gen_fn, co_fn) <- tcGen exp_ty act_tvs $ \ body_exp_ty ->
- tc_sub False act_sty act_ty body_exp_ty body_exp_ty
+tc_sub1 sub_ctxt act_sty act_ty exp_ib exp_sty exp_ty
+ | not exp_ib, -- SKOL does not apply if exp_ty is inside a box
+ isSigmaTy exp_ty
+ = do { (gen_fn, co_fn) <- tcGen exp_ty act_tvs $ \ _ body_exp_ty ->
+ tc_sub sub_ctxt act_sty act_ty False 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
+ -- It's really important to check for escape wrt
+ -- the free vars of both expected_ty *and* actual_ty
-----------------------------------
-- Specialisation case (rule ASPEC):
-- expected_ty: Int -> Int
-- co_fn e = e Int dOrdInt
-tc_sub outer act_sty actual_ty exp_sty expected_ty
+tc_sub1 sub_ctxt act_sty actual_ty exp_ib exp_sty expected_ty
+-- Implements the new SPEC rule in the Appendix of the paper
+-- "Boxy types: inference for higher rank types and impredicativity"
+-- (This appendix isn't in the published version.)
+-- The idea is to *first* do pre-subsumption, and then full subsumption
+-- Example: forall a. a->a <= Int -> (forall b. Int)
+-- Pre-subsumpion finds a|->Int, and that works fine, whereas
+-- just running full subsumption would fail.
| 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 False tau tau exp_sty expected_ty
- ; return (co_fn <.> inst_fn) }
+ = do { -- Perform pre-subsumption, and instantiate
+ -- the type with info from the pre-subsumption;
+ -- boxy tyvars if pre-subsumption gives no info
+ let (tyvars, theta, tau) = tcSplitSigmaTy actual_ty
+ tau_tvs = exactTyVarsOfType tau
+ ; inst_tys <- if exp_ib then -- Inside a box, do not do clever stuff
+ do { tyvars' <- mapM tcInstBoxyTyVar tyvars
+ ; return (mkTyVarTys tyvars') }
+ else -- Outside, do clever stuff
+ preSubType tyvars tau_tvs tau expected_ty
+ ; let subst' = zipOpenTvSubst tyvars inst_tys
+ tau' = substTy subst' tau
+
+ -- Perform a full subsumption check
+ ; traceTc (text "tc_sub_spec" <+> vcat [ppr actual_ty,
+ ppr tyvars <+> ppr theta <+> ppr tau,
+ ppr tau'])
+ ; co_fn2 <- tc_sub sub_ctxt tau' tau' exp_ib exp_sty expected_ty
+
+ -- Deal with the dictionaries
+ ; co_fn1 <- instCall InstSigOrigin inst_tys (substTheta subst' theta)
+ ; return (co_fn2 <.> co_fn1) }
-----------------------------------
-- 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
+tc_sub1 sub_ctxt act_sty (FunTy act_arg act_res) exp_ib exp_sty (FunTy exp_arg exp_res)
+ = addSubCtxt sub_ctxt act_sty exp_sty $
+ tc_sub_funs act_arg act_res exp_ib exp_arg exp_res
-- Function case (rule F2)
-tc_sub outer act_sty act_ty@(FunTy act_arg act_res) exp_sty (TyVarTy exp_tv)
+tc_sub1 sub_ctxt act_sty act_ty@(FunTy act_arg act_res) _ exp_sty (TyVarTy exp_tv)
| isBoxyTyVar exp_tv
- = do { cts <- readMetaTyVar exp_tv
+ = addSubCtxt sub_ctxt act_sty exp_sty $
+ do { cts <- readMetaTyVar exp_tv
; case cts of
- Indirect ty -> do { u_tys outer False act_sty act_ty True exp_sty ty
- ; return idCoercion }
+ Indirect ty -> tc_sub SubDone act_sty act_ty True exp_sty ty
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 } }
+ ; tc_sub_funs act_arg act_res True arg_ty res_ty } }
where
mk_res_ty [arg_ty', res_ty'] = mkFunTy arg_ty' res_ty'
+ mk_res_ty other = panic "TcUnify.mk_res_ty3"
fun_kinds = [argTypeKind, openTypeKind]
-- Everything else: defer to boxy matching
-tc_sub outer act_sty actual_ty exp_sty expected_ty
- = do { u_tys outer False act_sty actual_ty False exp_sty expected_ty
- ; return idCoercion }
+tc_sub1 sub_ctxt act_sty actual_ty exp_ib exp_sty expected_ty
+ = do { addSubCtxt sub_ctxt act_sty exp_sty $
+ u_tys True False act_sty actual_ty exp_ib exp_sty expected_ty
+ ; return idHsWrapper }
-----------------------------------
-tc_sub_funs act_arg act_res exp_arg exp_res
- = do { uTys False act_arg False exp_arg
- ; co_fn_res <- tc_sub False act_res act_res exp_res exp_res
+tc_sub_funs act_arg act_res exp_ib exp_arg exp_res
+ = do { uTys False act_arg exp_ib exp_arg
+ ; co_fn_res <- tc_sub SubDone act_res act_res exp_ib 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)
+ -> HsWrapper -- HsExpr a -> HsExpr b
+ -> TcM HsWrapper -- HsExpr (arg_tys -> a) -> HsExpr (arg_tys -> b)
wrapFunResCoercion arg_tys co_fn_res
- | isIdCoercion co_fn_res = return idCoercion
+ | isIdHsWrapper co_fn_res = return idHsWrapper
| 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))) }
+ = do { arg_ids <- newSysLocalIds FSLIT("sub") arg_tys
+ ; return (mkWpLams arg_ids <.> co_fn_res <.> mkWpApps arg_ids) }
\end{code}
-> TcTyVarSet -- Extra tyvars that the universally
-- quantified tyvars of expected_ty
-- must not be unified
- -> (BoxyRhoType -> TcM result) -- spec_ty
- -> TcM (ExprCoFn, result)
+ -> ([TcTyVar] -> BoxyRhoType -> TcM result)
+ -> TcM (HsWrapper, 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
-- 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) ->
+ ((tvs', theta', rho'), 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
#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])
+ text "inst ty" <+> ppr tvs' <+> ppr theta' <+> ppr rho',
+ text "free_tvs" <+> ppr free_tvs])
#endif
-- Type-check the arg and unify with poly type
- ; (result, lie) <- getLIE (thing_inside rho_ty)
+ ; (result, lie) <- getLIE (thing_inside tvs' rho')
-- 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.
- ; dicts <- newDicts (SigOrigin skol_info) theta
- ; inst_binds <- tcSimplifyCheck sig_msg forall_tvs dicts lie
+ ; dicts <- newDictBndrsO (SigOrigin skol_info) theta'
+ ; inst_binds <- tcSimplifyCheck sig_msg tvs' dicts lie
- ; checkSigTyVarsWrt free_tvs forall_tvs
+ ; checkSigTyVarsWrt free_tvs 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
+ -- The WpLet binds any Insts which came out of the simplification.
+ dict_ids = map instToId dicts
+ co_fn = mkWpTyLams tvs' <.> mkWpLams dict_ids <.> WpLet inst_binds
; returnM (co_fn, result) }
where
free_tvs = tyVarsOfType expected_ty `unionVarSet` extra_tvs
We call the first one \tr{ps_ty1}, \tr{ps_ty2} for ``possible synomym''.
\begin{code}
-type NoBoxes = Bool -- True <=> definitely no boxes in this type
- -- False <=> there might be boxes (always safe)
+type InBox = Bool -- True <=> we are inside a box
+ -- False <=> we are outside a box
+ -- The importance of this is that if we get "filled-box meets
+ -- filled-box", we'll look into the boxes and unify... but
+ -- we must not allow polytypes. But if we are in a box on
+ -- just one side, then we can allow polytypes
type Outer = Bool -- True <=> this is the outer level of a unification
-- so that the types being unified are the
-- pop the context to remove the "Expected/Acutal" context
uTysOuter, uTys
- :: NoBoxes -> TcType -- ty1 is the *expected* type
- -> NoBoxes -> TcType -- ty2 is the *actual* type
+ :: InBox -> TcType -- ty1 is the *expected* type
+ -> InBox -> TcType -- ty2 is the *actual* type
-> TcM ()
-uTysOuter nb1 ty1 nb2 ty2 = u_tys True nb1 ty1 ty1 nb2 ty2 ty2
-uTys nb1 ty1 nb2 ty2 = u_tys False nb1 ty1 ty1 nb2 ty2 ty2
+uTysOuter nb1 ty1 nb2 ty2 = do { traceTc (text "uTysOuter" <+> ppr ty1 <+> ppr ty2)
+ ; u_tys True nb1 ty1 ty1 nb2 ty2 ty2 }
+uTys nb1 ty1 nb2 ty2 = do { traceTc (text "uTys" <+> ppr ty1 <+> ppr ty2)
+ ; u_tys False nb1 ty1 ty1 nb2 ty2 ty2 }
--------------
-uTys_s :: NoBoxes -> [TcType] -- ty1 is the *actual* types
- -> NoBoxes -> [TcType] -- ty2 is the *expected* types
+uTys_s :: InBox -> [TcType] -- ty1 is the *actual* types
+ -> InBox -> [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
--------------
u_tys :: Outer
- -> NoBoxes -> TcType -> TcType -- ty1 is the *actual* type
- -> NoBoxes -> TcType -> TcType -- ty2 is the *expected* type
+ -> InBox -> TcType -> TcType -- ty1 is the *actual* type
+ -> InBox -> TcType -> TcType -- ty2 is the *expected* type
-> TcM ()
u_tys outer nb1 orig_ty1 ty1 nb2 orig_ty2 ty2
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.
+ -- If both sides are inside a box, we are in a "box-meets-box"
+ -- situation, and we should not have a polytype at all.
+ -- If we get here we have two boxes, already filled with
+ -- the same polytype... but it should be a monotype.
+ -- This check comes last, because the error message is
+ -- extremely unhelpful.
; ifM (nb1 && nb2) (notMonoType ty1)
}
where
-> Bool -- False => tyvar is the "expected"
-- True => ty is the "expected" thing
-> TcTyVar
- -> NoBoxes -- True <=> definitely no boxes in t2
+ -> InBox -- True <=> definitely no boxes in t2
-> TcTauType -> TcTauType -- printing and real versions
-> TcM ()
| otherwise = brackets (equals <+> ppr ty2)
; traceTc (text "uVar" <+> ppr swapped <+>
sep [ppr tv1 <+> dcolon <+> ppr (tyVarKind tv1 ),
- nest 2 (ptext SLIT(" :=: ")),
+ nest 2 (ptext SLIT(" <-> ")),
ppr ps_ty2 <+> dcolon <+> ppr (typeKind ty2) <+> expansion])
; details <- lookupTcTyVar tv1
; case details of
IndirectTv ty1
| swapped -> u_tys outer nb2 ps_ty2 ty2 True ty1 ty1 -- Swap back
| otherwise -> u_tys outer True ty1 ty1 nb2 ps_ty2 ty2 -- Same order
- -- The 'True' here says that ty1
- -- is definitely box-free
- DoneTv details1 -> uUnfilledVar outer swapped tv1 details1 nb2 ps_ty2 ty2
+ -- The 'True' here says that ty1 is now inside a box
+ DoneTv details1 -> uUnfilledVar outer swapped tv1 details1 ps_ty2 ty2
}
----------------
uUnfilledVar :: Outer
-> Bool -- Args are swapped
- -> TcTyVar -> TcTyVarDetails -- Tyvar 1
- -> NoBoxes -> TcTauType -> TcTauType -- Type 2
+ -> TcTyVar -> TcTyVarDetails -- Tyvar 1
+ -> TcTauType -> TcTauType -- Type 2
-> TcM ()
-- Invariant: tyvar 1 is not unified with anything
-uUnfilledVar outer swapped tv1 details1 nb2 ps_ty2 ty2
+uUnfilledVar outer swapped tv1 details1 ps_ty2 ty2
| Just ty2' <- tcView ty2
= -- Expand synonyms; ignore FTVs
- uUnfilledVar False swapped tv1 details1 nb2 ps_ty2 ty2'
+ uUnfilledVar False swapped tv1 details1 ps_ty2 ty2'
-uUnfilledVar outer swapped tv1 details1 nb2 ps_ty2 ty2@(TyVarTy tv2)
- -- Same type variable => no-op
- | tv1 == tv2
- = returnM ()
+uUnfilledVar outer swapped tv1 details1 ps_ty2 (TyVarTy tv2)
+ | tv1 == tv2 -- Same type variable => no-op (but watch out for the boxy case)
+ = case details1 of
+ MetaTv BoxTv ref1 -- A boxy type variable meets itself;
+ -- this is box-meets-box, so fill in with a tau-type
+ -> do { tau_tv <- tcInstTyVar tv1
+ ; updateMeta tv1 ref1 (mkTyVarTy tau_tv) }
+ other -> returnM () -- No-op
-- Distinct type variables
| otherwise
= do { lookup2 <- lookupTcTyVar tv2
; case lookup2 of
- IndirectTv ty2' -> uUnfilledVar outer swapped tv1 details1 True ty2' ty2'
+ IndirectTv ty2' -> uUnfilledVar outer swapped tv1 details1 ty2' ty2'
DoneTv details2 -> uUnfilledVars outer swapped tv1 details1 tv2 details2
}
-uUnfilledVar outer swapped tv1 details1 nb2 ps_ty2 non_var_ty2 -- ty2 is not a type variable
+uUnfilledVar outer swapped tv1 details1 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
+ MetaTv info ref1 -> uMetaVar swapped tv1 info ref1 ps_ty2 non_var_ty2
skolem_details -> mis_match
where
mis_match = unifyMisMatch outer swapped (TyVarTy tv1) ps_ty2
----------------
uMetaVar :: Bool
-> TcTyVar -> BoxInfo -> IORef MetaDetails
- -> NoBoxes -> TcType -> TcType
+ -> 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
+uMetaVar swapped tv1 BoxTv ref1 ps_ty2 non_var_ty2
+ = -- tv1 is a BoxTv. So we must unbox ty2, to ensure
+ -- that any boxes in ty2 are filled with monotypes
+ --
+ -- It should not be the case that tv1 occurs in ty2
+ -- (i.e. no occurs check should be needed), but if perchance
+ -- it does, the unbox operation will fill it, and the DEBUG
+ -- checks for that.
+ do { final_ty <- unBox ps_ty2
+#ifdef DEBUG
+ ; meta_details <- readMutVar ref1
+ ; case meta_details of
+ Indirect ty -> WARN( True, ppr tv1 <+> ppr ty )
+ return () -- This really should *not* happen
+ Flexi -> return ()
+#endif
+ ; checkUpdateMeta swapped tv1 ref1 final_ty }
+
+uMetaVar swapped tv1 info1 ref1 ps_ty2 non_var_ty2
+ = do { final_ty <- checkTauTvUpdate tv1 ps_ty2 -- Occurs check + monotype check
; checkUpdateMeta swapped tv1 ref1 final_ty }
----------------
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_pred (EqPred t1 t2) = do { t1' <- go t1; t2' <- go t2; return (EqPred t1' t2') }
go_tyvar tv (SkolemTv _) = return (TyVarTy tv)
go_tyvar tv (MetaTv box ref)
-- |- s' ~ box(s)
-- with input s', and result s
--
--- It remove all boxes from the input type, returning a non-boxy type.
+-- It removes 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
--
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') }
+unBoxPred (EqPred ty1 ty2) = do { ty1' <- unBox ty1; ty2' <- unBox ty2; return (EqPred ty1' ty2') }
\end{code}
----------------
-- If an error happens we try to figure out whether the function
-- function has been given too many or too few arguments, and say so.
-checkFunResCtxt fun actual_res_ty expected_res_ty tidy_env
- = do { exp_ty' <- zonkTcType expected_res_ty
- ; act_ty' <- zonkTcType actual_res_ty
- ; let
- (env1, exp_ty'') = tidyOpenType tidy_env exp_ty'
- (env2, act_ty'') = tidyOpenType env1 act_ty'
- (exp_args, _) = tcSplitFunTys exp_ty''
- (act_args, _) = tcSplitFunTys act_ty''
+addSubCtxt SubDone actual_res_ty expected_res_ty thing_inside
+ = thing_inside
+addSubCtxt sub_ctxt actual_res_ty expected_res_ty thing_inside
+ = addErrCtxtM mk_err thing_inside
+ where
+ mk_err tidy_env
+ = do { exp_ty' <- zonkTcType expected_res_ty
+ ; act_ty' <- zonkTcType actual_res_ty
+ ; let (env1, exp_ty'') = tidyOpenType tidy_env exp_ty'
+ (env2, act_ty'') = tidyOpenType env1 act_ty'
+ (exp_args, _) = tcSplitFunTys exp_ty''
+ (act_args, _) = tcSplitFunTys act_ty''
- len_act_args = length act_args
- len_exp_args = length exp_args
+ len_act_args = length act_args
+ len_exp_args = length exp_args
- message | len_exp_args < len_act_args = wrongArgsCtxt "too few" fun
- | len_exp_args > len_act_args = wrongArgsCtxt "too many" fun
- | otherwise = mkExpectedActualMsg act_ty'' exp_ty''
- ; return (env2, message) }
+ message = case sub_ctxt of
+ SubFun fun | len_exp_args < len_act_args -> wrongArgsCtxt "too few" fun
+ | len_exp_args > len_act_args -> wrongArgsCtxt "too many" fun
+ other -> mkExpectedActualMsg act_ty'' exp_ty''
+ ; return (env2, message) }
- where
wrongArgsCtxt too_many_or_few fun
= ptext SLIT("Probable cause:") <+> quotes (ppr fun)
<+> ptext SLIT("is applied to") <+> text too_many_or_few
simple_result = (env1, quotes (ppr tidy_ty), empty)
; case tidy_ty of
TyVarTy tv
- | isSkolemTyVar tv -> return (env2, pp_rigid tv',
- pprSkolTvBinding tv')
+ | isSkolemTyVar tv || isSigTyVar tv
+ -> return (env2, pp_rigid tv', pprSkolTvBinding tv')
| otherwise -> return simple_result
where
(env2, tv') = tidySkolemTyVar env1 tv
= do { ty' <- zonkTcType ty
; env0 <- tcInitTidyEnv
; let (env1, tidy_ty) = tidyOpenType env0 ty'
- msg = ptext SLIT("Cannot match a monotype with") <+> ppr tidy_ty
+ msg = ptext SLIT("Cannot match a monotype with") <+> quotes (ppr tidy_ty)
; failWithTcM (env1, msg) }
occurCheck tyvar ty
unifyKind :: TcKind -- Expected
-> TcKind -- Actual
-> TcM ()
-unifyKind LiftedTypeKind LiftedTypeKind = returnM ()
-unifyKind UnliftedTypeKind UnliftedTypeKind = returnM ()
+unifyKind (TyConApp kc1 []) (TyConApp kc2 [])
+ | isSubKindCon kc2 kc1 = 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 }
+unifyKind (FunTy a1 r1) (FunTy 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 (TyVarTy kv1) k2 = uKVar False kv1 k2
+unifyKind k1 (TyVarTy kv2) = uKVar True kv2 k1
unifyKind k1 k2 = unifyKindMisMatch k1 k2
unifyKinds :: [TcKind] -> [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 }
+ Flexi -> uUnboundKVar swapped kv1 k2
+ Indirect k1 | swapped -> unifyKind k2 k1
+ | otherwise -> unifyKind k1 k2 }
----------------
uUnboundKVar :: Bool -> KindVar -> TcKind -> TcM ()
-uUnboundKVar swapped kv1 k2@(KindVar kv2)
+uUnboundKVar swapped kv1 k2@(TyVarTy 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 }
+ Indirect k2 -> uUnboundKVar swapped kv1 k2
+ Flexi -> writeKindVar kv1 k2 }
uUnboundKVar swapped kv1 non_var_k2
= do { k2' <- zonkTcKind non_var_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
+ not_in (TyVarTy kv2) = kv1 /= kv2
+ not_in (FunTy 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
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 UnliftedTypeKind = return unliftedTypeKind
- go sw k@(KindVar _) = return k -- KindVars are always simple
+ go sw (FunTy k1 k2) = do { k1' <- go (not sw) k1
+ ; k2' <- go sw k2
+ ; return (mkArrowKind k1' k2') }
+ go True k
+ | isOpenTypeKind k = return liftedTypeKind
+ | isArgTypeKind k = return liftedTypeKind
+ go sw k
+ | isLiftedTypeKind k = return liftedTypeKind
+ | isUnliftedTypeKind k = return unliftedTypeKind
+ go sw k@(TyVarTy _) = 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
unifyFunKind :: TcKind -> TcM (Maybe (TcKind, TcKind))
-- Like unifyFunTy, but does not fail; instead just returns Nothing
-unifyFunKind (KindVar kvar)
- = readKindVar kvar `thenM` \ maybe_kind ->
+unifyFunKind (TyVarTy 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)) }
+ Indirect fun_kind -> unifyFunKind fun_kind
+ Flexi ->
+ 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
+unifyFunKind (FunTy arg_kind res_kind) = returnM (Just (arg_kind,res_kind))
+unifyFunKind other = returnM Nothing
\end{code}
%************************************************************************
projects / ghc-hetmet.git / blobdiff