• Ningning Xie's avatar
    Refactor coercion rule · 55a3f855
    Ningning Xie authored
    The patch is an attempt on #15192.
    It defines a new coercion rule
     | GRefl Role Type MCoercion
    which correspondes to the typing rule
         t1 : k1
      GRefl r t1 MRefl: t1 ~r t1
         t1 : k1       co :: k1 ~ k2
      GRefl r t1 (MCo co) : t1 ~r t1 |> co
    MCoercion wraps a coercion, which might be reflexive (MRefl)
    or not (MCo co). To know more about MCoercion see #14975.
    We keep Refl ty as a special case for nominal reflexive coercions,
    naemly, Refl ty :: ty ~n ty.
    This commit is meant to be a general performance improvement,
    but there are a few regressions. See #15192, comment:13 for
    more information.
    Test Plan: ./validate
    Reviewers: bgamari, goldfire, simonpj
    Subscribers: rwbarton, thomie, carter
    GHC Trac Issues: #15192
    Differential Revision: https://phabricator.haskell.org/D4747
CoreFVs.hs 29.8 KB