diff --git a/CONTRIBUTORS.md b/CONTRIBUTORS.md
index 1ecc5a4e05..63565a74e8 100644
--- a/CONTRIBUTORS.md
+++ b/CONTRIBUTORS.md
@@ -135,6 +135,7 @@ If you would prefer to use different terms, please use the section below instead
 | [@adnelson](https://github.com/adnelson) | Allen Nelson | [MIT license](http://opensource.org/licenses/MIT) |
 | [@dyerw](https://github.com/dyerw) | Liam Dyer | [MIT license](http://opensource.org/licenses/MIT) |
 | [@marcosh](https://github.com/marcosh) | Marco Perone | [MIT license](http://opensource.org/licenses/MIT) |
+| [@matthew-hilty](https://github.com/matthew-hilty) | Matthew Hilty | [MIT license](http://opensource.org/licenses/MIT) |
 
 ### Contributors using Modified Terms
 
diff --git a/src/Language/PureScript/AST/Declarations.hs b/src/Language/PureScript/AST/Declarations.hs
index 93f8d879e5..bde88f1ae6 100644
--- a/src/Language/PureScript/AST/Declarations.hs
+++ b/src/Language/PureScript/AST/Declarations.hs
@@ -64,6 +64,9 @@ onTypeSearchTypesM :: (Applicative m) => (SourceType -> m SourceType) -> TypeSea
 onTypeSearchTypesM f (TSAfter i r) = TSAfter <$> traverse (traverse f) i <*> traverse (traverse (traverse f)) r
 onTypeSearchTypesM _ (TSBefore env) = pure (TSBefore env)
 
+data DictMemberType = Fn | NonFn
+  deriving (Eq, Ord, Show)
+
 -- | A type of error messages
 data SimpleErrorMessage
   = ModuleNotFound ModuleName
@@ -101,6 +104,8 @@ data SimpleErrorMessage
   | InvalidDoBind
   | InvalidDoLet
   | CycleInDeclaration Ident
+  | CycleInDictDeclaration Ident [(Ident, SourceSpan, DictMemberType)]
+  | MissingEtaExpansion Ident
   | CycleInTypeSynonym (Maybe (ProperName 'TypeName))
   | CycleInTypeClassDeclaration [Qualified (ProperName 'ClassName)]
   | CycleInModules [ModuleName]
@@ -477,6 +482,22 @@ getValueDeclaration :: Declaration -> Maybe (ValueDeclarationData [GuardedExpr])
 getValueDeclaration (ValueDeclaration d) = Just d
 getValueDeclaration _ = Nothing
 
+isDictExpr :: Expr -> Bool
+isDictExpr expr = case stripTypedAndPositioned expr of
+  TypeClassDictionaryConstructorApp _ _ -> True
+  Abs _ expr' -> isDictExpr expr'
+  _ -> False
+
+getDictDeclaration :: Declaration -> Maybe (ValueDeclarationData [GuardedExpr])
+getDictDeclaration (ValueDeclaration d@(ValueDeclarationData _ _ Private _ [MkUnguarded expr]))
+  | isDictExpr expr = Just d
+getDictDeclaration _ = Nothing
+
+stripTypedAndPositioned :: Expr -> Expr
+stripTypedAndPositioned (TypedValue _ e _) = stripTypedAndPositioned e
+stripTypedAndPositioned (PositionedValue _ _ e) = stripTypedAndPositioned e
+stripTypedAndPositioned e = e
+
 pattern ValueDecl :: SourceAnn -> Ident -> NameKind -> [Binder] -> [GuardedExpr] -> Declaration
 pattern ValueDecl sann ident name binders expr
   = ValueDeclaration (ValueDeclarationData sann ident name binders expr)
diff --git a/src/Language/PureScript/AST/Traversals.hs b/src/Language/PureScript/AST/Traversals.hs
index 70543f8621..a78c36da7f 100644
--- a/src/Language/PureScript/AST/Traversals.hs
+++ b/src/Language/PureScript/AST/Traversals.hs
@@ -329,6 +329,34 @@ everythingOnValues (<>.) f g h i j = (f', g', h', i', j')
   k' (ConditionGuard e) = g' e
   k' (PatternGuard b e) = h' b <>. g' e
 
+-- |
+-- A fold for paramorphisms associated with (1) an initial object represented
+-- by the coproduct 'Node'
+-- @
+--   data Node
+--     = A Declaration
+--     | NonLiteral Expr
+--     | Literal Expr
+--     | B Binder
+--     | C CaseAlternative
+--     | D DoNotationElement
+-- @
+-- and (2) the functorial context
+-- > type Context s r = (s, r, r -> r -> r, s -> Node -> (s, r))
+--
+-- Given an initial state, a default output value, a binary action on the
+-- output type, and six independent state-transition transformers (one each for
+-- 'Declaration's, 'Binder's, 'CaseAlternative's, and 'DoNotationElement's; and
+-- two for 'Expr's), determine five corresponding mutually recursive data-
+-- gathering functions that generate "measurements" of type 'r' for values of
+-- any of the constituent types of the coproduct 'Node'.
+--
+-- Two input functions for 'Expr' are required in order to allow distinguishing
+-- of values inside 'Literal' 'Expr's from values independent of literal objects
+-- and arrays. (The function 'immediateLitIdentsAndAllOtherIdents' in module
+-- 'Language.PureScript.Sugar.BindingGroups' is an example of a client for
+-- this feature.)
+--
 everythingWithContextOnValues
   :: forall s r
    . s
@@ -336,6 +364,9 @@ everythingWithContextOnValues
   -> (r -> r -> r)
   -> (s -> Declaration       -> (s, r))
   -> (s -> Expr              -> (s, r))
+  -- ^ Transformer of 'Expr' nodes without 'Literal' ancestors
+  -> (s -> Expr              -> (s, r))
+  -- ^ Transformer of 'Expr' nodes strictly dominated by a 'Literal' 'Expr'
   -> (s -> Binder            -> (s, r))
   -> (s -> CaseAlternative   -> (s, r))
   -> (s -> DoNotationElement -> (s, r))
@@ -344,7 +375,8 @@ everythingWithContextOnValues
      , Binder            -> r
      , CaseAlternative   -> r
      , DoNotationElement -> r)
-everythingWithContextOnValues s0 r0 (<>.) f g h i j = (f'' s0, g'' s0, h'' s0, i'' s0, j'' s0)
+everythingWithContextOnValues s0 r0 (<>.) f g gLit h i j =
+  (f'' s0, g'' s0, h'' s0, i'' s0, j'' s0)
   where
 
   f'' :: s -> Declaration -> r
@@ -362,7 +394,7 @@ everythingWithContextOnValues s0 r0 (<>.) f g h i j = (f'' s0, g'' s0, h'' s0, i
   g'' s v = let (s', r) = g s v in r <>. g' s' v
 
   g' :: s -> Expr -> r
-  g' s (Literal _ l) = lit g'' s l
+  g' s (Literal _ l) = lit gLit'' s l
   g' s (UnaryMinus _ v1) = g'' s v1
   g' s (BinaryNoParens op v1 v2) = g'' s op <>. g'' s v1 <>. g'' s v2
   g' s (Parens v1) = g'' s v1
@@ -382,6 +414,29 @@ everythingWithContextOnValues s0 r0 (<>.) f g h i j = (f'' s0, g'' s0, h'' s0, i
   g' s (PositionedValue _ _ v1) = g'' s v1
   g' _ _ = r0
 
+  gLit'' :: s -> Expr -> r
+  gLit'' s v = let (s', r) = gLit s v in r <>. gLit' s' v
+
+  gLit' :: s -> Expr -> r
+  gLit' s (Literal _ l) = lit gLit'' s l
+  gLit' s (UnaryMinus _ v1) = gLit'' s v1
+  gLit' s (BinaryNoParens op v1 v2) = gLit'' s op <>. gLit'' s v1 <>. gLit'' s v2
+  gLit' s (Parens v1) = gLit'' s v1
+  gLit' s (TypeClassDictionaryConstructorApp _ v1) = gLit'' s v1
+  gLit' s (Accessor _ v1) = gLit'' s v1
+  gLit' s (ObjectUpdate obj vs) = foldl (<>.) (gLit'' s obj) (fmap (gLit'' s . snd) vs)
+  gLit' s (ObjectUpdateNested obj vs) = foldl (<>.) (gLit'' s obj) (fmap (gLit'' s) vs)
+  gLit' s (Abs binder v1) = h'' s binder <>. gLit'' s v1
+  gLit' s (App v1 v2) = gLit'' s v1 <>. gLit'' s v2
+  gLit' s (IfThenElse v1 v2 v3) = gLit'' s v1 <>. gLit'' s v2 <>. gLit'' s v3
+  gLit' s (Case vs alts) = foldl (<>.) (foldl (<>.) r0 (fmap (gLit'' s) vs)) (fmap (i'' s) alts)
+  gLit' s (TypedValue _ v1 _) = gLit'' s v1
+  gLit' s (Let _ ds v1) = foldl (<>.) r0 (fmap (f'' s) ds) <>. gLit'' s v1
+  gLit' s (Do _ es) = foldl (<>.) r0 (fmap (j'' s) es)
+  gLit' s (Ado _ es v1) = foldl (<>.) r0 (fmap (j'' s) es) <>. gLit'' s v1
+  gLit' s (PositionedValue _ _ v1) = gLit'' s v1
+  gLit' _ _ = r0
+
   h'' :: s -> Binder -> r
   h'' s b = let (s', r) = h s b in r <>. h' s' b
 
diff --git a/src/Language/PureScript/Environment.hs b/src/Language/PureScript/Environment.hs
index f6bea0e9dc..4649970aa7 100644
--- a/src/Language/PureScript/Environment.hs
+++ b/src/Language/PureScript/Environment.hs
@@ -359,6 +359,14 @@ isTypeOrApplied :: Type a -> Type b -> Bool
 isTypeOrApplied t1 (TypeApp _ t2 _) = eqType t1 t2
 isTypeOrApplied t1 t2 = eqType t1 t2
 
+isFunctionType :: SourceType -> Bool
+isFunctionType = eqType tyFunction . stripForAllAndTypeApp
+
+stripForAllAndTypeApp :: SourceType -> SourceType
+stripForAllAndTypeApp (ForAll _ _ _ st _) = stripForAllAndTypeApp st
+stripForAllAndTypeApp (TypeApp _ st _) = stripForAllAndTypeApp st
+stripForAllAndTypeApp st = st
+
 -- | Smart constructor for function types
 function :: SourceType -> SourceType -> SourceType
 function t1 t2 = TypeApp nullSourceAnn (TypeApp nullSourceAnn tyFunction t1) t2
diff --git a/src/Language/PureScript/Errors.hs b/src/Language/PureScript/Errors.hs
index cb4f460952..9f7a42f859 100644
--- a/src/Language/PureScript/Errors.hs
+++ b/src/Language/PureScript/Errors.hs
@@ -46,6 +46,9 @@ import qualified Text.Parsec.Error as PE
 import           Text.Parsec.Error (Message(..))
 import qualified Text.PrettyPrint.Boxes as Box
 
+noErrors :: MultipleErrors
+noErrors = MultipleErrors []
+
 newtype ErrorSuggestion = ErrorSuggestion Text
 
 -- | Get the source span for an error
@@ -111,6 +114,8 @@ errorCode em = case unwrapErrorMessage em of
   InvalidDoBind -> "InvalidDoBind"
   InvalidDoLet -> "InvalidDoLet"
   CycleInDeclaration{} -> "CycleInDeclaration"
+  CycleInDictDeclaration{} -> "CycleInDictDeclaration"
+  MissingEtaExpansion{} -> "MissingEtaExpansion"
   CycleInTypeSynonym{} -> "CycleInTypeSynonym"
   CycleInTypeClassDeclaration{} -> "CycleInTypeClassDeclaration"
   CycleInModules{} -> "CycleInModules"
@@ -574,7 +579,47 @@ prettyPrintSingleError (PPEOptions codeColor full level showDocs relPath) e = fl
             , indent $ line $ displaySourceSpan relPath ss
             ]
     renderSimpleErrorMessage (CycleInDeclaration nm) =
-      line $ "The value of " <> markCode (showIdent nm) <> " is undefined here, so this reference is not allowed."
+      line $ "The value of " <> markCode (showIdent nm) <> " is undefined here because of cyclical dependencies, so this reference is not allowed."
+    renderSimpleErrorMessage (CycleInDictDeclaration inst fields) =
+      let label' dmt = if dmt == Fn then "function " else "value "
+          label (i, ss, dmt) =
+            indent' . line $
+              label' dmt <> markCode (showIdent i) <> " at " <> displaySourceSpan relPath ss
+          prelude = line $ "The definition of instance " <> markCode (showIdent inst) <> " is invalid because of cyclical dependencies."
+          addendum =
+            [ line ""
+            , line $ "Note that cycles in the member functions of " <> markCode (showIdent inst) <> " may lead to non-terminating runtime behavior."
+            , line ""
+            , line $ "Consider replacing the functions' circular dependencies with independent terms."
+            , line ""
+            , line $ "If their definitions cannot be rewritten, eta-expansion is necessary to accommodate purescript's non-strict style of evaluation."
+            ]
+          addendum' = if (any (\(_, _, dmt) -> dmt == Fn) fields)
+                         then addendum
+                         else []
+      in case fields of
+        [] -> prelude
+        [field] ->
+          paras $ [ prelude
+                  , line ""
+                  , line $ "In particular, its member"
+                  , label field
+                  , line $ "implicitly references the instance itself."
+                  ] ++ addendum'
+        _ ->
+          paras $ [ prelude
+                  , line ""
+                  , line $ "In particular, its following members implicitly reference the instance itself."
+                  ] ++ map label fields ++ addendum'
+    renderSimpleErrorMessage (MissingEtaExpansion ident) =
+      paras [ line $ "A cycle appears in the definition of function " <> markCode (showIdent ident) <> "."
+            , line ""
+            , line $ "Note that cycles in functions may lead to non-terminating runtime behavior."
+            , line ""
+            , line $ "Consider replacing the circular dependencies in the definition of " <> markCode (showIdent ident) <> " with independent terms."
+            , line ""
+            , line "If the definition cannot be rewritten, eta-expansion is necessary to accommodate purescript's non-strict style of evaluation."
+            ]
     renderSimpleErrorMessage (CycleInModules mns) =
       case mns of
         [mn] ->
@@ -1438,6 +1483,10 @@ prettyPrintParseErrorMessages msgOr msgUnknown msgExpecting msgUnExpected msgEnd
 indent :: Box.Box -> Box.Box
 indent = Box.moveUp 1 . Box.moveDown 1 . Box.moveRight 2
 
+-- | Indent to the right without vertical padding.
+indent' :: Box.Box -> Box.Box
+indent' = Box.moveRight 2
+
 line :: Text -> Box.Box
 line = Box.text . T.unpack
 
diff --git a/src/Language/PureScript/Sugar/BindingGroups.hs b/src/Language/PureScript/Sugar/BindingGroups.hs
index a4efc201d6..6de8f4d2f0 100644
--- a/src/Language/PureScript/Sugar/BindingGroups.hs
+++ b/src/Language/PureScript/Sugar/BindingGroups.hs
@@ -12,7 +12,7 @@ module Language.PureScript.Sugar.BindingGroups
 import Prelude.Compat
 import Protolude (ordNub)
 
-import Control.Monad ((<=<))
+import Control.Monad (void, (<=<))
 import Control.Monad.Error.Class (MonadError(..))
 
 import Data.Graph
@@ -26,6 +26,7 @@ import Language.PureScript.Crash
 import Language.PureScript.Environment
 import Language.PureScript.Errors
 import Language.PureScript.Names
+import Language.PureScript.PSString (PSString, prettyPrintString)
 import Language.PureScript.Types
 
 -- |
@@ -53,7 +54,6 @@ createBindingGroups
   -> [Declaration]
   -> m [Declaration]
 createBindingGroups moduleName = mapM f <=< handleDecls
-
   where
   (f, _, _) = everywhereOnValuesTopDownM return handleExprs return
 
@@ -66,14 +66,22 @@ createBindingGroups moduleName = mapM f <=< handleDecls
   --
   handleDecls :: [Declaration] -> m [Declaration]
   handleDecls ds = do
-    let values = mapMaybe (fmap (fmap extractGuardedExpr) . getValueDeclaration) ds
-        dataDecls = filter isDataDecl ds
+    let dataDecls = filter isDataDecl ds
         allProperNames = fmap declTypeName dataDecls
         dataVerts = fmap (\d -> (d, declTypeName d, usedTypeNames moduleName d `intersect` allProperNames)) dataDecls
     dataBindingGroupDecls <- parU (stronglyConnComp dataVerts) toDataBindingGroup
-    let allIdents = fmap valdeclIdent values
+
+    let values = mapMaybe (fmap (fmap extractGuardedExpr) . getValueDeclaration) ds
+        allIdents = fmap valdeclIdent values
         valueVerts = fmap (\d -> (d, valdeclIdent d, usedIdents moduleName d `intersect` allIdents)) values
-    bindingGroupDecls <- parU (stronglyConnComp valueVerts) (toBindingGroup moduleName)
+    bindingGroupDecls <- parU (stronglyConnComp valueVerts) (toBindingGroups usedImmediateIdents moduleName)
+
+    let dictValues = mapMaybe (fmap (fmap extractGuardedExpr) . getDictDeclaration) ds
+        dictIdents = fmap valdeclIdent dictValues
+        dictValueVerts = fmap (\d -> (d, valdeclIdent d, usedIdents moduleName d `intersect` dictIdents)) dictValues
+        checkDeclsForInvalidCycles = toBindingGroups
+    void $ parU (stronglyConnComp dictValueVerts) (checkDeclsForInvalidCycles immediateLitIdentsAndAllOtherIdents moduleName)
+
     return $ filter isImportDecl ds ++
              filter isExternKindDecl ds ++
              filter isExternDataDecl ds ++
@@ -119,11 +127,32 @@ usedIdents moduleName = ordNub . usedIdents' S.empty . valdeclExpression
     | moduleName == moduleName' && ToplevelIdent name `S.notMember` scope = [name]
   usedNamesE _ _ = []
 
-usedImmediateIdents :: ModuleName -> Declaration -> [Ident]
-usedImmediateIdents moduleName =
-  let (f, _, _, _, _) = everythingWithContextOnValues True [] (++) def usedNamesE def def def
-  in ordNub . f
+immediateLitIdentsAndAllOtherIdents :: ModuleName -> Expr -> [Ident]
+immediateLitIdentsAndAllOtherIdents moduleName = ordNub . g
   where
+  (_, g, _, _, _) = everythingWithContextOnValues True [] (++) def usedNamesE usedNamesLitE def def def
+
+  def s _ = (s, [])
+
+  usedNamesE :: Bool -> Expr -> (Bool, [Ident])
+  usedNamesE True (Var _ (Qualified Nothing name)) = (True, [name])
+  usedNamesE True (Var _ (Qualified (Just moduleName') name))
+    | moduleName == moduleName' = (True, [name])
+  usedNamesE scope _ = (scope, [])
+
+  usedNamesLitE :: Bool -> Expr -> (Bool, [Ident])
+  usedNamesLitE True (Var _ (Qualified Nothing name)) = (True, [name])
+  usedNamesLitE True (Var _ (Qualified (Just moduleName') name))
+    | moduleName == moduleName' = (True, [name])
+  usedNamesLitE True (App (stripTypedAndPositioned -> (Abs _ e0)) e1) = (True, g e0 ++ g e1)
+  usedNamesLitE True (Abs _ _) = (False, [])
+  usedNamesLitE scope _ = (scope, [])
+
+usedImmediateIdents :: ModuleName -> Expr -> [Ident]
+usedImmediateIdents moduleName = ordNub . g
+  where
+  (_, g, _, _, _) = everythingWithContextOnValues True [] (++) def usedNamesE usedNamesE def def def
+
   def s _ = (s, [])
 
   usedNamesE :: Bool -> Expr -> (Bool, [Ident])
@@ -134,10 +163,10 @@ usedImmediateIdents moduleName =
   usedNamesE scope _ = (scope, [])
 
 usedTypeNames :: ModuleName -> Declaration -> [ProperName 'TypeName]
-usedTypeNames moduleName =
-  let (f, _, _, _, _) = accumTypes (everythingOnTypes (++) usedNames)
-  in ordNub . f
+usedTypeNames moduleName = ordNub . f
   where
+  (f, _, _, _, _) = accumTypes (everythingOnTypes (++) usedNames)
+
   usedNames :: SourceType -> [ProperName 'TypeName]
   usedNames (ConstrainedType _ con _) =
     case con of
@@ -157,37 +186,83 @@ declTypeName _ = internalError "Expected DataDeclaration"
 -- Convert a group of mutually-recursive dependencies into a BindingGroupDeclaration (or simple ValueDeclaration).
 --
 --
-toBindingGroup
+toBindingGroups
   :: forall m
    . (MonadError MultipleErrors m)
-   => ModuleName
+   => (ModuleName -> Expr -> [Ident])
+   -> ModuleName
    -> SCC (ValueDeclarationData Expr)
    -> m Declaration
-toBindingGroup _ (AcyclicSCC d) = return (mkDeclaration d)
-toBindingGroup moduleName (CyclicSCC ds') = do
+toBindingGroups _ _ (AcyclicSCC d) = return (mkDeclaration d)
+toBindingGroups getIdents moduleName (CyclicSCC ds') = do
   -- Once we have a mutually-recursive group of declarations, we need to sort
-  -- them further by their immediate dependencies (those outside function
-  -- bodies). In particular, this is relevant for type instance dictionaries
-  -- whose members require other type instances (for example, functorEff
-  -- defines (<$>) = liftA1, which depends on applicativeEff). Note that
-  -- superclass references are still inside functions, so don't count here.
+  -- them further by appropriate subsets of their dependencies (generally, those
+  -- outside function bodies). In particular, this is relevant for type instance
+  -- dictionaries whose members require other type instances (for example,
+  -- functorEff defines (<$>) = liftA1, which depends on applicativeEff). Note
+  -- that superclass references are still inside functions, so don't count here.
   -- If we discover declarations that still contain mutually-recursive
   -- immediate references, we're guaranteed to get an undefined reference at
-  -- runtime, so treat this as an error. See also github issue #365.
+  -- runtime, so treat this as an error.
+  -- (See also github issues #365, #2975, and #3429.)
   BindingGroupDeclaration . NEL.fromList <$> mapM toBinding (stronglyConnComp valueVerts)
   where
+  cycleErrors :: ValueDeclarationData Expr -> MultipleErrors
+  cycleErrors (ValueDeclarationData (ss, _) n _ _ e) =
+    case (e, stripAbs e) of
+      (TypedValue _ (stripTypedAndPositioned -> (Var _ _)) st, _)
+        | isFunctionType st -> errorMessage' ss $ MissingEtaExpansion n
+      (_, TypeClassDictionaryConstructorApp _ (getFields -> Just fields)) ->
+        let getData = map getFieldData . filter (refersToIdent n . snd)
+        in errorMessage' ss $ CycleInDictDeclaration n $ getData fields
+      _ -> errorMessage' ss $ CycleInDeclaration n
+
+  getFieldData :: (PSString, Expr) -> (Ident, SourceSpan, DictMemberType)
+  getFieldData (psString, expr) = case separateValAndType expr of
+    (expr', mSt) -> (ident, getSourceSpan expr', isFn mSt)
+    where
+    ident = Ident $ prettyPrintString psString
+    isFn = maybe NonFn (\st -> if isFunctionType st then Fn else NonFn)
+
+  getFields :: Expr -> Maybe [(PSString, Expr)]
+  getFields expr = case stripTypedAndPositioned expr of
+    Literal _ (ObjectLiteral fields) -> Just fields
+    _ -> Nothing
+
+  getSourceSpan :: Expr -> SourceSpan
+  getSourceSpan (PositionedValue ss _ _) = ss
+  getSourceSpan (Literal ss _) = ss
+  getSourceSpan (UnaryMinus ss _) = ss
+  getSourceSpan (Var ss _) = ss
+  getSourceSpan (Op ss _) = ss
+  getSourceSpan (Constructor ss _) = ss
+  getSourceSpan (App (stripTypedAndPositioned -> (Abs _ expr)) _) = getSourceSpan expr
+  getSourceSpan (TypedValue _ expr _) = getSourceSpan expr
+  getSourceSpan _ = NullSourceSpan
+
   idents :: [Ident]
   idents = fmap (\(_, i, _) -> i) valueVerts
 
-  valueVerts :: [(ValueDeclarationData Expr, Ident, [Ident])]
-  valueVerts = fmap (\d -> (d, valdeclIdent d, usedImmediateIdents moduleName (mkDeclaration d) `intersect` idents)) ds'
+  refersToIdent :: Ident -> Expr -> Bool
+  refersToIdent ident = elem ident . getIdents moduleName
+
+  separateValAndType :: Expr -> (Expr, Maybe SourceType)
+  separateValAndType (TypedValue _ e st) =
+    let (e', _) = separateValAndType e
+    in  (e', Just st)
+  separateValAndType e = (e, Nothing)
+
+  stripAbs :: Expr -> Expr
+  stripAbs e = case stripTypedAndPositioned e of
+    Abs _ e' -> stripAbs e'
+    e' -> e'
 
   toBinding :: SCC (ValueDeclarationData Expr) -> m ((SourceAnn, Ident), NameKind, Expr)
   toBinding (AcyclicSCC d) = return $ fromValueDecl d
-  toBinding (CyclicSCC ds) = throwError $ foldMap cycleError ds
+  toBinding (CyclicSCC ds) = throwError $ foldMap cycleErrors ds
 
-  cycleError :: ValueDeclarationData Expr -> MultipleErrors
-  cycleError (ValueDeclarationData (ss, _) n _ _ _) = errorMessage' ss $ CycleInDeclaration n
+  valueVerts :: [(ValueDeclarationData Expr, Ident, [Ident])]
+  valueVerts = fmap (\d -> (d, valdeclIdent d, getIdents moduleName (valdeclExpression d) `intersect` idents)) ds'
 
 toDataBindingGroup
   :: MonadError MultipleErrors m
diff --git a/src/Language/PureScript/Sugar/TypeClasses.hs b/src/Language/PureScript/Sugar/TypeClasses.hs
index 761de6f631..5866fedf9d 100644
--- a/src/Language/PureScript/Sugar/TypeClasses.hs
+++ b/src/Language/PureScript/Sugar/TypeClasses.hs
@@ -338,7 +338,7 @@ typeInstanceDictionaryDeclaration sa@(ss, _) name mn deps className tys decls =
   memberToValue :: [(Ident, SourceType)] -> Declaration -> Desugar m Expr
   memberToValue tys' (ValueDecl (ss', _) ident _ [] [MkUnguarded val]) = do
     _ <- maybe (throwError . errorMessage' ss' $ ExtraneousClassMember ident className) return $ lookup ident tys'
-    return val
+    return (PositionedValue ss' [] val)
   memberToValue _ _ = internalError "Invalid declaration in type instance definition"
 
 declIdent :: Declaration -> Maybe Ident
diff --git a/src/Language/PureScript/TypeChecker/Skolems.hs b/src/Language/PureScript/TypeChecker/Skolems.hs
index 170ea7ebcd..f883c01525 100644
--- a/src/Language/PureScript/TypeChecker/Skolems.hs
+++ b/src/Language/PureScript/TypeChecker/Skolems.hs
@@ -89,7 +89,7 @@ skolemEscapeCheck expr@TypedValue{} =
     traverse_ (throwError . singleError) (toSkolemErrors expr)
   where
     toSkolemErrors :: Expr -> [ErrorMessage]
-    (_, toSkolemErrors, _, _, _) = everythingWithContextOnValues (mempty, Nothing) [] (<>) def go def def def
+    (_, toSkolemErrors, _, _, _) = everythingWithContextOnValues (mempty, Nothing) [] (<>) def go go def def def
 
     def s _ = (s, [])
 
diff --git a/tests/purs/failing/3407-NewtypeInstanceDerivOfRecursType.purs b/tests/purs/failing/3407-NewtypeInstanceDerivOfRecursType.purs
new file mode 100644
index 0000000000..fa6c503824
--- /dev/null
+++ b/tests/purs/failing/3407-NewtypeInstanceDerivOfRecursType.purs
@@ -0,0 +1,10 @@
+-- @shouldFailWith CycleInDeclaration
+-- Example submitted by dbeacham in issue #3407.
+module Main where
+
+import Prelude
+import Data.Maybe
+
+newtype MyRec = MyRec { a :: Int, b :: Maybe MyRec }
+
+derive newtype instance showMyRec :: Show MyRec
diff --git a/tests/purs/failing/3429-00.purs b/tests/purs/failing/3429-00.purs
new file mode 100644
index 0000000000..16b8abf970
--- /dev/null
+++ b/tests/purs/failing/3429-00.purs
@@ -0,0 +1,10 @@
+-- @shouldFailWith CycleInDictDeclaration
+module Main where
+
+class C a where
+  c0 :: a
+  c1 :: a
+
+instance cInt :: C Int where
+  c0 = 0
+  c1 = c0
diff --git a/tests/purs/failing/3429-01.purs b/tests/purs/failing/3429-01.purs
new file mode 100644
index 0000000000..a19f8e7e69
--- /dev/null
+++ b/tests/purs/failing/3429-01.purs
@@ -0,0 +1,14 @@
+-- @shouldFailWith CycleInDictDeclaration
+module Main where
+
+class B
+
+instance b :: B
+
+class C a where
+  c0 :: a
+  c1 :: a
+
+instance cInt :: B => C Int where
+  c0 = 0
+  c1 = c0
diff --git a/tests/purs/failing/3429-02.purs b/tests/purs/failing/3429-02.purs
new file mode 100644
index 0000000000..d67184e77a
--- /dev/null
+++ b/tests/purs/failing/3429-02.purs
@@ -0,0 +1,18 @@
+-- @shouldFailWith CycleInDictDeclaration
+module Main where
+
+class B0
+
+instance b0 :: B0
+
+class B1
+
+instance b1 :: B1
+
+class C a where
+  c0 :: a
+  c1 :: a
+
+instance cInt :: (B0, B1) => C Int where
+  c0 = 0
+  c1 = c0
diff --git a/tests/purs/failing/3429-03.purs b/tests/purs/failing/3429-03.purs
new file mode 100644
index 0000000000..d8fc42ce57
--- /dev/null
+++ b/tests/purs/failing/3429-03.purs
@@ -0,0 +1,18 @@
+-- @shouldFailWith CycleInDictDeclaration
+module Main where
+
+class B0
+
+instance b0 :: B0
+
+class B1 a
+
+instance b1 :: B1 a
+
+class C a where
+  c0 :: a
+  c1 :: a
+
+instance cInt :: (B0, B1 Int) => C Int where
+  c0 = 0
+  c1 = c0
diff --git a/tests/purs/failing/3429-04.purs b/tests/purs/failing/3429-04.purs
new file mode 100644
index 0000000000..d8fc42ce57
--- /dev/null
+++ b/tests/purs/failing/3429-04.purs
@@ -0,0 +1,18 @@
+-- @shouldFailWith CycleInDictDeclaration
+module Main where
+
+class B0
+
+instance b0 :: B0
+
+class B1 a
+
+instance b1 :: B1 a
+
+class C a where
+  c0 :: a
+  c1 :: a
+
+instance cInt :: (B0, B1 Int) => C Int where
+  c0 = 0
+  c1 = c0
diff --git a/tests/purs/failing/3429-05.purs b/tests/purs/failing/3429-05.purs
new file mode 100644
index 0000000000..d98cd4b616
--- /dev/null
+++ b/tests/purs/failing/3429-05.purs
@@ -0,0 +1,25 @@
+-- @shouldFailWith CycleInDictDeclaration
+module Main where
+
+class B0
+
+instance b0 :: B0
+
+class B1 a where
+  x :: a
+
+instance b1Int :: B1 Int where
+  x = 0
+
+class C a where
+  c0 :: a
+  c1 :: a
+
+instance cInt :: (B0, B1 Int) => C Int where
+  c0 = 0
+  c1 =
+    let
+      const' :: forall a. B1 Int => a -> Int -> a
+      const' a _ = a
+    in
+      const' c0 x
diff --git a/tests/purs/failing/3429-06.purs b/tests/purs/failing/3429-06.purs
new file mode 100644
index 0000000000..ebdc9c1f77
--- /dev/null
+++ b/tests/purs/failing/3429-06.purs
@@ -0,0 +1,25 @@
+-- @shouldFailWith CycleInDictDeclaration
+module Main where
+
+class B0
+
+instance b0 :: B0
+
+class B1 a where
+  x :: a
+
+instance b1Int :: B1 Int where
+  x = 0
+
+class C a where
+  c0 :: a
+  c1 :: a
+
+instance cInt :: (B0, B1 Int) => C Int where
+  c0 = 0
+  c1 =
+    let
+      const' :: forall a b. a -> b -> a
+      const' a _ = a
+    in
+      const' c0 (x :: Int)
diff --git a/tests/purs/failing/3429-07.purs b/tests/purs/failing/3429-07.purs
new file mode 100644
index 0000000000..6a3f9cf85f
--- /dev/null
+++ b/tests/purs/failing/3429-07.purs
@@ -0,0 +1,15 @@
+-- @shouldFailWith CycleInDictDeclaration
+module Main where
+
+class B
+
+instance b :: B
+
+class C a where
+  c0 :: a
+  c1 :: a
+
+instance cInt :: C Int where
+  c0 = 0
+  c1 :: B => Int
+  c1 = c0
diff --git a/tests/purs/failing/3429-08.purs b/tests/purs/failing/3429-08.purs
new file mode 100644
index 0000000000..22c8c1c7ec
--- /dev/null
+++ b/tests/purs/failing/3429-08.purs
@@ -0,0 +1,15 @@
+-- @shouldFailWith CycleInDictDeclaration
+module Main where
+
+class B
+
+instance b :: B
+
+class B <= C a where
+  c0 :: a
+  c1 :: a
+
+instance cInt :: B => C Int where
+  c0 = 0
+  c1 :: B => Int
+  c1 = c0
diff --git a/tests/purs/failing/3429-09.purs b/tests/purs/failing/3429-09.purs
new file mode 100644
index 0000000000..6bed0cdf53
--- /dev/null
+++ b/tests/purs/failing/3429-09.purs
@@ -0,0 +1,18 @@
+-- @shouldFailWith CycleInDictDeclaration
+module Main where
+
+class B
+
+instance b :: B
+
+class C a where
+  c0 :: Int -> a
+  c1 :: Int -> a
+
+instance cInt :: C Int where
+  c0 _ = 0
+  c1 :: B => Int -> Int
+  c1 = c0
+
+c :: Int -> Int
+c = c0
diff --git a/tests/purs/failing/3429-10.purs b/tests/purs/failing/3429-10.purs
new file mode 100644
index 0000000000..c3cdd9e41d
--- /dev/null
+++ b/tests/purs/failing/3429-10.purs
@@ -0,0 +1,16 @@
+-- @shouldFailWith CycleInDictDeclaration
+-- @shouldFailWith CycleInDictDeclaration
+-- Cf. 3429-20.purs, passing/3429/19.purs, passing/3429/20.purs, passing/3429/21.purs
+module Main where
+
+class C0 a where
+  c0 :: a
+
+class C1 a where
+  c1 :: a
+
+instance c0Int :: C0 Int where
+  c0 = c1
+
+instance c1Int :: C1 Int where
+  c1 = c0
diff --git a/tests/purs/failing/3429-11.purs b/tests/purs/failing/3429-11.purs
new file mode 100644
index 0000000000..61ce799810
--- /dev/null
+++ b/tests/purs/failing/3429-11.purs
@@ -0,0 +1,19 @@
+-- @shouldFailWith CycleInDictDeclaration
+-- @shouldFailWith CycleInDictDeclaration
+module Main where
+
+class B
+
+instance b :: B
+
+class C0 a where
+  c0 :: a
+
+class C1 a where
+  c1 :: a
+
+instance c0Int :: B => C0 Int where
+  c0 = c1
+
+instance c1Int :: C1 Int where
+  c1 = c0
diff --git a/tests/purs/failing/3429-12.purs b/tests/purs/failing/3429-12.purs
new file mode 100644
index 0000000000..36ab88b063
--- /dev/null
+++ b/tests/purs/failing/3429-12.purs
@@ -0,0 +1,19 @@
+-- @shouldFailWith CycleInDictDeclaration
+-- @shouldFailWith CycleInDictDeclaration
+module Main where
+
+class B
+
+instance b :: B
+
+class C0 a where
+  c0 :: a
+
+class C1 a where
+  c1 :: a
+
+instance c0Int :: B => C0 Int where
+  c0 = c1
+
+instance c1Int :: B => C1 Int where
+  c1 = c0
diff --git a/tests/purs/failing/3429-13.purs b/tests/purs/failing/3429-13.purs
new file mode 100644
index 0000000000..d4e1d680c9
--- /dev/null
+++ b/tests/purs/failing/3429-13.purs
@@ -0,0 +1,20 @@
+-- @shouldFailWith CycleInDictDeclaration
+-- @shouldFailWith CycleInDictDeclaration
+module Main where
+
+class B
+
+instance b :: B
+
+class C0 a where
+  c0 :: a
+
+class C1 a where
+  c1 :: a
+
+instance c0Int :: C0 Int where
+  c0 :: B => Int
+  c0 = c1
+
+instance c1Int :: C1 Int where
+  c1 = c0
diff --git a/tests/purs/failing/3429-14.purs b/tests/purs/failing/3429-14.purs
new file mode 100644
index 0000000000..b64aaf061d
--- /dev/null
+++ b/tests/purs/failing/3429-14.purs
@@ -0,0 +1,21 @@
+-- @shouldFailWith CycleInDictDeclaration
+-- @shouldFailWith CycleInDictDeclaration
+module Main where
+
+class B
+
+instance b :: B
+
+class C0 a where
+  c0 :: a
+
+class C1 a where
+  c1 :: a
+
+instance c0Int :: C0 Int where
+  c0 :: B => Int
+  c0 = c1
+
+instance c1Int :: C1 Int where
+  c1 :: B => Int
+  c1 = c0
diff --git a/tests/purs/failing/3429-15.purs b/tests/purs/failing/3429-15.purs
new file mode 100644
index 0000000000..eb6d664763
--- /dev/null
+++ b/tests/purs/failing/3429-15.purs
@@ -0,0 +1,20 @@
+-- @shouldFailWith CycleInDictDeclaration
+-- @shouldFailWith CycleInDictDeclaration
+module Main where
+
+class B
+
+instance b :: B
+
+class C0 a where
+  c0 :: a
+
+class C1 a where
+  c1 :: a
+
+instance c0Int :: B => C0 Int where
+  c0 = c1
+
+instance c1Int :: B => C1 Int where
+  c1 :: B => Int
+  c1 = c0
diff --git a/tests/purs/failing/3429-16.purs b/tests/purs/failing/3429-16.purs
new file mode 100644
index 0000000000..404a6c4324
--- /dev/null
+++ b/tests/purs/failing/3429-16.purs
@@ -0,0 +1,21 @@
+-- @shouldFailWith CycleInDictDeclaration
+-- @shouldFailWith CycleInDictDeclaration
+module Main where
+
+class B
+
+instance b :: B
+
+class C0 a where
+  c0 :: a
+
+class C1 a where
+  c1 :: a
+
+instance c0Int :: B => C0 Int where
+  c0 :: B => Int
+  c0 = c1
+
+instance c1Int :: B => C1 Int where
+  c1 :: B => Int
+  c1 = c0
diff --git a/tests/purs/failing/3429-17.purs b/tests/purs/failing/3429-17.purs
new file mode 100644
index 0000000000..ffa2639fcf
--- /dev/null
+++ b/tests/purs/failing/3429-17.purs
@@ -0,0 +1,45 @@
+-- @shouldFailWith CycleInDictDeclaration
+module Main where
+
+import Data.Tuple (Tuple(Tuple))
+
+class B0
+
+instance b0 :: B0
+
+class B1 a where
+  x1 :: a
+
+instance b1Int :: B1 Int where
+  x1 = 0
+
+class B2 a where
+  x2 :: a
+
+instance b2Tuple :: B1 a => B2 (Tuple a a) where
+  x2 = Tuple x1 x1
+
+class B1 a <= B3 a where
+  x3 :: a
+
+instance b3Int :: B3 Int where
+  x3 = x1
+
+class C a where
+  c0 :: a
+  c1 :: a
+
+instance cInt
+  :: ( B0
+     , B1 Int
+     , B2 (Tuple Int Int)
+     , B3 Int
+     )
+  => C Int where
+  c0 = 0
+  c1 =
+    let
+      const' :: forall a b c d. a -> b -> c -> d -> a
+      const' a _ _ _ = a
+    in
+      const' c0 (x1 :: Int) (x2 :: Tuple Int Int) (x3 :: Int)
diff --git a/tests/purs/failing/3429-18.purs b/tests/purs/failing/3429-18.purs
new file mode 100644
index 0000000000..04a8bf07ac
--- /dev/null
+++ b/tests/purs/failing/3429-18.purs
@@ -0,0 +1,14 @@
+-- @shouldFailWith CycleInDictDeclaration
+module Main where
+
+class B
+
+instance b :: B
+
+class B <= C a where
+  c0 :: a
+  c1 :: a
+
+instance cInt :: C Int where
+  c0 = 0
+  c1 = c0
diff --git a/tests/purs/failing/3429-19.purs b/tests/purs/failing/3429-19.purs
new file mode 100644
index 0000000000..86a30e3d8a
--- /dev/null
+++ b/tests/purs/failing/3429-19.purs
@@ -0,0 +1,12 @@
+-- @shouldFailWith CycleInDictDeclaration
+module Main where
+
+data D a = D0 | D1 a
+
+class C a where
+  c0 :: a
+  c1 :: a
+
+instance cD :: C a => C (D a) where
+  c0 = D0
+  c1 = c0
diff --git a/tests/purs/failing/3429-20.purs b/tests/purs/failing/3429-20.purs
new file mode 100644
index 0000000000..59c49df390
--- /dev/null
+++ b/tests/purs/failing/3429-20.purs
@@ -0,0 +1,16 @@
+-- @shouldFailWith CycleInDictDeclaration
+-- @shouldFailWith CycleInDictDeclaration
+-- Cf. 3429-20.purs, passing/3429/19.purs, passing/3429/20.purs, passing/3429/21.purs
+module Main where
+
+class C0 a where
+  c0 :: Int -> a
+
+class C1 a where
+  c1 :: Int -> a
+
+instance c0Int :: C0 Int where
+  c0 = c1
+
+instance c1Int :: C1 Int where
+  c1 = c0
diff --git a/tests/purs/failing/3429-21.purs b/tests/purs/failing/3429-21.purs
new file mode 100644
index 0000000000..cac1988bd0
--- /dev/null
+++ b/tests/purs/failing/3429-21.purs
@@ -0,0 +1,15 @@
+-- @shouldFailWith CycleInDictDeclaration
+module Main where
+
+class B
+
+instance b :: B
+
+class C a where
+  c0 :: a
+  c1 :: a
+
+instance cInt :: B => C Int where
+  c0 = 0
+  c1 :: B => Int
+  c1 = c0
diff --git a/tests/purs/failing/3429-22.purs b/tests/purs/failing/3429-22.purs
new file mode 100644
index 0000000000..fdd6a6c0df
--- /dev/null
+++ b/tests/purs/failing/3429-22.purs
@@ -0,0 +1,9 @@
+-- @shouldFailWith CycleInDictDeclaration
+-- Cf. passing/3429/22.purs
+module Main where
+
+class C a where
+  c :: Int -> a
+
+instance cInt :: C Int where
+  c = c
diff --git a/tests/purs/failing/3429-23.purs b/tests/purs/failing/3429-23.purs
new file mode 100644
index 0000000000..55025c1e83
--- /dev/null
+++ b/tests/purs/failing/3429-23.purs
@@ -0,0 +1,16 @@
+-- @shouldFailWith CycleInDictDeclaration
+module Main where
+
+class C a where
+  c0 :: a
+  c1 :: a
+  c2 :: a
+  c3 :: a
+  c4 :: a
+
+instance cInt :: C Int where
+  c0 = 0
+  c1 = c0
+  c2 = c0
+  c3 = c0
+  c4 = c0
diff --git a/tests/purs/failing/3429-24.purs b/tests/purs/failing/3429-24.purs
new file mode 100644
index 0000000000..59a47e9396
--- /dev/null
+++ b/tests/purs/failing/3429-24.purs
@@ -0,0 +1,16 @@
+-- @shouldFailWith CycleInDictDeclaration
+module Main where
+
+class C a where
+  c0 :: a -> a
+  c1 :: a -> a
+  c2 :: a -> a
+  c3 :: a -> a
+  c4 :: a -> a
+
+instance cInt :: C Int where
+  c0 _ = 0
+  c1 = c0
+  c2 = c0
+  c3 = c0
+  c4 = c0
diff --git a/tests/purs/failing/3429-HeytingAlgebra.js b/tests/purs/failing/3429-HeytingAlgebra.js
new file mode 100644
index 0000000000..a076fd3fd4
--- /dev/null
+++ b/tests/purs/failing/3429-HeytingAlgebra.js
@@ -0,0 +1,17 @@
+"use strict";
+
+exports.boolConj = function (b1) {
+  return function (b2) {
+    return b1 && b2;
+  };
+};
+
+exports.boolDisj = function (b1) {
+  return function (b2) {
+    return b1 || b2;
+  };
+};
+
+exports.boolNot = function (b) {
+  return !b;
+};
diff --git a/tests/purs/failing/3429-HeytingAlgebra.purs b/tests/purs/failing/3429-HeytingAlgebra.purs
new file mode 100644
index 0000000000..d422b1ae1c
--- /dev/null
+++ b/tests/purs/failing/3429-HeytingAlgebra.purs
@@ -0,0 +1,34 @@
+-- @shouldFailWith CycleInDictDeclaration
+module Main where
+
+import Prelude ((<<<))
+
+class HeytingAlgebra a where
+  ff :: a
+  tt :: a
+  implies :: a -> a -> a
+  conj :: a -> a -> a
+  disj :: a -> a -> a
+  not :: a -> a
+
+foreign import boolConj :: Boolean -> Boolean -> Boolean
+foreign import boolDisj :: Boolean -> Boolean -> Boolean
+foreign import boolNot :: Boolean -> Boolean
+
+-- | Like the analogous instance declaration in 'passing/3429/HeytingAlgebra.purs',
+-- | this definition of `heytingAlgebraBoolean` is self-referential
+-- | in that one of its components, `implies`, depends on two of the instance's
+-- | other members (namely, `not` and `disj`).
+-- | However, although the definition in
+-- | 'passing/3429/HeytingAlgebra.purs' type-checks,
+-- | the following definition does not,
+-- | since the terms `not` and `||` are immediately applied to `<<<`.
+-- | In other words, no `Abs` expression exists to obscure the typechecker's
+-- | process for cycle determination.
+instance heytingAlgebraBoolean :: HeytingAlgebra Boolean where
+  ff = false
+  tt = true
+  implies = disj <<< not
+  conj = boolConj
+  disj = boolDisj
+  not = boolNot
diff --git a/tests/purs/failing/3429-chrismshelton.purs b/tests/purs/failing/3429-chrismshelton.purs
new file mode 100644
index 0000000000..34e72f2677
--- /dev/null
+++ b/tests/purs/failing/3429-chrismshelton.purs
@@ -0,0 +1,33 @@
+-- @shouldFailWith CycleInDictDeclaration
+-- Example submitted by chrismshelton.
+-- Cf. passing/3429/chrismshelton.purs
+module Main where
+
+import Prelude
+import Effect (Effect)
+import Effect.Console (log)
+
+class CA v a where
+  lengthA :: forall m . v m a -> Int
+
+class (CA w a) <= CB v w a | v a -> w, w a -> v where
+  lengthB :: v a -> Int
+  fromA :: forall m . w m a -> v a
+  toA   :: forall m . v a -> w m a
+
+defaultLengthB :: forall v w a . (CB v w a) => v a -> Int
+defaultLengthB v = lengthA $ toA v
+
+data DA m a = DA Int
+data DB a = DB Int
+
+instance caDA :: CA DA a where
+  lengthA (DA i) = i
+
+instance cbDB :: (CA DA a) => CB DB DA a where
+  lengthB = defaultLengthB
+  fromA (DA a) = (DB a)
+  toA (DB a) = (DA a)
+
+main :: Effect Unit
+main = log (show (lengthB (fromA (DA 3))))
diff --git a/tests/purs/failing/3429-fsoikin.purs b/tests/purs/failing/3429-fsoikin.purs
new file mode 100644
index 0000000000..d980508b56
--- /dev/null
+++ b/tests/purs/failing/3429-fsoikin.purs
@@ -0,0 +1,14 @@
+-- @shouldFailWith CycleInDictDeclaration
+-- Example submitted by fsoikin in issue #3488.
+module Main where
+
+import Prelude (class Ord, class Semiring, zero, (>))
+import Data.Array (filter)
+
+class C a where
+  f :: a -> Boolean
+  g :: Array a
+
+instance cInst :: (Ord a, Semiring a) => C a where
+  f i = i > zero
+  g = filter f []
diff --git a/tests/purs/failing/3429-nukisman.purs b/tests/purs/failing/3429-nukisman.purs
new file mode 100644
index 0000000000..71036e29f0
--- /dev/null
+++ b/tests/purs/failing/3429-nukisman.purs
@@ -0,0 +1,16 @@
+-- @shouldFailWith CycleInDictDeclaration
+-- Example submitted by nukisman in issue #2975.
+-- Cf. passing/3429/nukisman.purs
+module Main where
+
+import Data.Foldable (class Foldable, foldrDefault, foldMapDefaultL)
+
+data Tree a
+  = Leaf
+  | Branch (Tree a) a (Tree a)
+
+instance foldableTree :: Foldable Tree where
+  foldl _ acc Leaf = acc
+  foldl f acc (Branch l e r) = acc -- Just for debug
+  foldr = foldrDefault
+  foldMap = foldMapDefaultL
diff --git a/tests/purs/failing/365.purs b/tests/purs/failing/365.purs
index 86a56d307d..9fe86883fd 100644
--- a/tests/purs/failing/365.purs
+++ b/tests/purs/failing/365.purs
@@ -1,4 +1,5 @@
--- @shouldFailWith CycleInDeclaration
+-- @shouldFailWith CycleInDictDeclaration
+-- Cf. 3429-*.purs and passing/365.purs
 module Main where
 
 import Prelude
diff --git a/tests/purs/failing/Foldable.purs b/tests/purs/failing/Foldable.purs
index daea9d9cfc..12d498fc25 100644
--- a/tests/purs/failing/Foldable.purs
+++ b/tests/purs/failing/Foldable.purs
@@ -1,4 +1,5 @@
--- @shouldFailWith CycleInDeclaration
+-- @shouldFailWith CycleInDictDeclaration
+-- Cf. passing/Foldable.purs and 3429-*.purs
 module Main where
 
 import Prelude
diff --git a/tests/purs/failing/MissingEtaExpansion.purs b/tests/purs/failing/MissingEtaExpansion.purs
new file mode 100644
index 0000000000..7d915262b2
--- /dev/null
+++ b/tests/purs/failing/MissingEtaExpansion.purs
@@ -0,0 +1,6 @@
+-- @shouldFailWith MissingEtaExpansion
+-- Cf. passing/MissingEtaExpanson.purs and passing/UnifyInTypeInstanceLookup.purs
+module Main where
+
+f :: Int -> Int
+f = f
diff --git a/tests/purs/passing/3429.purs b/tests/purs/passing/3429.purs
new file mode 100644
index 0000000000..6892ecef15
--- /dev/null
+++ b/tests/purs/passing/3429.purs
@@ -0,0 +1,32 @@
+module Main where
+
+import Effect.Console (log)
+
+import Mod0
+import Mod1
+import Mod2
+import Mod3
+import Mod4
+import Mod5
+import Mod6
+import Mod7
+import Mod8
+import Mod9
+import Mod10
+import Mod11
+import Mod12
+import Mod13
+import Mod14
+import Mod15
+import Mod16
+import Mod17
+import Mod18
+import Mod19
+import Mod20
+import Mod21
+import Mod22
+import ChrisMShelton
+import HeytingAlgebra
+import Nukisman
+
+main = log "Done"
diff --git a/tests/purs/passing/3429/00.purs b/tests/purs/passing/3429/00.purs
new file mode 100644
index 0000000000..7f02a2438a
--- /dev/null
+++ b/tests/purs/passing/3429/00.purs
@@ -0,0 +1,17 @@
+module Mod0 where
+
+import Prelude
+
+class C a where
+  c0 :: a
+  c1 :: Unit -> a
+
+instance cInt :: C Int where
+  c0 = 0
+  c1 _ = c0
+
+c :: Int
+c = c0
+
+f :: Unit -> Int
+f = c1
diff --git a/tests/purs/passing/3429/01.purs b/tests/purs/passing/3429/01.purs
new file mode 100644
index 0000000000..44b0f1b5c6
--- /dev/null
+++ b/tests/purs/passing/3429/01.purs
@@ -0,0 +1,21 @@
+module Mod1 where
+
+import Prelude
+
+class B
+
+instance b :: B
+
+class C a where
+  c0 :: a
+  c1 :: Unit -> a
+
+instance cInt :: B => C Int where
+  c0 = 0
+  c1 _ = c0
+
+c :: Int
+c = c0
+
+f :: Unit -> Int
+f = c1
diff --git a/tests/purs/passing/3429/02.purs b/tests/purs/passing/3429/02.purs
new file mode 100644
index 0000000000..c1d3afcdc7
--- /dev/null
+++ b/tests/purs/passing/3429/02.purs
@@ -0,0 +1,19 @@
+module Mod2 where
+
+class C0 a where
+  c0 :: a
+
+class C1 a where
+  c1 :: a
+
+instance c0Int :: C0 Int where
+  c0 = 0
+
+instance c1Int :: C1 Int where
+  c1 = 1
+
+d0 :: Int
+d0 = c0
+
+d1 :: Int
+d1 = c1
diff --git a/tests/purs/passing/3429/03.purs b/tests/purs/passing/3429/03.purs
new file mode 100644
index 0000000000..49b905e211
--- /dev/null
+++ b/tests/purs/passing/3429/03.purs
@@ -0,0 +1,19 @@
+module Mod3 where
+
+class C0 a where
+  c0 :: a
+
+class C1 a where
+  c1 :: a
+
+instance c0Int :: C0 Int where
+  c0 = 0
+
+instance c1Int :: C1 Int where
+  c1 = c0
+
+d0 :: Int
+d0 = c0
+
+d1 :: Int
+d1 = c1
diff --git a/tests/purs/passing/3429/04.purs b/tests/purs/passing/3429/04.purs
new file mode 100644
index 0000000000..595029183c
--- /dev/null
+++ b/tests/purs/passing/3429/04.purs
@@ -0,0 +1,24 @@
+module Mod4 where
+
+class B
+
+instance b :: B
+
+class C0 a where
+  c0 :: a
+
+class C1 a where
+  c1 :: a
+
+instance c0Int :: C0 Int where
+  c0 :: B => Int
+  c0 = c1
+
+instance c1Int :: C1 Int where
+  c1 = 1
+
+d0 :: Int
+d0 = c0
+
+d1 :: Int
+d1 = c1
diff --git a/tests/purs/passing/3429/05.purs b/tests/purs/passing/3429/05.purs
new file mode 100644
index 0000000000..fc3cc1ba4f
--- /dev/null
+++ b/tests/purs/passing/3429/05.purs
@@ -0,0 +1,24 @@
+module Mod5 where
+
+class B
+
+instance b :: B
+
+class C0 a where
+  c0 :: a
+
+class C1 a where
+  c1 :: a
+
+instance c0Int :: B => C0 Int where
+  c0 = c1
+
+instance c1Int :: C1 Int where
+  c1 :: B => Int
+  c1 = 1
+
+d0 :: Int
+d0 = c0
+
+d1 :: Int
+d1 = c1
diff --git a/tests/purs/passing/3429/06.purs b/tests/purs/passing/3429/06.purs
new file mode 100644
index 0000000000..5b9c0f8c1b
--- /dev/null
+++ b/tests/purs/passing/3429/06.purs
@@ -0,0 +1,24 @@
+module Mod6 where
+
+class B
+
+instance b :: B
+
+class C0 a where
+  c0 :: a
+
+class C1 a where
+  c1 :: a
+
+instance c0Int :: B => C0 Int where
+  c0 = 0
+
+instance c1Int :: C1 Int where
+  c1 :: B => Int
+  c1 = c0
+
+d0 :: Int
+d0 = c0
+
+d1 :: Int
+d1 = c1
diff --git a/tests/purs/passing/3429/07.purs b/tests/purs/passing/3429/07.purs
new file mode 100644
index 0000000000..b45cf4dbe5
--- /dev/null
+++ b/tests/purs/passing/3429/07.purs
@@ -0,0 +1,24 @@
+module Mod7 where
+
+class B
+
+instance b :: B
+
+class C0 a where
+  c0 :: a
+
+class C1 a where
+  c1 :: a
+
+instance c0Int :: B => C0 Int where
+  c0 = 0
+
+instance c1Int :: B => C1 Int where
+  c1 :: B => Int
+  c1 = c0
+
+d0 :: Int
+d0 = c0
+
+d1 :: Int
+d1 = c1
diff --git a/tests/purs/passing/3429/08.purs b/tests/purs/passing/3429/08.purs
new file mode 100644
index 0000000000..8135766bae
--- /dev/null
+++ b/tests/purs/passing/3429/08.purs
@@ -0,0 +1,7 @@
+module Mod8 where
+
+class C a where
+  c :: Int -> a
+
+instance cInt :: C Int where
+  c i = c i
diff --git a/tests/purs/passing/3429/09.purs b/tests/purs/passing/3429/09.purs
new file mode 100644
index 0000000000..d5575c0c08
--- /dev/null
+++ b/tests/purs/passing/3429/09.purs
@@ -0,0 +1,23 @@
+module Mod9 where
+
+import Prelude
+
+class B a where
+  x :: a
+
+instance bUnit :: B Unit where
+  x = unit
+
+class C a where
+  c0 :: a
+  c1 :: a
+
+instance cUnit :: C Unit where
+  c0 = unit
+  c1 = x
+
+d0 :: Unit
+d0 = c0
+
+d1 :: Unit
+d1 = c0
diff --git a/tests/purs/passing/3429/10.purs b/tests/purs/passing/3429/10.purs
new file mode 100644
index 0000000000..057bf425c6
--- /dev/null
+++ b/tests/purs/passing/3429/10.purs
@@ -0,0 +1,23 @@
+module Mod10 where
+
+import Prelude
+
+class B a where
+  x :: a
+
+instance bUnit :: B Unit where
+  x = unit
+
+class B a <= C a where
+  c0 :: a
+  c1 :: a
+
+instance cUnit :: C Unit where
+  c0 = unit
+  c1 = x
+
+d0 :: Unit
+d0 = c0
+
+d1 :: Unit
+d1 = c0
diff --git a/tests/purs/passing/3429/11.purs b/tests/purs/passing/3429/11.purs
new file mode 100644
index 0000000000..33866a9089
--- /dev/null
+++ b/tests/purs/passing/3429/11.purs
@@ -0,0 +1,23 @@
+module Mod11 where
+
+import Prelude
+
+class B a where
+  x :: a
+
+instance bUnit :: B Unit where
+  x = unit
+
+class C a where
+  c0 :: a
+  c1 :: a
+
+instance cUnit :: B Unit => C Unit where
+  c0 = unit
+  c1 = x
+
+d0 :: Unit
+d0 = c0
+
+d1 :: Unit
+d1 = c0
diff --git a/tests/purs/passing/3429/12.purs b/tests/purs/passing/3429/12.purs
new file mode 100644
index 0000000000..10b73560cc
--- /dev/null
+++ b/tests/purs/passing/3429/12.purs
@@ -0,0 +1,19 @@
+module Mod12 where
+
+class B
+
+instance b :: B
+
+class C a where
+  c0 :: a
+  c1 :: B => a
+
+instance cInt :: C Int where
+  c0 = 0
+  c1 = c0
+
+d0 :: Int
+d0 = c0
+
+d1 :: Int
+d1 = c1
diff --git a/tests/purs/passing/3429/13.purs b/tests/purs/passing/3429/13.purs
new file mode 100644
index 0000000000..f46fe384ed
--- /dev/null
+++ b/tests/purs/passing/3429/13.purs
@@ -0,0 +1,20 @@
+module Mod13 where
+
+class B
+
+instance b :: B
+
+class C a where
+  c0 :: a
+  c1 :: B => a
+
+instance cInt :: C Int where
+  c0 = 0
+  c1 :: B => Int
+  c1 = c0
+
+d0 :: Int
+d0 = c0
+
+d1 :: Int
+d1 = c1
diff --git a/tests/purs/passing/3429/14.purs b/tests/purs/passing/3429/14.purs
new file mode 100644
index 0000000000..31a230dfe4
--- /dev/null
+++ b/tests/purs/passing/3429/14.purs
@@ -0,0 +1,21 @@
+module Mod14 where
+
+data D a = D0 | D1 a
+
+class C a where
+  c0 :: a
+  c1 :: a
+
+instance cInt :: C Int where
+  c0 = 0
+  c1 = 0
+
+instance cD :: C a => C (D a) where
+  c0 = D0
+  c1 = D1 c0
+
+d0 :: Int
+d0 = c0
+
+d1 :: Int
+d1 = c1
diff --git a/tests/purs/passing/3429/15.purs b/tests/purs/passing/3429/15.purs
new file mode 100644
index 0000000000..167cd99fa2
--- /dev/null
+++ b/tests/purs/passing/3429/15.purs
@@ -0,0 +1,21 @@
+-- Cf. 18.purs and 21.purs
+module Mod15 where
+
+class B
+
+instance b :: B
+
+class C a where
+  c0 :: B => a
+  c1 :: B => a
+
+instance cInt :: C Int where
+  c0 = c1
+  c1 = c0
+
+-- The following two values induce endless looping.
+-- d0 :: Int
+-- d0 = c0
+--
+-- d1 :: Int
+-- d1 = c1
diff --git a/tests/purs/passing/3429/16.purs b/tests/purs/passing/3429/16.purs
new file mode 100644
index 0000000000..85f8258273
--- /dev/null
+++ b/tests/purs/passing/3429/16.purs
@@ -0,0 +1,20 @@
+-- Cf. 17.purs and 20.purs
+module Mod16 where
+
+class B
+
+instance b :: B
+
+class C a where
+  c0 :: Int -> a
+  c1 :: Int -> a
+
+instance cInt :: C Int where
+  c0 i = c1 i
+  c1 i = c0 i
+
+d0 :: Int -> Int
+d0 = c0
+
+d1 :: Int -> Int
+d1 = c1
diff --git a/tests/purs/passing/3429/17.purs b/tests/purs/passing/3429/17.purs
new file mode 100644
index 0000000000..a7a56576a2
--- /dev/null
+++ b/tests/purs/passing/3429/17.purs
@@ -0,0 +1,20 @@
+-- Cf. 19.purs
+module Mod17 where
+
+class B
+
+instance b :: B
+
+class C a where
+  c0 :: Int -> a
+  c1 :: Int -> a
+
+instance cInt :: C Int where
+  c0 = \_ -> c0 0
+  c1 = \_ -> c1 0
+
+d0 :: Int -> Int
+d0 = c0
+
+d1 :: Int -> Int
+d1 = c1
diff --git a/tests/purs/passing/3429/18.purs b/tests/purs/passing/3429/18.purs
new file mode 100644
index 0000000000..6e9be25e99
--- /dev/null
+++ b/tests/purs/passing/3429/18.purs
@@ -0,0 +1,21 @@
+-- Cf. 17.purs
+module Mod18 where
+
+class B
+
+instance b :: B
+
+class C a where
+  c0 :: B => a
+  c1 :: B => a
+
+instance cInt :: C Int where
+  c0 = c0
+  c1 = c1
+
+-- The following two values induce endless looping.
+-- d0 :: Int
+-- d0 = c0
+--
+-- d1 :: Int
+-- d1 = c1
diff --git a/tests/purs/passing/3429/19.purs b/tests/purs/passing/3429/19.purs
new file mode 100644
index 0000000000..e5db7d9933
--- /dev/null
+++ b/tests/purs/passing/3429/19.purs
@@ -0,0 +1,25 @@
+-- Cf. 20.purs and failing/3429-20.purs
+module Mod19 where
+
+class B
+
+instance b :: B
+
+class C0 a where
+  c0 :: B => a
+
+class C1 a where
+  c1 :: B => a
+
+instance c0Int :: C0 Int where
+  c0 = c1
+
+instance c1Int :: C1 Int where
+  c1 = c0
+
+-- The following two values induce endless looping.
+-- d0 :: Int
+-- d0 = c0
+--
+-- d1 :: Int
+-- d1 = c1
diff --git a/tests/purs/passing/3429/20.purs b/tests/purs/passing/3429/20.purs
new file mode 100644
index 0000000000..543e8adb11
--- /dev/null
+++ b/tests/purs/passing/3429/20.purs
@@ -0,0 +1,20 @@
+-- Cf. 19.purs, 21.purs, failing/3429-10.purs, failing/3429-20.purs
+module Mod20 where
+
+class C0 a where
+  c0 :: Int -> a
+
+class C1 a where
+  c1 :: Int -> a
+
+instance c0Int :: C0 Int where
+  c0 _ = c1 0
+
+instance c1Int :: C1 Int where
+  c1 _ = c0 0
+
+d0 :: Int -> Int
+d0 = c0
+
+d1 :: Int -> Int
+d1 = c1
diff --git a/tests/purs/passing/3429/21.purs b/tests/purs/passing/3429/21.purs
new file mode 100644
index 0000000000..4cceaf8ff1
--- /dev/null
+++ b/tests/purs/passing/3429/21.purs
@@ -0,0 +1,20 @@
+-- Cf. 20.purs
+module Mod21 where
+
+class C0 a where
+  c0 :: Int -> a
+
+class C1 a where
+  c1 :: Int -> a
+
+instance c0Int :: C0 Int where
+  c0 = c1
+
+instance c1Int :: C1 Int where
+  c1 _ = c0 0
+
+d0 :: Int -> Int
+d0 = c0
+
+d1 :: Int -> Int
+d1 = c1
diff --git a/tests/purs/passing/3429/22.purs b/tests/purs/passing/3429/22.purs
new file mode 100644
index 0000000000..b9edda4fb9
--- /dev/null
+++ b/tests/purs/passing/3429/22.purs
@@ -0,0 +1,16 @@
+-- Cf. failing/3429-22.purs
+module Mod22 where
+
+class B
+
+instance b :: B
+
+class C a where
+  c :: B => a
+
+instance cInt :: C Int where
+  c = c
+
+-- The following value induces endless looping.
+-- c0 :: Int
+-- c0 = c
diff --git a/tests/purs/passing/3429/HeytingAlgebra.js b/tests/purs/passing/3429/HeytingAlgebra.js
new file mode 100644
index 0000000000..a076fd3fd4
--- /dev/null
+++ b/tests/purs/passing/3429/HeytingAlgebra.js
@@ -0,0 +1,17 @@
+"use strict";
+
+exports.boolConj = function (b1) {
+  return function (b2) {
+    return b1 && b2;
+  };
+};
+
+exports.boolDisj = function (b1) {
+  return function (b2) {
+    return b1 || b2;
+  };
+};
+
+exports.boolNot = function (b) {
+  return !b;
+};
diff --git a/tests/purs/passing/3429/HeytingAlgebra.purs b/tests/purs/passing/3429/HeytingAlgebra.purs
new file mode 100644
index 0000000000..0ad2addecd
--- /dev/null
+++ b/tests/purs/passing/3429/HeytingAlgebra.purs
@@ -0,0 +1,32 @@
+-- Cf. failing/3429-HeytingAlgebra.purs
+module HeytingAlgebra where
+
+class HeytingAlgebra a where
+  ff :: a
+  tt :: a
+  implies :: a -> a -> a
+  conj :: a -> a -> a
+  disj :: a -> a -> a
+  not :: a -> a
+
+infixr 2 disj as ||
+
+foreign import boolConj :: Boolean -> Boolean -> Boolean
+foreign import boolDisj :: Boolean -> Boolean -> Boolean
+foreign import boolNot :: Boolean -> Boolean
+
+-- | The definition of `heytingAlgebraBoolean` is self-referential
+-- | in that one of its components, `implies`, depends on two of the instance's
+-- | other members (namely, `not` and `disj`).
+-- | However, despite self-referencing, the following definition type-checks
+-- | because the terms `not` and `||` are within the body of an `Abs` expression
+-- | and therefore beyond the reach of the typechecker's current implementation
+-- | for cycle determination.
+-- | (Cf. tests/purs/failing/HeytingAlgebraBoolean.purs)
+instance heytingAlgebraBoolean :: HeytingAlgebra Boolean where
+  ff = false
+  tt = true
+  implies a b = not a || b
+  conj = boolConj
+  disj = boolDisj
+  not = boolNot
diff --git a/tests/purs/passing/3429/chrismshelton.purs b/tests/purs/passing/3429/chrismshelton.purs
new file mode 100644
index 0000000000..db224762d0
--- /dev/null
+++ b/tests/purs/passing/3429/chrismshelton.purs
@@ -0,0 +1,28 @@
+-- Example submitted by chrismshelton.
+-- Cf. failing/3429-chrismshelton.purs
+module ChrisMShelton where
+
+import Prelude
+
+class CA v a where
+  lengthA :: forall m . v m a -> Int
+
+class (CA w a) <= CB v w a | v a -> w, w a -> v where
+  lengthB :: v a -> Int
+  fromA :: forall m . w m a -> v a
+  toA   :: forall m . v a -> w m a
+
+defaultLengthB :: forall v w a . (CB v w a) => v a -> Int
+defaultLengthB v = lengthA $ toA v
+
+data DA m a = DA Int
+
+data DB a = DB Int
+
+instance caDA :: CA DA a where
+  lengthA (DA i) = i
+
+instance cbDB :: (CA DA a) => CB DB DA a where
+  lengthB x = defaultLengthB x
+  fromA (DA a) = (DB a)
+  toA (DB a) = (DA a)
diff --git a/tests/purs/passing/3429/nukisman.purs b/tests/purs/passing/3429/nukisman.purs
new file mode 100644
index 0000000000..c65c266858
--- /dev/null
+++ b/tests/purs/passing/3429/nukisman.purs
@@ -0,0 +1,19 @@
+-- Example submitted by nukisman in issue #2975.
+-- Cf. failing/3429-nukisman.purs
+module Nukisman where
+
+import Data.Foldable (class Foldable, foldrDefault, foldMapDefaultL)
+
+data Tree a
+  = Leaf
+  | Branch (Tree a) a (Tree a)
+
+instance foldableTree :: Foldable Tree where
+  foldl _ acc Leaf = acc
+  foldl f acc (Branch l e r) = acc -- Just for debug
+  foldr f = foldrDefault f
+  foldMap = foldMapDefaultL
+
+-- NOTE: `foldMap` doesn't need to be eta-expanded
+-- because, during elaboration, the `Monoid` constraint of `foldMapDefaultL`
+-- is transformed into an `Abs` node, which suppresses cycle checking.
diff --git a/tests/purs/passing/365.purs b/tests/purs/passing/365.purs
new file mode 100644
index 0000000000..81095de115
--- /dev/null
+++ b/tests/purs/passing/365.purs
@@ -0,0 +1,15 @@
+-- Cf. 3429/*.purs and failing/365.purs
+module Main where
+
+import Prelude
+import Effect.Console (log)
+
+class C a where
+  f :: a -> a
+  g :: a -> a
+
+instance cS :: C String where
+  f s = s
+  g s = f s
+
+main = log "Done"
diff --git a/tests/purs/passing/Foldable.purs b/tests/purs/passing/Foldable.purs
new file mode 100644
index 0000000000..6d2b1d24ea
--- /dev/null
+++ b/tests/purs/passing/Foldable.purs
@@ -0,0 +1,20 @@
+-- Cf. failing/Foldable.purs and 3429/*.purs
+module Main where
+
+import Prelude
+import Effect.Console (log)
+
+class Foldable f where
+  fold :: forall a b. (a -> b -> b) -> b -> f a -> b
+  size :: forall a. f a -> Number
+
+data L a = C a (L a) | N
+
+instance foldableL :: Foldable L where
+  fold _ z N = z
+  fold f z (C x xs) = x `f` (fold f z xs)
+  size i = fold (const ((+) 1.0)) 0.0 i
+
+x = size (C 1 (C 2 (C 3 N)))
+
+main = log "Done"
diff --git a/tests/purs/passing/MissingEtaExpansion.purs b/tests/purs/passing/MissingEtaExpansion.purs
new file mode 100644
index 0000000000..0a41d78046
--- /dev/null
+++ b/tests/purs/passing/MissingEtaExpansion.purs
@@ -0,0 +1,9 @@
+-- Cf. UnifyInTypeInstanceLookup.purs and failing/MissingEtaExpanson.purs
+module Main where
+
+import Effect.Console (log)
+
+f :: Int -> Int
+f i = f i
+
+main = log "Done"