diff --git a/CHANGELOG.d/fix_4196.md b/CHANGELOG.d/fix_4196.md
new file mode 100644
index 0000000000..75d783332d
--- /dev/null
+++ b/CHANGELOG.d/fix_4196.md
@@ -0,0 +1 @@
+* Support solving constraints of values where a polymorphic type was matched.
diff --git a/src/Language/PureScript/TypeChecker/Types.hs b/src/Language/PureScript/TypeChecker/Types.hs
index c0c37d042f..fd4c944d65 100644
--- a/src/Language/PureScript/TypeChecker/Types.hs
+++ b/src/Language/PureScript/TypeChecker/Types.hs
@@ -710,7 +710,8 @@ check' v@(Var _ var) ty = do
   checkVisibility var
   repl <- introduceSkolemScope <=< replaceAllTypeSynonyms <=< lookupVariable $ var
   ty' <- introduceSkolemScope <=< replaceAllTypeSynonyms <=< replaceTypeWildcards $ ty
-  elaborate <- subsumes repl ty'
+  currentSubst <- gets checkSubstitution
+  elaborate <- subsumes (substituteType currentSubst repl) ty'
   return $ TypedValue' True (elaborate v) ty'
 check' (DeferredDictionary className tys) ty = do
   {-
diff --git a/tests/purs/failing/3765.out b/tests/purs/failing/3765.out
index 1ae4deb72f..18af4c50f9 100644
--- a/tests/purs/failing/3765.out
+++ b/tests/purs/failing/3765.out
@@ -4,31 +4,32 @@ at tests/purs/failing/3765.purs:6:23 - 6:24 (line 6, column 23 - line 6, column
 
   Could not match type
               
-    ( b :: Int
+    ( a :: Int
     ...       
     | t0      
     )         
               
   with type
               
-    ( a :: Int
+    ( b :: Int
     ...       
     | t0      
     )         
               
 
-while trying to match type { b :: Int
-                           | t0      
-                           }         
-  with type t1
+while checking that type { a :: Int
+                         | t0      
+                         }         
+  is at least as general as type { b :: Int
+                                 | t0      
+                                 }         
 while checking that expression x
   has type { b :: Int
            | t0      
            }         
 in value declaration mkTricky
 
-where t1 is an unknown type
-      t0 is an unknown type
+where t0 is an unknown type
 
 See https://github.com/purescript/documentation/blob/master/errors/TypesDoNotUnify.md for more information,
 or to contribute content related to this error.
diff --git a/tests/purs/failing/SuggestComposition.out b/tests/purs/failing/SuggestComposition.out
index a588608250..d1886b3189 100644
--- a/tests/purs/failing/SuggestComposition.out
+++ b/tests/purs/failing/SuggestComposition.out
@@ -14,7 +14,7 @@ at tests/purs/failing/SuggestComposition.purs:7:5 - 7:6 (line 7, column 5 - line
 while trying to match type { g :: t0
                            | t1     
                            }        
-  with type t2 -> t3
+  with type Int -> Int
 while checking that expression g
   has type { g :: t0
            | t1     
@@ -22,9 +22,7 @@ while checking that expression g
 while checking type of property accessor g.g
 in value declaration f
 
-where t2 is an unknown type
-      t3 is an unknown type
-      t0 is an unknown type
+where t0 is an unknown type
       t1 is an unknown type
 
 See https://github.com/purescript/documentation/blob/master/errors/TypesDoNotUnify.md for more information,
diff --git a/tests/purs/passing/BoundVariableSubsumption.purs b/tests/purs/passing/BoundVariableSubsumption.purs
new file mode 100644
index 0000000000..d4f593fd14
--- /dev/null
+++ b/tests/purs/passing/BoundVariableSubsumption.purs
@@ -0,0 +1,14 @@
+module Main where
+
+import Prelude
+import Effect.Console (log)
+
+class Con
+
+newtype Identity a = Identity a
+
+test :: Con => Identity (Con => Int) -> Int
+test (Identity a) = a
+
+main = do
+  log "Done"