Better positions for kind-mismatch errors

[quark17]

I wrote this example, where I forgot that the type parameters to RegFile are value types and not the bit sizes:

import RegFile::*;

typedef struct {
} Config #(numeric type sz);

module mkTest #(Config#(sz) cfg) (Empty)
  provisos (
    NumAlias#(addr_sz, TAdd#(sz,2))
  );

  RegFile#(addr_sz, sz) rf <- mkRegFileFull;
  // RegFile#(Bit#(addr_sz), Bit#(sz)) rf <- mkRegFileFull;
endmodule

BSC gave me an error pointing to the NumAlias proviso and not to the source of the error (the RegFile instantiation):

Error: "Test.bsv", line 8, column 24: (T0027)
  The numeric type `TAdd#(sz, 2)' was found where a value type was expected.

If I rewrite the proviso to not use TAdd, the position improves, to point to the instantiation:

Add#(sz, 2, addr_sz)

Error: "Test.bsv", line 12, column 12: (T0027)
  The numeric type `addr_sz' was found where a value type was expected.

It's specifically the TAdd and not the use of NumAlias as confirmed by replacing the proviso with these other two options, which point to the instantiation and the proviso, respectively:

NumAlias#(addrs_sz, sz)

Add#(TAdd#(sz,2), 0, addr_sz)

Looking in Bluespec Inc's proprietary bug database (pre-GitHub), I see several relevant issues. This exact issue was reported as Bug 1869, with the following example, where the problem isn't numeric-vs-value kind mismatch but wrong number of type parameters (also a form of kind mismatch):

interface Ifc#(type a);
   method Action put(a x);
endinterface

module mkMod (Ifc#(a));
   method put(x) = noAction;
endmodule

module mkTest (Reg#(Bit#(ndw)))
  provisos (NumAlias#(TMul#(ndw,32),nd));

  // Source of the error is the wrong type arguments in this line
  Ifc#(nd,0) m <- mkMod;
endmodule

There is also Bug 1418, which is about improving the position information in errors. The following comments are on that bug entry:

As a result of the fix to bug1414, messages like this:

Error: "CDeflBSV.bsv", line 6, column 11: (T0068)
   Kind mismatch on bound type variable 'a'.
   The variable has kind '#' at position:
     "CDeflBSV.bsv", line 6, column 8
   The variable has kind '*' at position:
     "CDeflBSV.bsv", line 5, column 23

Are now reported like this:

Error: "CDeflBSV.bsv", line 6, column 8: (T0026)
   The non-numeric type `a' was found where a numeric type was expected.

The message is friendlier, but it loses the position of where the bound variable first appeared (and its kind first inferred).

If possible, kind-mismatch errors should report a location for where it inferred the given type. At least if the type is a tyvar (such as "a" in this example). For a type like "Bool", obviously the position is where Bool was defined, which is not useful.

There are two places in KIMisc where these "nice" messages come out: "unifyDef" (which just has the Id, not the Type! so it doesn't know if it's a tyvar!) and "unifyFunc" (which does have the Type, so it has some hope of knowing if it's a tyvar). Unfortunately, KVar does not have a position. So there is not currently a way of getting the position of the expected kind from the kind itself. (The way that the bound variable kind gets inserted into the type is via a list of assumptions passed to "MakeSymTab.convCTypeAssumps" which then gives that list to "trCType" which looks up tyvars in the type and replaces their kind with the kinds from the assumptions. It is here that we lose the position of the Id in the assumption list, when we just take its kind, which has no position.)

See all the examples in bsc.typechecker/kind/bound-vars/

Another possibility is that if the boundvar assumptions were stored in the KI monad, then when a kind-mismatch error came up, we could look up the tyvar in the list of assumptions in the state. That might be simpler than adding a Position to all the Kind values everywhere.

That is, "MakeSymTab.convCQTypeVars" would be made to push the list of assumptions onto the monad. (And the interface between "convCQTypeWithAssumps" and "convCQTypeVars" would have to change slightly, to pass the assumptions in.)

On a related note, see Comment 2 on Bug 992. The file Alias.bsv exhibits the new error message, which would benefit from two positions. Further, the example shows another failure of the new message: getting found-vs-expected in the wrong order.

In revision 24232, two testcases were added for when there's a kind mismatch between two provisos:

bsc.typechecker/kind/mismatch/ProvisoProvisoMismatch_TopLevel.bsv
bsc.typechecker/kind/mismatch/ProvisoProvisoMismatch_Local.bsv

In this case, the order of the provisos can affect whether BSC first assumes the variable is numeric or non-numeric. And reporting both locations would be helpful.

It mentions two locations in the testsuite for finding more examples.

It also mentions Bug 992, which has the following example, where a kind mismatch results because BSC couldn't infer the kinds of the parameters to MyAlias and so picked them to be value kinds by default (the user could add "numeric" to specify numeric instead):

typeclass MyAlias#(type a, type b);
endtypeclass

instance MyAlias#(a,a);
endinstance

typedef 25 DELAY;
typedef 10 SLACK;

module mkTest (Empty)
   provisos (MyAlias#(TLog#(TAdd#(DELAY, SLACK)), capSize) );

   Reg#(Bit#(capSize)) r <- mkRegU;
endmodule

This is related to Bug 1032 which is about the fact that kind inference of top-level types occurs first, before type-checking of top-level values. This means that uses of the type in top-level function/module signatures isn't used to help infer the kinds of the type parameters. If the kind of type parameters can't be worked out from just looking at top-level types, then BSC chooses them to be of value kind by default; and then a mismatch can occur, when typechecking the functions/modules that expect a different kind (like numeric).