Prevent recursive Coercible dictionaries

4 files changed, 46 insertions, 11 deletions

diff --git a/compiler/typecheck/TcErrors.lhs b/compiler/typecheck/TcErrors.lhs
index 018483bb82..3ccf456cf6 100644
--- a/compiler/typecheck/TcErrors.lhs
+++ b/compiler/typecheck/TcErrors.lhs
@@ -1168,9 +1168,6 @@ mk_dict_err ctxt (ct, (matches, unifiers, safe_haskell))
         all (null . lookupGRE_Name rdr_env) (map dataConName (tyConDataCons tc))
 
     coercible_msg_for_tycon rdr_env tc
-        | isRecursiveTyCon tc
-        = Just $ nest 2 $ hsep [ ptext $ sLit "because", quotes (ppr tc)
-                               , ptext $ sLit "is a recursive type constuctor" ]
         | isNewTyCon tc
         = tyConAbstractMsg rdr_env tc empty
         | otherwise
diff --git a/compiler/typecheck/TcInteract.lhs b/compiler/typecheck/TcInteract.lhs
index 685eeb462a..5b35717f05 100644
--- a/compiler/typecheck/TcInteract.lhs
+++ b/compiler/typecheck/TcInteract.lhs
@@ -1443,6 +1443,7 @@ doTopReactDict inerts fl cls xis
   = try_fundeps_and_return
 
   | Just ev <- lookupSolvedDict inerts pred   -- Cached
+  , ctEvCheckDepth (ctLocDepth (ctev_loc fl)) ev
   = do { setEvBind dict_id (ctEvTerm ev);
        ; return $ SomeTopInt { tir_rule = "Dict/Top (cached)"
                              , tir_new_item = Stop } }
@@ -1842,7 +1843,7 @@ matchClassInst _ clas [ ty ] _
 
 matchClassInst _ clas [ _k, ty1, ty2 ] loc
   | clas == coercibleClass =  do
-      traceTcS "matchClassInst for" $ ppr clas <+> ppr ty1 <+> ppr ty2
+      traceTcS "matchClassInst for" $ ppr clas <+> ppr ty1 <+> ppr ty2 <+> text "at depth" <+> ppr (ctLocDepth loc)
       rdr_env <- getGlobalRdrEnvTcS
       safeMode <- safeLanguageOn `fmap` getDynFlags
       ev <- getCoercibleInst safeMode rdr_env loc ty1 ty2
@@ -1957,7 +1958,6 @@ getCoercibleInst safeMode rdr_env loc ty1 ty2
 
   | Just (tc,tyArgs) <- splitTyConApp_maybe ty1,
     Just (_, _, _) <- unwrapNewTyCon_maybe tc,
-    not (isRecursiveTyCon tc),
     newTyConEtadArity tc <= length tyArgs,
     dataConsInScope rdr_env tc -- Do noot look at all tyConsOfTyCon
   = do markDataConsAsUsed rdr_env tc
@@ -1968,7 +1968,6 @@ getCoercibleInst safeMode rdr_env loc ty1 ty2
 
   | Just (tc,tyArgs) <- splitTyConApp_maybe ty2,
     Just (_, _, _) <- unwrapNewTyCon_maybe tc,
-    not (isRecursiveTyCon tc),
     newTyConEtadArity tc <= length tyArgs,
     dataConsInScope rdr_env tc -- Do noot look at all tyConsOfTyCon
   = do markDataConsAsUsed rdr_env tc
@@ -2005,7 +2004,8 @@ markDataConsAsUsed rdr_env tc = addUsedRdrNamesTcS
 requestCoercible :: CtLoc -> TcType -> TcType -> TcS MaybeNew
 requestCoercible loc ty1 ty2 =
     ASSERT2( typeKind ty1 `tcEqKind` typeKind ty2, ppr ty1 <+> ppr ty2)
-    newWantedEvVar loc (coercibleClass `mkClassPred` [typeKind ty1, ty1, ty2])
+    newWantedEvVarNonrec loc' (coercibleClass `mkClassPred` [typeKind ty1, ty1, ty2])
+  where loc' = bumpCtLocDepth CountConstraints loc
 
 \end{code}
 
@@ -2039,7 +2039,6 @@ are present:
  3. instance Coercible r b => Coercible (NT t1 t2 ...) b
     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 ...
      * the data constructors of NT are in scope.
 
