SizeOf remains after typecheck

[quark17]

The testsuite example bsc.typechecker/primtcons/ExpSizeOf_FieldSyn.bsv leads to this internal error:

Internal Bluespec Compiler Error:
...
AConv.aExpr at "ExpSizeOf_FieldSyn.bsv", line 6, column 5:PrimSelect ?3 ?(Prelude.SizeOf (Prelude.UInt 3)) ?6 _x__h90

"ExpSizeOf_FieldSyn.bsv", line 6, column 5:(IAps (ICon Prelude::primSelect (ICPrim _ PrimSelect) ) _ [(ICon _x__h90[IdP_bad_name,IdP_keep] (ICValue) )])

The AConv failure is due to the numeric type operators not being simplified during elaboration. The conversion function aExpr is expecting PrimSelect to have constant numeric type arguments, but the argument containing Prelude.SizeOf is unreduced.

This can be fixed by changing the following line in TCheck.tiField1:

-- XXX disable expanding of type synonyms until failures with TLM
-- XXX (type synonyms which drop parameters) is resolved
-- XXX (tcon_ps, ft) <- expPrimTCons (expandSyn ft0)
(tcon_ps, ft) <- expPrimTCons ft0

to be this:

(tcon_ps, ft) <- expPrimTCons (expandSyn ft0)

However, as the comment says, when we expand synonyms here, it causes AHB/Axi libraries (now in the bsc-contrib repo) to fail to compile. (Specifically, the functions getAHBSize, fromAHBSize, getAxiSize, and fromAxiSize.) This is because there are functions with prototypes like this:

function AHBSize getAHBSize(TLMBurstSize#(`TLM_PRM) incr);

function TLMBurstSize#(`TLM_PRM) fromAHBSize(AHBSize size);

where:

typedef Bit#(TLog#(TDiv#(data_size, 8))) TLMBurstSize#(`TLM_PRM_DCL);

The problem here is that the type alias drops many of the type variable. These definitions only work if type inference can unify against the alias with all its types -- when the alias synonym is expanded away, type inference fails. The TLMBurstSize type would need to be a true newtype (and not a macro) for this to work. BSC is being held back from expanding synonyms, to make this code work (mostly). I think that the TLM code should be rewritten, and BSC's expandSyn should be reinstated.

The TLM code can be changed to just use Bit#(n) (or Bit#(burst_size)) instead of TLMBurstSize#(`TLM_PRM). Or TLMBurstSize can be written as a real type, either by supporting actual newtype in BSC, or with a workaround like this:

 typedef struct {
      Bit#(TLog#(TDiv#(...))) bits;
   } TLMBurstSize#(...) deriving (Eq, Bits, Literal, Arith, ...);

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

Note that there is also an expandSyn in CtxRed that has been commented out, because of the TLM packages. That relates to an example that is filed as bug 1729 in Bluespec's database. Rather than make this issue entry longer, I'll file that as a separate issue here, too.

It's also possible that bsc.bsv-examples/AzureIP/TestDMA.bsv fails to compile, when one or both of these expansions are introduced.