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)

8 files changed, 38 insertions, 18 deletions

diff --git a/testsuite/tests/patsyn/should_compile/T17775-singleton.hs b/testsuite/tests/patsyn/should_compile/T17775-singleton.hs
new file mode 100644
index 0000000000..651dff583a
--- /dev/null
+++ b/testsuite/tests/patsyn/should_compile/T17775-singleton.hs
@@ -0,0 +1,18 @@
+{-# LANGUAGE PatternSynonyms #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ViewPatterns #-}
+module Bug where
+
+-- Ryan Scott (on MR !2600) said this failed
+
+type T = forall a. a -> ()
+
+toT :: () -> T
+toT x _ = x
+
+pattern ToT :: T -> ()
+pattern ToT{x} <- (toT -> x)
+
+-- f (toT -> (x::T)) = True
+
diff --git a/testsuite/tests/patsyn/should_compile/all.T b/testsuite/tests/patsyn/should_compile/all.T
index 6ef1928768..75be0c68b2 100644
--- a/testsuite/tests/patsyn/should_compile/all.T
+++ b/testsuite/tests/patsyn/should_compile/all.T
@@ -78,3 +78,4 @@ test('T14394', normal, ghci_script, ['T14394.script'])
 test('T14498', normal, compile, [''])
 test('T16682', [extra_files(['T16682.hs', 'T16682a.hs'])],
                multimod_compile, ['T16682', '-v0 -fwarn-incomplete-patterns -fno-code'])
+test('T17775-singleton', normal, compile, [''])
diff --git a/testsuite/tests/patsyn/should_fail/T11010.stderr b/testsuite/tests/patsyn/should_fail/T11010.stderr
index 6e3aae58f5..28216760ee 100644
--- a/testsuite/tests/patsyn/should_fail/T11010.stderr
+++ b/testsuite/tests/patsyn/should_fail/T11010.stderr
@@ -1,13 +1,13 @@
 
 T11010.hs:9:36: error:
     • Couldn't match type ‘a1’ with ‘Int’
+      Expected: a -> b
+        Actual: a1 -> b
       ‘a1’ is a rigid type variable bound by
         a pattern with constructor:
           Fun :: forall a b. String -> (a -> b) -> Expr a -> Expr b,
         in a pattern synonym declaration
         at T11010.hs:9:26-36
-      Expected type: a -> b
-        Actual type: a1 -> b
     • In the declaration for pattern synonym ‘IntFun’
     • Relevant bindings include
         x :: Expr a1 (bound at T11010.hs:9:36)
diff --git a/testsuite/tests/patsyn/should_fail/T11039.stderr b/testsuite/tests/patsyn/should_fail/T11039.stderr
index 14d67a2bb2..f8f4d35768 100644
--- a/testsuite/tests/patsyn/should_fail/T11039.stderr
+++ b/testsuite/tests/patsyn/should_fail/T11039.stderr
@@ -1,10 +1,10 @@
 
 T11039.hs:8:15: error:
     • Couldn't match type ‘f’ with ‘A’
+      Expected: f a
+        Actual: A a
       ‘f’ is a rigid type variable bound by
         the signature for pattern synonym ‘Q’
         at T11039.hs:7:1-38
-      Expected type: f a
-        Actual type: A a
     • In the pattern: A a
       In the declaration for pattern synonym ‘Q’
diff --git a/testsuite/tests/patsyn/should_fail/T14552.stderr b/testsuite/tests/patsyn/should_fail/T14552.stderr
index b9b6b8448b..34ee266cdd 100644
--- a/testsuite/tests/patsyn/should_fail/T14552.stderr
+++ b/testsuite/tests/patsyn/should_fail/T14552.stderr
@@ -1,8 +1,8 @@
 
 T14552.hs:22:9: error:
     • Cannot generalise type; skolem ‘k’ would escape its scope
-      if I tried to quantify (aa0 :: k) in this type:
-        forall k (w :: k --> *). Exp a0 (F @k @(*) w aa0)
+      if I tried to quantify (t0 :: k) in this type:
+        forall k (w :: k --> *). Exp a0 (F @k @(*) w t0)
       (Indeed, I sometimes struggle even printing this correctly,
        due to its ill-scoped nature.)
     • In the declaration for pattern synonym ‘FOO’
diff --git a/testsuite/tests/patsyn/should_fail/T15685.stderr b/testsuite/tests/patsyn/should_fail/T15685.stderr
index 7f01ebc479..37627b852b 100644
--- a/testsuite/tests/patsyn/should_fail/T15685.stderr
+++ b/testsuite/tests/patsyn/should_fail/T15685.stderr
@@ -1,6 +1,11 @@
 
 T15685.hs:13:24: error:
     • Couldn't match kind ‘a1’ with ‘[k0]’
+      When matching types
+        f :: a1 -> *
+        NP a0 :: [k0] -> *
+      Expected: f a2
+        Actual: NP a0 b0
         ‘a1’ is untouchable
           inside the constraints: as ~ (a2 : as1)
           bound by a pattern with constructor:
@@ -12,11 +17,6 @@ T15685.hs:13:24: error:
         the inferred type of HereNil :: NS f as
         at T15685.hs:13:9-15
       Possible fix: add a type signature for ‘HereNil’
-      When matching types
-        f :: a1 -> *
-        NP a0 :: [k0] -> *
-      Expected type: f a2
-        Actual type: NP a0 b0
     • In the pattern: Nil
       In the pattern: Here Nil
       In the declaration for pattern synonym ‘HereNil’
diff --git a/testsuite/tests/patsyn/should_fail/T15695.stderr b/testsuite/tests/patsyn/should_fail/T15695.stderr
index 6ef415ad9b..2e834c6d08 100644
--- a/testsuite/tests/patsyn/should_fail/T15695.stderr
+++ b/testsuite/tests/patsyn/should_fail/T15695.stderr
@@ -13,6 +13,8 @@ T15695.hs:39:14: warning: [-Wdeferred-type-errors (in -Wdefault)]
                            a3 -> ApplyT kind a b,
                  in an equation for ‘from'’
         at T15695.hs:39:8-21
+      Expected: a4
+        Actual: Either (NA 'VO) a3
       ‘a2’ is a rigid type variable bound by
         a pattern with pattern synonym:
           ASSO :: forall kind (a :: kind) (b :: Ctx kind).
@@ -24,8 +26,6 @@ T15695.hs:39:14: warning: [-Wdeferred-type-errors (in -Wdefault)]
                   a3 -> ApplyT kind a b,
         in an equation for ‘from'’
         at T15695.hs:39:8-21
-      Expected type: a4
-        Actual type: Either (NA 'VO) a3
     • In the pattern: Left a
       In the pattern: ASSO (Left a)
       In an equation for ‘from'’: from' (ASSO (Left a)) = Here (a :* Nil)
@@ -34,9 +34,10 @@ T15695.hs:39:14: warning: [-Wdeferred-type-errors (in -Wdefault)]
           (bound at T15695.hs:39:1)
 
 T15695.hs:40:26: warning: [-Wdeferred-type-errors (in -Wdefault)]
-    • Couldn't match type ‘a0 : as0’ with ‘'[]’
-      Expected type: NS (NP NA) '[ '[ 'VO]]
-        Actual type: NS (NP NA) ('[ 'VO] : a0 : as0)
+    • Couldn't match type: a0 : as0
+                     with: '[]
+      Expected: NS (NP NA) '[ '[ 'VO]]
+        Actual: NS (NP NA) ('[ 'VO] : a0 : as0)
     • In the expression: There (Here undefined)
       In an equation for ‘from'’:
           from' (ASSO (Right b)) = There (Here undefined)
diff --git a/testsuite/tests/patsyn/should_fail/mono.stderr b/testsuite/tests/patsyn/should_fail/mono.stderr
index 8f370ce2f0..264579f91b 100644
--- a/testsuite/tests/patsyn/should_fail/mono.stderr
+++ b/testsuite/tests/patsyn/should_fail/mono.stderr
@@ -1,8 +1,8 @@
 
 mono.hs:7:4: error:
     • Couldn't match type ‘Bool’ with ‘Int’
-      Expected type: [Bool]
-        Actual type: [Int]
+      Expected: [Bool]
+        Actual: [Int]
     • In the pattern: Single x
       In an equation for ‘f’: f (Single x) = x