From 9cf5ed93418e499bdc054e6cde3b2088fdde917f Mon Sep 17 00:00:00 2001
From: Joseph Young <jy14898@my.bristol.ac.uk>
Date: Mon, 1 Nov 2021 17:20:37 +0000
Subject: [PATCH 1/3] Fix

---
 src/Language/PureScript/TypeChecker/Types.hs    |  3 ++-
 tests/purs/failing/3765.out                     | 17 +++++++++--------
 tests/purs/failing/SuggestComposition.out       |  6 ++----
 .../purs/passing/BoundVariableSubsumption.purs  | 14 ++++++++++++++
 4 files changed, 27 insertions(+), 13 deletions(-)
 create mode 100644 tests/purs/passing/BoundVariableSubsumption.purs

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..77842a2e1d
--- /dev/null
+++ b/tests/purs/passing/BoundVariableSubsumption.purs
@@ -0,0 +1,14 @@
+module Main where
+
+import Prelude
+import Effect.Console (log)
+
+class Con
+
+data Identity a = Identity a
+
+test :: Con => Identity (Con => Int) -> Int
+test (Identity a) = a
+
+main = do
+  log "Done"

From aa63ffda578d03a804ef69af623261980174e0f9 Mon Sep 17 00:00:00 2001
From: Joseph Young <jy14898@my.bristol.ac.uk>
Date: Mon, 1 Nov 2021 17:25:14 +0000
Subject: [PATCH 2/3] Use newtype for Identity

---
 tests/purs/passing/BoundVariableSubsumption.purs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tests/purs/passing/BoundVariableSubsumption.purs b/tests/purs/passing/BoundVariableSubsumption.purs
index 77842a2e1d..d4f593fd14 100644
--- a/tests/purs/passing/BoundVariableSubsumption.purs
+++ b/tests/purs/passing/BoundVariableSubsumption.purs
@@ -5,7 +5,7 @@ import Effect.Console (log)
 
 class Con
 
-data Identity a = Identity a
+newtype Identity a = Identity a
 
 test :: Con => Identity (Con => Int) -> Int
 test (Identity a) = a

From 13e3d2b9938778f66ec2bcb2dc73568eabc08856 Mon Sep 17 00:00:00 2001
From: Joseph Young <jy14898@my.bristol.ac.uk>
Date: Mon, 1 Nov 2021 17:33:29 +0000
Subject: [PATCH 3/3] Update changelog

---
 CHANGELOG.d/fix_4196.md | 1 +
 1 file changed, 1 insertion(+)
 create mode 100644 CHANGELOG.d/fix_4196.md

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.