-- Various unifications
unifyType, unifyTypeList, unifyTheta, unifyKind,
- -- Occurs check error
- typeExtraInfoMsg, emitMisMatchErr,
-
--------------------------------
-- Holes
tcInfer,
import HsSyn
import TypeRep
-import TcErrors ( typeExtraInfoMsg )
+import TcErrors ( typeExtraInfoMsg, unifyCtxt )
import TcMType
-import TcEnv
import TcIface
import TcRnMonad
import TcType
import ErrUtils
import BasicTypes
import Bag
+
+import Maybes ( allMaybes )
import Util
import Outputable
import FastString
-- 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
+ = do { (sk_wrap, inst_wrap)
+ <- tcGen skol_info ty_expected $ \ _ sk_rho -> do
{ (in_wrap, in_rho) <- deeplyInstantiate origin ty_actual
; coi <- unifyType in_rho sk_rho
; return (coiToHsWrapper coi <.> in_wrap) }
%************************************************************************
\begin{code}
-tcGen :: SkolemInfo -> TcTyVarSet -> TcType
+tcGen :: SkolemInfo -> TcType
-> ([TcTyVar] -> TcRhoType -> TcM result)
-> TcM (HsWrapper, result)
-- 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
+tcGen skol_info 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
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
+ -- Generally 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)
-- 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
+ --
+ -- However [Oct 10] now that the untouchables are a range of
+ -- TcTyVars, all tihs is handled automatically with no need for
+ -- extra faffing around
- ; (ev_binds, result) <- checkConstraints skol_info free_tvs tvs' given $
+ ; (ev_binds, result) <- checkConstraints skol_info tvs' given $
thing_inside tvs' rho'
; return (wrap <.> mkWpLet ev_binds, result) }
-- 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
+checkConstraints skol_info 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
+ = do { (ev_binds, wanted, result) <- newImplication skol_info
skol_tvs given thing_inside
; emitConstraints wanted
; return (ev_binds, result) }
-newImplication :: SkolemInfo -> TcTyVarSet -> [TcTyVar]
+newImplication :: SkolemInfo -> [TcTyVar]
-> [EvVar] -> TcM result
-> TcM (TcEvBinds, WantedConstraints, result)
-newImplication skol_info free_tvs skol_tvs given thing_inside
+newImplication skol_info 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
+ do { ((result, untch), wanted) <- captureConstraints $
+ captureUntouchables $
+ thing_inside
; if isEmptyBag wanted && not (hasEqualities given)
-- Optimisation : if there are no wanteds, and the givens
return (emptyTcEvBinds, emptyWanteds, result)
else do
{ ev_binds_var <- newTcEvBinds
+ ; lcl_env <- getLclTypeEnv
; loc <- getCtLoc skol_info
- ; let implic = Implic { ic_env_tvs = all_free_tvs
+ ; let implic = Implic { ic_untch = untch
, ic_env = lcl_env
, ic_skols = mkVarSet skol_tvs
, ic_scoped = panic "emitImplication"
; return (TcEvBinds ev_binds_var, unitBag (WcImplic implic), result) } }
\end{code}
-
%************************************************************************
%* *
Boxy unification
--------------
-- It is always safe to defer unification to the main constraint solver
-- See Note [Deferred unification]
-uType_defer origin ty1 ty2
+uType_defer (item : origin) ty1 ty2
= do { co_var <- newWantedCoVar ty1 ty2
; traceTc "utype_defer" (vcat [ppr co_var, ppr ty1, ppr ty2, ppr origin])
- ; loc <- getCtLoc TypeEqOrigin
+ ; loc <- getCtLoc (TypeEqOrigin item)
; wrapEqCtxt origin $
emitConstraint (WcEvVar (WantedEvVar co_var loc))
; return $ ACo $ mkTyVarTy co_var }
+uType_defer [] _ _
+ = panic "uType_defer"
--------------
-- Push a new item on the origin stack (the most common case)
-- Predicates
go origin (PredTy p1) (PredTy p2) = uPred origin p1 p2
- -- Functions; just check the two parts
+ -- Coercion functions: (t1a ~ t1b) => t1c ~ (t2a ~ t2b) => t2c
+ go origin ty1 ty2
+ | Just (t1a,t1b,t1c) <- splitCoPredTy_maybe ty1,
+ Just (t2a,t2b,t2c) <- splitCoPredTy_maybe ty2
+ = do { co1 <- uType origin t1a t2a
+ ; co2 <- uType origin t1b t2b
+ ; co3 <- uType origin t1c t2c
+ ; return $ mkCoPredCoI co1 co2 co3 }
+
+ -- Functions (or predicate functions) just check the two parts
go origin (FunTy fun1 arg1) (FunTy fun2 arg2)
= do { coi_l <- uType origin fun1 fun2
; coi_r <- uType origin arg1 arg2
; return $ mkAppTyCoI coi_s coi_t }
go _ ty1 ty2
- | isSigmaTy ty1 || isSigmaTy ty2
+ | tcIsForAllTy ty1 || tcIsForAllTy ty2
= unifySigmaTy origin ty1 ty2
-- Anything else fails
in_scope = mkInScopeSet (mkVarSet skol_tvs)
phi1 = substTy (mkTvSubst in_scope (zipTyEnv tvs1 tys)) body1
phi2 = substTy (mkTvSubst in_scope (zipTyEnv tvs2 tys)) body2
- untch = tyVarsOfType ty1 `unionVarSet` tyVarsOfType ty2
-
- ; (coi, lie) <- getConstraints $
- setUntouchables untch $
- uType origin phi1 phi2
+-- untch = tyVarsOfType ty1 `unionVarSet` tyVarsOfType ty2
+ ; ((coi, _untch), lie) <- captureConstraints $
+ captureUntouchables $
+ uType origin phi1 phi2
-- Check for escape; e.g. (forall a. a->b) ~ (forall a. a->a)
; let bad_lie = filterBag is_bad lie
is_bad w = any (`elemVarSet` tyVarsOfWanted w) skol_tvs
-- (checkTauTvUpdate tv ty)
-- We are about to update the TauTv tv with ty.
-- Check (a) that tv doesn't occur in ty (occurs check)
--- (b) that ty is a monotype
--- (c) that kind(ty) is a sub-kind of kind(tv)
+-- (b) that kind(ty) is a sub-kind of kind(tv)
+-- (c) that ty does not contain any type families, see Note [Type family sharing]
--
-- We have two possible outcomes:
-- (1) Return the type to update the type variable with,
checkTauTvUpdate tv ty
= do { ty' <- zonkTcType ty
- ; if not (tv `elemVarSet` tyVarsOfType ty')
- && typeKind ty' `isSubKind` tyVarKind tv
- then return (Just ty')
+ ; if typeKind ty' `isSubKind` tyVarKind tv then
+ case ok ty' of
+ Nothing -> return Nothing
+ Just ty'' -> return (Just ty'')
else return Nothing }
+
+ where ok :: TcType -> Maybe TcType
+ ok (TyVarTy tv') | not (tv == tv') = Just (TyVarTy tv')
+ ok this_ty@(TyConApp tc tys)
+ | not (isSynFamilyTyCon tc), Just tys' <- allMaybes (map ok tys)
+ = Just (TyConApp tc tys')
+ | isSynTyCon tc, Just ty_expanded <- tcView this_ty
+ = ok ty_expanded -- See Note [Type synonyms and the occur check]
+ ok (PredTy sty) | Just sty' <- ok_pred sty = Just (PredTy sty')
+ ok (FunTy arg res) | Just arg' <- ok arg, Just res' <- ok res
+ = Just (FunTy arg' res')
+ ok (AppTy fun arg) | Just fun' <- ok fun, Just arg' <- ok arg
+ = Just (AppTy fun' arg')
+ ok (ForAllTy tv1 ty1) | Just ty1' <- ok ty1 = Just (ForAllTy tv1 ty1')
+ -- Fall-through
+ ok _ty = Nothing
+
+ ok_pred (IParam nm ty) | Just ty' <- ok ty = Just (IParam nm ty')
+ ok_pred (ClassP cl tys)
+ | Just tys' <- allMaybes (map ok tys)
+ = Just (ClassP cl tys')
+ ok_pred (EqPred ty1 ty2)
+ | Just ty1' <- ok ty1, Just ty2' <- ok ty2
+ = Just (EqPred ty1' ty2')
+ -- Fall-through
+ ok_pred _pty = Nothing
+
\end{code}
+Note [Type synonyms and the occur check]
+~~~~~~~~~~~~~~~~~~~~
+Generally speaking we need to update a variable with type synonyms not expanded, which
+improves later error messages, except for when looking inside a type synonym may help resolve
+a spurious occurs check error. Consider:
+ type A a = ()
+
+ f :: (A a -> a -> ()) -> ()
+ f = \ _ -> ()
+
+ x :: ()
+ x = f (\ x p -> p x)
+
+We will eventually get a constraint of the form t ~ A t. The ok function above will
+properly expand the type (A t) to just (), which is ok to be unified with t. If we had
+unified with the original type A t, we would lead the type checker into an infinite loop.
+
+Hence, if the occurs check fails for a type synonym application, then (and *only* then),
+the ok function expands the synonym to detect opportunities for occurs check success using
+the underlying definition of the type synonym.
+
+The same applies later on in the constraint interaction code; see TcInteract,
+function @occ_check_ok@.
+
+
+Note [Type family sharing]
+~~~~~~~~~~~~~~
+We must avoid eagerly unifying type variables to types that contain function symbols,
+because this may lead to loss of sharing, and in turn, in very poor performance of the
+constraint simplifier. Assume that we have a wanted constraint:
+{
+ m1 ~ [F m2],
+ m2 ~ [F m3],
+ m3 ~ [F m4],
+ D m1,
+ D m2,
+ D m3
+}
+where D is some type class. If we eagerly unify m1 := [F m2], m2 := [F m3], m3 := [F m2],
+then, after zonking, our constraint simplifier will be faced with the following wanted
+constraint:
+{
+ D [F [F [F m4]]],
+ D [F [F m4]],
+ D [F m4]
+}
+which has to be flattened by the constraint solver. However, because the sharing is lost,
+an polynomially larger number of flatten skolems will be created and the constraint sets
+we are working with will be polynomially larger.
+
+Instead, if we defer the unifications m1 := [F m2], etc. we will only be generating three
+flatten skolems, which is the maximum possible sharing arising from the original constraint.
\begin{code}
data LookupTyVarResult -- The result of a lookupTcTyVar call
-- and, if there is more than one item, the "Expected/inferred" part
-- comes from the outermost item
wrapEqCtxt [] thing_inside = thing_inside
-wrapEqCtxt [_] thing_inside = thing_inside
wrapEqCtxt items thing_inside = addErrCtxtM (unifyCtxt (last items)) thing_inside
---------------
failWithMisMatch :: [EqOrigin] -> TcM a
-- Generate the message when two types fail to match,
-- going to some trouble to make it helpful.
--- The argument order is: actual type, expected type
-failWithMisMatch []
- = panic "failWithMisMatch"
-failWithMisMatch origin@(item:_)
+-- We take the failing types from the top of the origin stack
+-- rather than reporting the particular ones we are looking
+-- at right now
+failWithMisMatch (item:origin)
= wrapEqCtxt origin $
- emitMisMatchErr (uo_actual item) (uo_expected item)
-
-mkExpectedActualMsg :: Type -> Type -> SDoc
-mkExpectedActualMsg act_ty exp_ty
- = nest 2 (vcat [ text "Expected type" <> colon <+> ppr exp_ty,
- text " Actual type" <> colon <+> ppr act_ty ])
-
-emitMisMatchErr :: TcType -> TcType -> TcM a
-emitMisMatchErr ty_act ty_exp
- = do { ty_act <- zonkTcType ty_act
- ; ty_exp <- zonkTcType ty_exp
+ do { ty_act <- zonkTcType (uo_actual item)
+ ; ty_exp <- zonkTcType (uo_expected item)
; env0 <- tcInitTidyEnv
; let (env1, pp_exp) = tidyOpenType env0 ty_exp
(env2, pp_act) = tidyOpenType env1 ty_act
; failWithTcM (misMatchMsg env2 pp_act pp_exp) }
+failWithMisMatch []
+ = panic "failWithMisMatch"
misMatchMsg :: TidyEnv -> TcType -> TcType -> (TidyEnv, SDoc)
misMatchMsg env ty_act ty_exp
where
(env1, extra1) = typeExtraInfoMsg env ty_exp
(env2, extra2) = typeExtraInfoMsg env1 ty_act
-
---------------------
-unifyCtxt :: EqOrigin -> TidyEnv -> TcM (TidyEnv, SDoc)
-unifyCtxt (UnifyOrigin { uo_actual = act_ty, uo_expected = exp_ty }) tidy_env
- = do { act_ty' <- zonkTcType act_ty
- ; exp_ty' <- zonkTcType exp_ty
- ; let (env1, exp_ty'') = tidyOpenType tidy_env exp_ty'
- (env2, act_ty'') = tidyOpenType env1 act_ty'
- ; return (env2, mkExpectedActualMsg act_ty'' exp_ty'') }
\end{code}
-- The extra_tvs can include boxy type variables;
-- e.g. TcMatches.tcCheckExistentialPat
checkSigTyVarsWrt extra_tvs sig_tvs
- = do { extra_tvs' <- zonkTcTyVarsAndFV (varSetElems extra_tvs)
+ = do { extra_tvs' <- zonkTcTyVarsAndFV extra_tvs
; check_sig_tyvars extra_tvs' sig_tvs }
check_sig_tyvars
projects / ghc-hetmet.git / blobdiff