import HsSyn
import TypeRep
-
-import TcErrors ( typeExtraInfoMsg, unifyCtxt )
+import CoreUtils( mkPiTypes )
+import TcErrors ( unifyCtxt )
import TcMType
import TcIface
import TcRnMonad
import Name
import ErrUtils
import BasicTypes
-import Bag
import Maybes ( allMaybes )
import Util
%************************************************************************
All the tcSub calls have the form
-
tcSub actual_ty expected_ty
which checks
actual_ty <= expected_ty
expected_ty.
\begin{code}
-tcSubType :: CtOrigin -> SkolemInfo -> TcSigmaType -> TcSigmaType -> TcM HsWrapper
+tcSubType :: CtOrigin -> UserTypeCtxt -> 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
+tcSubType origin ctxt ty_actual ty_expected
| isSigmaTy ty_actual
= do { (sk_wrap, inst_wrap)
- <- tcGen skol_info ty_expected $ \ _ sk_rho -> do
+ <- tcGen ctxt 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 -> TcType
+tcGen :: UserTypeCtxt -> TcType
-> ([TcTyVar] -> TcRhoType -> TcM result)
-> TcM (HsWrapper, result)
-- The expression has type: spec_ty -> expected_ty
-tcGen skol_info expected_ty thing_inside
+tcGen ctxt 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
+ ; (wrap, tvs', given, rho') <- deeplySkolemise expected_ty
; when debugIsOn $
traceTc "tcGen" $ vcat [
-- 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 tihs is handled automatically with no need for
+ -- TcTyVars, all this is handled automatically with no need for
-- extra faffing around
+ -- Use the *instantiated* type in the SkolemInfo
+ -- so that the names of displayed type variables line up
+ ; let skol_info = SigSkol ctxt (mkPiTypes given rho')
+
; (ev_binds, result) <- checkConstraints skol_info tvs' given $
thing_inside tvs' rho'
captureUntouchables $
thing_inside
- ; if isEmptyBag wanted && not (hasEqualities given)
+ ; if isEmptyWC 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:
{ ev_binds_var <- newTcEvBinds
; lcl_env <- getLclTypeEnv
; loc <- getCtLoc skol_info
- ; let implic = Implic { ic_untch = untch
- , 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 }
-
- ; emitConstraint (WcImplic implic)
+ ; emitImplication $ Implic { ic_untch = untch
+ , ic_env = lcl_env
+ , ic_skols = mkVarSet skol_tvs
+ , ic_given = given
+ , ic_wanted = wanted
+ , ic_insol = insolubleWC wanted
+ , ic_binds = ev_binds_var
+ , ic_loc = loc }
+
; return (TcEvBinds ev_binds_var, result) } }
\end{code}
-- It is always safe to defer unification to the main constraint solver
-- See Note [Deferred unification]
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])
+ = wrapEqCtxt origin $
+ do { co_var <- newCoVar ty1 ty2
; loc <- getCtLoc (TypeEqOrigin item)
- ; wrapEqCtxt origin $
- emitConstraint (WcEvVar (WantedEvVar co_var loc))
+ ; emitFlat (mkEvVarX co_var loc)
+
+ -- Error trace only
+ ; ctxt <- getErrCtxt
+ ; doc <- mkErrInfo emptyTidyEnv ctxt
+ ; traceTc "utype_defer" (vcat [ppr co_var, ppr ty1, ppr ty2, ppr origin, doc])
+
; return $ ACo $ mkTyVarTy co_var }
uType_defer [] _ _
= panic "uType_defer"
= do { traceTc "u_tys " $ vcat
[ sep [ ppr orig_ty1, text "~", ppr orig_ty2]
, ppr origin]
- ; coi <- go origin orig_ty1 orig_ty2
+ ; coi <- go orig_ty1 orig_ty2
; case coi of
ACo co -> traceTc "u_tys yields coercion:" (ppr co)
IdCo _ -> traceTc "u_tys yields no coercion" empty
bale_out :: [EqOrigin] -> TcM a
bale_out origin = failWithMisMatch origin
- go :: [EqOrigin] -> TcType -> TcType -> TcM CoercionI
+ go :: TcType -> TcType -> TcM CoercionI
-- The arguments to 'go' are always semantically identical
-- to orig_ty{1,2} except for looking through type synonyms
-- Note that we pass in *original* (before synonym expansion),
-- so that type variables tend to get filled in with
-- the most informative version of the type
- go origin (TyVarTy tyvar1) ty2 = uVar origin NotSwapped tyvar1 ty2
- go origin ty1 (TyVarTy tyvar2) = uVar origin IsSwapped tyvar2 ty1
+ go (TyVarTy tyvar1) ty2 = uVar origin NotSwapped tyvar1 ty2
+ go ty1 (TyVarTy tyvar2) = uVar origin IsSwapped tyvar2 ty1
-- Expand synonyms:
-- see Note [Unification and synonyms]
-- Do this after the variable case so that we tend to unify
- -- variables with un-expended type synonym
- go origin ty1 ty2
- | Just ty1' <- tcView ty1 = uType origin ty1' ty2
- | Just ty2' <- tcView ty2 = uType origin ty1 ty2'
+ -- variables with un-expanded type synonym
+ --
+ -- Also NB that we recurse to 'go' so that we don't push a
+ -- new item on the origin stack. As a result if we have
+ -- type Foo = Int
+ -- and we try to unify Foo ~ Bool
+ -- we'll end up saying "can't match Foo with Bool"
+ -- rather than "can't match "Int with Bool". See Trac #4535.
+ go ty1 ty2
+ | Just ty1' <- tcView ty1 = go ty1' ty2
+ | Just ty2' <- tcView ty2 = go ty1 ty2'
+
-- Predicates
- go origin (PredTy p1) (PredTy p2) = uPred origin p1 p2
+ go (PredTy p1) (PredTy p2) = uPred origin p1 p2
-- Coercion functions: (t1a ~ t1b) => t1c ~ (t2a ~ t2b) => t2c
- go origin ty1 ty2
+ go ty1 ty2
| Just (t1a,t1b,t1c) <- splitCoPredTy_maybe ty1,
Just (t2a,t2b,t2c) <- splitCoPredTy_maybe ty2
= do { co1 <- uType origin t1a t2a
; return $ mkCoPredCoI co1 co2 co3 }
-- Functions (or predicate functions) just check the two parts
- go origin (FunTy fun1 arg1) (FunTy fun2 arg2)
+ go (FunTy fun1 arg1) (FunTy fun2 arg2)
= do { coi_l <- uType origin fun1 fun2
; coi_r <- uType origin arg1 arg2
; return $ mkFunTyCoI coi_l coi_r }
-- Always defer if a type synonym family (type function)
-- is involved. (Data families behave rigidly.)
- go origin ty1@(TyConApp tc1 _) ty2
+ go ty1@(TyConApp tc1 _) ty2
| isSynFamilyTyCon tc1 = uType_defer origin ty1 ty2
- go origin ty1 ty2@(TyConApp tc2 _)
+ go ty1 ty2@(TyConApp tc2 _)
| isSynFamilyTyCon tc2 = uType_defer origin ty1 ty2
- go origin (TyConApp tc1 tys1) (TyConApp tc2 tys2)
+ go (TyConApp tc1 tys1) (TyConApp tc2 tys2)
| tc1 == tc2 -- See Note [TyCon app]
= do { cois <- uList origin uType tys1 tys2
; return $ mkTyConAppCoI tc1 cois }
-- See Note [Care with type applications]
- go origin (AppTy s1 t1) ty2
+ go (AppTy s1 t1) ty2
| Just (s2,t2) <- tcSplitAppTy_maybe ty2
= do { coi_s <- uType_np origin s1 s2 -- See Note [Unifying AppTy]
; coi_t <- uType origin t1 t2
; return $ mkAppTyCoI coi_s coi_t }
- go origin ty1 (AppTy s2 t2)
+ go ty1 (AppTy s2 t2)
| Just (s1,t1) <- tcSplitAppTy_maybe ty1
= do { coi_s <- uType_np origin s1 s2
; coi_t <- uType origin t1 t2
; return $ mkAppTyCoI coi_s coi_t }
- go _ ty1 ty2
+ go ty1 ty2
| tcIsForAllTy ty1 || tcIsForAllTy ty2
= unifySigmaTy origin ty1 ty2
-- Anything else fails
- go origin _ _ = bale_out origin
+ go _ _ = bale_out origin
unifySigmaTy :: [EqOrigin] -> TcType -> TcType -> TcM CoercionI
unifySigmaTy origin ty1 ty2
= do { let (tvs1, body1) = tcSplitForAllTys ty1
(tvs2, body2) = tcSplitForAllTys ty2
; unless (equalLength tvs1 tvs2) (failWithMisMatch origin)
- ; skol_tvs <- tcInstSkolTyVars UnkSkol tvs1 -- Not a helpful SkolemInfo
+ ; skol_tvs <- tcInstSkolTyVars tvs1
-- Get location from monad, not from tvs1
; let tys = mkTyVarTys skol_tvs
in_scope = mkInScopeSet (mkVarSet skol_tvs)
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
- ; when (not (isEmptyBag bad_lie))
+ -- VERY UNSATISFACTORY; the constraint might be fine, but
+ -- we fail eagerly because we don't have any place to put
+ -- the bindings from an implication constraint
+ -- This only works because most constraints get solved on the fly
+ -- See Note [Avoid deferring]
+ ; when (any (`elemVarSet` tyVarsOfWC lie) skol_tvs)
(failWithMisMatch origin) -- ToDo: give details from bad_lie
; emitConstraints lie
Just ty2' -> updateMeta tv1 ref1 ty2'
}
- _other -> do { traceTc "Skolem defer" (ppr tv1); defer } -- Skolems of all sorts
+ _other -> do { traceTc "Skolem defer" (ppr tv1); defer } -- Skolems of all sorts
where
- defer = unSwap swapped (uType_defer origin) (mkTyVarTy tv1) non_var_ty2
+ defer | Just ty2' <- tcView non_var_ty2 -- Note [Avoid deferring]
+ -- non_var_ty2 isn't expanded yet
+ = uUnfilledVar origin swapped tv1 details1 ty2'
+ | otherwise
+ = unSwap swapped (uType_defer origin) (mkTyVarTy tv1) non_var_ty2
-- Occurs check or an untouchable: just defer
-- NB: occurs check isn't necessarily fatal:
-- eg tv1 occured in type family parameter
ty1 = mkTyVarTy tv1
ty2 = mkTyVarTy tv2
- nicer_to_update_tv1 _ (SigTv _) = True
- nicer_to_update_tv1 (SigTv _) _ = False
+ nicer_to_update_tv1 _ SigTv = True
+ nicer_to_update_tv1 SigTv _ = False
nicer_to_update_tv1 _ _ = isSystemName (Var.varName tv1)
-- Try not to update SigTvs; and try to update sys-y type
-- variables in preference to ones gotten (say) by
= Just (EqPred ty1' ty2')
-- Fall-through
ok_pred _pty = Nothing
-
\end{code}
+Note [Avoid deferring]
+~~~~~~~~~~~~~~~~~~~~~~
+We try to avoid creating deferred constraints for two reasons.
+ * First, efficiency.
+ * Second, currently we can only defer some constraints
+ under a forall. See unifySigmaTy.
+So expanding synonyms here is a good thing to do. Example (Trac #4917)
+ a ~ Const a b
+where type Const a b = a. We can solve this immediately, even when
+'a' is a skolem, just by expanding the synonym; and we should do so
+ in case this unification happens inside unifySigmaTy (sigh).
+
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:
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Generally speaking we try to update a variable with type synonyms not
+expanded, which improves later error messages, unless looking
+inside a type synonym may help resolve a spurious occurs check
+error. Consider:
type A a = ()
f :: (A a -> a -> ()) -> ()
Indirect ty -> return (Filled ty)
Flexi -> do { is_untch <- isUntouchable tyvar
; let -- Note [Unifying untouchables]
- ret_details | is_untch = SkolemTv UnkSkol
+ ret_details | is_untch = vanillaSkolemTv
| otherwise = details
; return (Unfilled ret_details) } }
| otherwise
; env0 <- tcInitTidyEnv
; let (env1, pp_exp) = tidyOpenType env0 ty_exp
(env2, pp_act) = tidyOpenType env1 ty_act
- ; failWithTcM (misMatchMsg env2 pp_act pp_exp) }
+ ; failWithTcM (env2, misMatchMsg pp_act pp_exp) }
failWithMisMatch []
= panic "failWithMisMatch"
-misMatchMsg :: TidyEnv -> TcType -> TcType -> (TidyEnv, SDoc)
-misMatchMsg env ty_act ty_exp
- = (env2, sep [sep [ ptext (sLit "Couldn't match expected type") <+> quotes (ppr ty_exp)
- , nest 12 $ ptext (sLit "with actual type") <+> quotes (ppr ty_act)]
- , nest 2 (extra1 $$ extra2) ])
- where
- (env1, extra1) = typeExtraInfoMsg env ty_exp
- (env2, extra2) = typeExtraInfoMsg env1 ty_act
+misMatchMsg :: TcType -> TcType -> SDoc
+misMatchMsg ty_act ty_exp
+ = sep [ ptext (sLit "Couldn't match expected type") <+> quotes (ppr ty_exp)
+ , nest 12 $ ptext (sLit "with actual type") <+> quotes (ppr ty_act)]
\end{code}
projects / ghc-hetmet.git / blobdiff