Simple subsumptionwip/T17775

This patch simplifies GHC to use simple subsumption.
  Ticket #17775

Implements GHC proposal #287
   https://github.com/ghc-proposals/ghc-proposals/blob/master/
   proposals/0287-simplify-subsumption.rst

All the motivation is described there; I will not repeat it here.
The implementation payload:
 * tcSubType and friends become noticably simpler, because it no
   longer uses eta-expansion when checking subsumption.
 * No deeplyInstantiate or deeplySkolemise

That in turn means that some tests fail, by design; they can all
be fixed by eta expansion.  There is a list of such changes below.

Implementing the patch led me into a variety of sticky corners, so
the patch includes several othe changes, some quite significant:

* I made String wired-in, so that
    "foo" :: String   rather than
    "foo" :: [Char]
  This improves error messages, and fixes #15679

* The pattern match checker relies on knowing about in-scope equality
  constraints, andd adds them to the desugarer's environment using
  addTyCsDs.  But the co_fn in a FunBind was missed, and for some reason
  simple-subsumption ends up with dictionaries there. So I added a
  call to addTyCsDs.  This is really part of #18049.

* I moved the ic_telescope field out of Implication and into
  ForAllSkol instead.  This is a nice win; just expresses the code
  much better.

* There was a bug in GHC.Tc.TyCl.Instance.tcDataFamInstHeader.
  We called checkDataKindSig inside tc_kind_sig, /before/
  solveEqualities and zonking.  Obviously wrong, easily fixed.

* solveLocalEqualitiesX: there was a whole mess in here, around
  failing fast enough.  I discovered a bad latent bug where we
  could successfully kind-check a type signature, and use it,
  but have unsolved constraints that could fill in coercion
  holes in that signature --  aargh.

  It's all explained in Note [Failure in local type signatures]
  in GHC.Tc.Solver. Much better now.

* I fixed a serious bug in anonymous type holes. IN
    f :: Int -> (forall a. a -> _) -> Int
  that "_" should be a unification variable at the /outer/
  level; it cannot be instantiated to 'a'.  This was plain
  wrong.  New fields mode_lvl and mode_holes in TcTyMode,
  and auxiliary data type GHC.Tc.Gen.HsType.HoleMode.

  This fixes #16292, but makes no progress towards the more
  ambitious #16082

* I got sucked into an enormous refactoring of the reporting of
  equality errors in GHC.Tc.Errors, especially in
      mkEqErr1
      mkTyVarEqErr
      misMatchMsg
      misMatchMsgOrCND
  In particular, the very tricky mkExpectedActualMsg function
  is gone.

  It took me a full day.  But the result is far easier to understand.
  (Still not easy!)  This led to various minor improvements in error
  output, and an enormous number of test-case error wibbles.

  One particular point: for occurs-check errors I now just say
     Can't match 'a' against '[a]'
  rather than using the intimidating language of "occurs check".

* Pretty-printing AbsBinds

Tests review

* Eta expansions
   T11305: one eta expansion
   T12082: one eta expansion (undefined)
   T13585a: one eta expansion
   T3102:  one eta expansion
   T3692:  two eta expansions (tricky)
   T2239:  two eta expansions
   T16473: one eta
   determ004: two eta expansions (undefined)
   annfail06: two eta (undefined)
   T17923: four eta expansions (a strange program indeed!)
   tcrun035: one eta expansion

* Ambiguity check at higher rank.  Now that we have simple
  subsumption, a type like
     f :: (forall a. Eq a => Int) -> Int
  is no longer ambiguous, because we could write
     g :: (forall a. Eq a => Int) -> Int
     g = f
  and it'd typecheck just fine.  But f's type is a bit
  suspicious, and we might want to consider making the
  ambiguity check do a check on each sub-term.  Meanwhile,
  these tests are accepted, whereas they were previously
  rejected as ambiguous:
     T7220a
     T15438
     T10503
     T9222

* Some more interesting error message wibbles
   T13381: Fine: one error (Int ~ Exp Int)
           rather than two (Int ~ Exp Int, Exp Int ~ Int)
   T9834:  Small change in error (improvement)
   T10619: Improved
   T2414:  Small change, due to order of unification, fine
   T2534:  A very simple case in which a change of unification order
           means we get tow unsolved constraints instead of one
   tc211: bizarre impredicative tests; just accept this for now

Updates Cabal and haddock submodules.

Metric Increase:
  T12150
  T12234
  T5837
  haddock.base
Metric Decrease:
  haddock.compiler
  haddock.Cabal
  haddock.base

Merge note: This appears to break the
`UnliftedNewtypesDifficultUnification` test. It has been marked as
broken in the interest of merging.

(cherry picked from commit 66b7b195cb3dce93ed5078b80bf568efae904cc5)

46 files changed, 324 insertions, 214 deletions

diff --git a/testsuite/tests/typecheck/should_compile/FD3.stderr b/testsuite/tests/typecheck/should_compile/FD3.stderr
index 85728da0a6..d7ac728b6c 100644
--- a/testsuite/tests/typecheck/should_compile/FD3.stderr
+++ b/testsuite/tests/typecheck/should_compile/FD3.stderr
@@ -1,9 +1,13 @@
 
 FD3.hs:15:15: error:
-    • Occurs check: cannot construct the infinite type: a ~ (String, a)
+    • Couldn't match type ‘a’ with ‘(String, a)’
         arising from a functional dependency between:
           constraint ‘MkA (String, a) a’ arising from a use of ‘mkA’
           instance ‘MkA a1 a1’ at FD3.hs:12:10-16
+      ‘a’ is a rigid type variable bound by
+        the type signature for:
+          translate :: forall a. (String, a) -> A a
+        at FD3.hs:14:1-31
     • In the expression: mkA a
       In an equation for ‘translate’: translate a = mkA a
     • Relevant bindings include
diff --git a/testsuite/tests/typecheck/should_compile/T10072.stderr b/testsuite/tests/typecheck/should_compile/T10072.stderr
index ad7fe2602a..71a93c9573 100644
--- a/testsuite/tests/typecheck/should_compile/T10072.stderr
+++ b/testsuite/tests/typecheck/should_compile/T10072.stderr
@@ -6,5 +6,5 @@ T10072.hs:3:31: error:
                at T10072.hs:3:1-47
       To use the inferred type, enable PartialTypeSignatures
     • In the type ‘a -> _’
-      In a RULE for ‘f’: a -> _
+      In the type signature for ‘f’: a -> _
       When checking the transformation rule "map/empty"
diff --git a/testsuite/tests/typecheck/should_compile/T10283.hs b/testsuite/tests/typecheck/should_compile/T10283.hs
index e623b1cb0a..8c5b8e2f5a 100644
--- a/testsuite/tests/typecheck/should_compile/T10283.hs
+++ b/testsuite/tests/typecheck/should_compile/T10283.hs
@@ -20,4 +20,4 @@ wrapIdComp f = runIdComp . f . liftOuter
 
 class Applicative p => ApplicativeFix p where
   afix :: (forall q. Applicative q => (Comp p q) a -> (Comp p q) a) -> p a
-  afix = wrapIdComp
+  afix f = wrapIdComp f
diff --git a/testsuite/tests/typecheck/should_compile/T10390.hs b/testsuite/tests/typecheck/should_compile/T10390.hs
index e0648c9554..facb26a26d 100644
--- a/testsuite/tests/typecheck/should_compile/T10390.hs
+++ b/testsuite/tests/typecheck/should_compile/T10390.hs
@@ -6,7 +6,7 @@ class ApPair r where
   apPair :: (forall a . (ApPair a, Num a) => Maybe a) -> Maybe r
 
 instance (ApPair a, ApPair b) => ApPair (a,b) where
-  apPair = apPair'
+  apPair x = apPair' x
 
 apPair' :: (ApPair b, ApPair c)
         => (forall a . (Num a, ApPair a) => Maybe a) -> Maybe (b,c)
diff --git a/testsuite/tests/typecheck/should_compile/T11254.stderr b/testsuite/tests/typecheck/should_compile/T11254.stderr
index a7466b78b9..10132d2cb8 100644
--- a/testsuite/tests/typecheck/should_compile/T11254.stderr
+++ b/testsuite/tests/typecheck/should_compile/T11254.stderr
@@ -6,8 +6,8 @@ T11254.hs:16:10: warning: [-Wdeferred-type-errors (in -Wdefault)]
 
 T11254.hs:18:12: warning: [-Wdeferred-type-errors (in -Wdefault)]
     • Couldn't match type ‘GHC.Real.Ratio Integer’ with ‘Int’
