------------------
-tcSubExp :: BoxySigmaType -> BoxySigmaType -> TcM ExprCoFn -- Locally used only
- -- (tcSub act exp) checks that
- -- act <= exp
-tcSubExp actual_ty expected_ty
- = addErrCtxtM (unifyCtxt actual_ty expected_ty)
- (tc_sub True actual_ty actual_ty expected_ty expected_ty)
-
-tcFunResTy :: Name -> BoxySigmaType -> BoxySigmaType -> TcM ExprCoFn -- Locally used only
-tcFunResTy fun actual_ty expected_ty
- = addErrCtxtM (checkFunResCtxt fun actual_ty expected_ty) $
- (tc_sub True actual_ty actual_ty expected_ty expected_ty)
-
------------------
-tc_sub :: Outer -- See comments with uTys
- -> BoxySigmaType -- actual_ty, before expanding synonyms
- -> BoxySigmaType -- ..and after
- -> BoxySigmaType -- expected_ty, before
- -> BoxySigmaType -- ..and after
- -> TcM ExprCoFn
-
-tc_sub outer act_sty act_ty exp_sty exp_ty
- | Just exp_ty' <- tcView exp_ty = tc_sub False act_sty act_ty exp_sty exp_ty'
-tc_sub outer act_sty act_ty exp_sty exp_ty
- | Just act_ty' <- tcView act_ty = tc_sub False act_sty act_ty' 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_sub outer act_sty (TyVarTy tv) exp_sty exp_ty
- = do { uVar outer False tv False exp_sty exp_ty
- ; return idCoercion }
-
------------------------------------
--- 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_sub outer act_sty act_ty exp_sty exp_ty
- | isSigmaTy exp_ty
- = do { (gen_fn, co_fn) <- tcGen exp_ty act_tvs $ \ body_exp_ty ->
- tc_sub False act_sty act_ty 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_sub outer act_sty actual_ty 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 <- preSubType tyvars tau_tvs tau expected_ty
- ; let subst' = zipOpenTvSubst tyvars inst_tys
- tau' = substTy subst' tau
-
- -- Perform a full subsumption check
- ; co_fn <- tc_sub False tau' tau' exp_sty expected_ty
-
- -- Deal with the dictionaries
- ; dicts <- newDicts InstSigOrigin (substTheta subst' theta)
- ; extendLIEs dicts
- ; let inst_fn = CoApps (CoTyApps CoHole inst_tys)
- (map instToId dicts)
- ; return (co_fn <.> inst_fn) }
-
------------------------------------
--- Function case (rule F1)
-tc_sub _ _ (FunTy act_arg act_res) _ (FunTy exp_arg exp_res)
- = tc_sub_funs act_arg act_res exp_arg exp_res
-
--- Function case (rule F2)
-tc_sub outer act_sty act_ty@(FunTy act_arg act_res) exp_sty (TyVarTy exp_tv)
- | isBoxyTyVar exp_tv
- = do { cts <- readMetaTyVar exp_tv
- ; case cts of
- Indirect ty -> do { u_tys outer False act_sty act_ty True exp_sty ty
- ; return idCoercion }
- Flexi -> do { [arg_ty,res_ty] <- withMetaTvs exp_tv fun_kinds mk_res_ty
- ; tc_sub_funs act_arg act_res arg_ty res_ty } }
- where
- mk_res_ty [arg_ty', res_ty'] = mkFunTy arg_ty' res_ty'
- fun_kinds = [argTypeKind, openTypeKind]
-
--- Everything else: defer to boxy matching
-tc_sub outer act_sty actual_ty exp_sty expected_ty
- = do { u_tys outer False act_sty actual_ty False exp_sty expected_ty
- ; return idCoercion }
-
+tcSubType :: CtOrigin -> SkolemInfo -> TcSigmaType -> TcSigmaType -> TcM HsWrapper
+-- Check that ty_actual is more polymorphic than ty_expected
+-- Both arguments might be polytypes, so we must instantiate and skolemise
+-- Returns a wrapper of shape ty_actual ~ ty_expected
+tcSubType origin skol_info ty_actual ty_expected
+ | isSigmaTy ty_actual
+ = do { let extra_tvs = tyVarsOfType ty_actual
+ ; (sk_wrap, inst_wrap)
+ <- tcGen skol_info extra_tvs ty_expected $ \ _ sk_rho -> do
+ { (in_wrap, in_rho) <- deeplyInstantiate origin ty_actual
+ ; coi <- unifyType in_rho sk_rho
+ ; return (coiToHsWrapper coi <.> in_wrap) }
+ ; return (sk_wrap <.> inst_wrap) }
+
+ | otherwise -- Urgh! It seems deeply weird to have equality
+ -- when actual is not a polytype, and it makes a big
+ -- difference e.g. tcfail104
+ = do { coi <- unifyType ty_actual ty_expected
+ ; return (coiToHsWrapper coi) }
+
+tcInfer :: (TcType -> TcM a) -> TcM (a, TcType)
+tcInfer tc_infer = do { ty <- newFlexiTyVarTy openTypeKind
+ ; res <- tc_infer ty
+ ; return (res, ty) }