Get rid of some stuttering in comments and docs
[ghc.git] / compiler / typecheck / TcCanonical.hs
index 7b25925..1785b8b 100644 (file)
@@ -4,11 +4,14 @@ module TcCanonical(
      canonicalize,
      unifyDerived,
      makeSuperClasses, maybeSym,
-     StopOrContinue(..), stopWith, continueWith
+     StopOrContinue(..), stopWith, continueWith,
+     solveCallStack    -- For TcSimplify
   ) where
 
 #include "HsVersions.h"
 
+import GhcPrelude
+
 import TcRnTypes
 import TcUnify( swapOverTyVars, metaTyVarUpdateOK )
 import TcType
@@ -28,6 +31,7 @@ import Outputable
 import DynFlags( DynFlags )
 import NameSet
 import RdrName
+import HsTypes( HsIPName(..) )
 
 import Pair
 import Util
@@ -74,10 +78,18 @@ last time through, so we can skip the classification step.
 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
 canonicalize :: Ct -> TcS (StopOrContinue Ct)
-canonicalize ct@(CNonCanonical { cc_ev = ev })
-  = do { traceTcS "canonicalize (non-canonical)" (ppr ct)
-       ; {-# SCC "canEvVar" #-}
-         canEvNC ev }
+canonicalize (CNonCanonical { cc_ev = ev })
+  = {-# SCC "canNC" #-}
+    case classifyPredType (ctEvPred ev) of
+      ClassPred cls tys     -> do traceTcS "canEvNC:cls" (ppr cls <+> ppr tys)
+                                  canClassNC ev cls tys
+      EqPred eq_rel ty1 ty2 -> do traceTcS "canEvNC:eq" (ppr ty1 $$ ppr ty2)
+                                  canEqNC    ev eq_rel ty1 ty2
+      IrredPred {}          -> do traceTcS "canEvNC:irred" (ppr (ctEvPred ev))
+                                  canIrred ev
+
+canonicalize (CIrredCan { cc_ev = ev })
+  = canIrred ev
 
 canonicalize (CDictCan { cc_ev = ev, cc_class  = cls
                        , cc_tyargs = xis, cc_pend_sc = pend_sc })
@@ -100,21 +112,9 @@ canonicalize (CFunEqCan { cc_ev = ev
   = {-# SCC "canEqLeafFunEq" #-}
     canCFunEqCan ev fn xis1 fsk
 
-canonicalize (CIrredEvCan { cc_ev = ev })
-  = canIrred ev
 canonicalize (CHoleCan { cc_ev = ev, cc_hole = hole })
   = canHole ev hole
 
-canEvNC :: CtEvidence -> TcS (StopOrContinue Ct)
--- Called only for non-canonical EvVars
-canEvNC ev
-  = case classifyPredType (ctEvPred ev) of
-      ClassPred cls tys     -> do traceTcS "canEvNC:cls" (ppr cls <+> ppr tys)
-                                  canClassNC ev cls tys
-      EqPred eq_rel ty1 ty2 -> do traceTcS "canEvNC:eq" (ppr ty1 $$ ppr ty2)
-                                  canEqNC    ev eq_rel ty1 ty2
-      IrredPred {}          -> do traceTcS "canEvNC:irred" (ppr (ctEvPred ev))
-                                  canIrred   ev
 {-
 ************************************************************************
 *                                                                      *
@@ -132,10 +132,47 @@ canClassNC ev cls tys
   = do { sc_cts <- mkStrictSuperClasses ev cls tys
        ; emitWork sc_cts
        ; canClass ev cls tys False }
+
+  | isWanted ev
+  , Just ip_name <- isCallStackPred cls tys
+  , OccurrenceOf func <- ctLocOrigin loc
+  -- 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] in TcEvidence
+  -- and Note [Solving CallStack constraints] in TcSMonad
+  = do { -- 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]
+
+       ; new_ev <- newWantedEvVarNC new_loc pred
+
+         -- Then we solve the wanted by pushing the call-site
+         -- onto the newly emitted CallStack
+       ; let ev_cs = EvCsPushCall func (ctLocSpan loc) (ctEvTerm new_ev)
+       ; solveCallStack ev ev_cs
+
+       ; canClass new_ev cls tys False }
+
   | otherwise
   = canClass ev cls tys (has_scs cls)
+
   where
     has_scs cls = not (null (classSCTheta cls))
+    loc  = ctEvLoc ev
+    pred = ctEvPred ev
+
+solveCallStack :: CtEvidence -> EvCallStack -> TcS ()
+-- Also called from TcSimplify when defaulting call stacks
+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
 
 canClass :: CtEvidence
          -> Class -> [Type]
@@ -162,7 +199,7 @@ canClass ev cls tys pend_sc
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 We need to add superclass constraints for two reasons:
 
-* For givens [G], they give us a route to to proof.  E.g.
+* For givens [G], they give us a route to proof.  E.g.
     f :: Ord a => a -> Bool
     f x = x == x
   We get a Wanted (Eq a), which can only be solved from the superclass
@@ -294,7 +331,7 @@ Examples of how adding superclasses can help:
     Follow the superclass rules to add
          [G] F a ~ b
          [D] F a ~ beta
-    Now we we get [D] beta ~ b, and can solve that.
+    Now we get [D] beta ~ b, and can solve that.
 
     -- Example (tcfail138)
       class L a b | a -> b
@@ -449,25 +486,35 @@ mk_strict_superclasses rec_clss ev cls tys
 
 canIrred :: CtEvidence -> TcS (StopOrContinue Ct)
 -- Precondition: ty not a tuple and no other evidence form
-canIrred old_ev
-  = do { let old_ty = ctEvPred old_ev
-       ; traceTcS "can_pred" (text "IrredPred = " <+> ppr old_ty)
-       ; (xi,co) <- flatten FM_FlattenAll old_ev old_ty -- co :: xi ~ old_ty
-       ; rewriteEvidence old_ev xi co `andWhenContinue` \ new_ev ->
+canIrred ev
+  | EqPred eq_rel ty1 ty2 <- classifyPredType pred
+  = -- For insolubles (all of which are equalities, do /not/ flatten the arguments
+    -- In Trac #14350 doing so led entire-unnecessary and ridiculously large
+    -- type function expansion.  Instead, canEqNC just applies
+    -- the substitution to the predicate, and may do decomposition;
+    --    e.g. a ~ [a], where [G] a ~ [Int], can decompose
+    canEqNC ev eq_rel ty1 ty2
+
+  | otherwise
+  = do { traceTcS "can_pred" (text "IrredPred = " <+> ppr pred)
+       ; (xi,co) <- flatten FM_FlattenAll ev pred -- co :: xi ~ pred
+       ; rewriteEvidence ev xi co `andWhenContinue` \ new_ev ->
     do { -- Re-classify, in case flattening has improved its shape
        ; case classifyPredType (ctEvPred new_ev) of
            ClassPred cls tys     -> canClassNC new_ev cls tys
            EqPred eq_rel ty1 ty2 -> canEqNC new_ev eq_rel ty1 ty2
            _                     -> continueWith $
-                                    CIrredEvCan { cc_ev = new_ev } } }
+                                    mkIrredCt new_ev } }
+  where
+    pred = ctEvPred ev
 
 canHole :: CtEvidence -> Hole -> TcS (StopOrContinue Ct)
 canHole ev hole
   = do { let ty = ctEvPred ev
        ; (xi,co) <- flatten FM_SubstOnly ev ty -- co :: xi ~ ty
        ; rewriteEvidence ev xi co `andWhenContinue` \ new_ev ->
-    do { emitInsoluble (CHoleCan { cc_ev = new_ev
-                                 , cc_hole = hole })
+    do { updInertIrreds (`snocCts` (CHoleCan { cc_ev = new_ev
+                                             , cc_hole = hole }))
        ; stopWith new_ev "Emit insoluble hole" } }
 
 {-
@@ -782,7 +829,8 @@ zonk_eq_types = go
             -> do { cts <- readTcRef ref
                   ; case cts of
                       Flexi        -> give_up
-                      Indirect ty' -> unSwap swapped go ty' ty }
+                      Indirect ty' -> do { trace_indirect tv ty'
+                                         ; unSwap swapped go ty' ty } }
           _ -> give_up
       where
         give_up = return $ Left $ unSwap swapped Pair (mkTyVarTy tv) ty
@@ -795,12 +843,17 @@ zonk_eq_types = go
                           then go ty1' ty2'
                           else return $ Left (Pair (TyVarTy tv1) (TyVarTy tv2)) }
 
+    trace_indirect tv ty
+       = traceTcS "Following filled tyvar (zonk_eq_types)"
+                  (ppr tv <+> equals <+> ppr ty)
+
     quick_zonk tv = case tcTyVarDetails tv of
       MetaTv { mtv_ref = ref }
         -> do { cts <- readTcRef ref
               ; case cts of
                   Flexi        -> return (TyVarTy tv, False)
-                  Indirect ty' -> return (ty', True) }
+                  Indirect ty' -> do { trace_indirect tv ty'
+                                     ; return (ty', True) } }
       _ -> return (TyVarTy tv, False)
 
       -- This happens for type families, too. But recall that failure
@@ -870,7 +923,7 @@ Here's another place where this reflexivity check is key:
 Consider trying to prove (f a) ~R (f a). The AppTys in there can't
 be decomposed, because representational equality isn't congruent with respect
 to AppTy. So, when canonicalising the equality above, we get stuck and
-would normally produce a CIrredEvCan. However, we really do want to
+would normally produce a CIrredCan. However, we really do want to
 be able to solve (f a) ~R (f a). So, in the representational case only,
 we do a reflexivity check.
 
@@ -917,7 +970,7 @@ can_eq_app :: CtEvidence       -- :: s1 t1 ~r s2 t2
 -- See Note [Decomposing equality], note {4}
 can_eq_app ev ReprEq _ _ _ _
   = do { traceTcS "failing to decompose representational AppTy equality" (ppr ev)
-       ; continueWith (CIrredEvCan { cc_ev = ev }) }
+       ; continueWith (mkIrredCt ev) }
           -- no need to call canEqFailure, because that flattens, and the
           -- types involved here are already flat
 
@@ -990,7 +1043,7 @@ canTyConApp ev eq_rel tc1 tys1 tc2 tys2
   -- See Note [Skolem abstract data] (at tyConSkolem)
   | tyConSkolem tc1 || tyConSkolem tc2
   = do { traceTcS "canTyConApp: skolem abstract" (ppr tc1 $$ ppr tc2)
-       ; continueWith (CIrredEvCan { cc_ev = ev }) }
+       ; continueWith (mkIrredCt ev) }
 
   -- Fail straight away for better error messages
   -- See Note [Use canEqFailure in canDecomposableTyConApp]
@@ -1252,7 +1305,7 @@ canEqFailure ev ReprEq ty1 ty2
          vcat [ ppr ev, ppr ty1, ppr ty2, ppr xi1, ppr xi2 ]
        ; rewriteEqEvidence ev NotSwapped xi1 xi2 co1 co2
          `andWhenContinue` \ new_ev ->
-         continueWith (CIrredEvCan { cc_ev = new_ev }) }
+         continueWith (mkIrredCt new_ev) }
 
 -- | Call when canonicalizing an equality fails with utterly no hope.
 canEqHardFailure :: CtEvidence
@@ -1263,8 +1316,7 @@ canEqHardFailure ev ty1 ty2
        ; (s2, co2) <- flatten FM_SubstOnly ev ty2
        ; rewriteEqEvidence ev NotSwapped s1 s2 co1 co2
          `andWhenContinue` \ new_ev ->
-    do { emitInsoluble (mkNonCanonical new_ev)
-       ; stopWith new_ev "Definitely not equal" }}
+         continueWith (mkInsolubleCt new_ev) }
 
 {-
 Note [Decomposing TyConApps]
@@ -1440,7 +1492,7 @@ canEqTyVar ev eq_rel swapped tv1 co1 ps_ty1 xi2 ps_xi2
              -- kind_ev :: (k1 :: *) ~ (k2 :: *)
        ; traceTcS "Hetero equality gives rise to derived kind equality" $
            ppr ev
-       ; continueWith (CIrredEvCan { cc_ev = ev }) }
+       ; continueWith (mkIrredCt ev) }
 
   where
     lhs = mkTyVarTy tv1 `mkCastTy` co1
