Commit 3f5673f3 authored by Simon Peyton Jones's avatar Simon Peyton Jones

A collection of type-inference refactorings.

This patch does a raft of useful tidy-ups in the type checker.
I've been meaning to do this for some time, and finally made
time to do it en route to ICFP.

1. Modify TcType.ExpType to make a distinct data type,
   InferResult for the Infer case, and consequential
   refactoring.

2. Define a new function TcUnify.fillInferResult, to fill in
   an InferResult. It uses TcMType.promoteTcType to promote
   the type to the level of the InferResult.
   See TcMType Note [Promoting a type]
   This refactoring is in preparation for an improvement
   to typechecking pattern bindings, coming next.

   I flirted with an elaborate scheme to give better
   higher rank inference, but it was just too complicated.
   See TcMType Note [Promotion and higher rank types]

3. Add to InferResult a new field ir_inst :: Bool to say
   whether or not the type used to fill in the
   InferResult should be deeply instantiated.  See
   TcUnify Note [Deep instantiation of InferResult].

4. Add a TcLevel to SkolemTvs. This will be useful generally

    - it's a fast way to see if the type
      variable escapes when floating (not used yet)

    - it provides a good consistency check when updating a
      unification variable (TcMType.writeMetaTyVarRef, the
      level_check_ok check)

   I originally had another reason (related to the flirting
   in (2), but I left it in because it seems like a step in
   the right direction.

5. Reduce and simplify the plethora of uExpType,
   tcSubType and related functions in TcUnify.  It was
   such an opaque mess and it's still not great, but it's
   better.

6. Simplify the uo_expected field of TypeEqOrigin.  Richard
   had generatlised it to a ExpType, but it was almost always
   a Check type.  Now it's back to being a plain TcType which
   is much, much easier.

7. Improve error messages by refraining from skolemisation when
   it's clear that there's an error: see
   TcUnify Note [Don't skolemise unnecessarily]

8. Type.isPiTy and isForAllTy seem to be missing a coreView check,
   so I added it

9. Kill off tcs_used_tcvs.  Its purpose is to track the
   givens used by wanted constraints.  For dictionaries etc
   we do that via the free vars of the /bindings/ in the
   implication constraint ic_binds.  But for coercions we
   just do update-in-place in the type, rather than
   generating a binding.  So we need something analogous to
   bindings, to track what coercions we have added.

   That was the purpose of tcs_used_tcvs.  But it only
   worked for a /single/ iteration, whereas we may have
   multiple iterations of solving an implication.  Look
   at (the old) 'setImplicationStatus'.  If the constraint
   is unsolved, it just drops the used_tvs on the floor.
   If it becomes solved next time round, we'll pick up
   coercions used in that round, but ignore ones used in
   the first round.

   There was an outright bug.  Result = (potentialy) bogus
   unused-constraint errors.  Constructing a case where this
   actually happens seems quite trick so I did not do so.

   Solution: expand EvBindsVar to include the (free vars of
   the) coercions, so that the coercions are tracked in
   essentially the same way as the bindings.

   This turned out to be much simpler.  Less code, more
   correct.

10. Make the ic_binds field in an implication have type
      ic_binds :: EvBindsVar
    instead of (as previously)
       ic_binds :: Maybe EvBindsVar
    This is notably simpler, and faster to use -- less
    testing of the Maybe.  But in the occaional situation
    where we don't have anywhere to put the bindings, the
    belt-and-braces error check is lost.  So I put it back
    as an ASSERT in 'setImplicationStatus' (see the use of
    'termEvidenceAllowed')

All these changes led to quite bit of error message wibbling
parent d61c7e8d
......@@ -1218,7 +1218,7 @@ zonkRttiType = zonkTcTypeToType (mkEmptyZonkEnv zonk_unbound_meta)
where
zonk_unbound_meta tv
= ASSERT( isTcTyVar tv )
do { tv' <- skolemiseUnboundMetaTyVar tv RuntimeUnk
do { tv' <- skolemiseRuntimeUnk tv
-- This is where RuntimeUnks are born:
-- otherwise-unconstrained unification variables are
-- turned into RuntimeUnks as they leave the
......
......@@ -225,7 +225,7 @@ deeplyInstantiate :: CtOrigin -> TcSigmaType -> TcM (HsWrapper, TcRhoType)
-- if deeplyInstantiate ty = (wrap, rho)
-- and e :: ty
-- then wrap e :: rho
-- That is, wrap :: ty "->" rho
-- That is, wrap :: ty ~> rho
deeplyInstantiate orig ty
| Just (arg_tys, tvs, theta, rho) <- tcDeepSplitSigmaTy_maybe ty
......@@ -381,7 +381,7 @@ tcInstBinderX _ subst (Anon ty)
-- This is the *only* constraint currently handled in types.
| Just (mk, role, k1, k2) <- get_pred_tys_maybe substed_ty
= do { let origin = TypeEqOrigin { uo_actual = k1
, uo_expected = mkCheckExpType k2
, uo_expected = k2
, uo_thing = Nothing }
; co <- case role of
Nominal -> unifyKind noThing k1 k2
......
......@@ -33,7 +33,6 @@ import TcEvidence
import TcHsType
import TcPat
import TcMType
import Inst( deeplyInstantiate )
import FamInstEnv( normaliseType )
import FamInst( tcGetFamInstEnvs )
import TyCon
......@@ -741,7 +740,7 @@ mkExport prag_fn qtvs theta
-- an ambiguouse type and have AllowAmbiguousType
-- e..g infer x :: forall a. F a -> Int
else addErrCtxtM (mk_impedence_match_msg mono_info sel_poly_ty poly_ty) $
tcSubType_NC sig_ctxt sel_poly_ty (mkCheckExpType poly_ty)
tcSubType_NC sig_ctxt sel_poly_ty poly_ty
; warn_missing_sigs <- woptM Opt_WarnMissingLocalSignatures
; when warn_missing_sigs $
......@@ -1117,58 +1116,6 @@ for a non-overloaded function.
@tcMonoBinds@ deals with a perhaps-recursive group of HsBinds.
The signatures have been dealt with already.
Note [Pattern bindings]
~~~~~~~~~~~~~~~~~~~~~~~
The rule for typing pattern bindings is this:
..sigs..
p = e
where 'p' binds v1..vn, and 'e' may mention v1..vn,
typechecks exactly like
..sigs..
x = e -- Inferred type
v1 = case x of p -> v1
..
vn = case x of p -> vn
Note that
(f :: forall a. a -> a) = id
should not typecheck because
case id of { (f :: forall a. a->a) -> f }
will not typecheck.
Note [Instantiate when inferring a type]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider
f = (*)
As there is no incentive to instantiate the RHS, tcMonoBinds will
produce a type of forall a. Num a => a -> a -> a for `f`. This will then go
through simplifyInfer and such, remaining unchanged.
There are two problems with this:
1) If the definition were `g _ = (*)`, we get a very unusual type of
`forall {a}. a -> forall b. Num b => b -> b -> b` for `g`. This is
surely confusing for users.
2) The monomorphism restriction can't work. The MR is dealt with in
simplifyInfer, and simplifyInfer has no way of instantiating. This
could perhaps be worked around, but it may be hard to know even
when instantiation should happen.
There is an easy solution to both problems: instantiate (deeply) when
inferring a type. So that's what we do. Note that this decision is
user-facing.
We do this deep instantiation in tcMonoBinds, in the FunBind case
only, and only when we do not have a type signature. Conveniently,
the fun_co_fn field of FunBind gives a place to record the coercion.
We do not need to do this
* for PatBinds, because we don't have a function type
* for FunBinds where we have a signature, bucause we aren't doing inference
-}
data MonoBindInfo = MBI { mbi_poly_name :: Name
......@@ -1193,27 +1140,21 @@ tcMonoBinds is_rec sig_fn no_gen
-- e.g. f = \(x::forall a. a->a) -> <body>
-- We want to infer a higher-rank type for f
setSrcSpan b_loc $
do { rhs_ty <- newOpenInferExpType
; (co_fn, matches')
<- tcExtendIdBndrs [TcIdBndr_ExpType name rhs_ty NotTopLevel] $
do { ((co_fn, matches'), rhs_ty)
<- tcInferInst $ \ exp_ty ->
-- tcInferInst: see TcUnify,
-- Note [Deep instantiation of InferResult]
tcExtendIdBndrs [TcIdBndr_ExpType name exp_ty NotTopLevel] $
-- We extend the error context even for a non-recursive
-- function so that in type error messages we show the
-- type of the thing whose rhs we are type checking
tcMatchesFun (L nm_loc name) matches rhs_ty
; rhs_ty <- readExpType rhs_ty
-- Deeply instantiate the inferred type
-- See Note [Instantiate when inferring a type]
; let orig = matchesCtOrigin matches
; rhs_ty <- zonkTcType rhs_ty -- NB: zonk to uncover any foralls
; (inst_wrap, rhs_ty) <- addErrCtxtM (instErrCtxt name rhs_ty) $
deeplyInstantiate orig rhs_ty
tcMatchesFun (L nm_loc name) matches exp_ty
; mono_id <- newLetBndr no_gen name rhs_ty
; return (unitBag $ L b_loc $
FunBind { fun_id = L nm_loc mono_id,
fun_matches = matches', bind_fvs = fvs,
fun_co_fn = inst_wrap <.> co_fn, fun_tick = [] },
fun_co_fn = co_fn, fun_tick = [] },
[MBI { mbi_poly_name = name
, mbi_sig = Nothing
, mbi_mono_id = mono_id }]) }
......@@ -1297,7 +1238,7 @@ tcLhs sig_fn no_gen (PatBind { pat_lhs = pat, pat_rhs = grhss })
-- See Note [Existentials in pattern bindings]
; ((pat', nosig_mbis), pat_ty)
<- addErrCtxt (patMonoBindsCtxt pat grhss) $
tcInferInst $ \ exp_ty ->
tcInferNoInst $ \ exp_ty ->
tcLetPat inst_sig_fun no_gen pat exp_ty $
mapM lookup_info nosig_names
......@@ -1761,16 +1702,3 @@ patMonoBindsCtxt :: (OutputableBndrId id, Outputable body)
patMonoBindsCtxt pat grhss
= hang (text "In a pattern binding:") 2 (pprPatBind pat grhss)
instErrCtxt :: Name -> TcType -> TidyEnv -> TcM (TidyEnv, SDoc)
instErrCtxt name ty env
= do { let (env', ty') = tidyOpenType env ty
; return (env', hang (text "When instantiating" <+> quotes (ppr name) <>
text ", initially inferred to have" $$
text "this overly-general type:")
2 (ppr ty') $$
extra) }
where
extra = sdocWithDynFlags $ \dflags ->
ppWhen (xopt LangExt.MonomorphismRestriction dflags) $
text "NB: This instantiation can be caused by the" <+>
text "monomorphism restriction."
......@@ -142,9 +142,11 @@ reportUnsolved wanted
| warn_out_of_scope = HoleWarn
| otherwise = HoleDefer
; report_unsolved (Just binds_var) False type_errors expr_holes
; report_unsolved binds_var False type_errors expr_holes
type_holes out_of_scope_holes wanted
; getTcEvBinds binds_var }
; ev_binds <- getTcEvBindsMap binds_var
; return (evBindMapBinds ev_binds)}
-- | Report *all* unsolved goals as errors, even if -fdefer-type-errors is on
-- However, do not make any evidence bindings, because we don't
......@@ -155,17 +157,21 @@ reportUnsolved wanted
-- and for simplifyDefault.
reportAllUnsolved :: WantedConstraints -> TcM ()
reportAllUnsolved wanted
= report_unsolved Nothing False TypeError HoleError HoleError HoleError wanted
= do { ev_binds <- newTcEvBinds
; report_unsolved ev_binds False TypeError
HoleError HoleError HoleError wanted }
-- | Report all unsolved goals as warnings (but without deferring any errors to
-- run-time). See Note [Safe Haskell Overlapping Instances Implementation] in
-- TcSimplify
warnAllUnsolved :: WantedConstraints -> TcM ()
warnAllUnsolved wanted
= report_unsolved Nothing True TypeWarn HoleWarn HoleWarn HoleWarn wanted
= do { ev_binds <- newTcEvBinds
; report_unsolved ev_binds True TypeWarn
HoleWarn HoleWarn HoleWarn wanted }
-- | Report unsolved goals as errors or warnings.
report_unsolved :: Maybe EvBindsVar -- cec_binds
report_unsolved :: EvBindsVar -- cec_binds
-> Bool -- Errors as warnings
-> TypeErrorChoice -- Deferred type errors
-> HoleChoice -- Expression holes
......@@ -277,21 +283,15 @@ data ReportErrCtxt
-- ic_skols and givens are tidied, rest are not
, cec_tidy :: TidyEnv
, cec_binds :: Maybe EvBindsVar
-- Nothing <=> Report all errors, including holes
-- Do not add any evidence bindings, because
-- we have no convenient place to put them
-- See TcErrors.reportAllUnsolved
-- Just ev <=> make some errors (depending on cec_defer)
-- into warnings, and emit evidence bindings
-- into 'ev' for unsolved constraints
, cec_binds :: EvBindsVar -- Make some errors (depending on cec_defer)
-- into warnings, and emit evidence bindings
-- into 'cec_binds' for unsolved constraints
, cec_errors_as_warns :: Bool -- Turn all errors into warnings
-- (except for Holes, which are
-- controlled by cec_type_holes and
-- cec_expr_holes)
, cec_defer_type_errors :: TypeErrorChoice -- Defer type errors until runtime
-- Irrelevant if cec_binds = Nothing
-- cec_expr_holes is a union of:
-- cec_type_holes - a set of typed holes: '_', '_a', '_foo'
......@@ -325,7 +325,7 @@ Specifically (see reportWanteds)
reportImplic :: ReportErrCtxt -> Implication -> TcM ()
reportImplic ctxt implic@(Implic { ic_skols = tvs, ic_given = given
, ic_wanted = wanted, ic_binds = m_evb
, ic_wanted = wanted, ic_binds = evb
, ic_status = status, ic_info = info
, ic_env = tcl_env, ic_tclvl = tc_lvl })
| BracketSkol <- info
......@@ -356,11 +356,7 @@ reportImplic ctxt implic@(Implic { ic_skols = tvs, ic_given = given
-- tree rooted here, or we've come across
-- a suppress-worthy constraint higher up (Trac #11541)
, cec_binds = cec_binds ctxt *> m_evb }
-- If cec_binds ctxt is Nothing, that means
-- we're reporting *all* errors. Don't change
-- that behavior just because we're going into
-- an implication.
, cec_binds = evb }
dead_givens = case status of
IC_Solved { ics_dead = dead } -> dead
......@@ -754,12 +750,12 @@ addDeferredBinding :: ReportErrCtxt -> ErrMsg -> Ct -> TcM ()
addDeferredBinding ctxt err ct
| CtWanted { ctev_pred = pred, ctev_dest = dest } <- ctEvidence ct
-- Only add deferred bindings for Wanted constraints
, Just ev_binds_var <- cec_binds ctxt -- We have somewhere to put the bindings
= do { dflags <- getDynFlags
; let err_msg = pprLocErrMsg err
err_fs = mkFastString $ showSDoc dflags $
err_msg $$ text "(deferred type error)"
err_tm = EvDelayedError pred err_fs
ev_binds_var = cec_binds ctxt
; case dest of
EvVarDest evar
......@@ -1537,8 +1533,8 @@ mkEqInfoMsg ct ty1 ty2
-- mismatched types for suggestion about -fprint-explicit-kinds
(act_ty, exp_ty) = case ctOrigin ct of
TypeEqOrigin { uo_actual = act
, uo_expected = Check exp } -> (act, exp)
_ -> (ty1, ty2)
, uo_expected = exp } -> (act, exp)
_ -> (ty1, ty2)
invis_msg | Just vis <- tcEqTypeVis act_ty exp_ty
, not vis
......@@ -1706,7 +1702,7 @@ mkExpectedActualMsg :: Type -> Type -> CtOrigin -> Maybe TypeOrKind -> Bool
-- NotSwapped means (actual, expected), IsSwapped is the reverse
-- First return val is whether or not to print a herald above this msg
mkExpectedActualMsg ty1 ty2 (TypeEqOrigin { uo_actual = act
, uo_expected = Check exp
, uo_expected = exp
, uo_thing = maybe_thing })
m_level printExpanded
| KindLevel <- level, occurs_check_error = (True, Nothing, empty)
......
......@@ -13,7 +13,7 @@ module TcEvidence (
-- Evidence bindings
TcEvBinds(..), EvBindsVar(..),
EvBindMap(..), emptyEvBindMap, extendEvBinds,
lookupEvBind, evBindMapBinds, foldEvBindMap,
lookupEvBind, evBindMapBinds, foldEvBindMap, isEmptyEvBindMap,
EvBind(..), emptyTcEvBinds, isEmptyTcEvBinds, mkGivenEvBind, mkWantedEvBind,
sccEvBinds, evBindVar,
EvTerm(..), mkEvCast, evVarsOfTerm, mkEvScSelectors,
......@@ -283,8 +283,24 @@ data TcEvBinds
| EvBinds -- Immutable after zonking
(Bag EvBind)
data EvBindsVar = EvBindsVar (IORef EvBindMap) Unique
-- The Unique is for debug printing only
data EvBindsVar
= EvBindsVar {
ebv_uniq :: Unique,
-- The Unique is for debug printing only
ebv_binds :: IORef EvBindMap,
-- The main payload: the value-level evidence bindings
-- (dictionaries etc)
ebv_tcvs :: IORef TyCoVarSet
-- The free vars of the (rhss of) the coercion bindings
--
-- Coercions don't actually have bindings
-- because we plug them in-place (via a mutable
-- variable); but we keep their free variables
-- so that we can report unused given constraints
-- See Note [Tracking redundant constraints] in TcSimplify
}
instance Data.Data TcEvBinds where
-- Placeholder; we can't travers into TcEvBinds
......@@ -325,6 +341,9 @@ extendEvBinds bs ev_bind
(eb_lhs ev_bind)
ev_bind }
isEmptyEvBindMap :: EvBindMap -> Bool
isEmptyEvBindMap (EvBindMap m) = isEmptyDVarEnv m
lookupEvBind :: EvBindMap -> EvVar -> Maybe EvBind
lookupEvBind bs = lookupDVarEnv (ev_bind_varenv bs)
......@@ -334,6 +353,9 @@ evBindMapBinds = foldEvBindMap consBag emptyBag
foldEvBindMap :: (EvBind -> a -> a) -> a -> EvBindMap -> a
foldEvBindMap k z bs = foldDVarEnv k z (ev_bind_varenv bs)
instance Outputable EvBindMap where
ppr (EvBindMap m) = ppr m
-----------------
-- All evidence is bound by EvBinds; no side effects
data EvBind
......@@ -761,10 +783,11 @@ instance Outputable TcEvBinds where
ppr (EvBinds bs) = text "EvBinds" <> braces (vcat (map ppr (bagToList bs)))
instance Outputable EvBindsVar where
ppr (EvBindsVar _ u) = text "EvBindsVar" <> angleBrackets (ppr u)
ppr (EvBindsVar { ebv_uniq = u })
= text "EvBindsVar" <> angleBrackets (ppr u)
instance Uniquable EvBindsVar where
getUnique (EvBindsVar _ u) = u
getUnique (EvBindsVar { ebv_uniq = u }) = u
instance Outputable EvBind where
ppr (EvBind { eb_lhs = v, eb_rhs = e, eb_is_given = is_given })
......
......@@ -141,7 +141,7 @@ tcInferSigma expr = addErrCtxt (exprCtxt expr) (tcInferSigmaNC expr)
tcInferSigmaNC (L loc expr)
= setSrcSpan loc $
do { (expr', sigma) <- tcInfer (tcExpr expr)
do { (expr', sigma) <- tcInferNoInst (tcExpr expr)
; return (L loc expr', sigma) }
tcInferRho, tcInferRhoNC :: LHsExpr Name -> TcM (LHsExpr TcId, TcRhoType)
......@@ -1176,14 +1176,10 @@ tcInferFun (L loc (HsRecFld f))
; return (L loc fun, ty) }
tcInferFun fun
= do { (fun, fun_ty) <- tcInferSigma fun
= tcInferSigma fun
-- NB: tcInferSigma; see TcUnify
-- Note [Deep instantiation of InferResult]
-- Zonk the function type carefully, to expose any polymorphism
-- E.g. (( \(x::forall a. a->a). blah ) e)
-- We can see the rank-2 type of the lambda in time to generalise e
; fun_ty' <- zonkTcType fun_ty
; return (fun, fun_ty') }
----------------
-- | Type-check the arguments to a function, possibly including visible type
......@@ -1267,7 +1263,7 @@ tcTupArgs args tys
tcSyntaxOp :: CtOrigin
-> SyntaxExpr Name
-> [SyntaxOpType] -- ^ shape of syntax operator arguments
-> ExpType -- ^ overall result type
-> ExpRhoType -- ^ overall result type
-> ([TcSigmaType] -> TcM a) -- ^ Type check any arguments
-> TcM (a, SyntaxExpr TcId)
-- ^ Typecheck a syntax operator
......@@ -1365,7 +1361,7 @@ tcSynArgE orig sigma_ty syn_ty thing_inside
herald = text "This rebindable syntax expects a function with"
go rho_ty (SynType the_ty)
= do { wrap <- tcSubTypeET orig the_ty rho_ty
= do { wrap <- tcSubTypeET orig GenSigCtxt the_ty rho_ty
; result <- thing_inside []
; return (result, wrap) }
......@@ -1507,8 +1503,7 @@ tcExprSig expr sig@(PartialSig { psig_name = name, sig_loc = loc })
then return idHsWrapper -- Fast path; also avoids complaint when we infer
-- an ambiguouse type and have AllowAmbiguousType
-- e..g infer x :: forall a. F a -> Int
else tcSubType_NC ExprSigCtxt inferred_sigma
(mkCheckExpType my_sigma)
else tcSubType_NC ExprSigCtxt inferred_sigma my_sigma
; traceTc "tcExpSig" (ppr qtvs $$ ppr givens $$ ppr inferred_sigma $$ ppr my_sigma)
; let poly_wrap = wrap
......@@ -1581,6 +1576,7 @@ tcInferRecSelId (Ambiguous lbl _)
------------------------
tcInferId :: Name -> TcM (HsExpr TcId, TcSigmaType)
-- Look up an occurrence of an Id
-- Do not instantiate its type
tcInferId id_name
| id_name `hasKey` tagToEnumKey
= failWithTc (text "tagToEnum# must appear applied to one argument")
......@@ -1750,7 +1746,7 @@ tcSeq loc fun_name args res_ty
-> do { rr_ty <- newFlexiTyVarTy runtimeRepTy
; ty_arg2 <- tcHsTypeApp hs_ty_arg2 (tYPE rr_ty)
-- see Note [Typing rule for seq]
; _ <- tcSubTypeDS GenSigCtxt noThing ty_arg2 res_ty
; _ <- tcSubTypeDS (OccurrenceOf fun_name) GenSigCtxt ty_arg2 res_ty
; return (term_arg1, term_arg2, mkCheckExpType ty_arg2) }
[Left term_arg1, Left term_arg2]
-> return (term_arg1, term_arg2, res_ty)
......@@ -1773,7 +1769,7 @@ tcTagToEnum loc fun_name args res_ty
; arg <- case args of
[Right hs_ty_arg, Left term_arg]
-> do { ty_arg <- tcHsTypeApp hs_ty_arg liftedTypeKind
; _ <- tcSubTypeDS GenSigCtxt noThing ty_arg res_ty
; _ <- tcSubTypeDS (OccurrenceOf fun_name) GenSigCtxt ty_arg res_ty
-- other than influencing res_ty, we just
-- don't care about a type arg passed in.
-- So drop the evidence.
......
......@@ -1445,8 +1445,9 @@ zonk_tc_ev_binds env (TcEvBinds var) = zonkEvBindsVar env var
zonk_tc_ev_binds env (EvBinds bs) = zonkEvBinds env bs
zonkEvBindsVar :: ZonkEnv -> EvBindsVar -> TcM (ZonkEnv, Bag EvBind)
zonkEvBindsVar env (EvBindsVar ref _) = do { bs <- readMutVar ref
; zonkEvBinds env (evBindMapBinds bs) }
zonkEvBindsVar env (EvBindsVar { ebv_binds = ref })
= do { bs <- readMutVar ref
; zonkEvBinds env (evBindMapBinds bs) }
zonkEvBinds :: ZonkEnv -> Bag EvBind -> TcM (ZonkEnv, Bag EvBind)
zonkEvBinds env binds
......@@ -1598,7 +1599,7 @@ zonkTvSkolemising :: UnboundTyVarZonker
-- This variant is used for the LHS of rules
-- See Note [Zonking the LHS of a RULE].
zonkTvSkolemising tv
= do { tv' <- skolemiseUnboundMetaTyVar tv vanillaSkolemTv
= do { tv' <- skolemiseUnboundMetaTyVar tv
; return (mkTyVarTy tv') }
zonkTypeZapping :: UnboundTyVarZonker
......
......@@ -853,7 +853,7 @@ checkExpectedKind :: TcType -- the type whose kind we're checking
checkExpectedKind ty act_kind exp_kind
= do { (ty', act_kind') <- instantiate ty act_kind exp_kind
; let origin = TypeEqOrigin { uo_actual = act_kind'
, uo_expected = mkCheckExpType exp_kind
, uo_expected = exp_kind
, uo_thing = Just $ mkTypeErrorThing ty'
}
; co_k <- uType origin KindLevel act_kind' exp_kind
......@@ -1276,7 +1276,8 @@ kcHsTyVarBndrs name cusk open_fam all_kind_vars
, hsq_dependent = dep_names }) thing_inside
| cusk
= do { kv_kinds <- mk_kv_kinds
; let scoped_kvs = zipWith mk_skolem_tv kv_ns kv_kinds
; lvl <- getTcLevel
; let scoped_kvs = zipWith (mk_skolem_tv lvl) kv_ns kv_kinds
; tcExtendTyVarEnv2 (kv_ns `zip` scoped_kvs) $
do { (tc_binders, res_kind, stuff) <- solveEqualities $
bind_telescope hs_tvs thing_inside
......@@ -1527,14 +1528,16 @@ tcHsTyVarName m_kind name
_ -> do { kind <- case m_kind of
Just kind -> return kind
Nothing -> newMetaKindVar
; return (mk_skolem_tv name kind, False) }}
; tv <- newSkolemTyVar name kind
; return (tv, False) }}
-- makes a new skolem tv
newSkolemTyVar :: Name -> Kind -> TcM TcTyVar
newSkolemTyVar name kind = return (mk_skolem_tv name kind)
newSkolemTyVar name kind = do { lvl <- getTcLevel
; return (mk_skolem_tv lvl name kind) }
mk_skolem_tv :: Name -> Kind -> TcTyVar
mk_skolem_tv n k = mkTcTyVar n k vanillaSkolemTv
mk_skolem_tv :: TcLevel -> Name -> Kind -> TcTyVar
mk_skolem_tv lvl n k = mkTcTyVar n k (SkolemTv lvl False)
------------------
kindGeneralizeType :: Type -> TcM Type
......@@ -1810,7 +1813,7 @@ tcHsPartialSigType ctxt sig_ty
; tau <- zonkTcType tau
; checkValidType ctxt (mkSpecForAllTys all_tvs $ mkPhiTy theta tau)
; traceTc "tcHsPatSigType" (ppr all_tvs)
; traceTc "tcHsPartialSigType" (ppr all_tvs)
; return (wcs, wcx, all_tvs, theta, tau) }
where
new_implicit_tv name = do { kind <- newMetaKindVar
......@@ -1889,7 +1892,7 @@ tcPatSig in_pat_bind sig res_ty
; if null sig_tvs then do {
-- Just do the subsumption check and return
wrap <- addErrCtxtM (mk_msg sig_ty) $
tcSubTypeET_NC PatSigCtxt res_ty sig_ty
tcSubTypeET PatSigOrigin PatSigCtxt res_ty sig_ty
; return (sig_ty, [], sig_wcs, wrap)
} else do
-- Type signature binds at least one scoped type variable
......@@ -1912,7 +1915,7 @@ tcPatSig in_pat_bind sig res_ty
-- Now do a subsumption check of the pattern signature against res_ty
; wrap <- addErrCtxtM (mk_msg sig_ty) $
tcSubTypeET_NC PatSigCtxt res_ty sig_ty
tcSubTypeET PatSigOrigin PatSigCtxt res_ty sig_ty
-- Phew!
; return (sig_ty, sig_tvs, sig_wcs, wrap)
......
......@@ -810,7 +810,7 @@ tcInstDecl2 (InstInfo { iSpec = ispec, iBinds = ibinds })
, ic_given = dfun_ev_vars
, ic_wanted = mkImplicWC sc_meth_implics
, ic_status = IC_Unsolved
, ic_binds = Just dfun_ev_binds_var
, ic_binds = dfun_ev_binds_var
, ic_env = env
, ic_info = InstSkol }
......@@ -1017,7 +1017,7 @@ checkInstConstraints thing_inside
, ic_given = []
, ic_wanted = wanted
, ic_status = IC_Unsolved
, ic_binds = Just ev_binds_var
, ic_binds = ev_binds_var
, ic_env = env
, ic_info = InstSkol }
......@@ -1368,8 +1368,7 @@ tcMethodBodyHelp hs_sig_fn sel_id local_meth_id meth_bind
; sig_ty <- tcHsSigType (FunSigCtxt sel_name False) hs_sig_ty
; let local_meth_ty = idType local_meth_id
; hs_wrap <- addErrCtxtM (methSigCtxt sel_name sig_ty local_meth_ty) $
tcSubType ctxt (Just sel_id) sig_ty
(mkCheckExpType local_meth_ty)
tcSubType_NC ctxt sig_ty local_meth_ty
; return (sig_ty, hs_wrap) }
; inner_meth_name <- newName (nameOccName sel_name)
......
This diff is collapsed.
......@@ -869,10 +869,9 @@ tcDoStmt ctxt (RecStmt { recS_stmts = stmts, recS_later_ids = later_names
tup_ty = mkBigCoreTupTy tup_elt_tys
; tcExtendIdEnv tup_ids $ do
{ stmts_ty <- newOpenInferExpType
; (stmts', (ret_op', tup_rets))
<- tcStmtsAndThen ctxt tcDoStmt stmts stmts_ty $
\ inner_res_ty ->
{ ((stmts', (ret_op', tup_rets)), stmts_ty)
<- tcInferInst $ \ exp_ty ->
tcStmtsAndThen ctxt tcDoStmt stmts exp_ty $ \ inner_res_ty ->
do { tup_rets <- zipWithM tcCheckId tup_names
(map mkCheckExpType tup_elt_tys)
-- Unify the types of the "final" Ids (which may
......@@ -881,14 +880,12 @@ tcDoStmt ctxt (RecStmt { recS_stmts = stmts, recS_later_ids = later_names
<- tcSyntaxOp DoOrigin ret_op [synKnownType tup_ty]
inner_res_ty $ \_ -> return ()
; return (ret_op', tup_rets) }
; stmts_ty <- readExpType stmts_ty
; mfix_res_ty <- newOpenInferExpType
; (_, mfix_op')
<- tcSyntaxOp DoOrigin mfix_op
[synKnownType (mkFunTy tup_ty stmts_ty)] mfix_res_ty $
; ((_, mfix_op'), mfix_res_ty)
<- tcInferInst $ \ exp_ty ->
tcSyntaxOp DoOrigin mfix_op
[synKnownType (mkFunTy tup_ty stmts_ty)] exp_ty $
\ _ -> return ()
; mfix_res_ty <- readExpType mfix_res_ty
; ((thing, new_res_ty), bind_op')
<- tcSyntaxOp DoOrigin bind_op
......@@ -1014,7 +1011,7 @@ tcApplicativeStmts
tcApplicativeStmts ctxt pairs rhs_ty thing_inside
= do { body_ty <- newFlexiTyVarTy liftedTypeKind
; let arity = length pairs
; ts <- replicateM (arity-1) $ newOpenInferExpType
; ts <- replicateM (arity-1) $ newInferExpTypeInst
; exp_tys <- replicateM arity $ newFlexiTyVarTy liftedTypeKind
; pat_tys <- replicateM arity $ newFlexiTyVarTy liftedTypeKind
; let fun_ty = mkFunTys pat_tys body_ty
......
......@@ -397,7 +397,7 @@ tc_pat penv (ViewPat expr pat _) overall_pat_ty thing_inside
-- expr_wrap1 :: expr'_inferred "->" (inf_arg_ty -> inf_res_ty)
-- check that overall pattern is more polymorphic than arg type
; expr_wrap2 <- tcSubTypeET (pe_orig penv) overall_pat_ty inf_arg_ty
; expr_wrap2 <- tcSubTypePat penv overall_pat_ty inf_arg_ty
-- expr_wrap2 :: overall_pat_ty "->" inf_arg_ty
-- pattern must have inf_res_ty
......@@ -502,13 +502,12 @@ tc_pat penv (ConPatIn con arg_pats) pat_ty thing_inside
------------------------
-- Literal patterns
tc_pat _ (LitPat simple_lit) pat_ty thing_inside
tc_pat penv (LitPat simple_lit) pat_ty thing_inside
= do { let lit_ty = hsLitType simple_lit
; co <- unifyPatType simple_lit lit_ty pat_ty
-- coi is of kind: pat_ty ~ lit_ty
; res <- thing_inside
; wrap <- tcSubTypePat penv pat_ty lit_ty
; res <- thing_inside
; pat_ty <- readExpType pat_ty
; return ( mkHsWrapPatCo co (LitPat simple_lit) pat_ty
; return ( mkHsWrapPat wrap (LitPat simple_lit) pat_ty
, res) }
------------------------
......@@ -622,15 +621,6 @@ tc_pat penv (SplicePat (HsSpliced mod_finalizers (HsSplicedPat pat)))
tc_pat _ _other_pat _ _ = panic "tc_pat" -- ConPatOut, SigPatOut
----------------
unifyPatType :: Outputable a => a -> TcType -> ExpSigmaType -> TcM TcCoercion
-- In patterns we want a coercion from the
-- context type (expected) to the actual pattern type
-- But we don't want to reverse the args to unifyType because
-- that controls the actual/expected stuff in error messages
unifyPatType thing actual_ty expected_ty
= do { coi <- unifyExpType (Just thing) actual_ty expected_ty
; return (mkTcSymCo coi) }
{-
Note [Hopping the LIE in lazy patterns]
......@@ -841,7 +831,7 @@ tcPatSynPat penv (L con_span _) pat_syn pat_ty arg_pats thing_inside
prov_theta' = substTheta tenv prov_theta
req_theta' = substTheta tenv req_theta
; wrap <- tcSubTypeET (pe_orig penv) pat_ty ty'
; wrap <- tcSubTypePat penv pat_ty ty'
; traceTc "tcPatSynPat" (ppr pat_syn $$
ppr pat_ty $$
ppr ty' $$
......
......@@ -72,11 +72,9 @@ tcInferPatSynDecl PSB{ psb_id = lname@(L _ name), psb_args = details,
; let (arg_names, rec_fields, is_infix) = collectPatSynArgInfo details
; (tclvl, wanted, ((lpat', args), pat_ty))
<- pushLevelAndCaptureConstraints $
do { pat_ty <- newOpenInferExpType
; stuff <- tcPat PatSyn lpat pat_ty $
mapM tcLookupId arg_names
; pat_ty <- readExpType pat_ty
; return (stuff, pat_ty) }
tcInferInst $ \ exp_ty ->
tcPat PatSyn lpat exp_ty $
mapM tcLookupId arg_names
; let named_taus = (name, pat_ty) : map (\arg -> (getName arg, varType arg)) args
......@@ -390,11 +388,11 @@ tcPatSynMatcher (L loc name) lpat
(args, arg_tys) pat_ty
= do { rr_name <- newNameAt (mkTyVarOcc "rep") loc
; tv_name <- newNameAt (mkTyVarOcc "r") loc
; let rr_tv = mkTcTyVar rr_name runtimeRepTy (SkolemTv False)
rr = mkTyVarTy rr_tv
res_tv = mkTcTyVar tv_name (tYPE rr) (SkolemTv False)
is_unlifted = null args && null prov_dicts
; let rr_tv = mkTcTyVar rr_name runtimeRepTy vanillaSkolemTv
rr = mkTyVarTy rr_tv
res_tv = mkTcTyVar tv_name (tYPE rr) vanillaSkolemTv
res_ty = mkTyVarTy res_tv
is_unlifted = null args && null prov_dicts
(cont_args, cont_arg_tys)
| is_unlifted = ([nlHsVar voidPrimId], [voidPrimTy])
| otherwise = (args, arg_tys)
......
......@@ -48,8 +48,7 @@ module TcPluginM (
-- * Manipulating evidence bindings
newEvVar,