Skip to content

Fix wrong role in mkSelCo_maybe

Krzysztof Gogolewski requested to merge wip/T23938 into master

In the Lint failure in #23938 (closed), we start with a coercion Refl :: T a ~R T a, and call mkSelCo (SelTyCon 1 nominal) Refl. The function incorrectly returned Refl :: a ~R a. The returned role should be nominal, according to the SelCo rule:

      co : (T s1..sn) ~r0 (T t1..tn)
      r = tyConRole tc r0 i
      ----------------------------------
      SelCo (SelTyCon i r) : si ~r ti

In this test case, r is nominal while r0 is representational.

Merge request reports