Type synonyms with phantom parameters can lead to strange behaviors (E.g., compiler hang)

[rossc719g]

For example:

package PhantomAlias where

import Vector

-- Split a vector into many vectors of the same length.
splitN :: (Div len k n, Mul k n len, Add n n__ len) =>
  Vector len a -> Vector k (Vector n a)
splitN v = let getChunk :: Integer -> Vector n a
               getChunk i = takeAt ((valueOf n) * i) v
           in map getChunk genVector

type (PhantomVec :: # -> # -> * -> *) n k t = Vector n t
type PhantomVecReg n k t = Reg (PhantomVec n k t)

-- interface (PhantomVecReg :: # -> # -> * -> *) n k t =
--   _read  :: Vector n t            {-# always_ready #-}
--   _write :: Vector n t -> Action  {-# always_ready, always_enabled #-}

mkPhantomVecReg :: (IsModule m c, Bits t t_sz,  -- Add k k__ n,
                    Div n k w, Div n w k, Mul w k n) => m (PhantomVecReg n k t)
mkPhantomVecReg = module

  inVec :: Vector n (Wire t)
  inVec <- replicateM mkBypassWire

  let splitVec :: Vector w (Vector k t)
      splitVec = splitN $ readVReg inVec

  interface PhantomVecReg
    _read    = concat $ reverse splitVec
    _write i = zipWithM_ writeReg inVec i

mkPhantomVecRegDut :: (IsModule m c) => m (PhantomVecReg 6 2 (UInt 8))
mkPhantomVecRegDut = mkPhantomVecReg

As written, compiling with -g mkPhantomVecRegDut -verilog this will generate two errors, and then hang the compiler.

If you use the commented out interface (instead of the two type aliases), it will just give errors and not hang.
If you add the missing Add k k__ n proviso, it will give an error, and not hang.

I talked it over with @nanavati, and he said that type synonyms with phantom parameters should just be an error flat out, and that since they are not being flagged as an error, the compiler is free to go off in the weeds and get stuck.

Should type synonyms with phantom parameters just be a fatal error?

[quark17]

Yes, I would like for type synonyms with unused parameters to be illegal; but a reason why they are not is because it is used in the TLM packages (in the bsc-contrib repo). If we can find a way to rewrite those packages, then yes we can make such type synonyms illegal. Finding a way to rewrite those packages would also allow a number of other improvements around type synonyms. See the related isuse #312 , which summarizes how BSC is currently allowing structural unification on type synonyms. See also #310 and #311 which are about places in BSC where typedefs should be fully inlined, but we are holding back in order to allow, for instance, structural unification. And #221 which is about forbidding partial application of type synonyms. Type synonyms have no substance and it should be legal to immediately inline them, and for the code to still be valid -- phantom parameters violate that (when they are used to for unfication and binding of names). As an aside, we might consider whether there is kind of data type that is between a user type and a synonym, that has substance, which we could add a creation mechanism for to BSC, but off-hand I don't see that there is.

An example of phantom parameters in the TLM library is here. They look like this:

typedef Bit#(addr_size)  TLMAddr#(`TLM_PRM_DCL);

Where the macro is defined in TLM.defines:

`define TLM_PRM_DCL numeric type id_size,   \
	            numeric type addr_size, \
		    numeric type data_size, \
		    numeric type length_size, \
		    numeric type user_size

`define TLM_PRM    id_size,   \
	           addr_size, \
	           data_size, \
		   length_size, \
		   user_size

`define TLM_PRM_STD 4,  \
                    32, \
		    32, \
                    8, \
                    0

The typedef acts as a way of selecting out on of the parameters. For example, here:

typedef struct {TLMData#(`TLM_PRM)   data;
		TLMUser#(`TLM_PRM)   user;
		TLMBEKind#(`TLM_PRM) byte_enable;
		TLMId#(`TLM_PRM)     transaction_id;
		Bool                 is_last;
                } RequestData#(`TLM_PRM_DCL) deriving (Eq, Bits, Bounded);

which could be manually written out, since it's all still part of the library, but then in user code, you can also use it:

module mkAxi4RdMasterIFC#(BusSend#(Axi4AddrCmd#(`TLM_PRM))  request_addr,
			  BusRecv#(Axi4RdResp#(`TLM_PRM))   response) (Axi4RdMaster#(`TLM_PRM));

   Wire#(AxiId#(`TLM_PRM))   rID_wire   <- mkBypassWire;
   Wire#(AxiData#(`TLM_PRM)) rDATA_wire <- mkBypassWire;
   ...

Some of these could be done away with by introducing a typeclass:

typeclass TLMAddr#(full_type, addr_type) dependencies (full_type -> addr_type);
endtypeclass

instance TLMId#( TLMDummy#(`TLM_PRM_DCL), addr_size );
endinstance

However, there are some places where this couldn't be used -- for example, the struct declaration of RequestData. There, it would be necessary to allow some kind of user-defined type constructor -- possibly automatically defined based on the typeclass.

Or maybe there's a better way to write the TLM libraries that doesn't need any of this machinery.

And maybe someone wants to argue that we don't need to fix the TLM libraries before fixing BSC.

But it'd be great to figure out how we can move forward on fixing all of these known issues with type synonyms. And, yes, don't ever write new code that has phantom variables.

The hanging behavior that you describe is new to me. I'd have to look into it, to see what's going on.

[quark17]

I guess a possible fix for the TLM libraries would be to make these real data types and not type aliases. Anywhere that TLMAddr#(`TLM_PRM) needs to be used a Bit vector, an explicit pack can be added. This would also add some type safety -- if, for example, the addr and data sizes are both 32, a user could accidentally mix up values and BSC would not currently report an error, because it doesn't see them as different types. So maybe that's an extremely simple fix for the libraries?

[rossc719g]

I am curious to see if anyone can repro the hanging behavior.

It's interesting that it is possible to write code that is reliant on a feature that is so strongly discouraged. Is there a reason it is not supported? I could be way off base here, but it felt like a reasonable thing to try to do when I originally wrote the code that used it. I was surprised to find that it is (or should be) illegal.

[quark17]

A type synonym is not a new type, it's just an alias, and you are allowed to use it interchangeably. If you define this:

typedef Bit#(8) Byte;

You're allowed to pass values declared as type Byte to functions defined on type Bit n without having convert between Byte and Bit#(8) (say, with pack and unpack):

fn :: Bit n -> Bit n
fn = ...

x :: Byte
x = ...

y :: Bit 8
y = fn x

So with your definition of mkPhantomVecReg, I ought to be able to call it like this:

m :: Reg (Vector 6 (UInt 8))
m <- mkPhantomVecReg

But then where is mkPhantomVecReg getting its variable k from? The context where I've called it doesn't have such a parameter.

If PhantomVec or PhantomVecReg were a real type, then there'd be no problem using mkPhantomVecReg -- it's just that the context would be forced to be rewritten to expect that real type (and then explicitly convert it to an ordinary Reg or Vector if needed). But we've declared as an alias, as not a real type. We can't have the type both ways.

(I guess, technically, the only thing that BSC needs to disallow is the definition of mkPhantomVecReg which attempts to bind the phantom variable from the context. BSC could still allow such synonyms to be defined and to allow other uses, like what the TLM library does. Off-hand, I'm not sure how hard it would be to detect these uses; it's certainly easier to detect the phantom variables in the synonym declaration.)