------------------
-tcSubExp :: BoxySigmaType -> BoxySigmaType -> TcM HsWrapper -- Locally used only
- -- (tcSub act exp) checks that
- -- act <= exp
-tcSubExp 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"
- -- Example is tcfail165:
- -- do var <- newEmptyMVar :: IO (MVar (forall a. Show a => a -> String))
- -- putMVar var (show :: forall a. Show a => a -> String)
- -- Here the info does not flow from the 'var' arg of putMVar to its 'show' arg
- -- but after zonking it looks as if it does!
- --
- -- 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
-
-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
- -> 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 sub_ctxt 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
- -- 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
-
------------------------------------
--- 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
- | isSigmaTy exp_ty
- = 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
- 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
- ; 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
- -- 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)
- = 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
- = defer_to_boxy_matching sub_ctxt act_sty actual_ty exp_ib exp_sty expected_ty