Do not add a 'solved dict' for quantified constraintswip/T17267

GHC has a wonderful-but-delicate mechanism for building recursive
dictionaries by adding a goal to the "solved dictionaries" before
solving the sub-goals.  See Note [Solved dictionaries] in TcSMonad

Ticket #17267 showed that if you use this mechanism for local
/quantified/ constraints you can get a loop -- or even unsafe
coerce.   This patch fixes the bug.

Specifically

* Make TcSMonad.addSolvedDict be conditional on using a
  /top level/ instance, not a quantified one.

* Moreover, we /also/ don't want to add a solved dict
  for equalities (a~b).

* Add lots more comments to Note [Solved dictionaries]
  to explain the above cryptic stuff.

* Extend InstanceWhat to identify those strange built-in
  equality instances.

A couple of other things along the way

* Delete the unused Type.isIPPred_maybe.

* Stop making addSolvedDict conditional on not being an
  impolicit parameter.  This comes from way back. But
  it's irrelevant now because IP dicts are never solved
  via an instance.

16 files changed, 305 insertions, 42 deletions

diff --git a/compiler/typecheck/ClsInst.hs b/compiler/typecheck/ClsInst.hs
index 5e3501deda..ee1971345b 100644
--- a/compiler/typecheck/ClsInst.hs
+++ b/compiler/typecheck/ClsInst.hs
@@ -3,7 +3,7 @@
 module ClsInst (
      matchGlobalInst,
      ClsInstResult(..),
-     InstanceWhat(..), safeOverlap,
+     InstanceWhat(..), safeOverlap, instanceReturnsDictCon,
      AssocInstInfo(..), isNotAssociated
   ) where
 
@@ -31,7 +31,7 @@ import Id
 import Type
 import MkCore ( mkStringExprFS, mkNaturalExpr )
 
-import Name   ( Name )
+import Name   ( Name, pprDefinedAt )
 import VarEnv ( VarEnv )
 import DataCon
 import TyCon
@@ -91,6 +91,8 @@ data ClsInstResult
 
 data InstanceWhat
   = BuiltinInstance
+  | BuiltinEqInstance   -- A built-in "equality instance"; see the
+                        -- TcSMonad Note [Solved dictionaries]
   | LocalInstance
   | TopLevInstance { iw_dfun_id   :: DFunId
                    , iw_safe_over :: SafeOverlapping }
@@ -103,15 +105,24 @@ instance Outputable ClsInstResult where
     = text "OneInst" <+> vcat [ppr ev, ppr what]
 
 instance Outputable InstanceWhat where
-  ppr BuiltinInstance = text "built-in instance"
-  ppr LocalInstance   = text "locally-quantified instance"
-  ppr (TopLevInstance { iw_safe_over = so })
-     = text "top-level instance" <+> (text $ if so then "[safe]" else "[unsafe]")
+  ppr BuiltinInstance   = text "a built-in instance"
+  ppr BuiltinEqInstance = text "a built-in equality instance"
+  ppr LocalInstance     = text "a locally-quantified instance"
+  ppr (TopLevInstance { iw_dfun_id = dfun })
+      = hang (text "instance" <+> pprSigmaType (idType dfun))
+           2 (text "--" <+> pprDefinedAt (idName dfun))
 
 safeOverlap :: InstanceWhat -> Bool
 safeOverlap (TopLevInstance { iw_safe_over = so }) = so
 safeOverlap _                                      = True
 
+instanceReturnsDictCon :: InstanceWhat -> Bool
+-- See Note [Solved dictionaries] in TcSMonad
+instanceReturnsDictCon (TopLevInstance {}) = True
+instanceReturnsDictCon BuiltinInstance     = True
+instanceReturnsDictCon BuiltinEqInstance   = False
+instanceReturnsDictCon LocalInstance       = False
+
 matchGlobalInst :: DynFlags
                 -> Bool      -- True <=> caller is the short-cut solver
                              -- See Note [Shortcut solving: overlap]
