- -- The expression has type: spec_ty -> expected_ty
-
-tcGen expected_ty extra_tvs thing_inside -- We expect expected_ty to be a forall-type
- -- If not, the call is a no-op
- = do { -- We want the GenSkol info in the skolemised type variables to
- -- mention the *instantiated* tyvar names, so that we get a
- -- good error message "Rigid variable 'a' is bound by (forall a. a->a)"
- -- Hence the tiresome but innocuous fixM
- ((tvs', theta', rho'), skol_info) <- fixM (\ ~(_, skol_info) ->
- do { (forall_tvs, theta, rho_ty) <- tcInstSkolType skol_info expected_ty
- -- Get loation from monad, not from expected_ty
- ; let skol_info = GenSkol forall_tvs (mkPhiTy theta rho_ty)
- ; return ((forall_tvs, theta, rho_ty), skol_info) })
-
-#ifdef DEBUG
- ; traceTc (text "tcGen" <+> vcat [text "extra_tvs" <+> ppr extra_tvs,
- text "expected_ty" <+> ppr expected_ty,
- text "inst ty" <+> ppr tvs' <+> ppr theta' <+> ppr rho',
- text "free_tvs" <+> ppr free_tvs])
-#endif
-
- -- Type-check the arg and unify with poly type
- ; (result, lie) <- getLIE (thing_inside tvs' rho')
-
- -- Check that the "forall_tvs" havn'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.
- -- Conclusion: include the free vars of the expected_ty in the
- -- list of "free vars" for the signature check.
-
- ; loc <- getInstLoc (SigOrigin skol_info)
- ; dicts <- newDictBndrs loc theta'
- ; inst_binds <- tcSimplifyCheck loc tvs' dicts lie
-
- ; checkSigTyVarsWrt free_tvs tvs'
- ; traceTc (text "tcGen:done")
-
- ; let
- -- The WpLet binds any Insts which came out of the simplification.
- dict_ids = map instToId dicts
- co_fn = mkWpTyLams tvs' <.> mkWpLams dict_ids <.> WpLet inst_binds
- ; returnM (co_fn, result) }
- where
- free_tvs = tyVarsOfType expected_ty `unionVarSet` extra_tvs
-\end{code}
+ -- The expression has type: spec_ty -> expected_ty
+
+tcGen skol_info extra_tvs
+ expected_ty thing_inside -- We expect expected_ty to be a forall-type
+ -- If not, the call is a no-op
+ = do { traceTc "tcGen" empty
+ ; (wrap, tvs', given, rho') <- deeplySkolemise skol_info expected_ty
+
+ ; when debugIsOn $
+ traceTc "tcGen" $ vcat [
+ text "expected_ty" <+> ppr expected_ty,
+ text "inst ty" <+> ppr tvs' <+> ppr rho' ]
+
+ -- In 'free_tvs' we must check that the "forall_tvs" havn'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.
+ -- Conclusion: pass the free vars of the expected_ty to checkConsraints
+ ; let free_tvs = tyVarsOfType expected_ty `unionVarSet` extra_tvs
+
+ ; (ev_binds, result) <- checkConstraints skol_info free_tvs tvs' given $
+ thing_inside tvs' rho'
+
+ ; return (wrap <.> mkWpLet ev_binds, result) }
+ -- The ev_binds returned by checkConstraints is very
+ -- often empty, in which case mkWpLet is a no-op
+
+checkConstraints :: SkolemInfo
+ -> TcTyVarSet -- Free variables (other than the type envt)
+ -- for the skolem escape check
+ -> [TcTyVar] -- Skolems
+ -> [EvVar] -- Given
+ -> TcM result
+ -> TcM (TcEvBinds, result)
+
+checkConstraints skol_info free_tvs skol_tvs given thing_inside
+ | null skol_tvs && null given
+ = do { res <- thing_inside; return (emptyTcEvBinds, res) }
+ -- Just for efficiency. We check every function argument with
+ -- tcPolyExpr, which uses tcGen and hence checkConstraints.
+
+ | otherwise
+ = do { (ev_binds, wanted, result) <- newImplication skol_info free_tvs
+ skol_tvs given thing_inside
+ ; emitConstraints wanted
+ ; return (ev_binds, result) }
+
+newImplication :: SkolemInfo -> TcTyVarSet -> [TcTyVar]
+ -> [EvVar] -> TcM result
+ -> TcM (TcEvBinds, WantedConstraints, result)
+newImplication skol_info free_tvs skol_tvs given thing_inside
+ = ASSERT2( all isTcTyVar skol_tvs, ppr skol_tvs )
+ ASSERT2( all isSkolemTyVar skol_tvs, ppr skol_tvs )
+ do { gbl_tvs <- tcGetGlobalTyVars
+ ; lcl_env <- getLclTypeEnv
+ ; let all_free_tvs = gbl_tvs `unionVarSet` free_tvs
+
+ ; (result, wanted) <- getConstraints $
+ setUntouchables all_free_tvs $
+ thing_inside
+
+ ; if isEmptyBag wanted && not (hasEqualities given)
+ -- Optimisation : if there are no wanteds, and the givens
+ -- are sufficiently simple, don't generate an implication
+ -- at all. Reason for the hasEqualities test:
+ -- we don't want to lose the "inaccessible alternative"
+ -- error check
+ then
+ return (emptyTcEvBinds, emptyWanteds, result)
+ else do
+ { ev_binds_var <- newTcEvBinds
+ ; loc <- getCtLoc skol_info
+ ; let implic = Implic { ic_env_tvs = all_free_tvs
+ , ic_env = lcl_env
+ , ic_skols = mkVarSet skol_tvs
+ , ic_scoped = panic "emitImplication"
+ , ic_given = given
+ , ic_wanted = wanted
+ , ic_binds = ev_binds_var
+ , ic_loc = loc }
+
+ ; return (TcEvBinds ev_binds_var, unitBag (WcImplic implic), result) } }
+\end{code}