Plugin broken on GHC 8.4.2

[adamgundry]

There are lots of unsolved constraints involving flattening skolems. Perhaps Trac #15147 is related?

RationalExamples.hs:53:13: error:
    • Couldn't match type ‘Data.UnitsOfMeasure.Convert.ToCBU
                             (Unpack fsk1)’
                     with ‘(fsk0 *: One) /: One’
        arising from a use of ‘convert’
      The type variables ‘fsk1’, ‘fsk0’ are ambiguous
    • In the expression: convert $ (1 / 60) *: lngMinute
      In an equation for ‘lngSecond’:
          lngSecond = convert $ (1 / 60) *: lngMinute
   |
53 | lngSecond = convert $ (1 / 60) *: lngMinute

[adamgundry]

I believe this has broken because of changes in GHC's constraint solver in the 8.4.x series. In principle it should be possible to adapt to the constraints that GHC now throws at the plugin, but it will require a bit of digging into the code.

[philderbeast]

I ran a bisection on GHC and found the commit there that broke the uom-plugin:

> git bisect good
8dc6d645fc3384b3b8ded0578939f5c855dd2ed5 is the first bad commit
commit 8dc6d645fc3384b3b8ded0578939f5c855dd2ed5
Author: Simon Peyton Jones <simonpj@microsoft.com>
Date:   Fri May 26 09:31:38 2017 +0100

    Re-engineer Given flatten-skolems

    The big change here is to fix an outright bug in flattening of Givens,
    albeit one that is very hard to exhibit.  Suppose we have the constraint
        forall a. (a ~ F b) => ..., (forall c. ....(F b)...) ...

    Then
     - we'll flatten the (F) b to a fsk, say  (F b ~ fsk1)
     - we'll rewrite the (F b) inside the inner implication to 'fsk1'
     - when we leave the outer constraint we are suppose to unflatten;
       but that fsk1 will still be there
     - if we re-simplify the entire outer implication, we'll re-flatten
       the Given (F b) to, say, (F b ~ fsk2)
    Now we have two fsks standing for the same thing, and that is very
    wrong.

    Solution: make fsks behave more like fmvs:
     - A flatten-skolem is now a MetaTyVar, whose MetaInfo is FlatSkolTv
     - We "fill in" that meta-tyvar when leaving the implication
     - The old FlatSkol form of TcTyVarDetails is gone completely
     - We track the flatten-skolems for the current implication in
       a new field of InertSet, inert_fsks.

    See Note [The flattening story] in TcFlatten.

    In doing this I found various other things to fix:

    * I removed the zonkSimples from TcFlatten.unflattenWanteds; it wasn't
      needed.   But I added one in TcSimplify.floatEqualities, which does
      the zonk precisely when it is needed.

    * Trac #13674 showed up a case where we had
         - an insoluble Given,   e.g.  a ~ [a]
         - the same insoluble Wanted   a ~ [a]
      We don't use the Given to rewwrite the Wanted (obviously), but
      we therefore ended up reporting
          Can't deduce (a ~ [a]) from (a ~ [a])
      which is silly.

      Conclusion: when reporting errors, make the occurs check "win"
      See Note [Occurs check wins] in TcErrors

:040000 040000 bc8cbf367941ccb6678dbde5b64de93ad13bdccd 8ee7d6cb5c47d48b892448f5c6f7d82f2e48e3c0 M	compiler
:040000 040000 884ace486f4e79bfbdbd5c0015874a831065d44a 68882a528b26eab705a7e00dfeef44c68b135dd2 M	testsuite

[philderbeast]

I encountered quite a few commits that would not build GHC during the bisection that I had to skip. The log I saved as bisect.log. Once I thought to submodule hashable locally to workaround changes in base, a dependency of the uom-plugin:units test, the bisection went much faster.

[philderbeast]

@adamgundry, seeing how GHC changed, how might we change the plugin to keep up?

[adamgundry]

Thanks for investigating this; I'm sorry for letting this linger on, but it unfortunately requires rather a lot of detailed investigation to understand what the flattened constraints look like and how it might be possible to unflatten and solve them by unification.

There is actually WIP in GHC to simplify flattening (https://gitlab.haskell.org/ghc/ghc/-/merge_requests/4149). I haven't tried, but I imagine that patch may change things again, possibly in a good way?

[adamgundry]

See also: https://mail.haskell.org/pipermail/ghc-devs/2020-November/019355.html

[adamgundry]

Closing as we now support 9.0 or later successfully, thanks to the removal of flattening and to ghc-tcplugin-api.