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)

1 files changed, 38 insertions, 53 deletions

diff --git a/compiler/GHC/Tc/TyCl.hs b/compiler/GHC/Tc/TyCl.hs
index 144021caea..98550132c5 100644
--- a/compiler/GHC/Tc/TyCl.hs
+++ b/compiler/GHC/Tc/TyCl.hs
@@ -2313,18 +2313,18 @@ newtype instance T [a] :: <kind> where ...   -- See Point 5
 2. Where these kinds come from: Return kinds are processed through several
    different code paths:
 
-     data/newtypes: The return kind is part of the TyCon kind, gotten either
+   Data/newtypes: The return kind is part of the TyCon kind, gotten either
      by checkInitialKind (standalone kind signature / CUSK) or
      inferInitialKind. It is extracted by bindTyClTyVars in tcTyClDecl1. It is
      then passed to tcDataDefn.
 
-     families: The return kind is either written in a standalone signature
+   Families: The return kind is either written in a standalone signature
      or extracted from a family declaration in getInitialKind.
      If a family declaration is missing a result kind, it is assumed to be
      Type. This assumption is in getInitialKind for CUSKs or
      get_fam_decl_initial_kind for non-signature & non-CUSK cases.
 
-     instances: The data family already has a known kind. The return kind
+   Instances: The data family already has a known kind. The return kind
      of an instance is then calculated by applying the data family tycon
      to the patterns provided, as computed by the typeKind lhs_ty in the
      end of tcDataFamInstHeader. In the case of an instance written in GADT
@@ -2350,10 +2350,9 @@ newtype instance T [a] :: <kind> where ...   -- See Point 5
 4. Datatype return kind restriction: A data/data-instance return kind must end
    in a type that, after type-synonym expansion, yields `TYPE LiftedRep`. By
    "end in", we mean we strip any foralls and function arguments off before
-   checking: this remaining part of the type is returned from
-   etaExpandAlgTyCon. Note that we do *not* do type family reduction here.
-   Examples:
+   checking: this remaining part of the type is returned from etaExpandAlgTyCon.
 
+   Examples:
      data T1 :: Type                          -- good
      data T2 :: Bool -> Type                  -- good
      data T3 :: Bool -> forall k. Type        -- strange, but still accepted
@@ -2361,27 +2360,38 @@ newtype instance T [a] :: <kind> where ...   -- See Point 5
      data T5 :: Bool                          -- bad
      data T6 :: Type -> Bool                  -- bad
 
+   Exactly the same applies to data instance (but not data family)
+   declarations.  Examples
+     data instance D1 :: Type                 -- good
+     data instance D2 :: Boool -> Type        -- good
+
+   We can "look through" type synonyms
+     type Star = Type
+     data T7 :: Bool -> Star                  -- good (synonym expansion ok)
      type Arrow = (->)
-     data T7 :: Arrow Bool Type               -- good
+     data T8 :: Arrow Bool Type               -- good (ditto)
 
+   But we specifically do *not* do type family reduction here.
      type family ARROW where
        ARROW = (->)
-     data T8 :: ARROW Bool Type               -- bad
-
-     type Star = Type
-     data T9 :: Bool -> Star                  -- good
+     data T9 :: ARROW Bool Type               -- bad
 
      type family F a where
        F Int  = Bool
        F Bool = Type
      data T10 :: Bool -> F Bool               -- bad
 
+   The /principle/ here is that in the TyCon for a data type or data instance,
+   we must be able to lay out all the type-variable binders, one by one, until
+   we reach (TYPE xx).  There is no place for a cast here.  We could add one,
+   but let's not!
+
    This check is done in checkDataKindSig. For data declarations, this
    call is in tcDataDefn; for data instances, this call is in tcDataFamInstDecl.
 
-   However, because data instances in GADT syntax can have two return kinds (see
-   point (2) above), we must check both return kinds. The user-written return
-   kind is checked in tc_kind_sig within tcDataFamInstHeader. Examples:
+4a  Because data instances in GADT syntax can have two return kinds (see
+    point (2) above), we must check both return kinds. The user-written return
+    kind is checked by the call to checkDataKindSig in tcDataFamInstDecl. Examples:
 
      data family D (a :: Nat) :: k     -- good (see Point 6)
 