-      Expected type: Rational -> Frac Rational
-        Actual type: Rational -> Rational
+      Expected: Rational -> Frac Rational
+        Actual: Rational -> Rational
     • When checking that instance signature for ‘embed’
         is more general than its signature in the class
         Instance sig: Rational -> Rational
diff --git a/testsuite/tests/typecheck/should_compile/T11305.hs b/testsuite/tests/typecheck/should_compile/T11305.hs
index 14cb955ed5..ee138a017c 100644
--- a/testsuite/tests/typecheck/should_compile/T11305.hs
+++ b/testsuite/tests/typecheck/should_compile/T11305.hs
@@ -54,4 +54,5 @@ instance ProfunctorComonad Tambara where
       yon    ~(x,~(y,z)) = ((x,y),z)
 
 instance Profunctor p => Strong (Tambara p) where
-  first' = runTambara . produplicate
+  first' = (\x -> runTambara x) . produplicate
+  -- Simple subsumption (#17775) requires eta expansion here
diff --git a/testsuite/tests/typecheck/should_compile/T12082.hs b/testsuite/tests/typecheck/should_compile/T12082.hs
index 7aa4196737..0f001beabb 100644
--- a/testsuite/tests/typecheck/should_compile/T12082.hs
+++ b/testsuite/tests/typecheck/should_compile/T12082.hs
@@ -6,4 +6,5 @@ import Data.Typeable (Typeable)
 import Control.Monad.ST (RealWorld)
 
 f :: forall a. (forall b. Typeable b => b -> a) -> a
-f = undefined :: (RealWorld -> a) -> a
+f x = (undefined :: (RealWorld -> a) -> a) x
+  -- Simple subsumption (#17775) requires eta expansion here
diff --git a/testsuite/tests/typecheck/should_compile/T12427a.hs b/testsuite/tests/typecheck/should_compile/T12427a.hs
index cffab89749..56c7513012 100644
--- a/testsuite/tests/typecheck/should_compile/T12427a.hs
+++ b/testsuite/tests/typecheck/should_compile/T12427a.hs
@@ -36,5 +36,6 @@ h2 y = case y of T1 _ v -> v
 -- Fails in 7.10  (head exploded)
 -- Fails in 8.0.1 (ditto)
 -- Succeeds in 8.2
+-- Fails in 8.12 (simple subsumption)
 x3 :: (forall a. a->a) -> Int
 T1 _ x3 = undefined
diff --git a/testsuite/tests/typecheck/should_compile/T12427a.stderr b/testsuite/tests/typecheck/should_compile/T12427a.stderr
index efc87a1fc3..b9c3969bf0 100644
--- a/testsuite/tests/typecheck/should_compile/T12427a.stderr
+++ b/testsuite/tests/typecheck/should_compile/T12427a.stderr
@@ -12,8 +12,19 @@ T12427a.hs:17:29: error:
         h11 :: T -> p (bound at T12427a.hs:17:1)
 
 T12427a.hs:28:6: error:
-    • Cannot instantiate unification variable ‘p0’
+    • Couldn't match expected type ‘p0’
+                  with actual type ‘(forall b. [b] -> [b]) -> Int’
+      Cannot instantiate unification variable ‘p0’
       with a type involving polytypes: (forall b. [b] -> [b]) -> Int
-        GHC doesn't yet support impredicative polymorphism
     • In the pattern: T1 _ x1
       In a pattern binding: T1 _ x1 = undefined
+
+T12427a.hs:41:6: error:
+    • Couldn't match type ‘b’ with ‘[b]’
+      Expected: (forall b. [b] -> [b]) -> Int
+        Actual: (forall a. a -> a) -> Int
+      ‘b’ is a rigid type variable bound by
+        the type [b] -> [b]
+        at T12427a.hs:41:1-19
+    • In the pattern: T1 _ x3
+      In a pattern binding: T1 _ x3 = undefined
diff --git a/testsuite/tests/typecheck/should_compile/T13381.stderr b/testsuite/tests/typecheck/should_compile/T13381.stderr
index 9c8eab6e67..7f250eaec1 100644
--- a/testsuite/tests/typecheck/should_compile/T13381.stderr
+++ b/testsuite/tests/typecheck/should_compile/T13381.stderr
@@ -1,14 +1,8 @@
 
 T13381.hs:21:23: error:
     • Couldn't match type ‘Exp Int’ with ‘Int’
-      Expected type: Exp Int -> Iter (Exp Int) (Exp Char)
-        Actual type: Int -> Iter (Exp Int) (Exp Char)
+      Expected: Int -> Iter Int (Exp Char)
+        Actual: Int -> Iter (Exp Int) (Exp Char)
     • In the first argument of ‘iterLoop’, namely ‘f’
       In the first argument of ‘fromExp’, namely ‘(iterLoop f init)’
       In the expression: fromExp (iterLoop f init)
-
-T13381.hs:21:25: error:
-    • Couldn't match expected type ‘Exp Int’ with actual type ‘Int’
-    • In the second argument of ‘iterLoop’, namely ‘init’
-      In the first argument of ‘fromExp’, namely ‘(iterLoop f init)’
-      In the expression: fromExp (iterLoop f init)
diff --git a/testsuite/tests/typecheck/should_compile/T13585a.hs b/testsuite/tests/typecheck/should_compile/T13585a.hs
index 0652ece370..3f72a45ea3 100644
--- a/testsuite/tests/typecheck/should_compile/T13585a.hs
+++ b/testsuite/tests/typecheck/should_compile/T13585a.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE KindSignatures, RankNTypes, TypeFamilies, MultiParamTypeClasses, FlexibleInstances,UndecidableInstances #-}
+{-# LANGUAGE ScopedTypeVariables, KindSignatures, RankNTypes, TypeFamilies, MultiParamTypeClasses, FlexibleInstances,UndecidableInstances #-}
 
 module T13585a where
 
@@ -78,5 +78,6 @@ au k = withIso k $ \ sa bt f -> fmap sa (f bt)
 {-# INLINE au #-}
 
 ala :: (Functor f, Rewrapping s t) => (Unwrapped s -> s) -> ((Unwrapped t -> t) -> f s) -> f (Unwrapped s)
-ala = au . _Wrapping
+ala = au . (\x -> _Wrapping x)
+  -- Simple subsumption (#17775) requires eta expansion here
 {-# INLINE ala #-}
diff --git a/testsuite/tests/typecheck/should_compile/T13651.stderr b/testsuite/tests/typecheck/should_compile/T13651.stderr
index 6b6c64302f..150291c210 100644
--- a/testsuite/tests/typecheck/should_compile/T13651.stderr
+++ b/testsuite/tests/typecheck/should_compile/T13651.stderr
@@ -8,6 +8,12 @@ T13651.hs:11:8: error:
                           (F cr cu ~ Bar h (Bar r u), F cu cs ~ Bar (Foo h) (Bar u s)) =>
                           Bar h (Bar r u) -> Bar (Foo h) (Bar u s) -> Foo (cr -> cs)
         at T13651.hs:(11,8)-(13,65)
+      Expected: forall cr cu h r u cs s.
+                (F cr cu ~ Bar h (Bar r u), F cu cs ~ Bar (Foo h) (Bar u s)) =>
+                Bar h (Bar r u) -> Bar (Foo h) (Bar u s) -> Foo (cr -> cs)
+        Actual: forall cr cu h r u cs s.
+                (F cr cu ~ Bar h (Bar r u), F cu cs ~ Bar (Foo h) (Bar u s)) =>
+                Bar h (Bar r u) -> Bar (Foo h) (Bar u s) -> Foo (cr -> cs)
     • In the ambiguity check for ‘foo’
       To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
       In the type signature:
diff --git a/testsuite/tests/typecheck/should_compile/T14488.hs b/testsuite/tests/typecheck/should_compile/T14488.hs
index a4a12841b7..04c295b706 100644
--- a/testsuite/tests/typecheck/should_compile/T14488.hs
+++ b/testsuite/tests/typecheck/should_compile/T14488.hs
@@ -7,4 +7,4 @@ type Lens' s a = forall f. Functor f => (a -> f a) -> s -> f s
 data T a = MkT { _tfield :: Eq a => a }
 
 tfield :: Eq a => Lens' (T a) a
-tfield f t = MkT <$> f (_tfield t)
+tfield f t = (\x -> MkT x) <$> f (_tfield t)
diff --git a/testsuite/tests/typecheck/should_compile/T15368.stderr b/testsuite/tests/typecheck/should_compile/T15368.stderr
index 693779e1f5..7f022744c4 100644
--- a/testsuite/tests/typecheck/should_compile/T15368.stderr
+++ b/testsuite/tests/typecheck/should_compile/T15368.stderr
@@ -15,9 +15,10 @@ T15368.hs:11:15: warning: [-Wtyped-holes (in -Wdefault)]
         trigger :: a -> b -> (F a b, F b a) (bound at T15368.hs:11:1)
 
 T15368.hs:11:15: warning: [-Wdeferred-type-errors (in -Wdefault)]
-    • Couldn't match type ‘F b a’ with ‘F b0 a0’
-      Expected type: (F a b, F b a)
-        Actual type: (F a b, F b0 a0)
+    • Couldn't match type: F b a
+                     with: F b0 a0
+      Expected: (F a b, F b a)
+        Actual: (F a b, F b0 a0)
       NB: ‘F’ is a non-injective type family
       The type variables ‘b0’, ‘a0’ are ambiguous
     • In the expression: _ `transitive` trigger _ _
diff --git a/testsuite/tests/typecheck/should_compile/T15370.stderr b/testsuite/tests/typecheck/should_compile/T15370.stderr
index ec0ff67482..f359155dbd 100644
--- a/testsuite/tests/typecheck/should_compile/T15370.stderr
+++ b/testsuite/tests/typecheck/should_compile/T15370.stderr
@@ -1,6 +1,8 @@
 
 T15370.hs:14:10: warning: [-Wdeferred-type-errors (in -Wdefault)]
     • Couldn't match type ‘n’ with ‘j’
+      Expected: n :~: j
+        Actual: n :~: n
       ‘n’ is a rigid type variable bound by
         the type signature for:
           mkRefl :: forall {k} (n :: k) (j :: k). n :~: j
@@ -9,8 +11,6 @@ T15370.hs:14:10: warning: [-Wdeferred-type-errors (in -Wdefault)]
         the type signature for:
           mkRefl :: forall {k} (n :: k) (j :: k). n :~: j
         at T15370.hs:13:1-17
-      Expected type: n :~: j
-        Actual type: n :~: n
     • In the expression: Refl
       In an equation for ‘mkRefl’: mkRefl = Refl
     • Relevant bindings include
@@ -18,8 +18,8 @@ T15370.hs:14:10: warning: [-Wdeferred-type-errors (in -Wdefault)]
 
 T15370.hs:20:13: warning: [-Wdeferred-type-errors (in -Wdefault)]
     • Couldn't match type ‘S r’ with ‘()’
-      Expected type: ()
-        Actual type: S r
+      Expected: ()
+        Actual: S r
     • In the expression: no + _
       In a case alternative: Refl -> no + _
       In the expression: case mkRefl @x @y of { Refl -> no + _ }
diff --git a/testsuite/tests/typecheck/should_compile/T1634.hs b/testsuite/tests/typecheck/should_compile/T1634.hs
index b4c6f2b561..a8fdd9f8eb 100644
--- a/testsuite/tests/typecheck/should_compile/T1634.hs
+++ b/testsuite/tests/typecheck/should_compile/T1634.hs
@@ -3,4 +3,4 @@
 module T1634 where
 
 t1 :: a -> (forall b. b -> (a,b))
-t1 = (,)
+t1 x = (,) x
diff --git a/testsuite/tests/typecheck/should_compile/T17007.hs b/testsuite/tests/typecheck/should_compile/T17007.hs
index 21b7639dd0..0b2b0f28a2 100644
--- a/testsuite/tests/typecheck/should_compile/T17007.hs
+++ b/testsuite/tests/typecheck/should_compile/T17007.hs
@@ -10,4 +10,4 @@ get (x :: ItemColID a b) = x :: ItemColID a b
 type family ItemColID' a b where ItemColID' a b = Int  -- Discards a,b
 
 get' :: ItemColID' a b -> ItemColID' a b
-get' (x :: ItemColID' a b) = x :: ItemColID' a b
+get' (x :: ItemColID' p q) = x :: ItemColID' a b
diff --git a/testsuite/tests/typecheck/should_compile/T17775-view-pats.hs b/testsuite/tests/typecheck/should_compile/T17775-view-pats.hs
new file mode 100644
index 0000000000..8ffd704d9c
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T17775-view-pats.hs
@@ -0,0 +1,52 @@
+{-# LANGUAGE RankNTypes, ViewPatterns #-}
+
+module ViewPats where
+
+ex1 :: forall a. a -> a -> Int -> Eq a => Bool
+-- Accept; we skolemise over three args
+ex1 x ((== x) -> result) _ = result
+
+{-
+ex2 :: forall a. a -> a -> Int -> Eq a => Bool
+-- Reject: only skolemise over two args
+ex2 x ((== x) -> result) = \ _ -> result
+
+ex3 :: forall a. a -> a -> Int -> Eq a => Bool
+-- Reject: only skolemise over two args
+--    const (result :: Bool) :: b -> Eq a => Bool
+ex3 x ((== x) -> result) = const result
+-}
+
+ex4 :: forall a. a -> a -> Int -> Eq a => Bool
+-- Accept
+ex4 x y _ = x == y
+
+ex5 :: forall a. a -> a -> Int -> Eq a => Bool
+-- Accept
+ex5 x y = \ _ -> x == y
+
+{-
+ex6 :: forall a. a -> a -> Int -> Eq a => Bool
+-- Reject. Needs (const (bla :: Bool)) :: Int -> Eq a => Bool
+ex6 x y = const (x == y)
+-}
+
+ex7 :: forall a. a -> a -> Eq a => Bool
+-- Accept
+ex7 x ((== x) -> result) = result
+
+ex8 :: forall a. a -> a -> Eq a => Bool
+-- Accept
+ex8 x y = x == y
+
+ex9 :: forall a. a -> Eq a => a -> Bool
+-- Accept
+ex9 x ((== x) -> result) = result
+
+ex10 :: forall a. a -> Eq a => a -> Bool
+-- Accept
+ex10 x y = x == y
+
+ex11 :: forall a. a -> Eq a => a -> Bool
+-- Accept
+ex11 x = (== x)
diff --git a/testsuite/tests/typecheck/should_compile/T17775-viewpats-a.hs b/testsuite/tests/typecheck/should_compile/T17775-viewpats-a.hs
new file mode 100644
index 0000000000..96deb25631
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T17775-viewpats-a.hs
@@ -0,0 +1,35 @@
+{-# LANGUAGE RankNTypes, ViewPatterns #-}
+
+module ViewPats where
+
+ex1 :: forall a. a -> a -> Int -> Eq a => Bool
+-- Accept; we skolemise over three args
+ex1 x ((== x) -> result) _ = result
+
+ex4 :: forall a. a -> a -> Int -> Eq a => Bool
+-- Accept
+ex4 x y _ = x == y
+
+ex5 :: forall a. a -> a -> Int -> Eq a => Bool
+-- Accept
+ex5 x y = \ _ -> x == y
+
+ex7 :: forall a. a -> a -> Eq a => Bool
+-- Accept
+ex7 x ((== x) -> result) = result
+
+ex8 :: forall a. a -> a -> Eq a => Bool
+-- Accept
+ex8 x y = x == y
+
+ex9 :: forall a. a -> Eq a => a -> Bool
+-- Accept
+ex9 x ((== x) -> result) = result
+
+ex10 :: forall a. a -> Eq a => a -> Bool
+-- Accept
+ex10 x y = x == y
+
+ex11 :: forall a. a -> Eq a => a -> Bool
+-- Accept
+ex11 x = (== x)
diff --git a/testsuite/tests/typecheck/should_compile/T17775-viewpats-b.hs b/testsuite/tests/typecheck/should_compile/T17775-viewpats-b.hs
new file mode 100644
index 0000000000..18a6ec8da6
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T17775-viewpats-b.hs
@@ -0,0 +1,7 @@
+{-# LANGUAGE RankNTypes, ViewPatterns #-}
+
+module ViewPats where
+
+ex2 :: forall a. a -> a -> Int -> Eq a => Bool
+-- Reject: only skolemise over two args
+ex2 x ((== x) -> result) = \ _ -> result
diff --git a/testsuite/tests/typecheck/should_compile/T17775-viewpats-b.stderr b/testsuite/tests/typecheck/should_compile/T17775-viewpats-b.stderr
new file mode 100644
index 0000000000..e631106dd0
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T17775-viewpats-b.stderr
@@ -0,0 +1,10 @@
+
+T17775-viewpats-b.hs:7:9: error:
+    • No instance for (Eq a) arising from a use of ‘==’
+      Possible fix:
+        add (Eq a) to the context of
+          the type signature for:
+            ex2 :: forall a. a -> a -> Int -> Eq a => Bool
+    • In the expression: == x
+      In the pattern: (== x) -> result
+      In an equation for ‘ex2’: ex2 x ((== x) -> result) = \ _ -> result
diff --git a/testsuite/tests/typecheck/should_compile/T17775-viewpats-c.hs b/testsuite/tests/typecheck/should_compile/T17775-viewpats-c.hs
new file mode 100644
index 0000000000..78b4e9d0b5
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T17775-viewpats-c.hs
@@ -0,0 +1,8 @@
+{-# LANGUAGE RankNTypes, ViewPatterns #-}
+
+module ViewPats where
+
+ex3 :: forall a. a -> a -> Int -> Eq a => Bool
+-- Reject: only skolemise over two args
+--    const (result :: Bool) :: b -> Eq a => Bool
+ex3 x ((== x) -> result) = const result
diff --git a/testsuite/tests/typecheck/should_compile/T17775-viewpats-c.stderr b/testsuite/tests/typecheck/should_compile/T17775-viewpats-c.stderr
new file mode 100644
index 0000000000..a0456c5a70
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T17775-viewpats-c.stderr
@@ -0,0 +1,11 @@
+
+T17775-viewpats-c.hs:8:28: error:
+    • Couldn't match type ‘Bool’ with ‘Eq a => Bool’
+      Expected: Int -> Eq a => Bool
+        Actual: Int -> Bool
+    • In the expression: const result
+      In an equation for ‘ex3’: ex3 x ((== x) -> result) = const result
+    • Relevant bindings include
+        x :: a (bound at T17775-viewpats-c.hs:8:5)
+        ex3 :: a -> a -> Int -> Eq a => Bool
+          (bound at T17775-viewpats-c.hs:8:1)
diff --git a/testsuite/tests/typecheck/should_compile/T17775-viewpats-d.hs b/testsuite/tests/typecheck/should_compile/T17775-viewpats-d.hs
new file mode 100644
index 0000000000..3a133d7930
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T17775-viewpats-d.hs
@@ -0,0 +1,7 @@
+{-# LANGUAGE RankNTypes, ViewPatterns #-}
+
+module ViewPats where
+
+ex6 :: forall a. a -> a -> Int -> Eq a => Bool
+-- Reject. Needs (const (bla :: Bool)) :: Int -> Eq a => Bool
+ex6 x y = const (x == y)
diff --git a/testsuite/tests/typecheck/should_compile/T17775-viewpats-d.stderr b/testsuite/tests/typecheck/should_compile/T17775-viewpats-d.stderr
new file mode 100644
index 0000000000..e270cecc25
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T17775-viewpats-d.stderr
@@ -0,0 +1,12 @@
+
+T17775-viewpats-d.hs:7:11: error:
+    • Couldn't match type ‘Bool’ with ‘Eq a => Bool’
+      Expected: Int -> Eq a => Bool
+        Actual: Int -> Bool
+    • In the expression: const (x == y)
+      In an equation for ‘ex6’: ex6 x y = const (x == y)
+    • Relevant bindings include
+        y :: a (bound at T17775-viewpats-d.hs:7:7)
+        x :: a (bound at T17775-viewpats-d.hs:7:5)
+        ex6 :: a -> a -> Int -> Eq a => Bool
+          (bound at T17775-viewpats-d.hs:7:1)
diff --git a/testsuite/tests/typecheck/should_compile/T2494.stderr b/testsuite/tests/typecheck/should_compile/T2494.stderr
index 5cf4fde746..8e427c5ac8 100644
--- a/testsuite/tests/typecheck/should_compile/T2494.stderr
+++ b/testsuite/tests/typecheck/should_compile/T2494.stderr
@@ -1,14 +1,14 @@
 
 T2494.hs:15:14: error:
     • Couldn't match type ‘b’ with ‘a’
+      Expected: Maybe (m a) -> Maybe (m a)
+        Actual: Maybe (m b) -> Maybe (m b)
       ‘b’ is a rigid type variable bound by
         the RULE "foo/foo"
         at T2494.hs:(12,1)-(15,33)
       ‘a’ is a rigid type variable bound by
         the RULE "foo/foo"
         at T2494.hs:(12,1)-(15,33)
-      Expected type: Maybe (m a) -> Maybe (m a)
-        Actual type: Maybe (m b) -> Maybe (m b)
     • In the first argument of ‘foo’, namely ‘g’
       In the second argument of ‘foo’, namely ‘(foo g x)’
       In the expression: foo f (foo g x)
@@ -21,14 +21,14 @@ T2494.hs:15:14: error:
 
 T2494.hs:15:30: error:
     • Couldn't match type ‘b’ with ‘a’
+      Expected: Maybe (m b) -> Maybe (m a)
+        Actual: Maybe (m b) -> Maybe (m b)
       ‘b’ is a rigid type variable bound by
         the RULE "foo/foo"
         at T2494.hs:(12,1)-(15,33)
       ‘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)
-        Actual type: Maybe (m b) -> Maybe (m b)
     • In the second argument of ‘(.)’, namely ‘g’
       In the first argument of ‘foo’, namely ‘(f . g)’
       In the expression: foo (f . g) x
diff --git a/testsuite/tests/typecheck/should_compile/T3692.hs b/testsuite/tests/typecheck/should_compile/T3692.hs
index 5be093f55f..4d5a61074f 100644
--- a/testsuite/tests/typecheck/should_compile/T3692.hs
+++ b/testsuite/tests/typecheck/should_compile/T3692.hs
@@ -7,5 +7,8 @@ type Foo a b = () -> (Bar a => a)
 
 class Bar a where {}
 
+boo :: Foo p q
+boo x = undefined
+
 foo :: Foo a b
-foo = id (undefined :: Foo p q)
+foo y = id (\x -> boo x) y
diff --git a/testsuite/tests/typecheck/should_compile/T4284.hs b/testsuite/tests/typecheck/should_compile/T4284.hs
index 2d5164a487..5e1b9ceb5f 100644
--- a/testsuite/tests/typecheck/should_compile/T4284.hs
+++ b/testsuite/tests/typecheck/should_compile/T4284.hs
@@ -2,11 +2,11 @@
 module Test where
 
 foo :: () -> forall b. b
-foo = undefined
+foo x = undefined
 
-works = id foo
+works = id (\x -> foo x)
 
-fails = (id) foo
+fails = (id) (\x -> foo x)
 
 -- works type checks, but fails fails with the following error
 -- message:
diff --git a/testsuite/tests/typecheck/should_compile/T7220a.hs b/testsuite/tests/typecheck/should_compile/T7220a.hs
index 4739626fa5..2ea0150f29 100644
--- a/testsuite/tests/typecheck/should_compile/T7220a.hs
+++ b/testsuite/tests/typecheck/should_compile/T7220a.hs
@@ -23,5 +23,7 @@ f :: (forall b. (C a b, TF b ~ Y) => b) -> X
 --               g = f
 -- Now we fail in all ways!
 
-f _ = undefined
+-- But with simple subsumption (#17775) we
+-- no longer get an ambiguity check here
 
+f _ = undefined
diff --git a/testsuite/tests/typecheck/should_compile/T7220a.stderr b/testsuite/tests/typecheck/should_compile/T7220a.stderr
deleted file mode 100644
index 2b311c1111..0000000000
--- a/testsuite/tests/typecheck/should_compile/T7220a.stderr
+++ /dev/null
@@ -1,14 +0,0 @@
-
-T7220a.hs:17:6: error:
-    • Could not deduce (C a b)
-      from the context: (C a0 b, TF b ~ Y)
-        bound by a type expected by the context:
-                   forall b. (C a0 b, TF b ~ Y) => b
-        at T7220a.hs:17:6-44
-      Possible fix:
-        add (C a b) to the context of
-          a type expected by the context:
-            forall b. (C a0 b, TF b ~ Y) => b
-    • In the ambiguity check for ‘f’
-      To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
-      In the type signature: f :: (forall b. (C a b, TF b ~ Y) => b) -> X
diff --git a/testsuite/tests/typecheck/should_compile/T9569a.hs b/testsuite/tests/typecheck/should_compile/T9569a.hs
index 3205cb1b4e..0eeb4c40a7 100644
--- a/testsuite/tests/typecheck/should_compile/T9569a.hs
+++ b/testsuite/tests/typecheck/should_compile/T9569a.hs
@@ -5,7 +5,7 @@ g :: (Int -> Int) -> Int
 g f = f 4
 
 f1 :: (forall a. a -> a) -> Int
+-- Fails; needs eta-expansion
+-- cf T9569b
 f1 = g
 
-f2 :: (forall a. a -> a) -> Int
-f2 x = g x
diff --git a/testsuite/tests/typecheck/should_compile/T9569a.stderr b/testsuite/tests/typecheck/should_compile/T9569a.stderr
new file mode 100644
index 0000000000..57d44a0f2a
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T9569a.stderr
@@ -0,0 +1,8 @@
+
+T9569a.hs:10:6: error:
+    • Couldn't match type: Int -> Int
+                     with: forall a. a -> a
+      Expected: (forall a. a -> a) -> Int
+        Actual: (Int -> Int) -> Int
+    • In the expression: g
+      In an equation for ‘f1’: f1 = g
diff --git a/testsuite/tests/typecheck/should_compile/T9569b.hs b/testsuite/tests/typecheck/should_compile/T9569b.hs
new file mode 100644
index 0000000000..67ddf21d73
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T9569b.hs
@@ -0,0 +1,8 @@
+{-# LANGUAGE RankNTypes #-}
+module T9569a where
+
+g :: (Int -> Int) -> Int
+g f = f 4
+
+f2 :: (forall a. a -> a) -> Int
+f2 f = g f
diff --git a/testsuite/tests/typecheck/should_compile/T9834.hs b/testsuite/tests/typecheck/should_compile/T9834.hs
index c16e395f8c..728de2b8ed 100644
--- a/testsuite/tests/typecheck/should_compile/T9834.hs
+++ b/testsuite/tests/typecheck/should_compile/T9834.hs
@@ -20,4 +20,4 @@ wrapIdComp f = runIdComp . f . liftOuter
 
 class Applicative p => ApplicativeFix p where
   afix :: (forall q. Applicative q => (Comp p q) a -> (Comp p q) a) -> p a
-  afix = wrapIdComp
\ No newline at end of file
+  afix f = wrapIdComp f
diff --git a/testsuite/tests/typecheck/should_compile/T9834.stderr b/testsuite/tests/typecheck/should_compile/T9834.stderr
index 52f207d511..5963781325 100644
--- a/testsuite/tests/typecheck/should_compile/T9834.stderr
+++ b/testsuite/tests/typecheck/should_compile/T9834.stderr
@@ -1,40 +1,46 @@
 
-T9834.hs:23:10: warning: [-Wdeferred-type-errors (in -Wdefault)]
-    • Occurs check: cannot construct the infinite type: p ~ (->) (p a0)
-      Expected type: (forall (q :: * -> *).
-                      Applicative q =>
-                      Comp p q a -> Comp p q a)
-                     -> p a
-        Actual type: (forall (q :: * -> *).
-                      Applicative q =>
-                      Nat (Comp p q) (Comp p q))
-                     -> p a0 -> p a0
-    • In the expression: wrapIdComp
-      In an equation for ‘afix’: afix = wrapIdComp
+T9834.hs:23:12: warning: [-Wdeferred-type-errors (in -Wdefault)]
+    • Couldn't match type ‘p’ with ‘(->) (p a0)’
+      Expected: p a
+        Actual: p a0 -> p a0
+      ‘p’ is a rigid type variable bound by
+        the class declaration for ‘ApplicativeFix’
+        at T9834.hs:21:39
+    • In the expression: wrapIdComp f
+      In an equation for ‘afix’: afix f = wrapIdComp f
     • Relevant bindings include
+        f :: forall (q :: * -> *).
+             Applicative q =>
+             Comp p q a -> Comp p q a
+          (bound at T9834.hs:23:8)
         afix :: (forall (q :: * -> *).
                  Applicative q =>
                  Comp p q a -> Comp p q a)
                 -> p a
           (bound at T9834.hs:23:3)
 
-T9834.hs:23:10: warning: [-Wdeferred-type-errors (in -Wdefault)]
+T9834.hs:23:23: warning: [-Wdeferred-type-errors (in -Wdefault)]
     • Couldn't match type ‘a1’ with ‘a’
+      Expected: Comp p q a1 -> Comp p q a1
+        Actual: Comp p q a -> Comp p q a
       ‘a1’ is a rigid type variable bound by
         a type expected by the context:
           forall (q :: * -> *). Applicative q => Nat (Comp p q) (Comp p q)
-        at T9834.hs:23:10-19
+        at T9834.hs:23:23
       ‘a’ is a rigid type variable bound by
         the type signature for:
           afix :: forall a.
                   (forall (q :: * -> *). Applicative q => Comp p q a -> Comp p q a)
                   -> p a
         at T9834.hs:22:11-74
-      Expected type: Comp p q a1 -> Comp p q a1
-        Actual type: Comp p q a -> Comp p q a
-    • In the expression: wrapIdComp
-      In an equation for ‘afix’: afix = wrapIdComp
+    • In the first argument of ‘wrapIdComp’, namely ‘f’
+      In the expression: wrapIdComp f
+      In an equation for ‘afix’: afix f = wrapIdComp f
     • Relevant bindings include
+        f :: forall (q :: * -> *).
+             Applicative q =>
+             Comp p q a -> Comp p q a
+          (bound at T9834.hs:23:8)
         afix :: (forall (q :: * -> *).
                  Applicative q =>
                  Comp p q a -> Comp p q a)
diff --git a/testsuite/tests/typecheck/should_compile/UnliftedNewtypesUnifySig.hs b/testsuite/tests/typecheck/should_compile/UnliftedNewtypesUnifySig.hs
index 9f5b984025..a7645a0b3e 100644
--- a/testsuite/tests/typecheck/should_compile/UnliftedNewtypesUnifySig.hs
+++ b/testsuite/tests/typecheck/should_compile/UnliftedNewtypesUnifySig.hs
@@ -14,7 +14,10 @@ import GHC.Exts (Int#,Word#,RuntimeRep(IntRep))
 import GHC.Exts (TYPE)
 
 type KindOf (a :: TYPE k) = k
+
 data family D (a :: TYPE r) :: TYPE r
+
 newtype instance D a = MkWordD Word#
+
 newtype instance D a :: TYPE (KindOf a) where
   MkIntD :: forall (a :: TYPE 'IntRep). Int# -> D a
diff --git a/testsuite/tests/typecheck/should_compile/abstract_refinement_hole_fits.stderr b/testsuite/tests/typecheck/should_compile/abstract_refinement_hole_fits.stderr
index e422b8629e..119c6b91e5 100644
--- a/testsuite/tests/typecheck/should_compile/abstract_refinement_hole_fits.stderr
+++ b/testsuite/tests/typecheck/should_compile/abstract_refinement_hole_fits.stderr
@@ -42,29 +42,29 @@ abstract_refinement_hole_fits.hs:4:5: warning: [-Wtyped-holes (in -Wdefault)]
           where pure :: forall (f :: * -> *) a. Applicative f => a -> f a
         ($!) (_ :: [Integer] -> Integer)
           where ($!) :: forall a b. (a -> b) -> a -> b
-        curry (_ :: (a2, [Integer]) -> Integer) (_ :: a2)
+        curry (_ :: (t0, [Integer]) -> Integer) (_ :: t0)
           where curry :: forall a b c. ((a, b) -> c) -> a -> b -> c
         (.) (_ :: b1 -> Integer) (_ :: [Integer] -> b1)
           where (.) :: forall b c a. (b -> c) -> (a -> b) -> a -> c
-        flip (_ :: [Integer] -> b7 -> Integer) (_ :: b7)
+        flip (_ :: [Integer] -> t0 -> Integer) (_ :: t0)
           where flip :: forall a b c. (a -> b -> c) -> b -> a -> c
-        (>>=) (_ :: [Integer] -> a11) (_ :: a11 -> [Integer] -> Integer)
+        (>>=) (_ :: [Integer] -> a8) (_ :: a8 -> [Integer] -> Integer)
           where (>>=) :: forall (m :: * -> *) a b.
                          Monad m =>
                          m a -> (a -> m b) -> m b
-        (>>) (_ :: [Integer] -> a10) (_ :: [Integer] -> Integer)
+        (>>) (_ :: [Integer] -> a7) (_ :: [Integer] -> Integer)
           where (>>) :: forall (m :: * -> *) a b.
                         Monad m =>
                         m a -> m b -> m b
-        fmap (_ :: a12 -> Integer) (_ :: [Integer] -> a12)
+        fmap (_ :: a9 -> Integer) (_ :: [Integer] -> a9)
           where fmap :: forall (f :: * -> *) a b.
                         Functor f =>
                         (a -> b) -> f a -> f b
-        (<*>) (_ :: [Integer] -> a8 -> Integer) (_ :: [Integer] -> a8)
+        (<*>) (_ :: [Integer] -> a5 -> Integer) (_ :: [Integer] -> a5)
           where (<*>) :: forall (f :: * -> *) a b.
                          Applicative f =>
                          f (a -> b) -> f a -> f b
-        (*>) (_ :: [Integer] -> a7) (_ :: [Integer] -> Integer)
+        (*>) (_ :: [Integer] -> a4) (_ :: [Integer] -> Integer)
           where (*>) :: forall (f :: * -> *) a b.
                         Applicative f =>
                         f a -> f b -> f b
@@ -72,7 +72,7 @@ abstract_refinement_hole_fits.hs:4:5: warning: [-Wtyped-holes (in -Wdefault)]
           where (<$>) :: forall (f :: * -> *) a b.
                          Functor f =>
                          (a -> b) -> f a -> f b
-        (=<<) (_ :: a9 -> [Integer] -> Integer) (_ :: [Integer] -> a9)
+        (=<<) (_ :: a6 -> [Integer] -> Integer) (_ :: [Integer] -> a6)
           where (=<<) :: forall (m :: * -> *) a b.
                          Monad m =>
                          (a -> m b) -> m a -> m b
@@ -84,15 +84,15 @@ abstract_refinement_hole_fits.hs:4:5: warning: [-Wtyped-holes (in -Wdefault)]
           where (<$) :: forall (f :: * -> *) a b.
                         Functor f =>
                         a -> f b -> f a
-        id (_ :: t1 -> [Integer] -> Integer) (_ :: t1)
+        id (_ :: t0 -> [Integer] -> Integer) (_ :: t0)
           where id :: forall a. a -> a
-        head (_ :: [t1 -> [Integer] -> Integer]) (_ :: t1)
+        head (_ :: [t0 -> [Integer] -> Integer]) (_ :: t0)
           where head :: forall a. [a] -> a
-        last (_ :: [t1 -> [Integer] -> Integer]) (_ :: t1)
+        last (_ :: [t0 -> [Integer] -> Integer]) (_ :: t0)
           where last :: forall a. [a] -> a
-        fst (_ :: (t1 -> [Integer] -> Integer, b2)) (_ :: t1)
+        fst (_ :: (t0 -> [Integer] -> Integer, b2)) (_ :: t0)
           where fst :: forall a b. (a, b) -> a
-        snd (_ :: (a3, t1 -> [Integer] -> Integer)) (_ :: t1)
+        snd (_ :: (a2, t0 -> [Integer] -> Integer)) (_ :: t0)
           where snd :: forall a b. (a, b) -> b
         id (_ :: [Integer] -> Integer)
           where id :: forall a. a -> a
@@ -108,19 +108,19 @@ abstract_refinement_hole_fits.hs:4:5: warning: [-Wtyped-holes (in -Wdefault)]
           where fst :: forall a b. (a, b) -> a
         snd (_ :: (a0, [Integer] -> Integer))
           where snd :: forall a b. (a, b) -> b
-        const (_ :: [Integer] -> Integer) (_ :: b6)
+        const (_ :: [Integer] -> Integer) (_ :: t0)
           where const :: forall a b. a -> b -> a
-        seq (_ :: a13) (_ :: [Integer] -> Integer)
+        seq (_ :: t2) (_ :: [Integer] -> Integer)
           where seq :: forall a b. a -> b -> b
-        ($) (_ :: a5 -> [Integer] -> Integer) (_ :: a5)
+        ($) (_ :: t0 -> [Integer] -> Integer) (_ :: t0)
           where ($) :: forall a b. (a -> b) -> a -> b
-        return (_ :: [Integer] -> Integer) (_ :: t1)
+        return (_ :: [Integer] -> Integer) (_ :: t0)
           where return :: forall (m :: * -> *) a. Monad m => a -> m a
-        pure (_ :: [Integer] -> Integer) (_ :: t1)
+        pure (_ :: [Integer] -> Integer) (_ :: t0)
           where pure :: forall (f :: * -> *) a. Applicative f => a -> f a
-        uncurry (_ :: a4 -> b3 -> [Integer] -> Integer) (_ :: (a4, b3))
+        uncurry (_ :: a3 -> b3 -> [Integer] -> Integer) (_ :: (a3, b3))
           where uncurry :: forall a b c. (a -> b -> c) -> (a, b) -> c
-        ($!) (_ :: a6 -> [Integer] -> Integer) (_ :: a6)
+        ($!) (_ :: t0 -> [Integer] -> Integer) (_ :: t0)
           where ($!) :: forall a b. (a -> b) -> a -> b
 
 abstract_refinement_hole_fits.hs:7:5: warning: [-Wtyped-holes (in -Wdefault)]
@@ -158,31 +158,31 @@ abstract_refinement_hole_fits.hs:7:5: warning: [-Wtyped-holes (in -Wdefault)]
           where pure :: forall (f :: * -> *) a. Applicative f => a -> f a
         ($!) (_ :: Integer -> [Integer] -> Integer)
           where ($!) :: forall a b. (a -> b) -> a -> b
-        curry (_ :: (a2, Integer) -> [Integer] -> Integer) (_ :: a2)
+        curry (_ :: (t0, Integer) -> [Integer] -> Integer) (_ :: t0)
           where curry :: forall a b c. ((a, b) -> c) -> a -> b -> c
         (.) (_ :: b1 -> [Integer] -> Integer) (_ :: Integer -> b1)
           where (.) :: forall b c a. (b -> c) -> (a -> b) -> a -> c
-        flip (_ :: Integer -> b7 -> [Integer] -> Integer) (_ :: b7)
+        flip (_ :: Integer -> t0 -> [Integer] -> Integer) (_ :: t0)
           where flip :: forall a b c. (a -> b -> c) -> b -> a -> c
-        (>>=) (_ :: Integer -> a11)
-              (_ :: a11 -> Integer -> [Integer] -> Integer)
+        (>>=) (_ :: Integer -> a8)
+              (_ :: a8 -> Integer -> [Integer] -> Integer)
           where (>>=) :: forall (m :: * -> *) a b.
                          Monad m =>
                          m a -> (a -> m b) -> m b
-        (>>) (_ :: Integer -> a10) (_ :: Integer -> [Integer] -> Integer)
+        (>>) (_ :: Integer -> a7) (_ :: Integer -> [Integer] -> Integer)
           where (>>) :: forall (m :: * -> *) a b.
                         Monad m =>
                         m a -> m b -> m b
-        fmap (_ :: a12 -> [Integer] -> Integer) (_ :: Integer -> a12)
+        fmap (_ :: a9 -> [Integer] -> Integer) (_ :: Integer -> a9)
           where fmap :: forall (f :: * -> *) a b.
                         Functor f =>
                         (a -> b) -> f a -> f b
-        (<*>) (_ :: Integer -> a8 -> [Integer] -> Integer)
-              (_ :: Integer -> a8)
+        (<*>) (_ :: Integer -> a5 -> [Integer] -> Integer)
+              (_ :: Integer -> a5)
           where (<*>) :: forall (f :: * -> *) a b.
                          Applicative f =>
                          f (a -> b) -> f a -> f b
-        (*>) (_ :: Integer -> a7) (_ :: Integer -> [Integer] -> Integer)
+        (*>) (_ :: Integer -> a4) (_ :: Integer -> [Integer] -> Integer)
           where (*>) :: forall (f :: * -> *) a b.
                         Applicative f =>
                         f a -> f b -> f b
@@ -190,8 +190,8 @@ abstract_refinement_hole_fits.hs:7:5: warning: [-Wtyped-holes (in -Wdefault)]
           where (<$>) :: forall (f :: * -> *) a b.
                          Functor f =>
                          (a -> b) -> f a -> f b
-        (=<<) (_ :: a9 -> Integer -> [Integer] -> Integer)
-              (_ :: Integer -> a9)
+        (=<<) (_ :: a6 -> Integer -> [Integer] -> Integer)
+              (_ :: Integer -> a6)
           where (=<<) :: forall (m :: * -> *) a b.
                          Monad m =>
                          (a -> m b) -> m a -> m b
@@ -203,15 +203,15 @@ abstract_refinement_hole_fits.hs:7:5: warning: [-Wtyped-holes (in -Wdefault)]
           where (<$) :: forall (f :: * -> *) a b.
                         Functor f =>
                         a -> f b -> f a
-        id (_ :: t1 -> Integer -> [Integer] -> Integer) (_ :: t1)
+        id (_ :: t0 -> Integer -> [Integer] -> Integer) (_ :: t0)
           where id :: forall a. a -> a
-        head (_ :: [t1 -> Integer -> [Integer] -> Integer]) (_ :: t1)
+        head (_ :: [t0 -> Integer -> [Integer] -> Integer]) (_ :: t0)
           where head :: forall a. [a] -> a
-        last (_ :: [t1 -> Integer -> [Integer] -> Integer]) (_ :: t1)
+        last (_ :: [t0 -> Integer -> [Integer] -> Integer]) (_ :: t0)
           where last :: forall a. [a] -> a
-        fst (_ :: (t1 -> Integer -> [Integer] -> Integer, b2)) (_ :: t1)
+        fst (_ :: (t0 -> Integer -> [Integer] -> Integer, b2)) (_ :: t0)
           where fst :: forall a b. (a, b) -> a
-        snd (_ :: (a3, t1 -> Integer -> [Integer] -> Integer)) (_ :: t1)
+        snd (_ :: (a2, t0 -> Integer -> [Integer] -> Integer)) (_ :: t0)
           where snd :: forall a b. (a, b) -> b
         id (_ :: Integer -> [Integer] -> Integer)
           where id :: forall a. a -> a
@@ -228,18 +228,18 @@ abstract_refinement_hole_fits.hs:7:5: warning: [-Wtyped-holes (in -Wdefault)]
           where fst :: forall a b. (a, b) -> a
         snd (_ :: (a0, Integer -> [Integer] -> Integer))
           where snd :: forall a b. (a, b) -> b
-        const (_ :: Integer -> [Integer] -> Integer) (_ :: b6)
+        const (_ :: Integer -> [Integer] -> Integer) (_ :: t0)
           where const :: forall a b. a -> b -> a
-        seq (_ :: a13) (_ :: Integer -> [Integer] -> Integer)
+        seq (_ :: t2) (_ :: Integer -> [Integer] -> Integer)
           where seq :: forall a b. a -> b -> b
-        ($) (_ :: a5 -> Integer -> [Integer] -> Integer) (_ :: a5)
+        ($) (_ :: t0 -> Integer -> [Integer] -> Integer) (_ :: t0)
           where ($) :: forall a b. (a -> b) -> a -> b
-        return (_ :: Integer -> [Integer] -> Integer) (_ :: t1)
+        return (_ :: Integer -> [Integer] -> Integer) (_ :: t0)
           where return :: forall (m :: * -> *) a. Monad m => a -> m a
-        pure (_ :: Integer -> [Integer] -> Integer) (_ :: t1)
+        pure (_ :: Integer -> [Integer] -> Integer) (_ :: t0)
           where pure :: forall (f :: * -> *) a. Applicative f => a -> f a
-        uncurry (_ :: a4 -> b3 -> Integer -> [Integer] -> Integer)
-                (_ :: (a4, b3))
+        uncurry (_ :: a3 -> b3 -> Integer -> [Integer] -> Integer)
+                (_ :: (a3, b3))
           where uncurry :: forall a b c. (a -> b -> c) -> (a, b) -> c
-        ($!) (_ :: a6 -> Integer -> [Integer] -> Integer) (_ :: a6)
+        ($!) (_ :: t0 -> Integer -> [Integer] -> Integer) (_ :: t0)
           where ($!) :: forall a b. (a -> b) -> a -> b
diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T
index 3189595fc3..b4ac6c9916 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -422,7 +422,8 @@ test('TcStaticPointers02', normal, compile, [''])
 test('T8762', normal, compile, [''])
 test('MutRec', normal, compile, [''])
 test('T8856', normal, compile, [''])
-test('T9569a', normal, compile, [''])
+test('T9569a', normal, compile_fail, [''])
+test('T9569b', normal, compile, [''])
 test('T9117', normal, compile, [''])
 test('T9117_2', normal, compile, [''])
 test('T9117_3', normal, compile, [''])
@@ -430,7 +431,7 @@ test('T9708', expect_broken(9708), compile, [''])
 test('T9404', normal, compile, [''])
 test('T9404b', normal, compile, [''])
 test('T7220', normal, compile, [''])
-test('T7220a', normal, compile_fail, [''])
+test('T7220a', normal, compile, [''])
 test('T9151', normal, compile, [''])
 test('T9497a', normal, compile, ['-fdefer-typed-holes'])
 test('T9497b', normal, compile, ['-fdefer-typed-holes -fno-warn-typed-holes'])
@@ -684,7 +685,7 @@ test('UnliftedNewtypesUnifySig', normal, compile, [''])
 test('UnliftedNewtypesForall', normal, compile, [''])
 test('UnlifNewUnify', normal, compile, [''])
 test('UnliftedNewtypesLPFamily', normal, compile, [''])
-test('UnliftedNewtypesDifficultUnification', normal, compile, [''])
+test('UnliftedNewtypesDifficultUnification', when(compiler_debugged(), expect_broken(18300)), compile, [''])
 test('T16832', normal, ghci_script, ['T16832.script'])
 test('T16995', normal, compile, [''])
 test('T17007', normal, compile, [''])
@@ -711,3 +712,7 @@ test('T18129', expect_broken(18129), compile, [''])
 test('T18185', normal, compile, [''])
 test('ExplicitSpecificityA1', normal, compile, [''])
 test('ExplicitSpecificityA2', normal, compile, [''])
+test('T17775-viewpats-a', normal, compile, [''])
+test('T17775-viewpats-b', normal, compile_fail, [''])
+test('T17775-viewpats-c', normal, compile_fail, [''])
+test('T17775-viewpats-d', normal, compile_fail, [''])
diff --git a/testsuite/tests/typecheck/should_compile/subsumption_sort_hole_fits.stderr b/testsuite/tests/typecheck/should_compile/subsumption_sort_hole_fits.stderr
index eb4b02f34e..8ea32fcde6 100644
--- a/testsuite/tests/typecheck/should_compile/subsumption_sort_hole_fits.stderr
+++ b/testsuite/tests/typecheck/should_compile/subsumption_sort_hole_fits.stderr
@@ -1,6 +1,6 @@
 
 subsumption_sort_hole_fits.hs:2:5: warning: [-Wtyped-holes (in -Wdefault)]
-    • Found hole: _ :: [Char] -> [String]
+    • Found hole: _ :: String -> [String]
     • In the expression: _
       In the expression: _ "hello, world"
       In an equation for ‘f’: f = _ "hello, world"
@@ -22,7 +22,7 @@ subsumption_sort_hole_fits.hs:2:5: warning: [-Wtyped-holes (in -Wdefault)]
           (imported from ‘Prelude’ at subsumption_sort_hole_fits.hs:1:1
            (and originally defined in ‘GHC.List’))
         mempty :: forall a. Monoid a => a
-          with mempty @([Char] -> [String])
+          with mempty @(String -> [String])
           (imported from ‘Prelude’ at subsumption_sort_hole_fits.hs:1:1
            (and originally defined in ‘GHC.Base’))
         fail :: forall (m :: * -> *) a. MonadFail m => String -> m a
diff --git a/testsuite/tests/typecheck/should_compile/tc145.hs b/testsuite/tests/typecheck/should_compile/tc145.hs
index 8ab4a56321..9d1ada71a6 100644
--- a/testsuite/tests/typecheck/should_compile/tc145.hs
+++ b/testsuite/tests/typecheck/should_compile/tc145.hs
@@ -9,7 +9,7 @@ module ShouldCompile where
         -- implicit parameter to give
         --      r :: (?param::a) => a
     r :: Int -> ((?param :: a) => a)
-    r = error "urk"
+    r _ = error "urk"
 
         -- The unboxed tuple is OK because it is
         -- used on the right hand end of an arrow
diff --git a/testsuite/tests/typecheck/should_compile/tc160.hs b/testsuite/tests/typecheck/should_compile/tc160.hs
index 2425221aee..28e1b9e76b 100644
--- a/testsuite/tests/typecheck/should_compile/tc160.hs
+++ b/testsuite/tests/typecheck/should_compile/tc160.hs
@@ -7,8 +7,8 @@ module ShouldCompile where
 type Foo x = forall a. a -> x
 
 foo :: Foo (Foo ())
--- foo :: forall a b. a -> b -> ()
+-- foo :: forall a. a -> forall b. b -> ()
 --  NOT   forall a. a -> a -> ()
-foo =  undefined
+foo x = undefined
 
 baz = foo 'c' True
diff --git a/testsuite/tests/typecheck/should_compile/tc208.hs b/testsuite/tests/typecheck/should_compile/tc208.hs
index 8d9bb3636e..254eb82264 100644
--- a/testsuite/tests/typecheck/should_compile/tc208.hs
+++ b/testsuite/tests/typecheck/should_compile/tc208.hs
@@ -11,4 +11,4 @@ module ShouldCompile where
 type PPDoc = (?env :: Int) => Char
 
 f :: Char -> PPDoc
-f  = succ
+f x = succ x
diff --git a/testsuite/tests/typecheck/should_compile/tc210.hs b/testsuite/tests/typecheck/should_compile/tc210.hs
index b4a377f761..9a0de89d4e 100644
--- a/testsuite/tests/typecheck/should_compile/tc210.hs
+++ b/testsuite/tests/typecheck/should_compile/tc210.hs
@@ -3,10 +3,10 @@
 module ShouldCompile where
 
 f :: forall a. a -> forall b. b -> Int
-f = error "urk"
+f x = error "urk"
 
 -- Both these should be ok, but an early GHC 6.6 failed
 
-g1 = [ (+) :: Int -> Int -> Int, f ]
-g2 = [ f, (+) :: Int -> Int -> Int ]
+g1 = [ (+) :: Int -> Int -> Int, \x -> f x ]
+g2 = [ \x -> f x, (+) :: Int -> Int -> Int ]
 
diff --git a/testsuite/tests/typecheck/should_compile/tc211.stderr b/testsuite/tests/typecheck/should_compile/tc211.stderr
index ccc3da6fb0..bbffa16943 100644
--- a/testsuite/tests/typecheck/should_compile/tc211.stderr
+++ b/testsuite/tests/typecheck/should_compile/tc211.stderr
@@ -1,10 +1,11 @@
 
-tc211.hs:20:8: error:
-    • Couldn't match expected type ‘forall a. a -> a’
-                  with actual type ‘a9 -> a9’
-    • In the expression:
-          (:) ::
-            (forall a. a -> a) -> [forall a. a -> a] -> [forall a. a -> a]
+tc211.hs:21:17: error:
+    • Couldn't match expected type: a -> a
+                  with actual type: forall a. a -> a
+    • In the first argument of ‘(:) ::
+                                  (forall a. a -> a)
+                                  -> [forall a. a -> a] -> [forall a. a -> a]’, namely
+        ‘(head foo)’
       In the expression:
         ((:) ::
            (forall a. a -> a) -> [forall a. a -> a] -> [forall a. a -> a])
@@ -14,77 +15,3 @@ tc211.hs:20:8: error:
             = ((:) ::
                  (forall a. a -> a) -> [forall a. a -> a] -> [forall a. a -> a])
                 (head foo) foo
-
-tc211.hs:25:8: error:
-    • Couldn't match type ‘a1 -> a1’ with ‘forall a. a -> a’
-      Expected type: [forall a. a -> a]
-        Actual type: [a1 -> a1]
-    • In the expression: (head foo) : (tail foo)
-      In an equation for ‘barr’: barr = (head foo) : (tail foo)
-
-tc211.hs:25:20: error:
-    • Couldn't match type ‘forall a. a -> a’ with ‘a1 -> a1’
-      Expected type: [a1 -> a1]
-        Actual type: [forall a. a -> a]
-    • In the second argument of ‘(:)’, namely ‘(tail foo)’
-      In the expression: (head foo) : (tail foo)
-      In an equation for ‘barr’: barr = (head foo) : (tail foo)
-
-tc211.hs:62:18: error:
-    • Couldn't match expected type ‘forall a. a -> a’
-                  with actual type ‘a6 -> a6’
-    • In the expression:
-          Cons ::
-            (forall a. a -> a)
-            -> List (forall a. a -> a) -> List (forall a. a -> a)
-      In an equation for ‘cons’:
-          cons
-            = Cons ::
-                (forall a. a -> a)
-                -> List (forall a. a -> a) -> List (forall a. a -> a)
-      In the expression:
-        let
-          cons
-            = Cons ::
-                (forall a. a -> a)
-                -> List (forall a. a -> a) -> List (forall a. a -> a)
-        in cons (\ x -> x) Nil
-
-tc211.hs:68:8: error:
-    • Couldn't match expected type ‘forall a. a -> a’
-                  with actual type ‘a0 -> a0’
-    • In the expression:
-          Cons ::
-            ((forall a. a -> a)
-             -> List (forall a. a -> a) -> List (forall a. a -> a))
-      In the expression:
-        (Cons ::
-           ((forall a. a -> a)
-            -> List (forall a. a -> a) -> List (forall a. a -> a)))
-          (\ x -> x) Nil
-      In an equation for ‘xs2’:
-          xs2
-            = (Cons ::
-                 ((forall a. a -> a)
-                  -> List (forall a. a -> a) -> List (forall a. a -> a)))
-                (\ x -> x) Nil
-
-tc211.hs:76:9: error:
-    • Couldn't match type ‘forall a11. a11 -> a11’ with ‘a10 -> a10’
-      Expected type: List (forall a. a -> a)
-                     -> (forall a. a -> a) -> a10 -> a10
-        Actual type: List (a10 -> a10) -> (a10 -> a10) -> a10 -> a10
-    • In the expression:
-          foo2 ::
-            List (forall a. a -> a) -> (forall a. a -> a) -> (forall a. a -> a)
-      In the expression:
-        (foo2 ::
-           List (forall a. a -> a)
-           -> (forall a. a -> a) -> (forall a. a -> a))
-          xs1 (\ x -> x)
-      In an equation for ‘bar4’:
-          bar4
-            = (foo2 ::
-                 List (forall a. a -> a)
-                 -> (forall a. a -> a) -> (forall a. a -> a))
-                xs1 (\ x -> x)
diff --git a/testsuite/tests/typecheck/should_compile/twins.hs b/testsuite/tests/typecheck/should_compile/twins.hs
index 99c77aa796..31d967aa59 100644
--- a/testsuite/tests/typecheck/should_compile/twins.hs
+++ b/testsuite/tests/typecheck/should_compile/twins.hs
@@ -22,7 +22,7 @@ gzip f x y
     else Nothing
 
 gzipWithM :: Monad m => GenericQ (GenericM m) -> GenericQ (GenericM m)
-gzipWithM _ = error "urk"
+gzipWithM _ _ = error "urk"
 
 orElse :: Maybe a -> Maybe a -> Maybe a
 orElse = error "urk"
diff --git a/testsuite/tests/typecheck/should_compile/valid_hole_fits.stderr b/testsuite/tests/typecheck/should_compile/valid_hole_fits.stderr
index 1c108f719b..116a18f42f 100644
--- a/testsuite/tests/typecheck/should_compile/valid_hole_fits.stderr
+++ b/testsuite/tests/typecheck/should_compile/valid_hole_fits.stderr
@@ -225,7 +225,7 @@ valid_hole_fits.hs:38:10: warning: [-Wtyped-holes (in -Wdefault)]
            (and originally defined in ‘GHC.Base’))
 
 valid_hole_fits.hs:41:8: warning: [-Wtyped-holes (in -Wdefault)]
-    • Found hole: _ :: [Char] -> IO ()
+    • Found hole: _ :: String -> IO ()
     • In the expression: _
       In the expression: _ "hello, world"
       In an equation for ‘main’: main = _ "hello, world"
@@ -242,7 +242,7 @@ valid_hole_fits.hs:41:8: warning: [-Wtyped-holes (in -Wdefault)]
           (imported from ‘Prelude’ at valid_hole_fits.hs:3:1-40
            (and originally defined in ‘System.IO’))
         print :: forall a. Show a => a -> IO ()
-          with print @[Char]
+          with print @String
           (imported from ‘Prelude’ at valid_hole_fits.hs:3:1-40
            (and originally defined in ‘System.IO’))
         fail :: forall (m :: * -> *) a. MonadFail m => String -> m a
@@ -250,6 +250,6 @@ valid_hole_fits.hs:41:8: warning: [-Wtyped-holes (in -Wdefault)]
           (imported from ‘Prelude’ at valid_hole_fits.hs:3:1-40
            (and originally defined in ‘Control.Monad.Fail’))
         mempty :: forall a. Monoid a => a
-          with mempty @([Char] -> IO ())
+          with mempty @(String -> IO ())
           (imported from ‘Prelude’ at valid_hole_fits.hs:3:1-40
            (and originally defined in ‘GHC.Base’))