@@ -561,14 +572,14 @@ matchHeteroEquality :: [Type] -> TcM ClsInstResult
 matchHeteroEquality args
   = return (OneInst { cir_new_theta = [ mkTyConApp eqPrimTyCon args ]
                     , cir_mk_ev     = evDataConApp heqDataCon args
-                    , cir_what      = BuiltinInstance })
+                    , cir_what      = BuiltinEqInstance })
 
 matchHomoEquality :: [Type] -> TcM ClsInstResult
 -- Solves (t1 ~ t2)
 matchHomoEquality args@[k,t1,t2]
   = return (OneInst { cir_new_theta = [ mkTyConApp eqPrimTyCon [k,k,t1,t2] ]
                     , cir_mk_ev     = evDataConApp eqDataCon args
-                    , cir_what      = BuiltinInstance })
+                    , cir_what      = BuiltinEqInstance })
 matchHomoEquality args = pprPanic "matchHomoEquality" (ppr args)
 
 -- See also Note [The equality types story] in TysPrim
@@ -576,7 +587,7 @@ matchCoercible :: [Type] -> TcM ClsInstResult
 matchCoercible args@[k, t1, t2]
   = return (OneInst { cir_new_theta = [ mkTyConApp eqReprPrimTyCon args' ]
                     , cir_mk_ev     = evDataConApp coercibleDataCon args
-                    , cir_what      = BuiltinInstance })
+                    , cir_what      = BuiltinEqInstance })
   where
     args' = [k, k, t1, t2]
 matchCoercible args = pprPanic "matchLiftedCoercible" (ppr args)