@@ -2906,36 +2916,11 @@ tcTyFamInstEqnGuts fam_tc mb_clsinfo imp_vars exp_bndrs hs_pats hs_rhs_ty
        ; return (qtvs, pats, rhs_ty) }
 
 -----------------
-tcFamTyPats :: TyCon
-            -> HsTyPats GhcRn                -- Patterns
-            -> TcM (TcType, TcKind)          -- (lhs_type, lhs_kind)
--- Used for both type and data families
-tcFamTyPats fam_tc hs_pats
-  = do { traceTc "tcFamTyPats {" $
-         vcat [ ppr fam_tc, text "arity:" <+> ppr fam_arity ]
-
-       ; let fun_ty = mkTyConApp fam_tc []
-
-       ; (fam_app, res_kind) <- unsetWOptM Opt_WarnPartialTypeSignatures $
-                                setXOptM LangExt.PartialTypeSignatures $
-                                -- See Note [Wildcards in family instances] in
-                                -- GHC.Rename.Module
-                                tcInferApps typeLevelMode lhs_fun fun_ty hs_pats
-
-       ; traceTc "End tcFamTyPats }" $
-         vcat [ ppr fam_tc, text "res_kind:" <+> ppr res_kind ]
-
-       ; return (fam_app, res_kind) }
-  where
-    fam_name  = tyConName fam_tc
-    fam_arity = tyConArity fam_tc
-    lhs_fun   = noLoc (HsTyVar noExtField NotPromoted (noLoc fam_name))
-
 unravelFamInstPats :: TcType -> [TcType]
 -- Decompose fam_app to get the argument patterns
 --
 -- We expect fam_app to look like (F t1 .. tn)
--- tcInferApps is capable of returning ((F ty1 |> co) ty2),
+-- tcFamTyPats is capable of returning ((F ty1 |> co) ty2),
 -- but that can't happen here because we already checked the
 -- arity of F matches the number of pattern
 unravelFamInstPats fam_app
@@ -4749,20 +4734,20 @@ badDataConTyCon data_con res_ty_tmpl
       $+$ hang (text "Suggestion: instead use this type signature:")
              2 (ppr (dataConName data_con) <+> dcolon <+> ppr suggested_ty)
 
-    -- To construct a type that GHC would accept (suggested_ty), we:
-    --
-    -- 1) Find the existentially quantified type variables and the class
-    --    predicates from the datacon. (NB: We don't need the universally
-    --    quantified type variables, since rejigConRes won't substitute them in
-    --    the result type if it fails, as in this scenario.)
-    -- 2) Split apart the return type (which is headed by a forall or a
-    --    context) using tcSplitNestedSigmaTys, collecting the type variables
-    --    and class predicates we find, as well as the rho type lurking
-    --    underneath the nested foralls and contexts.
-    -- 3) Smash together the type variables and class predicates from 1) and
-    --    2), and prepend them to the rho type from 2).
-    (tvs, theta, rho) = tcSplitNestedSigmaTys (dataConUserType data_con)
+    -- To construct a type that GHC would accept (suggested_ty), we
+    -- simply drag all the foralls and (=>) contexts to the front
+    -- of the type.
     suggested_ty = mkSpecSigmaTy tvs theta rho
+    (tvs, theta, rho) = go (dataConUserType data_con)
+
+    go :: Type -> ([TyVar],ThetaType,Type)
+    -- The returned Type has no foralls or =>, even to the right of an (->)
+    go ty | null arg_tys = (tvs1, theta1, rho1)
+          | otherwise    = (tvs1 ++ tvs2, theta1 ++ theta2, mkVisFunTys arg_tys rho2)
+      where
+        (tvs1, theta1, rho1) = tcSplitNestedSigmaTys ty
+        (arg_tys, ty2)       = tcSplitFunTys rho1
+        (tvs2, theta2, rho2) = go ty2
 
 badGadtDecl :: Name -> SDoc
 badGadtDecl tc_name