diff --git a/compiler/typecheck/TcRnTypes.lhs b/compiler/typecheck/TcRnTypes.lhs
index b00d15c7df..57112d35ff 100644
--- a/compiler/typecheck/TcRnTypes.lhs
+++ b/compiler/typecheck/TcRnTypes.lhs
@@ -50,7 +50,7 @@ module TcRnTypes(
         isGivenCt, isHoleCt,
         ctEvidence, ctLoc, ctPred,
         mkNonCanonical, mkNonCanonicalCt,
-        ctEvPred, ctEvTerm, ctEvId,
+        ctEvPred, ctEvTerm, ctEvId, ctEvCheckDepth,
 
         WantedConstraints(..), insolubleWC, emptyWC, isEmptyWC,
         andWC, unionsWC, addFlats, addImplics, mkFlatWC, addInsols,
@@ -1396,7 +1396,6 @@ data CtEvidence
     -- rewrite anything other than a derived (there's no evidence!)
     -- but if we do manage to solve it may help in solving other goals.
 
-
 ctEvPred :: CtEvidence -> TcPredType
 -- The predicate of a flavor
 ctEvPred = ctev_pred
@@ -1407,6 +1406,12 @@ ctEvTerm (CtWanted  { ctev_evar = ev }) = EvId ev
 ctEvTerm ctev@(CtDerived {}) = pprPanic "ctEvTerm: derived constraint cannot have id"
                                       (ppr ctev)
 
+-- | Checks whether the evidence can be used to solve a goal with the given minimum depth
+ctEvCheckDepth :: SubGoalDepth -> CtEvidence -> Bool
+ctEvCheckDepth _      (CtGiven {})   = True -- Given evidence has infinite depth
+ctEvCheckDepth min ev@(CtWanted {})  = min <= ctLocDepth (ctev_loc ev)
+ctEvCheckDepth _   ev@(CtDerived {}) = pprPanic "ctEvCheckDepth: cannot consider derived evidence" (ppr ev)
+
 ctEvId :: CtEvidence -> TcId
 ctEvId (CtWanted  { ctev_evar = ev }) = ev
 ctEvId ctev = pprPanic "ctEvId:" (ppr ctev)
@@ -1554,6 +1559,27 @@ subGoalDepthExceeded (SubGoalDepth mc mf) (SubGoalDepth c f)
         | otherwise = Nothing
 \end{code}
 
+Note [Preventing recursive dictionaries]
+
+We have some classes where it is not very useful to build recursive
+dictionaries (Coercible, at the moment). So we need the constraint solver to
+prevent that. We conservativey ensure this property using the subgoal depth of
+the constraints: When solving a Coercible constraint at depth d, we do not
+consider evicence from a depth <= d as suitable.
+
+Therefore we need to record the minimum depth allowed to solve a CtWanted. This
+is done in the SubGoalDepth field of CtWanted. Most code now uses mkCtWanted,
+which initializes it to initialSubGoalDepth (i.e. 0); but when requesting a
+Coercible instance (requestCoercible in TcInteract), we bump the current depth
+by one and use that.
+
+There are two spots where wanted contraints attempted to be solved using
+existing constraints; doTopReactDict in TcInteract (in the general solver) and
+newWantedEvVarNonrec (only used by requestCoercible) in TcSMonad. Both use
+ctEvCheckDepth to make the check. That function ensures that a Given constraint
+can always be used to solve a goal (i.e. they are at depth infinity, for our
+purposes)
+
 
 %************************************************************************
 %*                                                                      *
diff --git a/compiler/typecheck/TcSMonad.lhs b/compiler/typecheck/TcSMonad.lhs
index ca95914306..3adb15855e 100644
--- a/compiler/typecheck/TcSMonad.lhs
+++ b/compiler/typecheck/TcSMonad.lhs
@@ -43,7 +43,7 @@ module TcSMonad (
 
     xCtFlavor,        -- Transform a CtEvidence during a step
     rewriteCtFlavor,  -- Specialized version of xCtFlavor for coercions
-    newWantedEvVar, newWantedEvVarNC, instDFunConstraints,
+    newWantedEvVar, newWantedEvVarNC, newWantedEvVarNonrec, instDFunConstraints,
     newDerived,
 
        -- Creation of evidence variables
@@ -1549,6 +1549,19 @@ newWantedEvVarNC loc pty
   = do { new_ev <- wrapTcS $ TcM.newEvVar pty
        ; return (CtWanted { ctev_pred = pty, ctev_evar = new_ev, ctev_loc = loc })}
 
+-- | Variant of newGivenEvVar that has a lower bound on the depth of the result
+--   (see Note [Preventing recursive dictionaries])
+newWantedEvVarNonrec :: CtLoc -> TcPredType -> TcS MaybeNew
+newWantedEvVarNonrec loc pty
+  = do { mb_ct <- lookupInInerts pty
+       ; case mb_ct of
+            Just ctev | not (isDerived ctev) && ctEvCheckDepth (ctLocDepth loc) ctev
+                      -> do { traceTcS "newWantedEvVarNonrec/cache hit" $ ppr ctev
+                            ; return (Cached (ctEvTerm ctev)) }
+            _ -> do { ctev <- newWantedEvVarNC loc pty
+                    ; traceTcS "newWantedEvVarNonrec/cache miss" $ ppr ctev
+                    ; return (Fresh ctev) } }
+
 newWantedEvVar :: CtLoc -> TcPredType -> TcS MaybeNew
 newWantedEvVar loc pty
   = do { mb_ct <- lookupInInerts pty