Fix solving of implicit parameter constraints
[ghc.git] / compiler / typecheck / TcInteract.hs
index 69e84a4..1298932 100644 (file)
@@ -3,15 +3,14 @@
 module TcInteract (
      solveSimpleGivens,   -- Solves [Ct]
      solveSimpleWanteds,  -- Solves Cts
-
-     solveCallStack,      -- for use in TcSimplify
   ) where
 
 #include "HsVersions.h"
 
+import GhcPrelude
+
 import BasicTypes ( SwapFlag(..), isSwapped,
                     infinity, IntWithInf, intGtLimit )
-import HsTypes ( HsIPName(..) )
 import TcCanonical
 import TcFlatten
 import TcUnify( canSolveByUnification )
@@ -28,9 +27,10 @@ import TcType
 import Name
 import RdrName ( lookupGRE_FieldLabel )
 import PrelNames ( knownNatClassName, knownSymbolClassName,
-                   typeableClassName, coercibleTyConKey,
+                   typeableClassName, typeableClassKey,
+                   coercibleTyConKey,
                    hasFieldClassName,
-                   heqTyConKey, ipClassKey )
+                   heqTyConKey, eqTyConKey, ipClassKey )
 import TysWiredIn ( typeNatKind, typeSymbolKind, heqDataCon,
                     coercibleDataCon, constraintKindTyCon )
 import TysPrim    ( eqPrimTyCon, eqReprPrimTyCon )
@@ -835,59 +835,38 @@ It is important to emphasize that failure means that we don't produce more
 efficient code, NOT that we fail to typecheck at all! This is purely an
 an optimization: exactly the same programs should typecheck with or without this
 procedure.
-
 -}
 
 interactDict :: InertCans -> Ct -> TcS (StopOrContinue Ct)
 interactDict inerts workItem@(CDictCan { cc_ev = ev_w, cc_class = cls, cc_tyargs = tys })
-  | isWanted ev_w
-  , Just ip_name      <- isCallStackPred (ctPred workItem)
-  , OccurrenceOf func <- ctLocOrigin (ctEvLoc ev_w)
-  -- If we're given a CallStack constraint that arose from a function
-  -- call, we need to push the current call-site onto the stack instead
-  -- of solving it directly from a given.
-  -- See Note [Overview of implicit CallStacks]
-  = do { let loc = ctEvLoc ev_w
-
-         -- First we emit a new constraint that will capture the
-         -- given CallStack.
-       ; let new_loc      = setCtLocOrigin loc (IPOccOrigin (HsIPName ip_name))
-                            -- We change the origin to IPOccOrigin so
-                            -- this rule does not fire again.
-                            -- See Note [Overview of implicit CallStacks]
-
-       ; mb_new <- newWantedEvVar new_loc (ctEvPred ev_w)
-       ; emitWorkNC (freshGoals [mb_new])
-
-         -- Then we solve the wanted by pushing the call-site onto the
-         -- newly emitted CallStack.
-       ; let ev_cs = EvCsPushCall func (ctLocSpan loc) (getEvTerm mb_new)
-       ; solveCallStack ev_w ev_cs
-       ; stopWith ev_w "Wanted CallStack IP" }
-  | Just ctev_i <- lookupInertDict inerts cls tys
-  = do
-  { dflags <- getDynFlags
-  -- See Note [Solving from instances when interacting Dicts]
-  ; try_inst_res <- trySolveFromInstance dflags ev_w ctev_i
-  ; case try_inst_res of
-      Just evs -> do
-        { flip mapM_ evs $ \(ev_t, ct_ev, cls, typ) -> do
-          { setWantedEvBind (ctEvId ct_ev) ev_t
-          ; addSolvedDict ct_ev cls typ }
-        ; stopWith ev_w "interactDict/solved from instance" }
-      -- We were unable to solve the [W] constraint from in-scope instances so
-      -- we solve it from the solution in the inerts we just retrieved.
-      Nothing ->  do
-        { (inert_effect, stop_now) <- solveOneFromTheOther ctev_i ev_w
-        ; traceTcS "lookupInertDict" (ppr inert_effect <+> ppr stop_now)
-        ; case inert_effect of
-            IRKeep    -> return ()
-            IRDelete  -> updInertDicts $ \ ds -> delDict ds cls tys
-            IRReplace -> updInertDicts $ \ ds -> addDict ds cls tys workItem
-        ; if stop_now then
-            return $ Stop ev_w (text "Dict equal" <+> parens (ppr inert_effect))
-          else
-            continueWith workItem } }
+  | Just ctev_i <- lookupInertDict inerts (ctEvLoc ev_w) cls tys
+  = -- There is a matching dictionary in the inert set
+    do { -- First to try to solve it /completely/ from
+         -- top level instances
+         -- See Note [Solving from instances when interacting Dicts]
+         dflags <- getDynFlags
+       ; try_inst_res <- trySolveFromInstance dflags ev_w ctev_i
+       ; case try_inst_res of
+           Just evs -> do
+             { flip mapM_ evs $ \(ev_t, ct_ev, cls, typ) -> do
+               { setWantedEvBind (ctEvId ct_ev) ev_t
+               ; addSolvedDict ct_ev cls typ }
+             ; stopWith ev_w "interactDict/solved from instance" }
+
+           -- We were unable to solve the [W] constraint from in-scope instances
+           -- so we solve it from the matching inert we found
+           Nothing ->  do
+             { (inert_effect, stop_now) <- solveOneFromTheOther ctev_i ev_w
+             ; traceTcS "lookupInertDict" (ppr inert_effect <+> ppr stop_now)
+             ; case inert_effect of
+                 IRKeep    -> return ()
+                 IRDelete  -> updInertDicts $ \ ds -> delDict ds cls tys
+                 IRReplace -> updInertDicts $ \ ds -> addDict ds cls tys workItem
+             ; if stop_now then
+                 return $ Stop ev_w (text "Dict equal" <+> parens (ppr inert_effect))
+               else
+                 continueWith workItem } }
+
   | cls `hasKey` ipClassKey
   , isGiven ev_w
   = interactGivenIP inerts workItem
