Skip to content
  • 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
       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 66b7b195)
    2b792fac