diff --git a/compiler/typecheck/TcInteract.hs b/compiler/typecheck/TcInteract.hs
index e946d04a23..9122a04436 100644
--- a/compiler/typecheck/TcInteract.hs
+++ b/compiler/typecheck/TcInteract.hs
@@ -2252,9 +2252,8 @@ doTopReactDict inerts work_item@(CDictCan { cc_ev = ev, cc_class = cls
         ; lkup_res <- matchClassInst dflags inerts cls xis dict_loc
         ; case lkup_res of
                OneInst { cir_what = what }
-                  -> do { unless (safeOverlap what) $
-                          insertSafeOverlapFailureTcS work_item
-                        ; when (isWanted ev) $ addSolvedDict ev cls xis
+                  -> do { insertSafeOverlapFailureTcS what work_item
+                        ; addSolvedDict what ev cls xis
                         ; chooseInstance work_item lkup_res }
                _  ->  -- NoInstance or NotSure
                      do { when (isImprovable ev) $
diff --git a/compiler/typecheck/TcSMonad.hs b/compiler/typecheck/TcSMonad.hs
index 0d15d26180..bc86f64bcd 100644
--- a/compiler/typecheck/TcSMonad.hs
+++ b/compiler/typecheck/TcSMonad.hs
@@ -139,7 +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 ClsInst( InstanceWhat(..) )
+import ClsInst( InstanceWhat(..), safeOverlap, instanceReturnsDictCon )
 import Kind
 import TcType
 import DynFlags
@@ -483,6 +483,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 +547,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 +557,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
@@ -1834,10 +1891,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 +1904,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) }
diff --git a/compiler/typecheck/TcValidity.hs b/compiler/typecheck/TcValidity.hs
index 307ec6d0c5..7e7712cd9c 100644
--- a/compiler/typecheck/TcValidity.hs
+++ b/compiler/typecheck/TcValidity.hs
@@ -53,7 +53,6 @@ import Name
 import VarEnv
 import VarSet
 import Var         ( VarBndr(..), mkTyVar )
-import Id          ( idType, idName )
 import FV
 import ErrUtils
 import DynFlags
@@ -1270,17 +1269,10 @@ checkSimplifiableClassConstraint env dflags ctxt cls tys
     simplifiable_constraint_warn what
      = vcat [ hang (text "The constraint" <+> quotes (ppr (tidyType env pred))
                     <+> text "matches")
-                 2 (ppr_what what)
+                 2 (ppr what)
             , hang (text "This makes type inference for inner bindings fragile;")
                  2 (text "either use MonoLocalBinds, or simplify it using the instance") ]
 
-    ppr_what BuiltinInstance = text "a built-in instance"
-    ppr_what LocalInstance   = text "a locally-quantified instance"
-    ppr_what (TopLevInstance { iw_dfun_id = dfun })
-      = hang (text "instance" <+> pprSigmaType (idType dfun))
-           2 (text "--" <+> pprDefinedAt (idName dfun))
-
-
 {- Note [Simplifiable given constraints]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 A type signature like
diff --git a/compiler/types/Type.hs b/compiler/types/Type.hs
index f8cd1da078..ed94241c5f 100644
--- a/compiler/types/Type.hs
+++ b/compiler/types/Type.hs
@@ -90,7 +90,7 @@ module Type (
         mkHeteroPrimEqPred, mkHeteroReprPrimEqPred,
         mkClassPred,
         isClassPred, isEqPrimPred, isEqPred, isEqPredClass,
-        isIPPred, isIPPred_maybe, isIPTyCon, isIPClass,
+        isIPPred, isIPTyCon, isIPClass,
         isCTupleClass,
 
         -- Deconstructing predicate types
@@ -1925,13 +1925,6 @@ isIPClass cls = cls `hasKey` ipClassKey
 isCTupleClass :: Class -> Bool
 isCTupleClass cls = isTupleTyCon (classTyCon cls)
 
-isIPPred_maybe :: Type -> Maybe (FastString, Type)
-isIPPred_maybe ty =
-  do (tc,[t1,t2]) <- splitTyConApp_maybe ty
-     guard (isIPTyCon tc)
-     x <- isStrLitTy t1
-     return (x,t2)
-
 {-
 Make PredTypes
 
diff --git a/testsuite/tests/quantified-constraints/T17267.hs b/testsuite/tests/quantified-constraints/T17267.hs
new file mode 100644
index 0000000000..eaad478003
--- /dev/null
+++ b/testsuite/tests/quantified-constraints/T17267.hs
@@ -0,0 +1,54 @@
+{-# LANGUAGE QuantifiedConstraints #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+module T17267 where
+
+class a ~ b => Thing a b
+instance a ~ b => Thing a b
+
+unsafeCoerce :: forall a b. a -> b
+unsafeCoerce a = oops a where
+  oops :: (a ~ b => Thing a b) => (Thing a b => r) -> r
+  oops r = r
+
+
+{-
+-- Now rejected
+class C a b where
+  op :: a -> b
+
+uc :: a -> b
+uc = oops where
+  oops :: (C a b => C a b) => a -> b
+  oops x = op x
+-}
+
+{-
+-- Now rejected
+uc :: a -> b
+uc = oops where
+  oops :: (a ~ b => a ~ b) => a -> b
+  oops x = x
+-}
+
+
+{-
+-- Now rejected
+class C a b where
+  op :: a -> b
+
+class C a b => Thing a b
+instance C a b => Thing a b
+
+unsafeCoerce :: forall a b. a -> b
+unsafeCoerce a = oops (op a :: Thing a b => b)
+  where
+    oops :: (C a b => Thing a b) => (Thing a b => x) -> x
+    oops r = r
+-}
+
diff --git a/testsuite/tests/quantified-constraints/T17267.stderr b/testsuite/tests/quantified-constraints/T17267.stderr
new file mode 100644
index 0000000000..79f09fdf98
--- /dev/null
+++ b/testsuite/tests/quantified-constraints/T17267.stderr
@@ -0,0 +1,16 @@
+
+T17267.hs:17:12: error:
+    • Reduction stack overflow; size = 201
+      When simplifying the following type: a ~ b
+      Use -freduction-depth=0 to disable this check
+      (any upper bound you could choose might fail unpredictably with
+       minor updates to GHC, so disabling the check is recommended if
+       you're sure that type checking should terminate)
+    • In the expression: r
+      In an equation for ‘oops’: oops r = r
+      In an equation for ‘unsafeCoerce’:
+          unsafeCoerce a
+            = oops a
+            where
+                oops :: (a ~ b => Thing a b) => (Thing a b => r) -> r
+                oops r = r
diff --git a/testsuite/tests/quantified-constraints/T17267a.hs b/testsuite/tests/quantified-constraints/T17267a.hs
new file mode 100644
index 0000000000..acf75b9355
--- /dev/null
+++ b/testsuite/tests/quantified-constraints/T17267a.hs
@@ -0,0 +1,18 @@
+{-# LANGUAGE QuantifiedConstraints #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+module T17267a where
+
+-- Now rejected
+class C a b where
+  op :: a -> b
+
+uc :: a -> b
+uc = oops where
+  oops :: (C a b => C a b) => a -> b
+  oops x = op x
diff --git a/testsuite/tests/quantified-constraints/T17267a.stderr b/testsuite/tests/quantified-constraints/T17267a.stderr
new file mode 100644
index 0000000000..c57eb1f75c
--- /dev/null
+++ b/testsuite/tests/quantified-constraints/T17267a.stderr
@@ -0,0 +1,16 @@
+
+T17267a.hs:18:12: error:
+    • Reduction stack overflow; size = 201
+      When simplifying the following type: C a b
+      Use -freduction-depth=0 to disable this check
+      (any upper bound you could choose might fail unpredictably with
+       minor updates to GHC, so disabling the check is recommended if
+       you're sure that type checking should terminate)
+    • In the expression: op x
+      In an equation for ‘oops’: oops x = op x
+      In an equation for ‘uc’:
+          uc
+            = oops
+            where
+                oops :: (C a b => C a b) => a -> b
+                oops x = op x
diff --git a/testsuite/tests/quantified-constraints/T17267b.hs b/testsuite/tests/quantified-constraints/T17267b.hs
new file mode 100644
index 0000000000..82285d0265
--- /dev/null
+++ b/testsuite/tests/quantified-constraints/T17267b.hs
@@ -0,0 +1,16 @@
+{-# LANGUAGE QuantifiedConstraints #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+module T17267b where
+
+-- Now rejected
+uc :: a -> b
+uc = oops where
+  oops :: (a ~ b => a ~ b) => a -> b
+  oops x = x
+
diff --git a/testsuite/tests/quantified-constraints/T17267b.stderr b/testsuite/tests/quantified-constraints/T17267b.stderr
new file mode 100644
index 0000000000..8a5eeec908
--- /dev/null
+++ b/testsuite/tests/quantified-constraints/T17267b.stderr
@@ -0,0 +1,16 @@
+
+T17267b.hs:15:12: error:
+    • Reduction stack overflow; size = 201
+      When simplifying the following type: a ~ b
+      Use -freduction-depth=0 to disable this check
+      (any upper bound you could choose might fail unpredictably with
+       minor updates to GHC, so disabling the check is recommended if
+       you're sure that type checking should terminate)
+    • In the expression: x
+      In an equation for ‘oops’: oops x = x
+      In an equation for ‘uc’:
+          uc
+            = oops
+            where
+                oops :: (a ~ b => a ~ b) => a -> b
+                oops x = x
diff --git a/testsuite/tests/quantified-constraints/T17267c.hs b/testsuite/tests/quantified-constraints/T17267c.hs
new file mode 100644
index 0000000000..caa93e8234
--- /dev/null
+++ b/testsuite/tests/quantified-constraints/T17267c.hs
@@ -0,0 +1,23 @@
+{-# LANGUAGE QuantifiedConstraints #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+module T17267c where
+
+-- Now rejected
+class C a b where
+  op :: a -> b
+
+class C a b => Thing a b
+instance C a b => Thing a b
+
+unsafeCoerce :: forall a b. a -> b
+unsafeCoerce a = oops (op a :: Thing a b => b)
+  where
+    oops :: (C a b => Thing a b) => (Thing a b => x) -> x
+    oops r = r
+
diff --git a/testsuite/tests/quantified-constraints/T17267c.stderr b/testsuite/tests/quantified-constraints/T17267c.stderr
new file mode 100644
index 0000000000..d616794abf
--- /dev/null
+++ b/testsuite/tests/quantified-constraints/T17267c.stderr
@@ -0,0 +1,16 @@
+
+T17267c.hs:22:14: error:
+    • Reduction stack overflow; size = 201
+      When simplifying the following type: C a b
+      Use -freduction-depth=0 to disable this check
+      (any upper bound you could choose might fail unpredictably with
+       minor updates to GHC, so disabling the check is recommended if
+       you're sure that type checking should terminate)
+    • In the expression: r
+      In an equation for ‘oops’: oops r = r
+      In an equation for ‘unsafeCoerce’:
+          unsafeCoerce a
+            = oops (op a :: Thing a b => b)
+            where
+                oops :: (C a b => Thing a b) => (Thing a b => x) -> x
+                oops r = r
diff --git a/testsuite/tests/quantified-constraints/T17267d.hs b/testsuite/tests/quantified-constraints/T17267d.hs
new file mode 100644
index 0000000000..0a9666eb03
--- /dev/null
+++ b/testsuite/tests/quantified-constraints/T17267d.hs
@@ -0,0 +1,28 @@
+{-# LANGUAGE QuantifiedConstraints #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE DeriveFunctor #-}
+
+-- The instances below have large demands, though I think they're pretty sane.
+{-# LANGUAGE UndecidableInstances #-}
+
+-- This test uses recursive dictionaries
+-- where we do addSolvedDict before solving sub-goals
+
+module Main where
+
+data Foo f a = Foo (f (Maybe a))
+deriving instance Show (f (Maybe a)) => Show (Foo f a)
+deriving instance Functor f => Functor (Foo f)
+
+data Bar x a = Pure a | Bar (x (Bar x) a)
+-- This Show instance is knarly. Basically we ask @x f@ to preserve Show whenever @f@ preserves Show.
+deriving instance (forall f b. (Show b, forall c. Show c => Show (f c))
+                            => Show (x f b), Show a)
+               => Show (Bar x a)
+deriving instance (forall f. Functor f => Functor (x f))
+               => Functor (Bar x)
+
+-- I should now be able to get Show and Functor for @Bar Foo@.
+-- This will involve mutual recursion between the Show/Functor instances for Foo and Bar.
+main :: IO ()
+main = print $ fmap (<> " there") $ Bar $ Foo $ Pure $ Just "Hello"
diff --git a/testsuite/tests/quantified-constraints/T17267d.stdout b/testsuite/tests/quantified-constraints/T17267d.stdout
new file mode 100644
index 0000000000..09bb77d7e9
--- /dev/null
+++ b/testsuite/tests/quantified-constraints/T17267d.stdout
@@ -0,0 +1 @@
+Bar (Foo (Pure (Just "Hello there")))
diff --git a/testsuite/tests/quantified-constraints/all.T b/testsuite/tests/quantified-constraints/all.T
index da585823b2..7fb728654a 100644
--- a/testsuite/tests/quantified-constraints/all.T
+++ b/testsuite/tests/quantified-constraints/all.T
@@ -21,3 +21,8 @@ test('T15359a', normal, compile, [''])
 test('T15625', normal, compile, [''])
 test('T15625a', normal, compile, [''])
 test('T15918', normal, compile_fail, [''])
+test('T17267', normal, compile_fail, [''])
+test('T17267a', normal, compile_fail, [''])
+test('T17267b', normal, compile_fail, [''])
+test('T17267c', normal, compile_fail, [''])
+test('T17267d', normal, compile_and_run, [''])