subFunTys :: SDoc -- Something like "The function f has 3 arguments"
-- or "The abstraction (\x.e) takes 1 argument"
-> Arity -- Expected # of args
- -> BoxyRhoType -- res_ty
+ -> BoxySigmaType -- res_ty
+ -> Maybe UserTypeCtxt -- Whether res_ty arises from a user signature
+ -- Only relevant if we encounter a sigma-type
-> ([BoxySigmaType] -> BoxyRhoType -> TcM a)
-> TcM (HsWrapper, a)
-- Attempt to decompse res_ty to have enough top-level arrows to
-}
-subFunTys error_herald n_pats res_ty thing_inside
+subFunTys error_herald n_pats res_ty mb_ctxt thing_inside
= loop n_pats [] res_ty
where
-- In 'loop', the parameter 'arg_tys' accumulates
| isSigmaTy res_ty -- Do this before checking n==0, because we
-- guarantee to return a BoxyRhoType, not a
-- BoxySigmaType
- = do { (gen_fn, (co_fn, res)) <- tcGen res_ty emptyVarSet $ \ _ res_ty' ->
- loop n args_so_far res_ty'
+ = do { (gen_fn, (co_fn, res)) <- tcGen res_ty emptyVarSet mb_ctxt $ \ _ res_ty ->
+ loop n args_so_far res_ty
; return (gen_fn <.> co_fn, res) }
loop 0 args_so_far res_ty
Nothing -> orig_boxy_ty
Just ty -> ty `boxyLub` orig_boxy_ty
- go _ (TyVarTy tv) | isMetaTyVar tv
+ go _ (TyVarTy tv) | isTcTyVar tv && isMetaTyVar tv
+ -- NB: A TyVar (not TcTyVar) is possible here, representing
+ -- a skolem, because in this pure boxy_match function
+ -- we don't instantiate foralls to TcTyVars; cf Trac #2714
= subst -- Don't fail if the template has more info than the target!
-- Otherwise, with tmpl_tvs = [a], matching (a -> Int) ~ (Bool -> beta)
-- would fail to instantiate 'a', because the meta-type-variable
if exp_ib then -- SKOL does not apply if exp_ty is inside a box
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 ->
+ { (gen_fn, co_fn) <- tcGen exp_ty act_tvs Nothing $ \ _ body_exp_ty ->
tc_sub orig act_sty act_ty False body_exp_ty body_exp_ty
; return (gen_fn <.> co_fn) }
}
%************************************************************************
\begin{code}
-tcGen :: BoxySigmaType -- expected_ty
- -> TcTyVarSet -- Extra tyvars that the universally
- -- quantified tyvars of expected_ty
- -- must not be unified
+tcGen :: BoxySigmaType -- expected_ty
+ -> TcTyVarSet -- Extra tyvars that the universally
+ -- quantified tyvars of expected_ty
+ -- must not be unified
+ -> Maybe UserTypeCtxt -- Just ctxt => this polytype arose directly
+ -- from a user type sig
+ -- Nothing => a higher order situation
-> ([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
- -- If not, the call is a no-op
+tcGen expected_ty extra_tvs mb_ctxt thing_inside -- We expect expected_ty to be a forall-type
+ -- If not, the call is a no-op
= do { traceTc (text "tcGen")
- -- 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
- ; ((tvs', theta', rho'), skol_info) <- fixM (\ ~(_, skol_info) ->
- do { (forall_tvs, theta, rho_ty) <- tcInstSkolType skol_info expected_ty
- -- Get loation from monad, not from expected_ty
- ; let skol_info = GenSkol forall_tvs (mkPhiTy theta rho_ty)
- ; return ((forall_tvs, theta, rho_ty), skol_info) })
+ ; ((tvs', theta', rho'), skol_info) <- instantiate expected_ty
; when debugIsOn $
traceTc (text "tcGen" <+> vcat [
text "free_tvs" <+> ppr free_tvs])
-- Type-check the arg and unify with poly type
- ; (result, lie) <- getLIE (thing_inside tvs' rho')
+ ; (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
; return (co_fn, result) }
where
free_tvs = tyVarsOfType expected_ty `unionVarSet` extra_tvs
+
+ instantiate :: TcType -> TcM (([TcTyVar],ThetaType,TcRhoType), SkolemInfo)
+ instantiate expected_ty
+ | Just ctxt <- mb_ctxt -- This case split is the wohle reason for mb_ctxt
+ = do { let skol_info = SigSkol ctxt
+ ; stuff <- tcInstSigType True skol_info expected_ty
+ ; return (stuff, skol_info) }
+
+ | otherwise -- 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
+ = fixM $ \ ~(_, skol_info) ->
+ do { stuff@(forall_tvs, theta, rho_ty) <- tcInstSkolType skol_info expected_ty
+ -- Get loation from *monad*, not from expected_ty
+ ; let skol_info = GenSkol forall_tvs (mkPhiTy theta rho_ty)
+ ; return (stuff, skol_info) }
\end{code}
go outer _ (PredTy p1) _ (PredTy p2)
= uPred outer nb1 p1 nb2 p2
- -- Type constructors must match
+ -- Non-synonym type constructors must match
go _ _ (TyConApp con1 tys1) _ (TyConApp con2 tys2)
| con1 == con2 && not (isOpenSynTyCon con1)
= do { cois <- uTys_s nb1 tys1 nb2 tys2
; return $ mkTyConAppCoI con1 tys1 cois
}
- -- See Note [TyCon app]
+ -- Family synonyms See Note [TyCon app]
| con1 == con2 && identicalOpenSynTyConApp
= do { cois <- uTys_s nb1 tys1' nb2 tys2'
; return $ mkTyConAppCoI con1 tys1 (replicate n IdCo ++ cois)
identicalOpenSynTyConApp = idxTys1 `tcEqTypes` idxTys2
-- See Note [OpenSynTyCon app]
+ -- If we can reduce a family app => proceed with reduct
+ -- NB: We use isOpenSynTyCon, not isOpenSynTyConApp as we also must
+ -- defer oversaturated applications!
+ go outer sty1 ty1@(TyConApp con1 _) sty2 ty2
+ | isOpenSynTyCon con1
+ = do { (coi1, ty1') <- tcNormaliseFamInst ty1
+ ; case coi1 of
+ IdCo -> defer -- no reduction, see [Deferred Unification]
+ _ -> liftM (coi1 `mkTransCoI`) $ go outer sty1 ty1' sty2 ty2
+ }
+
+ -- If we can reduce a family app => proceed with reduct
+ -- NB: We use isOpenSynTyCon, not isOpenSynTyConApp as we also must
+ -- defer oversaturated applications!
+ go outer sty1 ty1 sty2 ty2@(TyConApp con2 _)
+ | isOpenSynTyCon con2
+ = do { (coi2, ty2') <- tcNormaliseFamInst ty2
+ ; case coi2 of
+ IdCo -> defer -- no reduction, see [Deferred Unification]
+ _ -> liftM (`mkTransCoI` mkSymCoI coi2) $
+ go outer sty1 ty1 sty2 ty2'
+ }
+
-- Functions; just check the two parts
go _ _ (FunTy fun1 arg1) _ (FunTy fun2 arg2)
= do { coi_l <- uTys nb1 fun1 nb2 fun2
; coi_t <- uTys nb1 t1 nb2 t2
; return $ mkAppTyCoI s1 coi_s t1 coi_t }
- -- One or both outermost constructors are type family applications.
- -- If we can normalise them away, proceed as usual; otherwise, we
- -- need to defer unification by generating a wanted equality constraint.
- go outer sty1 ty1 sty2 ty2
- | ty1_is_fun || ty2_is_fun
- = do { (coi1, ty1') <- if ty1_is_fun then tcNormaliseFamInst ty1
- else return (IdCo, ty1)
- ; (coi2, ty2') <- if ty2_is_fun then tcNormaliseFamInst ty2
- else return (IdCo, ty2)
- ; coi <- if isOpenSynTyConApp ty1' || isOpenSynTyConApp ty2'
- then do { -- One type family app can't be reduced yet
- -- => defer
- ; ty1'' <- zonkTcType ty1'
- ; ty2'' <- zonkTcType ty2'
- ; if tcEqType ty1'' ty2''
- then return IdCo
- else -- see [Deferred Unification]
- defer_unification outer False orig_ty1 orig_ty2
- }
- else -- unification can proceed
- go outer sty1 ty1' sty2 ty2'
- ; return $ coi1 `mkTransCoI` coi `mkTransCoI` (mkSymCoI coi2)
- }
- where
- ty1_is_fun = isOpenSynTyConApp ty1
- ty2_is_fun = isOpenSynTyConApp ty2
-
-- Anything else fails
go outer _ _ _ _ = bale_out outer
+ defer = defer_unification outer False orig_ty1 orig_ty2
+
+
----------
uPred :: Outer -> InBox -> PredType -> InBox -> PredType -> TcM CoercionI
uPred _ nb1 (IParam n1 t1) nb2 (IParam n2 t2)
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,
+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.
-- tv1 is an un-filled-in meta type variable (maybe boxy, maybe tau)
-- ty2 is not a type variable
-uMetaVar _ swapped tv1 BoxTv ref1 ps_ty2 _
+uMetaVar outer swapped tv1 BoxTv ref1 ps_ty2 ty2
= -- tv1 is a BoxTv. So we must unbox ty2, to ensure
-- that any boxes in ty2 are filled with monotypes
--
-- it does, the unbox operation will fill it, and the debug code
-- checks for that.
do { final_ty <- unBox ps_ty2
- ; when debugIsOn $ do
- { meta_details <- readMutVar ref1
- ; case meta_details of
- Indirect ty -> WARN( True, ppr tv1 <+> ppr ty )
- return () -- This really should *not* happen
- Flexi -> return ()
- }
- ; checkUpdateMeta swapped tv1 ref1 final_ty
- ; return IdCo
+ ; meta_details <- readMutVar ref1
+ ; case meta_details of
+ Indirect _ -> -- This *can* happen due to an occurs check,
+ -- just as it can in checkTauTvUpdate in the next
+ -- equation of uMetaVar; see Trac #2414
+ -- Note [Occurs check]
+ -- Go round again. Probably there's an immediate
+ -- error, but maybe not (a type function might discard
+ -- its argument). Next time round we'll end up in the
+ -- TauTv case of uMetaVar.
+ uVar outer swapped tv1 False ps_ty2 ty2
+ -- Setting for nb2::InBox is irrelevant
+
+ Flexi -> do { checkUpdateMeta swapped tv1 ref1 final_ty
+ ; return IdCo }
}
uMetaVar outer swapped tv1 _ ref1 ps_ty2 _
}
}
+{- Note [Occurs check]
+ ~~~~~~~~~~~~~~~~~~~
+An eager occurs check is made in checkTauTvUpdate, deferring tricky
+cases by calling defer_unification (see notes with
+checkTauTvUpdate). An occurs check can also (and does) happen in the
+BoxTv case, but unBox doesn't check for occurrences, and in any case
+doesn't have the type-function-related complexity that
+checkTauTvUpdate has. So we content ourselves with spotting the potential
+occur check (by the fact that tv1 is now filled), and going round again.
+Next time round we'll get the TauTv case of uMetaVar.
+-}
+
----------------
uUnfilledVars :: Outer
-> SwapFlag
-- (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 -> *) :=: ?? -> *
+-- What about (kv -> *) ~ ?? -> *
kindSimpleKind orig_swapped orig_kind
= go orig_swapped orig_kind
where
| otherwise = do
(_errs, mb_r) <- tryTc (unifyKind exp_kind act_kind)
case mb_r of
- Just _ -> return () ; -- Unification succeeded
+ Just _ -> return () -- Unification succeeded
Nothing -> do
-- So there's definitely an error
check_sig_tyvars _ []
= return ()
check_sig_tyvars extra_tvs sig_tvs
- = ASSERT( all isSkolemTyVar sig_tvs )
+ = ASSERT( all isTcTyVar sig_tvs && 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,