module TcUnify (
-- Full-blown subsumption
- tcSubExp, tcFunResTy, tcGen,
+ tcSubExp, tcGen,
checkSigTyVars, checkSigTyVarsWrt, bleatEscapedTvs, sigCtxt,
-- Various unifications
-- Holes
tcInfer, subFunTys, unBox, refineBox, refineBoxToTau, withBox,
boxyUnify, boxyUnifyList, zapToMonotype,
- boxySplitListTy, boxySplitTyConApp, boxySplitAppTy,
+ boxySplitListTy, boxySplitPArrTy, boxySplitTyConApp, boxySplitAppTy,
wrapFunResCoercion
) where
\begin{code}
tcInfer :: (BoxyType -> TcM a) -> TcM (a, TcType)
-tcInfer tc_infer
- = do { box <- newBoxyTyVar openTypeKind
- ; res <- tc_infer (mkTyVarTy box)
- ; res_ty <- {- pprTrace "tcInfer" (ppr (mkTyVarTy box)) $ -} readFilledBox box -- Guaranteed filled-in by now
- ; return (res, res_ty) }
+tcInfer tc_infer = withBox openTypeKind tc_infer
\end{code}
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
+ -- 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) }
; co_fn' <- wrapFunResCoercion [arg_ty] co_fn
; return (co_fn', res) }
+ -- Try to normalise synonym families and defer if that's not possible
+ loop n args_so_far ty@(TyConApp tc tys)
+ | isOpenSynTyCon tc
+ = do { (coi1, ty') <- tcNormaliseFamInst ty
+ ; case coi1 of
+ IdCo -> defer n args_so_far ty
+ -- no progress, but maybe solvable => defer
+ ACo _ -> -- progress: so lets try again
+ do { (co_fn, res) <- loop n args_so_far ty'
+ ; return $ (co_fn <.> coiToHsWrapper (mkSymCoI coi1), res)
+ }
+ }
+
-- res_ty might have a type variable at the head, such as (a b c),
-- in which case we must fill in with (->). Simplest thing to do
-- is to use boxyUnify, but we catch failure and generate our own
-- error message on failure
loop n args_so_far res_ty@(AppTy _ _)
= do { [arg_ty',res_ty'] <- newBoxyTyVarTys [argTypeKind, openTypeKind]
- ; (_, mb_coi) <- tryTcErrs $ boxyUnify res_ty (FunTy arg_ty' res_ty')
+ ; (_, mb_coi) <- tryTcErrs $
+ boxyUnify res_ty (FunTy arg_ty' res_ty')
; if isNothing mb_coi then bale_out args_so_far
- else do { case expectJust "subFunTys" mb_coi of
- IdCo -> return ()
- ACo co -> traceTc (text "you're dropping a coercion: " <+> ppr co)
- ; loop n args_so_far (FunTy arg_ty' res_ty')
+ else do { let coi = expectJust "subFunTys" mb_coi
+ ; (co_fn, res) <- loop n args_so_far (FunTy arg_ty'
+ res_ty')
+ ; return (co_fn <.> coiToHsWrapper coi, res)
}
}
- loop n args_so_far (TyVarTy tv)
+ loop n args_so_far ty@(TyVarTy tv)
| isTyConableTyVar 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 (idHsWrapper, res) } }
+ Flexi ->
+ do { (res_ty:arg_tys) <- withMetaTvs tv kinds mk_res_ty
+ ; res <- thing_inside (reverse args_so_far ++ arg_tys)
+ res_ty
+ ; return (idHsWrapper, res) } }
+ | otherwise -- defer as tyvar may be refined by equalities
+ = defer n args_so_far ty
where
mk_res_ty (res_ty' : arg_tys') = mkFunTys arg_tys' res_ty'
mk_res_ty [] = panic "TcUnify.mk_res_ty1"
loop n args_so_far res_ty = bale_out args_so_far
+ -- build a template type a1 -> ... -> an -> b and defer an equality
+ -- between that template and the expected result type res_ty; then,
+ -- use the template to type the thing_inside
+ defer n args_so_far ty
+ = do { arg_tys <- newFlexiTyVarTys n argTypeKind
+ ; res_ty' <- newFlexiTyVarTy openTypeKind
+ ; let fun_ty = mkFunTys arg_tys res_ty'
+ err = error_herald <> comma $$
+ text "which does not match its type"
+ ; coi <- addErrCtxt err $
+ defer_unification False False fun_ty ty
+ ; res <- thing_inside (reverse args_so_far ++ arg_tys) res_ty'
+ ; return (coiToHsWrapper coi, res)
+ }
+
bale_out args_so_far
= do { env0 <- tcInitTidyEnv
; res_ty' <- zonkTcType res_ty
----------------------
boxySplitTyConApp :: TyCon -- T :: k1 -> ... -> kn -> *
-> BoxyRhoType -- Expected type (T a b c)
- -> TcM [BoxySigmaType] -- Element types, a b c
- -- It's used for wired-in tycons, so we call checkWiredInTyCOn
+ -> TcM ([BoxySigmaType], -- Element types, a b c
+ CoercionI) -- T a b c ~ orig_ty
+ -- It's used for wired-in tycons, so we call checkWiredInTyCon
-- Precondition: never called with FunTyCon
-- Precondition: input type :: *
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)
+ loop n_req args_so_far ty@(TyConApp tycon args)
| tc == tycon
= ASSERT( n_req == length args) -- ty::*
- return (args ++ args_so_far)
+ return (args ++ args_so_far, IdCo)
+
+ | isOpenSynTyCon tycon -- try to normalise type family application
+ = do { (coi1, ty') <- tcNormaliseFamInst ty
+ ; traceTc $ text "boxySplitTyConApp:" <+>
+ ppr ty <+> text "==>" <+> ppr ty'
+ ; case coi1 of
+ IdCo -> defer -- no progress, but maybe solvable => defer
+ ACo _ -> -- progress: so lets try again
+ do { (args, coi2) <- loop n_req args_so_far ty'
+ ; return $ (args, coi2 `mkTransCoI` mkSymCoI coi1)
+ }
+ }
loop n_req args_so_far (AppTy fun arg)
| n_req > 0
- = loop (n_req - 1) (arg:args_so_far) fun
+ = do { (args, coi) <- loop (n_req - 1) (arg:args_so_far) fun
+ ; return (args, mkAppTyCoI fun coi arg IdCo)
+ }
loop n_req args_so_far (TyVarTy tv)
| isTyConableTyVar 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) }
- }
+ ; return (arg_tys ++ args_so_far, IdCo) }
+ }
+ | otherwise -- defer as tyvar may be refined by equalities
+ = defer
where
- mk_res_ty arg_tys' = mkTyConApp tc arg_tys'
(arg_kinds, res_kind) = splitKindFunTysN n_req (tyConKind tc)
- loop _ _ _ = boxySplitFailure (mkTyConApp tc (mkTyVarTys (tyConTyVars tc))) orig_ty
+ loop _ _ _ = boxySplitFailure (mkTyConApp tc (mkTyVarTys (tyConTyVars tc)))
+ orig_ty
+
+ -- defer splitting by generating an equality constraint
+ defer = boxySplitDefer arg_kinds mk_res_ty orig_ty
+ where
+ (arg_kinds, _) = splitKindFunTys (tyConKind tc)
+
+ -- apply splitted tycon to arguments
+ mk_res_ty = mkTyConApp tc
----------------------
-boxySplitListTy :: BoxyRhoType -> TcM BoxySigmaType -- Special case for lists
-boxySplitListTy exp_ty = do { [elt_ty] <- boxySplitTyConApp listTyCon exp_ty
- ; return elt_ty }
+boxySplitListTy :: BoxyRhoType -> TcM (BoxySigmaType, CoercionI)
+-- Special case for lists
+boxySplitListTy exp_ty
+ = do { ([elt_ty], coi) <- boxySplitTyConApp listTyCon exp_ty
+ ; return (elt_ty, coi) }
+----------------------
+boxySplitPArrTy :: BoxyRhoType -> TcM (BoxySigmaType, CoercionI)
+-- Special case for parrs
+boxySplitPArrTy exp_ty
+ = do { ([elt_ty], coi) <- boxySplitTyConApp parrTyCon exp_ty
+ ; return (elt_ty, coi) }
----------------------
boxySplitAppTy :: BoxyRhoType -- Type to split: m a
- -> TcM (BoxySigmaType, BoxySigmaType) -- Returns m, a
+ -> TcM ((BoxySigmaType, BoxySigmaType), -- Returns m, a
+ CoercionI)
-- If the incoming type is a mutable type variable of kind k, then
-- boxySplitAppTy returns a new type variable (m: * -> k); note the *.
-- If the incoming type is boxy, then so are the result types; and vice versa
loop ty
| Just (fun_ty, arg_ty) <- tcSplitAppTy_maybe ty
- = return (fun_ty, arg_ty)
+ = return ((fun_ty, arg_ty), IdCo)
+
+ loop ty@(TyConApp tycon _args)
+ | isOpenSynTyCon tycon -- try to normalise type family application
+ = do { (coi1, ty') <- tcNormaliseFamInst ty
+ ; case coi1 of
+ IdCo -> defer -- no progress, but maybe solvable => defer
+ ACo co -> -- progress: so lets try again
+ do { (args, coi2) <- loop ty'
+ ; return $ (args, coi2 `mkTransCoI` mkSymCoI coi1)
+ }
+ }
loop (TyVarTy tv)
| isTyConableTyVar 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) } }
+ Flexi -> do { [fun_ty, arg_ty] <- withMetaTvs tv kinds mk_res_ty
+ ; return ((fun_ty, arg_ty), IdCo) } }
+ | otherwise -- defer as tyvar may be refined by equalities
+ = defer
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
loop _ = boxySplitFailure (mkAppTy alphaTy betaTy) orig_ty
+ -- defer splitting by generating an equality constraint
+ defer = do { ([ty1, ty2], coi) <- boxySplitDefer arg_kinds mk_res_ty orig_ty
+ ; return ((ty1, ty2), coi)
+ }
+ where
+ orig_kind = typeKind orig_ty
+ arg_kinds = [mkArrowKind liftedTypeKind (defaultKind orig_kind),
+ -- m :: * -> k
+ liftedTypeKind] -- arg type :: *
+
+ -- build type application
+ mk_res_ty [fun_ty', arg_ty'] = mkAppTy fun_ty' arg_ty'
+ mk_res_ty _other = panic "TcUnify.mk_res_ty2"
+
------------------
boxySplitFailure actual_ty expected_ty
= unifyMisMatch False False actual_ty expected_ty
-- "outer" is False, so we don't pop the context
-- which is what we want since we have not pushed one!
+
+------------------
+boxySplitDefer :: [Kind] -- kinds of required arguments
+ -> ([TcType] -> TcTauType) -- construct lhs from argument tyvars
+ -> BoxyRhoType -- type to split
+ -> TcM ([TcType], CoercionI)
+boxySplitDefer kinds mkTy orig_ty
+ = do { tau_tys <- mapM newFlexiTyVarTy kinds
+ ; coi <- defer_unification False False (mkTy tau_tys) orig_ty
+ ; return (tau_tys, coi)
+ }
\end{code}
withBox :: Kind -> (BoxySigmaType -> TcM a) -> TcM (a, TcType)
-- Allocate a *boxy* tyvar
withBox kind thing_inside
- = do { box_tv <- newMetaTyVar BoxTv kind
+ = do { box_tv <- newBoxyTyVar kind
; res <- thing_inside (mkTyVarTy box_tv)
; ty <- {- pprTrace "with_box" (ppr (mkTyVarTy box_tv)) $ -} readFilledBox box_tv
; return (res, ty) }
All the tcSub calls have the form
- tcSub expected_ty offered_ty
+ tcSub actual_ty expected_ty
which checks
- offered_ty <= expected_ty
+ actual_ty <= expected_ty
-That is, that a value of type offered_ty is acceptable in
+That is, that a value of type actual_ty is acceptable in
a place expecting a value of type expected_ty.
It returns a coercion function
- co_fn :: offered_ty ~ expected_ty
-which takes an HsExpr of type offered_ty into one of type
+ co_fn :: actual_ty ~ expected_ty
+which takes an HsExpr of type actual_ty into one of type
expected_ty.
\begin{code}
-----------------
-tcSubExp :: BoxySigmaType -> BoxySigmaType -> TcM HsWrapper -- Locally used only
+tcSubExp :: InstOrigin -> BoxySigmaType -> BoxySigmaType -> TcM HsWrapper
-- (tcSub act exp) checks that
-- act <= exp
-tcSubExp actual_ty expected_ty
+tcSubExp orig actual_ty expected_ty
= -- 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"
-- 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
+ tc_sub orig actual_ty actual_ty False expected_ty expected_ty
-tcFunResTy :: Name -> BoxySigmaType -> BoxySigmaType -> TcM HsWrapper -- Locally used only
-tcFunResTy fun actual_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
-
-----------------
-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
+tc_sub :: InstOrigin
-> BoxySigmaType -- actual_ty, before expanding synonyms
-> BoxySigmaType -- ..and after
-> InBox -- True <=> expected_ty is inside a box
-- 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_sub orig act_sty act_ty exp_ib exp_sty exp_ty
= traceTc (text "tc_sub" <+> ppr act_ty $$ ppr exp_ty) >>
- tc_sub1 sub_ctxt act_sty act_ty exp_ib exp_sty exp_ty
+ tc_sub1 orig 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_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
+tc_sub1 orig act_sty act_ty exp_ib exp_sty exp_ty
+ | Just exp_ty' <- tcView exp_ty = tc_sub orig act_sty act_ty exp_ib exp_sty exp_ty'
+tc_sub1 orig act_sty act_ty exp_ib exp_sty exp_ty
+ | Just act_ty' <- tcView act_ty = tc_sub orig 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_sub1 sub_ctxt act_sty (TyVarTy tv) exp_ib exp_sty exp_ty
+tc_sub1 orig act_sty (TyVarTy tv) exp_ib exp_sty exp_ty
= do { traceTc (text "tc_sub1 - case 1")
- ; coi <- addSubCtxt sub_ctxt act_sty exp_sty $
+ ; coi <- addSubCtxt orig act_sty exp_sty $
uVar True False tv exp_ib exp_sty exp_ty
; traceTc (case coi of
IdCo -> text "tc_sub1 (Rule SBOXY) IdCo"
ACo co -> text "tc_sub1 (Rule SBOXY) ACo" <+> ppr co)
- ; return $ case coi of
- IdCo -> idHsWrapper
- ACo co -> WpCo co
+ ; return $ coiToHsWrapper coi
}
-----------------------------------
-- g :: Ord b => b->b
-- Consider f g !
-tc_sub1 sub_ctxt act_sty act_ty exp_ib exp_sty exp_ty
+tc_sub1 orig act_sty act_ty exp_ib exp_sty exp_ty
| isSigmaTy exp_ty
= do { traceTc (text "tc_sub1 - case 2") ;
if exp_ib then -- SKOL does not apply if exp_ty is inside a box
- defer_to_boxy_matching sub_ctxt act_sty act_ty exp_ib exp_sty exp_ty
+ defer_to_boxy_matching orig act_sty act_ty exp_ib exp_sty exp_ty
else 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
+ tc_sub orig act_sty act_ty False body_exp_ty body_exp_ty
; return (gen_fn <.> co_fn) }
}
where
-- expected_ty: Int -> Int
-- co_fn e = e Int dOrdInt
-tc_sub1 sub_ctxt act_sty actual_ty exp_ib exp_sty expected_ty
+tc_sub1 orig 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.)
; 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
+ ; co_fn2 <- tc_sub orig tau' tau' exp_ib exp_sty expected_ty
-- Deal with the dictionaries
- -- The origin gives a helpful origin when we have
- -- a function with type f :: Int -> forall a. Num a => ...
- -- This way the (Num a) dictionary gets an OccurrenceOf f origin
- ; let orig = case sub_ctxt of
- SubFun n -> OccurrenceOf n
- other -> InstSigOrigin -- Unhelpful
; co_fn1 <- instCall orig inst_tys (substTheta subst' theta)
; return (co_fn2 <.> co_fn1) }
-----------------------------------
-- Function case (rule F1)
-tc_sub1 sub_ctxt act_sty (FunTy act_arg act_res) exp_ib exp_sty (FunTy exp_arg exp_res)
+tc_sub1 orig act_sty (FunTy act_arg act_res) exp_ib exp_sty (FunTy exp_arg exp_res)
= do { traceTc (text "tc_sub1 - case 4")
- ; addSubCtxt sub_ctxt act_sty exp_sty $
- tc_sub_funs act_arg act_res exp_ib exp_arg exp_res
+ ; tc_sub_funs orig act_arg act_res exp_ib exp_arg exp_res
}
-- Function case (rule F2)
-tc_sub1 sub_ctxt act_sty act_ty@(FunTy act_arg act_res) _ exp_sty (TyVarTy exp_tv)
+tc_sub1 orig act_sty act_ty@(FunTy act_arg act_res) _ exp_sty (TyVarTy exp_tv)
| isBoxyTyVar exp_tv
- = addSubCtxt sub_ctxt act_sty exp_sty $
- do { traceTc (text "tc_sub1 - case 5")
+ = do { traceTc (text "tc_sub1 - case 5")
; cts <- readMetaTyVar exp_tv
; case cts of
- Indirect ty -> tc_sub SubDone act_sty act_ty True exp_sty ty
+ Indirect ty -> tc_sub orig 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 True arg_ty res_ty } }
+ ; tc_sub_funs orig 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_sub1 sub_ctxt act_sty actual_ty exp_ib exp_sty expected_ty@(TyVarTy exp_tv)
+tc_sub1 orig act_sty actual_ty exp_ib exp_sty expected_ty@(TyVarTy exp_tv)
= do { traceTc (text "tc_sub1 - case 6a" <+> ppr [isBoxyTyVar exp_tv, isMetaTyVar exp_tv, isSkolemTyVar exp_tv, isExistentialTyVar exp_tv,isSigTyVar exp_tv] )
- ; defer_to_boxy_matching sub_ctxt act_sty actual_ty exp_ib exp_sty expected_ty
+ ; defer_to_boxy_matching orig act_sty actual_ty exp_ib exp_sty expected_ty
}
-tc_sub1 sub_ctxt act_sty actual_ty exp_ib exp_sty expected_ty
+tc_sub1 orig act_sty actual_ty exp_ib exp_sty expected_ty
= do { traceTc (text "tc_sub1 - case 6")
- ; defer_to_boxy_matching sub_ctxt act_sty actual_ty exp_ib exp_sty expected_ty
+ ; defer_to_boxy_matching orig act_sty actual_ty exp_ib exp_sty expected_ty
}
-----------------------------------
-defer_to_boxy_matching sub_ctxt act_sty actual_ty exp_ib exp_sty expected_ty
- = do { coi <- addSubCtxt sub_ctxt act_sty exp_sty $
- u_tys outer False act_sty actual_ty exp_ib exp_sty expected_ty
- ; return $ case coi of
- IdCo -> idHsWrapper
- ACo co -> WpCo co
- }
- where
- outer = case sub_ctxt of -- Ugh
- SubDone -> False
- other -> True
+defer_to_boxy_matching orig act_sty actual_ty exp_ib exp_sty expected_ty
+ = do { coi <- addSubCtxt orig act_sty exp_sty $
+ u_tys True False act_sty actual_ty exp_ib exp_sty expected_ty
+ ; return $ coiToHsWrapper coi }
-----------------------------------
-tc_sub_funs act_arg act_res exp_ib exp_arg exp_res
- = do { arg_coi <- uTys False act_arg exp_ib exp_arg
- ; co_fn_res <- tc_sub SubDone act_res act_res exp_ib exp_res exp_res
+tc_sub_funs orig act_arg act_res exp_ib exp_arg exp_res
+ = do { arg_coi <- addSubCtxt orig act_arg exp_arg $
+ uTysOuter False act_arg exp_ib exp_arg
+ ; co_fn_res <- tc_sub orig act_res act_res exp_ib exp_res exp_res
; wrapper1 <- wrapFunResCoercion [exp_arg] co_fn_res
; let wrapper2 = case arg_coi of
IdCo -> idHsWrapper
ACo co -> WpCo $ FunTy co act_res
- ; return (wrapper1 <.> wrapper2)
- }
+ ; return (wrapper1 <.> wrapper2) }
-----------------------------------
wrapFunResCoercion
-- list of "free vars" for the signature check.
; loc <- getInstLoc (SigOrigin skol_info)
- ; dicts <- newDictBndrs loc theta'
+ ; dicts <- newDictBndrs loc theta' -- Includes equalities
; inst_binds <- tcSimplifyCheck loc tvs' dicts lie
; checkSigTyVarsWrt free_tvs tvs'
----------------
-- 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.
-addSubCtxt SubDone actual_res_ty expected_res_ty thing_inside
- = thing_inside
-addSubCtxt sub_ctxt actual_res_ty expected_res_ty thing_inside
+addSubCtxt orig actual_res_ty expected_res_ty thing_inside
= addErrCtxtM mk_err thing_inside
where
mk_err tidy_env
len_act_args = length act_args
len_exp_args = length exp_args
- 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''
+ message = case orig of
+ OccurrenceOf 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) }
wrongArgsCtxt too_many_or_few fun
-----------------------
unifyMisMatch outer swapped ty1 ty2
- = do { (env, msg) <- if swapped then misMatchMsg ty2 ty1
- else misMatchMsg ty1 ty2
-
- -- This is the whole point of the 'outer' stuff
- ; if outer then popErrCtxt (failWithTcM (env, msg))
- else failWithTcM (env, msg)
- }
+ | swapped = unifyMisMatch outer False ty2 ty1
+ | outer = popErrCtxt $ unifyMisMatch False swapped ty1 ty2 -- This is the whole point of the 'outer' stuff
+ | otherwise = failWithMisMatch ty1 ty2
\end{code}
projects / ghc-hetmet.git / blobdiff