• Ningning Xie's avatar
    Refactor coercion rule · 55a3f855
    Ningning Xie authored
    Summary:
    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
    55a3f855
TcCanonical.hs 96.7 KB