Unwrap casts before checking vars in eager unifier

Previously, checking whether (tv |> co) ~ (tv |> co) got deferred,
because we looked for vars before stripping casts. (The left type
would get stripped, and then tv ~ (tv |> co) would scare the occurs-
checker.)

This opportunity for improvement presented itself in other work.
This is just an optimization. Some programs can now report more
errors simultaneously.

7 files changed, 146 insertions, 63 deletions

diff --git a/testsuite/tests/partial-sigs/should_fail/T12634.stderr b/testsuite/tests/partial-sigs/should_fail/T12634.stderr
index dd661a9355..316f7eb2c5 100644
--- a/testsuite/tests/partial-sigs/should_fail/T12634.stderr
+++ b/testsuite/tests/partial-sigs/should_fail/T12634.stderr
@@ -15,3 +15,17 @@ T12634.hs:14:58: error:
       In the type signature:
         bench_twacePow :: forall t m m' r.
                           _ => t m' r -> Bench '(t, m, m', r)
+
+T12634.hs:15:18: error:
+    • Couldn't match kind ‘(* -> * -> *, *, *, *)’ with ‘*’
+      When matching types
+        params0 :: *
+        '(t, m, m', r) :: (* -> * -> *, *, *, *)
+      Expected type: t m' r -> Bench '(t, m, m', r)
+        Actual type: t m' r -> Bench params0
+    • In the expression: bench (twacePowDec :: t m' r -> t m r)
+      In an equation for ‘bench_twacePow’:
+          bench_twacePow = bench (twacePowDec :: t m' r -> t m r)
+    • Relevant bindings include
+        bench_twacePow :: t m' r -> Bench '(t, m, m', r)
+          (bound at T12634.hs:15:1)
diff --git a/testsuite/tests/partial-sigs/should_fail/T14040a.stderr b/testsuite/tests/partial-sigs/should_fail/T14040a.stderr
index c0e0664a06..b9318940fd 100644
--- a/testsuite/tests/partial-sigs/should_fail/T14040a.stderr
+++ b/testsuite/tests/partial-sigs/should_fail/T14040a.stderr
@@ -1,41 +1,4 @@
 
-T14040a.hs:21:18: error:
-    • Couldn't match type ‘a’ with ‘k0’
-      ‘a’ is a rigid type variable bound by
-        the type signature for:
-          elimWeirdList :: forall a1 (wl :: WeirdList a1) (p :: forall x.
-                                                                x -> WeirdList x -> *).
-                           Sing wl
-                           -> (forall y. p k0 w0 'WeirdNil)
-                           -> (forall z1 (x :: z1) (xs :: WeirdList (WeirdList z1)).
-                               Sing x
-                               -> Sing xs -> p (WeirdList k1) w1 xs -> p k1 w2 ('WeirdCons x xs))
-                           -> p k2 w3 wl
-        at T14040a.hs:(21,18)-(28,23)
-      Expected type: Sing wl
-                     -> (forall y. p k1 w0 'WeirdNil)
-                     -> (forall z1 (x :: z1) (xs :: WeirdList (WeirdList z1)).
-                         Sing x
-                         -> Sing xs -> p (WeirdList k0) w1 xs -> p k0 w2 ('WeirdCons x xs))
-                     -> p k2 w3 wl
-        Actual type: Sing wl
-                     -> (forall y. p k1 w0 'WeirdNil)
-                     -> (forall z1 (x :: z1) (xs :: WeirdList (WeirdList z1)).
-                         Sing x
-                         -> Sing xs -> p (WeirdList k0) w1 xs -> p k0 w2 ('WeirdCons x xs))
-                     -> p k2 w3 wl
-    • In the ambiguity check for ‘elimWeirdList’
-      To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
-      In the type signature:
-        elimWeirdList :: forall (a :: Type)
-                                (wl :: WeirdList a)
-                                (p :: forall (x :: Type). x -> WeirdList x -> Type).
-                         Sing wl
-                         -> (forall (y :: Type). p _ WeirdNil)
-                            -> (forall (z :: Type) (x :: z) (xs :: WeirdList (WeirdList z)).
-                                Sing x -> Sing xs -> p _ xs -> p _ (WeirdCons x xs))
-                               -> p _ wl
-
 T14040a.hs:34:8: error:
     • Cannot apply expression of type ‘Sing wl
                                        -> (forall y. p k0 w0 'WeirdNil)
diff --git a/testsuite/tests/partial-sigs/should_fail/T14584.stderr b/testsuite/tests/partial-sigs/should_fail/T14584.stderr
index c53c822ba3..f4f1887f4d 100644
--- a/testsuite/tests/partial-sigs/should_fail/T14584.stderr
+++ b/testsuite/tests/partial-sigs/should_fail/T14584.stderr
@@ -1,26 +1,58 @@
 
 T14584.hs:56:41: warning: [-Wdeferred-type-errors (in -Wdefault)]
-    • Could not deduce (SingI a) arising from a use of ‘sing’
+    • Could not deduce: m1 ~ Type
       from the context: (Action act, Monoid a, Good m1)
         bound by the instance declaration at T14584.hs:54:10-89
+      ‘m1’ is a rigid type variable bound by
+        the instance declaration
+        at T14584.hs:54:10-89
+      When matching types
+        a :: Type
+        a0 :: m
+      Expected type: Sing a0
+        Actual type: Sing a
     • In the second argument of ‘fromSing’, namely
         ‘(sing @m @a :: Sing _)’
       In the fourth argument of ‘act’, namely
         ‘(fromSing @m (sing @m @a :: Sing _))’
       In the expression:
         act @_ @_ @act (fromSing @m (sing @m @a :: Sing _))
+    • Relevant bindings include
+        monHom :: a -> a (bound at T14584.hs:56:3)
 
-T14584.hs:56:50: warning: [-Wdeferred-type-errors (in -Wdefault)]
-    • Expected kind ‘m1’, but ‘a’ has kind ‘Type’
-    • In the type ‘a’
-      In the second argument of ‘fromSing’, namely
+T14584.hs:56:41: warning: [-Wdeferred-type-errors (in -Wdefault)]
+    • Could not deduce: a ~~ a0
+      from the context: (Action act, Monoid a, Good m1)
+        bound by the instance declaration at T14584.hs:54:10-89
+      ‘a’ is a rigid type variable bound by
+        the instance declaration
+        at T14584.hs:54:10-89
+      Expected type: Sing a0
+        Actual type: Sing a
+    • In the second argument of ‘fromSing’, namely
         ‘(sing @m @a :: Sing _)’
       In the fourth argument of ‘act’, namely
         ‘(fromSing @m (sing @m @a :: Sing _))’
+      In the expression:
+        act @_ @_ @act (fromSing @m (sing @m @a :: Sing _))
+    • Relevant bindings include
+        monHom :: a -> a (bound at T14584.hs:56:3)
+
+T14584.hs:56:41: warning: [-Wdeferred-type-errors (in -Wdefault)]
+    • Could not deduce (SingI a) arising from a use of ‘sing’
+      from the context: (Action act, Monoid a, Good m1)
+        bound by the instance declaration at T14584.hs:54:10-89
+    • In the second argument of ‘fromSing’, namely
+        ‘(sing @m @a :: Sing _)’
+      In the fourth argument of ‘act’, namely
+        ‘(fromSing @m (sing @m @a :: Sing _))’
+      In the expression:
+        act @_ @_ @act (fromSing @m (sing @m @a :: Sing _))
 
 T14584.hs:56:60: warning: [-Wpartial-type-signatures (in -Wdefault)]
-    • Found type wildcard ‘_’ standing for ‘a :: m’
-      Where: ‘a’, ‘m’ are rigid type variables bound by
+    • Found type wildcard ‘_’ standing for ‘a0 :: m’
+      Where: ‘a0’ is an ambiguous type variable
+             ‘m’ is a rigid type variable bound by
                the instance declaration
                at T14584.hs:54:10-89
     • In an expression type signature: Sing _
diff --git a/testsuite/tests/polykinds/T12593.stderr b/testsuite/tests/polykinds/T12593.stderr
index 3e63159057..43f762221e 100644
--- a/testsuite/tests/polykinds/T12593.stderr
+++ b/testsuite/tests/polykinds/T12593.stderr
@@ -10,7 +10,8 @@ T12593.hs:12:31: error:
     • Expecting one more argument to ‘k’
       Expected a type, but
       ‘k’ has kind
-      ‘(((k0 -> k1 -> *) -> Constraint) -> k2 -> *) -> Constraint’
+      ‘(((k0 -> k1 -> *) -> Constraint) -> (k2 -> k3 -> *) -> *)
+       -> Constraint’
     • In the kind ‘k’
       In the type signature:
         run :: k2 q =>
@@ -21,21 +22,65 @@ T12593.hs:12:40: error:
     • Expecting two more arguments to ‘k1’
       Expected a type, but
       ‘k1’ has kind
-      ‘((k0 -> k1 -> *) -> Constraint) -> k2 -> *’
+      ‘((k0 -> k1 -> *) -> Constraint) -> (k2 -> k3 -> *) -> *’
     • In the kind ‘k1’
       In the type signature:
         run :: k2 q =>
                Free k k1 k2 p a b
                -> (forall (c :: k) (d :: k1). p c d -> q c d) -> q a b
 
-T12593.hs:12:54: error:
-    • Couldn't match kind ‘((k0 -> k1 -> *) -> Constraint) -> k2 -> *’
+T12593.hs:12:47: error:
+    • Couldn't match kind ‘(((k0 -> k1 -> *) -> Constraint)
+                            -> (k2 -> k3 -> *) -> *)
+                           -> Constraint’
+                     with ‘*’
+      When matching kinds
+        k2 :: *
+        k :: (((k0 -> k1 -> *) -> Constraint) -> (k2 -> k3 -> *) -> *)
+             -> Constraint
+    • In the first argument of ‘p’, namely ‘c’
+      In the type signature:
+        run :: k2 q =>
+               Free k k1 k2 p a b
+               -> (forall (c :: k) (d :: k1). p c d -> q c d) -> q a b
+
+T12593.hs:12:49: error:
+    • Couldn't match kind ‘((k0 -> k1 -> *) -> Constraint)
+                           -> (k2 -> k3 -> *) -> *’
+                     with ‘*’
+      When matching kinds
+        k3 :: *
+        k4 :: ((k0 -> k1 -> *) -> Constraint) -> (k2 -> k3 -> *) -> *
+    • In the second argument of ‘p’, namely ‘d’
+      In the type signature:
+        run :: k2 q =>
+               Free k k1 k2 p a b
+               -> (forall (c :: k) (d :: k1). p c d -> q c d) -> q a b
+
+T12593.hs:12:56: error:
+    • Couldn't match kind ‘(((k0 -> k1 -> *) -> Constraint)
+                            -> (k2 -> k3 -> *) -> *)
+                           -> Constraint’
+                     with ‘*’
+      When matching kinds
+        k0 :: *
+        k :: (((k0 -> k1 -> *) -> Constraint) -> (k2 -> k3 -> *) -> *)
+             -> Constraint
+    • In the first argument of ‘q’, namely ‘c’
+      In the type signature:
+        run :: k2 q =>
+               Free k k1 k2 p a b
+               -> (forall (c :: k) (d :: k1). p c d -> q c d) -> q a b
+
+T12593.hs:12:58: error:
+    • Couldn't match kind ‘((k0 -> k1 -> *) -> Constraint)
+                           -> (k2 -> k3 -> *) -> *’
                      with ‘*’
       When matching kinds
-        k3 :: ((k0 -> k1 -> *) -> Constraint) -> k2 -> *
         k1 :: *
-      Expected kind ‘k -> k3 -> *’, but ‘q’ has kind ‘k0 -> k1 -> *’
-    • In the type signature:
+        k4 :: ((k0 -> k1 -> *) -> Constraint) -> (k2 -> k3 -> *) -> *
+    • In the second argument of ‘q’, namely ‘d’
+      In the type signature:
         run :: k2 q =>
                Free k k1 k2 p a b
                -> (forall (c :: k) (d :: k1). p c d -> q c d) -> q a b
diff --git a/testsuite/tests/polykinds/T14846.stderr b/testsuite/tests/polykinds/T14846.stderr
index 1bfa94218c..3abdb88d2f 100644
--- a/testsuite/tests/polykinds/T14846.stderr
+++ b/testsuite/tests/polykinds/T14846.stderr
@@ -3,11 +3,11 @@ T14846.hs:38:8: error:
     • Couldn't match type ‘ríki’ with ‘Hom riki’
       ‘ríki’ is a rigid type variable bound by
         the type signature for:
-          i :: forall k5 (cls1 :: k5
-                                  -> Constraint) k6 (xx :: k6) (a :: Struct cls1) (ríki :: Struct
-                                                                                             cls1
+          i :: forall k5 (cls2 :: k5
+                                  -> Constraint) k6 (xx :: k6) (a :: Struct cls2) (ríki :: Struct
+                                                                                             cls2
                                                                                            -> Struct
-                                                                                                cls1
+                                                                                                cls2
                                                                                            -> *).
                StructI xx a =>
                ríki a a
@@ -30,11 +30,18 @@ T14846.hs:38:8: error:
                       ríki a a
       In the instance declaration for ‘Category (Hom riki)’
 
-T14846.hs:39:44: error:
-    • Expected kind ‘Struct cls0 -> Constraint’,
-        but ‘cls’ has kind ‘k4 -> Constraint’
-    • In the second argument of ‘Structured’, namely ‘cls’
-      In the first argument of ‘AStruct’, namely ‘(Structured a cls)’
+T14846.hs:39:31: error:
+    • Couldn't match kind ‘k4’ with ‘Struct cls0’
+      ‘k4’ is a rigid type variable bound by
+        the instance declaration
+        at T14846.hs:37:10-65
+      When matching kinds
+        cls :: k4 -> Constraint
+        cls1 :: Struct cls0 -> Constraint
+      Expected kind ‘Struct cls1’,
+        but ‘Structured a cls’ has kind ‘Struct cls’
+    • In the first argument of ‘AStruct’, namely ‘(Structured a cls)’
       In an expression type signature: AStruct (Structured a cls)
+      In the expression: struct :: AStruct (Structured a cls)
     • Relevant bindings include
         i :: Hom riki a a (bound at T14846.hs:39:3)
diff --git a/testsuite/tests/typecheck/should_compile/T2494.stderr b/testsuite/tests/typecheck/should_compile/T2494.stderr
index 4a9d3c0978..5cf4fde746 100644
--- a/testsuite/tests/typecheck/should_compile/T2494.stderr
+++ b/testsuite/tests/typecheck/should_compile/T2494.stderr
@@ -20,11 +20,11 @@ T2494.hs:15:14: error:
         x :: Maybe a (bound at T2494.hs:14:65)
 
 T2494.hs:15:30: error:
-    • Couldn't match type ‘a’ with ‘b’
-      ‘a’ is a rigid type variable bound by
+    • Couldn't match type ‘b’ with ‘a’
+      ‘b’ is a rigid type variable bound by
         the RULE "foo/foo"
         at T2494.hs:(12,1)-(15,33)
-      ‘b’ is a rigid type variable bound by
+      ‘a’ is a rigid type variable bound by
         the RULE "foo/foo"
         at T2494.hs:(12,1)-(15,33)
       Expected type: Maybe (m b) -> Maybe (m a)
diff --git a/testsuite/tests/typecheck/should_fail/VtaFail.stderr b/testsuite/tests/typecheck/should_fail/VtaFail.stderr
index a9958016ce..6cb1f442a7 100644
--- a/testsuite/tests/typecheck/should_fail/VtaFail.stderr
+++ b/testsuite/tests/typecheck/should_fail/VtaFail.stderr
@@ -25,6 +25,17 @@ VtaFail.hs:26:15: error:
       In the expression: first @Int F
       In an equation for ‘fInt’: fInt = first @Int F
 
+VtaFail.hs:26:19: error:
+    • Couldn't match kind ‘*’ with ‘* -> *’
+      When matching types
+        a1 :: * -> *
+        Int :: *
+      Expected type: First Int
+        Actual type: First a1
+    • In the second argument of ‘first’, namely ‘F’
+      In the expression: first @Int F
+      In an equation for ‘fInt’: fInt = first @Int F
+
 VtaFail.hs:33:18: error:
     • Couldn't match type ‘Int’ with ‘Bool’
       Expected type: Proxy Bool
@@ -39,6 +50,17 @@ VtaFail.hs:40:17: error:
       In the expression: too @Maybe T
       In an equation for ‘threeBad’: threeBad = too @Maybe T
 
+VtaFail.hs:40:23: error:
+    • Couldn't match kind ‘*’ with ‘k0 -> *’
+      When matching types
+        a0 :: * -> k0 -> *
+        Maybe :: * -> *
+      Expected type: Three Maybe
+        Actual type: Three a0
+    • In the second argument of ‘too’, namely ‘T’
+      In the expression: too @Maybe T
+      In an equation for ‘threeBad’: threeBad = too @Maybe T
+
 VtaFail.hs:41:27: error:
     • Couldn't match type ‘Either’ with ‘(->)’
       Expected type: Three (->)