@@ -934,7 +913,7 @@ trySolveFromInstance dflags ev_w ctev_i
     new_wanted_cached :: DictMap CtEvidence -> TcPredType -> MaybeT TcS MaybeNew
     new_wanted_cached cache pty
       | ClassPred cls tys <- classifyPredType pty
-      = lift $ case findDict cache cls tys of
+      = lift $ case findDict cache loc_w cls tys of
           Just ctev -> return $ Cached (ctEvTerm ctev)
           Nothing -> Fresh <$> newWantedNC loc_w pty
       | otherwise = mzero
@@ -1035,7 +1014,6 @@ interactGivenIP inerts workItem@(CDictCan { cc_ev = ev, cc_class = cls
 
 interactGivenIP _ wi = pprPanic "interactGivenIP" (ppr wi)
 
-
 {- Note [Shadowing of Implicit Parameters]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Consider the following example:
@@ -1174,7 +1152,7 @@ improveLocalFunEqs work_ev inerts fam_tc args fsk
     rhs           = lookupFlattenTyVar ieqs fsk
     work_loc      = ctEvLoc work_ev
     work_pred     = ctEvPred work_ev
-    fam_inj_info  = familyTyConInjectivityInfo fam_tc
+    fam_inj_info  = tyConInjectivityInfo fam_tc
 
     --------------------
     improvement_eqns :: [FunDepEqn CtLoc]
@@ -1743,7 +1721,7 @@ improve_top_fun_eqs fam_envs fam_tc args rhs_ty
 
   -- see Note [Type inference for type families with injectivity]
   | isOpenTypeFamilyTyCon fam_tc
-  , Injective injective_args <- familyTyConInjectivityInfo fam_tc
+  , Injective injective_args <- tyConInjectivityInfo fam_tc
   , let fam_insts = lookupFamInstEnvByTyCon fam_envs fam_tc
   = -- it is possible to have several compatible equations in an open type
     -- family but we only want to derive equalities from one such equation.
@@ -1755,7 +1733,7 @@ improve_top_fun_eqs fam_envs fam_tc args rhs_ty
          take 1 improvs }
 
   | Just ax <- isClosedSynFamilyTyConWithAxiom_maybe fam_tc
-  , Injective injective_args <- familyTyConInjectivityInfo fam_tc
+  , Injective injective_args <- tyConInjectivityInfo fam_tc
   = concatMapM (injImproveEqns injective_args) $
     buildImprovementData (fromBranches (co_ax_branches ax))
                          cab_tvs cab_lhs cab_rhs Just
@@ -2073,7 +2051,7 @@ doTopReactDict inerts work_item@(CDictCan { cc_ev = fl, cc_class = cls
   = do { try_fundep_improvement
        ; continueWith work_item }
 
-  | Just ev <- lookupSolvedDict inerts cls xis   -- Cached
+  | Just ev <- lookupSolvedDict inerts dict_loc cls xis   -- Cached
   = do { setEvBindIfWanted fl (ctEvTerm ev)
        ; stopWith fl "Dict/Top (cached)" }
 
@@ -2205,6 +2183,17 @@ match_class_inst dflags clas tys loc
   where
     cls_name = className clas
 
+-- | If a class is "naturally coherent", then we needn't worry at all, in any
+-- way, about overlapping/incoherent instances. Just solve the thing!
+naturallyCoherentClass :: Class -> Bool
+-- See also Note [The equality class story] in TysPrim.
+naturallyCoherentClass cls
+  = isCTupleClass cls ||   -- See "Tuple classes" in Note [Instance and Given overlap]
+    cls `hasKey` heqTyConKey ||
+    cls `hasKey` eqTyConKey ||
+    cls `hasKey` coercibleTyConKey ||
+    cls `hasKey` typeableClassKey
+
 {- Note [Instance and Given overlap]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Example, from the OutsideIn(X) paper:
@@ -2260,6 +2249,15 @@ Other notes:
 
 * Another "live" example is Trac #10195; another is #10177.
 
+* Tuple classes.  For reasons described in TcSMonad
+  Note [Tuples hiding implicit parameters], we may have a constraint
+     [W] (?x::Int, C a)
+  with an exactly-matching Given constraint.  We must decompose this
+  tuple and solve the components separately, otherwise we won't solve
+  it at all!  It is perfectly safe to decompose it, because the "instance"
+  for class tuples is bidirectional: the Given can also be decomposed
+  to provide the pieces.
+
 * We ignore the overlap problem if -XIncoherentInstances is in force:
   see Trac #6002 for a worked-out example where this makes a
   difference.
@@ -2529,14 +2527,6 @@ a TypeRep for them.  For qualified but not polymorphic types, like
    For now we leave it off, until we have a better story for impredicativity.
 -}
 
-solveCallStack :: CtEvidence -> EvCallStack -> TcS ()
-solveCallStack ev ev_cs = do
-  -- We're given ev_cs :: CallStack, but the evidence term should be a
-  -- dictionary, so we have to coerce ev_cs to a dictionary for
-  -- `IP ip CallStack`. See Note [Overview of implicit CallStacks]
-  let ev_tm = mkEvCast (EvCallStack ev_cs) (wrapIP (ctEvPred ev))
-  setWantedEvBind (ctEvId ev) ev_tm
-
 {- ********************************************************************
 *                                                                     *
                    Class lookup for lifted equality