------------------------------------
--- 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
- = do { addSubCtxt sub_ctxt act_sty exp_sty $
- uVar True False tv exp_ib exp_sty exp_ty
- ; return idHsWrapper }
-
------------------------------------
--- 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
-
--- It is essential to do this *before* the specialisation case
--- Example: f :: (Eq a => a->a) -> ...
--- g :: Ord b => b->b
--- Consider f g !
-
-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
-
------------------------------------
--- Specialisation case (rule ASPEC):
--- actual_ty: forall a. Ord a => a->a
--- expected_ty: Int -> Int
--- co_fn e = e Int dOrdInt
-
-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 { -- 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_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_sub1 sub_ctxt 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 { cts <- readMetaTyVar exp_tv
- ; case cts of
- 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 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
- = 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_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 }