• Simon Peyton Jones's avatar
    Simple subsumption · 2b792fac
    Simon Peyton Jones authored
    This patch simplifies GHC to use simple subsumption.
      Ticket #17775
    Implements GHC proposal #287
    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
      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:
    * 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:
    Metric Decrease:
    Merge note: This appears to break the
    `UnliftedNewtypesDifficultUnification` test. It has been marked as
    broken in the interest of merging.
    (cherry picked from commit 66b7b195)
Code owners : Ben Gamari
UI.hs 169 KB