tcSplitForAllTys, tcSplitAppTy_maybe, tcSplitFunTys, mkTyVarTys,
tcSplitSigmaTy, tyVarsOfType, mkPhiTy, mkTyVarTy, mkPredTy,
typeKind, mkForAllTys, mkAppTy, isBoxyTyVar,
- exactTyVarsOfType,
+ tcView, exactTyVarsOfType,
tidyOpenType, tidyOpenTyVar, tidyOpenTyVars,
- pprType, tidyKind, tidySkolemTyVar, isSkolemTyVar, tcView,
+ pprType, tidyKind, tidySkolemTyVar, isSkolemTyVar, isSigTyVar,
TvSubst, mkTvSubst, zipTyEnv, zipOpenTvSubst, emptyTvSubst,
substTy, substTheta,
lookupTyVar, extendTvSubst )
; return (idCoercion, 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.
; 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
- -- that can be instantiated with boxy types
+ -- 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
-- info from the pre-subsumption, if there is any
-- a boxy type variable otherwise
--
--- 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
+-- 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
boxy_match_s tmpl_tvs (t_ty:t_tys) boxy_tvs (b_ty:b_tys) 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
------------
; tc_sub_funs act_arg act_res 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
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