-tc_sub :: InstOrigin
- -> 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 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 orig act_sty act_ty exp_ib exp_sty exp_ty
- = traceTc (text "tc_sub" <+> ppr act_ty $$ ppr 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 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 orig act_sty (TyVarTy tv) exp_ib exp_sty exp_ty
- = do { traceTc (text "tc_sub1 - case 1")
- ; coi <- addSubCtxt orig act_sty exp_sty $
- uVar (Unify True act_sty exp_sty) 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 $ coiToHsWrapper coi
- }
-
------------------------------------
--- 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 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 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 orig 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 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.)
--- 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 { traceTc (text "tc_sub1 - case 3")
- ; -- 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 orig tau' tau' exp_ib exp_sty expected_ty
-
- -- Deal with the dictionaries
- ; co_fn1 <- instCall orig inst_tys (substTheta subst' theta)
- ; return (co_fn2 <.> co_fn1) }
-
------------------------------------
--- Function case (rule F1)
-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")
- ; tc_sub_funs orig act_arg act_res exp_ib exp_arg exp_res
- }
-
--- Function case (rule F2)
-tc_sub1 orig act_sty act_ty@(FunTy act_arg act_res) _ exp_sty (TyVarTy exp_tv)
- | isBoxyTyVar exp_tv
- = do { traceTc (text "tc_sub1 - case 5")
- ; cts <- readMetaTyVar exp_tv
- ; case cts of
- 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 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 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 orig 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 orig 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
- = do { coi <- addSubCtxt orig act_sty exp_sty $
- u_tys (Unify True act_sty exp_sty)
- False act_sty actual_ty exp_ib exp_sty expected_ty
- ; return $ coiToHsWrapper coi }
-
------------------------------------
-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 -> WpCast $ FunTy co act_res
- ; return (wrapper1 <.> wrapper2) }