Break up TcRnTypes, among other modules.
[ghc.git] / compiler / typecheck / TcSMonad.hs
index c5ffb05..ca6022f 100644 (file)
@@ -1,4 +1,4 @@
-{-# LANGUAGE CPP, TypeFamilies #-}
+{-# LANGUAGE CPP, DeriveFunctor, TypeFamilies #-}
 
 -- Type definitions for the constraint solver
 module TcSMonad (
@@ -19,7 +19,7 @@ module TcSMonad (
     nestTcS, nestImplicTcS, setEvBindsTcS,
     checkConstraintsTcS, checkTvConstraintsTcS,
 
-    runTcPluginTcS, addUsedGRE, addUsedGREs,
+    runTcPluginTcS, addUsedGRE, addUsedGREs, keepAlive,
     matchGlobalInst, TcM.ClsInstResult(..),
 
     QCInst(..),
@@ -33,8 +33,10 @@ module TcSMonad (
     MaybeNew(..), freshGoals, isFresh, getEvExpr,
 
     newTcEvBinds, newNoTcEvBinds,
-    newWantedEq, emitNewWantedEq,
-    newWanted, newWantedEvVar, newWantedNC, newWantedEvVarNC, newDerivedNC,
+    newWantedEq, newWantedEq_SI, emitNewWantedEq,
+    newWanted, newWanted_SI, newWantedEvVar,
+    newWantedNC, newWantedEvVarNC,
+    newDerivedNC,
     newBoundEvVarId,
     unifyTyVar, unflattenFmv, reportUnifications,
     setEvBind, setWantedEq,
@@ -137,8 +139,7 @@ import qualified TcMType as TcM
 import qualified ClsInst as TcM( matchGlobalInst, ClsInstResult(..) )
 import qualified TcEnv as TcM
        ( checkWellStaged, tcGetDefaultTys, tcLookupClass, tcLookupId, topIdLvl )
-import PrelNames( heqTyConKey, eqTyConKey )
-import ClsInst( InstanceWhat(..) )
+import ClsInst( InstanceWhat(..), safeOverlap, instanceReturnsDictCon )
 import Kind
 import TcType
 import DynFlags
@@ -163,6 +164,9 @@ import Bag
 import UniqSupply
 import Util
 import TcRnTypes
+import TcOrigin
+import Constraint
+import Predicate
 
 import Unique
 import UniqFM
@@ -212,7 +216,7 @@ It's very important to process equalities /first/:
   and then kicking it out later.  That's extra work compared to just
   doing the equality first.
 
-* (Avoiding fundep iteration) As Trac #14723 showed, it's possible to
+* (Avoiding fundep iteration) As #14723 showed, it's possible to
   get non-termination if we
       - Emit the Derived fundep equalities for a class constraint,
         generating some fresh unification variables.
@@ -245,7 +249,7 @@ see Note [The equality types story] in TysPrim.
 
 Failing to prioritise these is inefficient (more kick-outs etc).
 But, worse, it can prevent us spotting a "recursive knot" among
-Wanted constraints.  See comment:10 of Trac #12734 for a worked-out
+Wanted constraints.  See comment:10 of #12734 for a worked-out
 example.
 
 So we arrange to put these particular class constraints in the wl_eqs.
@@ -328,8 +332,7 @@ extendWorkListCt ct wl
        -> extendWorkListEq ct wl
 
      ClassPred cls _  -- See Note [Prioritise class equalities]
-       |  cls `hasKey` heqTyConKey
-       || cls `hasKey` eqTyConKey
+       |  isEqPredClass cls
        -> extendWorkListEq ct wl
 
      _ -> extendWorkListNonEq ct wl
@@ -483,6 +486,63 @@ Now 'd1' goes in inert_solved_dicts, and we can solve d2 directly from d1.
     d2 = d1
 
 See Note [Example of recursive dictionaries]
+
+VERY IMPORTANT INVARIANT:
+
+ (Solved Dictionary Invariant)
+    Every member of the inert_solved_dicts is the result
+    of applying an instance declaration that "takes a step"
+
+    An instance "takes a step" if it has the form
+        dfunDList d1 d2 = MkD (...) (...) (...)
+    That is, the dfun is lazy in its arguments, and guarantees to
+    immediately return a dictionary constructor.  NB: all dictionary
+    data constructors are lazy in their arguments.
+
+    This property is crucial to ensure that all dictionaries are
+    non-bottom, which in turn ensures that the whole "recursive
+    dictionary" idea works at all, even if we get something like
+        rec { d = dfunDList d dx }
+    See Note [Recursive superclasses] in TcInstDcls.
+
+ Reason:
+   - All instances, except two exceptions listed below, "take a step"
+     in the above sense
+
+   - Exception 1: local quantified constraints have no such guarantee;
+     indeed, adding a "solved dictionary" when appling a quantified
+     constraint led to the ability to define unsafeCoerce
+     in #17267.
+
+   - Exception 2: the magic built-in instace for (~) has no
+     such guarantee.  It behaves as if we had
+         class    (a ~# b) => (a ~ b) where {}
+         instance (a ~# b) => (a ~ b) where {}
+     The "dfun" for the instance is strict in the coercion.
+     Anyway there's no point in recording a "solved dict" for
+     (t1 ~ t2); it's not going to allow a recursive dictionary
+     to be constructed.  Ditto (~~) and Coercible.
+
+THEREFORE we only add a "solved dictionary"
+  - when applying an instance declaration
+  - subject to Exceptions 1 and 2 above
+
+In implementation terms
+  - TcSMonad.addSolvedDict adds a new solved dictionary,
+    conditional on the kind of instance
+
+  - It is only called when applying an instance decl,
+    in TcInteract.doTopReactDict
+
+  - ClsInst.InstanceWhat says what kind of instance was
+    used to solve the constraint.  In particular
+      * LocalInstance identifies quantified constraints
+      * BuiltinEqInstance identifies the strange built-in
+        instances for equality.
+
+  - ClsInst.instanceReturnsDictCon says which kind of
+    instance guarantees to return a dictionary constructor
+
 Other notes about solved dictionaries
 
 * See also Note [Do not add superclasses of solved dictionaries]
@@ -490,7 +550,7 @@ Other notes about solved dictionaries
 * The inert_solved_dicts field is not rewritten by equalities,
   so it may get out of date.
 
-* THe inert_solved_dicts are all Wanteds, never givens
+* The inert_solved_dicts are all Wanteds, never givens
 
 * We only cache dictionaries from top-level instances, not from
   local quantified constraints.  Reason: if we cached the latter
@@ -500,8 +560,8 @@ Other notes about solved dictionaries
 
 Note [Do not add superclasses of solved dictionaries]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Every member of inert_solved_dicts is the result of applying a dictionary
-function, NOT of applying superclass selection to anything.
+Every member of inert_solved_dicts is the result of applying a
+dictionary function, NOT of applying superclass selection to anything.
 Consider
 
         class Ord a => C a where
@@ -980,7 +1040,7 @@ head of the top-level application chain (a t1 .. tn).  See
 TcType.isTyVarHead. This is encoded in (K3b).
 
 Beware: if we make this test succeed too often, we kick out too much,
-and the solver might loop.  Consider (Trac #14363)
+and the solver might loop.  Consider (#14363)
   work item:   [G] a ~R f b
   inert item:  [G] b ~R f a
 In GHC 8.2 the completeness tests more aggressive, and kicked out
@@ -1043,7 +1103,7 @@ instance Outputable InertCans where
 Note [The improvement story and derived shadows]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Because Wanteds cannot rewrite Wanteds (see Note [Wanteds do not
-rewrite Wanteds] in TcRnTypes), we may miss some opportunities for
+rewrite Wanteds] in Constraint), we may miss some opportunities for
 solving.  Here's a classic example (indexed-types/should_fail/T4093a)
 
     Ambiguity check for f: (Foo e ~ Maybe e) => Foo e
@@ -1236,7 +1296,7 @@ This is triggered by test case typecheck/should_compile/SplitWD.
 
 Note [Examples of how Derived shadows helps completeness]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Trac #10009, a very nasty example:
+#10009, a very nasty example:
 
     f :: (UnF (F b) ~ b) => F b -> ()
 
@@ -1276,7 +1336,7 @@ useful unification.
 
 But (a) I have been unable to come up with an example of this
         happening
-    (b) see Trac #12660 for how adding the derived shadows
+    (b) see #12660 for how adding the derived shadows
         of a Given led to an infinite loop.
     (c) It's unlikely that rewriting derived Givens will lead
         to a unification because Givens don't mention touchable
@@ -1316,7 +1376,7 @@ because we've already added its superclasses.  So we won't re-add
 them.  If we forget the pend_sc flag, our cunning scheme for avoiding
 generating superclasses repeatedly will fail.
 
-See Trac #11379 for a case of this.
+See #11379 for a case of this.
 
 Note [Do not do improvement for WOnly]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -1347,7 +1407,7 @@ Reasons:
   with the inert [W] C Int b in the inert set; after all,
   it's the very constraint from which the [D] C Int Bool
   was split!  We can avoid this by not doing improvement
-  on [W] constraints. This came up in Trac #12860.
+  on [W] constraints. This came up in #12860.
 -}
 
 maybeEmitShadow :: InertCans -> Ct -> TcS Ct
@@ -1500,7 +1560,7 @@ addInertForAll new_qci
 
 {- Note [Do not add duplicate quantified instances]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Consider this (Trac #15244):
+Consider this (#15244):
 
   f :: (C g, D g) => ....
   class S g => C g where ...
@@ -1551,7 +1611,7 @@ rewrite the inerts. But we *must* kick out the first one, to get:
           [D] fmv1 ~ fmv2
 
 and now improvement will discover [D] alpha ~ beta. This is important;
-eg in Trac #9587.
+eg in #9587.
 
 So in kickOutRewritable we look at all the tyvars of the
 CFunEqCan, including the fsk.
@@ -1668,7 +1728,7 @@ kick_out_rewritable new_fr new_tv
     -- constraints, which perhaps may have become soluble after new_tv
     -- is substituted; ditto the dictionaries, which may include (a~b)
     -- or (a~~b) constraints.
-    kicked_out = foldrBag extendWorkListCt
+    kicked_out = foldr extendWorkListCt
                           (emptyWorkList { wl_eqs    = tv_eqs_out
                                          , wl_funeqs = feqs_out })
                           ((dicts_out `andCts` irs_out)
@@ -1810,7 +1870,7 @@ constructors match.
 
 Similarly, if we have a CHoleCan, we'd like to rewrite it with any
 Givens, to give as informative an error messasge as possible
-(Trac #12468, #11325).
+(#12468, #11325).
 
 Hence:
  * In the main simlifier loops in TcSimplify (solveWanteds,
@@ -1834,10 +1894,11 @@ addInertSafehask ics item@(CDictCan { cc_class = cls, cc_tyargs = tys })
 addInertSafehask _ item
   = pprPanic "addInertSafehask: can't happen! Inserting " $ ppr item
 
-insertSafeOverlapFailureTcS :: Ct -> TcS ()
+insertSafeOverlapFailureTcS :: InstanceWhat -> Ct -> TcS ()
 -- See Note [Safe Haskell Overlapping Instances Implementation] in TcSimplify
-insertSafeOverlapFailureTcS item
-  = updInertCans (\ics -> addInertSafehask ics item)
+insertSafeOverlapFailureTcS what item
+  | safeOverlap what = return ()
+  | otherwise        = updInertCans (\ics -> addInertSafehask ics item)
 
 getSafeOverlapFailures :: TcS Cts
 -- See Note [Safe Haskell Overlapping Instances Implementation] in TcSimplify
@@ -1846,16 +1907,17 @@ getSafeOverlapFailures
       ; return $ foldDicts consCts safehask emptyCts }
 
 --------------
-addSolvedDict :: CtEvidence -> Class -> [Type] -> TcS ()
--- Add a new item in the solved set of the monad
+addSolvedDict :: InstanceWhat -> CtEvidence -> Class -> [Type] -> TcS ()
+-- Conditionally add a new item in the solved set of the monad
 -- See Note [Solved dictionaries]
-addSolvedDict item cls tys
-  | isIPPred (ctEvPred item)    -- Never cache "solved" implicit parameters (not sure why!)
-  = return ()
-  | otherwise
+addSolvedDict what item cls tys
+  | isWanted item
+  , instanceReturnsDictCon what
   = do { traceTcS "updSolvedSetTcs:" $ ppr item
        ; updInertTcS $ \ ics ->
              ics { inert_solved_dicts = addDict (inert_solved_dicts ics) cls tys item } }
+  | otherwise
+  = return ()
 
 getSolvedDicts :: TcS (DictMap CtEvidence)
 getSolvedDicts = do { ics <- getTcSInerts; return (inert_solved_dicts ics) }
@@ -2054,7 +2116,7 @@ getNoGivenEqs :: TcLevel          -- TcLevel of this implication
 getNoGivenEqs tclvl skol_tvs
   = do { inerts@(IC { inert_eqs = ieqs, inert_irreds = irreds })
               <- getInertCans
-       ; let has_given_eqs = foldrBag ((||) . ct_given_here) False irreds
+       ; let has_given_eqs = foldr ((||) . ct_given_here) False irreds
                           || anyDVarEnv eqs_given_here ieqs
              insols = filterBag insolubleEqCt irreds
                       -- Specifically includes ones that originated in some
@@ -2157,7 +2219,7 @@ where beta is a unification variable that has already been unified
 to () in an outer scope.  Then we can float the (alpha ~ Int) out
 just fine. So when deciding whether the givens contain an equality,
 we should canonicalise first, rather than just looking at the original
-givens (Trac #8644).
+givens (#8644).
 
 So we simply look at the inert, canonical Givens and see if there are
 any equalities among them, the calculation of has_given_eqs.  There
@@ -2209,7 +2271,7 @@ b) 'a' will have been completely substituted out in the inert set,
    so we can safely discard it.  Notably, it doesn't need to be
    returned as part of 'fsks'
 
-For an example, see Trac #9211.
+For an example, see #9211.
 
 See also TcUnify Note [Deeper level on the left] for how we ensure
 that the right variable is on the left of the equality when both are
@@ -2217,7 +2279,7 @@ tyvars.
 
 You might wonder whether the skokem really needs to be bound "in the
 very same implication" as the equuality constraint.
-(c.f. Trac #15009) Consider this:
+(c.f. #15009) Consider this:
 
   data S a where
     MkS :: (a ~ Int) => S a
@@ -2317,7 +2379,7 @@ lookupSolvedDict (IS { inert_solved_dicts = solved }) loc cls tys
 ********************************************************************* -}
 
 foldIrreds :: (Ct -> b -> b) -> Cts -> b -> b
-foldIrreds k irreds z = foldrBag k z irreds
+foldIrreds k irreds z = foldr k z irreds
 
 
 {- *********************************************************************
@@ -2402,7 +2464,7 @@ Consider
 
 The call to 'g' gives rise to a Wanted constraint (?x::Int, C a).
 We must /not/ solve this from the Given (?x::Int, C a), because of
-the intervening binding for (?x::Int).  Trac #14218.
+the intervening binding for (?x::Int).  #14218.
 
 We deal with this by arranging that we always fail when looking up a
 tuple constraint that hides an implicit parameter. Not that this applies
@@ -2467,7 +2529,7 @@ addDict m cls tys item = insertTcApp m (getUnique cls) tys item
 
 addDictsByClass :: DictMap Ct -> Class -> Bag Ct -> DictMap Ct
 addDictsByClass m cls items
-  = addToUDFM m cls (foldrBag add emptyTM items)
+  = addToUDFM m cls (foldr add emptyTM items)
   where
     add ct@(CDictCan { cc_tyargs = tys }) tm = insertTM tys ct tm
     add ct _ = pprPanic "addDictsByClass" (ppr ct)
@@ -2601,10 +2663,7 @@ data TcSEnv
     }
 
 ---------------
-newtype TcS a = TcS { unTcS :: TcSEnv -> TcM a }
-
-instance Functor TcS where
-  fmap f m = TcS $ fmap f . unTcS m
+newtype TcS a = TcS { unTcS :: TcSEnv -> TcM a } deriving (Functor)
 
 instance Applicative TcS where
   pure x = TcS (\_ -> return x)
@@ -2765,7 +2824,7 @@ checkForCyclicBinds ev_binds_map
     cycles = [c | CyclicSCC c <- stronglyConnCompFromEdgedVerticesUniq edges]
 
     coercion_cycles = [c | c <- cycles, any is_co_bind c]
-    is_co_bind (EvBind { eb_lhs = b }) = isEqPred (varType b)
+    is_co_bind (EvBind { eb_lhs = b }) = isEqPrimPred (varType b)
 
     edges :: [ Node EvVar EvBind ]
     edges = [ DigraphNode bind bndr (nonDetEltsUniqSet (evVarsOfTerm rhs))
@@ -2875,7 +2934,7 @@ checkTvConstraintsTcS skol_info skol_tvs (TcS thing_inside)
 
        ; unless (null wanteds) $
          do { ev_binds_var <- TcM.newNoTcEvBinds
-            ; imp <- newImplication
+            ; imp <- TcM.newImplication
             ; let wc = emptyWC { wc_simple = wanteds }
                   imp' = imp { ic_tclvl  = new_tclvl
                              , ic_skols  = skol_tvs
@@ -2914,7 +2973,7 @@ checkConstraintsTcS skol_info skol_tvs given (TcS thing_inside)
                                         thing_inside new_tcs_env
 
        ; ev_binds_var <- TcM.newTcEvBinds
-       ; imp <- newImplication
+       ; imp <- TcM.newImplication
        ; let wc = emptyWC { wc_simple = wanteds }
              imp' = imp { ic_tclvl  = new_tclvl
                         , ic_skols  = skol_tvs
@@ -3069,6 +3128,8 @@ addUsedGREs gres = wrapTcS  $ TcM.addUsedGREs gres
 addUsedGRE :: Bool -> GlobalRdrElt -> TcS ()
 addUsedGRE warn_if_deprec gre = wrapTcS $ TcM.addUsedGRE warn_if_deprec gre
 
+keepAlive :: Name -> TcS ()
+keepAlive = wrapTcS . TcM.keepAlive
 
 -- Various smaller utilities [TODO, maybe will be absorbed in the instance matcher]
 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -3382,7 +3443,7 @@ newGivenEvVar :: CtLoc -> (TcPredType, EvTerm) -> TcS CtEvidence
 -- Make a new variable of the given PredType,
 -- immediately bind it to the given term
 -- and return its CtEvidence
--- See Note [Bind new Givens immediately] in TcRnTypes
+-- See Note [Bind new Givens immediately] in Constraint
 newGivenEvVar loc (pred, rhs)
   = do { new_ev <- newBoundEvVarId pred rhs
        ; return (CtGiven { ctev_pred = pred, ctev_evar = new_ev, ctev_loc = loc }) }
@@ -3406,12 +3467,18 @@ emitNewWantedEq loc role ty1 ty2
        ; return co }
 
 -- | Make a new equality CtEvidence
-newWantedEq :: CtLoc -> Role -> TcType -> TcType -> TcS (CtEvidence, Coercion)
-newWantedEq loc role ty1 ty2
+newWantedEq :: CtLoc -> Role -> TcType -> TcType
+            -> TcS (CtEvidence, Coercion)
+newWantedEq = newWantedEq_SI WDeriv
+
+newWantedEq_SI :: ShadowInfo -> CtLoc -> Role
+               -> TcType -> TcType
+               -> TcS (CtEvidence, Coercion)
+newWantedEq_SI si loc role ty1 ty2
   = do { hole <- wrapTcS $ TcM.newCoercionHole pty
        ; traceTcS "Emitting new coercion hole" (ppr hole <+> dcolon <+> ppr pty)
        ; return ( CtWanted { ctev_pred = pty, ctev_dest = HoleDest hole
-                           , ctev_nosh = WDeriv
+                           , ctev_nosh = si
                            , ctev_loc = loc}
                 , mkHoleCo hole ) }
   where
@@ -3419,35 +3486,44 @@ newWantedEq loc role ty1 ty2
 
 -- no equalities here. Use newWantedEq instead
 newWantedEvVarNC :: CtLoc -> TcPredType -> TcS CtEvidence
+newWantedEvVarNC = newWantedEvVarNC_SI WDeriv
+
+newWantedEvVarNC_SI :: ShadowInfo -> CtLoc -> TcPredType -> TcS CtEvidence
 -- Don't look up in the solved/inerts; we know it's not there
-newWantedEvVarNC loc pty
+newWantedEvVarNC_SI si loc pty
   = do { new_ev <- newEvVar pty
        ; traceTcS "Emitting new wanted" (ppr new_ev <+> dcolon <+> ppr pty $$
                                          pprCtLoc loc)
        ; return (CtWanted { ctev_pred = pty, ctev_dest = EvVarDest new_ev
-                          , ctev_nosh = WDeriv
+                          , ctev_nosh = si
                           , ctev_loc = loc })}
 
 newWantedEvVar :: CtLoc -> TcPredType -> TcS MaybeNew
+newWantedEvVar = newWantedEvVar_SI WDeriv
+
+newWantedEvVar_SI :: ShadowInfo -> CtLoc -> TcPredType -> TcS MaybeNew
 -- For anything except ClassPred, this is the same as newWantedEvVarNC
-newWantedEvVar loc pty
+newWantedEvVar_SI si loc pty
   = do { mb_ct <- lookupInInerts loc pty
        ; case mb_ct of
             Just ctev
               | not (isDerived ctev)
               -> do { traceTcS "newWantedEvVar/cache hit" $ ppr ctev
                     ; return $ Cached (ctEvExpr ctev) }
-            _ -> do { ctev <- newWantedEvVarNC loc pty
+            _ -> do { ctev <- newWantedEvVarNC_SI si loc pty
                     ; return (Fresh ctev) } }
 
--- deals with both equalities and non equalities. Tries to look
--- up non-equalities in the cache
 newWanted :: CtLoc -> PredType -> TcS MaybeNew
-newWanted loc pty
+-- Deals with both equalities and non equalities. Tries to look
+-- up non-equalities in the cache
+newWanted = newWanted_SI WDeriv
+
+newWanted_SI :: ShadowInfo -> CtLoc -> PredType -> TcS MaybeNew
+newWanted_SI si loc pty
   | Just (role, ty1, ty2) <- getEqPredTys_maybe pty
-  = Fresh . fst <$> newWantedEq loc role ty1 ty2
+  = Fresh . fst <$> newWantedEq_SI si loc role ty1 ty2
   | otherwise
-  = newWantedEvVar loc pty
+  = newWantedEvVar_SI si loc pty
 
 -- deals with both equalities and non equalities. Doesn't do any cache lookups.
 newWantedNC :: CtLoc -> PredType -> TcS CtEvidence