[Git][ghc/ghc][wip/T17775] Wibbles
Simon Peyton Jones
gitlab at gitlab.haskell.org
Thu Apr 30 01:07:39 UTC 2020
Simon Peyton Jones pushed to branch wip/T17775 at Glasgow Haskell Compiler / GHC
Commits:
a4249525 by Simon Peyton Jones at 2020-04-30T02:06:53+01:00
Wibbles
esp to tcPolyCheck
- - - - -
5 changed files:
- compiler/GHC/Tc/Gen/Bind.hs
- compiler/GHC/Tc/Gen/Expr.hs
- compiler/GHC/Tc/Gen/Sig.hs
- compiler/GHC/Tc/Utils/TcType.hs
- compiler/GHC/Tc/Utils/Unify.hs
Changes:
=====================================
compiler/GHC/Tc/Gen/Bind.hs
=====================================
@@ -697,7 +697,7 @@ tcPolyCheck prag_fn
; mono_name <- newNameAt (nameOccName name) nm_loc
; (wrap_gen, (wrap_res, matches'))
<- setSrcSpan sig_loc $ -- Sets the binding location for the skolems
- tcSkolemise ctxt (idType poly_id) $ \_ rho_ty ->
+ tcSkolemiseScoped ctxt (idType poly_id) $ \rho_ty ->
-- Unwraps multiple layers; e.g
-- f :: forall a. Eq a => forall b. Ord b => blah
-- NB: tcSkolemise makes fresh type variables
=====================================
compiler/GHC/Tc/Gen/Expr.hs
=====================================
@@ -1574,7 +1574,7 @@ tcSynArgE :: CtOrigin
-- ^ returns a wrapper :: (type of right shape) "->" (type passed in)
tcSynArgE orig sigma_ty syn_ty thing_inside
= do { (skol_wrap, (result, ty_wrapper))
- <- tcSkolemise GenSigCtxt sigma_ty $ \ _ rho_ty ->
+ <- tcSkolemise GenSigCtxt sigma_ty $ \ rho_ty ->
go rho_ty syn_ty
; return (result, skol_wrap <.> ty_wrapper) }
where
@@ -1726,22 +1726,10 @@ in the other order, the extra signature in f2 is reqd.
tcExprSig :: LHsExpr GhcRn -> TcIdSigInfo -> TcM (LHsExpr GhcTc, TcType)
tcExprSig expr (CompleteSig { sig_bndr = poly_id, sig_loc = loc })
= setSrcSpan loc $ -- Sets the location for the implication constraint
- do { (tv_prs, theta, tau) <- tcInstType tcInstSkolTyVars poly_id
- ; given <- newEvVars theta
- ; traceTc "tcExprSig: CompleteSig" $
- vcat [ text "poly_id:" <+> ppr poly_id <+> dcolon <+> ppr (idType poly_id)
- , text "tv_prs:" <+> ppr tv_prs ]
-
- ; let skol_info = SigSkol ExprSigCtxt (idType poly_id) tv_prs
- skol_tvs = map snd tv_prs
- ; (ev_binds, expr') <- checkConstraints skol_info skol_tvs given $
- tcExtendNameTyVarEnv tv_prs $
- tcCheckPolyExprNC expr tau
-
- ; let poly_wrap = mkWpTyLams skol_tvs
- <.> mkWpLams given
- <.> mkWpLet ev_binds
- ; return (mkLHsWrap poly_wrap expr', idType poly_id) }
+ do { let poly_ty = idType poly_id
+ ; (wrap, expr') <- tcSkolemiseScoped ExprSigCtxt poly_ty $ \rho_ty ->
+ tcCheckMonoExprNC expr rho_ty
+ ; return (mkLHsWrap wrap expr', poly_ty) }
tcExprSig expr sig@(PartialSig { psig_name = name, sig_loc = loc })
= setSrcSpan loc $ -- Sets the location for the implication constraint
=====================================
compiler/GHC/Tc/Gen/Sig.hs
=====================================
@@ -777,7 +777,7 @@ tcSpecWrapper :: UserTypeCtxt -> TcType -> TcType -> TcM HsWrapper
-- See Note [Handling SPECIALISE pragmas], wrinkle 1
tcSpecWrapper ctxt poly_ty spec_ty
= do { (sk_wrap, inst_wrap)
- <- tcSkolemise ctxt spec_ty $ \ _ spec_tau ->
+ <- tcSkolemise ctxt spec_ty $ \ spec_tau ->
do { (inst_wrap, tau) <- topInstantiate orig poly_ty
; _ <- unifyType Nothing spec_tau tau
-- Deliberately ignore the evidence
=====================================
compiler/GHC/Tc/Utils/TcType.hs
=====================================
@@ -1993,9 +1993,9 @@ isSigmaTy _ = False
isRhoTy :: TcType -> Bool -- True of TcRhoTypes; see Note [TcRhoType]
isRhoTy ty | Just ty' <- tcView ty = isRhoTy ty'
-isRhoTy (ForAllTy {}) = False
-isRhoTy (FunTy { ft_af = VisArg, ft_res = r }) = isRhoTy r
-isRhoTy _ = True
+isRhoTy (ForAllTy {}) = False
+isRhoTy (FunTy { ft_af = InvisArg }) = False
+isRhoTy _ = True
-- | Like 'isRhoTy', but also says 'True' for 'Infer' types
isRhoExpTy :: ExpType -> Bool
=====================================
compiler/GHC/Tc/Utils/Unify.hs
=====================================
@@ -14,7 +14,7 @@
module GHC.Tc.Utils.Unify (
-- Full-blown subsumption
tcWrapResult, tcWrapResultO, tcWrapResultMono,
- tcSkolemise, tcSkolemiseET,
+ tcSkolemise, tcSkolemiseScoped, tcSkolemiseET,
tcSubType, tcSubTypeSigma, tcSubTypePat,
checkConstraints, checkTvConstraints,
buildImplicationFor, buildTvImplication, emitResidualTvConstraint,
@@ -160,7 +160,7 @@ matchExpectedFunTys herald ctx arity orig_ty thing_inside
go acc_arg_tys n ty
| (tvs, theta, _) <- tcSplitSigmaTy ty
, not (null tvs && null theta)
- = do { (wrap_gen, (wrap_res, result)) <- tcSkolemise ctx ty $ \_ ty' ->
+ = do { (wrap_gen, (wrap_res, result)) <- tcSkolemise ctx ty $ \ty' ->
go acc_arg_tys n ty'
; return (wrap_gen <.> wrap_res, result) }
@@ -611,7 +611,7 @@ tc_sub_type unify inst_orig ctxt ty_actual ty_expected
, text "ty_expected =" <+> ppr ty_expected ]
; (sk_wrap, inner_wrap)
- <- tcSkolemise ctxt ty_expected $ \ _ sk_rho ->
+ <- tcSkolemise ctxt ty_expected $ \ sk_rho ->
do { (wrap, rho_a) <- topInstantiate inst_orig ty_actual
; cow <- unify rho_a sk_rho
; return (mkWpCastN cow <.> wrap) }
@@ -937,49 +937,53 @@ the thinking.
* *
********************************************************************* -}
--- | Take an "expected type" and strip off quantifiers to expose the
--- type underneath, binding the new skolems for the @thing_inside at .
--- The returned 'HsWrapper' has type @specific_ty -> expected_ty at .
-tcSkolemise :: UserTypeCtxt -> TcSigmaType
- -> ([TcTyVar] -> TcType -> TcM result)
- -- ^ These are only ever used for scoped type variables.
- -> TcM (HsWrapper, result)
- -- ^ The expression has type: spec_ty -> expected_ty
+{- Note [Skolemisation]
+~~~~~~~~~~~~~~~~~~~~~~~
+tcSkolemise takes "expected type" and strip off quantifiers to expose the
+type underneath, binding the new skolems for the 'thing_inside'
+The returned 'HsWrapper' has type (specific_ty -> expected_ty).
+
+Note:
+
+* tcSkolemiseScoped deals specially with just the outer forall,
+ because only the outer forall has type variables that scope
+ over the body
+
+-}
+
+tcSkolemise, tcSkolemiseScoped
+ :: UserTypeCtxt -> TcSigmaType
+ -> (TcType -> TcM result)
+ -> TcM (HsWrapper, result)
+ -- ^ The wrapper has type: spec_ty ~> expected_ty
+
+tcSkolemiseScoped ctxt expected_ty thing_inside
+ = do { (wrap, tv_prs, given, rho_ty) <- topSkolemise expected_ty
+ ; let skol_tvs = map snd tv_prs
+ skol_info = SigSkol ctxt expected_ty tv_prs
+
+ ; (ev_binds, res)
+ <- checkConstraints skol_info skol_tvs given $
+ tcExtendNameTyVarEnv tv_prs $
+ thing_inside rho_ty
+
+ ; return (wrap <.> mkWpLet ev_binds, res) }
tcSkolemise ctxt expected_ty thing_inside
-- We expect expected_ty to be a forall-type
-- If not, the call is a no-op
- = do { traceTc "tcSkolemise" Outputable.empty
- ; (wrap, tv_prs, given, rho') <- topSkolemise expected_ty
-
- ; lvl <- getTcLevel
- ; when debugIsOn $
- traceTc "tcSkolemise" $ vcat [
- ppr lvl,
- text "expected_ty" <+> ppr expected_ty,
- text "inst tyvars" <+> ppr tv_prs,
- text "given" <+> ppr given,
- text "inst type" <+> ppr rho' ]
-
- -- Generally we must check that the "forall_tvs" haven't been constrained
- -- The interesting bit here is that we must include the free variables
- -- of the expected_ty. Here's an example:
- -- runST (newVar True)
- -- Here, if we don't make a check, we'll get a type (ST s (MutVar s Bool))
- -- for (newVar True), with s fresh. Then we unify with the runST's arg type
- -- forall s'. ST s' a. That unifies s' with s, and a with MutVar s Bool.
- -- So now s' isn't unconstrained because it's linked to a.
- --
- -- However [Oct 10] now that the untouchables are a range of
- -- TcTyVars, all this is handled automatically with no need for
- -- extra faffing around
+ | isRhoTy expected_ty
+ = do { res <- thing_inside expected_ty
+ ; return (idHsWrapper, res) }
+ | otherwise
+ = do { (wrap, tv_prs, given, rho_ty) <- topSkolemise expected_ty
- ; let tvs' = map snd tv_prs
+ ; let skol_tvs = map snd tv_prs
skol_info = SigSkol ctxt expected_ty tv_prs
- ; (ev_binds, result) <- checkConstraints skol_info tvs' given $
- tcExtendNameTyVarEnv tv_prs $
- thing_inside tvs' rho'
+ ; (ev_binds, result)
+ <- checkConstraints skol_info skol_tvs given $
+ thing_inside rho_ty
; return (wrap <.> mkWpLet ev_binds, result) }
-- The ev_binds returned by checkConstraints is very
@@ -992,7 +996,8 @@ tcSkolemiseET :: UserTypeCtxt -> ExpSigmaType
tcSkolemiseET _ et@(Infer {}) thing_inside
= (idHsWrapper, ) <$> thing_inside et
tcSkolemiseET ctxt (Check ty) thing_inside
- = tcSkolemise ctxt ty $ \_ -> thing_inside . mkCheckExpType
+ = tcSkolemise ctxt ty $ \rho_ty ->
+ thing_inside (mkCheckExpType rho_ty)
checkConstraints :: SkolemInfo
-> [TcTyVar] -- Skolems
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/a4249525036262c9ecf52cbcdd9ad70304c53d57
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/a4249525036262c9ecf52cbcdd9ad70304c53d57
You're receiving this email because of your account on gitlab.haskell.org.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-commits/attachments/20200429/b3274abe/attachment-0001.html>
More information about the ghc-commits
mailing list