@@ -1508,21 +1560,18 @@ canEqTyVar2 dflags ev eq_rel swapped tv1 co1 orhs
        ; rewriteEqEvidence ev swapped nlhs nrhs rewrite_co1 rewrite_co2
          `andWhenContinue` \ new_ev ->
          if isInsolubleOccursCheck eq_rel tv1 nrhs
-         then do { emitInsoluble (mkNonCanonical new_ev)
+         then continueWith (mkInsolubleCt new_ev)
              -- If we have a ~ [a], it is not canonical, and in particular
              -- we don't want to rewrite existing inerts with it, otherwise
              -- we'd risk divergence in the constraint solver
-                 ; stopWith new_ev "Occurs check" }
 
+         else continueWith (mkIrredCt new_ev) }
              -- A representational equality with an occurs-check problem isn't
              -- insoluble! For example:
              --   a ~R b a
              -- We might learn that b is the newtype Id.
              -- But, the occurs-check certainly prevents the equality from being
              -- canonical, and we might loop if we were to use it in rewriting.
-         else do { traceTcS "Possibly-soluble occurs check"
-                           (ppr nlhs $$ ppr nrhs)
-                 ; continueWith (CIrredEvCan { cc_ev = new_ev }) } }
   where
     role = eqRelRole eq_rel
 
@@ -1574,7 +1623,7 @@ canEqTyVarTyVar, are these
 
 Note [Avoid unnecessary swaps]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-If we swap without actually improving matters, we can get an infnite loop.
+If we swap without actually improving matters, we can get an infinite loop.
 Consider
     work item:  a ~ b
    inert item:  b ~ c
@@ -1802,7 +1851,7 @@ rewriteEvidence old_ev new_pred co
   | isTcReflCo co -- See Note [Rewriting with Refl]
   = continueWith (old_ev { ctev_pred = new_pred })
 
-rewriteEvidence ev@(CtGiven { ctev_evar = old_evar , ctev_loc = loc }) new_pred co
+rewriteEvidence ev@(CtGiven { ctev_evar = old_evar, ctev_loc = loc }) new_pred co
   = do { new_ev <- newGivenEvVar loc (new_pred, new_tm)
        ; continueWith new_ev }
   where