Custom Cans for equivalent constraints involving tallies

[nfrisby]

If the plugin simplifies a level 2 frag equivalence constraint to sko[2] ~ sko[1] :+ 1, then GHC will flatten to sko[2] ~ flat[2] where flat is either a fsk or an fmv and reorient to flat[2] ~ sko[2]. Thus occurrences of sko[2] will not be replaced with sko[1] :+ 1.

That seems problematic. As far as I understand, the reason we want to eliminate deeper leveled tyvars is so that more ~ constraints will float. (TODO Is there any other reason? Edit: I don't think so; see email from SPJ.) This happens two related ways.

• Eliminating all level 2 occurrences in a Wanted will make that Wanted eligible for floating to level 1. For example, a level 2 Wanted tau[1] ~ sko[2] would not become tau[1] ~ sko[1] :+ 1, and so could not float from 2 to 1 because of the level 2 variable in its RHS.
• A level 2 Given CTyEqCan sko[2] ~ ... triggers the has_given_eqs exception for https://gitlab.haskell.org/ghc/ghc/issues/15009, so ~ constraints can float out from under it based on the assumption that it has eliminated all occurrences of sko[2].

However, fsk[2] ~ sko[2] is misoriented for the has_givens_eqs exception, so the failure to eliminate sko[2] from Wanteds is moot: nothing can float out from under that Given.

If we had no Givens and these Wanteds sko[1] :+ 1 ~ fmv[2], fmv[2] ~ tau[2], and tau[1] ~ tau[2], I think it already works: unflattenWanteds unifies tau[2] := sko[1] :+ 1 despite the apparent misorientation, so the third constraint will get to float.

The question is how to represent the Given sko[2] ~ sko[1] :+ 1 in a way that will trigger the 15009 has_given_eqs exception. Maybe I could change it to a CDictCan if it conceptually triggers the exception -- a CDictCan the plugin still interprets as the intended CTyEqCan.

[nfrisby]

I emailed ghc-devs with a related question, wondering if eliminating occurrences of deeper leveled tyvars matters in the absence of GHC's 15009 has_given_eqs exception.

Edit: Simon replied. He confirmed my understanding of how 15009 matters. He didn't directly confirm that 15009 is indeed a necessary ingredient. But he did say things that make me even more sure that it is.

[nfrisby]

I think there are three options for a ~ constraint involving tallies.

• Write it as a genuine ~. This is somewhat tedious because GHC fights us on some rewrites we'd like. But it seems to handle taus in Wanteds pretty nicely.
  • Write it as a class, if the 15009 exception should apply. GHC won't fight us and Wanteds can float out from under it.
  • Write it as a type family when 15009 does not apply. GHC won't fight us and this appropriately blocks all floating.

I'm going to investigate the third option, to see how painful it is to handle tau assignment manually. If it's alright, I'll prefer it because it simplifies the notion of "work". Then I'll figure out how to add the 15009 exception as a follow-up ticket, probably.

[nfrisby]

EqFrag l r ~ '() seems to be working (frag and motley tests passing). I'm assigning to a tau LHS if tau is touchable and unfilled. I worry I should check for something else too, but I'm not sure what. (Signature tyvar, maybe?)

This change revealed a bug and a "bug". The "bug" is that I wasn't counting reduction of FragEQ a q to k when the multiplicity table has a singleton interval as progress (setM). That wasn't necessary before, since GHC was probably doing that rewrite for us when we're lucky. Moreover, it would loop sometimes, since GHC would do the opposite rewrite when we're unlucky. With EqFrag, it's no longer a dice roll.

I'll close this and open a separate Issue for the 15009 case. (I'll open a bug for over-eager assignment when I witness it -- seems likely.)