Commit 8a9a7a8c authored by Simon Peyton Jones's avatar Simon Peyton Jones

Add type "holes", enabled by -XTypeHoles, Trac #5910

This single commit combines a lot of work done by
Thijs Alkemade <thijsalkemade@gmail.com>, plus a slew
of subsequent refactoring by Simon PJ.

The basic idea is
* Add a new expression form "_", a hole, standing for a not-yet-written expression
* Give a useful error message that
   (a) gives the type of the hole
   (b) gives the types of some enclosing value bindings that
       mention the hole

Driven by this goal I did a LOT of refactoring in TcErrors, which in turn
allows us to report enclosing value bindings for other errors, not just
holes.  (Thijs rightly did not attempt this!)

The major data type change is a new form of constraint
  data Ct = ...
    	  | CHoleCan {
    	      cc_ev       :: CtEvidence,
    	      cc_hole_ty  :: TcTauType,
    	      cc_depth    :: SubGoalDepth }

I'm still in two minds about whether this is the best plan. Another
possibility would be to have a predicate type for holes, somthing like
   class Hole a where
     holeValue :: a

It works the way it is, but there are some annoying special cases for
CHoleCan (just grep for "CHoleCan").
parent b0db9308
......@@ -576,6 +576,7 @@ addTickHsExpr (HsWrap w e) =
(addTickHsExpr e) -- explicitly no tick on inside
addTickHsExpr e@(HsType _) = return e
addTickHsExpr HsHole = panic "addTickHsExpr.HsHole"
-- Others dhould never happen in expression content.
addTickHsExpr e = pprPanic "addTickHsExpr" (ppr e)
......
......@@ -216,6 +216,8 @@ dsExpr (HsLamCase arg matches@(MatchGroup _ rhs_ty))
dsExpr (HsApp fun arg)
= mkCoreAppDs <$> dsLExpr fun <*> dsLExpr arg
dsExpr HsHole = panic "dsExpr: HsHole"
\end{code}
Note [Desugaring vars]
......
......@@ -294,6 +294,7 @@ data HsExpr id
| HsWrap HsWrapper -- TRANSLATION
(HsExpr id)
| HsHole
deriving (Data, Typeable)
-- HsTupArg is used for tuple sections
......@@ -559,6 +560,8 @@ ppr_expr (HsArrForm (L _ (HsVar v)) (Just _) [arg1, arg2])
ppr_expr (HsArrForm op _ args)
= hang (ptext (sLit "(|") <> ppr_lexpr op)
4 (sep (map (pprCmdArg.unLoc) args) <> ptext (sLit "|)"))
ppr_expr HsHole
= ptext $ sLit "_"
pprCmdArg :: OutputableBndr id => HsCmdTop id -> SDoc
pprCmdArg (HsCmdTop cmd@(L _ (HsArrForm _ Nothing [])) _ _ _)
......
......@@ -507,6 +507,7 @@ data ExtensionFlag
| Opt_TraditionalRecordSyntax
| Opt_LambdaCase
| Opt_MultiWayIf
| Opt_TypeHoles
deriving (Eq, Enum, Show)
-- | Contains not only a collection of 'DynFlag's but also a plethora of
......@@ -2449,7 +2450,8 @@ xFlags = [
( "OverlappingInstances", Opt_OverlappingInstances, nop ),
( "UndecidableInstances", Opt_UndecidableInstances, nop ),
( "IncoherentInstances", Opt_IncoherentInstances, nop ),
( "PackageImports", Opt_PackageImports, nop )
( "PackageImports", Opt_PackageImports, nop ),
( "TypeHoles", Opt_TypeHoles, nop )
]
defaultFlags :: Platform -> [DynFlag]
......
......@@ -34,7 +34,7 @@ import HsSyn
import TcRnMonad
import TcEnv ( thRnBrack )
import RnEnv
import RnTypes
import RnTypes
import RnPat
import DynFlags
import BasicTypes ( FixityDirection(..) )
......@@ -299,6 +299,9 @@ rnExpr (ArithSeq _ seq)
rnExpr (PArrSeq _ seq)
= rnArithSeq seq `thenM` \ (new_seq, fvs) ->
return (PArrSeq noPostTcExpr new_seq, fvs)
rnExpr HsHole
= return (HsHole, emptyFVs)
\end{code}
These three are pattern syntax appearing in expressions.
......@@ -306,7 +309,11 @@ Since all the symbols are reservedops we can simply reject them.
We return a (bogus) EWildPat in each case.
\begin{code}
rnExpr e@EWildPat = patSynErr e
rnExpr e@EWildPat = do { holes <- xoptM Opt_TypeHoles
; if holes
then return (HsHole, emptyFVs)
else patSynErr e
}
rnExpr e@(EAsPat {}) = patSynErr e
rnExpr e@(EViewPat {}) = patSynErr e
rnExpr e@(ELazyPat {}) = patSynErr e
......
......@@ -356,14 +356,14 @@ tcSyntaxName orig ty (std_nm, user_nm_expr) = do
syntaxNameCtxt :: HsExpr Name -> CtOrigin -> Type -> TidyEnv
-> TcRn (TidyEnv, SDoc)
syntaxNameCtxt name orig ty tidy_env = do
inst_loc <- getCtLoc orig
let
msg = vcat [ptext (sLit "When checking that") <+> quotes (ppr name) <+>
ptext (sLit "(needed by a syntactic construct)"),
nest 2 (ptext (sLit "has the required type:") <+> ppr (tidyType tidy_env ty)),
nest 2 (pprArisingAt inst_loc)]
return (tidy_env, msg)
syntaxNameCtxt name orig ty tidy_env
= do { inst_loc <- getCtLoc orig
; let msg = vcat [ ptext (sLit "When checking that") <+> quotes (ppr name)
<+> ptext (sLit "(needed by a syntactic construct)")
, nest 2 (ptext (sLit "has the required type:")
<+> ppr (tidyType tidy_env ty))
, nest 2 (pprArisingAt inst_loc) ]
; return (tidy_env, msg) }
\end{code}
......@@ -523,6 +523,7 @@ tyVarsOfCt (CTyEqCan { cc_tyvar = tv, cc_rhs = xi }) = extendVarSet (tyVarsOf
tyVarsOfCt (CFunEqCan { cc_tyargs = tys, cc_rhs = xi }) = tyVarsOfTypes (xi:tys)
tyVarsOfCt (CDictCan { cc_tyargs = tys }) = tyVarsOfTypes tys
tyVarsOfCt (CIrredEvCan { cc_ty = ty }) = tyVarsOfType ty
tyVarsOfCt (CHoleCan { cc_hole_ty = ty }) = tyVarsOfType ty
tyVarsOfCt (CNonCanonical { cc_ev = fl }) = tyVarsOfType (ctEvPred fl)
tyVarsOfCts :: Cts -> TcTyVarSet
......@@ -551,8 +552,10 @@ tidyCt :: TidyEnv -> Ct -> Ct
-- Used only in error reporting
-- Also converts it to non-canonical
tidyCt env ct
= CNonCanonical { cc_ev = tidy_flavor env (cc_ev ct)
, cc_depth = cc_depth ct }
= case ct of
CHoleCan {} -> ct { cc_ev = tidy_flavor env (cc_ev ct) }
_ -> CNonCanonical { cc_ev = tidy_flavor env (cc_ev ct)
, cc_depth = cc_depth ct }
where
tidy_flavor :: TidyEnv -> CtEvidence -> CtEvidence
-- NB: we do not tidy the ctev_evtm/var field because we don't
......@@ -569,8 +572,8 @@ tidyEvVar :: TidyEnv -> EvVar -> EvVar
tidyEvVar env var = setVarType var (tidyType env (varType var))
tidyGivenLoc :: TidyEnv -> GivenLoc -> GivenLoc
tidyGivenLoc env (CtLoc skol span ctxt)
= CtLoc (tidySkolemInfo env skol) span ctxt
tidyGivenLoc env (CtLoc skol lcl)
= CtLoc (tidySkolemInfo env skol) lcl
tidySkolemInfo :: TidyEnv -> SkolemInfo -> SkolemInfo
tidySkolemInfo env (SigSkol cx ty) = SigSkol cx (tidyType env ty)
......@@ -635,8 +638,8 @@ substFlavor subst ctev@(CtDerived { ctev_pred = pty })
= ctev { ctev_pred = substTy subst pty }
substGivenLoc :: TvSubst -> GivenLoc -> GivenLoc
substGivenLoc subst (CtLoc skol span ctxt)
= CtLoc (substSkolemInfo subst skol) span ctxt
substGivenLoc subst (CtLoc skol lcl)
= CtLoc (substSkolemInfo subst skol) lcl
substSkolemInfo :: TvSubst -> SkolemInfo -> SkolemInfo
substSkolemInfo subst (SigSkol cx ty) = SigSkol cx (substTy subst ty)
......
This diff is collapsed.
......@@ -195,7 +195,9 @@ canonicalize (CIrredEvCan { cc_ev = fl
, cc_depth = d
, cc_ty = xi })
= canIrred d fl xi
canonicalize ct@(CHoleCan {})
= do { emitInsoluble ct
; return Stop }
canEvNC :: SubGoalDepth
-> CtEvidence
......@@ -227,7 +229,6 @@ canTuple d fl tys
; canEvVarsCreated d ctevs }
\end{code}
%************************************************************************
%* *
%* Class Canonicalization
......@@ -818,7 +819,9 @@ canEqAppTy d fl s1 t1 s2 t2
; canEvVarsCreated d ctevs }
canEqFailure :: SubGoalDepth -> CtEvidence -> TcS StopOrContinue
canEqFailure d fl = do { emitFrozenError fl d; return Stop }
canEqFailure d fl
= do { emitInsoluble (CNonCanonical { cc_ev = fl, cc_depth = d })
; return Stop }
------------------------
emitKindConstraint :: Ct -> TcS StopOrContinue
......
......@@ -25,6 +25,8 @@ module TcEnv(
tcExtendTyVarEnv, tcExtendTyVarEnv2,
tcExtendGhciEnv, tcExtendLetEnv,
tcExtendIdEnv, tcExtendIdEnv1, tcExtendIdEnv2,
tcExtendIdBndrs,
tcLookup, tcLookupLocated, tcLookupLocalIds,
tcLookupId, tcLookupTyVar,
tcLookupLcl_maybe,
......@@ -375,27 +377,36 @@ tcExtendLetEnv closed ids thing_inside
; tc_extend_local_env [ (idName id, ATcId { tct_id = id
, tct_closed = closed
, tct_level = thLevel stage })
| id <- ids]
thing_inside }
| id <- ids] $
tcExtendIdBndrs [TcIdBndr id closed | id <- ids] thing_inside }
tcExtendIdEnv :: [TcId] -> TcM a -> TcM a
tcExtendIdEnv ids thing_inside
= tcExtendIdEnv2 [(idName id, id) | id <- ids] thing_inside
= tcExtendIdEnv2 [(idName id, id) | id <- ids] $
tcExtendIdBndrs [TcIdBndr id NotTopLevel | id <- ids]
thing_inside
tcExtendIdEnv1 :: Name -> TcId -> TcM a -> TcM a
tcExtendIdEnv1 name id thing_inside
= tcExtendIdEnv2 [(name,id)] thing_inside
= tcExtendIdEnv2 [(name,id)] $
tcExtendIdBndrs [TcIdBndr id NotTopLevel]
thing_inside
tcExtendIdEnv2 :: [(Name,TcId)] -> TcM a -> TcM a
-- Do *not* extend the tcl_bndrs stack
-- The tct_closed flag really doesn't matter
-- Invariant: the TcIds are fully zonked (see tcExtendIdEnv above)
tcExtendIdEnv2 names_w_ids thing_inside
= do { stage <- getStage
; tc_extend_local_env [ (name, ATcId { tct_id = id
, tct_closed = NotTopLevel
, tct_level = thLevel stage })
| (name,id) <- names_w_ids]
| (name,id) <- names_w_ids] $
thing_inside }
tcExtendIdBndrs :: [TcIdBinder] -> TcM a -> TcM a
tcExtendIdBndrs bndrs = updLclEnv (\env -> env { tcl_bndrs = bndrs ++ tcl_bndrs env })
tcExtendGhciEnv :: [TcId] -> TcM a -> TcM a
-- Used to bind Ids for GHCi identifiers bound earlier in the user interaction
-- Note especially that we bind them at
......
This diff is collapsed.
......@@ -231,6 +231,15 @@ tcExpr (HsType ty) _
-- so it's not enabled yet.
-- Can't eliminate it altogether from the parser, because the
-- same parser parses *patterns*.
tcExpr HsHole res_ty
= do { ty <- newFlexiTyVarTy liftedTypeKind
; traceTc "tcExpr.HsHole" (ppr ty)
; ev <- mkSysLocalM (mkFastString "_") ty
; loc <- getCtLoc HoleOrigin
; let can = CHoleCan { cc_ev = CtWanted loc ty ev, cc_hole_ty = ty, cc_depth = 0 }
; traceTc "tcExpr.HsHole emitting" (ppr can)
; emitInsoluble can
; tcWrapResult (HsVar ev) ty res_ty }
\end{code}
......
......@@ -713,6 +713,9 @@ zonkExpr env (HsWrap co_fn expr)
zonkExpr env1 expr `thenM` \ new_expr ->
return (HsWrap new_co_fn new_expr)
zonkExpr _ HsHole
= return HsHole
zonkExpr _ expr = pprPanic "zonkExpr" (ppr expr)
zonkCmdTop :: ZonkEnv -> LHsCmdTop TcId -> TcM (LHsCmdTop Id)
......
......@@ -725,12 +725,14 @@ zonkWC function an evidence variable to collect all the extra
variables.
\begin{code}
zonkCt :: Ct -> TcM Ct
zonkCt ct
= do { fl' <- zonkCtEvidence (cc_ev ct)
; return (CNonCanonical { cc_ev = fl'
, cc_depth = cc_depth ct }) }
| isHoleCt ct = do { fl' <- zonkCtEvidence (cc_ev ct)
; return $ ct { cc_ev = fl' } }
| otherwise = do { fl' <- zonkCtEvidence (cc_ev ct)
; return $
CNonCanonical { cc_ev = fl'
, cc_depth = cc_depth ct } }
zonkCtEvidence :: CtEvidence -> TcM CtEvidence
zonkCtEvidence ctev@(CtGiven { ctev_gloc = loc, ctev_pred = pred })
......@@ -746,9 +748,9 @@ zonkCtEvidence ctev@(CtDerived { ctev_pred = pred })
zonkGivenLoc :: GivenLoc -> TcM GivenLoc
-- GivenLocs may have unification variables inside them!
zonkGivenLoc (CtLoc skol_info span ctxt)
zonkGivenLoc (CtLoc skol_info lcl)
= do { skol_info' <- zonkSkolemInfo skol_info
; return (CtLoc skol_info' span ctxt) }
; return (CtLoc skol_info' lcl) }
zonkSkolemInfo :: SkolemInfo -> TcM SkolemInfo
zonkSkolemInfo (SigSkol cx ty) = do { ty' <- zonkTcType ty
......
......@@ -146,6 +146,7 @@ initTc hsc_env hsc_src keep_rn_syntax mod do_this
tcl_th_ctxt = topStage,
tcl_arrow_ctxt = NoArrowCtxt,
tcl_env = emptyNameEnv,
tcl_bndrs = [],
tcl_tidy = emptyTidyEnv,
tcl_tyvars = tvs_var,
tcl_lie = lie_var,
......@@ -366,15 +367,8 @@ newUniqueSupply
writeMutVar u_var us1 ;
return us2 }}}
newLocalName :: Name -> TcRnIf gbl lcl Name
newLocalName name -- Make a clone
= do { uniq <- newUnique
; return (mkInternalName uniq (nameOccName name) (getSrcSpan name)) }
newSysLocalIds :: FastString -> [TcType] -> TcRnIf gbl lcl [TcId]
newSysLocalIds fs tys
= do { us <- newUniqueSupply
; return (zipWith (mkSysLocal fs) (uniqsFromSupply us) tys) }
newLocalName :: Name -> TcM Name
newLocalName name = newName (nameOccName name)
newName :: OccName -> TcM Name
newName occ
......@@ -382,6 +376,11 @@ newName occ
; loc <- getSrcSpanM
; return (mkInternalName uniq occ loc) }
newSysLocalIds :: FastString -> [TcType] -> TcRnIf gbl lcl [TcId]
newSysLocalIds fs tys
= do { us <- newUniqueSupply
; return (zipWith (mkSysLocal fs) (uniqsFromSupply us) tys) }
instance MonadUnique (IOEnv (Env gbl lcl)) where
getUniqueM = newUnique
getUniqueSupplyM = newUniqueSupply
......@@ -818,12 +817,15 @@ popErrCtxt = updCtxt (\ msgs -> case msgs of { [] -> []; (_ : ms) -> ms })
getCtLoc :: orig -> TcM (CtLoc orig)
getCtLoc origin
= do { loc <- getSrcSpanM ; env <- getLclEnv ;
return (CtLoc origin loc (tcl_ctxt env)) }
= do { env <- getLclEnv ; return (CtLoc origin env) }
setCtLoc :: CtLoc orig -> TcM a -> TcM a
setCtLoc (CtLoc _ src_loc ctxt) thing_inside
= setSrcSpan src_loc (setErrCtxt ctxt thing_inside)
-- Set the SrcSpan and error context from the CtLoc
setCtLoc (CtLoc _ lcl) thing_inside
= updLclEnv (\env -> env { tcl_loc = tcl_loc lcl
, tcl_bndrs = tcl_bndrs lcl
, tcl_ctxt = tcl_ctxt lcl })
thing_inside
\end{code}
%************************************************************************
......@@ -1024,6 +1026,13 @@ emitImplications ct
= do { lie_var <- getConstraintVar ;
updTcRef lie_var (`addImplics` ct) }
emitInsoluble :: Ct -> TcM ()
emitInsoluble ct
= do { lie_var <- getConstraintVar ;
updTcRef lie_var (`addInsols` unitBag ct) ;
v <- readTcRef lie_var ;
traceTc "emitInsoluble" (ppr v) }
captureConstraints :: TcM a -> TcM (a, WantedConstraints)
-- (captureConstraints m) runs m, and returns the type constraints it generates
captureConstraints thing_inside
......
......@@ -38,7 +38,7 @@ module TcRnTypes(
WhereFrom(..), mkModDeps,
-- Typechecker types
TcTypeEnv, TcTyThing(..), PromotionErr(..),
TcTypeEnv, TcIdBinder(..), TcTyThing(..), PromotionErr(..),
pprTcTyThingCategory, pprPECategory,
-- Template Haskell
......@@ -53,16 +53,16 @@ module TcRnTypes(
singleCt, extendCts, isEmptyCts, isCTyEqCan, isCFunEqCan,
isCDictCan_Maybe, isCFunEqCan_Maybe,
isCIrredEvCan, isCNonCanonical, isWantedCt, isDerivedCt,
isGivenCt,
isGivenCt, isHoleCt,
ctWantedLoc, ctEvidence,
SubGoalDepth, mkNonCanonical, mkNonCanonicalCt,
ctPred, ctEvPred, ctEvTerm, ctEvId,
ctPred, ctEvPred, ctEvTerm, ctEvId, ctEvEnv,
WantedConstraints(..), insolubleWC, emptyWC, isEmptyWC,
andWC, addFlats, addImplics, mkFlatWC,
andWC, unionsWC, addFlats, addImplics, mkFlatWC, addInsols,
Implication(..),
CtLoc(..), ctLocSpan, ctLocOrigin, setCtLocOrigin,
CtLoc(..), ctLocSpan, ctLocEnv, ctLocOrigin, setCtLocOrigin,
CtOrigin(..), EqOrigin(..),
WantedLoc, GivenLoc, pushErrCtxt,
pushErrCtxtSameOrigin,
......@@ -121,7 +121,6 @@ import FastString
import Util
import Data.Set (Set)
\end{code}
......@@ -408,12 +407,11 @@ Why? Because they are now Ids not TcIds. This final GlobalEnv is
data TcLclEnv -- Changes as we move inside an expression
-- Discarded after typecheck/rename; not passed on to desugarer
= TcLclEnv {
tcl_loc :: SrcSpan, -- Source span
tcl_ctxt :: [ErrCtxt], -- Error context, innermost on top
tcl_errs :: TcRef Messages, -- Place to accumulate errors
tcl_th_ctxt :: ThStage, -- Template Haskell context
tcl_arrow_ctxt :: ArrowCtxt, -- Arrow-notation context
tcl_loc :: SrcSpan, -- Source span
tcl_ctxt :: [ErrCtxt], -- Error context, innermost on top
tcl_untch :: Untouchables, -- Birthplace for new unification variables
tcl_th_ctxt :: ThStage, -- Template Haskell context
tcl_arrow_ctxt :: ArrowCtxt, -- Arrow-notation context
tcl_rdr :: LocalRdrEnv, -- Local name envt
-- Maintained during renaming, of course, but also during
......@@ -427,8 +425,11 @@ data TcLclEnv -- Changes as we move inside an expression
-- We still need the unsullied global name env so that
-- we can look up record field names
tcl_env :: TcTypeEnv, -- The local type environment: Ids and
-- TyVars defined in this module
tcl_env :: TcTypeEnv, -- The local type environment:
-- Ids and TyVars defined in this module
tcl_bndrs :: [TcIdBinder], -- Stack of locally-bound Ids, innermost on top
-- Used only for error reporting
tcl_tidy :: TidyEnv, -- Used for tidying types; contains all
-- in-scope type variables (but not term variables)
......@@ -439,12 +440,12 @@ data TcLclEnv -- Changes as we move inside an expression
-- in tcl_lenv.
-- Why mutable? see notes with tcGetGlobalTyVars
tcl_lie :: TcRef WantedConstraints, -- Place to accumulate type constraints
tcl_untch :: Untouchables
tcl_lie :: TcRef WantedConstraints, -- Place to accumulate type constraints
tcl_errs :: TcRef Messages -- Place to accumulate errors
}
type TcTypeEnv = NameEnv TcTyThing
data TcIdBinder = TcIdBndr TcId TopLevelFlag
{- Note [Given Insts]
~~~~~~~~~~~~~~~~~~
......@@ -900,6 +901,13 @@ data Ct
cc_ev :: CtEvidence,
cc_depth :: SubGoalDepth
}
| CHoleCan {
cc_ev :: CtEvidence,
cc_hole_ty :: TcTauType, -- Not a Xi! See same not as above
cc_depth :: SubGoalDepth -- See Note [WorkList]
}
\end{code}
Note [Ct/evidence invariant]
......@@ -979,6 +987,11 @@ isCFunEqCan _ = False
isCNonCanonical :: Ct -> Bool
isCNonCanonical (CNonCanonical {}) = True
isCNonCanonical _ = False
isHoleCt:: Ct -> Bool
isHoleCt (CHoleCan {}) = True
isHoleCt _ = False
\end{code}
\begin{code}
......@@ -991,6 +1004,7 @@ instance Outputable Ct where
CNonCanonical {} -> "CNonCanonical"
CDictCan {} -> "CDictCan"
CIrredEvCan {} -> "CIrredEvCan"
CHoleCan {} -> "CHoleCan"
\end{code}
\begin{code}
......@@ -1057,6 +1071,9 @@ andWC (WC { wc_flat = f1, wc_impl = i1, wc_insol = n1 })
, wc_impl = i1 `unionBags` i2
, wc_insol = n1 `unionBags` n2 }
unionsWC :: [WantedConstraints] -> WantedConstraints
unionsWC = foldr andWC emptyWC
addFlats :: WantedConstraints -> Bag Ct -> WantedConstraints
addFlats wc cts
= wc { wc_flat = wc_flat wc `unionBags` cts }
......@@ -1064,6 +1081,10 @@ addFlats wc cts
addImplics :: WantedConstraints -> Bag Implication -> WantedConstraints
addImplics wc implic = wc { wc_impl = wc_impl wc `unionBags` implic }
addInsols :: WantedConstraints -> Bag Ct -> WantedConstraints
addInsols wc cts
= wc { wc_insol = wc_insol wc `unionBags` cts }
instance Outputable WantedConstraints where
ppr (WC {wc_flat = f, wc_impl = i, wc_insol = n})
= ptext (sLit "WC") <+> braces (vcat
......@@ -1090,11 +1111,6 @@ data Implication
= Implic {
ic_untch :: Untouchables, -- Untouchables: unification variables
-- free in the environment
ic_env :: TcTypeEnv, -- The type environment
-- Used only when generating error messages
-- Generally, ic_untch is a superset of tvsof(ic_env)
-- However, we don't zonk ic_env when zonking the Implication
-- Instead we do that when generating a skolem-escape error message
ic_skols :: [TcTyVar], -- Introduced skolems
-- See Note [Skolems in an implication]
......@@ -1260,6 +1276,11 @@ ctEvTerm (CtWanted { ctev_evar = ev }) = EvId ev
ctEvTerm ctev@(CtDerived {}) = pprPanic "ctEvTerm: derived constraint cannot have id"
(ppr ctev)
ctEvEnv :: CtEvidence -> TcLclEnv
ctEvEnv (CtWanted { ctev_wloc = loc }) = ctLocEnv loc
ctEvEnv (CtDerived { ctev_wloc = loc }) = ctLocEnv loc
ctEvEnv (CtGiven { ctev_gloc = loc }) = ctLocEnv loc
ctEvId :: CtEvidence -> TcId
ctEvId (CtWanted { ctev_evar = ev }) = ev
ctEvId ctev = pprPanic "ctEvId:" (ppr ctev)
......@@ -1339,26 +1360,35 @@ dictionaries don't appear in the original source code.
type will evolve...
\begin{code}
data CtLoc orig = CtLoc orig SrcSpan [ErrCtxt]
data CtLoc orig = CtLoc orig TcLclEnv
-- The TcLclEnv includes particularly
-- source location: tcl_loc :: SrcSpan
-- context: tcl_ctxt :: [ErrCtxt]
-- binder stack: tcl_bndrs :: [TcIdBinders]
type WantedLoc = CtLoc CtOrigin -- Instantiation for wanted constraints
type GivenLoc = CtLoc SkolemInfo -- Instantiation for given constraints
type WantedLoc = CtLoc CtOrigin -- Instantiation for wanted constraints
type GivenLoc = CtLoc SkolemInfo -- Instantiation for given constraints
ctLocEnv :: CtLoc o -> TcLclEnv
ctLocEnv (CtLoc _ lcl) = lcl
ctLocSpan :: CtLoc o -> SrcSpan
ctLocSpan (CtLoc _ s _) = s
ctLocSpan (CtLoc _ lcl) = tcl_loc lcl
ctLocOrigin :: CtLoc o -> o
ctLocOrigin (CtLoc o _ _) = o
ctLocOrigin (CtLoc o _) = o
setCtLocOrigin :: CtLoc o -> o' -> CtLoc o'
setCtLocOrigin (CtLoc _ s c) o = CtLoc o s c
setCtLocOrigin (CtLoc _ lcl) o = CtLoc o lcl
pushErrCtxt :: orig -> ErrCtxt -> CtLoc orig -> CtLoc orig
pushErrCtxt o err (CtLoc _ s errs) = CtLoc o s (err:errs)
pushErrCtxt o err (CtLoc _ lcl)
= CtLoc o (lcl { tcl_ctxt = err : tcl_ctxt lcl })
pushErrCtxtSameOrigin :: ErrCtxt -> CtLoc orig -> CtLoc orig
-- Just add information w/o updating the origin!
pushErrCtxtSameOrigin err (CtLoc o s errs) = CtLoc o s (err:errs)
pushErrCtxtSameOrigin err (CtLoc o lcl)
= CtLoc o (lcl { tcl_ctxt = err : tcl_ctxt lcl })
pprArising :: CtOrigin -> SDoc
-- Used for the main, top-level error message
......@@ -1368,8 +1398,8 @@ pprArising FunDepOrigin = empty
pprArising orig = text "arising from" <+> ppr orig
pprArisingAt :: Outputable o => CtLoc o -> SDoc
pprArisingAt (CtLoc o s _) = sep [ text "arising from" <+> ppr o
, text "at" <+> ppr s]
pprArisingAt (CtLoc o lcl) = sep [ text "arising from" <+> ppr o
, text "at" <+> ppr (tcl_loc lcl)]
\end{code}
%************************************************************************
......@@ -1496,6 +1526,7 @@ data CtOrigin
| ProcOrigin -- Arising from a proc expression
| AnnOrigin -- An annotation
| FunDepOrigin
| HoleOrigin
data EqOrigin
= UnifyOrigin
......@@ -1533,6 +1564,7 @@ pprO ProcOrigin = ptext (sLit "a proc expression")
pprO (TypeEqOrigin eq) = ptext (sLit "an equality") <+> ppr eq
pprO AnnOrigin = ptext (sLit "an annotation")
pprO FunDepOrigin = ptext (sLit "a functional dependency")
pprO HoleOrigin = ptext (sLit "a use of the hole") <+> quotes (ptext $ sLit "_")
instance Outputable EqOrigin where
ppr (UnifyOrigin t1 t2) = ppr t1 <+> char '~' <+> ppr t2
......
......@@ -26,7 +26,6 @@ import TcEnv
import TcEvidence( TcEvBinds(..) )
import Type
import Id
import NameEnv( emptyNameEnv )
import Name
import Var
import VarSet
......@@ -139,10 +138,10 @@ tcRule (HsRule name act hs_bndrs lhs fv_lhs rhs fv_rhs)
-- Note [Typechecking rules]
; vars <- tcRuleBndrs hs_bndrs
; let (id_bndrs, tv_bndrs) = partition (isId . snd) vars
; let (id_bndrs, tv_bndrs) = partition isId vars
; (lhs', lhs_wanted, rhs', rhs_wanted, rule_ty)
<- tcExtendTyVarEnv2 tv_bndrs $
tcExtendIdEnv2 id_bndrs $
<- tcExtendTyVarEnv tv_bndrs $
tcExtendIdEnv id_bndrs $
do { ((lhs', rule_ty), lhs_wanted) <- captureConstraints (tcInferRho lhs)
; (rhs', rhs_wanted) <- captureConstraints (tcMonoExpr rhs rule_ty)
; return (lhs', lhs_wanted, rhs', rhs_wanted, rule_ty) }
......@@ -161,7 +160,7 @@ tcRule (HsRule name act hs_bndrs lhs fv_lhs rhs fv_rhs)
-- the LHS, lest they otherwise get defaulted to Any; but we do that
-- during zonking (see TcHsSyn.zonkRule)
; let tpl_ids = lhs_evs ++ map snd id_bndrs
; let tpl_ids = lhs_evs ++ id_bndrs
forall_tvs = tyVarsOfTypes (rule_ty : map idType tpl_ids)
; zonked_forall_tvs <- zonkTyVarsAndFV forall_tvs
; gbl_tvs <- tcGetGlobalTyVars -- Already zonked
......@@ -181,7 +180,6 @@ tcRule (HsRule name act hs_bndrs lhs fv_lhs rhs fv_rhs)
; loc <- getCtLoc (RuleSkol name)
; rhs_binds_var <- newTcEvBinds
; emitImplication $ Implic { ic_untch = noUntouchables
, ic_env = emptyNameEnv
, ic_skols = qtkvs
, ic_fsks = []
, ic_given = lhs_evs
......@@ -195,7 +193,6 @@ tcRule (HsRule name act hs_bndrs lhs fv_lhs rhs fv_rhs)
-- (b) so that we bind any soluble ones
; lhs_binds_var <- newTcEvBinds
; emitImplication $ Implic { ic_untch = noUntouchables
, ic_env = emptyNameEnv
, ic_skols = qtkvs
, ic_fsks = []
, ic_given = lhs_evs
......@@ -209,25 +206,30 @@ tcRule (HsRule name act hs_bndrs lhs fv_lhs rhs fv_rhs)
(mkHsDictLet (TcEvBinds lhs_binds_var) lhs') fv_lhs
(mkHsDictLet (TcEvBinds rhs_binds_var) rhs') fv_rhs) }
tcRuleBndrs :: [RuleBndr Name] -> TcM [(Name, Var)]
tcRuleBndrs :: [RuleBndr Name] -> TcM [Var]
tcRuleBndrs []
= return []
tcRuleBndrs (RuleBndr (L _ name) : rule_bndrs)
= do { ty <- newFlexiTyVarTy openTypeKind
; vars <- tcRuleBndrs rule_bndrs
; return ((name, mkLocalId name ty) : vars) }
; return (mkLocalId name ty : vars) }
tcRuleBndrs (RuleBndrSig (L _ name) rn_ty : rule_bndrs)
-- e.g x :: a->a
-- The tyvar 'a' is brought into scope first, just as if you'd written
-- a::*, x :: a->a
= do { let ctxt = RuleSigCtxt name
; (id_ty, skol_tvs) <- tcHsPatSigType ctxt rn_ty
; let id = mkLocalId name id_ty
; (id_ty, tv_prs) <- tcHsPatSigType ctxt rn_ty
; let id = mkLocalId name id_ty
tvs = map snd tv_prs
-- tcHsPatSigType returns (Name,TyVar) pairs
-- for for RuleSigCtxt their Names are not
-- cloned, so we get (n, tv-with-name-n) pairs
-- See Note [Pattern signature binders] in TcHsType
-- The type variables scope over subsequent bindings; yuk
; vars <- tcExtendTyVarEnv2 skol_tvs $
; vars <- tcExtendTyVarEnv tvs $
tcRuleBndrs rule_bndrs
; return (skol_tvs ++ (name, id) : vars) }
; return (tvs ++ id : vars) }
ruleCtxt :: FastString -> SDoc
ruleCtxt name = ptext (sLit "When checking the transformation rule") <+>
......
......@@ -22,7 +22,7 @@ module TcSMonad (
updTcSImplics,
Ct(..), Xi, tyVarsOfCt, tyVarsOfCts,
emitFrozenError,
emitInsoluble,
isWanted, isDerived,
isGivenCt, isWantedCt, isDerivedCt, pprFlavorArising,
......@@ -88,7 +88,6 @@ module TcSMonad (
matchClass, matchFam, MatchInstResult (..),
checkWellStagedDFun,
warnTcS,
pprEq -- Smaller utils, re-exported from TcM
-- TODO (DV): these are only really used in the
-- instance matcher in TcSimplify. I am wondering
......@@ -306,6 +305,9 @@ data CCanMap a
keepGivenCMap :: CCanMap a -> CCanMap a
keepGivenCMap cc = emptyCCanMap { cts_given = cts_given cc }
instance Outputable (CCanMap a) where
ppr (CCanMap given derived wanted) = ptext (sLit "CCanMap") <+> (ppr given) <+> (ppr derived) <+> (ppr wanted)
cCanMapToBag :: CCanMap a -> Cts
cCanMapToBag cmap = foldUFM unionBags rest_wder (cts_given cmap)
where rest_wder = foldUFM unionBags rest_der (cts_wanted cmap)
......@@ -592,8 +594,6 @@ insertInertItem :: Ct -> InertSet -> InertSet
-- Add a new inert element to the inert set.
insertInertItem item is
= -- A canonical Given, Wanted, or Derived
ASSERT2( not (isCNonCanonical item), ppr item )
-- Can't be CNonCanonical, because they only land in inert_insols
is { inert_cans = upd_inert_cans (inert_cans is) item }
where upd_inert_cans :: InertCans -> Ct -> InertCans
......@@ -626,7 +626,9 @@ insertInertItem item is
(unFamHeadMap $ inert_funeqs ics)) }
| otherwise
= pprPanic "upd_inert set: can't happen! Inserting " $
ppr item
ppr item -- Can't be CNonCanonical, CHoleCan,
-- because they only land in inert_insols
insertInertItemTcS :: Ct -> TcS ()
-- Add a new item in the inerts of the monad
......@@ -813,6 +815,10 @@ extractRelevantInerts wi
where
fam_head = mkTyConApp (cc_fun ct) (cc_tyargs ct)
extract_ics_relevants (CHoleCan {}) ics
= pprPanic "extractRelevantInerts" (ppr wi)
-- Holes are put straight into inert_frozen, so never get here
extract_ics_relevants (CIrredEvCan { }) ics =
let cts = inert_irreds ics
in (cts, ics { inert_irreds = emptyCts })
......@@ -1138,21 +1144,20 @@ updTcSImplics f
; wrapTcS $ do { implics <- TcM.readTcRef impl_ref
; TcM.writeTcRef impl_ref (f implics) } }
emitFrozenError :: CtEvidence -> SubGoalDepth -> TcS ()
emitInsoluble :: Ct -> TcS ()
-- Emits a non-canonical constraint that will stand for a frozen error in the inerts.
emitFrozenError fl depth
= do { traceTcS "Emit frozen error" (ppr (ctEvPred fl))
emitInsoluble ct
= do { traceTcS "Emit insoluble" (ppr ct)
; updInertTcS add_insol }
where
add_insol is@(IS { inert_cans = ics@(IC { inert_insols = old_insols }) })
| already_there = is
| otherwise = is { inert_cans = ics { inert_insols = extendCts old_insols insol_ct } }
| otherwise = is { inert_cans = ics { inert_insols = extendCts old_insols ct } }
where
already_there = not (isWanted fl) && anyBag (eqType this_pred . ctPred) old_insols
already_there = not (isWantedCt ct) && anyBag (eqType this_pred . ctPred) old_insols
-- See Note [Do not add duplicate derived insolubles]
insol_ct = CNonCanonical { cc_ev = fl, cc_depth = depth }
this_pred = ctEvPred fl
this_pred = ctPred ct
getTcSImplicsRef :: TcS (IORef (Bag Implication))