Type checker plugin

[dmcclean]

(Warning, this is a doozy.)

It would be really nice if we had a type checker plugin capable of solving constraints like d ~ DOne / (DOne / d) and other "obvious" proof obligations that arise.

These sorts of things were crippling to the first attempt at using this for dimensional linear algebra, and especially for dimensional linear algebra as it applies to control theory. (Some of those sketches using dimensional-dk are no longer visible in history at that link.)

It turns out that unification in abelian groups (like the group of dimensions) is decidable, and that unification discharges all of these things that we think are obvious, and a few more besides. The agum package provides a Haskell implementation (unfortunately with GPL licensing) of this that could be used to do "the hard part" of this problem. Of course, the actual hard part is figuring out how the GHC type checker plugin API works. ;)

[dmcclean]

I'm going to see if I can recruit anyone to work on this with me at Hac Boston in a couple of weeks, since I don't understand how to do it myself. The API GHC provides for this has a lot of cryptic abbreviated names that probably make a lot more sense to someone who understands the internals of the type checker.

[bjornbm]

+1

[dmcclean]

Objective is to get past problems like this that cripple my attempt at dimensional linear algebra:

examples\Controls.hs:42:46:
    Couldn't match type `((x / iv) / u) * u' with `((x / iv) / x) * x'
    NB: `*' is a type function, and may not be injective
    Expected type: DimMat
                     ('VectorShape
                        (((x / iv) / x) * x)
                        (MapMul (((x / iv) / x) * x) (MapDiv (x / iv) (MapDiv iv xs))))
                     e
      Actual type: DimMat
                     (ShapeProduct
                        ('MatrixShape
                           ((x / iv) / u)
                           (MapDiv (x / iv) (MapDiv iv xs))
                           (MapMul
                              u (Numeric.LinearAlgebra.Dimensional.DK.Shapes.MapRecip us)))
                        ('VectorShape u us))
                     e
    Relevant bindings include
      xDot :: DimMat
                ('VectorShape
                   (((x / iv) / x) * x)
                   (MapMul (((x / iv) / x) * x) (MapDiv (x / iv) (MapDiv iv xs))))
                e
        (bound at examples\Controls.hs:42:23)
      a :: DimMat
             ('MatrixShape
                ((x / iv) / x)
                (MapDiv (x / iv) (MapDiv iv xs))
                (MapMul
                   x (Numeric.LinearAlgebra.Dimensional.DK.Shapes.MapRecip xs)))
             e
        (bound at examples\Controls.hs:38:23)
      b :: DimMat
             ('MatrixShape
                ((x / iv) / u)
                (MapDiv (x / iv) (MapDiv iv xs))
                (MapMul
                   u (Numeric.LinearAlgebra.Dimensional.DK.Shapes.MapRecip us)))
             e
        (bound at examples\Controls.hs:39:23)
      y :: DimMat
             ('VectorShape ((y / x) * x) (MapMul ((y / x) * x) (MapDiv y ys))) e
        (bound at examples\Controls.hs:43:23)
      c :: DimMat
             ('MatrixShape
                (y / x)
                (MapDiv y ys)
                (MapMul
                   x (Numeric.LinearAlgebra.Dimensional.DK.Shapes.MapRecip xs)))
             e
        (bound at examples\Controls.hs:40:23)
      d :: DimMat
             ('MatrixShape
                (y / u)
                (MapDiv y ys)
                (MapMul
                   u (Numeric.LinearAlgebra.Dimensional.DK.Shapes.MapRecip us)))
             e
        (bound at examples\Controls.hs:41:23)
      (Some bindings suppressed; use -fmax-relevant-binds=N or -fno-max-relevant-binds)
    In the second argument of `add', namely `(b <> u)'
    In the expression: (a <> x) `add` (b <> u)
    In an equation for `xDot': xDot = (a <> x) `add` (b <> u)

It does all the seemingly difficult parts, but then gets tripped up trying to unify ((x / iv) / u) * u with ((x / iv) / x) * x (where all the variables have kind Dimension), which seems like a frustratingly simple consequence of the group axioms. 😒

[adamgundry]

Good luck! You might be aware of this already, but my uom-plugin (paper) does something like this, though competition is very welcome. I'm on the wrong side of the pond to go to Hac Boston, but feel free to ask questions about the plugins API (or perhaps better ask on ghc-devs). We are still figuring out how the API should work...

[dmcclean]

Hi @adamgundry. Definitely have checked out your work and your paper, which is cool. It looks like you do solve the same type plugin problem that this issue is about, which is awesome.

As far as the competition goes, we should think about joining forces. You have this issue kicked. We have more arithmetic, a library that works for almost all use cases without TH, a wide variety of pre-defined units and dimension synonyms. We also have a branch where we are exploring tracking unit names, which is pretty interesting for user interfaces.

[dmcclean]

Digging in to the way the uom-plugin solver works and trying to line up Adam's terminology with ours.

His NormUnit type fills essentially the same purpose as our Dimension' type, so we can use our term-level dimensions module to do the relevant parts of what's in Data.UnitsOfMeasure.Plugin.NormalForm.

Near as I can tell, we don't have an equivalent of his Pack and Unpack type families, which I believe form composite type-level units, so I think we get to skip those cases.

Data.UnitsOfMeasure.Plugin.Convert deals with loading the names of all the important type families and constructors that are treated specially by the plugin. It also converts normal forms (our Dimension's) to Types and also goes the other way when possible. Interestingly for us when this is possible it can be done by applying the type family definitions for (*) and (\) etc. In contrast, Adam's type families are abstract in the sense that they have no instances, because he has an open world for base dimensions. So perhaps there is some way to provoke GHC to perform this simplification step for us when it is necessary, but if not then we need to write a version of his normaliseUnit that performs the simplifications, because we need to provoke new rounds of attempting this simplification, as at https://github.com/adamgundry/uom-plugin/blob/master/uom-plugin/src/Data/UnitsOfMeasure/Plugin/Unify.hs#L97-L99.

I don't understand what our analog of his Atom type would be:

-- | An atom in the normal form is either a base unit, a variable or a
-- stuck type family application (but not one of the built-in type
-- families that correspond to group operations).
data Atom = BaseAtom Type | VarAtom TyVar | FamAtom TyCon [Type]

• Is the FamAtom case intended to cover stuck applications of type families that correspond to sort of "composite" group operations like exponentiation? Or of Pack and Unpack? Or of other random type families that users may have declared in their own modules?
• Why is it BaseAtom Type and not BaseAtom NormUnit?

I am at the phase where I understand the broad outlines of what's going on, just digging deeper into the details.

[dmcclean]

Also this is probably an embarrassingly simple question, but I could use help unpacking this comment:

-- | A substitution is essentially a list of (variable, unit) pairs,
-- but we keep the original 'Ct' that lead to the substitution being
-- made, for use when turning the substitution back into constraints.
type TySubst = [SubstItem]

I tried to look up the Ct type in the GHC source code to figure out what on earth a Ct is supposed to be, but AFAICT even that file doesn't include a comment explaining what the name or the type is supposed to mean. I looked at the various cases, but I couldn't figure it out.

It's compounded by the fact that I'm not sure what it means to turn the substitution back into constraints, and so I can't guess what information we would need then.

[dmcclean]

Well, I thought I understood...

If it's true that Dimension' is our analog of NormUnit then I'm confused, because:

-- | Apply a substitution to a single normalised unit
substsUnit :: TySubst -> NormUnit -> NormUnit
substsUnit []     u = u
substsUnit (si:s) u = substsUnit s (substUnit (siVar si) (siUnit si) u)

... but ours don't include any variables. So it must not be the case that NormUnit and Dimension' have the same role. I think the difference is that because Adam's universe is open to begin with, his normal form already has to have a case for variables. Since ours is closed, it doesn't.

Now I think that our Atom is something like:

data Atom = LitAtom Dimension' -- a literal dimension
          | VarAtom TyVar -- a dimension that we don't know anything about besides that it's a type variable
          | FamAtom TyCon [Type] -- I still am confused about this case, as I was two comments above

and that we have a NormUnit type substantially like Adam's, maintaining the invariant that there is only one LitAtom key in any NormUnit Map and it always has an exponent of 1. (Or some equivalent representation, like a single Dimension' and a map that doesn't include any LitAtom atoms.

[dmcclean]

Having the implementation as the solver gives @adamgundry's approach a much nicer type for square root than ours.

From his paper:

sqrt :: (Floating a) => Quantity a (u * u) -> Quantity a u

Compared to ours which needs the Root type family. Having the root type family does allow us to use arbitrary natural roots, which is nice I suppose.

I think there are going to be some hoops to go through to make a similar solver that can deal with the root type family. In essence it needs to solve a ~ Root 3 b by solving a ^ 3 ~ b instead, but I think it might need to preserve the fact that it was originally written as a root so that if it doesn't end up simplifying it retains the original form.

[dmcclean]

OK, I think I figured out everything except the Convert module.

Our trick is that applications of the Dim type constructor may be partially known and partially not, depending on what the arguments are. If they are all literal numbers, or at any rate are reducible to literal numbers (like Pos2 + Pos3), then it is a known combination of BaseAtoms. If they are all type variables, then in a sense the whole thing is one big dimension variable, but I think it still needs to be split into pieces.

Excerpt from @adamgundry 's code:

normaliseUnit uds (TyConApp tc tys)
  | tc == unitOneTyCon  uds                = pure one
  | tc == unitBaseTyCon uds, [x]    <- tys = pure $ baseUnit x
  | tc == mulTyCon      uds, [u, v] <- tys = (*:) <$> normaliseUnit uds u <*> normaliseUnit uds v
  | tc == divTyCon      uds, [u, v] <- tys = (/:) <$> normaliseUnit uds u <*> normaliseUnit uds v
  | tc == expTyCon      uds, [u, n] <- tys = (^:) <$> normaliseUnit uds u <*> isNumLitTy n
  | isFamilyTyCon tc                       = pure $ famUnit tc tys

The case of a Dim application that still includes type variables is essentially equivalent to the expTyCon case, but when isNumLitTy returns Nothing. I'm unclear on how Adam gets away with returning Nothing as an overall result in this case. Does this mean that he can't unify x with y when x ^: n ~ y ^: n, because n is a type variable and not a literal?

It seems like it would be a fairly major change to extend the grammar in figure 5 of his paper (assuming it's possible?) to allow variables in the position of integers on the RHS of exponents, although having such variables would handle this case and the case of things like Dim l m t 'Zero th n j.

Am I missing a subtle reason why this doesn't matter? Or alternatively is it the reason that Data.UnitsOfMeasure doesn't (appear to?) provide an exponentiation operator corresponding to the one in https://github.com/bjornbm/dimensional-dk/blob/961346f521bd40b1452db8539f58ccb7b2cd42c1/src/Numeric/Units/Dimensional/DK.hs#L411-L419 but instead provides an example:

-- >>> let cube x = x *: x *: x
-- >>> :t cube
-- cube :: Num a => Quantity a v -> Quantity a (v ^: 3)

[dmcclean]

I'm not completely sure that I'm reading it right, but I think that this paper discusses the problem of allowing variables in the exponents.

I think we are case E2 in the second row of table 1 and so that problem is undecidable? But I can't tell for sure if they are discussing the case where there is only one type, which can appear on either side of the exponentiation operator. In our case we have two separate types, one which can only appear on the left and the other which can only appear on the right. They use the same metavariable y in both positions, but in two different axioms, so it is unclear to me.

[dmcclean]

Rats. I powered through it and actually got this working! (Thanks to Adam.)

... and it actually fixed the error message that was my reason for initiating this thread, the one about Couldn't match type ((x / iv) / u) * u with ((x / iv) / x) * x.

... but that just got me to a whole bunch of new error messages, related to not being able to solve similar types of things for the MapMul and MapDiv type families that the linear algebra library uses.

Example:

Couldn't match type ys with MapMul ((y / x) * x) (MapDiv y ys)

These types logically match, because dividing each element of ys by y, and then multiplying each element of the result by ((y / x) * x) is equivalent to doing nothing at all.

It couldn't even do this simpler case, which I am slightly confused by because I thought it might:

Couldn't match type MapMul ((y / u) * u) (MapDiv y ys)
               with MapMul ((y / x) * x) (MapDiv y ys)

(The reason I felt this one is simpler is because, if you rewrote ((a / b) * b) to just a for any a and b then they would become syntactically identical.) (Update: Another way to think about it is that if we had injective type families alongside this solver, they would solve this simpler case but not the first one.)

There may yet be hope, because we don't really need the integer variables I was discussing above to tackle any of the cases I have seen so far, but we might need either a more complicated solver that is aware of MapMul and MapDiv or possibly switch to the constaint-based (instead of type family based) encoding for these sorts of things that @aavogt was using in his effort at the DimMat library, but which I was never really able to get my head around.

[aavogt]

@dmcclean, the idea was something like: let's define MapMulEq x y z :: Constraint instead of using (MapMul x y ~ z) :: Constraint, since the second version can't figure out x given y and z.

I haven't looked at Adam's paper or code, but maybe some of the ideas/experience Christan has https://hackage.haskell.org/package/ghc-typelits-natnormalise will help you

[dmcclean]

Thanks @aavogt for the reminder.

That approach is cool in that it provides bidirectional inference, and it's cool in that I think it would fix this problem, allowing a solver in Adam's style to figure everything out.

The big drawback that I see is that I can't figure out how to describe data types with polymorphic shapes. By switching away from the "forwards style" type families, you lose the ability to express types like this one, where there are four matrices with interrelated shapes determined by just a few choices of dimensions (for the independent variable, system states, system outputs, and control inputs respectively):

data ContinuousLiSystem (iv :: Dimension) (xs :: [Dimension]) (ys :: [Dimension]) (us :: [Dimension]) e =
  ContinuousLiSystem
  {
    a'' :: DimMat (DivideVectorLists (MapDiv iv xs) xs) e,
    b'' :: DimMat (DivideVectorLists (MapDiv iv xs) us) e,
    c'' :: DimMat (DivideVectorLists ys xs) e,
    d'' :: DimMat (DivideVectorLists ys us) e
  }

Do you happen to have any ideas on how to deal with this? Is the right approach to make the data type a totally unconstrained record of four matrices and then apply the constraints only in the functions that deal with it? I'm having trouble picturing exactly how that would work, especially for the construction function.

[aavogt]

I seem to have had some success with "forwards style" type families and making the plugin add wanted constraints that calculate the "backwards": https://github.com/aavogt/HListPlugin. Maybe it's easier to implement, but probably you get worse error messages and slower compile times with that idea.

That ContinuousLiSystem might work with ExistentialQuantification/GADT too. I mean translating what you wrote into something like:

data CLiSys iv xs ys us e = forall ivxs a b c d.
 (MapDiv iv xs ~ ivxs,
  DivideVectorLists ivxs xs ~ a,
  DivideVectorLists ivxs us ~ b,
  DivideVectorLists xs ys ~ c,
  DivideVectorLists ys us ~ d) => CLiSys {
   a'' :: DimMat a e,
   b'' :: DimMat b e,
   c'' :: DimMat c e,
   d'' :: DimMat d e }

and then just replace the DivideVectorLists xs ys ~ c with some DivideVectorListsEq xs ys c.

[dmcclean]

I will definitely take a look at how that plugin works.

The existential/GADT encoding idea is a good one, and I think it would have a good chance of checking everything it needs to check, but I think it might also kind of defeat my purposes because I don't think it would be able to calculate the "forwards" type for documentation purposes, it could only tell you if you were correct.

[dmcclean]

@adamgundry, if you have a minute could you answer a question I have about the solver API?

The tcPluginSolve function has type state -> [Ct] -> [Ct] -> [Ct] -> TcPluginM TcPluginResult for whatever the particular plugin's state is.

The definition of TcPluginResult is something like (taking from github GHC repository, may be more recent than what's in 7.10):

data TcPluginResult
  = TcPluginContradiction [Ct]
    -- ^ The plugin found a contradiction.
    -- The returned constraints are removed from the inert set,
    -- and recorded as insoluable.

  | TcPluginOk [(EvTerm,Ct)] [Ct]
    -- ^ The first field is for constraints that were solved.
    -- These are removed from the inert set,
    -- and the evidence for them is recorded.
    -- The second field contains new work, that should be processed by
    -- the constraint solver.

The three [Ct] arguments to the solver are labeled "given", "derived", and "wanted" in the docs, but I can't find anywhere that explains what that means. I assume wanted constraints are the ones the solver is being asked to solve? And that given constraints are the ones that we know are true from context? But what are the derived ones?

If I wanted to convert constraints like (MapMul d2 (MapMul d xs)) ~ ys into (xs ~ ys, 1 ~ d * d2) could I do it? I haven't solved them exactly, because the solution is conditional on being able to prove the new things. Is that what the second list in the TcPluginResult is meant for? If so, what should the evidence term look like given that we aren't sure yet if the global solution will even be possible?

I hope I am even wording this question in a way that makes sense.

[dmcclean]

Or maybe for that scenario I'm meant to ignore the second list in the TcPluginResult, but call the newWanted TcPluginM monad action, and somehow use its result to cook up the evidence for the constraint that would be solved, conditionally, if the new wanted constraint(s) were eventually solved?

[adamgundry]

@dmcclean excellent digging, sorry it's taken me a few days to respond to everything.

Indeed, uom-plugin doesn't currently provide much support for non-literal exponents, because they fall outside the abelian group fragment and do not necessarily have most general unifiers (e.g. a^i ~ 1 has two unifiers a ~ 1 and i ~ 0). However, normaliseUnit probably shouldn't completely fail in such a case, rather they should be treated like other unknown type families. This lack of support does show up in Data.UnitsOfMeasure.Convert, where the plugin doesn't solve all the constraints that arise.

The three [Ct] arguments to the solver are labeled "given", "derived", and "wanted" in the docs, but I can't find anywhere that explains what that means. I assume wanted constraints are the ones the solver is being asked to solve? And that given constraints are the ones that we know are true from context? But what are the derived ones?

Yes, Ct is the type of constraints, which are divided into "wanted" (things the solver needs to solve), "given" (things the solver may assume) and "derived". As an example of the first two cases, consider the following:

f :: a ~ b => [a] -> [b]
f x = x

When checking the body of f, the solver will have a ~ b as a given and [a] ~ [b] as a wanted. (And of course, GHC's internal solver will solve the wanted from the given.)

The case of "derived" constraints is a bit more interesting. These are constraints that aren't given (i.e. they cannot be assumed to be true) but also aren't wanted (i.e. they are not truly required in order for the program to typecheck). The typical case is with functional dependencies, e.g. suppose we have

class C a b | a -> b

Now if GHC has two wanted constraints C a b and C a c it will generate a derived constraint b ~ c from the functional dependency. It doesn't matter if this can't be solved, but if it can, it might help determine some otherwise ambiguous variables.

If I wanted to convert constraints like (MapMul d2 (MapMul d xs)) ~ ys into (xs ~ ys, 1 ~ d * d2) could I do it? I haven't solved them exactly, because the solution is conditional on being able to prove the new things. Is that what the second list in the TcPluginResult is meant for? If so, what should the evidence term look like given that we aren't sure yet if the global solution will even be possible?

You can indeed do this by calling newWanted to generate the two new wanted constraints xs ~ ys and 1 ~ d * d2, then returning TcPluginOk with the original constraint in the first argument (as it has been solved under the assumption of the new constraints) and the two new constraints in the second argument. To construct an evidence term, you can use ctEvTerm . ctEvidence to get (variables standing for) evidence out of the new constraints, then build a bigger coercion. But it may be simpler initially to generate fake evidence, for which see evByFiat. (This can also be used to generate "axioms", as the built-in GHC axioms are not extensible.)

In this case, the new constraints are strong enough to prove the original constraint (assuming an appropriate axiom). If the constraints you were generating were not sufficient to prove the original constraint, another approach would be to leave the original constraint unsolved but return additional "derived" constraints. It might be trickier to avoid loops this way, as you'd need to check you were not emitting the same constraints repeatedly.

[dmcclean]

See, that first paragraph is why I am an amateur at this. ;) I sensed that something was impossible but I couldn't put my finger on why, much less explain it.

Thanks very much for the rest. I think I know how to proceed with that pretty quickly, hopefully I will get a chance to take a crack at it next weekend.

One other worry I have is how does the faking of evidence interact with stuff that converts types to terms, like:

instance ( KnownTypeInt l
         , KnownTypeInt m
         , KnownTypeInt t
         , KnownTypeInt i
         , KnownTypeInt th
         , KnownTypeInt n
         , KnownTypeInt j
         ) => HasDimension (Proxy ('Dim l m t i th n j))
  where 
    dimension _ = Dim'
                (toNum (Proxy :: Proxy l))
                (toNum (Proxy :: Proxy m))
                (toNum (Proxy :: Proxy t))
                (toNum (Proxy :: Proxy i))
                (toNum (Proxy :: Proxy th))
                (toNum (Proxy :: Proxy n))
                (toNum (Proxy :: Proxy j))

I can see two possibilities, but there might be others.

1. As long as there aren't mistakes in the solver, it doesn't matter, because the two types equated by the fake evidence are actually equivalent and thus it doesn't matter which we start from to generate the term level representation.
2. Even though it doesn't matter which we start with, GHC's approach to generating the term level representation for types that have been simplified by the solver nevertheless uses the evidence terms, and we end up with some sort of runtime error when someone "calls our bluff".

I'm having trouble knowing how to construct test cases to investigate this, because I might just not be testing the scenario where things explode.

Can we discuss, perhaps in another forum, the copyright/licensing issues? I had intended to use your code just for reading and learning, but I was short on time at the hackathon where I had access to some people who could answer questions, so I ended up justifying to myself that I could copy and paste some things to get running, change them enough to understand the gist of how they work, and clean up the mess later. Obviously I didn't and won't release the result, but now I feel badly about it and I am realizing it isn't that easy to clean up later, because know you already know everything you copied, etc. It did hit github because I forgot I wasn't in a private repository, but I can fix that. My personal email is in my github profile.

[dmcclean]

Chasing docs from evByFiat got me to Note [UnivCo] in the GHC comments. Tried to paste it here but it made markdown quite upset, so https://github.com/ghc/ghc/blob/0aaea5b8345fc4b061b97df8bcaa7c6b07594719/compiler/types/Coercion.hs#L438.

I'm not sure how the Role argument ends up playing out. Perhaps the answer to the question of whether there is a problem here is related to a comment in #46, where we were discussing a named-units branch of dimensional-dk that (unfortunately, and at least without addressing GHC ticket 8177), changes the role signature of our Dimensional type constructor from nominal phantom representational to nominal nominal nominal. The second type parameter is the dimension, the one that the solver is equating things between. The Dimensional type family decides on the basis of the first nominal parameter whether to be one type or another, but on either choice the remaining roles are phantom representational, but GHC doesn't see that as a result the whole data family can be viewed to be that way.

So perhaps the faking of the evidence would be more severe if the named-units branch were adopted? Or perhaps not, because I honestly don't understand most of what the GHC note is talking about.

[dmcclean]

In any event it seems possible to cook up the "real" evidence with enough effort, or evidence with the right runtime implementation, because it really is a phantom, so even if there is a problem here there is probably a way around it.

[dmcclean]

WTH is the meaning of the verb "zonk" in the GHC source? There are all sorts of functions for zonking this or that, and comments about the need to zonk or not to zonk various things at various times, but I can't chase down an explanation of what is being talked about, and I can't puzzle it out from the definitions. 😕

More specifically, why do you zonkCt the givens? Or not zonkCt the others?

[dmcclean]

Stackoverflow was able to answer the zonking question.

[adamgundry]

One other worry I have is how does the faking of evidence interact with stuff that converts types to terms
...

1. As long as there aren't mistakes in the solver, it doesn't matter, because the two types equated by the fake evidence are actually equivalent and thus it doesn't matter which we start from to generate the term level representation.

I believe this is the case. GHC's core theory is "proof-irrelevant", which means it doesn't matter how a proof of an equality constraint is constructed, provided the constraint doesn't equate two types that are actually distinguishable. Ultimately nothing is going to look at the proofs, because they are erased at runtime!

This is true regardless of roles. The difference roles make is to the consistency requirement: fake evidence at role nominal must not equate two types that are nominally distinct (e.g. a type and a newtype of it), fake evidence at role representational must not equate two types with different representations (e.g. Int and Bool), while fake evidence at role phantom is basically meaningless and can equate anything it likes.

why do you zonkCt the givens? Or not zonkCt the others?

I wouldn't read too much into this; it's very possibly not the right thing, because my understanding of how zonking works is very limited. I think that GHC will already have zonked the wanteds, but not the givens, by the time it gives them to the plugin.

[dmcclean]

Awesome, thanks.

I think that even though according to the current rules our fake evidence is at role nominal, the consequences don't actually matter because it logically is phantom, it's just that the current compiler can't be convinced of that. Either way it is of no operational significance so there is nothing bad that can happen.

[dmcclean]

@adamgundry Do you know if anything changed in 7.10.2 with respect to this? I have 7.10.1 on my windows machine where the draft plugin works, but then I installed a new ubuntu VM with 7.10.2 because hmatrix is easier to install on linux (vast understatement...) and there it doesn't work. It doesn't report any errors, but it also doesn't solve the constraints that it does on windows/7.10.1.

I read the release notes and nothing jumped out at me except 10321, which doesn't really seem related.

[adamgundry]

@dmcclean I'm not aware of any such changes, but it wouldn't entirely surprise me if minor adjustments to the typechecker were made in 7.10.2, and those might have tripped up the plugin. Unfortunately I don't have much to suggest other than digging through the output of -ddump-tc-trace to look at the constraints being produced...

[dmcclean]

Curiously it looks from comparing the -ddump-tc-trace -ddump-to-file outputs that the plugin isn't being invoked at all on 7.10.2, it doesn't even mention tcPluginInit. I have quadruple-checked for typos but I must be missing one. I intentionally changed the spelling in my -fplugin setting to something incorrect though, and that did produce an error message which I don't get when using the correct spelling.

Something curious is going on here.

I tried to compile your uom-plugin-examples on 7.10.2 to see if that would work, but I got an error about:

Examples.hs:79:8:
    Conflicting family instance declarations:
      CanonicalBaseUnit "ft" -- Defined at Examples.hs:79:8
      CanonicalBaseUnit "ft" -- Defined in ‘Examples’

I will dig further after work.

[adamgundry]

That sounds strange; it seems unlikely, but could you be using a stage1 build of 7.10.2 that doesn't support plugins/TH/GHCi? Or perhaps the -fplugin option is going to the wrong place, if it isn't in the module itself?

Thanks for pointing out the error with uom-plugin-examples: it was a bit out of date, and I've updated it. (A more useful test is cabal test in uom-plugin itself.) It works fine for me on x86_64 Linux Mint (an Ubuntu derivative) with the 7.10.2 binary distribution.

[dmcclean]

The tests in uom-plugin and the revised uom-plugin-examples work on the same system, so I must be goofing something basic somewhere.

The {-# OPTIONS_GHC -fplugin ... } is in the module itself and is getting processed because changing the name of the plugin module to something that doesn't exist causes the compilation to fail.

I'm also on Ubuntu (32 bit though, in a VirtualBox) with 7.10.2 distribution that I got by cargo culting some instructions that used sudo add-apt-repository -y ppa:hvr/ghc ...

[dmcclean]

Found it, it has to do with GHCi.

Your module gets the plugin because the module is being built by cabal repl as part of the .cabal file.

My module didn't get the plugin because I was doing cabal repl for a project that didn't mention it, and then once that was open doing :load examples\Controls.hs. If I add Controls to my cabal file's other-modules: then I get the plugin.

However, on 7.10.1 on windows the :load workflow works and gets the plugin.

Whether it should or shouldn't is above my knowledge, so I don't know if this is a regression or a bug fix. Any thoughts?

[adamgundry]

If Controls.hs includes {-# OPTIONS_GHC -fplugin ... } but the plugin doesn't get run during (interactive) compilation of that module, that sounds like a bug. But GHCi has its own set of options that interact with the options specified by modules in strange ways, e.g. you may need to :seti -fplugin in GHCi for interactive evaluation even if the plugin is enabled on a module you have loaded.

[dmcclean]

I had :set it, I didn't know about :seti. :seti makes it work. On 7.10.1 on windows it doesn't require either :set or :seti.