From 453a092e5f2b7abf35e7b0baa642658e0d545e9d Mon Sep 17 00:00:00 2001
From: Simon Peyton Jones <simonpj@microsoft.com>
Date: Fri, 25 Oct 2013 14:43:25 +0100
Subject: [PATCH] Untabify and remove trailing whitespace
... plus a couple of unused variables in TcSMonad
---
compiler/typecheck/TcInteract.lhs | 971 +++++++++++++++---------------
compiler/typecheck/TcRnTypes.lhs | 50 +-
compiler/typecheck/TcSMonad.lhs | 584 +++++++++---------
compiler/typecheck/TcSimplify.lhs | 365 ++++++-----
compiler/typecheck/TcType.lhs | 569 +++++++++--------
5 files changed, 1255 insertions(+), 1284 deletions(-)
diff --git a/compiler/typecheck/TcInteract.lhs b/compiler/typecheck/TcInteract.lhs
index a8637b7b2541..f33d5940423f 100644
--- a/compiler/typecheck/TcInteract.lhs
+++ b/compiler/typecheck/TcInteract.lhs
@@ -1,15 +1,8 @@
\begin{code}
-{-# OPTIONS -fno-warn-tabs #-}
--- The above warning supression flag is a temporary kludge.
--- While working on this module you are encouraged to remove it and
--- detab the module (please do the detabbing in a separate patch). See
--- http://ghc.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#TabsvsSpaces
--- for details
-
-module TcInteract (
+module TcInteract (
solveInteractGiven, -- Solves [EvVar],GivenLoc
solveInteract, -- Solves Cts
- ) where
+ ) where
#include "HsVersions.h"
@@ -54,38 +47,38 @@ import Control.Monad( when, unless )
import Pair (Pair(..))
import Unique( hasKey )
import UniqFM
-import FastString ( sLit )
+import FastString ( sLit )
import DynFlags
import Util
\end{code}
**********************************************************************
-* *
+* *
* Main Interaction Solver *
* *
**********************************************************************
-Note [Basic Simplifier Plan]
+Note [Basic Simplifier Plan]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-1. Pick an element from the WorkList if there exists one with depth
- less thanour context-stack depth.
+1. Pick an element from the WorkList if there exists one with depth
+ less thanour context-stack depth.
-2. Run it down the 'stage' pipeline. Stages are:
+2. Run it down the 'stage' pipeline. Stages are:
- canonicalization
- inert reactions
- spontaneous reactions
- top-level intreactions
- Each stage returns a StopOrContinue and may have sideffected
+ Each stage returns a StopOrContinue and may have sideffected
the inerts or worklist.
-
- The threading of the stages is as follows:
- - If (Stop) is returned by a stage then we start again from Step 1.
- - If (ContinueWith ct) is returned by a stage, we feed 'ct' on to
- the next stage in the pipeline.
-4. If the element has survived (i.e. ContinueWith x) the last stage
+
+ The threading of the stages is as follows:
+ - If (Stop) is returned by a stage then we start again from Step 1.
+ - If (ContinueWith ct) is returned by a stage, we feed 'ct' on to
+ the next stage in the pipeline.
+4. If the element has survived (i.e. ContinueWith x) the last stage
then we add him in the inerts and jump back to Step 1.
-If in Step 1 no such element exists, we have exceeded our context-stack
+If in Step 1 no such element exists, we have exceeded our context-stack
depth and will simply fail.
\begin{code}
solveInteractGiven :: CtLoc -> [TcTyVar] -> [EvVar] -> TcS ()
@@ -101,7 +94,7 @@ solveInteractGiven loc fsks givens
-- What would the evidence look like?!
-- See Note [Do not decompose given polytype equalities]
-- in TcCanonical
- where
+ where
given_bag = listToBag [ mkNonCanonical loc $ CtGiven { ctev_evtm = EvId ev_id
, ctev_pred = evVarPred ev_id }
| ev_id <- givens ]
@@ -128,7 +121,7 @@ solveInteract cts
solve_loop max_depth
= {-# SCC "solve_loop" #-}
do { sel <- selectNextWorkItem max_depth
- ; case sel of
+ ; case sel of
NoWorkRemaining -- Done, successfuly (modulo frozen)
-> return ()
MaxDepthExceeded ct -- Failure, depth exceeded
@@ -140,46 +133,46 @@ type WorkItem = Ct
type SimplifierStage = WorkItem -> TcS StopOrContinue
continueWith :: WorkItem -> TcS StopOrContinue
-continueWith work_item = return (ContinueWith work_item)
+continueWith work_item = return (ContinueWith work_item)
-data SelectWorkItem
+data SelectWorkItem
= NoWorkRemaining -- No more work left (effectively we're done!)
| MaxDepthExceeded Ct -- More work left to do but this constraint has exceeded
- -- the max subgoal depth and we must stop
- | NextWorkItem Ct -- More work left, here's the next item to look at
+ -- the max subgoal depth and we must stop
+ | NextWorkItem Ct -- More work left, here's the next item to look at
selectNextWorkItem :: SubGoalDepth -- Max depth allowed
-> TcS SelectWorkItem
selectNextWorkItem max_depth
= updWorkListTcS_return pick_next
- where
+ where
pick_next :: WorkList -> (SelectWorkItem, WorkList)
- pick_next wl
+ pick_next wl
= case selectWorkItem wl of
- (Nothing,_)
+ (Nothing,_)
-> (NoWorkRemaining,wl) -- No more work
- (Just ct, new_wl)
+ (Just ct, new_wl)
| ctLocDepth (cc_loc ct) > max_depth -- Depth exceeded
-> (MaxDepthExceeded ct,new_wl)
- (Just ct, new_wl)
+ (Just ct, new_wl)
-> (NextWorkItem ct, new_wl) -- New workitem and worklist
-runSolverPipeline :: [(String,SimplifierStage)] -- The pipeline
- -> WorkItem -- The work item
- -> TcS ()
+runSolverPipeline :: [(String,SimplifierStage)] -- The pipeline
+ -> WorkItem -- The work item
+ -> TcS ()
-- Run this item down the pipeline, leaving behind new work and inerts
-runSolverPipeline pipeline workItem
- = do { initial_is <- getTcSInerts
- ; traceTcS "Start solver pipeline {" $
- vcat [ ptext (sLit "work item = ") <+> ppr workItem
+runSolverPipeline pipeline workItem
+ = do { initial_is <- getTcSInerts
+ ; traceTcS "Start solver pipeline {" $
+ vcat [ ptext (sLit "work item = ") <+> ppr workItem
, ptext (sLit "inerts = ") <+> ppr initial_is]
; bumpStepCountTcS -- One step for each constraint processed
; final_res <- run_pipeline pipeline (ContinueWith workItem)
; final_is <- getTcSInerts
- ; case final_res of
- Stop -> do { traceTcS "End solver pipeline (discharged) }"
+ ; case final_res of
+ Stop -> do { traceTcS "End solver pipeline (discharged) }"
(ptext (sLit "inerts = ") <+> ppr final_is)
; return () }
ContinueWith ct -> do { traceFireTcS ct (ptext (sLit "Kept as inert:") <+> ppr ct)
@@ -190,14 +183,14 @@ runSolverPipeline pipeline workItem
; insertInertItemTcS ct }
}
where run_pipeline :: [(String,SimplifierStage)] -> StopOrContinue -> TcS StopOrContinue
- run_pipeline [] res = return res
- run_pipeline _ Stop = return Stop
+ run_pipeline [] res = return res
+ run_pipeline _ Stop = return Stop
run_pipeline ((stg_name,stg):stgs) (ContinueWith ct)
= do { traceTcS ("runStage " ++ stg_name ++ " {")
- (text "workitem = " <+> ppr ct)
- ; res <- stg ct
+ (text "workitem = " <+> ppr ct)
+ ; res <- stg ct
; traceTcS ("end stage " ++ stg_name ++ " }") empty
- ; run_pipeline stgs res
+ ; run_pipeline stgs res
}
\end{code}
@@ -234,13 +227,13 @@ thePipeline = [ ("canonicalization", TcCanonical.canonicalize)
*********************************************************************************
-* *
+* *
The spontaneous-solve Stage
* *
*********************************************************************************
\begin{code}
-spontaneousSolveStage :: SimplifierStage
+spontaneousSolveStage :: SimplifierStage
-- CTyEqCans are always consumed, returning Stop
spontaneousSolveStage workItem
= do { mb_solved <- trySpontaneousSolve workItem
@@ -249,13 +242,13 @@ spontaneousSolveStage workItem
| CTyEqCan { cc_tyvar = tv, cc_rhs = rhs, cc_ev = fl } <- workItem
-- Unsolved equality
-> do { untch <- getUntouchables
- ; traceTcS "Can't solve tyvar equality"
+ ; traceTcS "Can't solve tyvar equality"
(vcat [ text "LHS:" <+> ppr tv <+> dcolon <+> ppr (tyVarKind tv)
, text "RHS:" <+> ppr rhs <+> dcolon <+> ppr (typeKind rhs)
, text "Untouchables =" <+> ppr untch ])
; n_kicked <- kickOutRewritable (ctEvFlavour fl) tv
; traceFireTcS workItem $
- ptext (sLit "Kept as inert") <+> ppr_kicked n_kicked <> colon
+ ptext (sLit "Kept as inert") <+> ppr_kicked n_kicked <> colon
<+> ppr workItem
; insertInertItemTcS workItem
; return Stop }
@@ -267,13 +260,13 @@ spontaneousSolveStage workItem
-- see Note [Spontaneously solved in TyBinds]
-> do { n_kicked <- kickOutRewritable Given new_tv
; traceFireTcS workItem $
- ptext (sLit "Spontaneously solved") <+> ppr_kicked n_kicked <> colon
+ ptext (sLit "Spontaneously solved") <+> ppr_kicked n_kicked <> colon
<+> ppr workItem
; return Stop } }
ppr_kicked :: Int -> SDoc
ppr_kicked 0 = empty
-ppr_kicked n = parens (int n <+> ptext (sLit "kicked out"))
+ppr_kicked n = parens (int n <+> ptext (sLit "kicked out"))
\end{code}
Note [Spontaneously solved in TyBinds]
@@ -292,14 +285,14 @@ and only record them in the TyBinds of the TcS monad. The flattener is now consu
these binds /and/ the inerts for potentially unsolved or other given equalities.
\begin{code}
-kickOutRewritable :: CtFlavour -- Flavour of the equality that is
+kickOutRewritable :: CtFlavour -- Flavour of the equality that is
-- being added to the inert set
-> TcTyVar -- The new equality is tv ~ ty
-> TcS Int
kickOutRewritable new_flav new_tv
= do { wl <- modifyInertTcS kick_out
- ; traceTcS "kickOutRewritable" $
- vcat [ text "tv = " <+> ppr new_tv
+ ; traceTcS "kickOutRewritable" $
+ vcat [ text "tv = " <+> ppr new_tv
, ptext (sLit "Kicked out =") <+> ppr wl]
; updWorkListTcS (appendWorkList wl)
; return (workListSize wl) }
@@ -311,9 +304,9 @@ kickOutRewritable new_flav new_tv
, inert_irreds = irreds
, inert_insols = insols } }))
= (kicked_out, is { inert_cans = inert_cans_in })
- -- NB: Notice that don't rewrite
+ -- NB: Notice that don't rewrite
-- inert_solved_dicts, and inert_solved_funeqs
- -- optimistically. But when we lookup we have to take the
+ -- optimistically. But when we lookup we have to take the
-- subsitution into account
where
inert_cans_in = IC { inert_eqs = tv_eqs_in
@@ -324,9 +317,9 @@ kickOutRewritable new_flav new_tv
kicked_out = WorkList { wl_eqs = varEnvElts tv_eqs_out
, wl_funeqs = foldrBag insertDeque emptyDeque feqs_out
- , wl_rest = bagToList (dicts_out `andCts` irs_out
+ , wl_rest = bagToList (dicts_out `andCts` irs_out
`andCts` insols_out) }
-
+
(tv_eqs_out, tv_eqs_in) = partitionVarEnv kick_out_eq tv_eqs
(feqs_out, feqs_in) = partCtFamHeadMap kick_out_ct funeqmap
(dicts_out, dicts_in) = partitionCCanMap kick_out_ct dictmap
@@ -335,13 +328,13 @@ kickOutRewritable new_flav new_tv
-- Kick out even insolubles; see Note [Kick out insolubles]
kick_out_ct inert_ct = new_flav `canRewrite` (ctFlavour inert_ct) &&
- (new_tv `elemVarSet` tyVarsOfCt inert_ct)
- -- NB: tyVarsOfCt will return the type
- -- variables /and the kind variables/ that are
+ (new_tv `elemVarSet` tyVarsOfCt inert_ct)
+ -- NB: tyVarsOfCt will return the type
+ -- variables /and the kind variables/ that are
-- directly visible in the type. Hence we will
-- have exposed all the rewriting we care about
- -- to make the most precise kinds visible for
- -- matching classes etc. No need to kick out
+ -- to make the most precise kinds visible for
+ -- matching classes etc. No need to kick out
-- constraints that mention type variables whose
-- kinds could contain this variable!
@@ -361,42 +354,42 @@ kickOutRewritable new_flav new_tv
Note [Kick out insolubles]
~~~~~~~~~~~~~~~~~~~~~~~~~~
Suppose we have an insoluble alpha ~ [alpha], which is insoluble
-because an occurs check. And then we unify alpha := [Int].
+because an occurs check. And then we unify alpha := [Int].
Then we really want to rewrite the insouluble to [Int] ~ [[Int]].
Now it can be decomposed. Otherwise we end up with a "Can't match
[Int] ~ [[Int]]" which is true, but a bit confusing because the
-outer type constructors match.
+outer type constructors match.
Note [Delicate equality kick-out]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-When adding an equality (a ~ xi), we kick out an inert type-variable
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+When adding an equality (a ~ xi), we kick out an inert type-variable
equality (b ~ phi) in two cases
(1) If the new tyvar can rewrite the kind LHS or RHS of the inert
equality. Example:
Work item: [W] k ~ *
- Inert: [W] (a:k) ~ ty
+ Inert: [W] (a:k) ~ ty
[W] (b:*) ~ c :: k
We must kick out those blocked inerts so that we rewrite them
and can subsequently unify.
-(2) If the new tyvar can
+(2) If the new tyvar can
Work item: [G] a ~ b
Inert: [W] b ~ [a]
Now at this point the work item cannot be further rewritten by the
inert (due to the weaker inert flavor). But we can't add the work item
- as-is because the inert set would then have a cyclic substitution,
- when rewriting a wanted type mentioning 'a'. So we must kick the inert out.
+ as-is because the inert set would then have a cyclic substitution,
+ when rewriting a wanted type mentioning 'a'. So we must kick the inert out.
We have to do this only if the inert *cannot* rewrite the work item;
- it it can, then the work item will have been fully rewritten by the
+ it it can, then the work item will have been fully rewritten by the
inert during canonicalisation. So for example:
Work item: [W] a ~ Int
Inert: [W] b ~ [a]
No need to kick out the inert, beause the inert substitution is not
necessarily idemopotent. See Note [Non-idempotent inert substitution].
-See also point (8) of Note [Detailed InertCans Invariants]
+See also point (8) of Note [Detailed InertCans Invariants]
\begin{code}
data SPSolveResult = SPCantSolve
@@ -404,11 +397,11 @@ data SPSolveResult = SPCantSolve
-- We solved this /unification/ variable to some type using reflexivity
-- SPCantSolve means that we can't do the unification because e.g. the variable is untouchable
--- SPSolved workItem' gives us a new *given* to go on
+-- SPSolved workItem' gives us a new *given* to go on
-- @trySpontaneousSolve wi@ solves equalities where one side is a
-- touchable unification variable.
--- See Note [Touchables and givens]
+-- See Note [Touchables and givens]
trySpontaneousSolve :: WorkItem -> TcS SPSolveResult
trySpontaneousSolve workItem@(CTyEqCan { cc_ev = gw
, cc_tyvar = tv1, cc_rhs = xi, cc_loc = d })
@@ -422,20 +415,20 @@ trySpontaneousSolve workItem@(CTyEqCan { cc_ev = gw
(True, True) -> trySpontaneousEqTwoWay d gw tv1 tv2
(True, False) -> trySpontaneousEqOneWay d gw tv1 xi
(False, True) -> trySpontaneousEqOneWay d gw tv2 (mkTyVarTy tv1)
- _ -> return SPCantSolve }
+ _ -> return SPCantSolve }
| otherwise
= do { tch1 <- isTouchableMetaTyVarTcS tv1
; if tch1 then trySpontaneousEqOneWay d gw tv1 xi
else return SPCantSolve }
- -- No need for
+ -- No need for
-- trySpontaneousSolve (CFunEqCan ...) = ...
-- See Note [No touchables as FunEq RHS] in TcSMonad
trySpontaneousSolve item = do { traceTcS "Spont: no tyvar on lhs" (ppr item)
; return SPCantSolve }
----------------
-trySpontaneousEqOneWay :: CtLoc -> CtEvidence
+trySpontaneousEqOneWay :: CtLoc -> CtEvidence
-> TcTyVar -> Xi -> TcS SPSolveResult
-- tv is a MetaTyVar, not untouchable
trySpontaneousEqOneWay d gw tv xi
@@ -446,7 +439,7 @@ trySpontaneousEqOneWay d gw tv xi
= return SPCantSolve
----------------
-trySpontaneousEqTwoWay :: CtLoc -> CtEvidence
+trySpontaneousEqTwoWay :: CtLoc -> CtEvidence
-> TcTyVar -> TcTyVar -> TcS SPSolveResult
-- Both tyvars are *touchable* MetaTyvars so there is only a chance for kind error here
@@ -463,15 +456,15 @@ trySpontaneousEqTwoWay d gw tv1 tv2
nicer_to_update_tv2 = isSigTyVar tv1 || isSystemName (Var.varName tv2)
\end{code}
-Note [Avoid double unifications]
+Note [Avoid double unifications]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The spontaneous solver has to return a given which mentions the unified unification
-variable *on the left* of the equality. Here is what happens if not:
- Original wanted: (a ~ alpha), (alpha ~ Int)
-We spontaneously solve the first wanted, without changing the order!
- given : a ~ alpha [having unified alpha := a]
+variable *on the left* of the equality. Here is what happens if not:
+ Original wanted: (a ~ alpha), (alpha ~ Int)
+We spontaneously solve the first wanted, without changing the order!
+ given : a ~ alpha [having unified alpha := a]
Now the second wanted comes along, but he cannot rewrite the given, so we simply continue.
-At the end we spontaneously solve that guy, *reunifying* [alpha := Int]
+At the end we spontaneously solve that guy, *reunifying* [alpha := Int]
We avoid this problem by orienting the resulting given so that the unification
variable is on the left. [Note that alternatively we could attempt to
@@ -483,27 +476,27 @@ unification variables as RHS of type family equations: F xis ~ alpha.
\begin{code}
solveWithIdentity :: CtLoc -> CtEvidence -> TcTyVar -> Xi -> TcS SPSolveResult
--- Solve with the identity coercion
+-- Solve with the identity coercion
-- Precondition: kind(xi) is a sub-kind of kind(tv)
-- Precondition: CtEvidence is Wanted or Derived
--- See [New Wanted Superclass Work] to see why solveWithIdentity
+-- See [New Wanted Superclass Work] to see why solveWithIdentity
-- must work for Derived as well as Wanted
--- Returns: workItem where
+-- Returns: workItem where
-- workItem = the new Given constraint
--
--- NB: No need for an occurs check here, because solveWithIdentity always
+-- NB: No need for an occurs check here, because solveWithIdentity always
-- arises from a CTyEqCan, a *canonical* constraint. Its invariants
-- say that in (a ~ xi), the type variable a does not appear in xi.
-- See TcRnTypes.Ct invariants.
-solveWithIdentity _d wd tv xi
+solveWithIdentity _d wd tv xi
= do { let tv_ty = mkTyVarTy tv
- ; traceTcS "Sneaky unification:" $
+ ; traceTcS "Sneaky unification:" $
vcat [text "Unifies:" <+> ppr tv <+> ptext (sLit ":=") <+> ppr xi,
text "Coercion:" <+> pprEq tv_ty xi,
text "Left Kind is:" <+> ppr (typeKind tv_ty),
text "Right Kind is:" <+> ppr (typeKind xi) ]
- ; let xi' = defaultKind xi
+ ; let xi' = defaultKind xi
-- We only instantiate kind unification variables
-- with simple kinds like *, not OpenKind or ArgKind
-- cf TcUnify.uUnboundKVar
@@ -511,7 +504,7 @@ solveWithIdentity _d wd tv xi
; setWantedTyBind tv xi'
; let refl_evtm = EvCoercion (mkTcReflCo xi')
- ; when (isWanted wd) $
+ ; when (isWanted wd) $
setEvBind (ctev_evar wd) refl_evtm
; return (SPSolved tv) }
@@ -519,7 +512,7 @@ solveWithIdentity _d wd tv xi
*********************************************************************************
-* *
+* *
The interact-with-inert Stage
* *
*********************************************************************************
@@ -531,65 +524,65 @@ Note [The Solver Invariant]
We always add Givens first. So you might think that the solver has
the invariant
- If the work-item is Given,
+ If the work-item is Given,
then the inert item must Given
-But this isn't quite true. Suppose we have,
+But this isn't quite true. Suppose we have,
c1: [W] beta ~ [alpha], c2 : [W] blah, c3 :[W] alpha ~ Int
After processing the first two, we get
c1: [G] beta ~ [alpha], c2 : [W] blah
Now, c3 does not interact with the the given c1, so when we spontaneously
-solve c3, we must re-react it with the inert set. So we can attempt a
+solve c3, we must re-react it with the inert set. So we can attempt a
reaction between inert c2 [W] and work-item c3 [G].
It *is* true that [Solver Invariant]
- If the work-item is Given,
+ If the work-item is Given,
AND there is a reaction
then the inert item must Given
or, equivalently,
- If the work-item is Given,
+ If the work-item is Given,
and the inert item is Wanted/Derived
then there is no reaction
\begin{code}
-- Interaction result of WorkItem <~> Ct
-data InteractResult
+data InteractResult
= IRWorkItemConsumed { ir_fire :: String } -- Work item discharged by interaction; stop
| IRReplace { ir_fire :: String } -- Inert item replaced by work item; stop
- | IRInertConsumed { ir_fire :: String } -- Inert item consumed, keep going with work item
+ | IRInertConsumed { ir_fire :: String } -- Inert item consumed, keep going with work item
| IRKeepGoing { ir_fire :: String } -- Inert item remains, keep going with work item
-interactWithInertsStage :: WorkItem -> TcS StopOrContinue
--- Precondition: if the workitem is a CTyEqCan then it will not be able to
--- react with anything at this stage.
-interactWithInertsStage wi
+interactWithInertsStage :: WorkItem -> TcS StopOrContinue
+-- Precondition: if the workitem is a CTyEqCan then it will not be able to
+-- react with anything at this stage.
+interactWithInertsStage wi
= do { traceTcS "interactWithInerts" $ text "workitem = " <+> ppr wi
- ; rels <- extractRelevantInerts wi
+ ; rels <- extractRelevantInerts wi
; traceTcS "relevant inerts are:" $ ppr rels
; builtInInteractions
; foldlBagM interact_next (ContinueWith wi) rels }
- where interact_next Stop atomic_inert
+ where interact_next Stop atomic_inert
= do { insertInertItemTcS atomic_inert; return Stop }
- interact_next (ContinueWith wi) atomic_inert
+ interact_next (ContinueWith wi) atomic_inert
= do { ir <- doInteractWithInert atomic_inert wi
- ; let mk_msg rule keep_doc
+ ; let mk_msg rule keep_doc
= vcat [ text rule <+> keep_doc
, ptext (sLit "InertItem =") <+> ppr atomic_inert
, ptext (sLit "WorkItem =") <+> ppr wi ]
- ; case ir of
- IRWorkItemConsumed { ir_fire = rule }
+ ; case ir of
+ IRWorkItemConsumed { ir_fire = rule }
-> do { traceFireTcS wi (mk_msg rule (text "WorkItemConsumed"))
; insertInertItemTcS atomic_inert
- ; return Stop }
+ ; return Stop }
IRReplace { ir_fire = rule }
- -> do { traceFireTcS atomic_inert
+ -> do { traceFireTcS atomic_inert
(mk_msg rule (text "InertReplace"))
; insertInertItemTcS wi
- ; return Stop }
+ ; return Stop }
IRInertConsumed { ir_fire = rule }
- -> do { traceFireTcS atomic_inert
+ -> do { traceFireTcS atomic_inert
(mk_msg rule (text "InertItemConsumed"))
; return (ContinueWith wi) }
IRKeepGoing {}
@@ -630,7 +623,7 @@ doInteractWithInert :: Ct -> Ct -> TcS InteractResult
-- Identical class constraints.
doInteractWithInert inertItem@(CDictCan { cc_ev = fl1, cc_class = cls1, cc_tyargs = tys1, cc_loc = loc1 })
workItem@(CDictCan { cc_ev = fl2, cc_class = cls2, cc_tyargs = tys2, cc_loc = loc2 })
- | cls1 == cls2
+ | cls1 == cls2
= do { let pty1 = mkClassPred cls1 tys1
pty2 = mkClassPred cls2 tys2
inert_pred_loc = (pty1, pprArisingAt loc1)
@@ -643,14 +636,14 @@ doInteractWithInert inertItem@(CDictCan { cc_ev = fl1, cc_class = cls1, cc_tyarg
-- from pairs of Givens, and also because of floating when we approximate
-- implications. The relevant test is: typecheck/should_fail/FDsFromGivens.hs
-- Also see Note [When improvement happens]
-
- ; traceTcS "doInteractWithInert:dict"
+
+ ; traceTcS "doInteractWithInert:dict"
(vcat [ text "inertItem =" <+> ppr inertItem
, text "workItem =" <+> ppr workItem
, text "fundeps =" <+> ppr fd_work ])
-
+
; case fd_work of
- -- No Functional Dependencies
+ -- No Functional Dependencies
[] | eqTypes tys1 tys2 -> solveOneFromTheOther "Cls/Cls" fl1 workItem
| otherwise -> return (IRKeepGoing "NOP")
@@ -661,14 +654,14 @@ doInteractWithInert inertItem@(CDictCan { cc_ev = fl1, cc_class = cls1, cc_tyarg
-- Standard thing: create derived fds and keep on going. Importantly we don't
-- throw workitem back in the worklist because this can cause loops. See #5236.
- | otherwise
+ | otherwise
-> do { updWorkListTcS (extendWorkListEqs fd_work)
- ; return (IRKeepGoing "Cls/Cls (new fundeps)") } -- Just keep going without droping the inert
+ ; return (IRKeepGoing "Cls/Cls (new fundeps)") } -- Just keep going without droping the inert
}
-
--- Two pieces of irreducible evidence: if their types are *exactly identical*
--- we can rewrite them. We can never improve using this:
--- if we want ty1 :: Constraint and have ty2 :: Constraint it clearly does not
+
+-- Two pieces of irreducible evidence: if their types are *exactly identical*
+-- we can rewrite them. We can never improve using this:
+-- if we want ty1 :: Constraint and have ty2 :: Constraint it clearly does not
-- mean that (ty1 ~ ty2)
doInteractWithInert (CIrredEvCan { cc_ev = ifl })
workItem@(CIrredEvCan { cc_ev = wfl })
@@ -676,32 +669,32 @@ doInteractWithInert (CIrredEvCan { cc_ev = ifl })
= solveOneFromTheOther "Irred/Irred" ifl workItem
doInteractWithInert ii@(CFunEqCan { cc_ev = ev1, cc_fun = tc1
- , cc_tyargs = args1, cc_rhs = xi1, cc_loc = d1 })
+ , cc_tyargs = args1, cc_rhs = xi1, cc_loc = d1 })
wi@(CFunEqCan { cc_ev = ev2, cc_fun = tc2
, cc_tyargs = args2, cc_rhs = xi2, cc_loc = d2 })
| i_solves_w && (not (w_solves_i && isMetaTyVarTy xi1))
-- See Note [Carefully solve the right CFunEqCan]
= ASSERT( lhss_match ) -- extractRelevantInerts ensures this
- do { traceTcS "interact with inerts: FunEq/FunEq" $
+ do { traceTcS "interact with inerts: FunEq/FunEq" $
vcat [ text "workItem =" <+> ppr wi
, text "inertItem=" <+> ppr ii ]
; let xev = XEvTerm xcomp xdecomp
- -- xcomp : [(xi2 ~ xi1)] -> (F args ~ xi2)
+ -- xcomp : [(xi2 ~ xi1)] -> (F args ~ xi2)
xcomp [x] = EvCoercion (co1 `mkTcTransCo` mk_sym_co x)
xcomp _ = panic "No more goals!"
- -- xdecomp : (F args ~ xi2) -> [(xi2 ~ xi1)]
+ -- xdecomp : (F args ~ xi2) -> [(xi2 ~ xi1)]
xdecomp x = [EvCoercion (mk_sym_co x `mkTcTransCo` co1)]
; ctevs <- xCtFlavor ev2 [mkTcEqPred xi2 xi1] xev
-- No caching! See Note [Cache-caused loops]
-- Why not (mkTcEqPred xi1 xi2)? See Note [Efficient orientation]
- ; emitWorkNC d2 ctevs
+ ; emitWorkNC d2 ctevs
; return (IRWorkItemConsumed "FunEq/FunEq") }
| w_solves_i
= ASSERT( lhss_match ) -- extractRelevantInerts ensures this
- do { traceTcS "interact with inerts: FunEq/FunEq" $
+ do { traceTcS "interact with inerts: FunEq/FunEq" $
vcat [ text "workItem =" <+> ppr wi
, text "inertItem=" <+> ppr ii ]
@@ -712,34 +705,34 @@ doInteractWithInert ii@(CFunEqCan { cc_ev = ev1, cc_fun = tc1
-- xdecomp : (F args ~ xi1) -> [(xi2 ~ xi1)]
xdecomp x = [EvCoercion (mkTcSymCo co2 `mkTcTransCo` evTermCoercion x)]
- ; ctevs <- xCtFlavor ev1 [mkTcEqPred xi2 xi1] xev
+ ; ctevs <- xCtFlavor ev1 [mkTcEqPred xi2 xi1] xev
-- Why not (mkTcEqPred xi1 xi2)? See Note [Efficient orientation]
- ; emitWorkNC d1 ctevs
+ ; emitWorkNC d1 ctevs
; return (IRInertConsumed "FunEq/FunEq") }
where
- lhss_match = tc1 == tc2 && eqTypes args1 args2
+ lhss_match = tc1 == tc2 && eqTypes args1 args2
co1 = evTermCoercion $ ctEvTerm ev1
co2 = evTermCoercion $ ctEvTerm ev2
mk_sym_co x = mkTcSymCo (evTermCoercion x)
fl1 = ctEvFlavour ev1
fl2 = ctEvFlavour ev2
- i_solves_w = fl1 `canRewrite` fl2
- w_solves_i = fl2 `canRewrite` fl1
+ i_solves_w = fl1 `canRewrite` fl2
+ w_solves_i = fl2 `canRewrite` fl1
doInteractWithInert _ _ = return (IRKeepGoing "NOP")
\end{code}
-Note [Efficient Orientation]
+Note [Efficient Orientation]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Suppose we are interacting two FunEqCans with the same LHS:
- (inert) ci :: (F ty ~ xi_i)
- (work) cw :: (F ty ~ xi_w)
+ (inert) ci :: (F ty ~ xi_i)
+ (work) cw :: (F ty ~ xi_w)
We prefer to keep the inert (else we pass the work item on down
the pipeline, which is a bit silly). If we keep the inert, we
-will (a) discharge 'cw'
+will (a) discharge 'cw'
(b) produce a new equality work-item (xi_w ~ xi_i)
Notice the orientation (xi_w ~ xi_i) NOT (xi_i ~ xi_w):
new_work :: xi_w ~ xi_i
@@ -759,7 +752,7 @@ Note [Carefully solve the right CFunEqCan]
Consider the constraints
c1 :: F Int ~ a -- Arising from an application line 5
c2 :: F Int ~ Bool -- Arising from an application line 10
-Suppose that 'a' is a unification variable, arising only from
+Suppose that 'a' is a unification variable, arising only from
flattening. So there is no error on line 5; it's just a flattening
variable. But there is (or might be) an error on line 10.
@@ -831,8 +824,8 @@ I can think of two ways to fix this:
Note [Cache-caused loops]
~~~~~~~~~~~~~~~~~~~~~~~~~
-It is very dangerous to cache a rewritten wanted family equation as 'solved' in our
-solved cache (which is the default behaviour or xCtFlavor), because the interaction
+It is very dangerous to cache a rewritten wanted family equation as 'solved' in our
+solved cache (which is the default behaviour or xCtFlavor), because the interaction
may not be contributing towards a solution. Here is an example:
Initial inert set:
@@ -840,54 +833,54 @@ Initial inert set:
Work item:
[W] g2 : F a ~ beta2
The work item will react with the inert yielding the _same_ inert set plus:
- i) Will set g2 := g1 `cast` g3
+ i) Will set g2 := g1 `cast` g3
ii) Will add to our solved cache that [S] g2 : F a ~ beta2
- iii) Will emit [W] g3 : beta1 ~ beta2
+ iii) Will emit [W] g3 : beta1 ~ beta2
Now, the g3 work item will be spontaneously solved to [G] g3 : beta1 ~ beta2
-and then it will react the item in the inert ([W] g1 : F a ~ beta1). So it
-will set
- g1 := g ; sym g3
+and then it will react the item in the inert ([W] g1 : F a ~ beta1). So it
+will set
+ g1 := g ; sym g3
and what is g? Well it would ideally be a new goal of type (F a ~ beta2) but
-remember that we have this in our solved cache, and it is ... g2! In short we
+remember that we have this in our solved cache, and it is ... g2! In short we
created the evidence loop:
- g2 := g1 ; g3
+ g2 := g1 ; g3
g3 := refl
- g1 := g2 ; sym g3
+ g1 := g2 ; sym g3
-To avoid this situation we do not cache as solved any workitems (or inert)
-which did not really made a 'step' towards proving some goal. Solved's are
-just an optimization so we don't lose anything in terms of completeness of
+To avoid this situation we do not cache as solved any workitems (or inert)
+which did not really made a 'step' towards proving some goal. Solved's are
+just an optimization so we don't lose anything in terms of completeness of
solving.
\begin{code}
-solveOneFromTheOther :: String -- Info
- -> CtEvidence -- Inert
- -> Ct -- WorkItem
+solveOneFromTheOther :: String -- Info
+ -> CtEvidence -- Inert
+ -> Ct -- WorkItem
-> TcS InteractResult
--- Preconditions:
+-- Preconditions:
-- 1) inert and work item represent evidence for the /same/ predicate
-- 2) ip/class/irred evidence (no coercions) only
solveOneFromTheOther info ifl workItem
| isDerived wfl
= return (IRWorkItemConsumed ("Solved[DW] " ++ info))
- | isDerived ifl -- The inert item is Derived, we can just throw it away,
- -- The workItem is inert wrt earlier inert-set items,
- -- so it's safe to continue on from this point
+ | isDerived ifl -- The inert item is Derived, we can just throw it away,
+ -- The workItem is inert wrt earlier inert-set items,
+ -- so it's safe to continue on from this point
= return (IRInertConsumed ("Solved[DI] " ++ info))
-
+
| CtWanted { ctev_evar = ev_id } <- wfl
= do { setEvBind ev_id (ctEvTerm ifl); return (IRWorkItemConsumed ("Solved(w) " ++ info)) }
| CtWanted { ctev_evar = ev_id } <- ifl
= do { setEvBind ev_id (ctEvTerm wfl); return (IRInertConsumed ("Solved(g) " ++ info)) }
- | otherwise -- If both are Given, we already have evidence; no need to duplicate
+ | otherwise -- If both are Given, we already have evidence; no need to duplicate
-- But the work item *overrides* the inert item (hence IRReplace)
-- See Note [Shadowing of Implicit Parameters]
= return (IRReplace ("Replace(gg) " ++ info))
- where
+ where
wfl = cc_ev workItem
\end{code}
@@ -933,80 +926,80 @@ Note [Superclasses and recursive dictionaries]
ToDo: check overlap and delete redundant stuff
Right before adding a given into the inert set, we must
-produce some more work, that will bring the superclasses
-of the given into scope. The superclass constraints go into
-our worklist.
+produce some more work, that will bring the superclasses
+of the given into scope. The superclass constraints go into
+our worklist.
When we simplify a wanted constraint, if we first see a matching
-instance, we may produce new wanted work. To (1) avoid doing this work
-twice in the future and (2) to handle recursive dictionaries we may ``cache''
-this item as given into our inert set WITHOUT adding its superclass constraints,
+instance, we may produce new wanted work. To (1) avoid doing this work
+twice in the future and (2) to handle recursive dictionaries we may ``cache''
+this item as given into our inert set WITHOUT adding its superclass constraints,
otherwise we'd be in danger of creating a loop [In fact this was the exact reason
-for doing the isGoodRecEv check in an older version of the type checker].
+for doing the isGoodRecEv check in an older version of the type checker].
-But now we have added partially solved constraints to the worklist which may
-interact with other wanteds. Consider the example:
+But now we have added partially solved constraints to the worklist which may
+interact with other wanteds. Consider the example:
-Example 1:
+Example 1:
class Eq b => Foo a b --- 0-th selector
instance Eq a => Foo [a] a --- fooDFun
-and wanted (Foo [t] t). We are first going to see that the instance matches
+and wanted (Foo [t] t). We are first going to see that the instance matches
and create an inert set that includes the solved (Foo [t] t) but not its superclasses:
- d1 :_g Foo [t] t d1 := EvDFunApp fooDFun d3
+ d1 :_g Foo [t] t d1 := EvDFunApp fooDFun d3
Our work list is going to contain a new *wanted* goal
- d3 :_w Eq t
+ d3 :_w Eq t
-Ok, so how do we get recursive dictionaries, at all:
+Ok, so how do we get recursive dictionaries, at all:
Example 2:
data D r = ZeroD | SuccD (r (D r));
-
+
instance (Eq (r (D r))) => Eq (D r) where
ZeroD == ZeroD = True
(SuccD a) == (SuccD b) = a == b
_ == _ = False;
-
+
equalDC :: D [] -> D [] -> Bool;
equalDC = (==);
We need to prove (Eq (D [])). Here's how we go:
- d1 :_w Eq (D [])
+ d1 :_w Eq (D [])
by instance decl, holds if
- d2 :_w Eq [D []]
- where d1 = dfEqD d2
-
-*BUT* we have an inert set which gives us (no superclasses):
- d1 :_g Eq (D [])
-By the instance declaration of Eq we can show the 'd2' goal if
- d3 :_w Eq (D [])
- where d2 = dfEqList d3
- d1 = dfEqD d2
-Now, however this wanted can interact with our inert d1 to set:
- d3 := d1
-and solve the goal. Why was this interaction OK? Because, if we chase the
-evidence of d1 ~~> dfEqD d2 ~~-> dfEqList d3, so by setting d3 := d1 we
+ d2 :_w Eq [D []]
+ where d1 = dfEqD d2
+
+*BUT* we have an inert set which gives us (no superclasses):
+ d1 :_g Eq (D [])
+By the instance declaration of Eq we can show the 'd2' goal if
+ d3 :_w Eq (D [])
+ where d2 = dfEqList d3
+ d1 = dfEqD d2
+Now, however this wanted can interact with our inert d1 to set:
+ d3 := d1
+and solve the goal. Why was this interaction OK? Because, if we chase the
+evidence of d1 ~~> dfEqD d2 ~~-> dfEqList d3, so by setting d3 := d1 we
are really setting
- d3 := dfEqD2 (dfEqList d3)
-which is FINE because the use of d3 is protected by the instance function
-applications.
+ d3 := dfEqD2 (dfEqList d3)
+which is FINE because the use of d3 is protected by the instance function
+applications.
So, our strategy is to try to put solved wanted dictionaries into the
inert set along with their superclasses (when this is meaningful,
i.e. when new wanted goals are generated) but solve a wanted dictionary
from a given only in the case where the evidence variable of the
wanted is mentioned in the evidence of the given (recursively through
-the evidence binds) in a protected way: more instance function applications
+the evidence binds) in a protected way: more instance function applications
than superclass selectors.
Here are some more examples from GHC's previous type checker
-Example 3:
+Example 3:
This code arises in the context of "Scrap Your Boilerplate with Class"
class Sat a
@@ -1014,7 +1007,7 @@ This code arises in the context of "Scrap Your Boilerplate with Class"
instance Sat (ctx Char) => Data ctx Char -- dfunData1
instance (Sat (ctx [a]), Data ctx a) => Data ctx [a] -- dfunData2
- class Data Maybe a => Foo a
+ class Data Maybe a => Foo a
instance Foo t => Sat (Maybe t) -- dfunSat
@@ -1023,90 +1016,90 @@ This code arises in the context of "Scrap Your Boilerplate with Class"
instance Foo [Char] -- dfunFoo3
Consider generating the superclasses of the instance declaration
- instance Foo a => Foo [a]
+ instance Foo a => Foo [a]
So our problem is this
d0 :_g Foo t
- d1 :_w Data Maybe [t]
+ d1 :_w Data Maybe [t]
We may add the given in the inert set, along with its superclasses
-[assuming we don't fail because there is a matching instance, see
+[assuming we don't fail because there is a matching instance, see
topReactionsStage, given case ]
Inert:
- d0 :_g Foo t
- WorkList
- d01 :_g Data Maybe t -- d2 := EvDictSuperClass d0 0
- d1 :_w Data Maybe [t]
+ d0 :_g Foo t
+ WorkList
+ d01 :_g Data Maybe t -- d2 := EvDictSuperClass d0 0
+ d1 :_w Data Maybe [t]
Then d2 can readily enter the inert, and we also do solving of the wanted
- Inert:
- d0 :_g Foo t
- d1 :_s Data Maybe [t] d1 := dfunData2 d2 d3
+ Inert:
+ d0 :_g Foo t
+ d1 :_s Data Maybe [t] d1 := dfunData2 d2 d3
WorkList
- d2 :_w Sat (Maybe [t])
+ d2 :_w Sat (Maybe [t])
d3 :_w Data Maybe t
- d01 :_g Data Maybe t
-Now, we may simplify d2 more:
+ d01 :_g Data Maybe t
+Now, we may simplify d2 more:
Inert:
- d0 :_g Foo t
- d1 :_s Data Maybe [t] d1 := dfunData2 d2 d3
- d1 :_g Data Maybe [t]
- d2 :_g Sat (Maybe [t]) d2 := dfunSat d4
- WorkList:
- d3 :_w Data Maybe t
- d4 :_w Foo [t]
- d01 :_g Data Maybe t
+ d0 :_g Foo t
+ d1 :_s Data Maybe [t] d1 := dfunData2 d2 d3
+ d1 :_g Data Maybe [t]
+ d2 :_g Sat (Maybe [t]) d2 := dfunSat d4
+ WorkList:
+ d3 :_w Data Maybe t
+ d4 :_w Foo [t]
+ d01 :_g Data Maybe t
Now, we can just solve d3.
Inert
- d0 :_g Foo t
- d1 :_s Data Maybe [t] d1 := dfunData2 d2 d3
- d2 :_g Sat (Maybe [t]) d2 := dfunSat d4
+ d0 :_g Foo t
+ d1 :_s Data Maybe [t] d1 := dfunData2 d2 d3
+ d2 :_g Sat (Maybe [t]) d2 := dfunSat d4
WorkList
- d4 :_w Foo [t]
- d01 :_g Data Maybe t
+ d4 :_w Foo [t]
+ d01 :_g Data Maybe t
And now we can simplify d4 again, but since it has superclasses we *add* them to the worklist:
Inert
- d0 :_g Foo t
- d1 :_s Data Maybe [t] d1 := dfunData2 d2 d3
- d2 :_g Sat (Maybe [t]) d2 := dfunSat d4
- d4 :_g Foo [t] d4 := dfunFoo2 d5
+ d0 :_g Foo t
+ d1 :_s Data Maybe [t] d1 := dfunData2 d2 d3
+ d2 :_g Sat (Maybe [t]) d2 := dfunSat d4
+ d4 :_g Foo [t] d4 := dfunFoo2 d5
WorkList:
- d5 :_w Foo t
+ d5 :_w Foo t
d6 :_g Data Maybe [t] d6 := EvDictSuperClass d4 0
- d01 :_g Data Maybe t
-Now, d5 can be solved! (and its superclass enter scope)
+ d01 :_g Data Maybe t
+Now, d5 can be solved! (and its superclass enter scope)
Inert
- d0 :_g Foo t
- d1 :_s Data Maybe [t] d1 := dfunData2 d2 d3
- d2 :_g Sat (Maybe [t]) d2 := dfunSat d4
- d4 :_g Foo [t] d4 := dfunFoo2 d5
+ d0 :_g Foo t
+ d1 :_s Data Maybe [t] d1 := dfunData2 d2 d3
+ d2 :_g Sat (Maybe [t]) d2 := dfunSat d4
+ d4 :_g Foo [t] d4 := dfunFoo2 d5
d5 :_g Foo t d5 := dfunFoo1 d7
WorkList:
d7 :_w Data Maybe t
d6 :_g Data Maybe [t]
d8 :_g Data Maybe t d8 := EvDictSuperClass d5 0
- d01 :_g Data Maybe t
+ d01 :_g Data Maybe t
-Now, two problems:
- [1] Suppose we pick d8 and we react him with d01. Which of the two givens should
- we keep? Well, we *MUST NOT* drop d01 because d8 contains recursive evidence
+Now, two problems:
+ [1] Suppose we pick d8 and we react him with d01. Which of the two givens should
+ we keep? Well, we *MUST NOT* drop d01 because d8 contains recursive evidence
that must not be used (look at case interactInert where both inert and workitem
- are givens). So we have several options:
+ are givens). So we have several options:
- Drop the workitem always (this will drop d8)
This feels very unsafe -- what if the work item was the "good" one
that should be used later to solve another wanted?
- - Don't drop anyone: the inert set may contain multiple givens!
- [This is currently implemented]
+ - Don't drop anyone: the inert set may contain multiple givens!
+ [This is currently implemented]
-The "don't drop anyone" seems the most safe thing to do, so now we come to problem 2:
+The "don't drop anyone" seems the most safe thing to do, so now we come to problem 2:
[2] We have added both d6 and d01 in the inert set, and we are interacting our wanted
- d7. Now the [isRecDictEv] function in the ineration solver
- [case inert-given workitem-wanted] will prevent us from interacting d7 := d8
- precisely because chasing the evidence of d8 leads us to an unguarded use of d7.
+ d7. Now the [isRecDictEv] function in the ineration solver
+ [case inert-given workitem-wanted] will prevent us from interacting d7 := d8
+ precisely because chasing the evidence of d8 leads us to an unguarded use of d7.
+
+ So, no interaction happens there. Then we meet d01 and there is no recursion
+ problem there [isRectDictEv] gives us the OK to interact and we do solve d7 := d01!
- So, no interaction happens there. Then we meet d01 and there is no recursion
- problem there [isRectDictEv] gives us the OK to interact and we do solve d7 := d01!
-
Note [SUPERCLASS-LOOP 1]
~~~~~~~~~~~~~~~~~~~~~~~~
We have to be very, very careful when generating superclasses, lest we
@@ -1116,33 +1109,33 @@ accidentally build a loop. Here's an example:
class S a => C a where { opc :: a -> a }
class S b => D b where { opd :: b -> b }
-
+
instance C Int where
opc = opd
-
+
instance D Int where
opd = opc
From (instance C Int) we get the constraint set {ds1:S Int, dd:D Int}
Simplifying, we may well get:
- $dfCInt = :C ds1 (opd dd)
- dd = $dfDInt
- ds1 = $p1 dd
-Notice that we spot that we can extract ds1 from dd.
+ $dfCInt = :C ds1 (opd dd)
+ dd = $dfDInt
+ ds1 = $p1 dd
+Notice that we spot that we can extract ds1 from dd.
Alas! Alack! We can do the same for (instance D Int):
- $dfDInt = :D ds2 (opc dc)
- dc = $dfCInt
- ds2 = $p1 dc
+ $dfDInt = :D ds2 (opc dc)
+ dc = $dfCInt
+ ds2 = $p1 dc
And now we've defined the superclass in terms of itself.
Two more nasty cases are in
- tcrun021
- tcrun033
+ tcrun021
+ tcrun033
-Solution:
- - Satisfy the superclass context *all by itself*
+Solution:
+ - Satisfy the superclass context *all by itself*
(tcSimplifySuperClasses)
- And do so completely; i.e. no left-over constraints
to mix with the constraints arising from method declarations
@@ -1153,27 +1146,27 @@ Note [SUPERCLASS-LOOP 2]
We need to be careful when adding "the constaint we are trying to prove".
Suppose we are *given* d1:Ord a, and want to deduce (d2:C [a]) where
- class Ord a => C a where
- instance Ord [a] => C [a] where ...
+ class Ord a => C a where
+ instance Ord [a] => C [a] where ...
Then we'll use the instance decl to deduce C [a] from Ord [a], and then add the
superclasses of C [a] to avails. But we must not overwrite the binding
for Ord [a] (which is obtained from Ord a) with a superclass selection or we'll just
-build a loop!
+build a loop!
Here's another variant, immortalised in tcrun020
- class Monad m => C1 m
- class C1 m => C2 m x
- instance C2 Maybe Bool
+ class Monad m => C1 m
+ class C1 m => C2 m x
+ instance C2 Maybe Bool
For the instance decl we need to build (C1 Maybe), and it's no good if
-we run around and add (C2 Maybe Bool) and its superclasses to the avails
+we run around and add (C2 Maybe Bool) and its superclasses to the avails
before we search for C1 Maybe.
-Here's another example
- class Eq b => Foo a b
- instance Eq a => Foo [a] a
+Here's another example
+ class Eq b => Foo a b
+ instance Eq a => Foo [a] a
If we are reducing
- (Foo [t] t)
+ (Foo [t] t)
we'll first deduce that it holds (via the instance decl). We must not
then overwrite the Eq t constraint with a superclass selection!
@@ -1185,13 +1178,13 @@ I found a very obscure program (now tcrun021) in which improvement meant the
simplifier got two bites a the cherry... so something seemed to be an Stop
first time, but reducible next time.
-Now we implement the Right Solution, which is to check for loops directly
+Now we implement the Right Solution, which is to check for loops directly
when adding superclasses. It's a bit like the occurs check in unification.
Note [Recursive instances and superclases]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Consider this code, which arises in the context of "Scrap Your
-Boilerplate with Class".
+Consider this code, which arises in the context of "Scrap Your
+Boilerplate with Class".
class Sat a
class Data ctx a
@@ -1215,12 +1208,12 @@ So that leaves (Sat (Maybe [a])). Using the instance for Sat means
we need (Foo [a]). And that is the very dictionary we are bulding
an instance for! So we must put that in the "givens". So in this
case we have
- Given: Foo a, Foo [a]
- Wanted: Data Maybe [a]
+ Given: Foo a, Foo [a]
+ Wanted: Data Maybe [a]
BUT we must *not not not* put the *superclasses* of (Foo [a]) in
the givens, which is what 'addGiven' would normally do. Why? Because
-(Data Maybe [a]) is the superclass, so we'd "satisfy" the wanted
+(Data Maybe [a]) is the superclass, so we'd "satisfy" the wanted
by selecting a superclass from Foo [a], which simply makes a loop.
On the other hand we *must* put the superclasses of (Foo a) in
@@ -1228,7 +1221,7 @@ the givens, as you can see from the derivation described above.
Conclusion: in the very special case of tcSimplifySuperClasses
we have one 'given' (namely the "this" dictionary) whose superclasses
-must not be added to 'givens' by addGiven.
+must not be added to 'givens' by addGiven.
There is a complication though. Suppose there are equalities
instance (Eq a, a~b) => Num (a,b)
@@ -1242,28 +1235,28 @@ We need a persistent property of the dictionary to record this
special-ness. Current I'm using the InstLocOrigin (a bit of a hack,
but cool), which is maintained by dictionary normalisation.
Specifically, the InstLocOrigin is
- NoScOrigin
+ NoScOrigin
then the no-superclass thing kicks in. WATCH OUT if you fiddle
with InstLocOrigin!
Note [MATCHING-SYNONYMS]
~~~~~~~~~~~~~~~~~~~~~~~~
-When trying to match a dictionary (D tau) to a top-level instance, or a
-type family equation (F taus_1 ~ tau_2) to a top-level family instance,
+When trying to match a dictionary (D tau) to a top-level instance, or a
+type family equation (F taus_1 ~ tau_2) to a top-level family instance,
we do *not* need to expand type synonyms because the matcher will do that for us.
-Note [RHS-FAMILY-SYNONYMS]
+Note [RHS-FAMILY-SYNONYMS]
~~~~~~~~~~~~~~~~~~~~~~~~~~
-The RHS of a family instance is represented as yet another constructor which is
-like a type synonym for the real RHS the programmer declared. Eg:
- type instance F (a,a) = [a]
-Becomes:
+The RHS of a family instance is represented as yet another constructor which is
+like a type synonym for the real RHS the programmer declared. Eg:
+ type instance F (a,a) = [a]
+Becomes:
:R32 a = [a] -- internal type synonym introduced
- F (a,a) ~ :R32 a -- instance
+ F (a,a) ~ :R32 a -- instance
-When we react a family instance with a type family equation in the work list
-we keep the synonym-using RHS without expansion.
+When we react a family instance with a type family equation in the work list
+we keep the synonym-using RHS without expansion.
%************************************************************************
@@ -1278,18 +1271,18 @@ constraint right away. This avoids two dangers
Danger 1: If we send the original constraint on down the pipeline
it may react with an instance declaration, and in delicate
- situations (when a Given overlaps with an instance) that
- may produce new insoluble goals: see Trac #4952
+ situations (when a Given overlaps with an instance) that
+ may produce new insoluble goals: see Trac #4952
Danger 2: If we don't rewrite the constraint, it may re-react
with the same thing later, and produce the same equality
again --> termination worries.
To achieve this required some refactoring of FunDeps.lhs (nicer
-now!).
+now!).
\begin{code}
-rewriteWithFunDeps :: [Equation] -> CtLoc -> TcS [Ct]
+rewriteWithFunDeps :: [Equation] -> CtLoc -> TcS [Ct]
-- NB: The returned constraints are all Derived
-- Post: returns no trivial equalities (identities) and all EvVars returned are fresh
rewriteWithFunDeps eqn_pred_locs loc
@@ -1302,88 +1295,88 @@ instFunDepEqn loc (FDEqn { fd_qtvs = tvs, fd_eqs = eqs
, fd_pred1 = d1, fd_pred2 = d2 })
= do { (subst, _) <- instFlexiTcS tvs -- Takes account of kind substitution
; foldM (do_one subst) [] eqs }
- where
+ where
der_loc = pushErrCtxt FunDepOrigin (False, mkEqnMsg d1 d2) loc
do_one subst ievs (FDEq { fd_ty_left = ty1, fd_ty_right = ty2 })
- | eqType sty1 sty2
+ | eqType sty1 sty2
= return ievs -- Return no trivial equalities
| otherwise
= do { mb_eqv <- newDerived (mkTcEqPred sty1 sty2)
; case mb_eqv of
Just ev -> return (mkNonCanonical der_loc ev : ievs)
Nothing -> return ievs }
- -- We are eventually going to emit FD work back in the work list so
- -- it is important that we only return the /freshly created/ and not
+ -- We are eventually going to emit FD work back in the work list so
+ -- it is important that we only return the /freshly created/ and not
-- some existing equality!
where
- sty1 = Type.substTy subst ty1
- sty2 = Type.substTy subst ty2
+ sty1 = Type.substTy subst ty1
+ sty2 = Type.substTy subst ty2
-mkEqnMsg :: (TcPredType, SDoc)
+mkEqnMsg :: (TcPredType, SDoc)
-> (TcPredType, SDoc) -> TidyEnv -> TcM (TidyEnv, SDoc)
mkEqnMsg (pred1,from1) (pred2,from2) tidy_env
= do { zpred1 <- zonkTcPredType pred1
; zpred2 <- zonkTcPredType pred2
- ; let { tpred1 = tidyType tidy_env zpred1
+ ; let { tpred1 = tidyType tidy_env zpred1
; tpred2 = tidyType tidy_env zpred2 }
- ; let msg = vcat [ptext (sLit "When using functional dependencies to combine"),
- nest 2 (sep [ppr tpred1 <> comma, nest 2 from1]),
- nest 2 (sep [ppr tpred2 <> comma, nest 2 from2])]
- ; return (tidy_env, msg) }
+ ; let msg = vcat [ptext (sLit "When using functional dependencies to combine"),
+ nest 2 (sep [ppr tpred1 <> comma, nest 2 from1]),
+ nest 2 (sep [ppr tpred2 <> comma, nest 2 from2])]
+ ; return (tidy_env, msg) }
\end{code}
*********************************************************************************
-* *
+* *
The top-reaction Stage
* *
*********************************************************************************
\begin{code}
topReactionsStage :: WorkItem -> TcS StopOrContinue
-topReactionsStage wi
+topReactionsStage wi
= do { inerts <- getTcSInerts
; tir <- doTopReact inerts wi
- ; case tir of
+ ; case tir of
NoTopInt -> return (ContinueWith wi)
- SomeTopInt rule what_next
+ SomeTopInt rule what_next
-> do { traceFireTcS wi $
vcat [ ptext (sLit "Top react:") <+> text rule
, text "WorkItem =" <+> ppr wi ]
; return what_next } }
-data TopInteractResult
+data TopInteractResult
= NoTopInt
| SomeTopInt { tir_rule :: String, tir_new_item :: StopOrContinue }
doTopReact :: InertSet -> WorkItem -> TcS TopInteractResult
--- The work item does not react with the inert set, so try interaction with top-level
+-- The work item does not react with the inert set, so try interaction with top-level
-- instances. Note:
--
--- (a) The place to add superclasses in not here in doTopReact stage.
+-- (a) The place to add superclasses in not here in doTopReact stage.
-- Instead superclasses are added in the worklist as part of the
-- canonicalization process. See Note [Adding superclasses].
--
--- (b) See Note [Given constraint that matches an instance declaration]
--- for some design decisions for given dictionaries.
+-- (b) See Note [Given constraint that matches an instance declaration]
+-- for some design decisions for given dictionaries.
doTopReact inerts workItem
= do { traceTcS "doTopReact" (ppr workItem)
; case workItem of
- CDictCan { cc_ev = fl, cc_class = cls, cc_tyargs = xis
- , cc_loc = d }
- -> doTopReactDict inerts fl cls xis d
+ CDictCan { cc_ev = fl, cc_class = cls, cc_tyargs = xis
+ , cc_loc = d }
+ -> doTopReactDict inerts fl cls xis d
- CFunEqCan { cc_ev = fl, cc_fun = tc, cc_tyargs = args
- , cc_rhs = xi, cc_loc = d }
- -> doTopReactFunEq workItem fl tc args xi d
+ CFunEqCan { cc_ev = fl, cc_fun = tc, cc_tyargs = args
+ , cc_rhs = xi, cc_loc = d }
+ -> doTopReactFunEq workItem fl tc args xi d
- _ -> -- Any other work item does not react with any top-level equations
- return NoTopInt }
+ _ -> -- Any other work item does not react with any top-level equations
+ return NoTopInt }
--------------------
doTopReactDict :: InertSet -> CtEvidence -> Class -> [Xi]
@@ -1393,33 +1386,33 @@ doTopReactDict inerts fl cls xis loc
= try_fundeps_and_return
| Just ev <- lookupSolvedDict inerts pred -- Cached
- = do { setEvBind dict_id (ctEvTerm ev);
- ; return $ SomeTopInt { tir_rule = "Dict/Top (cached)"
- , tir_new_item = Stop } }
+ = do { setEvBind dict_id (ctEvTerm ev);
+ ; return $ SomeTopInt { tir_rule = "Dict/Top (cached)"
+ , tir_new_item = Stop } }
| otherwise -- Not cached
= do { lkup_inst_res <- matchClassInst inerts cls xis loc
; case lkup_inst_res of
- GenInst wtvs ev_term -> do { addSolvedDict fl
+ GenInst wtvs ev_term -> do { addSolvedDict fl
; solve_from_instance wtvs ev_term }
NoInstance -> try_fundeps_and_return }
- where
+ where
arising_sdoc = pprArisingAt loc
dict_id = ctEvId fl
pred = mkClassPred cls xis
-
+
solve_from_instance :: [CtEvidence] -> EvTerm -> TcS TopInteractResult
-- Precondition: evidence term matches the predicate workItem
- solve_from_instance evs ev_term
+ solve_from_instance evs ev_term
| null evs
= do { traceTcS "doTopReact/found nullary instance for" $
ppr dict_id
; setEvBind dict_id ev_term
- ; return $
- SomeTopInt { tir_rule = "Dict/Top (solved, no new work)"
+ ; return $
+ SomeTopInt { tir_rule = "Dict/Top (solved, no new work)"
, tir_new_item = Stop } }
- | otherwise
- = do { traceTcS "doTopReact/found non-nullary instance for" $
+ | otherwise
+ = do { traceTcS "doTopReact/found non-nullary instance for" $
ppr dict_id
; setEvBind dict_id ev_term
; let mk_new_wanted ev
@@ -1430,24 +1423,24 @@ doTopReactDict inerts fl cls xis loc
SomeTopInt { tir_rule = "Dict/Top (solved, more work)"
, tir_new_item = Stop } }
- -- We didn't solve it; so try functional dependencies with
+ -- We didn't solve it; so try functional dependencies with
-- the instance environment, and return
-- NB: even if there *are* some functional dependencies against the
- -- instance environment, there might be a unique match, and if
+ -- instance environment, there might be a unique match, and if
-- so we make sure we get on and solve it first. See Note [Weird fundeps]
try_fundeps_and_return
- = do { instEnvs <- getInstEnvs
+ = do { instEnvs <- getInstEnvs
; let fd_eqns = improveFromInstEnv instEnvs (pred, arising_sdoc)
; fd_work <- rewriteWithFunDeps fd_eqns loc
; unless (null fd_work) (updWorkListTcS (extendWorkListEqs fd_work))
; return NoTopInt }
-
+
--------------------
doTopReactFunEq :: Ct -> CtEvidence -> TyCon -> [Xi] -> Xi
-> CtLoc -> TcS TopInteractResult
doTopReactFunEq _ct fl fun_tc args xi loc
= ASSERT(isSynFamilyTyCon fun_tc) -- No associated data families have
- -- reached this far
+ -- reached this far
-- Look in the cache of solved funeqs
do { fun_eq_cache <- getTcSInerts >>= (return . inert_solved_funeqs)
; case lookupFamHead fun_eq_cache fam_ty of {
@@ -1455,7 +1448,7 @@ doTopReactFunEq _ct fl fun_tc args xi loc
| ctEvFlavour ctev `canRewrite` ctEvFlavour fl
-> ASSERT( not (isDerived ctev) )
succeed_with "Fun/Cache" (evTermCoercion (ctEvTerm ctev)) rhs_ty ;
- _other ->
+ _other ->
-- Look up in top-level instances, or built-in axiom
do { match_res <- matchFam fun_tc args -- See Note [MATCHING-SYNONYMS]
@@ -1493,7 +1486,7 @@ doTopReactFunEq _ct fl fun_tc args xi loc
CNonCanonical { cc_ev = ctev
, cc_loc = bumpCtLocDepth loc }
ctevs -> -- No subgoal (because it's cached)
- ASSERT( null ctevs) return ()
+ ASSERT( null ctevs) return ()
; return $ SomeTopInt { tir_rule = str
, tir_new_item = Stop } }
where
@@ -1504,32 +1497,32 @@ doTopReactFunEq _ct fl fun_tc args xi loc
\end{code}
-Note [FunDep and implicit parameter reactions]
+Note [FunDep and implicit parameter reactions]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Currently, our story of interacting two dictionaries (or a dictionary
and top-level instances) for functional dependencies, and implicit
paramters, is that we simply produce new Derived equalities. So for example
- class D a b | a -> b where ...
- Inert:
+ class D a b | a -> b where ...
+ Inert:
d1 :g D Int Bool
- WorkItem:
+ WorkItem:
d2 :w D Int alpha
We generate the extra work item
cv :d alpha ~ Bool
- where 'cv' is currently unused. However, this new item can perhaps be
+ where 'cv' is currently unused. However, this new item can perhaps be
spontaneously solved to become given and react with d2,
discharging it in favour of a new constraint d2' thus:
d2' :w D Int Bool
- d2 := d2' |> D Int cv
+ d2 := d2' |> D Int cv
Now d2' can be discharged from d1
-We could be more aggressive and try to *immediately* solve the dictionary
-using those extra equalities, but that requires those equalities to carry
+We could be more aggressive and try to *immediately* solve the dictionary
+using those extra equalities, but that requires those equalities to carry
evidence and derived do not carry evidence.
-If that were the case with the same inert set and work item we might dischard
+If that were the case with the same inert set and work item we might dischard
d2 directly:
cv :w alpha ~ Bool
@@ -1537,16 +1530,16 @@ d2 directly:
But in general it's a bit painful to figure out the necessary coercion,
so we just take the first approach. Here is a better example. Consider:
- class C a b c | a -> b
-And:
- [Given] d1 : C T Int Char
- [Wanted] d2 : C T beta Int
-In this case, it's *not even possible* to solve the wanted immediately.
+ class C a b c | a -> b
+And:
+ [Given] d1 : C T Int Char
+ [Wanted] d2 : C T beta Int
+In this case, it's *not even possible* to solve the wanted immediately.
So we should simply output the functional dependency and add this guy
-[but NOT its superclasses] back in the worklist. Even worse:
- [Given] d1 : C T Int beta
- [Wanted] d2: C T beta Int
-Then it is solvable, but its very hard to detect this on the spot.
+[but NOT its superclasses] back in the worklist. Even worse:
+ [Given] d1 : C T Int beta
+ [Wanted] d2: C T beta Int
+Then it is solvable, but its very hard to detect this on the spot.
It's exactly the same with implicit parameters, except that the
"aggressive" approach would be much easier to implement.
@@ -1558,8 +1551,8 @@ We fire an improvement rule when
* Two constraints match (modulo the fundep)
e.g. C t1 t2, C t1 t3 where C a b | a->b
The two match because the first arg is identical
-
-Note that we *do* fire the improvement if one is Given and one is Derived (e.g. a
+
+Note that we *do* fire the improvement if one is Given and one is Derived (e.g. a
superclass of a Wanted goal) or if both are Given.
Example (tcfail138)
@@ -1578,24 +1571,24 @@ Use the instance decl to get
The (C a b') is inert, so we generate its Derived superclasses (L a b'),
and now we need improvement between that derived superclass an the Given (L a b)
-Test typecheck/should_fail/FDsFromGivens also shows why it's a good idea to
-emit Derived FDs for givens as well.
+Test typecheck/should_fail/FDsFromGivens also shows why it's a good idea to
+emit Derived FDs for givens as well.
Note [Weird fundeps]
~~~~~~~~~~~~~~~~~~~~
Consider class Het a b | a -> b where
het :: m (f c) -> a -> m b
- class GHet (a :: * -> *) (b :: * -> *) | a -> b
- instance GHet (K a) (K [a])
- instance Het a b => GHet (K a) (K b)
+ class GHet (a :: * -> *) (b :: * -> *) | a -> b
+ instance GHet (K a) (K [a])
+ instance Het a b => GHet (K a) (K b)
The two instances don't actually conflict on their fundeps,
although it's pretty strange. So they are both accepted. Now
try [W] GHet (K Int) (K Bool)
-This triggers fudeps from both instance decls; but it also
+This triggers fudeps from both instance decls; but it also
matches a *unique* instance decl, and we should go ahead and
-pick that one right now. Otherwise, if we don't, it ends up
+pick that one right now. Otherwise, if we don't, it ends up
unsolved in the inert set and is reported as an error.
Trac #7875 is a case in point.
@@ -1604,8 +1597,8 @@ Note [Overriding implicit parameters]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider
f :: (?x::a) -> Bool -> a
-
- g v = let ?x::Int = 3
+
+ g v = let ?x::Int = 3
in (f v, let ?x::Bool = True in f v)
This should probably be well typed, with
@@ -1616,115 +1609,115 @@ Hence a work-item Given overrides an inert-item Given.
Note [Given constraint that matches an instance declaration]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-What should we do when we discover that one (or more) top-level
-instances match a given (or solved) class constraint? We have
+What should we do when we discover that one (or more) top-level
+instances match a given (or solved) class constraint? We have
two possibilities:
1. Reject the program. The reason is that there may not be a unique
best strategy for the solver. Example, from the OutsideIn(X) paper:
- instance P x => Q [x]
- instance (x ~ y) => R [x] y
-
- wob :: forall a b. (Q [b], R b a) => a -> Int
-
- g :: forall a. Q [a] => [a] -> Int
- g x = wob x
-
- will generate the impliation constraint:
- Q [a] => (Q [beta], R beta [a])
- If we react (Q [beta]) with its top-level axiom, we end up with a
- (P beta), which we have no way of discharging. On the other hand,
- if we react R beta [a] with the top-level we get (beta ~ a), which
- is solvable and can help us rewrite (Q [beta]) to (Q [a]) which is
- now solvable by the given Q [a].
-
- However, this option is restrictive, for instance [Example 3] from
- Note [Recursive instances and superclases] will fail to work.
+ instance P x => Q [x]
+ instance (x ~ y) => R [x] y
+
+ wob :: forall a b. (Q [b], R b a) => a -> Int
+
+ g :: forall a. Q [a] => [a] -> Int
+ g x = wob x
+
+ will generate the impliation constraint:
+ Q [a] => (Q [beta], R beta [a])
+ If we react (Q [beta]) with its top-level axiom, we end up with a
+ (P beta), which we have no way of discharging. On the other hand,
+ if we react R beta [a] with the top-level we get (beta ~ a), which
+ is solvable and can help us rewrite (Q [beta]) to (Q [a]) which is
+ now solvable by the given Q [a].
+
+ However, this option is restrictive, for instance [Example 3] from
+ Note [Recursive instances and superclases] will fail to work.
2. Ignore the problem, hoping that the situations where there exist indeed
- such multiple strategies are rare: Indeed the cause of the previous
- problem is that (R [x] y) yields the new work (x ~ y) which can be
- *spontaneously* solved, not using the givens.
+ such multiple strategies are rare: Indeed the cause of the previous
+ problem is that (R [x] y) yields the new work (x ~ y) which can be
+ *spontaneously* solved, not using the givens.
We are choosing option 2 below but we might consider having a flag as well.
-Note [New Wanted Superclass Work]
+Note [New Wanted Superclass Work]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Even in the case of wanted constraints, we may add some superclasses
-as new given work. The reason is:
-
- To allow FD-like improvement for type families. Assume that
- we have a class
- class C a b | a -> b
- and we have to solve the implication constraint:
- C a b => C a beta
- Then, FD improvement can help us to produce a new wanted (beta ~ b)
-
- We want to have the same effect with the type family encoding of
- functional dependencies. Namely, consider:
- class (F a ~ b) => C a b
- Now suppose that we have:
- given: C a b
- wanted: C a beta
- By interacting the given we will get given (F a ~ b) which is not
- enough by itself to make us discharge (C a beta). However, we
+Even in the case of wanted constraints, we may add some superclasses
+as new given work. The reason is:
+
+ To allow FD-like improvement for type families. Assume that
+ we have a class
+ class C a b | a -> b
+ and we have to solve the implication constraint:
+ C a b => C a beta
+ Then, FD improvement can help us to produce a new wanted (beta ~ b)
+
+ We want to have the same effect with the type family encoding of
+ functional dependencies. Namely, consider:
+ class (F a ~ b) => C a b
+ Now suppose that we have:
+ given: C a b
+ wanted: C a beta
+ By interacting the given we will get given (F a ~ b) which is not
+ enough by itself to make us discharge (C a beta). However, we
may create a new derived equality from the super-class of the
- wanted constraint (C a beta), namely derived (F a ~ beta).
- Now we may interact this with given (F a ~ b) to get:
- derived : beta ~ b
- But 'beta' is a touchable unification variable, and hence OK to
- unify it with 'b', replacing the derived evidence with the identity.
+ wanted constraint (C a beta), namely derived (F a ~ beta).
+ Now we may interact this with given (F a ~ b) to get:
+ derived : beta ~ b
+ But 'beta' is a touchable unification variable, and hence OK to
+ unify it with 'b', replacing the derived evidence with the identity.
This requires trySpontaneousSolve to solve *derived*
equalities that have a touchable in their RHS, *in addition*
to solving wanted equalities.
-We also need to somehow use the superclasses to quantify over a minimal,
+We also need to somehow use the superclasses to quantify over a minimal,
constraint see note [Minimize by Superclasses] in TcSimplify.
-Finally, here is another example where this is useful.
+Finally, here is another example where this is useful.
Example 1:
----------
- class (F a ~ b) => C a b
+ class (F a ~ b) => C a b
And we are given the wanteds:
- w1 : C a b
- w2 : C a c
- w3 : b ~ c
+ w1 : C a b
+ w2 : C a c
+ w3 : b ~ c
We surely do *not* want to quantify over (b ~ c), since if someone provides
-dictionaries for (C a b) and (C a c), these dictionaries can provide a proof
-of (b ~ c), hence no extra evidence is necessary. Here is what will happen:
+dictionaries for (C a b) and (C a c), these dictionaries can provide a proof
+of (b ~ c), hence no extra evidence is necessary. Here is what will happen:
- Step 1: We will get new *given* superclass work,
+ Step 1: We will get new *given* superclass work,
provisionally to our solving of w1 and w2
-
- g1: F a ~ b, g2 : F a ~ c,
+
+ g1: F a ~ b, g2 : F a ~ c,
w1 : C a b, w2 : C a c, w3 : b ~ c
- The evidence for g1 and g2 is a superclass evidence term:
+ The evidence for g1 and g2 is a superclass evidence term:
g1 := sc w1, g2 := sc w2
- Step 2: The givens will solve the wanted w3, so that
- w3 := sym (sc w1) ; sc w2
-
+ Step 2: The givens will solve the wanted w3, so that
+ w3 := sym (sc w1) ; sc w2
+
Step 3: Now, one may naively assume that then w2 can be solve from w1
- after rewriting with the (now solved equality) (b ~ c).
-
- But this rewriting is ruled out by the isGoodRectDict!
+ after rewriting with the (now solved equality) (b ~ c).
+
+ But this rewriting is ruled out by the isGoodRectDict!
-Conclusion, we will (correctly) end up with the unsolved goals
- (C a b, C a c)
+Conclusion, we will (correctly) end up with the unsolved goals
+ (C a b, C a c)
-NB: The desugarer needs be more clever to deal with equalities
- that participate in recursive dictionary bindings.
+NB: The desugarer needs be more clever to deal with equalities
+ that participate in recursive dictionary bindings.
\begin{code}
data LookupInstResult
= NoInstance
- | GenInst [CtEvidence] EvTerm
+ | GenInst [CtEvidence] EvTerm
instance Outputable LookupInstResult where
ppr NoInstance = text "NoInstance"
@@ -1786,38 +1779,38 @@ matchClassInst inerts clas tys loc
, text "untouchables=" <+> ppr untch ]
; instEnvs <- getInstEnvs
; case lookupInstEnv instEnvs clas tys of
- ([], _, _) -- Nothing matches
- -> do { traceTcS "matchClass not matching" $
+ ([], _, _) -- Nothing matches
+ -> do { traceTcS "matchClass not matching" $
vcat [ text "dict" <+> ppr pred ]
; return NoInstance }
- ([(ispec, inst_tys)], [], _) -- A single match
+ ([(ispec, inst_tys)], [], _) -- A single match
| not (xopt Opt_IncoherentInstances dflags)
- , given_overlap untch
+ , given_overlap untch
-> -- See Note [Instance and Given overlap]
- do { traceTcS "Delaying instance application" $
+ do { traceTcS "Delaying instance application" $
vcat [ text "Workitem=" <+> pprType (mkClassPred clas tys)
, text "Relevant given dictionaries=" <+> ppr givens_for_this_clas ]
; return NoInstance }
| otherwise
- -> do { let dfun_id = instanceDFunId ispec
- ; traceTcS "matchClass success" $
- vcat [text "dict" <+> ppr pred,
+ -> do { let dfun_id = instanceDFunId ispec
+ ; traceTcS "matchClass success" $
+ vcat [text "dict" <+> ppr pred,
text "witness" <+> ppr dfun_id
<+> ppr (idType dfun_id) ]
- -- Record that this dfun is needed
+ -- Record that this dfun is needed
; match_one dfun_id inst_tys }
- (matches, _, _) -- More than one matches
+ (matches, _, _) -- More than one matches
-- Defer any reactions of a multitude
- -- until we learn more about the reagent
- -> do { traceTcS "matchClass multiple matches, deferring choice" $
+ -- until we learn more about the reagent
+ -> do { traceTcS "matchClass multiple matches, deferring choice" $
vcat [text "dict" <+> ppr pred,
text "matches" <+> ppr matches]
; return NoInstance } }
- where
- pred = mkClassPred clas tys
+ where
+ pred = mkClassPred clas tys
match_one :: DFunId -> [Maybe TcType] -> TcS LookupInstResult
-- See Note [DFunInstType: instantiating types] in InstEnv
@@ -1830,13 +1823,13 @@ matchClassInst inerts clas tys loc
else do
{ evc_vars <- instDFunConstraints theta
; let new_ev_vars = freshGoals evc_vars
- -- new_ev_vars are only the real new variables that can be emitted
+ -- new_ev_vars are only the real new variables that can be emitted
dfun_app = EvDFunApp dfun_id tys (getEvTerms evc_vars)
; return $ GenInst new_ev_vars dfun_app } }
givens_for_this_clas :: Cts
- givens_for_this_clas
- = lookupUFM (cts_given (inert_dicts $ inert_cans inerts)) clas
+ givens_for_this_clas
+ = lookupUFM (cts_given (inert_dicts $ inert_cans inerts)) clas
`orElse` emptyCts
given_overlap :: Untouchables -> Bool
@@ -1846,7 +1839,7 @@ matchClassInst inerts clas tys loc
, cc_ev = fl })
| isGiven fl
= ASSERT( clas_g == clas )
- case tcUnifyTys (\tv -> if isTouchableMetaTyVar untch tv &&
+ case tcUnifyTys (\tv -> if isTouchableMetaTyVar untch tv &&
tv `elemVarSet` tyVarsOfTypes tys
then BindMe else Skolem) tys sys of
-- We can't learn anything more about any variable at this point, so the only
@@ -1855,7 +1848,7 @@ matchClassInst inerts clas tys loc
-- we use tcUnifyTys instead of tcMatchTys to rule out cyclic substitutions.
Nothing -> False
Just _ -> True
- | otherwise = False -- No overlap with a solved, already been taken care of
+ | otherwise = False -- No overlap with a solved, already been taken care of
-- by the overlap check with the instance environment.
matchable _tys ct = pprPanic "Expecting dictionary!" (ppr ct)
@@ -1890,7 +1883,7 @@ getCoercibleInst safeMode rdr_env ty1 ty2
not (isRecursiveTyCon tc),
dataConsInScope rdr_env tc -- Do noot look at all tyConsOfTyCon
= do markDataConsAsUsed rdr_env tc
- let concTy = newTyConInstRhs tc tyArgs
+ let concTy = newTyConInstRhs tc tyArgs
ct_ev <- requestCoercible concTy ty2
return $ GenInst (freshGoals [ct_ev])
$ EvCoercible (EvCoercibleNewType CLeft tc tyArgs (getEvTerm ct_ev))
@@ -1900,7 +1893,7 @@ getCoercibleInst safeMode rdr_env ty1 ty2
not (isRecursiveTyCon tc),
dataConsInScope rdr_env tc -- Do noot look at all tyConsOfTyCon
= do markDataConsAsUsed rdr_env tc
- let concTy = newTyConInstRhs tc tyArgs
+ let concTy = newTyConInstRhs tc tyArgs
ct_ev <- requestCoercible ty1 concTy
return $ GenInst (freshGoals [ct_ev])
$ EvCoercible (EvCoercibleNewType CRight tc tyArgs (getEvTerm ct_ev))
@@ -1932,7 +1925,7 @@ markDataConsAsUsed rdr_env tc = addUsedRdrNamesTcS
, Imported (imp_spec:_) <- [gre_prov (head gres)] ]
requestCoercible :: TcType -> TcType -> TcS MaybeNew
-requestCoercible ty1 ty2 = newWantedEvVar (coercibleClass `mkClassPred` [ty1, ty2])
+requestCoercible ty1 ty2 = newWantedEvVar (coercibleClass `mkClassPred` [ty1, ty2])
\end{code}
@@ -1961,9 +1954,9 @@ are present:
instance Coercible a r => Coercible a (NT t1 t2 ...)
for a newtype constructor NT where
* NT is not recursive
- * r is the concrete type of NT, instantiated with the arguments t1 t2 ...
+ * r is the concrete type of NT, instantiated with the arguments t1 t2 ...
* the data constructors of NT are in scope.
-
+
These three shapes of instances correspond to the three constructors of
EvCoercible (defined in EvEvidence). They are assembled here and turned to Core
by dsEvTerm in DsBinds.
@@ -1973,38 +1966,38 @@ Note [Instance and Given overlap]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Assume that we have an inert set that looks as follows:
[Given] D [Int]
-And an instance declaration:
+And an instance declaration:
instance C a => D [a]
-A new wanted comes along of the form:
+A new wanted comes along of the form:
[Wanted] D [alpha]
-One possibility is to apply the instance declaration which will leave us
-with an unsolvable goal (C alpha). However, later on a new constraint may
-arise (for instance due to a functional dependency between two later dictionaries),
-that will add the equality (alpha ~ Int), in which case our ([Wanted] D [alpha])
-will be transformed to [Wanted] D [Int], which could have been discharged by the given.
+One possibility is to apply the instance declaration which will leave us
+with an unsolvable goal (C alpha). However, later on a new constraint may
+arise (for instance due to a functional dependency between two later dictionaries),
+that will add the equality (alpha ~ Int), in which case our ([Wanted] D [alpha])
+will be transformed to [Wanted] D [Int], which could have been discharged by the given.
-The solution is that in matchClassInst and eventually in topReact, we get back with
+The solution is that in matchClassInst and eventually in topReact, we get back with
a matching instance, only when there is no Given in the inerts which is unifiable to
this particular dictionary.
-The end effect is that, much as we do for overlapping instances, we delay choosing a
-class instance if there is a possibility of another instance OR a given to match our
+The end effect is that, much as we do for overlapping instances, we delay choosing a
+class instance if there is a possibility of another instance OR a given to match our
constraint later on. This fixes bugs #4981 and #5002.
-This is arguably not easy to appear in practice due to our aggressive prioritization
-of equality solving over other constraints, but it is possible. I've added a test case
+This is arguably not easy to appear in practice due to our aggressive prioritization
+of equality solving over other constraints, but it is possible. I've added a test case
in typecheck/should-compile/GivenOverlapping.hs
We ignore the overlap problem if -XIncoherentInstances is in force: see
Trac #6002 for a worked-out example where this makes a difference.
-Moreover notice that our goals here are different than the goals of the top-level
+Moreover notice that our goals here are different than the goals of the top-level
overlapping checks. There we are interested in validating the following principle:
-
+
If we inline a function f at a site where the same global instance environment
- is available as the instance environment at the definition site of f then we
- should get the same behaviour.
+ is available as the instance environment at the definition site of f then we
+ should get the same behaviour.
-But for the Given Overlap check our goal is just related to completeness of
-constraint solving.
+But for the Given Overlap check our goal is just related to completeness of
+constraint solving.
diff --git a/compiler/typecheck/TcRnTypes.lhs b/compiler/typecheck/TcRnTypes.lhs
index 41da1d4f7dbc..46abfa879c3e 100644
--- a/compiler/typecheck/TcRnTypes.lhs
+++ b/compiler/typecheck/TcRnTypes.lhs
@@ -366,7 +366,7 @@ We gather two sorts of usage information
(see RnNames.reportUnusedNames)
(b) to generate version-tracking usage info in interface
files (see MkIface.mkUsedNames)
- This usage info is mainly gathered by the renamer's
+ This usage info is mainly gathered by the renamer's
gathering of free-variables
* tcg_used_rdrnames
@@ -374,7 +374,7 @@ We gather two sorts of usage information
Used only to report unused import declarations
Notice that they are RdrNames, not Names, so we can
tell whether the reference was qualified or unqualified, which
- is esssential in deciding whether a particular import decl
+ is esssential in deciding whether a particular import decl
is unnecessary. This info isn't present in Names.
@@ -484,9 +484,9 @@ data TcLclEnv -- Changes as we move inside an expression
type TcTypeEnv = NameEnv TcTyThing
-data TcIdBinder
- = TcIdBndr
- TcId
+data TcIdBinder
+ = TcIdBndr
+ TcId
TopLevelFlag -- Tells whether the bindind is syntactically top-level
-- (The monomorphic Ids for a recursive group count
-- as not-top-level for this purpose.)
@@ -869,7 +869,7 @@ The @WhereFrom@ type controls where the renamer looks for an interface file
data WhereFrom
= ImportByUser IsBootInterface -- Ordinary user import (perhaps {-# SOURCE #-})
| ImportBySystem -- Non user import.
- | ImportByPlugin -- Importing a plugin;
+ | ImportByPlugin -- Importing a plugin;
-- See Note [Care with plugin imports] in LoadIface
instance Outputable WhereFrom where
@@ -914,7 +914,7 @@ data Ct
| CIrredEvCan { -- These stand for yet-unusable predicates
cc_ev :: CtEvidence, -- See Note [Ct/evidence invariant]
- -- The ctev_pred of the evidence is
+ -- The ctev_pred of the evidence is
-- of form (tv xi1 xi2 ... xin)
-- or (tv1 ~ ty2) where the CTyEqCan kind invariant fails
-- or (F tys ~ ty) where the CFunEqCan kind invariant fails
@@ -993,14 +993,14 @@ Eg wanted1 rewrites wanted2; if both were compatible kinds before,
wanted2 will be afterwards. Similarly givens.
Caveat:
- - Givens from higher-rank, such as:
- type family T b :: * -> * -> *
- type instance T Bool = (->)
+ - Givens from higher-rank, such as:
+ type family T b :: * -> * -> *
+ type instance T Bool = (->)
- f :: forall a. ((T a ~ (->)) => ...) -> a -> ...
- flop = f (...) True
- Whereas we would be able to apply the type instance, we would not be able to
- use the given (T Bool ~ (->)) in the body of 'flop'
+ f :: forall a. ((T a ~ (->)) => ...) -> a -> ...
+ flop = f (...) True
+ Whereas we would be able to apply the type instance, we would not be able to
+ use the given (T Bool ~ (->)) in the body of 'flop'
Note [CIrredEvCan constraints]
@@ -1011,12 +1011,12 @@ CIrredEvCan constraints are used for constraints that are "stuck"
- but they may become soluble if we substitute for some
of the type variables in the constraint
-Example 1: (c Int), where c :: * -> Constraint. We can't do anything
+Example 1: (c Int), where c :: * -> Constraint. We can't do anything
with this yet, but if later c := Num, *then* we can solve it
Example 2: a ~ b, where a :: *, b :: k, where k is a kind variable
We don't want to use this to substitute 'b' for 'a', in case
- 'k' is subequently unifed with (say) *->*, because then
+ 'k' is subequently unifed with (say) *->*, because then
we'd have ill-kinded types floating about. Rather we want
to defer using the equality altogether until 'k' get resolved.
@@ -1058,15 +1058,15 @@ dropDerivedWC wc@(WC { wc_flat = flats, wc_insol = insols })
Note [Insoluble derived constraints]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
In general we discard derived constraints at the end of constraint solving;
-see dropDerivedWC. For example,
+see dropDerivedWC. For example,
- * If we have an unsolved (Ord a), we don't want to complain about
+ * If we have an unsolved (Ord a), we don't want to complain about
an unsolved (Eq a) as well.
- * If we have kind-incompatible (a::* ~ Int#::#) equality, we
- don't want to complain about the kind error twice.
+ * If we have kind-incompatible (a::* ~ Int#::#) equality, we
+ don't want to complain about the kind error twice.
-Arguably, for *some* derived constraints we might want to report errors.
-Notably, functional dependencies. If we have
+Arguably, for *some* derived constraints we might want to report errors.
+Notably, functional dependencies. If we have
class C a b | a -> b
and we have
[W] C a b, [W] C a c
@@ -1652,7 +1652,7 @@ data CtOrigin
| HoleOrigin
| UnboundOccurrenceOf RdrName
| ListOrigin -- An overloaded list
-
+
pprO :: CtOrigin -> SDoc
pprO (GivenOrigin sk) = ppr sk
pprO (OccurrenceOf name) = hsep [ptext (sLit "a use of"), quotes (ppr name)]
@@ -1660,8 +1660,8 @@ pprO AppOrigin = ptext (sLit "an application")
pprO (SpecPragOrigin name) = hsep [ptext (sLit "a specialisation pragma for"), quotes (ppr name)]
pprO (IPOccOrigin name) = hsep [ptext (sLit "a use of implicit parameter"), quotes (ppr name)]
pprO RecordUpdOrigin = ptext (sLit "a record update")
-pprO (AmbigOrigin ctxt) = ptext (sLit "the ambiguity check for")
- <+> case ctxt of
+pprO (AmbigOrigin ctxt) = ptext (sLit "the ambiguity check for")
+ <+> case ctxt of
FunSigCtxt name -> quotes (ppr name)
InfSigCtxt name -> quotes (ppr name)
_ -> pprUserTypeCtxt ctxt
diff --git a/compiler/typecheck/TcSMonad.lhs b/compiler/typecheck/TcSMonad.lhs
index a7bb3f4d8bbf..3a01e31eb2df 100644
--- a/compiler/typecheck/TcSMonad.lhs
+++ b/compiler/typecheck/TcSMonad.lhs
@@ -1,38 +1,31 @@
\begin{code}
-{-# OPTIONS -fno-warn-tabs -w #-}
--- The above warning supression flag is a temporary kludge.
--- While working on this module you are encouraged to remove it and
--- detab the module (please do the detabbing in a separate patch). See
--- http://ghc.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#TabsvsSpaces
--- for details
-
-- Type definitions for the constraint solver
-module TcSMonad (
+module TcSMonad (
-- Canonical constraints, definition is now in TcRnTypes
WorkList(..), isEmptyWorkList, emptyWorkList,
- workListFromEq, workListFromNonEq, workListFromCt,
- extendWorkListEq, extendWorkListFunEq,
- extendWorkListNonEq, extendWorkListCt,
+ workListFromEq, workListFromNonEq, workListFromCt,
+ extendWorkListEq, extendWorkListFunEq,
+ extendWorkListNonEq, extendWorkListCt,
extendWorkListCts, extendWorkListEqs, appendWorkList, selectWorkItem,
withWorkList, workListSize,
updWorkListTcS, updWorkListTcS_return,
-
- updTcSImplics,
- Ct(..), Xi, tyVarsOfCt, tyVarsOfCts,
+ updTcSImplics,
+
+ Ct(..), Xi, tyVarsOfCt, tyVarsOfCts,
emitInsoluble,
- isWanted, isDerived,
- isGivenCt, isWantedCt, isDerivedCt,
+ isWanted, isDerived,
+ isGivenCt, isWantedCt, isDerivedCt,
- canRewrite,
- mkGivenLoc,
+ canRewrite,
+ mkGivenLoc,
- TcS, runTcS, runTcSWithEvBinds, failTcS, panicTcS, traceTcS, -- Basic functionality
- traceFireTcS, bumpStepCountTcS,
+ TcS, runTcS, runTcSWithEvBinds, failTcS, panicTcS, traceTcS, -- Basic functionality
+ traceFireTcS, bumpStepCountTcS,
tryTcS, nestTcS, nestImplicTcS, recoverTcS,
wrapErrTcS, wrapWarnTcS,
@@ -41,18 +34,18 @@ module TcSMonad (
-- Marking stuff as used
addUsedRdrNamesTcS,
-
- deferTcSForAllEq,
-
+
+ deferTcSForAllEq,
+
setEvBind,
XEvTerm(..),
MaybeNew (..), isFresh, freshGoal, freshGoals, getEvTerm, getEvTerms,
- xCtFlavor, -- Transform a CtEvidence during a step
+ xCtFlavor, -- Transform a CtEvidence during a step
rewriteCtFlavor, -- Specialized version of xCtFlavor for coercions
newWantedEvVar, newWantedEvVarNC, instDFunConstraints,
newDerived,
-
+
-- Creation of evidence variables
setWantedTyBind, reportUnifications,
@@ -61,16 +54,16 @@ module TcSMonad (
getTcEvBindsMap, getTcSTyBindsMap,
- lookupFlatEqn, newFlattenSkolem, -- Flatten skolems
+ lookupFlatEqn, newFlattenSkolem, -- Flatten skolems
-- Deque
Deque(..), insertDeque, emptyDeque,
- -- Inerts
- InertSet(..), InertCans(..),
- getInertEqs,
- emptyInert, getTcSInerts, lookupInInerts,
- getInertUnsolved, checkAllSolved,
+ -- Inerts
+ InertSet(..), InertCans(..),
+ getInertEqs,
+ emptyInert, getTcSInerts, lookupInInerts,
+ getInertUnsolved, checkAllSolved,
prepareInertsForImplications,
modifyInertTcS,
insertInertItemTcS, partitionCCanMap, partitionEqMap,
@@ -90,27 +83,27 @@ module TcSMonad (
getDefaultInfo, getDynFlags, getGlobalRdrEnvTcS,
- matchFam, matchOpenFam,
- checkWellStagedDFun,
+ matchFam, matchOpenFam,
+ checkWellStagedDFun,
pprEq -- Smaller utils, re-exported from TcM
- -- TODO (DV): these are only really used in the
+ -- TODO (DV): these are only really used in the
-- instance matcher in TcSimplify. I am wondering
-- if the whole instance matcher simply belongs
- -- here
-) where
+ -- here
+) where
#include "HsVersions.h"
import HscTypes
import Inst
-import InstEnv
-import FamInst
+import InstEnv
+import FamInst
import FamInstEnv
import qualified TcRnMonad as TcM
import qualified TcMType as TcM
-import qualified TcEnv as TcM
+import qualified TcEnv as TcM
( checkWellStaged, topIdLvl, tcGetDefaultTys )
import Kind
import TcType
@@ -132,15 +125,15 @@ import MonadUtils
import FastString
import Util
-import Id
+import Id
import TcRnTypes
-import Unique
+import Unique
import UniqFM
import Maybes ( orElse, catMaybes, firstJust )
import Pair ( pSnd )
-import Control.Monad( unless, when, zipWithM )
+import Control.Monad( when, zipWithM )
import Data.IORef
import TrieMap
@@ -152,39 +145,39 @@ import Digraph
\end{code}
%************************************************************************
-%* *
+%* *
%* Worklists *
%* Canonical and non-canonical constraints that the simplifier has to *
%* work on. Including their simplification depths. *
%* *
-%* *
+%* *
%************************************************************************
Note [WorkList priorities]
~~~~~~~~~~~~~~~~~~~~~~~~~~~
-A WorkList contains canonical and non-canonical items (of all flavors).
-Notice that each Ct now has a simplification depth. We may
-consider using this depth for prioritization as well in the future.
+A WorkList contains canonical and non-canonical items (of all flavors).
+Notice that each Ct now has a simplification depth. We may
+consider using this depth for prioritization as well in the future.
As a simple form of priority queue, our worklist separates out
-equalities (wl_eqs) from the rest of the canonical constraints,
-so that it's easier to deal with them first, but the separation
-is not strictly necessary. Notice that non-canonical constraints
-are also parts of the worklist.
+equalities (wl_eqs) from the rest of the canonical constraints,
+so that it's easier to deal with them first, but the separation
+is not strictly necessary. Notice that non-canonical constraints
+are also parts of the worklist.
Note [NonCanonical Semantics]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Note that canonical constraints involve a CNonCanonical constructor. In the worklist
-we use this constructor for constraints that have not yet been canonicalized such as
- [Int] ~ [a]
-In other words, all constraints start life as NonCanonicals.
+we use this constructor for constraints that have not yet been canonicalized such as
+ [Int] ~ [a]
+In other words, all constraints start life as NonCanonicals.
On the other hand, in the Inert Set (see below) the presence of a NonCanonical somewhere
-means that we have a ``frozen error''.
+means that we have a ``frozen error''.
NonCanonical constraints never interact directly with other constraints -- but they can
-be rewritten by equalities (for instance if a non canonical exists in the inert, we'd
+be rewritten by equalities (for instance if a non canonical exists in the inert, we'd
better rewrite it as much as possible before reporting it as an error to the user)
\begin{code}
@@ -219,12 +212,12 @@ extractDeque (DQ [] bs) = case reverse bs of
-- See Note [WorkList priorities]
data WorkList = WorkList { wl_eqs :: [Ct]
, wl_funeqs :: Deque Ct
- , wl_rest :: [Ct]
+ , wl_rest :: [Ct]
}
appendWorkList :: WorkList -> WorkList -> WorkList
-appendWorkList new_wl orig_wl
+appendWorkList new_wl orig_wl
= WorkList { wl_eqs = wl_eqs new_wl ++ wl_eqs orig_wl
, wl_funeqs = wl_funeqs new_wl `appendDeque` wl_funeqs orig_wl
, wl_rest = wl_rest new_wl ++ wl_rest orig_wl }
@@ -236,14 +229,14 @@ workListSize (WorkList { wl_eqs = eqs, wl_funeqs = funeqs, wl_rest = rest })
extendWorkListEq :: Ct -> WorkList -> WorkList
-- Extension by equality
-extendWorkListEq ct wl
+extendWorkListEq ct wl
| Just {} <- isCFunEqCan_maybe ct
= extendWorkListFunEq ct wl
| otherwise
= wl { wl_eqs = ct : wl_eqs wl }
extendWorkListFunEq :: Ct -> WorkList -> WorkList
-extendWorkListFunEq ct wl
+extendWorkListFunEq ct wl
= wl { wl_funeqs = insertDeque ct (wl_funeqs wl) }
extendWorkListEqs :: [Ct] -> WorkList -> WorkList
@@ -252,7 +245,7 @@ extendWorkListEqs cts wl = foldr extendWorkListEq wl cts
extendWorkListNonEq :: Ct -> WorkList -> WorkList
-- Extension by non equality
-extendWorkListNonEq ct wl
+extendWorkListNonEq ct wl
= wl { wl_rest = ct : wl_rest wl }
extendWorkListCt :: Ct -> WorkList -> WorkList
@@ -266,7 +259,7 @@ extendWorkListCts :: [Ct] -> WorkList -> WorkList
extendWorkListCts cts wl = foldr extendWorkListCt wl cts
isEmptyWorkList :: WorkList -> Bool
-isEmptyWorkList wl
+isEmptyWorkList wl
= null (wl_eqs wl) && null (wl_rest wl) && isEmptyDeque (wl_funeqs wl)
emptyWorkList :: WorkList
@@ -279,8 +272,8 @@ workListFromNonEq :: Ct -> WorkList
workListFromNonEq ct = extendWorkListNonEq ct emptyWorkList
workListFromCt :: Ct -> WorkList
--- Agnostic
-workListFromCt ct | isEqPred (ctPred ct) = workListFromEq ct
+-- Agnostic
+workListFromCt ct | isEqPred (ctPred ct) = workListFromEq ct
| otherwise = workListFromNonEq ct
@@ -293,8 +286,8 @@ selectWorkItem wl@(WorkList { wl_eqs = eqs, wl_funeqs = feqs, wl_rest = rest })
(_,_,(ct:cts)) -> (Just ct, wl { wl_rest = cts })
(_,_,_) -> (Nothing,wl)
--- Pretty printing
-instance Outputable WorkList where
+-- Pretty printing
+instance Outputable WorkList where
ppr wl = vcat [ text "WorkList (eqs) = " <+> ppr (wl_eqs wl)
, text "WorkList (funeqs)= " <+> ppr (wl_funeqs wl)
, text "WorkList (rest) = " <+> ppr (wl_rest wl)
@@ -302,7 +295,7 @@ instance Outputable WorkList where
-- Canonical constraint maps
-data CCanMap a
+data CCanMap a
= CCanMap { cts_given :: UniqFM Cts -- All Given
, cts_derived :: UniqFM Cts -- All Derived
, cts_wanted :: UniqFM Cts } -- All Wanted
@@ -313,33 +306,33 @@ 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 :: CCanMap a -> Cts
cCanMapToBag cmap = foldUFM unionBags rest_wder (cts_given cmap)
- where rest_wder = foldUFM unionBags rest_der (cts_wanted cmap)
+ where rest_wder = foldUFM unionBags rest_der (cts_wanted cmap)
rest_der = foldUFM unionBags emptyCts (cts_derived cmap)
-emptyCCanMap :: CCanMap a
-emptyCCanMap = CCanMap { cts_given = emptyUFM, cts_derived = emptyUFM, cts_wanted = emptyUFM }
+emptyCCanMap :: CCanMap a
+emptyCCanMap = CCanMap { cts_given = emptyUFM, cts_derived = emptyUFM, cts_wanted = emptyUFM }
-updCCanMap:: Uniquable a => (a,Ct) -> CCanMap a -> CCanMap a
-updCCanMap (a,ct) cmap
- = case cc_ev ct of
- CtWanted {} -> cmap { cts_wanted = insert_into (cts_wanted cmap) }
+updCCanMap:: Uniquable a => (a,Ct) -> CCanMap a -> CCanMap a
+updCCanMap (a,ct) cmap
+ = case cc_ev ct of
+ CtWanted {} -> cmap { cts_wanted = insert_into (cts_wanted cmap) }
CtGiven {} -> cmap { cts_given = insert_into (cts_given cmap) }
CtDerived {} -> cmap { cts_derived = insert_into (cts_derived cmap) }
- where
+ where
insert_into m = addToUFM_C unionBags m a (singleCt ct)
-getRelevantCts :: Uniquable a => a -> CCanMap a -> (Cts, CCanMap a)
+getRelevantCts :: Uniquable a => a -> CCanMap a -> (Cts, CCanMap a)
-- Gets the relevant constraints and returns the rest of the CCanMap
-getRelevantCts a cmap
+getRelevantCts a cmap
= let relevant = lookup (cts_wanted cmap) `unionBags`
lookup (cts_given cmap) `unionBags`
- lookup (cts_derived cmap)
+ lookup (cts_derived cmap)
residual_map = cmap { cts_wanted = delFromUFM (cts_wanted cmap) a
, cts_given = delFromUFM (cts_given cmap) a
, cts_derived = delFromUFM (cts_derived cmap) a }
- in (relevant, residual_map)
+ in (relevant, residual_map)
where
lookup map = lookupUFM map a `orElse` emptyCts
@@ -362,22 +355,22 @@ findEvidence pick_me cts
pick ct deflt | let ctev = cc_ev ct, pick_me ctev = Just ctev
| otherwise = deflt
-partitionCCanMap :: (Ct -> Bool) -> CCanMap a -> (Cts,CCanMap a)
+partitionCCanMap :: (Ct -> Bool) -> CCanMap a -> (Cts,CCanMap a)
-- All constraints that /match/ the predicate go in the bag, the rest remain in the map
partitionCCanMap pred cmap
- = let (ws_map,ws) = foldUFM_Directly aux (emptyUFM,emptyCts) (cts_wanted cmap)
+ = let (ws_map,ws) = foldUFM_Directly aux (emptyUFM,emptyCts) (cts_wanted cmap)
(ds_map,ds) = foldUFM_Directly aux (emptyUFM,emptyCts) (cts_derived cmap)
- (gs_map,gs) = foldUFM_Directly aux (emptyUFM,emptyCts) (cts_given cmap)
+ (gs_map,gs) = foldUFM_Directly aux (emptyUFM,emptyCts) (cts_given cmap)
in (ws `andCts` ds `andCts` gs, cmap { cts_wanted = ws_map
, cts_given = gs_map
- , cts_derived = ds_map })
+ , cts_derived = ds_map })
where aux k this_cts (mp,acc_cts) = (new_mp, new_acc_cts)
where new_mp = addToUFM mp k cts_keep
new_acc_cts = acc_cts `andCts` cts_out
(cts_out, cts_keep) = partitionBag pred this_cts
partitionEqMap :: (Ct -> Bool) -> TyVarEnv (Ct,TcCoercion) -> ([Ct], TyVarEnv (Ct,TcCoercion))
-partitionEqMap pred isubst
+partitionEqMap pred isubst
= let eqs_out = foldVarEnv extend_if_pred [] isubst
eqs_in = filterVarEnv_Directly (\_ (ct,_) -> not (pred ct)) isubst
in (eqs_out, eqs_in)
@@ -426,8 +419,8 @@ delFamHead (FamHeadMap m) key = FamHeadMap (deleteTM key m)
anyFamHeadMap :: (Ct -> Bool) -> CtFamHeadMap -> Bool
anyFamHeadMap f ctmap = foldTM ((||) . f) (unFamHeadMap ctmap) False
-partCtFamHeadMap :: (Ct -> Bool)
- -> CtFamHeadMap
+partCtFamHeadMap :: (Ct -> Bool)
+ -> CtFamHeadMap
-> (Cts, CtFamHeadMap)
partCtFamHeadMap f (FamHeadMap ctmap)
= let (cts, tymap_final) = foldTM upd_acc ctmap (emptyBag, ctmap)
@@ -436,11 +429,11 @@ partCtFamHeadMap f (FamHeadMap ctmap)
upd_acc ct (cts,acc_map)
| f ct = (extendCts cts ct, deleteTM fam_head acc_map)
| otherwise = (cts,acc_map)
- where
+ where
fam_head = funEqHead ct
funEqHead :: Ct -> Type
-funEqHead ct = case isCFunEqCan_maybe ct of
+funEqHead ct = case isCFunEqCan_maybe ct of
Just (tc,tys) -> mkTyConApp tc tys
Nothing -> pprPanic "funEqHead" (ppr ct)
@@ -451,10 +444,10 @@ filterSolved p (PredMap mp) = PredMap (foldTM upd mp emptyTM)
\end{code}
%************************************************************************
-%* *
+%* *
%* Inert Sets *
%* *
-%* *
+%* *
%************************************************************************
Note [Detailed InertCans Invariants]
@@ -463,15 +456,15 @@ The InertCans represents a collection of constraints with the following properti
1 All canonical
2 All Given or Wanted or Derived. No (partially) Solved
3 No two dictionaries with the same head
- 4 No two family equations with the same head
+ 4 No two family equations with the same head
NB: This is enforced by construction since we use a CtFamHeadMap for inert_funeqs
5 Family equations inert wrt top-level family axioms
- 6 Dictionaries have no matching top-level instance
-
+ 6 Dictionaries have no matching top-level instance
+
7 Non-equality constraints are fully rewritten with respect to the equalities (CTyEqCan)
8 Equalities _do_not_ form an idempotent substitution, but they are
- guaranteed to not have any occurs errors. Additional notes:
+ guaranteed to not have any occurs errors. Additional notes:
- The lack of idempotence of the inert substitution implies
that we must make sure that when we rewrite a constraint we
@@ -494,7 +487,7 @@ The InertCans represents a collection of constraints with the following properti
will not cause the first equality to have an occurs check
then we do not rewrite the inert equality. This happens in
TcInteract, rewriteInertEqsFromInertEq.
-
+
See Note [Delicate equality kick-out] to see which inert
equalities can safely stay in the inert set and which must be
kicked out to be rewritten and re-checked for occurs errors.
@@ -530,12 +523,12 @@ Type-family equations, of form (ev : F tys ~ ty), live in four places
sharing. It contains lots of things that are still in the work-list.
E.g Suppose we have (w1: F (G a) ~ Int), and (w2: H (G a) ~ Int) in the
work list. Then we flatten w1, dumping (w3: G a ~ f1) in the work
- list. Now if we flatten w2 before we get to w3, we still want to
+ list. Now if we flatten w2 before we get to w3, we still want to
share that (G a).
Because it contains work-list things, DO NOT use the flat cache to solve
- a top-level goal. Eg in the above example we don't want to solve w3
- using w3 itself!
+ a top-level goal. Eg in the above example we don't want to solve w3
+ using w3 itself!
* The inert_solved_funeqs. These are all "solved" goals (see Note [Solved constraints]),
the result of using a top-level type-family instance.
@@ -546,34 +539,34 @@ Type-family equations, of form (ev : F tys ~ ty), live in four places
\begin{code}
-- All Given (fully known) or Wanted or Derived
-- See Note [Detailed InertCans Invariants] for more
-data InertCans
+data InertCans
= IC { inert_eqs :: TyVarEnv Ct
- -- Must all be CTyEqCans! If an entry exists of the form:
+ -- Must all be CTyEqCans! If an entry exists of the form:
-- a |-> ct,co
- -- Then ct = CTyEqCan { cc_tyvar = a, cc_rhs = xi }
+ -- Then ct = CTyEqCan { cc_tyvar = a, cc_rhs = xi }
-- And co : a ~ xi
-- Some Refl equalities are also in tcs_ty_binds
-- see Note [Spontaneously solved in TyBinds] in TcInteract
, inert_dicts :: CCanMap Class
-- Dictionaries only, index is the class
- -- NB: index is /not/ the whole type because FD reactions
+ -- NB: index is /not/ the whole type because FD reactions
-- need to match the class but not necessarily the whole type.
, inert_funeqs :: CtFamHeadMap
-- Family equations, index is the whole family head type.
- , inert_irreds :: Cts
+ , inert_irreds :: Cts
-- Irreducible predicates
- , inert_insols :: Cts
+ , inert_insols :: Cts
-- Frozen errors (as non-canonicals)
}
-
-
+
+
-- The Inert Set
data InertSet
= IS { inert_cans :: InertCans
-- Canonical Given, Wanted, Derived (no Solved)
- -- Sometimes called "the inert set"
+ -- Sometimes called "the inert set"
, inert_flat_cache :: FamHeadMap (CtEvidence, TcType)
-- See Note [Type family equations]
@@ -583,33 +576,33 @@ data InertSet
-- (w:F ty ~ a) by setting w:=w! We just use the flat-cache
-- when allocating a new flatten-skolem.
-- Not necessarily inert wrt top-level equations (or inert_cans)
-
+
, inert_fsks :: [TcTyVar] -- Rigid flatten-skolems (arising from givens)
-- allocated in this local scope
, inert_solved_funeqs :: FamHeadMap (CtEvidence, TcType)
-- See Note [Type family equations]
- -- Of form co :: F xis ~ xi
+ -- Of form co :: F xis ~ xi
-- Always the result of using a top-level family axiom F xis ~ tau
- -- No Deriveds
+ -- No Deriveds
-- Not necessarily fully rewritten (by type substitutions)
- , inert_solved_dicts :: PredMap CtEvidence
- -- Of form ev :: C t1 .. tn
+ , inert_solved_dicts :: PredMap CtEvidence
+ -- Of form ev :: C t1 .. tn
-- Always the result of using a top-level instance declaration
-- See Note [Solved constraints]
- -- - Used to avoid creating a new EvVar when we have a new goal
- -- that we have solved in the past
- -- - Stored not necessarily as fully rewritten
- -- (ToDo: rewrite lazily when we lookup)
+ -- - Used to avoid creating a new EvVar when we have a new goal
+ -- that we have solved in the past
+ -- - Stored not necessarily as fully rewritten
+ -- (ToDo: rewrite lazily when we lookup)
}
-instance Outputable InertCans where
- ppr ics = vcat [ ptext (sLit "Equalities:")
+instance Outputable InertCans where
+ ppr ics = vcat [ ptext (sLit "Equalities:")
<+> vcat (map ppr (varEnvElts (inert_eqs ics)))
, ptext (sLit "Type-function equalities:")
- <+> vcat (map ppr (Bag.bagToList $
+ <+> vcat (map ppr (Bag.bagToList $
ctTypeMapCts (unFamHeadMap $ inert_funeqs ics)))
, ptext (sLit "Dictionaries:")
<+> vcat (map ppr (Bag.bagToList $ cCanMapToBag (inert_dicts ics)))
@@ -618,8 +611,8 @@ instance Outputable InertCans where
, text "Insolubles =" <+> -- Clearly print frozen errors
braces (vcat (map ppr (Bag.bagToList $ inert_insols ics)))
]
-
-instance Outputable InertSet where
+
+instance Outputable InertSet where
ppr is = vcat [ ppr $ inert_cans is
, text "Solved dicts" <+> int (sizePredMap (inert_solved_dicts is))
, text "Solved funeqs" <+> int (sizeFamHeadMap (inert_solved_funeqs is))]
@@ -633,91 +626,91 @@ emptyInert
, inert_insols = emptyCts }
, inert_fsks = []
, inert_flat_cache = emptyFamHeadMap
- , inert_solved_dicts = PredMap emptyTM
+ , inert_solved_dicts = PredMap emptyTM
, inert_solved_funeqs = emptyFamHeadMap }
-insertInertItem :: Ct -> InertSet -> InertSet
--- Add a new inert element to the inert set.
+insertInertItem :: Ct -> InertSet -> InertSet
+-- Add a new inert element to the inert set.
insertInertItem item is
= -- A canonical Given, Wanted, or Derived
is { inert_cans = upd_inert_cans (inert_cans is) item }
-
+
where upd_inert_cans :: InertCans -> Ct -> InertCans
-- Precondition: item /is/ canonical
upd_inert_cans ics item
- | isCTyEqCan item
+ | isCTyEqCan item
= let upd_err a b = pprPanic "insertInertItem" $
vcat [ text "Multiple inert equalities:"
, text "Old (already inert):" <+> ppr a
, text "Trying to insert :" <+> ppr b ]
-
- eqs' = extendVarEnv_C upd_err (inert_eqs ics)
- (cc_tyvar item) item
+
+ eqs' = extendVarEnv_C upd_err (inert_eqs ics)
+ (cc_tyvar item) item
in ics { inert_eqs = eqs' }
| isCIrredEvCan item -- Presently-irreducible evidence
= ics { inert_irreds = inert_irreds ics `Bag.snocBag` item }
- | Just cls <- isCDictCan_Maybe item -- Dictionary
+ | Just cls <- isCDictCan_Maybe item -- Dictionary
= ics { inert_dicts = updCCanMap (cls,item) (inert_dicts ics) }
| Just (tc,tys) <- isCFunEqCan_maybe item -- Function equality
= let fam_head = mkTyConApp tc tys
upd_funeqs Nothing = Just item
- upd_funeqs (Just _already_there)
+ upd_funeqs (Just _already_there)
= panic "insertInertItem: item already there!"
- in ics { inert_funeqs = FamHeadMap
- (alterTM fam_head upd_funeqs $
+ in ics { inert_funeqs = FamHeadMap
+ (alterTM fam_head upd_funeqs $
(unFamHeadMap $ inert_funeqs ics)) }
| otherwise
- = pprPanic "upd_inert set: can't happen! Inserting " $
- ppr item -- Can't be CNonCanonical, CHoleCan,
+ = pprPanic "upd_inert set: can't happen! Inserting " $
+ 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
insertInertItemTcS item
- = do { traceTcS "insertInertItemTcS {" $
+ = do { traceTcS "insertInertItemTcS {" $
text "Trying to insert new inert item:" <+> ppr item
- ; updInertTcS (insertInertItem item)
-
+ ; updInertTcS (insertInertItem item)
+
; traceTcS "insertInertItemTcS }" $ empty }
addSolvedDict :: CtEvidence -> TcS ()
-- Add a new item in the solved set of the monad
addSolvedDict item
| isIPPred (ctEvPred item) -- Never cache "solved" implicit parameters (not sure why!)
- = return ()
+ = return ()
| otherwise
= do { traceTcS "updSolvedSetTcs:" $ ppr item
; updInertTcS upd_solved_dicts }
where
- upd_solved_dicts is
- = is { inert_solved_dicts = PredMap $ insertTM pred item $
+ upd_solved_dicts is
+ = is { inert_solved_dicts = PredMap $ insertTM pred item $
unPredMap $ inert_solved_dicts is }
pred = ctEvPred item
addSolvedFunEq :: TcType -> CtEvidence -> TcType -> TcS ()
addSolvedFunEq fam_ty ev rhs_ty
- = updInertTcS $ \ inert ->
- inert { inert_solved_funeqs = insertFamHead (inert_solved_funeqs inert)
+ = updInertTcS $ \ inert ->
+ inert { inert_solved_funeqs = insertFamHead (inert_solved_funeqs inert)
fam_ty (ev, rhs_ty) }
-modifyInertTcS :: (InertSet -> (a,InertSet)) -> TcS a
+modifyInertTcS :: (InertSet -> (a,InertSet)) -> TcS a
-- Modify the inert set with the supplied function
-modifyInertTcS upd
+modifyInertTcS upd
= do { is_var <- getTcSInertsRef
; curr_inert <- wrapTcS (TcM.readTcRef is_var)
; let (a, new_inert) = upd curr_inert
; wrapTcS (TcM.writeTcRef is_var new_inert)
; return a }
-updInertTcS :: (InertSet -> InertSet) -> TcS ()
+updInertTcS :: (InertSet -> InertSet) -> TcS ()
-- Modify the inert set with the supplied function
-updInertTcS upd
+updInertTcS upd
= do { is_var <- getTcSInertsRef
; curr_inert <- wrapTcS (TcM.readTcRef is_var)
; let new_inert = upd curr_inert
@@ -734,18 +727,18 @@ prepareInertsForImplications is
, inert_irreds = irreds
, inert_funeqs = FamHeadMap funeqs
, inert_dicts = dicts })
- = IC { inert_eqs = filterVarEnv_Directly (\_ ct -> isGivenCt ct) eqs
+ = IC { inert_eqs = filterVarEnv_Directly (\_ ct -> isGivenCt ct) eqs
, inert_funeqs = FamHeadMap (foldTM given_from_wanted funeqs emptyTM)
, inert_irreds = Bag.filterBag isGivenCt irreds
, inert_dicts = keepGivenCMap dicts
, inert_insols = emptyCts }
given_from_wanted :: Ct -> TypeMap Ct -> TypeMap Ct
- given_from_wanted funeq fhm -- This is where the magic processing happens
+ given_from_wanted funeq fhm -- This is where the magic processing happens
-- for type-function equalities
-- See Note [Preparing inert set for implications]
| isWanted ev = insert_one (funeq { cc_ev = given_ev }) fhm
- | isGiven ev = insert_one funeq fhm
+ | isGiven ev = insert_one funeq fhm
| otherwise = fhm -- Drop derived constraints
where
ev = ctEvidence funeq
@@ -753,22 +746,22 @@ prepareInertsForImplications is
, ctev_pred = ctev_pred ev }
insert_one :: Ct -> TypeMap Ct -> TypeMap Ct
- insert_one funeq fhm = insertTM (funEqHead funeq) funeq fhm
+ insert_one funeq fhm = insertTM (funEqHead funeq) funeq fhm
\end{code}
Note [Preparing inert set for implications]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Before solving the nested implications, we trim the inert set,
-retaining only Givens. These givens can be used when solving
+retaining only Givens. These givens can be used when solving
the inner implications.
With one wrinkle! We take all *wanted* *funeqs*, and turn them into givens.
Consider (Trac #4935)
- type instance F True a b = a
+ type instance F True a b = a
type instance F False a b = b
- [w] F c a b ~ gamma
- (c ~ True) => a ~ gamma
+ [w] F c a b ~ gamma
+ (c ~ True) => a ~ gamma
(c ~ False) => b ~ gamma
Obviously this is soluble with gamma := F c a b. But
@@ -776,9 +769,9 @@ Since solveCTyFunEqs happens at the very end of solving, the only way
to solve the two implications is temporarily consider (F c a b ~ gamma)
as Given and push it inside the implications. Now, when we come
out again at the end, having solved the implications solveCTyFunEqs
-will solve this equality.
+will solve this equality.
-Turning type-function equalities into Givens is easy becase they
+Turning type-function equalities into Givens is easy becase they
*stay inert*. No need to re-process them.
We don't try to turn any *other* Wanteds into Givens:
@@ -790,8 +783,8 @@ We don't try to turn any *other* Wanteds into Givens:
There might be cases where interactions between wanteds can help
to solve a constraint. For example
- class C a b | a -> b
- (C Int alpha), (forall d. C d blah => C Int a)
+ class C a b | a -> b
+ (C Int alpha), (forall d. C d blah => C Int a)
If we push the (C Int alpha) inwards, as a given, it can produce a
fundep (alpha~a) and this can float out again and be used to fix
@@ -818,7 +811,7 @@ getInertUnsolved
(unsolved_funeqs,_) = partCtFamHeadMap is_unsolved (inert_funeqs icans)
unsolved_eqs = foldVarEnv add_if_unsolved emptyCts (inert_eqs icans)
- unsolved_flats = unsolved_eqs `unionBags` unsolved_irreds `unionBags`
+ unsolved_flats = unsolved_eqs `unionBags` unsolved_irreds `unionBags`
unsolved_dicts `unionBags` unsolved_funeqs
; return (unsolved_flats, inert_insols icans) }
@@ -858,49 +851,49 @@ getInertsFunEqTyCon tc =
extractRelevantInerts :: Ct -> TcS Cts
--- Returns the constraints from the inert set that are 'relevant' to react with
--- this constraint. The monad is left with the 'thinner' inerts.
+-- Returns the constraints from the inert set that are 'relevant' to react with
+-- this constraint. The monad is left with the 'thinner' inerts.
-- NB: This function contains logic specific to the constraint solver, maybe move there?
-extractRelevantInerts wi
+extractRelevantInerts wi
= modifyInertTcS (extract_relevants wi)
- where
+ where
extract_relevants :: Ct -> InertSet -> (Cts,InertSet)
- extract_relevants wi is
+ extract_relevants wi is
= let (cts,ics') = extract_ics_relevants wi (inert_cans is)
- in (cts, is { inert_cans = ics' })
-
+ in (cts, is { inert_cans = ics' })
+
extract_ics_relevants :: Ct -> InertCans -> (Cts, InertCans)
- extract_ics_relevants (CDictCan {cc_class = cl}) ics =
- let (cts,dict_map) = getRelevantCts cl (inert_dicts ics)
+ extract_ics_relevants (CDictCan {cc_class = cl}) ics =
+ let (cts,dict_map) = getRelevantCts cl (inert_dicts ics)
in (cts, ics { inert_dicts = dict_map })
- extract_ics_relevants (CFunEqCan { cc_fun = tc, cc_tyargs = tys })
+ extract_ics_relevants (CFunEqCan { cc_fun = tc, cc_tyargs = tys })
ics@(IC { inert_funeqs = funeq_map })
| let fam_head = mkTyConApp tc tys
, Just ct <- lookupFamHead funeq_map fam_head
= (singleCt ct, ics { inert_funeqs = delFamHead funeq_map fam_head })
- extract_ics_relevants (CHoleCan {}) ics
+ extract_ics_relevants (CHoleCan {}) _
= 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
+ extract_ics_relevants (CIrredEvCan { }) ics =
+ let cts = inert_irreds ics
in (cts, ics { inert_irreds = emptyCts })
extract_ics_relevants _ ics = (emptyCts,ics)
-
+
lookupFlatEqn :: TcType -> TcS (Maybe (CtEvidence, TcType))
-lookupFlatEqn fam_ty
+lookupFlatEqn fam_ty
= do { IS { inert_solved_funeqs = solved_funeqs
, inert_flat_cache = flat_cache
, inert_cans = IC { inert_funeqs = inert_funeqs } } <- getTcSInerts
- ; return (lookupFamHead solved_funeqs fam_ty `firstJust`
+ ; return (lookupFamHead solved_funeqs fam_ty `firstJust`
lookup_in_inerts inert_funeqs `firstJust`
lookupFamHead flat_cache fam_ty) }
where
- lookup_in_inerts inert_funeqs
+ lookup_in_inerts inert_funeqs
= case lookupFamHead inert_funeqs fam_ty of
Nothing -> Nothing
Just ct -> Just (ctEvidence ct, cc_rhs ct)
@@ -915,31 +908,31 @@ lookupInInerts pty
lookupSolvedDict :: InertSet -> TcPredType -> Maybe CtEvidence
-- Returns just if exactly this predicate type exists in the solved.
-lookupSolvedDict (IS { inert_solved_dicts = solved }) pty
+lookupSolvedDict (IS { inert_solved_dicts = solved }) pty
= lookupTM pty (unPredMap solved)
lookupInInertCans :: InertSet -> TcPredType -> Maybe CtEvidence
-- Returns Just if exactly this pred type exists in the inert canonicals
lookupInInertCans (IS { inert_cans = ics }) pty
= case (classifyPredType pty) of
- ClassPred cls _
+ ClassPred cls _
-> lookupCCanMap cls (\ct -> ctEvPred ct `eqType` pty) (inert_dicts ics)
- EqPred ty1 _ty2
+ EqPred ty1 _ty2
| Just tv <- getTyVar_maybe ty1 -- Tyvar equation
, Just ct <- lookupVarEnv (inert_eqs ics) tv
- , let ctev = ctEvidence ct
- , ctEvPred ctev `eqType` pty
- -> Just ctev
+ , let ctev = ctEvidence ct
+ , ctEvPred ctev `eqType` pty
+ -> Just ctev
- | Just _ <- splitTyConApp_maybe ty1 -- Family equation
- , Just ct <- lookupTM ty1 (unFamHeadMap $ inert_funeqs ics)
- , let ctev = ctEvidence ct
- , ctEvPred ctev `eqType` pty
- -> Just ctev
+ | Just _ <- splitTyConApp_maybe ty1 -- Family equation
+ , Just ct <- lookupTM ty1 (unFamHeadMap $ inert_funeqs ics)
+ , let ctev = ctEvidence ct
+ , ctEvPred ctev `eqType` pty
+ -> Just ctev
IrredPred {} -> findEvidence (\ct -> ctEvPred ct `eqType` pty) (inert_irreds ics)
-
+
_other -> Nothing -- NB: No caching for IPs or holes
\end{code}
@@ -947,9 +940,9 @@ lookupInInertCans (IS { inert_cans = ics }) pty
%************************************************************************
-%* *
-%* The TcS solver monad *
-%* *
+%* *
+%* The TcS solver monad *
+%* *
%************************************************************************
Note [The TcS monad]
@@ -991,30 +984,30 @@ data TcSEnv
\begin{code}
---------------
-newtype TcS a = TcS { unTcS :: TcSEnv -> TcM a }
+newtype TcS a = TcS { unTcS :: TcSEnv -> TcM a }
instance Functor TcS where
fmap f m = TcS $ fmap f . unTcS m
-instance Monad TcS where
- return x = TcS (\_ -> return x)
- fail err = TcS (\_ -> fail err)
+instance Monad TcS where
+ return x = TcS (\_ -> return x)
+ fail err = TcS (\_ -> fail err)
m >>= k = TcS (\ebs -> unTcS m ebs >>= \r -> unTcS (k r) ebs)
--- Basic functionality
+-- Basic functionality
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-wrapTcS :: TcM a -> TcS a
+wrapTcS :: TcM a -> TcS a
-- Do not export wrapTcS, because it promotes an arbitrary TcM to TcS,
-- and TcS is supposed to have limited functionality
wrapTcS = TcS . const -- a TcM action will not use the TcEvBinds
-wrapErrTcS :: TcM a -> TcS a
+wrapErrTcS :: TcM a -> TcS a
-- The thing wrapped should just fail
-- There's no static check; it's up to the user
-- Having a variant for each error message is too painful
wrapErrTcS = wrapTcS
-wrapWarnTcS :: TcM a -> TcS a
+wrapWarnTcS :: TcM a -> TcS a
-- The thing wrapped should just add a warning, or no-op
-- There's no static check; it's up to the user
wrapWarnTcS = wrapTcS
@@ -1039,14 +1032,14 @@ bumpStepCountTcS = TcS $ \env -> do { let ref = tcs_count env
traceFireTcS :: Ct -> SDoc -> TcS ()
-- Dump a rule-firing trace
-traceFireTcS ct doc
- = TcS $ \env ->
- TcM.whenDOptM Opt_D_dump_cs_trace $
+traceFireTcS ct doc
+ = TcS $ \env ->
+ TcM.whenDOptM Opt_D_dump_cs_trace $
do { n <- TcM.readTcRef (tcs_count env)
; let msg = int n <> brackets (int (ctLocDepth (cc_loc ct))) <+> doc
; TcM.dumpTcRn msg }
-runTcS :: TcS a -- What to run
+runTcS :: TcS a -- What to run
-> TcM (a, Bag EvBind)
runTcS tcs
= do { ev_binds_var <- TcM.newTcEvBinds
@@ -1055,24 +1048,24 @@ runTcS tcs
; return (res, ev_binds) }
runTcSWithEvBinds :: EvBindsVar
- -> TcS a
+ -> TcS a
-> TcM a
runTcSWithEvBinds ev_binds_var tcs
= do { ty_binds_var <- TcM.newTcRef (False, emptyVarEnv)
; step_count <- TcM.newTcRef 0
- ; inert_var <- TcM.newTcRef is
+ ; inert_var <- TcM.newTcRef is
; let env = TcSEnv { tcs_ev_binds = ev_binds_var
, tcs_ty_binds = ty_binds_var
- , tcs_count = step_count
+ , tcs_count = step_count
, tcs_inerts = inert_var
, tcs_worklist = panic "runTcS: worklist"
, tcs_implics = panic "runTcS: implics" }
-- NB: Both these are initialised by withWorkList
- -- Run the computation
+ -- Run the computation
; res <- unTcS tcs env
- -- Perform the type unifications required
+ -- Perform the type unifications required
; (_, ty_binds) <- TcM.readTcRef ty_binds_var
; mapM_ do_unification (varEnvElts ty_binds)
@@ -1089,11 +1082,11 @@ runTcSWithEvBinds ev_binds_var tcs
where
do_unification (tv,ty) = TcM.writeMetaTyVar tv ty
is = emptyInert
-
+
#ifdef DEBUG
checkForCyclicBinds :: Bag EvBind -> TcM ()
checkForCyclicBinds ev_binds
- | null cycles
+ | null cycles
= return ()
| null coercion_cycles
= TcM.traceTc "Cycle in evidence binds" $ ppr cycles
@@ -1108,12 +1101,12 @@ checkForCyclicBinds ev_binds
edges :: [(EvBind, EvVar, [EvVar])]
edges = [(bind, bndr, varSetElems (evVarsOfTerm rhs)) | bind@(EvBind bndr rhs) <- bagToList ev_binds]
-#endif
+#endif
-nestImplicTcS :: EvBindsVar -> Untouchables -> InertSet -> TcS a -> TcS a
-nestImplicTcS ref inner_untch inerts (TcS thing_inside)
+nestImplicTcS :: EvBindsVar -> Untouchables -> InertSet -> TcS a -> TcS a
+nestImplicTcS ref inner_untch inerts (TcS thing_inside)
= TcS $ \ TcSEnv { tcs_ty_binds = ty_binds
- , tcs_count = count } ->
+ , tcs_count = count } ->
do { new_inert_var <- TcM.newTcRef inerts
; let nest_env = TcSEnv { tcs_ev_binds = ref
, tcs_ty_binds = ty_binds
@@ -1125,13 +1118,13 @@ nestImplicTcS ref inner_untch inerts (TcS thing_inside)
}
; res <- TcM.setUntouchables inner_untch $
thing_inside nest_env
-
+
#ifdef DEBUG
-- Perform a check that the thing_inside did not cause cycles
; ev_binds <- TcM.getTcEvBinds ref
; checkForCyclicBinds ev_binds
#endif
-
+
; return res }
recoverTcS :: TcS a -> TcS a -> TcS a
@@ -1139,11 +1132,11 @@ recoverTcS (TcS recovery_code) (TcS thing_inside)
= TcS $ \ env ->
TcM.recoverM (recovery_code env) (thing_inside env)
-nestTcS :: TcS a -> TcS a
+nestTcS :: TcS a -> TcS a
-- Use the current untouchables, augmenting the current
-- evidence bindings, ty_binds, and solved caches
-- But have no effect on the InertCans or insolubles
-nestTcS (TcS thing_inside)
+nestTcS (TcS thing_inside)
= TcS $ \ env@(TcSEnv { tcs_inerts = inerts_var }) ->
do { inerts <- TcM.readTcRef inerts_var
; new_inert_var <- TcM.newTcRef inerts
@@ -1178,14 +1171,14 @@ tryTcS (TcS thing_inside)
getTcSInertsRef :: TcS (IORef InertSet)
getTcSInertsRef = TcS (return . tcs_inerts)
-getTcSWorkListRef :: TcS (IORef WorkList)
-getTcSWorkListRef = TcS (return . tcs_worklist)
+getTcSWorkListRef :: TcS (IORef WorkList)
+getTcSWorkListRef = TcS (return . tcs_worklist)
-getTcSInerts :: TcS InertSet
-getTcSInerts = getTcSInertsRef >>= wrapTcS . (TcM.readTcRef)
+getTcSInerts :: TcS InertSet
+getTcSInerts = getTcSInertsRef >>= wrapTcS . (TcM.readTcRef)
-updWorkListTcS :: (WorkList -> WorkList) -> TcS ()
-updWorkListTcS f
+updWorkListTcS :: (WorkList -> WorkList) -> TcS ()
+updWorkListTcS f
= do { wl_var <- getTcSWorkListRef
; wl_curr <- wrapTcS (TcM.readTcRef wl_var)
; let new_work = f wl_curr
@@ -1219,13 +1212,13 @@ withWorkList work_items (TcS thing_inside)
return implics }
updTcSImplics :: (Bag Implication -> Bag Implication) -> TcS ()
-updTcSImplics f
+updTcSImplics f
= do { impl_ref <- getTcSImplicsRef
; wrapTcS $ do { implics <- TcM.readTcRef impl_ref
; TcM.writeTcRef impl_ref (f implics) } }
emitInsoluble :: Ct -> TcS ()
--- Emits a non-canonical constraint that will stand for a frozen error in the inerts.
+-- Emits a non-canonical constraint that will stand for a frozen error in the inerts.
emitInsoluble ct
= do { traceTcS "Emit insoluble" (ppr ct)
; updInertTcS add_insol }
@@ -1236,13 +1229,13 @@ emitInsoluble ct
| otherwise = is { inert_cans = ics { inert_insols = extendCts old_insols ct } }
where
already_there = not (isWantedCt ct) && anyBag (eqType this_pred . ctPred) old_insols
- -- See Note [Do not add duplicate derived insolubles]
+ -- See Note [Do not add duplicate derived insolubles]
getTcSImplicsRef :: TcS (IORef (Bag Implication))
-getTcSImplicsRef = TcS (return . tcs_implics)
+getTcSImplicsRef = TcS (return . tcs_implics)
getTcEvBinds :: TcS EvBindsVar
-getTcEvBinds = TcS (return . tcs_ev_binds)
+getTcEvBinds = TcS (return . tcs_ev_binds)
getUntouchables :: TcS Untouchables
getUntouchables = wrapTcS TcM.getUntouchables
@@ -1260,16 +1253,16 @@ getTcSTyBindsMap = do { ref <- getTcSTyBinds
getTcEvBindsMap :: TcS EvBindMap
getTcEvBindsMap
- = do { EvBindsVar ev_ref _ <- getTcEvBinds
+ = do { EvBindsVar ev_ref _ <- getTcEvBinds
; wrapTcS $ TcM.readTcRef ev_ref }
-setWantedTyBind :: TcTyVar -> TcType -> TcS ()
+setWantedTyBind :: TcTyVar -> TcType -> TcS ()
-- Add a type binding
-- We never do this twice!
-setWantedTyBind tv ty
+setWantedTyBind tv ty
= ASSERT2( isMetaTyVar tv, ppr tv )
do { ref <- getTcSTyBinds
- ; wrapTcS $
+ ; wrapTcS $
do { (_dirty, ty_binds) <- TcM.readTcRef ref
; when debugIsOn $
TcM.checkErr (not (tv `elemVarEnv` ty_binds)) $
@@ -1303,17 +1296,17 @@ getDefaultInfo = wrapTcS TcM.tcGetDefaultTys
-- Just get some environments needed for instance looking up and matching
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-getInstEnvs :: TcS (InstEnv, InstEnv)
-getInstEnvs = wrapTcS $ Inst.tcGetInstEnvs
+getInstEnvs :: TcS (InstEnv, InstEnv)
+getInstEnvs = wrapTcS $ Inst.tcGetInstEnvs
-getFamInstEnvs :: TcS (FamInstEnv, FamInstEnv)
+getFamInstEnvs :: TcS (FamInstEnv, FamInstEnv)
getFamInstEnvs = wrapTcS $ FamInst.tcGetFamInstEnvs
-getTopEnv :: TcS HscEnv
-getTopEnv = wrapTcS $ TcM.getTopEnv
+getTopEnv :: TcS HscEnv
+getTopEnv = wrapTcS $ TcM.getTopEnv
-getGblEnv :: TcS TcGblEnv
-getGblEnv = wrapTcS $ TcM.getGblEnv
+getGblEnv :: TcS TcGblEnv
+getGblEnv = wrapTcS $ TcM.getGblEnv
-- Setting names as used (used in the deriving of Coercible evidence)
-- Too hackish to expose it to TcS? In that case somehow extract the used
@@ -1324,9 +1317,9 @@ addUsedRdrNamesTcS names = wrapTcS $ addUsedRdrNames names
-- Various smaller utilities [TODO, maybe will be absorbed in the instance matcher]
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-checkWellStagedDFun :: PredType -> DFunId -> CtLoc -> TcS ()
-checkWellStagedDFun pred dfun_id loc
- = wrapTcS $ TcM.setCtLoc loc $
+checkWellStagedDFun :: PredType -> DFunId -> CtLoc -> TcS ()
+checkWellStagedDFun pred dfun_id loc
+ = wrapTcS $ TcM.setCtLoc loc $
do { use_stage <- TcM.getStage
; TcM.checkWellStaged pp_thing bind_lvl (thLevel use_stage) }
where
@@ -1337,20 +1330,20 @@ pprEq :: TcType -> TcType -> SDoc
pprEq ty1 ty2 = pprType $ mkEqPred ty1 ty2
isTouchableMetaTyVarTcS :: TcTyVar -> TcS Bool
-isTouchableMetaTyVarTcS tv
+isTouchableMetaTyVarTcS tv
= do { untch <- getUntouchables
- ; return $ isTouchableMetaTyVar untch tv }
+ ; return $ isTouchableMetaTyVar untch tv }
isFilledMetaTyVar_maybe :: TcTyVar -> TcS (Maybe Type)
isFilledMetaTyVar_maybe tv
= ASSERT2( isTcTyVar tv, ppr tv )
case tcTyVarDetails tv of
- MetaTv { mtv_ref = ref }
+ MetaTv { mtv_ref = ref }
-> do { cts <- wrapTcS (TcM.readTcRef ref)
- ; case cts of
+ ; case cts of
Indirect ty -> return (Just ty)
Flexi -> return Nothing }
- _ -> return Nothing
+ _ -> return Nothing
zonkTyVarsAndFV :: TcTyVarSet -> TcS TcTyVarSet
zonkTyVarsAndFV tvs = wrapTcS (TcM.zonkTyVarsAndFV tvs)
@@ -1380,8 +1373,8 @@ it is only used if the program has a type error anyway.
Example of (b): assume a top-level class and instance declaration:
- class D a b | a -> b
- instance D [a] [a]
+ class D a b | a -> b
+ instance D [a] [a]
Assume we have started with an implication:
@@ -1410,15 +1403,15 @@ which will result in two Deriveds to end up in the insoluble set:
\begin{code}
-- Flatten skolems
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-newFlattenSkolem :: CtFlavour
+newFlattenSkolem :: CtFlavour
-> TcType -- F xis
-> TcS (CtEvidence, TcType) -- co :: F xis ~ ty
-- We have already looked up in the cache; no need to so so again
newFlattenSkolem Given fam_ty
- = do { tv <- wrapTcS $
+ = do { tv <- wrapTcS $
do { uniq <- TcM.newUnique
; let name = TcM.mkTcTyVarName uniq (fsLit "f")
- ; return $ mkTcTyVar name (typeKind fam_ty) (FlatSkol fam_ty) }
+ ; return $ mkTcTyVar name (typeKind fam_ty) (FlatSkol fam_ty) }
; traceTcS "New Flatten Skolem Born" $
ppr tv <+> text "[:= " <+> ppr fam_ty <+> text "]"
@@ -1426,7 +1419,7 @@ newFlattenSkolem Given fam_ty
ctev = CtGiven { ctev_pred = mkTcEqPred fam_ty rhs_ty
, ctev_evtm = EvCoercion (mkTcReflCo fam_ty) }
; dflags <- getDynFlags
- ; updInertTcS $ \ is@(IS { inert_fsks = fsks }) ->
+ ; updInertTcS $ \ is@(IS { inert_fsks = fsks }) ->
extendFlatCache dflags fam_ty ctev rhs_ty
is { inert_fsks = tv : fsks }
@@ -1447,14 +1440,14 @@ extendFlatCache dflags
| not (gopt Opt_FlatCache dflags)
= \ _ _ _ is -> is
| otherwise
- = \ fam_ty ctev rhs_ty is@(IS { inert_flat_cache = fc }) ->
+ = \ fam_ty ctev rhs_ty is@(IS { inert_flat_cache = fc }) ->
is { inert_flat_cache = insertFamHead fc fam_ty (ctev,rhs_ty) }
--- Instantiations
+-- Instantiations
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
instDFunType :: DFunId -> [DFunInstType] -> TcS ([TcType], TcType)
-instDFunType dfun_id mb_inst_tys
+instDFunType dfun_id mb_inst_tys
= wrapTcS $ go dfun_tvs mb_inst_tys (mkTopTvSubst [])
where
(dfun_tvs, dfun_phi) = tcSplitForAllTys (idType dfun_id)
@@ -1472,7 +1465,7 @@ instDFunType dfun_id mb_inst_tys
; return (ty : tys, phi) }
go _ _ _ = pprPanic "instDFunTypes" (ppr dfun_id $$ ppr mb_inst_tys)
-newFlexiTcSTy :: Kind -> TcS TcType
+newFlexiTcSTy :: Kind -> TcS TcType
newFlexiTcSTy knd = wrapTcS (TcM.newFlexiTyVarTy knd)
cloneMetaTyVar :: TcTyVar -> TcS TcTyVar
@@ -1481,16 +1474,16 @@ cloneMetaTyVar tv = wrapTcS (TcM.cloneMetaTyVar tv)
instFlexiTcS :: [TKVar] -> TcS (TvSubst, [TcType])
instFlexiTcS tvs = wrapTcS (mapAccumLM inst_one emptyTvSubst tvs)
where
- inst_one subst tv
- = do { ty' <- instFlexiTcSHelper (tyVarName tv)
+ inst_one subst tv
+ = do { ty' <- instFlexiTcSHelper (tyVarName tv)
(substTy subst (tyVarKind tv))
; return (extendTvSubst subst tv ty', ty') }
instFlexiTcSHelper :: Name -> Kind -> TcM TcType
instFlexiTcSHelper tvname kind
- = do { uniq <- TcM.newUnique
+ = do { uniq <- TcM.newUnique
; details <- TcM.newMetaDetails TauTv
- ; let name = setNameUnique tvname uniq
+ ; let name = setNameUnique tvname uniq
; return (mkTyVarTy (mkTcTyVar name kind details)) }
instFlexiTcSHelperTcS :: Name -> Kind -> TcS TcType
@@ -1500,11 +1493,11 @@ instFlexiTcSHelperTcS n k = wrapTcS (instFlexiTcSHelper n k)
-- Creating and setting evidence variables and CtFlavors
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-data XEvTerm =
+data XEvTerm =
XEvTerm { ev_comp :: [EvTerm] -> EvTerm
- -- How to compose evidence
+ -- How to compose evidence
, ev_decomp :: EvTerm -> [EvTerm]
- -- How to decompose evidence
+ -- How to decompose evidence
}
data MaybeNew = Fresh CtEvidence | Cached EvTerm
@@ -1535,7 +1528,7 @@ setEvBind the_ev tm
; wrapTcS $ TcM.addTcEvBind tc_evbinds the_ev tm }
newGivenEvVar :: TcPredType -> EvTerm -> TcS CtEvidence
--- Make a new variable of the given PredType,
+-- Make a new variable of the given PredType,
-- immediately bind it to the given term
-- and return its CtEvidence
newGivenEvVar pred rhs
@@ -1553,7 +1546,7 @@ newWantedEvVar :: TcPredType -> TcS MaybeNew
newWantedEvVar pty
= do { mb_ct <- lookupInInerts pty
; case mb_ct of
- Just ctev | not (isDerived ctev)
+ Just ctev | not (isDerived ctev)
-> do { traceTcS "newWantedEvVar/cache hit" $ ppr ctev
; return (Cached (ctEvTerm ctev)) }
_ -> do { ctev <- newWantedEvVarNC pty
@@ -1561,7 +1554,7 @@ newWantedEvVar pty
; return (Fresh ctev) } }
newDerived :: TcPredType -> TcS (Maybe CtEvidence)
--- Returns Nothing if cached,
+-- Returns Nothing if cached,
-- Just pred if not cached
newDerived pty
= do { mb_ct <- lookupInInerts pty
@@ -1572,7 +1565,7 @@ newDerived pty
instDFunConstraints :: TcThetaType -> TcS [MaybeNew]
instDFunConstraints = mapM newWantedEvVar
\end{code}
-
+
Note [xCFlavor]
~~~~~~~~~~~~~~~
@@ -1580,14 +1573,14 @@ A call might look like this:
xCtFlavor ev subgoal-preds evidence-transformer
- ev is Given => use ev_decomp to create new Givens for subgoal-preds,
+ ev is Given => use ev_decomp to create new Givens for subgoal-preds,
and return them
- ev is Wanted => create new wanteds for subgoal-preds,
- use ev_comp to bind ev,
+ ev is Wanted => create new wanteds for subgoal-preds,
+ use ev_comp to bind ev,
return fresh wanteds (ie ones not cached in inert_cans or solved)
- ev is Derived => create new deriveds for subgoal-preds
+ ev is Derived => create new deriveds for subgoal-preds
(unless cached in inert_cans or solved)
Note: The [CtEvidence] returned is a subset of the subgoal-preds passed in
@@ -1614,7 +1607,7 @@ See Note [Coercion evidence terms] in TcEvidence.
\begin{code}
-xCtFlavor :: CtEvidence -- Original flavor
+xCtFlavor :: CtEvidence -- Original flavor
-> [TcPredType] -- New predicate types
-> XEvTerm -- Instructions about how to manipulate evidence
-> TcS [CtEvidence]
@@ -1623,12 +1616,12 @@ xCtFlavor (CtGiven { ctev_evtm = tm }) ptys xev
= ASSERT( equalLength ptys (ev_decomp xev tm) )
zipWithM newGivenEvVar ptys (ev_decomp xev tm)
-- See Note [Bind new Givens immediately]
-
-xCtFlavor ctev@(CtWanted { ctev_evar = evar }) ptys xev
+
+xCtFlavor (CtWanted { ctev_evar = evar }) ptys xev
= do { new_evars <- mapM newWantedEvVar ptys
; setEvBind evar (ev_comp xev (getEvTerms new_evars))
; return (freshGoals new_evars) }
-
+
xCtFlavor (CtDerived {}) ptys _xev
= do { ders <- mapM newDerived ptys
; return (catMaybes ders) }
@@ -1636,12 +1629,12 @@ xCtFlavor (CtDerived {}) ptys _xev
-----------------------------
rewriteCtFlavor :: CtEvidence
-> TcPredType -- new predicate
- -> TcCoercion -- new ~ old
+ -> TcCoercion -- new ~ old
-> TcS (Maybe CtEvidence)
-- Returns Just new_fl iff either (i) 'co' is reflexivity
-- or (ii) 'co' is not reflexivity, and 'new_pred' not cached
-- In either case, there is nothing new to do with new_fl
-{-
+{-
rewriteCtFlavor old_fl new_pred co
Main purpose: create new evidence for new_pred;
unless new_pred is cached already
@@ -1665,13 +1658,13 @@ Main purpose: create new evidence for new_pred;
rewriteCtFlavor (CtDerived {}) new_pred _co
= -- If derived, don't even look at the coercion.
-- This is very important, DO NOT re-order the equations for
- -- rewriteCtFlavor to put the isTcReflCo test first!
- -- Why? Because for *Derived* constraints, c, the coercion, which
- -- was produced by flattening, may contain suspended calls to
+ -- rewriteCtFlavor to put the isTcReflCo test first!
+ -- Why? Because for *Derived* constraints, c, the coercion, which
+ -- was produced by flattening, may contain suspended calls to
-- (ctEvTerm c), which fails for Derived constraints.
-- (Getting this wrong caused Trac #7384.)
newDerived new_pred
-
+
rewriteCtFlavor old_ev new_pred co
| isTcReflCo co -- If just reflexivity then you may re-use the same variable
= return (Just (if ctEvPred old_ev `eqType` new_pred
@@ -1688,16 +1681,15 @@ rewriteCtFlavor (CtGiven { ctev_evtm = old_tm }) new_pred co
; return (Just new_ev) }
where
new_tm = mkEvCast old_tm (mkTcSymCo co) -- mkEvCast optimises ReflCo
-
-rewriteCtFlavor (CtWanted { ctev_evar = evar, ctev_pred = old_pred }) new_pred co
+
+rewriteCtFlavor (CtWanted { ctev_evar = evar }) new_pred co
= do { new_evar <- newWantedEvVar new_pred
; setEvBind evar (mkEvCast (getEvTerm new_evar) co)
; case new_evar of
- Fresh ctev -> return (Just ctev)
+ Fresh ctev -> return (Just ctev)
_ -> return Nothing }
-
matchOpenFam :: TyCon -> [Type] -> TcS (Maybe FamInstMatch)
matchOpenFam tycon args = wrapTcS $ tcLookupFamInst tycon args
@@ -1724,7 +1716,7 @@ matchFam tycon args
| otherwise
= return Nothing
-
+
\end{code}
\begin{code}
@@ -1735,8 +1727,8 @@ deferTcSForAllEq :: (CtLoc,EvVar) -- Original wanted equality flavor
-> ([TyVar],TcType) -- ForAll tvs1 body1
-> ([TyVar],TcType) -- ForAll tvs2 body2
-> TcS ()
--- Some of this functionality is repeated from TcUnify,
--- consider having a single place where we create fresh implications.
+-- Some of this functionality is repeated from TcUnify,
+-- consider having a single place where we create fresh implications.
deferTcSForAllEq (loc,orig_ev) (tvs1,body1) (tvs2,body2)
= do { (subst1, skol_tvs) <- wrapTcS $ TcM.tcInstSkolTyVars tvs1
; let tys = mkTyVarTys skol_tvs
@@ -1750,21 +1742,21 @@ deferTcSForAllEq (loc,orig_ev) (tvs1,body1) (tvs2,body2)
; env <- wrapTcS $ TcM.getLclEnv
; let ev_binds = TcEvBinds ev_binds_var
new_ct = mkNonCanonical loc ctev
- new_co = evTermCoercion (ctEvTerm ctev)
+ new_co = evTermCoercion (ctEvTerm ctev)
new_untch = pushUntouchables (tcl_untch env)
- ; let wc = WC { wc_flat = singleCt new_ct
+ ; let wc = WC { wc_flat = singleCt new_ct
, wc_impl = emptyBag
, wc_insol = emptyCts }
imp = Implic { ic_untch = new_untch
, ic_skols = skol_tvs
, ic_fsks = []
, ic_given = []
- , ic_wanted = wc
+ , ic_wanted = wc
, ic_insol = False
, ic_binds = ev_binds_var
, ic_env = env
, ic_info = skol_info }
- ; updTcSImplics (consBag imp)
+ ; updTcSImplics (consBag imp)
; return (TcLetCo ev_binds new_co) }
; setEvBind orig_ev $
diff --git a/compiler/typecheck/TcSimplify.lhs b/compiler/typecheck/TcSimplify.lhs
index 14d7af5f01af..57bf399a79ba 100644
--- a/compiler/typecheck/TcSimplify.lhs
+++ b/compiler/typecheck/TcSimplify.lhs
@@ -1,15 +1,8 @@
\begin{code}
-{-# OPTIONS -fno-warn-tabs #-}
--- The above warning supression flag is a temporary kludge.
--- While working on this module you are encouraged to remove it and
--- detab the module (please do the detabbing in a separate patch). See
--- http://ghc.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#TabsvsSpaces
--- for details
-
-module TcSimplify(
+module TcSimplify(
simplifyInfer, quantifyPred,
simplifyAmbiguityCheck,
- simplifyDefault,
+ simplifyDefault,
simplifyRule, simplifyTop, simplifyInteractive,
solveWantedsTcM
) where
@@ -20,9 +13,9 @@ import TcRnTypes
import TcRnMonad
import TcErrors
import TcMType as TcM
-import TcType
+import TcType
import TcSMonad as TcS
-import TcInteract
+import TcInteract
import Kind ( defaultKind_maybe )
import Inst
import FunDeps ( growThetaTyVars )
@@ -31,7 +24,7 @@ import Class ( Class )
import Var
import Unique
import VarSet
-import VarEnv
+import VarEnv
import TcEvidence
import Name
import Bag
@@ -41,7 +34,7 @@ import PrelInfo
import PrelNames
import Control.Monad ( unless )
import DynFlags ( ExtensionFlag( Opt_AllowAmbiguousTypes ) )
-import Class ( classKey )
+import Class ( classKey )
import BasicTypes ( RuleName )
import Outputable
import FastString
@@ -50,7 +43,7 @@ import TrieMap () -- DV: for now
*********************************************************************************
-* *
+* *
* External interface *
* *
*********************************************************************************
@@ -62,7 +55,7 @@ simplifyTop :: WantedConstraints -> TcM (Bag EvBind)
-- but when there is nothing to quantify we don't wrap
-- in a degenerate implication, so we do that here instead
simplifyTop wanteds
- = do { traceTc "simplifyTop {" $ text "wanted = " <+> ppr wanteds
+ = do { traceTc "simplifyTop {" $ text "wanted = " <+> ppr wanteds
; ev_binds_var <- newTcEvBinds
; zonked_final_wc <- solveWantedsTcMWithEvBinds ev_binds_var wanteds simpl_top
; binds1 <- TcRnMonad.getTcEvBinds ev_binds_var
@@ -190,8 +183,8 @@ simplifyInteractive wanteds
simplifyTop wanteds
------------------
-simplifyDefault :: ThetaType -- Wanted; has no type variables in it
- -> TcM () -- Succeeds iff the constraint is soluble
+simplifyDefault :: ThetaType -- Wanted; has no type variables in it
+ -> TcM () -- Succeeds iff the constraint is soluble
simplifyDefault theta
= do { traceTc "simplifyInteractive" empty
; wanted <- newFlatWanteds DefaultOrigin theta
@@ -210,7 +203,7 @@ simplifyDefault theta
*********************************************************************************
-* *
+* *
* Inference
* *
***********************************************************************************
@@ -223,15 +216,15 @@ simplifyInfer :: Bool
-> WantedConstraints
-> TcM ([TcTyVar], -- Quantify over these type variables
[EvVar], -- ... and these constraints
- Bool, -- The monomorphism restriction did something
- -- so the results type is not as general as
- -- it could be
+ Bool, -- The monomorphism restriction did something
+ -- so the results type is not as general as
+ -- it could be
TcEvBinds) -- ... binding these evidence variables
simplifyInfer _top_lvl apply_mr name_taus wanteds
| isEmptyWC wanteds
= do { gbl_tvs <- tcGetGlobalTyVars
; qtkvs <- quantifyTyVars gbl_tvs (tyVarsOfTypes (map snd name_taus))
- ; traceTc "simplifyInfer: empty WC" (ppr name_taus $$ ppr qtkvs)
+ ; traceTc "simplifyInfer: empty WC" (ppr name_taus $$ ppr qtkvs)
; return (qtkvs, [], False, emptyTcEvBinds) }
| otherwise
@@ -248,7 +241,7 @@ simplifyInfer _top_lvl apply_mr name_taus wanteds
-- #4361, we have taken in out now. That's why we start
-- with step 2!
- -- Step 2) First try full-blown solving
+ -- Step 2) First try full-blown solving
-- NB: we must gather up all the bindings from doing
-- this solving; hence (runTcSWithEvBinds ev_binds_var).
@@ -258,17 +251,17 @@ simplifyInfer _top_lvl apply_mr name_taus wanteds
-- constraint.
; ev_binds_var <- newTcEvBinds
- ; wanted_transformed_incl_derivs
+ ; wanted_transformed_incl_derivs
<- solveWantedsTcMWithEvBinds ev_binds_var wanteds solve_wanteds
-- Post: wanted_transformed are zonked
-- Step 4) Candidates for quantification are an approximation of wanted_transformed
- -- NB: Already the fixpoint of any unifications that may have happened
+ -- NB: Already the fixpoint of any unifications that may have happened
-- NB: We do not do any defaulting when inferring a type, this can lead
-- to less polymorphic types, see Note [Default while Inferring]
-
- -- Step 5) Minimize the quantification candidates
- -- Step 6) Final candidates for quantification
+
+ -- Step 5) Minimize the quantification candidates
+ -- Step 6) Final candidates for quantification
-- We discard bindings, insolubles etc, because all we are
-- care aout it
@@ -281,8 +274,8 @@ simplifyInfer _top_lvl apply_mr name_taus wanteds
-- NB: must include derived errors
else do { gbl_tvs <- tcGetGlobalTyVars
; let quant_cand = approximateWC wanted_transformed
- meta_tvs = filter isMetaTyVar (varSetElems (tyVarsOfCts quant_cand))
- ; ((flats, _insols), _extra_binds) <- runTcS $
+ meta_tvs = filter isMetaTyVar (varSetElems (tyVarsOfCts quant_cand))
+ ; ((flats, _insols), _extra_binds) <- runTcS $
do { mapM_ (promoteAndDefaultTyVar untch gbl_tvs) meta_tvs
-- See Note [Promote _and_ default when inferring]
; _implics <- solveInteract quant_cand
@@ -294,24 +287,24 @@ simplifyInfer _top_lvl apply_mr name_taus wanteds
-- at this point. Nothing bad, but inferred contexts might
-- look complicated.
- -- NB: quant_pred_candidates is already the fixpoint of any
+ -- NB: quant_pred_candidates is already the fixpoint of any
-- unifications that may have happened
; gbl_tvs <- tcGetGlobalTyVars
; zonked_tau_tvs <- TcM.zonkTyVarsAndFV (tyVarsOfTypes (map snd name_taus))
; let poly_qtvs = growThetaTyVars quant_pred_candidates zonked_tau_tvs
`minusVarSet` gbl_tvs
pbound = filter (quantifyPred poly_qtvs) quant_pred_candidates
-
- -- Monomorphism restriction
+
+ -- Monomorphism restriction
constrained_tvs = tyVarsOfTypes pbound `unionVarSet` gbl_tvs
- mr_bites = apply_mr && not (null pbound)
+ mr_bites = apply_mr && not (null pbound)
- ; (qtvs, bound) <- if mr_bites
+ ; (qtvs, bound) <- if mr_bites
then do { qtvs <- quantifyTyVars constrained_tvs zonked_tau_tvs
; return (qtvs, []) }
else do { qtvs <- quantifyTyVars gbl_tvs poly_qtvs
; return (qtvs, pbound) }
-
+
; traceTc "simplifyWithApprox" $
vcat [ ptext (sLit "quant_pred_candidates =") <+> ppr quant_pred_candidates
, ptext (sLit "gbl_tvs=") <+> ppr gbl_tvs
@@ -324,7 +317,7 @@ simplifyInfer _top_lvl apply_mr name_taus wanteds
, ptext (sLit "qtvs =") <+> ppr qtvs ]
; if null qtvs && null bound
- then do { traceTc "} simplifyInfer/no implication needed" empty
+ then do { traceTc "} simplifyInfer/no implication needed" empty
; emitConstraints wanted_transformed
-- Includes insolubles (if -fdefer-type-errors)
-- as well as flats and implications
@@ -345,13 +338,13 @@ simplifyInfer _top_lvl apply_mr name_taus wanteds
, ic_fsks = [] -- wanted_tansformed arose only from solveWanteds
-- hence no flatten-skolems (which come from givens)
, ic_given = minimal_bound_ev_vars
- , ic_wanted = wanted_transformed
+ , ic_wanted = wanted_transformed
, ic_insol = False
, ic_binds = ev_binds_var
, ic_info = skol_info
, ic_env = tc_lcl_env }
; emitImplication implic
-
+
; traceTc "} simplifyInfer/produced residual implication for quantification" $
vcat [ ptext (sLit "implic =") <+> ppr implic
-- ic_skols, ic_given give rest of result
@@ -363,27 +356,27 @@ simplifyInfer _top_lvl apply_mr name_taus wanteds
, mr_bites, TcEvBinds ev_binds_var) } }
quantifyPred :: TyVarSet -- Quantifying over these
- -> PredType -> Bool -- True <=> quantify over this wanted
+ -> PredType -> Bool -- True <=> quantify over this wanted
quantifyPred qtvs pred
| isIPPred pred = True -- Note [Inheriting implicit parameters]
- | otherwise = tyVarsOfType pred `intersectsVarSet` qtvs
+ | otherwise = tyVarsOfType pred `intersectsVarSet` qtvs
\end{code}
Note [Inheriting implicit parameters]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider this:
- f x = (x::Int) + ?y
+ f x = (x::Int) + ?y
where f is *not* a top-level binding.
From the RHS of f we'll get the constraint (?y::Int).
There are two types we might infer for f:
- f :: Int -> Int
+ f :: Int -> Int
(so we get ?y from the context of f's definition), or
- f :: (?y::Int) => Int -> Int
+ f :: (?y::Int) => Int -> Int
At first you might think the first was better, because then
?y behaves like a free variable of the definition, rather than
@@ -405,7 +398,7 @@ type we have found. For two reasons
a) Minimise downstream errors
b) Avoid spurious errors from this function
-But NB that we must include *derived* errors in the check. Example:
+But NB that we must include *derived* errors in the check. Example:
(a::*) ~ Int#
We get an insoluble derived error *~#, and we don't want to discard
it before doing the isInsolubleWC test! (Trac #8262)
@@ -416,38 +409,38 @@ Our current plan is that defaulting only happens at simplifyTop and
not simplifyInfer. This may lead to some insoluble deferred constraints
Example:
-instance D g => C g Int b
+instance D g => C g Int b
constraint inferred = (forall b. 0 => C gamma alpha b) /\ Num alpha
-type inferred = gamma -> gamma
+type inferred = gamma -> gamma
-Now, if we try to default (alpha := Int) we will be able to refine the implication to
- (forall b. 0 => C gamma Int b)
-which can then be simplified further to
+Now, if we try to default (alpha := Int) we will be able to refine the implication to
+ (forall b. 0 => C gamma Int b)
+which can then be simplified further to
(forall b. 0 => D gamma)
Finally we /can/ approximate this implication with (D gamma) and infer the quantified
type: forall g. D g => g -> g
-Instead what will currently happen is that we will get a quantified type
+Instead what will currently happen is that we will get a quantified type
(forall g. g -> g) and an implication:
forall g. 0 => (forall b. 0 => C g alpha b) /\ Num alpha
-which, even if the simplifyTop defaults (alpha := Int) we will still be left with an
+which, even if the simplifyTop defaults (alpha := Int) we will still be left with an
unsolvable implication:
forall g. 0 => (forall b. 0 => D g)
-The concrete example would be:
+The concrete example would be:
h :: C g a s => g -> a -> ST s a
f (x::gamma) = (\_ -> x) (runST (h x (undefined::alpha)) + 1)
But it is quite tedious to do defaulting and resolve the implication constraints and
-we have not observed code breaking because of the lack of defaulting in inference so
+we have not observed code breaking because of the lack of defaulting in inference so
we don't do it for now.
Note [Minimize by Superclasses]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When we quantify over a constraint, in simplifyInfer we need to
quantify over a constraint that is minimal in some sense: For
instance, if the final wanted constraint is (Eq alpha, Ord alpha),
@@ -459,19 +452,19 @@ to check the original wanted.
Note [Avoid unecessary constraint simplification]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
- -------- NB NB NB (Jun 12) -------------
+ -------- NB NB NB (Jun 12) -------------
This note not longer applies; see the notes with Trac #4361.
But I'm leaving it in here so we remember the issue.)
----------------------------------------
When inferring the type of a let-binding, with simplifyInfer,
try to avoid unnecessarily simplifying class constraints.
-Doing so aids sharing, but it also helps with delicate
+Doing so aids sharing, but it also helps with delicate
situations like
instance C t => C [t] where ..
f :: C [t] => ....
- f x = let g y = ...(constraint C [t])...
+ f x = let g y = ...(constraint C [t])...
in ...
When inferring a type for 'g', we don't want to apply the
instance decl, because then we can't satisfy (C t). So we
@@ -482,7 +475,7 @@ This only half-works, but then let-generalisation only half-works.
*********************************************************************************
-* *
+* *
* RULES *
* *
***********************************************************************************
@@ -505,14 +498,14 @@ So we see whether the simplificaiotn step yielded any type errors,
and if so refrain from quantifying over *any* equalites.
\begin{code}
-simplifyRule :: RuleName
- -> WantedConstraints -- Constraints from LHS
- -> WantedConstraints -- Constraints from RHS
+simplifyRule :: RuleName
+ -> WantedConstraints -- Constraints from LHS
+ -> WantedConstraints -- Constraints from RHS
-> TcM ([EvVar], WantedConstraints) -- LHS evidence varaibles
-- See Note [Simplifying RULE constraints] in TcRule
simplifyRule name lhs_wanted rhs_wanted
- = do { -- We allow ourselves to unify environment
- -- variables: runTcS runs with NoUntouchables
+ = do { -- We allow ourselves to unify environment
+ -- variables: runTcS runs with NoUntouchables
(resid_wanted, _) <- solveWantedsTcM (lhs_wanted `andWC` rhs_wanted)
-- Post: these are zonked and unflattened
@@ -529,10 +522,10 @@ simplifyRule name lhs_wanted rhs_wanted
= not (t1 `eqType` t2)
| otherwise
= True
-
+
; traceTc "simplifyRule" $
vcat [ ptext (sLit "LHS of rule") <+> doubleQuotes (ftext name)
- , text "zonked_lhs_flats" <+> ppr zonked_lhs_flats
+ , text "zonked_lhs_flats" <+> ppr zonked_lhs_flats
, text "q_cts" <+> ppr q_cts
, text "non_q_cts" <+> ppr non_q_cts ]
@@ -542,7 +535,7 @@ simplifyRule name lhs_wanted rhs_wanted
*********************************************************************************
-* *
+* *
* Main Simplifier *
* *
***********************************************************************************
@@ -602,8 +595,8 @@ solveWantedsTcMWithEvBinds :: EvBindsVar
-- Returns a *zonked* result
-- We zonk when we finish primarily to un-flatten out any
-- flatten-skolems etc introduced by canonicalisation of
--- types involving type funuctions. Happily the result
--- is typically much smaller than the input, indeed it is
+-- types involving type funuctions. Happily the result
+-- is typically much smaller than the input, indeed it is
-- often empty.
solveWantedsTcMWithEvBinds ev_binds_var wc tcs_action
= do { traceTc "solveWantedsTcMWithEvBinds" $ text "wanted=" <+> ppr wc
@@ -616,7 +609,7 @@ solveWantedsTcM :: WantedConstraints -> TcM (WantedConstraints, Bag EvBind)
-- Return the evidence binds in the BagEvBinds result
-- Discards all Derived stuff in result
-- Postcondition: fully zonked and unflattened constraints
-solveWantedsTcM wanted
+solveWantedsTcM wanted
= do { ev_binds_var <- newTcEvBinds
; wanteds' <- solveWantedsTcMWithEvBinds ev_binds_var wanted solve_wanteds_and_drop
; binds <- TcRnMonad.getTcEvBinds ev_binds_var
@@ -625,37 +618,37 @@ solveWantedsTcM wanted
solve_wanteds_and_drop :: WantedConstraints -> TcS (WantedConstraints)
-- Since solve_wanteds returns the residual WantedConstraints,
-- it should always be called within a runTcS or something similar,
-solve_wanteds_and_drop wanted = do { wc <- solve_wanteds wanted
+solve_wanteds_and_drop wanted = do { wc <- solve_wanteds wanted
; return (dropDerivedWC wc) }
-solve_wanteds :: WantedConstraints -> TcS WantedConstraints
+solve_wanteds :: WantedConstraints -> TcS WantedConstraints
-- so that the inert set doesn't mindlessly propagate.
-- NB: wc_flats may be wanted /or/ derived now
-solve_wanteds wanted@(WC { wc_flat = flats, wc_impl = implics, wc_insol = insols })
+solve_wanteds wanted@(WC { wc_flat = flats, wc_impl = implics, wc_insol = insols })
= do { traceTcS "solveWanteds {" (ppr wanted)
- -- Try the flat bit, including insolubles. Solving insolubles a
- -- second time round is a bit of a waste; but the code is simple
- -- and the program is wrong anyway, and we don't run the danger
- -- of adding Derived insolubles twice; see
- -- TcSMonad Note [Do not add duplicate derived insolubles]
+ -- Try the flat bit, including insolubles. Solving insolubles a
+ -- second time round is a bit of a waste; but the code is simple
+ -- and the program is wrong anyway, and we don't run the danger
+ -- of adding Derived insolubles twice; see
+ -- TcSMonad Note [Do not add duplicate derived insolubles]
; traceTcS "solveFlats {" empty
; let all_flats = flats `unionBags` insols
; impls_from_flats <- solveInteract all_flats
; traceTcS "solveFlats end }" (ppr impls_from_flats)
- -- solve_wanteds iterates when it is able to float equalities
- -- out of one or more of the implications.
+ -- solve_wanteds iterates when it is able to float equalities
+ -- out of one or more of the implications.
; unsolved_implics <- simpl_loop 1 (implics `unionBags` impls_from_flats)
; (unsolved_flats, insoluble_flats) <- getInertUnsolved
-- We used to unflatten here but now we only do it once at top-level
-- during zonking -- see Note [Unflattening while zonking] in TcMType
- ; let wc = WC { wc_flat = unsolved_flats
- , wc_impl = unsolved_implics
+ ; let wc = WC { wc_flat = unsolved_flats
+ , wc_impl = unsolved_implics
, wc_insol = insoluble_flats }
-
+
; bb <- getTcEvBindsMap
; tb <- getTcSTyBindsMap
; traceTcS "solveWanteds }" $
@@ -691,24 +684,24 @@ simpl_loop n implics
solveNestedImplications :: Bag Implication
-> TcS (Cts, Bag Implication)
--- Precondition: the TcS inerts may contain unsolved flats which have
+-- Precondition: the TcS inerts may contain unsolved flats which have
-- to be converted to givens before we go inside a nested implication.
solveNestedImplications implics
| isEmptyBag implics
= return (emptyBag, emptyBag)
- | otherwise
+ | otherwise
= do { inerts <- getTcSInerts
; let thinner_inerts = prepareInertsForImplications inerts
-- See Note [Preparing inert set for implications]
-
- ; traceTcS "solveNestedImplications starting {" $
+
+ ; traceTcS "solveNestedImplications starting {" $
vcat [ text "original inerts = " <+> ppr inerts
, text "thinner_inerts = " <+> ppr thinner_inerts ]
-
+
; (floated_eqs, unsolved_implics)
<- flatMapBagPairM (solveImplication thinner_inerts) implics
- -- ... and we are back in the original TcS inerts
+ -- ... and we are back in the original TcS inerts
-- Notice that the original includes the _insoluble_flats so it was safe to ignore
-- them in the beginning of this function.
; traceTcS "solveNestedImplications end }" $
@@ -721,24 +714,24 @@ solveImplication :: InertSet
-> Implication -- Wanted
-> TcS (Cts, -- All wanted or derived floated equalities: var = type
Bag Implication) -- Unsolved rest (always empty or singleton)
--- Precondition: The TcS monad contains an empty worklist and given-only inerts
+-- Precondition: The TcS monad contains an empty worklist and given-only inerts
-- which after trying to solve this implication we must restore to their original value
solveImplication inerts
imp@(Implic { ic_untch = untch
, ic_binds = ev_binds
- , ic_skols = skols
+ , ic_skols = skols
, ic_fsks = old_fsks
, ic_given = givens
, ic_wanted = wanteds
, ic_info = info
, ic_env = env })
- = do { traceTcS "solveImplication {" (ppr imp)
+ = do { traceTcS "solveImplication {" (ppr imp)
-- Solve the nested constraints
-- NB: 'inerts' has empty inert_fsks
- ; (new_fsks, residual_wanted)
+ ; (new_fsks, residual_wanted)
<- nestImplicTcS ev_binds untch inerts $
- do { solveInteractGiven (mkGivenLoc info env) old_fsks givens
+ do { solveInteractGiven (mkGivenLoc info env) old_fsks givens
; residual_wanted <- solve_wanteds wanteds
-- solve_wanteds, *not* solve_wanteds_and_drop, because
-- we want to retain derived equalities so we can float
@@ -749,7 +742,7 @@ solveImplication inerts
; (floated_eqs, final_wanted)
<- floatEqualities (skols ++ new_fsks) givens residual_wanted
- ; let res_implic | isEmptyWC final_wanted
+ ; let res_implic | isEmptyWC final_wanted
= emptyBag
| otherwise
= unitBag (imp { ic_fsks = new_fsks
@@ -805,16 +798,16 @@ Consider floated_eqs (all wanted or derived):
simpl_loop. So we iterate if there any of these
\begin{code}
-floatEqualities :: [TcTyVar] -> [EvVar] -> WantedConstraints
+floatEqualities :: [TcTyVar] -> [EvVar] -> WantedConstraints
-> TcS (Cts, WantedConstraints)
-- Post: The returned FlavoredEvVar's are only Wanted or Derived
--- and come from the input wanted ev vars or deriveds
+-- and come from the input wanted ev vars or deriveds
-- Also performs some unifications, adding to monadically-carried ty_binds
-- These will be used when processing floated_eqs later
floatEqualities skols can_given wanteds@(WC { wc_flat = flats })
- | hasEqualities can_given
+ | hasEqualities can_given
= return (emptyBag, wanteds) -- Note [Float Equalities out of Implications]
- | otherwise
+ | otherwise
= do { let (float_eqs, remaining_flats) = partitionBag is_floatable flats
; untch <- TcS.getUntouchables
; mapM_ (promoteTyVar untch) (varSetElems (tyVarsOfCts float_eqs))
@@ -824,12 +817,12 @@ floatEqualities skols can_given wanteds@(WC { wc_flat = flats })
, text "Floated eqs =" <+> ppr float_eqs
, text "Ty binds =" <+> ppr ty_binds])
; return (float_eqs, wanteds { wc_flat = remaining_flats }) }
- where
+ where
-- See Note [Float equalities from under a skolem binding]
skol_set = fixVarSet mk_next (mkVarSet skols)
mk_next tvs = foldrBag grow_one tvs flats
grow_one (CFunEqCan { cc_tyargs = xis, cc_rhs = rhs }) tvs
- | intersectsVarSet tvs (tyVarsOfTypes xis)
+ | intersectsVarSet tvs (tyVarsOfTypes xis)
= tvs `unionVarSet` tyVarsOfType rhs
grow_one _ tvs = tvs
@@ -842,7 +835,7 @@ promoteTyVar :: Untouchables -> TcTyVar -> TcS ()
-- When we float a constraint out of an implication we must restore
-- invariant (MetaTvInv) in Note [Untouchable type variables] in TcType
-- See Note [Promoting unification variables]
-promoteTyVar untch tv
+promoteTyVar untch tv
| isFloatedTouchableMetaTyVar untch tv
= do { cloned_tv <- TcS.cloneMetaTyVar tv
; let rhs_tv = setMetaTyVarUntouchables cloned_tv untch
@@ -853,7 +846,7 @@ promoteTyVar untch tv
promoteAndDefaultTyVar :: Untouchables -> TcTyVarSet -> TyVar -> TcS ()
-- See Note [Promote _and_ default when inferring]
promoteAndDefaultTyVar untch gbl_tvs tv
- = do { tv1 <- if tv `elemVarSet` gbl_tvs
+ = do { tv1 <- if tv `elemVarSet` gbl_tvs
then return tv
else defaultTyVar tv
; promoteTyVar untch tv1 }
@@ -872,17 +865,17 @@ defaultTyVar the_tv
-- See Note [DefaultTyVar]
-- We keep the same Untouchables on tv'
- | otherwise = return the_tv -- The common case
+ | otherwise = return the_tv -- The common case
approximateWC :: WantedConstraints -> Cts
--- Postcondition: Wanted or Derived Cts
+-- Postcondition: Wanted or Derived Cts
-- See Note [ApproximateWC]
-approximateWC wc
+approximateWC wc
= float_wc emptyVarSet wc
- where
+ where
float_wc :: TcTyVarSet -> WantedConstraints -> Cts
- float_wc trapping_tvs (WC { wc_flat = flats, wc_impl = implics })
- = filterBag is_floatable flats `unionBags`
+ float_wc trapping_tvs (WC { wc_flat = flats, wc_impl = implics })
+ = filterBag is_floatable flats `unionBags`
do_bag (float_implic new_trapping_tvs) implics
where
new_trapping_tvs = fixVarSet grow trapping_tvs
@@ -901,9 +894,9 @@ approximateWC wc
| otherwise -- See Note [ApproximateWC]
= float_wc new_trapping_tvs (ic_wanted imp)
where
- new_trapping_tvs = trapping_tvs `extendVarSetList` ic_skols imp
+ new_trapping_tvs = trapping_tvs `extendVarSetList` ic_skols imp
`extendVarSetList` ic_fsks imp
-
+
do_bag :: (a -> Bag c) -> Bag a -> Bag c
do_bag f = foldrBag (unionBags.f) emptyBag
\end{code}
@@ -929,9 +922,9 @@ There are two caveats:
f TInt = 3::Int
- We get the implication (a ~ Int => res ~ Int), where so far we've decided
+ We get the implication (a ~ Int => res ~ Int), where so far we've decided
f :: T a -> res
- We don't want to float (res~Int) out because then we'll infer
+ We don't want to float (res~Int) out because then we'll infer
f :: T a -> Int
which is only on of the possible types. (GHC 7.6 accidentally *did*
float out of such implications, which meant it would happily infer
@@ -942,11 +935,11 @@ There are two caveats:
forall a. F a ~ beta, Integral beta
We don't want to float out (Integral beta). Doing so would be bad
when defaulting, because then we'll default beta:=Integer, and that
- makes the error message much worse; we'd get
+ makes the error message much worse; we'd get
Can't solve F a ~ Integer
rather than
Can't solve Integral (F a)
-
+
Moreover, floating out these "contaminated" constraints doesn't help
when generalising either. If we generalise over (Integral b), we still
can't solve the retained implication (forall a. F a ~ b). Indeed,
@@ -955,7 +948,7 @@ There are two caveats:
Note [DefaultTyVar]
~~~~~~~~~~~~~~~~~~~
defaultTyVar is used on any un-instantiated meta type variables to
-default the kind of OpenKind and ArgKind etc to *. This is important
+default the kind of OpenKind and ArgKind etc to *. This is important
to ensure that instance declarations match. For example consider
instance Show (a->b)
@@ -976,8 +969,8 @@ default is default_k we do not simply generate [D] (k ~ default_k) because:
(1) k may be ArgKind and default_k may be * so we will fail
(2) We need to rewrite all occurrences of the tv to be a type
- variable with the right kind and we choose to do this by rewriting
- the type variable /itself/ by a new variable which does have the
+ variable with the right kind and we choose to do this by rewriting
+ the type variable /itself/ by a new variable which does have the
right kind.
Note [Promote _and_ default when inferring]
@@ -985,8 +978,8 @@ Note [Promote _and_ default when inferring]
When we are inferring a type, we simplify the constraint, and then use
approximateWC to produce a list of candidate constraints. Then we MUST
- a) Promote any meta-tyvars that have been floated out by
- approximateWC, to restore invariant (MetaTvInv) described in
+ a) Promote any meta-tyvars that have been floated out by
+ approximateWC, to restore invariant (MetaTvInv) described in
Note [Untouchable type variables] in TcType.
b) Default the kind of any meta-tyyvars that are not mentioned in
@@ -994,66 +987,66 @@ approximateWC to produce a list of candidate constraints. Then we MUST
To see (b), suppose the constraint is (C ((a :: OpenKind) -> Int)), and we
have an instance (C ((x:*) -> Int)). The instance doesn't match -- but it
-should! If we don't solve the constraint, we'll stupidly quantify over
+should! If we don't solve the constraint, we'll stupidly quantify over
(C (a->Int)) and, worse, in doing so zonkQuantifiedTyVar will quantify over
(b:*) instead of (a:OpenKind), which can lead to disaster; see Trac #7332.
Trac #7641 is a simpler example.
Note [Float Equalities out of Implications]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-For ordinary pattern matches (including existentials) we float
-equalities out of implications, for instance:
- data T where
- MkT :: Eq a => a -> T
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+For ordinary pattern matches (including existentials) we float
+equalities out of implications, for instance:
+ data T where
+ MkT :: Eq a => a -> T
f x y = case x of MkT _ -> (y::Int)
-We get the implication constraint (x::T) (y::alpha):
+We get the implication constraint (x::T) (y::alpha):
forall a. [untouchable=alpha] Eq a => alpha ~ Int
We want to float out the equality into a scope where alpha is no
-longer untouchable, to solve the implication!
+longer untouchable, to solve the implication!
But we cannot float equalities out of implications whose givens may
yield or contain equalities:
- data T a where
+ data T a where
T1 :: T Int
T2 :: T Bool
- T3 :: T a
-
+ T3 :: T a
+
h :: T a -> a -> Int
-
- f x y = case x of
+
+ f x y = case x of
T1 -> y::Int
T2 -> y::Bool
T3 -> h x y
-We generate constraint, for (x::T alpha) and (y :: beta):
+We generate constraint, for (x::T alpha) and (y :: beta):
[untouchables = beta] (alpha ~ Int => beta ~ Int) -- From 1st branch
[untouchables = beta] (alpha ~ Bool => beta ~ Bool) -- From 2nd branch
- (alpha ~ beta) -- From 3rd branch
+ (alpha ~ beta) -- From 3rd branch
-If we float the equality (beta ~ Int) outside of the first implication and
+If we float the equality (beta ~ Int) outside of the first implication and
the equality (beta ~ Bool) out of the second we get an insoluble constraint.
But if we just leave them inside the implications we unify alpha := beta and
solve everything.
-Principle:
+Principle:
We do not want to float equalities out which may need the given *evidence*
to become soluble.
-Consequence: classes with functional dependencies don't matter (since there is
-no evidence for a fundep equality), but equality superclasses do matter (since
+Consequence: classes with functional dependencies don't matter (since there is
+no evidence for a fundep equality), but equality superclasses do matter (since
they carry evidence).
Note [Float equalities from under a skolem binding]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
You might worry about skolem escape with all this floating.
For example, consider
- [2] forall a. (a ~ F beta[2] delta,
+ [2] forall a. (a ~ F beta[2] delta,
Maybe beta[2] ~ gamma[1])
The (Maybe beta ~ gamma) doesn't mention 'a', so we float it, and
-solve with gamma := beta. But what if later delta:=Int, and
- F b Int = b.
+solve with gamma := beta. But what if later delta:=Int, and
+ F b Int = b.
Then we'd get a ~ beta[2], and solve to get beta:=a, and now the
skolem has escaped!
@@ -1072,16 +1065,16 @@ a) [2]forall a. (F a delta[1] ~ beta[2], delta[1] ~ Maybe beta[2])
b) [2]forall a. (F b ty ~ beta[2], G beta[2] ~ gamma[2])
c) [2]forall a. (F a ty ~ beta[2], delta[1] ~ Maybe beta[2])
-In (a) we *must* float out the second equality,
+In (a) we *must* float out the second equality,
else we can't solve at all (Trac #7804).
-In (b) we *must not* float out the second equality.
+In (b) we *must not* float out the second equality.
It will ultimately be solved (by flattening) in situ, but if we
float it we'll promote beta,gamma, and render the first equality insoluble.
In (c) it would be OK to float the second equality but better not to.
- If we flatten we see (delta[1] ~ Maybe (F a ty)), which is a
- skolem-escape problem. If we float the secodn equality we'll
+ If we flatten we see (delta[1] ~ Maybe (F a ty)), which is a
+ skolem-escape problem. If we float the secodn equality we'll
end up with (F a ty ~ beta'[1]), which is a less explicable error.
Hence we start with the skolems, grow them by the CFunEqCans, and
@@ -1099,17 +1092,17 @@ with two implications and a class with a functional dependency.
class C x y | x -> y
instance C [a] [a]
-
+
(I1) [untch=beta]forall b. 0 => F Int ~ [beta]
(I2) [untch=beta]forall c. 0 => F Int ~ [[alpha]] /\ C beta [c]
-We float (F Int ~ [beta]) out of I1, and we float (F Int ~ [[alpha]]) out of I2.
-They may react to yield that (beta := [alpha]) which can then be pushed inwards
+We float (F Int ~ [beta]) out of I1, and we float (F Int ~ [[alpha]]) out of I2.
+They may react to yield that (beta := [alpha]) which can then be pushed inwards
the leftover of I2 to get (C [alpha] [a]) which, using the FunDep, will mean that
(alpha := a). In the end we will have the skolem 'b' escaping in the untouchable
beta! Concrete example is in indexed_types/should_fail/ExtraTcsUntch.hs:
- class C x y | x -> y where
+ class C x y | x -> y where
op :: x -> y -> ()
instance C [a] [a]
@@ -1119,11 +1112,11 @@ beta! Concrete example is in indexed_types/should_fail/ExtraTcsUntch.hs:
h :: F Int -> ()
h = undefined
- data TEx where
- TEx :: a -> TEx
+ data TEx where
+ TEx :: a -> TEx
- f (x::beta) =
+ f (x::beta) =
let g1 :: forall b. b -> ()
g1 _ = h [x]
g2 z = case z of TEx y -> (h [[undefined]], op x [y])
@@ -1131,24 +1124,24 @@ beta! Concrete example is in indexed_types/should_fail/ExtraTcsUntch.hs:
-Note [Solving Family Equations]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Note [Solving Family Equations]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
After we are done with simplification we may be left with constraints of the form:
- [Wanted] F xis ~ beta
-If 'beta' is a touchable unification variable not already bound in the TyBinds
+ [Wanted] F xis ~ beta
+If 'beta' is a touchable unification variable not already bound in the TyBinds
then we'd like to create a binding for it, effectively "defaulting" it to be 'F xis'.
-When is it ok to do so?
- 1) 'beta' must not already be defaulted to something. Example:
+When is it ok to do so?
+ 1) 'beta' must not already be defaulted to something. Example:
[Wanted] F Int ~ beta <~ Will default [beta := F Int]
- [Wanted] F Char ~ beta <~ Already defaulted, can't default again. We
+ [Wanted] F Char ~ beta <~ Already defaulted, can't default again. We
have to report this as unsolved.
- 2) However, we must still do an occurs check when defaulting (F xis ~ beta), to
+ 2) However, we must still do an occurs check when defaulting (F xis ~ beta), to
set [beta := F xis] only if beta is not among the free variables of xis.
- 3) Notice that 'beta' can't be bound in ty binds already because we rewrite RHS
+ 3) Notice that 'beta' can't be bound in ty binds already because we rewrite RHS
of type family equations. See Inert Set invariants in TcInteract.
This solving is now happening during zonking, see Note [Unflattening while zonking]
@@ -1156,7 +1149,7 @@ in TcMType.
*********************************************************************************
-* *
+* *
* Defaulting and disamgiguation *
* *
*********************************************************************************
@@ -1164,16 +1157,16 @@ in TcMType.
\begin{code}
applyDefaultingRules :: Cts -> TcS Bool
-- True <=> I did some defaulting, reflected in ty_binds
-
+
-- Return some extra derived equalities, which express the
--- type-class default choice.
+-- type-class default choice.
applyDefaultingRules wanteds
- | isEmptyBag wanteds
+ | isEmptyBag wanteds
= return False
| otherwise
- = do { traceTcS "applyDefaultingRules { " $
+ = do { traceTcS "applyDefaultingRules { " $
text "wanteds =" <+> ppr wanteds
-
+
; info@(default_tys, _) <- getDefaultInfo
; let groups = findDefaultableGroups info wanteds
; traceTcS "findDefaultableGroups" $ vcat [ text "groups=" <+> ppr groups
@@ -1188,74 +1181,74 @@ applyDefaultingRules wanteds
\begin{code}
-findDefaultableGroups
+findDefaultableGroups
:: ( [Type]
, (Bool,Bool) ) -- (Overloaded strings, extended default rules)
- -> Cts -- Unsolved (wanted or derived)
+ -> Cts -- Unsolved (wanted or derived)
-> [[(Ct,Class,TcTyVar)]]
findDefaultableGroups (default_tys, (ovl_strings, extended_defaults)) wanteds
| null default_tys = []
| otherwise = filter is_defaultable_group (equivClasses cmp_tv unaries)
- where
+ where
unaries :: [(Ct, Class, TcTyVar)] -- (C tv) constraints
non_unaries :: [Ct] -- and *other* constraints
-
+
(unaries, non_unaries) = partitionWith find_unary (bagToList wanteds)
-- Finds unary type-class constraints
- find_unary cc
+ find_unary cc
| Just (cls,[ty]) <- getClassPredTys_maybe (ctPred cc)
, Just tv <- tcGetTyVar_maybe ty
- , isMetaTyVar tv -- We might have runtime-skolems in GHCi, and
+ , isMetaTyVar tv -- We might have runtime-skolems in GHCi, and
-- we definitely don't want to try to assign to those!
= Left (cc, cls, tv)
- find_unary cc = Right cc -- Non unary or non dictionary
+ find_unary cc = Right cc -- Non unary or non dictionary
- bad_tvs :: TcTyVarSet -- TyVars mentioned by non-unaries
- bad_tvs = foldr (unionVarSet . tyVarsOfCt) emptyVarSet non_unaries
+ bad_tvs :: TcTyVarSet -- TyVars mentioned by non-unaries
+ bad_tvs = foldr (unionVarSet . tyVarsOfCt) emptyVarSet non_unaries
cmp_tv (_,_,tv1) (_,_,tv2) = tv1 `compare` tv2
is_defaultable_group ds@((_,_,tv):_)
- = let b1 = isTyConableTyVar tv -- Note [Avoiding spurious errors]
+ = let b1 = isTyConableTyVar tv -- Note [Avoiding spurious errors]
b2 = not (tv `elemVarSet` bad_tvs)
b4 = defaultable_classes [cls | (_,cls,_) <- ds]
in (b1 && b2 && b4)
is_defaultable_group [] = panic "defaultable_group"
- defaultable_classes clss
+ defaultable_classes clss
| extended_defaults = any isInteractiveClass clss
| otherwise = all is_std_class clss && (any is_num_class clss)
-- In interactive mode, or with -XExtendedDefaultRules,
-- we default Show a to Show () to avoid graututious errors on "show []"
- isInteractiveClass cls
+ isInteractiveClass cls
= is_num_class cls || (classKey cls `elem` [showClassKey, eqClassKey, ordClassKey])
is_num_class cls = isNumericClass cls || (ovl_strings && (cls `hasKey` isStringClassKey))
- -- is_num_class adds IsString to the standard numeric classes,
+ -- is_num_class adds IsString to the standard numeric classes,
-- when -foverloaded-strings is enabled
is_std_class cls = isStandardClass cls || (ovl_strings && (cls `hasKey` isStringClassKey))
-- Similarly is_std_class
------------------------------
-disambigGroup :: [Type] -- The default types
+disambigGroup :: [Type] -- The default types
-> [(Ct, Class, TcTyVar)] -- All classes of the form (C a)
- -- sharing same type variable
+ -- sharing same type variable
-> TcS Bool -- True <=> something happened, reflected in ty_binds
disambigGroup [] _grp
= return False
disambigGroup (default_ty:default_tys) group
= do { traceTcS "disambigGroup {" (ppr group $$ ppr default_ty)
- ; success <- tryTcS $ -- Why tryTcS? If this attempt fails, we want to
+ ; success <- tryTcS $ -- Why tryTcS? If this attempt fails, we want to
-- discard all side effects from the attempt
do { setWantedTyBind the_tv default_ty
; implics_from_defaulting <- solveInteract wanteds
; MASSERT(isEmptyBag implics_from_defaulting)
-- I am not certain if any implications can be generated
-- but I am letting this fail aggressively if this ever happens.
-
+
; checkAllSolved }
; if success then
@@ -1278,7 +1271,7 @@ Note [Avoiding spurious errors]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When doing the unification for defaulting, we check for skolem
type variables, and simply don't default them. For example:
- f = (*) -- Monomorphic
+ f = (*) -- Monomorphic
g :: Num a => a -> a
g x = f x x
Here, we get a complaint when checking the type signature for g,
diff --git a/compiler/typecheck/TcType.lhs b/compiler/typecheck/TcType.lhs
index deab2a2e5357..9ccb08ac3c6e 100644
--- a/compiler/typecheck/TcType.lhs
+++ b/compiler/typecheck/TcType.lhs
@@ -4,28 +4,21 @@
%
\section[TcType]{Types used in the typechecker}
-This module provides the Type interface for front-end parts of the
-compiler. These parts
+This module provides the Type interface for front-end parts of the
+compiler. These parts
- * treat "source types" as opaque:
- newtypes, and predicates are meaningful.
- * look through usage types
+ * treat "source types" as opaque:
+ newtypes, and predicates are meaningful.
+ * look through usage types
The "tc" prefix is for "TypeChecker", because the type checker
is the principal client.
\begin{code}
-{-# OPTIONS -fno-warn-tabs #-}
--- The above warning supression flag is a temporary kludge.
--- While working on this module you are encouraged to remove it and
--- detab the module (please do the detabbing in a separate patch). See
--- http://ghc.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#TabsvsSpaces
--- for details
-
module TcType (
--------------------------------
- -- Types
- TcType, TcSigmaType, TcRhoType, TcTauType, TcPredType, TcThetaType,
+ -- Types
+ TcType, TcSigmaType, TcRhoType, TcTauType, TcPredType, TcThetaType,
TcTyVar, TcTyVarSet, TcKind, TcCoVar,
-- Untouchables
@@ -35,13 +28,13 @@ module TcType (
-- MetaDetails
UserTypeCtxt(..), pprUserTypeCtxt,
TcTyVarDetails(..), pprTcTyVarDetails, vanillaSkolemTv, superSkolemTv,
- MetaDetails(Flexi, Indirect), MetaInfo(..),
+ MetaDetails(Flexi, Indirect), MetaInfo(..),
isImmutableTyVar, isSkolemTyVar, isMetaTyVar, isMetaTyVarTy, isTyVarTy,
isSigTyVar, isOverlappableTyVar, isTyConableTyVar, isFlatSkolTyVar,
isAmbiguousTyVar, metaTvRef, metaTyVarInfo,
isFlexi, isIndirect, isRuntimeUnkSkol,
- isTypeVar, isKindVar,
- metaTyVarUntouchables, setMetaTyVarUntouchables,
+ isTypeVar, isKindVar,
+ metaTyVarUntouchables, setMetaTyVarUntouchables,
isTouchableMetaTyVar, isFloatedTouchableMetaTyVar,
--------------------------------
@@ -49,7 +42,7 @@ module TcType (
mkPhiTy, mkSigmaTy, mkTcEqPred,
--------------------------------
- -- Splitters
+ -- Splitters
-- These are important because they do not look through newtypes
tcView,
tcSplitForAllTys, tcSplitPhiTy, tcSplitPredFunTy_maybe,
@@ -58,20 +51,20 @@ module TcType (
tcSplitAppTy_maybe, tcSplitAppTy, tcSplitAppTys, repSplitAppTy_maybe,
tcInstHeadTyNotSynonym, tcInstHeadTyAppAllTyVars,
tcGetTyVar_maybe, tcGetTyVar,
- tcSplitSigmaTy, tcDeepSplitSigmaTy_maybe,
+ tcSplitSigmaTy, tcDeepSplitSigmaTy_maybe,
---------------------------------
- -- Predicates.
+ -- Predicates.
-- Again, newtypes are opaque
eqType, eqTypes, eqPred, cmpType, cmpTypes, cmpPred, eqTypeX,
pickyEqType, eqKind,
isSigmaTy, isOverloadedTy,
isDoubleTy, isFloatTy, isIntTy, isWordTy, isStringTy,
isIntegerTy, isBoolTy, isUnitTy, isCharTy,
- isTauTy, isTauTyCon, tcIsTyVarTy, tcIsForAllTy,
+ isTauTy, isTauTyCon, tcIsTyVarTy, tcIsForAllTy,
isSynFamilyTyConApp,
isPredTy, isTyVarClassPred,
-
+
---------------------------------
-- Misc type manipulators
deNoteType, occurCheckExpand, OccCheckResult(..),
@@ -81,9 +74,9 @@ module TcType (
evVarPred_maybe, evVarPred,
---------------------------------
- -- Predicate types
+ -- Predicate types
mkMinimalBySCs, transSuperClasses, immSuperClasses,
-
+
-- * Finding type instances
tcTyFamInsts,
@@ -102,45 +95,45 @@ module TcType (
isFFILabelTy, -- :: Type -> Bool
isFFIDotnetTy, -- :: DynFlags -> Type -> Bool
isFFIDotnetObjTy, -- :: Type -> Bool
- isFFITy, -- :: Type -> Bool
+ isFFITy, -- :: Type -> Bool
isFunPtrTy, -- :: Type -> Bool
- tcSplitIOType_maybe, -- :: Type -> Maybe Type
+ tcSplitIOType_maybe, -- :: Type -> Maybe Type
--------------------------------
-- Rexported from Kind
Kind, typeKind,
unliftedTypeKind, liftedTypeKind,
- openTypeKind, constraintKind, mkArrowKind, mkArrowKinds,
- isLiftedTypeKind, isUnliftedTypeKind, isSubOpenTypeKind,
+ openTypeKind, constraintKind, mkArrowKind, mkArrowKinds,
+ isLiftedTypeKind, isUnliftedTypeKind, isSubOpenTypeKind,
tcIsSubKind, splitKindFunTys, defaultKind,
--------------------------------
-- Rexported from Type
Type, PredType, ThetaType,
- mkForAllTy, mkForAllTys,
- mkFunTy, mkFunTys, zipFunTys,
+ mkForAllTy, mkForAllTys,
+ mkFunTy, mkFunTys, zipFunTys,
mkTyConApp, mkAppTy, mkAppTys, applyTy, applyTys,
mkTyVarTy, mkTyVarTys, mkTyConTy,
isClassPred, isEqPred, isIPPred,
mkClassPred,
isDictLikeTy,
- tcSplitDFunTy, tcSplitDFunHead,
- mkEqPred,
+ tcSplitDFunTy, tcSplitDFunHead,
+ mkEqPred,
-- Type substitutions
- TvSubst(..), -- Representation visible to a few friends
- TvSubstEnv, emptyTvSubst,
- mkOpenTvSubst, zipOpenTvSubst, zipTopTvSubst,
+ TvSubst(..), -- Representation visible to a few friends
+ TvSubstEnv, emptyTvSubst,
+ mkOpenTvSubst, zipOpenTvSubst, zipTopTvSubst,
mkTopTvSubst, notElemTvSubst, unionTvSubst,
- getTvSubstEnv, setTvSubstEnv, getTvInScope, extendTvInScope,
+ getTvSubstEnv, setTvSubstEnv, getTvInScope, extendTvInScope,
Type.lookupTyVar, Type.extendTvSubst, Type.substTyVarBndr,
extendTvSubstList, isInScope, mkTvSubst, zipTyEnv,
- Type.substTy, substTys, substTyWith, substTheta, substTyVar, substTyVars,
+ Type.substTy, substTys, substTyWith, substTheta, substTyVar, substTyVars,
- isUnLiftedType, -- Source types are always lifted
- isUnboxedTupleType, -- Ditto
- isPrimitiveType,
+ isUnLiftedType, -- Source types are always lifted
+ isUnboxedTupleType, -- Ditto
+ isPrimitiveType,
tyVarsOfType, tyVarsOfTypes, closeOverKinds,
tcTyVarsOfType, tcTyVarsOfTypes,
@@ -187,24 +180,24 @@ import Control.Applicative (Applicative(..))
\end{code}
%************************************************************************
-%* *
+%* *
\subsection{Types}
-%* *
+%* *
%************************************************************************
-The type checker divides the generic Type world into the
+The type checker divides the generic Type world into the
following more structured beasts:
sigma ::= forall tyvars. phi
- -- A sigma type is a qualified type
- --
- -- Note that even if 'tyvars' is empty, theta
- -- may not be: e.g. (?x::Int) => Int
+ -- A sigma type is a qualified type
+ --
+ -- Note that even if 'tyvars' is empty, theta
+ -- may not be: e.g. (?x::Int) => Int
- -- Note that 'sigma' is in prenex form:
- -- all the foralls are at the front.
- -- A 'phi' type has no foralls to the right of
- -- an arrow
+ -- Note that 'sigma' is in prenex form:
+ -- all the foralls are at the front.
+ -- A 'phi' type has no foralls to the right of
+ -- an arrow
phi :: theta => rho
@@ -222,13 +215,13 @@ tau ::= tyvar
-- provided it expands to the required form.
\begin{code}
-type TcTyVar = TyVar -- Used only during type inference
-type TcCoVar = CoVar -- Used only during type inference; mutable
-type TcType = Type -- A TcType can have mutable type variables
- -- Invariant on ForAllTy in TcTypes:
- -- forall a. T
- -- a cannot occur inside a MutTyVar in T; that is,
- -- T is "flattened" before quantifying over a
+type TcTyVar = TyVar -- Used only during type inference
+type TcCoVar = CoVar -- Used only during type inference; mutable
+type TcType = Type -- A TcType can have mutable type variables
+ -- Invariant on ForAllTy in TcTypes:
+ -- forall a. T
+ -- a cannot occur inside a MutTyVar in T; that is,
+ -- T is "flattened" before quantifying over a
-- These types do not have boxy type variables in them
type TcPredType = PredType
@@ -242,9 +235,9 @@ type TcTyVarSet = TyVarSet
%************************************************************************
-%* *
+%* *
\subsection{TyVarDetails}
-%* *
+%* *
%************************************************************************
TyVarDetails gives extra info about type variables, used during type
@@ -264,10 +257,10 @@ Consider this
Here, x and y have type sigs, which go into the environment. We used to
instantiate their types with skolem constants, and push those types into
the RHS, so we'd typecheck the RHS with type
- ( [a*], b*, c )
+ ( [a*], b*, c )
where a*, b* are skolem constants, and c is an ordinary meta type varible.
-The trouble is that the occurrences of z in the RHS force a* and b* to
+The trouble is that the occurrences of z in the RHS force a* and b* to
be the *same*, so we can't make them into skolem constants that don't unify
with each other. Alas.
@@ -294,12 +287,12 @@ data TcTyVarDetails
| FlatSkol TcType
-- The "skolem" obtained by flattening during
- -- constraint simplification
-
+ -- constraint simplification
+
-- In comments we will use the notation alpha[flat = ty]
-- to represent a flattening skolem variable alpha
-- identified with type ty.
-
+
| MetaTv { mtv_info :: MetaInfo
, mtv_ref :: IORef MetaDetails
, mtv_untch :: Untouchables } -- See Note [Untouchable type variables]
@@ -311,7 +304,7 @@ superSkolemTv = SkolemTv True -- Treat this as a completely distinct type
-----------------------------
data MetaDetails
- = Flexi -- Flexi type variables unify to become Indirects
+ = Flexi -- Flexi type variables unify to become Indirects
| Indirect TcType
instance Outputable MetaDetails where
@@ -319,86 +312,86 @@ instance Outputable MetaDetails where
ppr (Indirect ty) = ptext (sLit "Indirect") <+> ppr ty
data MetaInfo
- = TauTv -- This MetaTv is an ordinary unification variable
- -- A TauTv is always filled in with a tau-type, which
- -- never contains any ForAlls
+ = TauTv -- This MetaTv is an ordinary unification variable
+ -- A TauTv is always filled in with a tau-type, which
+ -- never contains any ForAlls
| PolyTv -- Like TauTv, but can unify with a sigma-type
- | SigTv -- A variant of TauTv, except that it should not be
- -- unified with a type, only with a type variable
- -- SigTvs are only distinguished to improve error messages
- -- see Note [Signature skolems]
- -- The MetaDetails, if filled in, will
- -- always be another SigTv or a SkolemTv
+ | SigTv -- A variant of TauTv, except that it should not be
+ -- unified with a type, only with a type variable
+ -- SigTvs are only distinguished to improve error messages
+ -- see Note [Signature skolems]
+ -- The MetaDetails, if filled in, will
+ -- always be another SigTv or a SkolemTv
-------------------------------------
-- UserTypeCtxt describes the origin of the polymorphic type
-- in the places where we need to an expression has that type
data UserTypeCtxt
- = FunSigCtxt Name -- Function type signature
- -- Also used for types in SPECIALISE pragmas
- | InfSigCtxt Name -- Inferred type for function
- | ExprSigCtxt -- Expression type signature
- | ConArgCtxt Name -- Data constructor argument
- | TySynCtxt Name -- RHS of a type synonym decl
- | LamPatSigCtxt -- Type sig in lambda pattern
- -- f (x::t) = ...
- | BindPatSigCtxt -- Type sig in pattern binding pattern
- -- (x::t, y) = e
+ = FunSigCtxt Name -- Function type signature
+ -- Also used for types in SPECIALISE pragmas
+ | InfSigCtxt Name -- Inferred type for function
+ | ExprSigCtxt -- Expression type signature
+ | ConArgCtxt Name -- Data constructor argument
+ | TySynCtxt Name -- RHS of a type synonym decl
+ | LamPatSigCtxt -- Type sig in lambda pattern
+ -- f (x::t) = ...
+ | BindPatSigCtxt -- Type sig in pattern binding pattern
+ -- (x::t, y) = e
| RuleSigCtxt Name -- LHS of a RULE forall
-- RULE "foo" forall (x :: a -> a). f (Just x) = ...
- | ResSigCtxt -- Result type sig
- -- f x :: t = ....
- | ForSigCtxt Name -- Foreign import or export signature
- | DefaultDeclCtxt -- Types in a default declaration
+ | ResSigCtxt -- Result type sig
+ -- f x :: t = ....
+ | ForSigCtxt Name -- Foreign import or export signature
+ | DefaultDeclCtxt -- Types in a default declaration
| InstDeclCtxt -- An instance declaration
- | SpecInstCtxt -- SPECIALISE instance pragma
- | ThBrackCtxt -- Template Haskell type brackets [t| ... |]
+ | SpecInstCtxt -- SPECIALISE instance pragma
+ | ThBrackCtxt -- Template Haskell type brackets [t| ... |]
| GenSigCtxt -- Higher-rank or impredicative situations
-- e.g. (f e) where f has a higher-rank type
-- We might want to elaborate this
| GhciCtxt -- GHCi command :kind <type>
- | ClassSCCtxt Name -- Superclasses of a class
- | SigmaCtxt -- Theta part of a normal for-all type
- -- f :: <S> => a -> a
- | DataTyCtxt Name -- Theta part of a data decl
- -- data <S> => T a = MkT a
+ | ClassSCCtxt Name -- Superclasses of a class
+ | SigmaCtxt -- Theta part of a normal for-all type
+ -- f :: <S> => a -> a
+ | DataTyCtxt Name -- Theta part of a data decl
+ -- data <S> => T a = MkT a
\end{code}
-- Notes re TySynCtxt
-- We allow type synonyms that aren't types; e.g. type List = []
--
--- If the RHS mentions tyvars that aren't in scope, we'll
+-- If the RHS mentions tyvars that aren't in scope, we'll
-- quantify over them:
--- e.g. type T = a->a
--- will become type T = forall a. a->a
+-- e.g. type T = a->a
+-- will become type T = forall a. a->a
--
--- With gla-exts that's right, but for H98 we should complain.
+-- With gla-exts that's right, but for H98 we should complain.
%************************************************************************
-%* *
- Untoucable type variables
-%* *
+%* *
+ Untoucable type variables
+%* *
%************************************************************************
Note [Untouchable type variables]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-* Each unification variable (MetaTv)
+* Each unification variable (MetaTv)
and each Implication
has a level number (of type Untouchables)
-
-* INVARIANTS. In a tree of Implications,
- (ImplicInv) The level number of an Implication is
+* INVARIANTS. In a tree of Implications,
+
+ (ImplicInv) The level number of an Implication is
STRICTLY GREATER THAN that of its parent
- (MetaTvInv) The level number of a unification variable is
- LESS THAN OR EQUAL TO that of its parent
+ (MetaTvInv) The level number of a unification variable is
+ LESS THAN OR EQUAL TO that of its parent
implication
* A unification variable is *touchable* if its level number
@@ -433,13 +426,13 @@ and NOW we can unify alpha.
The same idea of only unifying touchables solves another problem.
Suppose we had
- (F Int ~ uf[0]) /\ [1](forall a. C a => F Int ~ beta[1])
-In this example, beta is touchable inside the implication. The
-first solveInteract step leaves 'uf' un-unified. Then we move inside
+ (F Int ~ uf[0]) /\ [1](forall a. C a => F Int ~ beta[1])
+In this example, beta is touchable inside the implication. The
+first solveInteract step leaves 'uf' un-unified. Then we move inside
the implication where a new constraint
- uf ~ beta
-emerges. If we (wrongly) spontaneously solved it to get uf := beta,
-the whole implication disappears but when we pop out again we are left with
+ uf ~ beta
+emerges. If we (wrongly) spontaneously solved it to get uf := beta,
+the whole implication disappears but when we pop out again we are left with
(F Int ~ uf) which will be unified by our final solveCTyFunEqs stage and
uf will get unified *once more* to (F Int).
@@ -450,21 +443,21 @@ newtype Untouchables = Untouchables Int
noUntouchables :: Untouchables
noUntouchables = Untouchables 0 -- 0 = outermost level
-pushUntouchables :: Untouchables -> Untouchables
+pushUntouchables :: Untouchables -> Untouchables
pushUntouchables (Untouchables us) = Untouchables (us+1)
isFloatedTouchable :: Untouchables -> Untouchables -> Bool
-isFloatedTouchable (Untouchables ctxt_untch) (Untouchables tv_untch)
+isFloatedTouchable (Untouchables ctxt_untch) (Untouchables tv_untch)
= ctxt_untch < tv_untch
isTouchable :: Untouchables -> Untouchables -> Bool
-isTouchable (Untouchables ctxt_untch) (Untouchables tv_untch)
+isTouchable (Untouchables ctxt_untch) (Untouchables tv_untch)
= ctxt_untch == tv_untch -- NB: invariant ctxt_untch >= tv_untch
-- So <= would be equivalent
checkTouchableInvariant :: Untouchables -> Untouchables -> Bool
-- Checks (MetaTvInv) from Note [Untouchable type variables]
-checkTouchableInvariant (Untouchables ctxt_untch) (Untouchables tv_untch)
+checkTouchableInvariant (Untouchables ctxt_untch) (Untouchables tv_untch)
= ctxt_untch >= tv_untch
instance Outputable Untouchables where
@@ -473,9 +466,9 @@ instance Outputable Untouchables where
%************************************************************************
-%* *
- Pretty-printing
-%* *
+%* *
+ Pretty-printing
+%* *
%************************************************************************
\begin{code}
@@ -526,10 +519,10 @@ pprUserTypeCtxt (DataTyCtxt tc) = ptext (sLit "the context of the data type de
-- | Finds outermost type-family applications occuring in a type,
-- after expanding synonyms.
tcTyFamInsts :: Type -> [(TyCon, [Type])]
-tcTyFamInsts ty
+tcTyFamInsts ty
| Just exp_ty <- tcView ty = tcTyFamInsts exp_ty
tcTyFamInsts (TyVarTy _) = []
-tcTyFamInsts (TyConApp tc tys)
+tcTyFamInsts (TyConApp tc tys)
| isSynFamilyTyCon tc = [(tc, tys)]
| otherwise = concat (map tcTyFamInsts tys)
tcTyFamInsts (LitTy {}) = []
@@ -548,7 +541,7 @@ Note [Silly type synonym]
~~~~~~~~~~~~~~~~~~~~~~~~~
Consider
type T a = Int
-What are the free tyvars of (T x)? Empty, of course!
+What are the free tyvars of (T x)? Empty, of course!
Here's the example that Ralf Laemmel showed me:
foo :: (forall a. C u a -> C u a) -> u
mappend :: Monoid u => u -> u -> u
@@ -566,7 +559,7 @@ smart-app checking code --- see TcExpr.tcIdApp
On the other hand, consider a *top-level* definition
f = (\x -> x) :: T a -> T a
If we don't abstract over 'a' it'll get fixed to GHC.Prim.Any, and then
-if we have an application like (f "x") we get a confusing error message
+if we have an application like (f "x") we get a confusing error message
involving Any. So the conclusion is this: when generalising
- at top level use tyVarsOfType
- in nested bindings use exactTyVarsOfType
@@ -592,18 +585,18 @@ exactTyVarsOfTypes tys = foldr (unionVarSet . exactTyVarsOfType) emptyVarSet tys
\end{code}
%************************************************************************
-%* *
- Predicates
-%* *
+%* *
+ Predicates
+%* *
%************************************************************************
\begin{code}
isTouchableMetaTyVar :: Untouchables -> TcTyVar -> Bool
isTouchableMetaTyVar ctxt_untch tv
= ASSERT2( isTcTyVar tv, ppr tv )
- case tcTyVarDetails tv of
- MetaTv { mtv_untch = tv_untch }
- -> ASSERT2( checkTouchableInvariant ctxt_untch tv_untch,
+ case tcTyVarDetails tv of
+ MetaTv { mtv_untch = tv_untch }
+ -> ASSERT2( checkTouchableInvariant ctxt_untch tv_untch,
ppr tv $$ ppr tv_untch $$ ppr ctxt_untch )
isTouchable ctxt_untch tv_untch
_ -> False
@@ -611,7 +604,7 @@ isTouchableMetaTyVar ctxt_untch tv
isFloatedTouchableMetaTyVar :: Untouchables -> TcTyVar -> Bool
isFloatedTouchableMetaTyVar ctxt_untch tv
= ASSERT2( isTcTyVar tv, ppr tv )
- case tcTyVarDetails tv of
+ case tcTyVarDetails tv of
MetaTv { mtv_untch = tv_untch } -> isFloatedTouchable ctxt_untch tv_untch
_ -> False
@@ -621,24 +614,24 @@ isImmutableTyVar tv
| otherwise = True
isTyConableTyVar, isSkolemTyVar, isOverlappableTyVar,
- isMetaTyVar, isAmbiguousTyVar, isFlatSkolTyVar :: TcTyVar -> Bool
+ isMetaTyVar, isAmbiguousTyVar, isFlatSkolTyVar :: TcTyVar -> Bool
-isTyConableTyVar tv
- -- True of a meta-type variable that can be filled in
- -- with a type constructor application; in particular,
- -- not a SigTv
- = ASSERT( isTcTyVar tv)
+isTyConableTyVar tv
+ -- True of a meta-type variable that can be filled in
+ -- with a type constructor application; in particular,
+ -- not a SigTv
+ = ASSERT( isTcTyVar tv)
case tcTyVarDetails tv of
- MetaTv { mtv_info = SigTv } -> False
- _ -> True
-
+ MetaTv { mtv_info = SigTv } -> False
+ _ -> True
+
isFlatSkolTyVar tv
= ASSERT2( isTcTyVar tv, ppr tv )
case tcTyVarDetails tv of
FlatSkol {} -> True
_ -> False
-isSkolemTyVar tv
+isSkolemTyVar tv
= ASSERT2( isTcTyVar tv, ppr tv )
case tcTyVarDetails tv of
SkolemTv {} -> True
@@ -652,23 +645,23 @@ isOverlappableTyVar tv
SkolemTv overlappable -> overlappable
_ -> False
-isMetaTyVar tv
+isMetaTyVar tv
= ASSERT2( isTcTyVar tv, ppr tv )
case tcTyVarDetails tv of
- MetaTv {} -> True
- _ -> False
+ MetaTv {} -> True
+ _ -> False
-- isAmbiguousTyVar is used only when reporting type errors
-- It picks out variables that are unbound, namely meta
-- type variables and the RuntimUnk variables created by
-- RtClosureInspect.zonkRTTIType. These are "ambiguous" in
-- the sense that they stand for an as-yet-unknown type
-isAmbiguousTyVar tv
+isAmbiguousTyVar tv
= ASSERT2( isTcTyVar tv, ppr tv )
case tcTyVarDetails tv of
- MetaTv {} -> True
- RuntimeUnk {} -> True
- _ -> False
+ MetaTv {} -> True
+ RuntimeUnk {} -> True
+ _ -> False
isMetaTyVarTy :: TcType -> Bool
isMetaTyVarTy (TyVarTy tv) = isMetaTyVar tv
@@ -696,18 +689,18 @@ setMetaTyVarUntouchables tv untch
_ -> pprPanic "metaTyVarUntouchables" (ppr tv)
isSigTyVar :: Var -> Bool
-isSigTyVar tv
+isSigTyVar tv
= ASSERT( isTcTyVar tv )
case tcTyVarDetails tv of
- MetaTv { mtv_info = SigTv } -> True
- _ -> False
+ MetaTv { mtv_info = SigTv } -> True
+ _ -> False
metaTvRef :: TyVar -> IORef MetaDetails
-metaTvRef tv
+metaTvRef tv
= ASSERT2( isTcTyVar tv, ppr tv )
case tcTyVarDetails tv of
- MetaTv { mtv_ref = ref } -> ref
- _ -> pprPanic "metaTvRef" (ppr tv)
+ MetaTv { mtv_ref = ref } -> ref
+ _ -> pprPanic "metaTvRef" (ppr tv)
isFlexi, isIndirect :: MetaDetails -> Bool
isFlexi Flexi = True
@@ -725,9 +718,9 @@ isRuntimeUnkSkol x
%************************************************************************
-%* *
+%* *
\subsection{Tau, sigma and rho}
-%* *
+%* *
%************************************************************************
\begin{code}
@@ -738,7 +731,7 @@ mkPhiTy :: [PredType] -> Type -> Type
mkPhiTy theta ty = foldr mkFunTy ty theta
mkTcEqPred :: TcType -> TcType -> Type
--- During type checking we build equalities between
+-- During type checking we build equalities between
-- type variables with OpenKind or ArgKind. Ultimately
-- they will all settle, but we want the equality predicate
-- itself to have kind '*'. I think.
@@ -760,22 +753,22 @@ mkTcEqPred ty1 ty2
\begin{code}
isTauTy :: Type -> Bool
isTauTy ty | Just ty' <- tcView ty = isTauTy ty'
-isTauTy (TyVarTy _) = True
+isTauTy (TyVarTy _) = True
isTauTy (LitTy {}) = True
isTauTy (TyConApp tc tys) = all isTauTy tys && isTauTyCon tc
-isTauTy (AppTy a b) = isTauTy a && isTauTy b
-isTauTy (FunTy a b) = isTauTy a && isTauTy b
+isTauTy (AppTy a b) = isTauTy a && isTauTy b
+isTauTy (FunTy a b) = isTauTy a && isTauTy b
isTauTy (ForAllTy {}) = False
isTauTyCon :: TyCon -> Bool
-- Returns False for type synonyms whose expansion is a polytype
-isTauTyCon tc
+isTauTyCon tc
| Just (_, rhs) <- synTyConDefn_maybe tc = isTauTy rhs
| otherwise = True
---------------
getDFunTyKey :: Type -> OccName -- Get some string from a type, to be used to
- -- construct a dictionary function name
+ -- construct a dictionary function name
getDFunTyKey ty | Just ty' <- tcView ty = getDFunTyKey ty'
getDFunTyKey (TyVarTy tv) = getOccName tv
getDFunTyKey (TyConApp tc _) = getOccName tc
@@ -791,13 +784,13 @@ getDFunTyLitKey (StrTyLit n) = mkOccName Name.varName (show n) -- hm
%************************************************************************
-%* *
+%* *
\subsection{Expanding and splitting}
-%* *
+%* *
%************************************************************************
These tcSplit functions are like their non-Tc analogues, but
- *) they do not look through newtypes
+ *) they do not look through newtypes
However, they are non-monadic and do not follow through mutable type
variables. It's up to you to make sure this doesn't matter.
@@ -817,7 +810,7 @@ tcIsForAllTy _ = False
tcSplitPredFunTy_maybe :: Type -> Maybe (PredType, Type)
-- Split off the first predicate argument from a type
-tcSplitPredFunTy_maybe ty
+tcSplitPredFunTy_maybe ty
| Just ty' <- tcView ty = tcSplitPredFunTy_maybe ty'
tcSplitPredFunTy_maybe (FunTy arg res)
| isPredTy arg = Just (arg, res)
@@ -828,15 +821,15 @@ tcSplitPhiTy :: Type -> (ThetaType, Type)
tcSplitPhiTy ty
= split ty []
where
- split ty ts
+ split ty ts
= case tcSplitPredFunTy_maybe ty of
- Just (pred, ty) -> split ty (pred:ts)
- Nothing -> (reverse ts, ty)
+ Just (pred, ty) -> split ty (pred:ts)
+ Nothing -> (reverse ts, ty)
tcSplitSigmaTy :: Type -> ([TyVar], ThetaType, Type)
tcSplitSigmaTy ty = case tcSplitForAllTys ty of
- (tvs, rho) -> case tcSplitPhiTy rho of
- (theta, tau) -> (tvs, theta, tau)
+ (tvs, rho) -> case tcSplitPhiTy rho of
+ (theta, tau) -> (tvs, theta, tau)
-----------------------
tcDeepSplitSigmaTy_maybe
@@ -858,60 +851,60 @@ tcDeepSplitSigmaTy_maybe ty
-----------------------
tcTyConAppTyCon :: Type -> TyCon
tcTyConAppTyCon ty = case tcSplitTyConApp_maybe ty of
- Just (tc, _) -> tc
- Nothing -> pprPanic "tcTyConAppTyCon" (pprType ty)
+ Just (tc, _) -> tc
+ Nothing -> pprPanic "tcTyConAppTyCon" (pprType ty)
tcTyConAppArgs :: Type -> [Type]
tcTyConAppArgs ty = case tcSplitTyConApp_maybe ty of
- Just (_, args) -> args
- Nothing -> pprPanic "tcTyConAppArgs" (pprType ty)
+ Just (_, args) -> args
+ Nothing -> pprPanic "tcTyConAppArgs" (pprType ty)
tcSplitTyConApp :: Type -> (TyCon, [Type])
tcSplitTyConApp ty = case tcSplitTyConApp_maybe ty of
- Just stuff -> stuff
- Nothing -> pprPanic "tcSplitTyConApp" (pprType ty)
+ Just stuff -> stuff
+ Nothing -> pprPanic "tcSplitTyConApp" (pprType ty)
tcSplitTyConApp_maybe :: Type -> Maybe (TyCon, [Type])
tcSplitTyConApp_maybe ty | Just ty' <- tcView ty = tcSplitTyConApp_maybe ty'
tcSplitTyConApp_maybe (TyConApp tc tys) = Just (tc, tys)
tcSplitTyConApp_maybe (FunTy arg res) = Just (funTyCon, [arg,res])
- -- Newtypes are opaque, so they may be split
- -- However, predicates are not treated
- -- as tycon applications by the type checker
+ -- Newtypes are opaque, so they may be split
+ -- However, predicates are not treated
+ -- as tycon applications by the type checker
tcSplitTyConApp_maybe _ = Nothing
-----------------------
tcSplitFunTys :: Type -> ([Type], Type)
tcSplitFunTys ty = case tcSplitFunTy_maybe ty of
- Nothing -> ([], ty)
- Just (arg,res) -> (arg:args, res')
- where
- (args,res') = tcSplitFunTys res
+ Nothing -> ([], ty)
+ Just (arg,res) -> (arg:args, res')
+ where
+ (args,res') = tcSplitFunTys res
tcSplitFunTy_maybe :: Type -> Maybe (Type, Type)
tcSplitFunTy_maybe ty | Just ty' <- tcView ty = tcSplitFunTy_maybe ty'
tcSplitFunTy_maybe (FunTy arg res) | not (isPredTy arg) = Just (arg, res)
tcSplitFunTy_maybe _ = Nothing
- -- Note the typeKind guard
- -- Consider (?x::Int) => Bool
- -- We don't want to treat this as a function type!
- -- A concrete example is test tc230:
- -- f :: () -> (?p :: ()) => () -> ()
- --
- -- g = f () ()
+ -- Note the typeKind guard
+ -- Consider (?x::Int) => Bool
+ -- We don't want to treat this as a function type!
+ -- A concrete example is test tc230:
+ -- f :: () -> (?p :: ()) => () -> ()
+ --
+ -- g = f () ()
tcSplitFunTysN
- :: TcRhoType
- -> Arity -- N: Number of desired args
- -> ([TcSigmaType], -- Arg types (N or fewer)
- TcSigmaType) -- The rest of the type
+ :: TcRhoType
+ -> Arity -- N: Number of desired args
+ -> ([TcSigmaType], -- Arg types (N or fewer)
+ TcSigmaType) -- The rest of the type
tcSplitFunTysN ty n_args
| n_args == 0
= ([], ty)
| Just (arg,res) <- tcSplitFunTy_maybe ty
= case tcSplitFunTysN res (n_args - 1) of
- (args, res) -> (arg:args, res)
+ (args, res) -> (arg:args, res)
| otherwise
= ([], ty)
@@ -931,16 +924,16 @@ tcSplitAppTy_maybe ty = repSplitAppTy_maybe ty
tcSplitAppTy :: Type -> (Type, Type)
tcSplitAppTy ty = case tcSplitAppTy_maybe ty of
- Just stuff -> stuff
- Nothing -> pprPanic "tcSplitAppTy" (pprType ty)
+ Just stuff -> stuff
+ Nothing -> pprPanic "tcSplitAppTy" (pprType ty)
tcSplitAppTys :: Type -> (Type, [Type])
tcSplitAppTys ty
= go ty []
where
go ty args = case tcSplitAppTy_maybe ty of
- Just (ty', arg) -> go ty' (arg:args)
- Nothing -> (ty,args)
+ Just (ty', arg) -> go ty' (arg:args)
+ Nothing -> (ty,args)
-----------------------
tcGetTyVar_maybe :: Type -> Maybe TyVar
@@ -960,13 +953,13 @@ tcSplitDFunTy :: Type -> ([TyVar], [Type], Class, [Type])
-- We don't use tcSplitSigmaTy, because a DFun may (with NDP)
-- have non-Pred arguments, such as
-- df :: forall m. (forall b. Eq b => Eq (m b)) -> C m
---
--- Also NB splitFunTys, not tcSplitFunTys;
--- the latter specifically stops at PredTy arguments,
+--
+-- Also NB splitFunTys, not tcSplitFunTys;
+-- the latter specifically stops at PredTy arguments,
-- and we don't want to do that here
-tcSplitDFunTy ty
+tcSplitDFunTy ty
= case tcSplitForAllTys ty of { (tvs, rho) ->
- case splitFunTys rho of { (theta, tau) ->
+ case splitFunTys rho of { (theta, tau) ->
case tcSplitDFunHead tau of { (clas, tys) ->
(tvs, theta, clas, tys) }}}
@@ -991,23 +984,23 @@ tcInstHeadTyAppAllTyVars ty
= tcInstHeadTyAppAllTyVars ty'
| otherwise
= case ty of
- TyConApp _ tys -> ok (filter (not . isKind) tys) -- avoid kinds
- FunTy arg res -> ok [arg, res]
- _ -> False
+ TyConApp _ tys -> ok (filter (not . isKind) tys) -- avoid kinds
+ FunTy arg res -> ok [arg, res]
+ _ -> False
where
- -- Check that all the types are type variables,
- -- and that each is distinct
+ -- Check that all the types are type variables,
+ -- and that each is distinct
ok tys = equalLength tvs tys && hasNoDups tvs
- where
- tvs = mapCatMaybes get_tv tys
+ where
+ tvs = mapCatMaybes get_tv tys
- get_tv (TyVarTy tv) = Just tv -- through synonyms
+ get_tv (TyVarTy tv) = Just tv -- through synonyms
get_tv _ = Nothing
\end{code}
\begin{code}
pickyEqType :: TcType -> TcType -> Bool
--- Check when two types _look_ the same, _including_ synonyms.
+-- Check when two types _look_ the same, _including_ synonyms.
-- So (pickyEqType String [Char]) returns False
pickyEqType ty1 ty2
= go init_env ty1 ty2
@@ -1052,7 +1045,7 @@ See also Note [Type synonyms and canonicalization] in TcCanonical
\begin{code}
data OccCheckResult a
= OC_OK a
- | OC_Forall
+ | OC_Forall
| OC_NonTyVar
| OC_Occurs
@@ -1069,19 +1062,19 @@ instance Monad OccCheckResult where
OC_Forall >>= _ = OC_Forall
OC_NonTyVar >>= _ = OC_NonTyVar
OC_Occurs >>= _ = OC_Occurs
-
+
occurCheckExpand :: DynFlags -> TcTyVar -> Type -> OccCheckResult Type
-- See Note [Occurs check expansion]
--- Check whether
--- a) the given variable occurs in the given type.
+-- Check whether
+-- a) the given variable occurs in the given type.
-- b) there is a forall in the type (unless we have -XImpredicativeTypes
-- or it's a PolyTv
-- c) if it's a SigTv, ty should be a tyvar
--
-- We may have needed to do some type synonym unfolding in order to
-- get rid of the variable (or forall), so we also return the unfolded
--- version of the type, which is guaranteed to be syntactically free
--- of the given type variable. If the type is already syntactically
+-- version of the type, which is guaranteed to be syntactically free
+-- of the given type variable. If the type is already syntactically
-- free of the variable, then the same type is returned.
occurCheckExpand dflags tv ty
@@ -1092,7 +1085,7 @@ occurCheckExpand dflags tv ty
where
details = ASSERT2( isTcTyVar tv, ppr tv ) tcTyVarDetails tv
- impredicative
+ impredicative
= case details of
MetaTv { mtv_info = PolyTv } -> True
MetaTv { mtv_info = SigTv } -> False
@@ -1114,7 +1107,7 @@ occurCheckExpand dflags tv ty
fast_check (TyConApp _ tys) = all fast_check tys
fast_check (FunTy arg res) = fast_check arg && fast_check res
fast_check (AppTy fun arg) = fast_check fun && fast_check arg
- fast_check (ForAllTy tv' ty) = impredicative
+ fast_check (ForAllTy tv' ty) = impredicative
&& fast_check (tyVarKind tv')
&& (tv == tv' || fast_check ty)
@@ -1122,15 +1115,15 @@ occurCheckExpand dflags tv ty
| otherwise = return t
go ty@(LitTy {}) = return ty
go (AppTy ty1 ty2) = do { ty1' <- go ty1
- ; ty2' <- go ty2
- ; return (mkAppTy ty1' ty2') }
- go (FunTy ty1 ty2) = do { ty1' <- go ty1
- ; ty2' <- go ty2
- ; return (mkFunTy ty1' ty2') }
+ ; ty2' <- go ty2
+ ; return (mkAppTy ty1' ty2') }
+ go (FunTy ty1 ty2) = do { ty1' <- go ty1
+ ; ty2' <- go ty2
+ ; return (mkFunTy ty1' ty2') }
go ty@(ForAllTy tv' body_ty)
| not impredicative = OC_Forall
| not (fast_check (tyVarKind tv')) = OC_Occurs
- -- Can't expand away the kinds unless we create
+ -- Can't expand away the kinds unless we create
-- fresh variables which we don't want to do at this point.
-- In principle fast_check might fail because of a for-all
-- but we don't yet have poly-kinded tyvars so I'm not
@@ -1152,9 +1145,9 @@ occurCheckExpand dflags tv ty
\end{code}
%************************************************************************
-%* *
+%* *
\subsection{Predicate types}
-%* *
+%* *
%************************************************************************
Deconstructors and tests on predicate types
@@ -1200,7 +1193,7 @@ transSuperClasses :: Class -> [Type] -> [PredType]
transSuperClasses cls tys -- Superclasses of (cls tys),
-- excluding (cls tys) itself
= concatMap trans_sc (immSuperClasses cls tys)
- where
+ where
trans_sc :: PredType -> [PredType]
-- (trans_sc p) returns (p : p's superclasses)
trans_sc p = case classifyPredType p of
@@ -1211,20 +1204,20 @@ transSuperClasses cls tys -- Superclasses of (cls tys),
immSuperClasses :: Class -> [Type] -> [PredType]
immSuperClasses cls tys
= substTheta (zipTopTvSubst tyvars tys) sc_theta
- where
+ where
(tyvars,sc_theta,_,_) = classBigSig cls
\end{code}
%************************************************************************
-%* *
+%* *
\subsection{Predicates}
-%* *
+%* *
%************************************************************************
-isSigmaTy returns true of any qualified type. It doesn't *necessarily* have
+isSigmaTy returns true of any qualified type. It doesn't *necessarily* have
any foralls. E.g.
- f :: (?x::Int) => Int -> Int
+ f :: (?x::Int) => Int -> Int
\begin{code}
isSigmaTy :: Type -> Bool
@@ -1264,8 +1257,8 @@ isStringTy ty
is_tc :: Unique -> Type -> Bool
-- Newtypes are opaque to this
is_tc uniq ty = case tcSplitTyConApp_maybe ty of
- Just (tc, _) -> uniq == getUnique tc
- Nothing -> False
+ Just (tc, _) -> uniq == getUnique tc
+ Nothing -> False
\end{code}
\begin{code}
@@ -1273,16 +1266,16 @@ is_tc uniq ty = case tcSplitTyConApp_maybe ty of
-- hence no 'coreView'. This could, however, be changed without breaking
-- any code.
isSynFamilyTyConApp :: TcTauType -> Bool
-isSynFamilyTyConApp (TyConApp tc tys) = isSynFamilyTyCon tc &&
- length tys == tyConArity tc
+isSynFamilyTyConApp (TyConApp tc tys) = isSynFamilyTyCon tc &&
+ length tys == tyConArity tc
isSynFamilyTyConApp _other = False
\end{code}
%************************************************************************
-%* *
+%* *
\subsection{Misc}
-%* *
+%* *
%************************************************************************
\begin{code}
@@ -1294,14 +1287,14 @@ deNoteType ty = ty
tcTyVarsOfType :: Type -> TcTyVarSet
-- Just the *TcTyVars* free in the type
-- (Types.tyVarsOfTypes finds all free TyVars)
-tcTyVarsOfType (TyVarTy tv) = if isTcTyVar tv then unitVarSet tv
- else emptyVarSet
+tcTyVarsOfType (TyVarTy tv) = if isTcTyVar tv then unitVarSet tv
+ else emptyVarSet
tcTyVarsOfType (TyConApp _ tys) = tcTyVarsOfTypes tys
tcTyVarsOfType (LitTy {}) = emptyVarSet
-tcTyVarsOfType (FunTy arg res) = tcTyVarsOfType arg `unionVarSet` tcTyVarsOfType res
-tcTyVarsOfType (AppTy fun arg) = tcTyVarsOfType fun `unionVarSet` tcTyVarsOfType arg
+tcTyVarsOfType (FunTy arg res) = tcTyVarsOfType arg `unionVarSet` tcTyVarsOfType res
+tcTyVarsOfType (AppTy fun arg) = tcTyVarsOfType fun `unionVarSet` tcTyVarsOfType arg
tcTyVarsOfType (ForAllTy tyvar ty) = tcTyVarsOfType ty `delVarSet` tyvar
- -- We do sometimes quantify over skolem TcTyVars
+ -- We do sometimes quantify over skolem TcTyVars
tcTyVarsOfTypes :: [Type] -> TyVarSet
tcTyVarsOfTypes tys = foldr (unionVarSet.tcTyVarsOfType) emptyVarSet tys
@@ -1318,14 +1311,14 @@ orphNamesOfTyCon tycon = unitNameSet (getName tycon) `unionNameSets` case tyConC
orphNamesOfType :: Type -> NameSet
orphNamesOfType ty | Just ty' <- tcView ty = orphNamesOfType ty'
- -- Look through type synonyms (Trac #4912)
-orphNamesOfType (TyVarTy _) = emptyNameSet
+ -- Look through type synonyms (Trac #4912)
+orphNamesOfType (TyVarTy _) = emptyNameSet
orphNamesOfType (TyConApp tycon tys) = orphNamesOfTyCon tycon
`unionNameSets` orphNamesOfTypes tys
orphNamesOfType (LitTy {}) = emptyNameSet
-orphNamesOfType (FunTy arg res) = orphNamesOfType arg `unionNameSets` orphNamesOfType res
-orphNamesOfType (AppTy fun arg) = orphNamesOfType fun `unionNameSets` orphNamesOfType arg
-orphNamesOfType (ForAllTy _ ty) = orphNamesOfType ty
+orphNamesOfType (FunTy arg res) = orphNamesOfType arg `unionNameSets` orphNamesOfType res
+orphNamesOfType (AppTy fun arg) = orphNamesOfType fun `unionNameSets` orphNamesOfType arg
+orphNamesOfType (ForAllTy _ ty) = orphNamesOfType ty
orphNamesOfThings :: (a -> NameSet) -> [a] -> NameSet
orphNamesOfThings f = foldr (unionNameSets . f) emptyNameSet
@@ -1334,16 +1327,16 @@ orphNamesOfTypes :: [Type] -> NameSet
orphNamesOfTypes = orphNamesOfThings orphNamesOfType
orphNamesOfDFunHead :: Type -> NameSet
--- Find the free type constructors and classes
+-- Find the free type constructors and classes
-- of the head of the dfun instance type
-- The 'dfun_head_type' is because of
--- instance Foo a => Baz T where ...
+-- instance Foo a => Baz T where ...
-- The decl is an orphan if Baz and T are both not locally defined,
--- even if Foo *is* locally defined
-orphNamesOfDFunHead dfun_ty
+-- even if Foo *is* locally defined
+orphNamesOfDFunHead dfun_ty
= case tcSplitSigmaTy dfun_ty of
- (_, _, head_ty) -> orphNamesOfType head_ty
-
+ (_, _, head_ty) -> orphNamesOfType head_ty
+
orphNamesOfCo :: Coercion -> NameSet
orphNamesOfCo (Refl _ ty) = orphNamesOfType ty
orphNamesOfCo (TyConAppCo _ tc cos) = unitNameSet (getName tc) `unionNameSets` orphNamesOfCos cos
@@ -1378,9 +1371,9 @@ orphNamesOfCoAxBranch (CoAxBranch { cab_lhs = lhs, cab_rhs = rhs })
%************************************************************************
-%* *
+%* *
\subsection[TysWiredIn-ext-type]{External types}
-%* *
+%* *
%************************************************************************
The compiler's foreign function interface supports the passing of a
@@ -1406,7 +1399,7 @@ isFFITy ty = checkRepTyCon legalFFITyCon ty
isFFIArgumentTy :: DynFlags -> Safety -> Type -> Bool
-- Checks for valid argument type for a 'foreign import'
-isFFIArgumentTy dflags safety ty
+isFFIArgumentTy dflags safety ty
= checkRepTyCon (legalOutgoingTyCon dflags safety) ty
isFFIExternalTy :: Type -> Bool
@@ -1414,7 +1407,7 @@ isFFIExternalTy :: Type -> Bool
isFFIExternalTy ty = checkRepTyCon legalFEArgTyCon ty
isFFIImportResultTy :: DynFlags -> Type -> Bool
-isFFIImportResultTy dflags ty
+isFFIImportResultTy dflags ty
= checkRepTyCon (legalFIResultTyCon dflags) ty
isFFIExportResultTy :: Type -> Bool
@@ -1456,11 +1449,11 @@ isFFIPrimResultTy dflags ty
isFFIDotnetTy :: DynFlags -> Type -> Bool
isFFIDotnetTy dflags ty
- = checkRepTyCon (\ tc -> (legalFIResultTyCon dflags tc ||
- isFFIDotnetObjTy ty || isStringTy ty)) ty
- -- NB: isStringTy used to look through newtypes, but
- -- it no longer does so. May need to adjust isFFIDotNetTy
- -- if we do want to look through newtypes.
+ = checkRepTyCon (\ tc -> (legalFIResultTyCon dflags tc ||
+ isFFIDotnetObjTy ty || isStringTy ty)) ty
+ -- NB: isStringTy used to look through newtypes, but
+ -- it no longer does so. May need to adjust isFFIDotNetTy
+ -- if we do want to look through newtypes.
isFFIDotnetObjTy :: Type -> Bool
isFFIDotnetObjTy ty
@@ -1517,7 +1510,7 @@ legalFEArgTyCon tc
legalFIResultTyCon :: DynFlags -> TyCon -> Bool
legalFIResultTyCon dflags tc
| tc == unitTyCon = True
- | otherwise = marshalableTyCon dflags tc
+ | otherwise = marshalableTyCon dflags tc
legalFEResultTyCon :: TyCon -> Bool
legalFEResultTyCon tc
@@ -1536,26 +1529,26 @@ legalFFITyCon tc
marshalableTyCon :: DynFlags -> TyCon -> Bool
marshalableTyCon dflags tc
- = (xopt Opt_UnliftedFFITypes dflags
+ = (xopt Opt_UnliftedFFITypes dflags
&& isUnLiftedTyCon tc
&& not (isUnboxedTupleTyCon tc)
- && case tyConPrimRep tc of -- Note [Marshalling VoidRep]
- VoidRep -> False
- _ -> True)
+ && case tyConPrimRep tc of -- Note [Marshalling VoidRep]
+ VoidRep -> False
+ _ -> True)
|| boxedMarshalableTyCon tc
boxedMarshalableTyCon :: TyCon -> Bool
boxedMarshalableTyCon tc
= getUnique tc `elem` [ intTyConKey, int8TyConKey, int16TyConKey
- , int32TyConKey, int64TyConKey
- , wordTyConKey, word8TyConKey, word16TyConKey
- , word32TyConKey, word64TyConKey
- , floatTyConKey, doubleTyConKey
- , ptrTyConKey, funPtrTyConKey
- , charTyConKey
- , stablePtrTyConKey
- , boolTyConKey
- ]
+ , int32TyConKey, int64TyConKey
+ , wordTyConKey, word8TyConKey, word16TyConKey
+ , word32TyConKey, word64TyConKey
+ , floatTyConKey, doubleTyConKey
+ , ptrTyConKey, funPtrTyConKey
+ , charTyConKey
+ , stablePtrTyConKey
+ , boolTyConKey
+ ]
legalFIPrimArgTyCon :: DynFlags -> TyCon -> Bool
-- Check args of 'foreign import prim', only allow simple unlifted types.
@@ -1573,16 +1566,16 @@ legalFIPrimResultTyCon dflags tc
= xopt Opt_UnliftedFFITypes dflags
&& isUnLiftedTyCon tc
&& (isUnboxedTupleTyCon tc
- || case tyConPrimRep tc of -- Note [Marshalling VoidRep]
- VoidRep -> False
- _ -> True)
+ || case tyConPrimRep tc of -- Note [Marshalling VoidRep]
+ VoidRep -> False
+ _ -> True)
\end{code}
Note [Marshalling VoidRep]
~~~~~~~~~~~~~~~~~~~~~~~~~~
We don't treat State# (whose PrimRep is VoidRep) as marshalable.
In turn that means you can't write
- foreign import foo :: Int -> State# RealWorld
+ foreign import foo :: Int -> State# RealWorld
Reason: the back end falls over with panic "primRepHint:VoidRep";
- and there is no compelling reason to permit it
+ and there is no compelling reason to permit it
--
GitLab