Unification of type synonyms

[quark17]

I'm opening this bug to record what we know about the issue. The issue is that we have occasionally relied on the typechecker to structurally unifty type aliases. That is, if a value has type T#(x,y) and its context expects T#(a,b), then we rely on BSC to conclude to that x==a and y==b. This first showed up in Bluespec's internal bug 1281, when a Sudoku design created TSquare#(n) as an alias to TMul#(n,n).

The discussion on that internal bug 1281 shows that there are type constructors/functions that shouldn't structurally unify. Unifying TAdd#(x,y) and TAdd#(a,b) does not imply that x==a and y==b. We addressed this by introducing the NumEq typeclass, which can be used to delay unification until more information is known. When we encounter TAdd#(x,y) and TAdd#(a,b) we can replace them with the variable v and add the provisos that NumEq#(v, TAdd#(x,y)) and NumEq#(v, TAdd#(a,b)).

It turns out, though, that structural unification of type synonyms was still happening, and some code relied on it. I have a patch (see below) which expands all synonyms in the symbol table. It exposes a few a places that rely on structural unification -- and specifically also on the ability to bind type variables in function signatures when those variables are arguments to type synonym constructors.

Before I get to that, let me just say that this was uncovered when I added a fix for Bluespec internal bug 1720 (recorded here as #310) that involved adding expandSyn to the handling of struct field updates. expandSyn is a function that expands type synonyms. This exposed a problem in code generation where BSC had a mismatch between a value and its context in the number of type variables that are being passed -- because one side had expanded a type synonym that ignored some of its arguments. An attempted fix for this was to expand type synonyms everywhere (so that the ignored variables were not created on either side), and this exposed the issue.

Then, a fix for Bluespec internal bug 1729 (recorded here as #311) also involved adding expandSyn and that again pointed out how fragile the current handling of type synonyms is in the presence of extra expanding of synonyms.

If we can find fixes for #310 and #311 that don't involve expanding synonyms (or find some other clever way to retain type synonym boundaries), then we could resolve those issues while leaving the current support for unifying type synonyms. But the question is: is that a feature that people should be able to rely on?

One argument against supporting it is that you can define this:

typedef TAdd#(a,b) A#(type a, type b);

Now, while TAdd#(a,b) and TAdd#(x,y) cannot be unified, the user has given implicit permission that A#(a,b) and A#(x,y) can be unified by saying that a==x and b==y. This is what we intend when we create type synonyms for TLM which have a number of parameters, like TLMRequest#(data_size, addr_size). However, what if we created something like this:

typedef Bit#(TAdd#(high_size, low_size)) BusAddr#(type high_size, type low_size);

Actually, maybe this isn't a great example. Because, while BusAddr#(12,20) and BusAddr#(16,16) do unify, we really would prefer that it not.

Anyway, that's one example.

Another example of what goes wrong is this:

typedef Bit#(TLog#(n)) Ptr#(type n);
function Ptr#(type n) maxPtr();
   return fromInteger(valueOf(n));
endfunction

This code can't work if you expand synonyms, because the context is only going to provide Bit#(m) and you can't reconstruct what the n is whose log is m, because multiple values are possible. This is the variable binding issue that I mentioned above. The user can't write this:

function Bit#(TLog#(m)) maxPtr();

because it's impossible to figure out m. Even if the user provided a value defined as:

Bit#(TLog#(32)) m = maxPtr;

The typechecker is not allowed to unify TLog#(32) and TLog#(m) to conclude that m is 32. It only when we use a type alias that we have given BSC permission to unify structurally.

Do we want to support this (which requires alternate fixes to #310 and #311) or do we want to forbid it, for which the attached patch is a start. We'd probably also want to improve error messages by specifically looking for bad type synonyms and reporting specific errors about them.

The patch I mentioned is here: expandSyn_bug1730.patch

This patch expands all synonyms when creating the symbol table. It also puts back in the expandSyn that was backed out in the fixes for #310 and #311. Presumably there are now redundant uses of expandSyn in the compiler, but I'm not sure where to go looking, to remove them.

The patch also includes small fixes to the AHB and Axi libraries to fix functions that were exposed as ambiguous (due to uses of TLog in type synonyms).

This patch is from 2011. At the time, the testsuite had failures in the following locations:

Running ./bsc.bluesim/misc/misc.exp ...
FAIL: module `mkGenerateTest3' in `GenerateTest3.bsv'
Running ./bsc.bsv_examples/sudoku/sudoku.exp ...
FAIL: module `mkGenerateTest3' in `GenerateTest3.bsv'
Running ./bsc.bugs/b1325/b1325.exp ...
FAIL: module `' in `Test5.bsv'
Running ./bsc.bsv_examples/AzureIP/azureip.exp ...
FAIL: module `sysTestDMA' in `TestDMA.bsv'

The first three are uses of TSquare in versions of the Sudoku code. The last one is a use of let that needs to be changed into an explicit type, in the use of a TLM default value.

This is bug 1730 in Bluespec Inc's pre-GitHub bug database.